Hets - the Heterogeneous Tool Set

Copyright(c) Christian Maeder DFKI GmbH 2011
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

Fpl.As

Description

abstract syntax for FPL, logic for functional programs as CASL extension

Synopsis

Documentation

data FplExt Source #

Instances

Data FplExt Source # 

Methods

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

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

toConstr :: FplExt -> Constr

dataTypeOf :: FplExt -> DataType

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

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

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

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

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

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

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

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

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

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

Show FplExt Source # 

Methods

showsPrec :: Int -> FplExt -> ShowS

show :: FplExt -> String

showList :: [FplExt] -> ShowS

GetRange FplExt Source # 
AParsable FplExt Source # 
Pretty FplExt Source # 
Syntax Fpl FplBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
StaticAnalysis Fpl FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol Source # 

Methods

basic_analysis :: Fpl -> Maybe ((FplBasicSpec, FplSign, GlobalAnnos) -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])) Source #

sen_analysis :: Fpl -> Maybe ((FplBasicSpec, FplSign, FplForm) -> Result FplForm) Source #

extBasicAnalysis :: Fpl -> IRI -> LibName -> FplBasicSpec -> FplSign -> GlobalAnnos -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm]) Source #

stat_symb_map_items :: Fpl -> FplSign -> Maybe FplSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Fpl -> FplSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: Fpl -> Maybe ((FplSign, [Named FplForm]) -> FplBasicSpec) Source #

ensures_amalgamability :: Fpl -> ([CASLAmalgOpt], Gr FplSign (Int, FplMor), [(Int, FplMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Fpl -> FplMor -> [Named FplForm] -> Result (FplSign, [Named FplForm]) Source #

signature_colimit :: Fpl -> Gr FplSign (Int, FplMor) -> Result (FplSign, Map Int FplMor) Source #

qualify :: Fpl -> SIMPLE_ID -> LibName -> FplMor -> FplSign -> Result (FplMor, [Named FplForm]) Source #

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

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

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

empty_signature :: Fpl -> FplSign Source #

add_symb_to_sign :: Fpl -> FplSign -> Symbol -> Result FplSign Source #

signature_union :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

signatureDiff :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

intersection :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

final_union :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

morphism_union :: Fpl -> FplMor -> FplMor -> Result FplMor Source #

is_subsig :: Fpl -> FplSign -> FplSign -> Bool Source #

subsig_inclusion :: Fpl -> FplSign -> FplSign -> Result FplMor Source #

generated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor Source #

cogenerated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor Source #

induced_from_morphism :: Fpl -> EndoMap RawSymbol -> FplSign -> Result FplMor Source #

induced_from_to_morphism :: Fpl -> EndoMap RawSymbol -> ExtSign FplSign Symbol -> ExtSign FplSign Symbol -> Result FplMor Source #

is_transportable :: Fpl -> FplMor -> Bool Source #

is_injective :: Fpl -> FplMor -> Bool Source #

theory_to_taxonomy :: Fpl -> TaxoGraphKind -> MMiSSOntology -> FplSign -> [Named FplForm] -> Result MMiSSOntology Source #

corresp2th :: Fpl -> String -> Bool -> FplSign -> FplSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (FplSign, [Named FplForm], FplSign, FplSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Fpl -> FplSign -> FplSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (FplSign, FplSign, FplSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Fpl -> [IRI] -> (FplSign, [Named FplForm]) -> Result (FplSign, [Named FplForm]) Source #

Logic Fpl () FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: Fpl -> Maybe (FplBasicSpec -> AParser st FplForm) Source #

stability :: Fpl -> Stability Source #

data_logic :: Fpl -> Maybe AnyLogic Source #

top_sublogic :: Fpl -> () Source #

all_sublogics :: Fpl -> [()] Source #

bottomSublogic :: Fpl -> Maybe () Source #

sublogicDimensions :: Fpl -> [[()]] Source #

parseSublogic :: Fpl -> String -> Maybe () Source #

proj_sublogic_epsilon :: Fpl -> () -> FplSign -> FplMor Source #

provers :: Fpl -> [Prover FplSign FplForm FplMor () ()] Source #

default_prover :: Fpl -> String Source #

cons_checkers :: Fpl -> [ConsChecker FplSign FplForm () FplMor ()] Source #

conservativityCheck :: Fpl -> [ConservativityChecker FplSign FplForm FplMor] Source #

empty_proof_tree :: Fpl -> () Source #

syntaxTable :: Fpl -> FplSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Fpl -> Maybe OMCD Source #

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

export_senToOmdoc :: Fpl -> NameMap Symbol -> FplForm -> Result TCorOMElement Source #

export_theoryToOmdoc :: Fpl -> SigMap Symbol -> FplSign -> [Named FplForm] -> Result [TCElement] Source #

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

omdocToSen :: Fpl -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FplForm)) Source #

addOMadtToTheory :: Fpl -> SigMapI Symbol -> (FplSign, [Named FplForm]) -> [[OmdADT]] -> Result (FplSign, [Named FplForm]) Source #

addOmdocToTheory :: Fpl -> SigMapI Symbol -> (FplSign, [Named FplForm]) -> [TCElement] -> Result (FplSign, [Named FplForm]) Source #

data FplSortItem Source #

Instances

Data FplSortItem Source # 

Methods

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

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

toConstr :: FplSortItem -> Constr

dataTypeOf :: FplSortItem -> DataType

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

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

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

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

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

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

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

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

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

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

Show FplSortItem Source # 

Methods

showsPrec :: Int -> FplSortItem -> ShowS

show :: FplSortItem -> String

showList :: [FplSortItem] -> ShowS

GetRange FplSortItem Source # 
Pretty FplSortItem Source # 
ListCheck FplSortItem Source # 

Methods

innerList :: FplSortItem -> [()] Source #

data FplOpItem Source #

Instances

Data FplOpItem Source # 

Methods

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

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

toConstr :: FplOpItem -> Constr

dataTypeOf :: FplOpItem -> DataType

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

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

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

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

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

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

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

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

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

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

Show FplOpItem Source # 

Methods

showsPrec :: Int -> FplOpItem -> ShowS

show :: FplOpItem -> String

showList :: [FplOpItem] -> ShowS

GetRange FplOpItem Source # 
Pretty FplOpItem Source # 
ListCheck FplOpItem Source # 

Methods

innerList :: FplOpItem -> [()] Source #

data FunDef Source #

Instances

Eq FunDef Source # 

Methods

(==) :: FunDef -> FunDef -> Bool

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

Data FunDef Source # 

Methods

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

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

toConstr :: FunDef -> Constr

dataTypeOf :: FunDef -> DataType

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

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

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

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

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

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

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

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

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

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

Ord FunDef Source # 

Methods

compare :: FunDef -> FunDef -> Ordering

(<) :: FunDef -> FunDef -> Bool

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

(>) :: FunDef -> FunDef -> Bool

(>=) :: FunDef -> FunDef -> Bool

max :: FunDef -> FunDef -> FunDef

min :: FunDef -> FunDef -> FunDef

Show FunDef Source # 

Methods

showsPrec :: Int -> FunDef -> ShowS

show :: FunDef -> String

showList :: [FunDef] -> ShowS

GetRange FunDef Source # 
Pretty FunDef Source # 

data TermExt Source #

extra terms of FPL. if-then-else must use a term as guard with result sort Bool. To allow true, false and an equality test an extra term parser is needed that must not be used when parsing formulas.

Instances

Eq TermExt Source # 

Methods

(==) :: TermExt -> TermExt -> Bool

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

Data TermExt Source # 

Methods

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

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

toConstr :: TermExt -> Constr

dataTypeOf :: TermExt -> DataType

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

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

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

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

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

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

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

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

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

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

Ord TermExt Source # 

Methods

compare :: TermExt -> TermExt -> Ordering

(<) :: TermExt -> TermExt -> Bool

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

(>) :: TermExt -> TermExt -> Bool

(>=) :: TermExt -> TermExt -> Bool

max :: TermExt -> TermExt -> TermExt

min :: TermExt -> TermExt -> TermExt

Show TermExt Source # 

Methods

showsPrec :: Int -> TermExt -> ShowS

show :: TermExt -> String

showList :: [TermExt] -> ShowS

GetRange TermExt Source # 
TermParser TermExt Source # 

Methods

termParser :: Bool -> AParser st TermExt Source #

Pretty TermExt Source # 
FormExtension TermExt Source # 
Sentences Fpl FplForm FplSign FplMor Symbol Source # 
Syntax Fpl FplBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
StaticAnalysis Fpl FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol Source # 

Methods

basic_analysis :: Fpl -> Maybe ((FplBasicSpec, FplSign, GlobalAnnos) -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])) Source #

sen_analysis :: Fpl -> Maybe ((FplBasicSpec, FplSign, FplForm) -> Result FplForm) Source #

extBasicAnalysis :: Fpl -> IRI -> LibName -> FplBasicSpec -> FplSign -> GlobalAnnos -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm]) Source #

stat_symb_map_items :: Fpl -> FplSign -> Maybe FplSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Fpl -> FplSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: Fpl -> Maybe ((FplSign, [Named FplForm]) -> FplBasicSpec) Source #

ensures_amalgamability :: Fpl -> ([CASLAmalgOpt], Gr FplSign (Int, FplMor), [(Int, FplMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Fpl -> FplMor -> [Named FplForm] -> Result (FplSign, [Named FplForm]) Source #

signature_colimit :: Fpl -> Gr FplSign (Int, FplMor) -> Result (FplSign, Map Int FplMor) Source #

qualify :: Fpl -> SIMPLE_ID -> LibName -> FplMor -> FplSign -> Result (FplMor, [Named FplForm]) Source #

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

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

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

empty_signature :: Fpl -> FplSign Source #

add_symb_to_sign :: Fpl -> FplSign -> Symbol -> Result FplSign Source #

signature_union :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

signatureDiff :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

intersection :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

final_union :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

morphism_union :: Fpl -> FplMor -> FplMor -> Result FplMor Source #

is_subsig :: Fpl -> FplSign -> FplSign -> Bool Source #

subsig_inclusion :: Fpl -> FplSign -> FplSign -> Result FplMor Source #

generated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor Source #

cogenerated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor Source #

induced_from_morphism :: Fpl -> EndoMap RawSymbol -> FplSign -> Result FplMor Source #

induced_from_to_morphism :: Fpl -> EndoMap RawSymbol -> ExtSign FplSign Symbol -> ExtSign FplSign Symbol -> Result FplMor Source #

is_transportable :: Fpl -> FplMor -> Bool Source #

is_injective :: Fpl -> FplMor -> Bool Source #

theory_to_taxonomy :: Fpl -> TaxoGraphKind -> MMiSSOntology -> FplSign -> [Named FplForm] -> Result MMiSSOntology Source #

corresp2th :: Fpl -> String -> Bool -> FplSign -> FplSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (FplSign, [Named FplForm], FplSign, FplSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Fpl -> FplSign -> FplSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (FplSign, FplSign, FplSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Fpl -> [IRI] -> (FplSign, [Named FplForm]) -> Result (FplSign, [Named FplForm]) Source #

Logic Fpl () FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: Fpl -> Maybe (FplBasicSpec -> AParser st FplForm) Source #

stability :: Fpl -> Stability Source #

data_logic :: Fpl -> Maybe AnyLogic Source #

top_sublogic :: Fpl -> () Source #

all_sublogics :: Fpl -> [()] Source #

bottomSublogic :: Fpl -> Maybe () Source #

sublogicDimensions :: Fpl -> [[()]] Source #

parseSublogic :: Fpl -> String -> Maybe () Source #

proj_sublogic_epsilon :: Fpl -> () -> FplSign -> FplMor Source #

provers :: Fpl -> [Prover FplSign FplForm FplMor () ()] Source #

default_prover :: Fpl -> String Source #

cons_checkers :: Fpl -> [ConsChecker FplSign FplForm () FplMor ()] Source #

conservativityCheck :: Fpl -> [ConservativityChecker FplSign FplForm FplMor] Source #

empty_proof_tree :: Fpl -> () Source #

syntaxTable :: Fpl -> FplSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Fpl -> Maybe OMCD Source #

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

export_senToOmdoc :: Fpl -> NameMap Symbol -> FplForm -> Result TCorOMElement Source #

export_theoryToOmdoc :: Fpl -> SigMap Symbol -> FplSign -> [Named FplForm] -> Result [TCElement] Source #

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

omdocToSen :: Fpl -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FplForm)) Source #

addOMadtToTheory :: Fpl -> SigMapI Symbol -> (FplSign, [Named FplForm]) -> [[OmdADT]] -> Result (FplSign, [Named FplForm]) Source #

addOmdocToTheory :: Fpl -> SigMapI Symbol -> (FplSign, [Named FplForm]) -> [TCElement] -> Result (FplSign, [Named FplForm]) Source #

funDef :: [String] -> AParser st FunDef Source #

optVarDecls :: [String] -> AParser st ([VAR_DECL], [Token]) Source #

boolTerm :: [String] -> AParser st FplTerm Source #

eqTerm :: [String] -> AParser st FplTerm Source #

eqForm :: [String] -> AParser st TermExt Source #

extra formulas to compare bool terms with true or false. Interpreting boolean valued terms as formulas is still missing.

fplTerm :: [String] -> AParser st TermExt Source #

caseTerm :: [String] -> AParser st TermExt Source #

patTermPair :: [String] -> AParser st (FplTerm, FplTerm) Source #

letVar :: [String] -> AParser st FunDef Source #

letTerm :: [String] -> AParser st TermExt Source #

ifThenElse :: [String] -> AParser st TermExt Source #

fplExt :: [String] -> AParser st FplExt Source #

freeType :: [String] -> SORT -> AParser st FplSortItem Source #

fplOpItem :: [String] -> AParser st FplOpItem Source #