Hets - the Heterogeneous Tool Set

Copyright(c) Christian Maeder and Uni Bremen 2003-2005
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityexperimental
Portabilityportable
Safe HaskellSafe

HasCASL.As

Contents

Description

abstract syntax for HasCASL, more liberal than Concrete-Syntax.txt, annotations are almost as for CASL

Synopsis

abstract syntax entities with small utility functions

data BasicSpec Source #

annotated basic items

Constructors

BasicSpec [Annoted BasicItem] 

Instances

Data BasicSpec Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BasicSpec -> c BasicSpec

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BasicSpec

toConstr :: BasicSpec -> Constr

dataTypeOf :: BasicSpec -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c BasicSpec)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BasicSpec)

gmapT :: (forall b. Data b => b -> b) -> BasicSpec -> BasicSpec

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BasicSpec -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BasicSpec -> r

gmapQ :: (forall d. Data d => d -> u) -> BasicSpec -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> BasicSpec -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BasicSpec -> m BasicSpec

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BasicSpec -> m BasicSpec

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BasicSpec -> m BasicSpec

Show BasicSpec Source # 

Methods

showsPrec :: Int -> BasicSpec -> ShowS

show :: BasicSpec -> String

showList :: [BasicSpec] -> ShowS

GetRange BasicSpec Source # 
Syntax HasCASL BasicSpec Symbol SymbItems SymbMapItems Source # 
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source # 

Methods

basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source #

sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source #

stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source #

convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source #

ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source #

signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source #

qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source #

symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source #

id_to_raw :: HasCASL -> Id -> RawSymbol Source #

matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: HasCASL -> Env Source #

add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source #

signature_union :: HasCASL -> Env -> Env -> Result Env Source #

signatureDiff :: HasCASL -> Env -> Env -> Result Env Source #

intersection :: HasCASL -> Env -> Env -> Result Env Source #

final_union :: HasCASL -> Env -> Env -> Result Env Source #

morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: HasCASL -> Env -> Env -> Bool Source #

subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source #

generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source #

cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source #

induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source #

induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source #

is_transportable :: HasCASL -> Morphism -> Bool Source #

is_injective :: HasCASL -> Morphism -> Bool Source #

theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #

Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source #

stability :: HasCASL -> Stability Source #

data_logic :: HasCASL -> Maybe AnyLogic Source #

top_sublogic :: HasCASL -> Sublogic Source #

all_sublogics :: HasCASL -> [Sublogic] Source #

bottomSublogic :: HasCASL -> Maybe Sublogic Source #

sublogicDimensions :: HasCASL -> [[Sublogic]] Source #

parseSublogic :: HasCASL -> String -> Maybe Sublogic Source #

proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source #

provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source #

default_prover :: HasCASL -> String Source #

cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source #

conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source #

empty_proof_tree :: HasCASL -> () Source #

syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source #

omdoc_metatheory :: HasCASL -> Maybe OMCD Source #

export_symToOmdoc :: HasCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source #

addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source #

Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 

data BasicItem Source #

the possible items

Instances

Data BasicItem Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BasicItem -> c BasicItem

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BasicItem

toConstr :: BasicItem -> Constr

dataTypeOf :: BasicItem -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c BasicItem)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BasicItem)

gmapT :: (forall b. Data b => b -> b) -> BasicItem -> BasicItem

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BasicItem -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BasicItem -> r

gmapQ :: (forall d. Data d => d -> u) -> BasicItem -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> BasicItem -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BasicItem -> m BasicItem

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BasicItem -> m BasicItem

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BasicItem -> m BasicItem

Show BasicItem Source # 

Methods

showsPrec :: Int -> BasicItem -> ShowS

show :: BasicItem -> String

showList :: [BasicItem] -> ShowS

data SigItems Source #

signature items are types or functions

Instances

Data SigItems Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SigItems -> c SigItems

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SigItems

toConstr :: SigItems -> Constr

dataTypeOf :: SigItems -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SigItems)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SigItems)

gmapT :: (forall b. Data b => b -> b) -> SigItems -> SigItems

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SigItems -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SigItems -> r

gmapQ :: (forall d. Data d => d -> u) -> SigItems -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SigItems -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SigItems -> m SigItems

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SigItems -> m SigItems

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SigItems -> m SigItems

Show SigItems Source # 

Methods

showsPrec :: Int -> SigItems -> ShowS

show :: SigItems -> String

showList :: [SigItems] -> ShowS

data OpBrand Source #

indicator for predicate, operation or function

Constructors

Pred 
Op 
Fun 

Instances

Eq OpBrand Source # 

Methods

(==) :: OpBrand -> OpBrand -> Bool

(/=) :: OpBrand -> OpBrand -> Bool

Data OpBrand Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpBrand -> c OpBrand

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpBrand

toConstr :: OpBrand -> Constr

dataTypeOf :: OpBrand -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c OpBrand)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpBrand)

gmapT :: (forall b. Data b => b -> b) -> OpBrand -> OpBrand

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpBrand -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpBrand -> r

gmapQ :: (forall d. Data d => d -> u) -> OpBrand -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> OpBrand -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpBrand -> m OpBrand

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpBrand -> m OpBrand

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpBrand -> m OpBrand

Ord OpBrand Source # 

Methods

compare :: OpBrand -> OpBrand -> Ordering

(<) :: OpBrand -> OpBrand -> Bool

(<=) :: OpBrand -> OpBrand -> Bool

(>) :: OpBrand -> OpBrand -> Bool

(>=) :: OpBrand -> OpBrand -> Bool

max :: OpBrand -> OpBrand -> OpBrand

min :: OpBrand -> OpBrand -> OpBrand

Show OpBrand Source # 

Methods

showsPrec :: Int -> OpBrand -> ShowS

show :: OpBrand -> String

showList :: [OpBrand] -> ShowS

isPred :: OpBrand -> Bool Source #

test if the function was declared as predicate

data Instance Source #

indicator in ClassItems and TypeItems

Constructors

Instance 
Plain 

Instances

Eq Instance Source # 

Methods

(==) :: Instance -> Instance -> Bool

(/=) :: Instance -> Instance -> Bool

Data Instance Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Instance -> c Instance

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Instance

toConstr :: Instance -> Constr

dataTypeOf :: Instance -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Instance)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Instance)

gmapT :: (forall b. Data b => b -> b) -> Instance -> Instance

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Instance -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Instance -> r

gmapQ :: (forall d. Data d => d -> u) -> Instance -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Instance -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Instance -> m Instance

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Instance -> m Instance

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Instance -> m Instance

Ord Instance Source # 

Methods

compare :: Instance -> Instance -> Ordering

(<) :: Instance -> Instance -> Bool

(<=) :: Instance -> Instance -> Bool

(>) :: Instance -> Instance -> Bool

(>=) :: Instance -> Instance -> Bool

max :: Instance -> Instance -> Instance

min :: Instance -> Instance -> Instance

Show Instance Source # 

Methods

showsPrec :: Int -> Instance -> ShowS

show :: Instance -> String

showList :: [Instance] -> ShowS

data ClassItem Source #

a class item

Instances

Data ClassItem Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ClassItem -> c ClassItem

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ClassItem

toConstr :: ClassItem -> Constr

dataTypeOf :: ClassItem -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ClassItem)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ClassItem)

gmapT :: (forall b. Data b => b -> b) -> ClassItem -> ClassItem

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ClassItem -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ClassItem -> r

gmapQ :: (forall d. Data d => d -> u) -> ClassItem -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ClassItem -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ClassItem -> m ClassItem

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ClassItem -> m ClassItem

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ClassItem -> m ClassItem

Show ClassItem Source # 

Methods

showsPrec :: Int -> ClassItem -> ShowS

show :: ClassItem -> String

showList :: [ClassItem] -> ShowS

data ClassDecl Source #

declaring class identifiers

Constructors

ClassDecl [Id] Kind Range 

Instances

Data ClassDecl Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ClassDecl -> c ClassDecl

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ClassDecl

toConstr :: ClassDecl -> Constr

dataTypeOf :: ClassDecl -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ClassDecl)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ClassDecl)

gmapT :: (forall b. Data b => b -> b) -> ClassDecl -> ClassDecl

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ClassDecl -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ClassDecl -> r

gmapQ :: (forall d. Data d => d -> u) -> ClassDecl -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ClassDecl -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ClassDecl -> m ClassDecl

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ClassDecl -> m ClassDecl

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ClassDecl -> m ClassDecl

Show ClassDecl Source # 

Methods

showsPrec :: Int -> ClassDecl -> ShowS

show :: ClassDecl -> String

showList :: [ClassDecl] -> ShowS

data Variance Source #

co- or contra- variance indicator

Constructors

InVar 
CoVar 
ContraVar 
NonVar 

Instances

Eq Variance Source # 

Methods

(==) :: Variance -> Variance -> Bool

(/=) :: Variance -> Variance -> Bool

Data Variance Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Variance -> c Variance

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Variance

toConstr :: Variance -> Constr

dataTypeOf :: Variance -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Variance)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Variance)

gmapT :: (forall b. Data b => b -> b) -> Variance -> Variance

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Variance -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Variance -> r

gmapQ :: (forall d. Data d => d -> u) -> Variance -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Variance -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Variance -> m Variance

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Variance -> m Variance

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Variance -> m Variance

Ord Variance Source # 

Methods

compare :: Variance -> Variance -> Ordering

(<) :: Variance -> Variance -> Bool

(<=) :: Variance -> Variance -> Bool

(>) :: Variance -> Variance -> Bool

(>=) :: Variance -> Variance -> Bool

max :: Variance -> Variance -> Variance

min :: Variance -> Variance -> Variance

Show Variance Source # 

Methods

showsPrec :: Int -> Variance -> ShowS

show :: Variance -> String

showList :: [Variance] -> ShowS

data AnyKind a Source #

(higher) kinds

Constructors

ClassKind a 
FunKind Variance (AnyKind a) (AnyKind a) Range 

Instances

Ord a => Eq (AnyKind a) Source # 

Methods

(==) :: AnyKind a -> AnyKind a -> Bool

(/=) :: AnyKind a -> AnyKind a -> Bool

Data a => Data (AnyKind a) Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AnyKind a -> c (AnyKind a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (AnyKind a)

toConstr :: AnyKind a -> Constr

dataTypeOf :: AnyKind a -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (AnyKind a))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (AnyKind a))

gmapT :: (forall b. Data b => b -> b) -> AnyKind a -> AnyKind a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AnyKind a -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AnyKind a -> r

gmapQ :: (forall d. Data d => d -> u) -> AnyKind a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> AnyKind a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AnyKind a -> m (AnyKind a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AnyKind a -> m (AnyKind a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AnyKind a -> m (AnyKind a)

Ord a => Ord (AnyKind a) Source # 

Methods

compare :: AnyKind a -> AnyKind a -> Ordering

(<) :: AnyKind a -> AnyKind a -> Bool

(<=) :: AnyKind a -> AnyKind a -> Bool

(>) :: AnyKind a -> AnyKind a -> Bool

(>=) :: AnyKind a -> AnyKind a -> Bool

max :: AnyKind a -> AnyKind a -> AnyKind a

min :: AnyKind a -> AnyKind a -> AnyKind a

Show a => Show (AnyKind a) Source # 

Methods

showsPrec :: Int -> AnyKind a -> ShowS

show :: AnyKind a -> String

showList :: [AnyKind a] -> ShowS

data TypeItem Source #

the possible type items

Instances

Data TypeItem Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeItem -> c TypeItem

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeItem

toConstr :: TypeItem -> Constr

dataTypeOf :: TypeItem -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c TypeItem)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeItem)

gmapT :: (forall b. Data b => b -> b) -> TypeItem -> TypeItem

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeItem -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeItem -> r

gmapQ :: (forall d. Data d => d -> u) -> TypeItem -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeItem -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeItem -> m TypeItem

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeItem -> m TypeItem

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeItem -> m TypeItem

Show TypeItem Source # 

Methods

showsPrec :: Int -> TypeItem -> ShowS

show :: TypeItem -> String

showList :: [TypeItem] -> ShowS

data Vars Source #

a tuple pattern for SubtypeDefn

Constructors

Var Id 
VarTuple [Vars] Range 

Instances

Eq Vars Source # 

Methods

(==) :: Vars -> Vars -> Bool

(/=) :: Vars -> Vars -> Bool

Data Vars Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Vars -> c Vars

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Vars

toConstr :: Vars -> Constr

dataTypeOf :: Vars -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Vars)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Vars)

gmapT :: (forall b. Data b => b -> b) -> Vars -> Vars

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Vars -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Vars -> r

gmapQ :: (forall d. Data d => d -> u) -> Vars -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Vars -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Vars -> m Vars

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Vars -> m Vars

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Vars -> m Vars

Ord Vars Source # 

Methods

compare :: Vars -> Vars -> Ordering

(<) :: Vars -> Vars -> Bool

(<=) :: Vars -> Vars -> Bool

(>) :: Vars -> Vars -> Bool

(>=) :: Vars -> Vars -> Bool

max :: Vars -> Vars -> Vars

min :: Vars -> Vars -> Vars

Show Vars Source # 

Methods

showsPrec :: Int -> Vars -> ShowS

show :: Vars -> String

showList :: [Vars] -> ShowS

data TypePattern Source #

the lhs of most type items

Instances

Data TypePattern Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypePattern -> c TypePattern

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypePattern

toConstr :: TypePattern -> Constr

dataTypeOf :: TypePattern -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c TypePattern)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypePattern)

gmapT :: (forall b. Data b => b -> b) -> TypePattern -> TypePattern

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypePattern -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypePattern -> r

gmapQ :: (forall d. Data d => d -> u) -> TypePattern -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TypePattern -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypePattern -> m TypePattern

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypePattern -> m TypePattern

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypePattern -> m TypePattern

Show TypePattern Source # 

Methods

showsPrec :: Int -> TypePattern -> ShowS

show :: TypePattern -> String

showList :: [TypePattern] -> ShowS

GetRange TypePattern Source # 

data Type Source #

types based on variable or constructor names and applications

Instances

Eq Type Source # 

Methods

(==) :: Type -> Type -> Bool

(/=) :: Type -> Type -> Bool

Data Type Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type -> c Type

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type

toConstr :: Type -> Constr

dataTypeOf :: Type -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Type)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)

gmapT :: (forall b. Data b => b -> b) -> Type -> Type

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r

gmapQ :: (forall d. Data d => d -> u) -> Type -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Type -> m Type

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type

Ord Type Source # 

Methods

compare :: Type -> Type -> Ordering

(<) :: Type -> Type -> Bool

(<=) :: Type -> Type -> Bool

(>) :: Type -> Type -> Bool

(>=) :: Type -> Type -> Bool

max :: Type -> Type -> Type

min :: Type -> Type -> Type

Show Type Source # 

Methods

showsPrec :: Int -> Type -> ShowS

show :: Type -> String

showList :: [Type] -> ShowS

GetRange Type Source # 

mapTypeOfScheme :: (Type -> Type) -> TypeScheme -> TypeScheme Source #

change the type within a scheme

data TypeScheme Source #

a type with bound type variables. The bound variables within the scheme should have negative numbers in the order given by the type argument list. The type arguments store proper kinds (including downsets) whereas the kind within the type names are only raw kinds.

Constructors

TypeScheme [TypeArg] Type Range 

Instances

Eq TypeScheme Source # 

Methods

(==) :: TypeScheme -> TypeScheme -> Bool

(/=) :: TypeScheme -> TypeScheme -> Bool

Data TypeScheme Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeScheme -> c TypeScheme

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeScheme

toConstr :: TypeScheme -> Constr

dataTypeOf :: TypeScheme -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c TypeScheme)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeScheme)

gmapT :: (forall b. Data b => b -> b) -> TypeScheme -> TypeScheme

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeScheme -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeScheme -> r

gmapQ :: (forall d. Data d => d -> u) -> TypeScheme -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeScheme -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeScheme -> m TypeScheme

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeScheme -> m TypeScheme

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeScheme -> m TypeScheme

Ord TypeScheme Source # 
Show TypeScheme Source # 

Methods

showsPrec :: Int -> TypeScheme -> ShowS

show :: TypeScheme -> String

showList :: [TypeScheme] -> ShowS

GetRange TypeScheme Source # 

data Partiality Source #

indicator for partial or total functions

Constructors

Partial 
Total 

Instances

Eq Partiality Source # 

Methods

(==) :: Partiality -> Partiality -> Bool

(/=) :: Partiality -> Partiality -> Bool

Data Partiality Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Partiality -> c Partiality

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Partiality

toConstr :: Partiality -> Constr

dataTypeOf :: Partiality -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Partiality)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Partiality)

gmapT :: (forall b. Data b => b -> b) -> Partiality -> Partiality

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Partiality -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Partiality -> r

gmapQ :: (forall d. Data d => d -> u) -> Partiality -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Partiality -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Partiality -> m Partiality

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Partiality -> m Partiality

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Partiality -> m Partiality

Ord Partiality Source # 
Show Partiality Source # 

Methods

showsPrec :: Int -> Partiality -> ShowS

show :: Partiality -> String

showList :: [Partiality] -> ShowS

data OpItem Source #

function declarations or definitions

Instances

Data OpItem Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpItem -> c OpItem

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpItem

toConstr :: OpItem -> Constr

dataTypeOf :: OpItem -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c OpItem)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpItem)

gmapT :: (forall b. Data b => b -> b) -> OpItem -> OpItem

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpItem -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpItem -> r

gmapQ :: (forall d. Data d => d -> u) -> OpItem -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> OpItem -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpItem -> m OpItem

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpItem -> m OpItem

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpItem -> m OpItem

Show OpItem Source # 

Methods

showsPrec :: Int -> OpItem -> ShowS

show :: OpItem -> String

showList :: [OpItem] -> ShowS

data BinOpAttr Source #

attributes without arguments for binary functions

Constructors

Assoc 
Comm 
Idem 

Instances

Eq BinOpAttr Source # 

Methods

(==) :: BinOpAttr -> BinOpAttr -> Bool

(/=) :: BinOpAttr -> BinOpAttr -> Bool

Data BinOpAttr Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BinOpAttr -> c BinOpAttr

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BinOpAttr

toConstr :: BinOpAttr -> Constr

dataTypeOf :: BinOpAttr -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c BinOpAttr)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BinOpAttr)

gmapT :: (forall b. Data b => b -> b) -> BinOpAttr -> BinOpAttr

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BinOpAttr -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BinOpAttr -> r

gmapQ :: (forall d. Data d => d -> u) -> BinOpAttr -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> BinOpAttr -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BinOpAttr -> m BinOpAttr

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BinOpAttr -> m BinOpAttr

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BinOpAttr -> m BinOpAttr

Ord BinOpAttr Source # 

Methods

compare :: BinOpAttr -> BinOpAttr -> Ordering

(<) :: BinOpAttr -> BinOpAttr -> Bool

(<=) :: BinOpAttr -> BinOpAttr -> Bool

(>) :: BinOpAttr -> BinOpAttr -> Bool

(>=) :: BinOpAttr -> BinOpAttr -> Bool

max :: BinOpAttr -> BinOpAttr -> BinOpAttr

min :: BinOpAttr -> BinOpAttr -> BinOpAttr

Show BinOpAttr Source # 

Methods

showsPrec :: Int -> BinOpAttr -> ShowS

show :: BinOpAttr -> String

showList :: [BinOpAttr] -> ShowS

data OpAttr Source #

possible function attributes (including a term as a unit element)

Instances

Eq OpAttr Source # 

Methods

(==) :: OpAttr -> OpAttr -> Bool

(/=) :: OpAttr -> OpAttr -> Bool

Data OpAttr Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpAttr -> c OpAttr

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpAttr

toConstr :: OpAttr -> Constr

dataTypeOf :: OpAttr -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c OpAttr)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpAttr)

gmapT :: (forall b. Data b => b -> b) -> OpAttr -> OpAttr

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpAttr -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpAttr -> r

gmapQ :: (forall d. Data d => d -> u) -> OpAttr -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> OpAttr -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpAttr -> m OpAttr

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpAttr -> m OpAttr

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpAttr -> m OpAttr

Ord OpAttr Source # 

Methods

compare :: OpAttr -> OpAttr -> Ordering

(<) :: OpAttr -> OpAttr -> Bool

(<=) :: OpAttr -> OpAttr -> Bool

(>) :: OpAttr -> OpAttr -> Bool

(>=) :: OpAttr -> OpAttr -> Bool

max :: OpAttr -> OpAttr -> OpAttr

min :: OpAttr -> OpAttr -> OpAttr

Show OpAttr Source # 

Methods

showsPrec :: Int -> OpAttr -> ShowS

show :: OpAttr -> String

showList :: [OpAttr] -> ShowS

GetRange OpAttr Source # 

data DatatypeDecl Source #

a polymorphic data type declaration with a deriving clause

Instances

Data DatatypeDecl Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DatatypeDecl -> c DatatypeDecl

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DatatypeDecl

toConstr :: DatatypeDecl -> Constr

dataTypeOf :: DatatypeDecl -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c DatatypeDecl)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DatatypeDecl)

gmapT :: (forall b. Data b => b -> b) -> DatatypeDecl -> DatatypeDecl

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DatatypeDecl -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DatatypeDecl -> r

gmapQ :: (forall d. Data d => d -> u) -> DatatypeDecl -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DatatypeDecl -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DatatypeDecl -> m DatatypeDecl

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DatatypeDecl -> m DatatypeDecl

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DatatypeDecl -> m DatatypeDecl

Show DatatypeDecl Source # 

Methods

showsPrec :: Int -> DatatypeDecl -> ShowS

show :: DatatypeDecl -> String

showList :: [DatatypeDecl] -> ShowS

data Alternative Source #

Alternatives are subtypes or a constructor with a list of (curried) tuples as arguments. Only the components of the first tuple can be addressed by the places of the mixfix constructor.

Instances

Data Alternative Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Alternative -> c Alternative

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Alternative

toConstr :: Alternative -> Constr

dataTypeOf :: Alternative -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Alternative)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Alternative)

gmapT :: (forall b. Data b => b -> b) -> Alternative -> Alternative

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Alternative -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Alternative -> r

gmapQ :: (forall d. Data d => d -> u) -> Alternative -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Alternative -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Alternative -> m Alternative

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Alternative -> m Alternative

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Alternative -> m Alternative

Show Alternative Source # 

Methods

showsPrec :: Int -> Alternative -> ShowS

show :: Alternative -> String

showList :: [Alternative] -> ShowS

data Component Source #

A component is a type with on optional (only pre- or postfix) selector function.

Instances

Eq Component Source # 

Methods

(==) :: Component -> Component -> Bool

(/=) :: Component -> Component -> Bool

Data Component Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Component -> c Component

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Component

toConstr :: Component -> Constr

dataTypeOf :: Component -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Component)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Component)

gmapT :: (forall b. Data b => b -> b) -> Component -> Component

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Component -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Component -> r

gmapQ :: (forall d. Data d => d -> u) -> Component -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Component -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Component -> m Component

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Component -> m Component

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Component -> m Component

Ord Component Source # 

Methods

compare :: Component -> Component -> Ordering

(<) :: Component -> Component -> Bool

(<=) :: Component -> Component -> Bool

(>) :: Component -> Component -> Bool

(>=) :: Component -> Component -> Bool

max :: Component -> Component -> Component

min :: Component -> Component -> Component

Show Component Source # 

Methods

showsPrec :: Int -> Component -> ShowS

show :: Component -> String

showList :: [Component] -> ShowS

data Quantifier Source #

the possible quantifiers

Constructors

Universal 
Existential 
Unique 

Instances

Eq Quantifier Source # 

Methods

(==) :: Quantifier -> Quantifier -> Bool

(/=) :: Quantifier -> Quantifier -> Bool

Data Quantifier Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Quantifier -> c Quantifier

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Quantifier

toConstr :: Quantifier -> Constr

dataTypeOf :: Quantifier -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Quantifier)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quantifier)

gmapT :: (forall b. Data b => b -> b) -> Quantifier -> Quantifier

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quantifier -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quantifier -> r

gmapQ :: (forall d. Data d => d -> u) -> Quantifier -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Quantifier -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quantifier -> m Quantifier

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantifier -> m Quantifier

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantifier -> m Quantifier

Ord Quantifier Source # 
Show Quantifier Source # 

Methods

showsPrec :: Int -> Quantifier -> ShowS

show :: Quantifier -> String

showList :: [Quantifier] -> ShowS

data TypeQual Source #

the possibly type annotations of terms

Constructors

OfType 
AsType 
InType 
Inferred 

Instances

Eq TypeQual Source # 

Methods

(==) :: TypeQual -> TypeQual -> Bool

(/=) :: TypeQual -> TypeQual -> Bool

Data TypeQual Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeQual -> c TypeQual

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeQual

toConstr :: TypeQual -> Constr

dataTypeOf :: TypeQual -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c TypeQual)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeQual)

gmapT :: (forall b. Data b => b -> b) -> TypeQual -> TypeQual

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeQual -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeQual -> r

gmapQ :: (forall d. Data d => d -> u) -> TypeQual -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeQual -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeQual -> m TypeQual

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeQual -> m TypeQual

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeQual -> m TypeQual

Ord TypeQual Source # 

Methods

compare :: TypeQual -> TypeQual -> Ordering

(<) :: TypeQual -> TypeQual -> Bool

(<=) :: TypeQual -> TypeQual -> Bool

(>) :: TypeQual -> TypeQual -> Bool

(>=) :: TypeQual -> TypeQual -> Bool

max :: TypeQual -> TypeQual -> TypeQual

min :: TypeQual -> TypeQual -> TypeQual

Show TypeQual Source # 

Methods

showsPrec :: Int -> TypeQual -> ShowS

show :: TypeQual -> String

showList :: [TypeQual] -> ShowS

data LetBrand Source #

an indicator of (otherwise equivalent) let or where equations

Constructors

Let 
Where 
Program 

Instances

Eq LetBrand Source # 

Methods

(==) :: LetBrand -> LetBrand -> Bool

(/=) :: LetBrand -> LetBrand -> Bool

Data LetBrand Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LetBrand -> c LetBrand

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LetBrand

toConstr :: LetBrand -> Constr

dataTypeOf :: LetBrand -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c LetBrand)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LetBrand)

gmapT :: (forall b. Data b => b -> b) -> LetBrand -> LetBrand

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LetBrand -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LetBrand -> r

gmapQ :: (forall d. Data d => d -> u) -> LetBrand -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LetBrand -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LetBrand -> m LetBrand

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LetBrand -> m LetBrand

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LetBrand -> m LetBrand

Ord LetBrand Source # 

Methods

compare :: LetBrand -> LetBrand -> Ordering

(<) :: LetBrand -> LetBrand -> Bool

(<=) :: LetBrand -> LetBrand -> Bool

(>) :: LetBrand -> LetBrand -> Bool

(>=) :: LetBrand -> LetBrand -> Bool

max :: LetBrand -> LetBrand -> LetBrand

min :: LetBrand -> LetBrand -> LetBrand

Show LetBrand Source # 

Methods

showsPrec :: Int -> LetBrand -> ShowS

show :: LetBrand -> String

showList :: [LetBrand] -> ShowS

data BracketKind Source #

the possible kinds of brackets (that should match when parsed)

Constructors

Parens 
Squares 
Braces 
NoBrackets 

Instances

Eq BracketKind Source # 

Methods

(==) :: BracketKind -> BracketKind -> Bool

(/=) :: BracketKind -> BracketKind -> Bool

Data BracketKind Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BracketKind -> c BracketKind

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BracketKind

toConstr :: BracketKind -> Constr

dataTypeOf :: BracketKind -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c BracketKind)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BracketKind)

gmapT :: (forall b. Data b => b -> b) -> BracketKind -> BracketKind

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BracketKind -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BracketKind -> r

gmapQ :: (forall d. Data d => d -> u) -> BracketKind -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> BracketKind -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BracketKind -> m BracketKind

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BracketKind -> m BracketKind

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BracketKind -> m BracketKind

Ord BracketKind Source # 
Show BracketKind Source # 

Methods

showsPrec :: Int -> BracketKind -> ShowS

show :: BracketKind -> String

showList :: [BracketKind] -> ShowS

getBrackets :: BracketKind -> (String, String) Source #

the brackets as strings for printing

data InstKind Source #

Constructors

UserGiven 
Infer 

Instances

Eq InstKind Source # 

Methods

(==) :: InstKind -> InstKind -> Bool

(/=) :: InstKind -> InstKind -> Bool

Data InstKind Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> InstKind -> c InstKind

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c InstKind

toConstr :: InstKind -> Constr

dataTypeOf :: InstKind -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c InstKind)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InstKind)

gmapT :: (forall b. Data b => b -> b) -> InstKind -> InstKind

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> InstKind -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InstKind -> r

gmapQ :: (forall d. Data d => d -> u) -> InstKind -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> InstKind -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> InstKind -> m InstKind

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> InstKind -> m InstKind

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> InstKind -> m InstKind

Ord InstKind Source # 

Methods

compare :: InstKind -> InstKind -> Ordering

(<) :: InstKind -> InstKind -> Bool

(<=) :: InstKind -> InstKind -> Bool

(>) :: InstKind -> InstKind -> Bool

(>=) :: InstKind -> InstKind -> Bool

max :: InstKind -> InstKind -> InstKind

min :: InstKind -> InstKind -> InstKind

Show InstKind Source # 

Methods

showsPrec :: Int -> InstKind -> ShowS

show :: InstKind -> String

showList :: [InstKind] -> ShowS

data Term Source #

The possible terms and patterns. Formulas are also kept as terms. Local variables and constants are kept separatetly. The variant ResolvedMixTerm is an intermediate representation for type checking only.

Instances

Eq Term Source # 

Methods

(==) :: Term -> Term -> Bool

(/=) :: Term -> Term -> Bool

Data Term Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term -> c Term

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Term

toConstr :: Term -> Constr

dataTypeOf :: Term -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Term)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)

gmapT :: (forall b. Data b => b -> b) -> Term -> Term

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r

gmapQ :: (forall d. Data d => d -> u) -> Term -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Term -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term -> m Term

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term

Ord Term Source # 

Methods

compare :: Term -> Term -> Ordering

(<) :: Term -> Term -> Bool

(<=) :: Term -> Term -> Bool

(>) :: Term -> Term -> Bool

(>=) :: Term -> Term -> Bool

max :: Term -> Term -> Term

min :: Term -> Term -> Term

Show Term Source # 

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

GetRange Term Source # 

data ProgEq Source #

an equation or a case as pair of a pattern and a term

Constructors

ProgEq Term Term Range 

Instances

Eq ProgEq Source # 

Methods

(==) :: ProgEq -> ProgEq -> Bool

(/=) :: ProgEq -> ProgEq -> Bool

Data ProgEq Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProgEq -> c ProgEq

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProgEq

toConstr :: ProgEq -> Constr

dataTypeOf :: ProgEq -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ProgEq)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProgEq)

gmapT :: (forall b. Data b => b -> b) -> ProgEq -> ProgEq

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProgEq -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProgEq -> r

gmapQ :: (forall d. Data d => d -> u) -> ProgEq -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProgEq -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProgEq -> m ProgEq

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProgEq -> m ProgEq

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProgEq -> m ProgEq

Ord ProgEq Source # 

Methods

compare :: ProgEq -> ProgEq -> Ordering

(<) :: ProgEq -> ProgEq -> Bool

(<=) :: ProgEq -> ProgEq -> Bool

(>) :: ProgEq -> ProgEq -> Bool

(>=) :: ProgEq -> ProgEq -> Bool

max :: ProgEq -> ProgEq -> ProgEq

min :: ProgEq -> ProgEq -> ProgEq

Show ProgEq Source # 

Methods

showsPrec :: Int -> ProgEq -> ShowS

show :: ProgEq -> String

showList :: [ProgEq] -> ShowS

data PolyId Source #

an identifier with an optional list of type declarations

Constructors

PolyId Id [TypeArg] Range 

Instances

Eq PolyId Source # 

Methods

(==) :: PolyId -> PolyId -> Bool

(/=) :: PolyId -> PolyId -> Bool

Data PolyId Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PolyId -> c PolyId

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PolyId

toConstr :: PolyId -> Constr

dataTypeOf :: PolyId -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c PolyId)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PolyId)

gmapT :: (forall b. Data b => b -> b) -> PolyId -> PolyId

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PolyId -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PolyId -> r

gmapQ :: (forall d. Data d => d -> u) -> PolyId -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> PolyId -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PolyId -> m PolyId

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PolyId -> m PolyId

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PolyId -> m PolyId

Ord PolyId Source # 

Methods

compare :: PolyId -> PolyId -> Ordering

(<) :: PolyId -> PolyId -> Bool

(<=) :: PolyId -> PolyId -> Bool

(>) :: PolyId -> PolyId -> Bool

(>=) :: PolyId -> PolyId -> Bool

max :: PolyId -> PolyId -> PolyId

min :: PolyId -> PolyId -> PolyId

Show PolyId Source # 

Methods

showsPrec :: Int -> PolyId -> ShowS

show :: PolyId -> String

showList :: [PolyId] -> ShowS

data SeparatorKind Source #

an indicator if variables were separated by commas or by separate declarations

Constructors

Comma 
Other 

Instances

Eq SeparatorKind Source # 
Data SeparatorKind Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SeparatorKind -> c SeparatorKind

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SeparatorKind

toConstr :: SeparatorKind -> Constr

dataTypeOf :: SeparatorKind -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SeparatorKind)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SeparatorKind)

gmapT :: (forall b. Data b => b -> b) -> SeparatorKind -> SeparatorKind

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SeparatorKind -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SeparatorKind -> r

gmapQ :: (forall d. Data d => d -> u) -> SeparatorKind -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SeparatorKind -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SeparatorKind -> m SeparatorKind

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SeparatorKind -> m SeparatorKind

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SeparatorKind -> m SeparatorKind

Ord SeparatorKind Source # 
Show SeparatorKind Source # 

Methods

showsPrec :: Int -> SeparatorKind -> ShowS

show :: SeparatorKind -> String

showList :: [SeparatorKind] -> ShowS

data VarDecl Source #

a variable with its type

Instances

Eq VarDecl Source # 

Methods

(==) :: VarDecl -> VarDecl -> Bool

(/=) :: VarDecl -> VarDecl -> Bool

Data VarDecl Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VarDecl -> c VarDecl

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VarDecl

toConstr :: VarDecl -> Constr

dataTypeOf :: VarDecl -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c VarDecl)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarDecl)

gmapT :: (forall b. Data b => b -> b) -> VarDecl -> VarDecl

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VarDecl -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VarDecl -> r

gmapQ :: (forall d. Data d => d -> u) -> VarDecl -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> VarDecl -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> VarDecl -> m VarDecl

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VarDecl -> m VarDecl

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VarDecl -> m VarDecl

Ord VarDecl Source # 

Methods

compare :: VarDecl -> VarDecl -> Ordering

(<) :: VarDecl -> VarDecl -> Bool

(<=) :: VarDecl -> VarDecl -> Bool

(>) :: VarDecl -> VarDecl -> Bool

(>=) :: VarDecl -> VarDecl -> Bool

max :: VarDecl -> VarDecl -> VarDecl

min :: VarDecl -> VarDecl -> VarDecl

Show VarDecl Source # 

Methods

showsPrec :: Int -> VarDecl -> ShowS

show :: VarDecl -> String

showList :: [VarDecl] -> ShowS

GetRange VarDecl Source # 

data VarKind Source #

the kind of a type variable (or a type argument in schemes)

Instances

Eq VarKind Source # 

Methods

(==) :: VarKind -> VarKind -> Bool

(/=) :: VarKind -> VarKind -> Bool

Data VarKind Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VarKind -> c VarKind

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VarKind

toConstr :: VarKind -> Constr

dataTypeOf :: VarKind -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c VarKind)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarKind)

gmapT :: (forall b. Data b => b -> b) -> VarKind -> VarKind

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VarKind -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VarKind -> r

gmapQ :: (forall d. Data d => d -> u) -> VarKind -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> VarKind -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> VarKind -> m VarKind

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VarKind -> m VarKind

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VarKind -> m VarKind

Ord VarKind Source # 

Methods

compare :: VarKind -> VarKind -> Ordering

(<) :: VarKind -> VarKind -> Bool

(<=) :: VarKind -> VarKind -> Bool

(>) :: VarKind -> VarKind -> Bool

(>=) :: VarKind -> VarKind -> Bool

max :: VarKind -> VarKind -> VarKind

min :: VarKind -> VarKind -> VarKind

Show VarKind Source # 

Methods

showsPrec :: Int -> VarKind -> ShowS

show :: VarKind -> String

showList :: [VarKind] -> ShowS

data TypeArg Source #

a (simple) type variable with its kind (or supertype)

Instances

Eq TypeArg Source # 

Methods

(==) :: TypeArg -> TypeArg -> Bool

(/=) :: TypeArg -> TypeArg -> Bool

Data TypeArg Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeArg -> c TypeArg

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeArg

toConstr :: TypeArg -> Constr

dataTypeOf :: TypeArg -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c TypeArg)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeArg)

gmapT :: (forall b. Data b => b -> b) -> TypeArg -> TypeArg

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeArg -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeArg -> r

gmapQ :: (forall d. Data d => d -> u) -> TypeArg -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeArg -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeArg -> m TypeArg

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeArg -> m TypeArg

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeArg -> m TypeArg

Ord TypeArg Source # 

Methods

compare :: TypeArg -> TypeArg -> Ordering

(<) :: TypeArg -> TypeArg -> Bool

(<=) :: TypeArg -> TypeArg -> Bool

(>) :: TypeArg -> TypeArg -> Bool

(>=) :: TypeArg -> TypeArg -> Bool

max :: TypeArg -> TypeArg -> TypeArg

min :: TypeArg -> TypeArg -> TypeArg

Show TypeArg Source # 

Methods

showsPrec :: Int -> TypeArg -> ShowS

show :: TypeArg -> String

showList :: [TypeArg] -> ShowS

GetRange TypeArg Source # 

data GenVarDecl Source #

a value or type variable

Instances

Eq GenVarDecl Source # 

Methods

(==) :: GenVarDecl -> GenVarDecl -> Bool

(/=) :: GenVarDecl -> GenVarDecl -> Bool

Data GenVarDecl Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GenVarDecl -> c GenVarDecl

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GenVarDecl

toConstr :: GenVarDecl -> Constr

dataTypeOf :: GenVarDecl -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c GenVarDecl)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GenVarDecl)

gmapT :: (forall b. Data b => b -> b) -> GenVarDecl -> GenVarDecl

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GenVarDecl -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GenVarDecl -> r

gmapQ :: (forall d. Data d => d -> u) -> GenVarDecl -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> GenVarDecl -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> GenVarDecl -> m GenVarDecl

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GenVarDecl -> m GenVarDecl

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GenVarDecl -> m GenVarDecl

Ord GenVarDecl Source # 
Show GenVarDecl Source # 

Methods

showsPrec :: Int -> GenVarDecl -> ShowS

show :: GenVarDecl -> String

showList :: [GenVarDecl] -> ShowS

symbol data types symbols

data SymbItems Source #

Instances

Eq SymbItems Source # 

Methods

(==) :: SymbItems -> SymbItems -> Bool

(/=) :: SymbItems -> SymbItems -> Bool

Data SymbItems Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbItems -> c SymbItems

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbItems

toConstr :: SymbItems -> Constr

dataTypeOf :: SymbItems -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SymbItems)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbItems)

gmapT :: (forall b. Data b => b -> b) -> SymbItems -> SymbItems

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbItems -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbItems -> r

gmapQ :: (forall d. Data d => d -> u) -> SymbItems -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbItems -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymbItems -> m SymbItems

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbItems -> m SymbItems

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbItems -> m SymbItems

Ord SymbItems Source # 

Methods

compare :: SymbItems -> SymbItems -> Ordering

(<) :: SymbItems -> SymbItems -> Bool

(<=) :: SymbItems -> SymbItems -> Bool

(>) :: SymbItems -> SymbItems -> Bool

(>=) :: SymbItems -> SymbItems -> Bool

max :: SymbItems -> SymbItems -> SymbItems

min :: SymbItems -> SymbItems -> SymbItems

Show SymbItems Source # 

Methods

showsPrec :: Int -> SymbItems -> ShowS

show :: SymbItems -> String

showList :: [SymbItems] -> ShowS

Syntax HasCASL BasicSpec Symbol SymbItems SymbMapItems Source # 
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source # 

Methods

basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source #

sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source #

stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source #

convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source #

ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source #

signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source #

qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source #

symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source #

id_to_raw :: HasCASL -> Id -> RawSymbol Source #

matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: HasCASL -> Env Source #

add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source #

signature_union :: HasCASL -> Env -> Env -> Result Env Source #

signatureDiff :: HasCASL -> Env -> Env -> Result Env Source #

intersection :: HasCASL -> Env -> Env -> Result Env Source #

final_union :: HasCASL -> Env -> Env -> Result Env Source #

morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: HasCASL -> Env -> Env -> Bool Source #

subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source #

generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source #

cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source #

induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source #

induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source #

is_transportable :: HasCASL -> Morphism -> Bool Source #

is_injective :: HasCASL -> Morphism -> Bool Source #

theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #

Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source #

stability :: HasCASL -> Stability Source #

data_logic :: HasCASL -> Maybe AnyLogic Source #

top_sublogic :: HasCASL -> Sublogic Source #

all_sublogics :: HasCASL -> [Sublogic] Source #

bottomSublogic :: HasCASL -> Maybe Sublogic Source #

sublogicDimensions :: HasCASL -> [[Sublogic]] Source #

parseSublogic :: HasCASL -> String -> Maybe Sublogic Source #

proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source #

provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source #

default_prover :: HasCASL -> String Source #

cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source #

conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source #

empty_proof_tree :: HasCASL -> () Source #

syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source #

omdoc_metatheory :: HasCASL -> Maybe OMCD Source #

export_symToOmdoc :: HasCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source #

addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source #

Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 

data SymbMapItems Source #

mapped symbols

Instances

Eq SymbMapItems Source # 

Methods

(==) :: SymbMapItems -> SymbMapItems -> Bool

(/=) :: SymbMapItems -> SymbMapItems -> Bool

Data SymbMapItems Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbMapItems -> c SymbMapItems

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbMapItems

toConstr :: SymbMapItems -> Constr

dataTypeOf :: SymbMapItems -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SymbMapItems)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbMapItems)

gmapT :: (forall b. Data b => b -> b) -> SymbMapItems -> SymbMapItems

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbMapItems -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbMapItems -> r

gmapQ :: (forall d. Data d => d -> u) -> SymbMapItems -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbMapItems -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymbMapItems -> m SymbMapItems

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbMapItems -> m SymbMapItems

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbMapItems -> m SymbMapItems

Ord SymbMapItems Source # 
Show SymbMapItems Source # 

Methods

showsPrec :: Int -> SymbMapItems -> ShowS

show :: SymbMapItems -> String

showList :: [SymbMapItems] -> ShowS

Syntax HasCASL BasicSpec Symbol SymbItems SymbMapItems Source # 
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source # 

Methods

basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source #

sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source #

stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source #

convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source #

ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source #

signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source #

qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source #

symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source #

id_to_raw :: HasCASL -> Id -> RawSymbol Source #

matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: HasCASL -> Env Source #

add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source #

signature_union :: HasCASL -> Env -> Env -> Result Env Source #

signatureDiff :: HasCASL -> Env -> Env -> Result Env Source #

intersection :: HasCASL -> Env -> Env -> Result Env Source #

final_union :: HasCASL -> Env -> Env -> Result Env Source #

morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: HasCASL -> Env -> Env -> Bool Source #

subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source #

generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source #

cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source #

induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source #

induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source #

is_transportable :: HasCASL -> Morphism -> Bool Source #

is_injective :: HasCASL -> Morphism -> Bool Source #

theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #

Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source #

stability :: HasCASL -> Stability Source #

data_logic :: HasCASL -> Maybe AnyLogic Source #

top_sublogic :: HasCASL -> Sublogic Source #

all_sublogics :: HasCASL -> [Sublogic] Source #

bottomSublogic :: HasCASL -> Maybe Sublogic Source #

sublogicDimensions :: HasCASL -> [[Sublogic]] Source #

parseSublogic :: HasCASL -> String -> Maybe Sublogic Source #

proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source #

provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source #

default_prover :: HasCASL -> String Source #

cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source #

conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source #

empty_proof_tree :: HasCASL -> () Source #

syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source #

omdoc_metatheory :: HasCASL -> Maybe OMCD Source #

export_symToOmdoc :: HasCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source #

addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source #

Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 

data SymbKind Source #

kind of symbols

Instances

Eq SymbKind Source # 

Methods

(==) :: SymbKind -> SymbKind -> Bool

(/=) :: SymbKind -> SymbKind -> Bool

Data SymbKind Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbKind -> c SymbKind

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbKind

toConstr :: SymbKind -> Constr

dataTypeOf :: SymbKind -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SymbKind)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbKind)

gmapT :: (forall b. Data b => b -> b) -> SymbKind -> SymbKind

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbKind -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbKind -> r

gmapQ :: (forall d. Data d => d -> u) -> SymbKind -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbKind -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymbKind -> m SymbKind

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbKind -> m SymbKind

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbKind -> m SymbKind

Ord SymbKind Source # 

Methods

compare :: SymbKind -> SymbKind -> Ordering

(<) :: SymbKind -> SymbKind -> Bool

(<=) :: SymbKind -> SymbKind -> Bool

(>) :: SymbKind -> SymbKind -> Bool

(>=) :: SymbKind -> SymbKind -> Bool

max :: SymbKind -> SymbKind -> SymbKind

min :: SymbKind -> SymbKind -> SymbKind

Show SymbKind Source # 

Methods

showsPrec :: Int -> SymbKind -> ShowS

show :: SymbKind -> String

showList :: [SymbKind] -> ShowS

Pretty SymbKind Source # 

data Symb Source #

type annotated symbols

Constructors

Symb Id (Maybe SymbType) Range 

Instances

Eq Symb Source # 

Methods

(==) :: Symb -> Symb -> Bool

(/=) :: Symb -> Symb -> Bool

Data Symb Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Symb -> c Symb

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Symb

toConstr :: Symb -> Constr

dataTypeOf :: Symb -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Symb)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symb)

gmapT :: (forall b. Data b => b -> b) -> Symb -> Symb

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symb -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symb -> r

gmapQ :: (forall d. Data d => d -> u) -> Symb -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Symb -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Symb -> m Symb

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Symb -> m Symb

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Symb -> m Symb

Ord Symb Source # 

Methods

compare :: Symb -> Symb -> Ordering

(<) :: Symb -> Symb -> Bool

(<=) :: Symb -> Symb -> Bool

(>) :: Symb -> Symb -> Bool

(>=) :: Symb -> Symb -> Bool

max :: Symb -> Symb -> Symb

min :: Symb -> Symb -> Symb

Show Symb Source # 

Methods

showsPrec :: Int -> Symb -> ShowS

show :: Symb -> String

showList :: [Symb] -> ShowS

data SymbType Source #

type for symbols

Constructors

SymbType TypeScheme 

Instances

Eq SymbType Source # 

Methods

(==) :: SymbType -> SymbType -> Bool

(/=) :: SymbType -> SymbType -> Bool

Data SymbType Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbType -> c SymbType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbType

toConstr :: SymbType -> Constr

dataTypeOf :: SymbType -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SymbType)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbType)

gmapT :: (forall b. Data b => b -> b) -> SymbType -> SymbType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbType -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbType -> r

gmapQ :: (forall d. Data d => d -> u) -> SymbType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymbType -> m SymbType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbType -> m SymbType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbType -> m SymbType

Ord SymbType Source # 

Methods

compare :: SymbType -> SymbType -> Ordering

(<) :: SymbType -> SymbType -> Bool

(<=) :: SymbType -> SymbType -> Bool

(>) :: SymbType -> SymbType -> Bool

(>=) :: SymbType -> SymbType -> Bool

max :: SymbType -> SymbType -> SymbType

min :: SymbType -> SymbType -> SymbType

Show SymbType Source # 

Methods

showsPrec :: Int -> SymbType -> ShowS

show :: SymbType -> String

showList :: [SymbType] -> ShowS

data SymbOrMap Source #

mapped symbol

Constructors

SymbOrMap Symb (Maybe Symb) Range 

Instances

Eq SymbOrMap Source # 

Methods

(==) :: SymbOrMap -> SymbOrMap -> Bool

(/=) :: SymbOrMap -> SymbOrMap -> Bool

Data SymbOrMap Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbOrMap -> c SymbOrMap

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbOrMap

toConstr :: SymbOrMap -> Constr

dataTypeOf :: SymbOrMap -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SymbOrMap)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbOrMap)

gmapT :: (forall b. Data b => b -> b) -> SymbOrMap -> SymbOrMap

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbOrMap -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbOrMap -> r

gmapQ :: (forall d. Data d => d -> u) -> SymbOrMap -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbOrMap -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymbOrMap -> m SymbOrMap

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbOrMap -> m SymbOrMap

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbOrMap -> m SymbOrMap

Ord SymbOrMap Source # 

Methods

compare :: SymbOrMap -> SymbOrMap -> Ordering

(<) :: SymbOrMap -> SymbOrMap -> Bool

(<=) :: SymbOrMap -> SymbOrMap -> Bool

(>) :: SymbOrMap -> SymbOrMap -> Bool

(>=) :: SymbOrMap -> SymbOrMap -> Bool

max :: SymbOrMap -> SymbOrMap -> SymbOrMap

min :: SymbOrMap -> SymbOrMap -> SymbOrMap

Show SymbOrMap Source # 

Methods

showsPrec :: Int -> SymbOrMap -> ShowS

show :: SymbOrMap -> String

showList :: [SymbOrMap] -> ShowS

equality instances ignoring positions

compute better position

bestRange :: GetRange a => [a] -> Range -> Range Source #

get a reasonable position for a list with an additional position list