Copyright	(c) Christian Maeder DFKI GmbH 2011
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	None

Fpl.As

Description

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

Synopsis

type FplBasicSpec = BASIC_SPEC FplExt () TermExt
type FplTerm = TERM TermExt
type FplForm = FORMULA TermExt
data FplExt
- = FplSortItems [Annoted FplSortItem] Range
- | FplOpItems [Annoted FplOpItem] Range
data FplSortItem
- = FreeType DATATYPE_DECL
- | CaslSortItem (SORT_ITEM TermExt)
data FplOpItem
- = FunOp FunDef
- | CaslOpItem (OP_ITEM TermExt)
prepPunctBar :: [Doc] -> [Doc]
printDD :: DATATYPE_DECL -> Doc
data FunDef = FunDef OP_NAME OP_HEAD (Annoted FplTerm) Range
kindHead :: OpKind -> OP_HEAD -> OP_HEAD
data TermExt
- = FixDef FunDef
- | Case FplTerm [(FplTerm, FplTerm)] Range
- | Let FunDef FplTerm Range
- | IfThenElse FplTerm FplTerm FplTerm Range
- | EqTerm FplTerm FplTerm Range
- | BoolTerm FplTerm
fplReservedWords :: [String]
funDef :: [String] -> AParser st FunDef
optVarDecls :: [String] -> AParser st ([VAR_DECL], [Token])
constBool :: AParser st FplTerm
boolTerm :: [String] -> AParser st FplTerm
eqTerm :: [String] -> AParser st FplTerm
eqForm :: [String] -> AParser st TermExt
fplTerm :: [String] -> AParser st TermExt
caseTerm :: [String] -> AParser st TermExt
patTermPair :: [String] -> AParser st (FplTerm, FplTerm)
letVar :: [String] -> AParser st FunDef
letTerm :: [String] -> AParser st TermExt
ifThenElse :: [String] -> AParser st TermExt
fplExt :: [String] -> AParser st FplExt
fplSortItem :: [String] -> AParser st FplSortItem
freeType :: [String] -> SORT -> AParser st FplSortItem
fplOpItem :: [String] -> AParser st FplOpItem

Documentation

type FplBasicSpec = BASIC_SPEC FplExt () TermExt Source #

type FplTerm = TERM TermExt Source #

type FplForm = FORMULA TermExt Source #

data FplExt Source #

Constructors

FplSortItems [Annoted FplSortItem] Range
FplOpItems [Annoted FplOpItem] Range

Instances

Instances details

Data FplExt Source #
Instance details Defined in Fpl.As 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 :: forall r r'. (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 #
Instance details Defined in Fpl.As Methods showsPrec :: Int -> FplExt -> ShowS show :: FplExt -> String showList :: [FplExt] -> ShowS
Generic FplExt
Instance details Defined in Fpl.ATC_Fpl Associated Types type Rep FplExt :: Type -> Type Methods from :: FplExt -> Rep FplExt x to :: Rep FplExt x -> FplExt
GetRange FplExt Source #
Instance details Defined in Fpl.As Methods getRange :: FplExt -> Range Source # rangeSpan :: FplExt -> [Pos] Source #
FromJSON FplExt
Instance details Defined in Fpl.ATC_Fpl Methods parseJSON :: Value -> Parser FplExt parseJSONList :: Value -> Parser [FplExt]
ToJSON FplExt
Instance details Defined in Fpl.ATC_Fpl Methods toJSON :: FplExt -> Value toEncoding :: FplExt -> Encoding toJSONList :: [FplExt] -> Value toEncodingList :: [FplExt] -> Encoding
ShATermConvertible FplExt
Instance details Defined in Fpl.ATC_Fpl Methods toShATermAux :: ATermTable -> FplExt -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FplExt] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FplExt) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FplExt])
Pretty FplExt Source #
Instance details Defined in Fpl.As Methods pretty :: FplExt -> Doc Source # pretties :: [FplExt] -> Doc Source #
AParsable FplExt Source #
Instance details Defined in Fpl.As Methods aparser :: AParser st FplExt Source #
Syntax Fpl FplBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in Fpl.Logic_Fpl Methods parsersAndPrinters :: Fpl -> Map String (PrefixMap -> AParser st FplBasicSpec, FplBasicSpec -> Doc) Source # parse_basic_spec :: Fpl -> Maybe (PrefixMap -> AParser st FplBasicSpec) Source # parseSingleSymbItem :: Fpl -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: Fpl -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: Fpl -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: Fpl -> FplBasicSpec -> Item Source # symb_items_name :: Fpl -> SYMB_ITEMS -> [String] Source #
StaticAnalysis Fpl FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol Source #
Instance details Defined in Fpl.Logic_Fpl 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 #
Instance details Defined in Fpl.Logic_Fpl 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 # sublogicOfTheo :: Fpl -> (FplSign, [FplForm]) -> () Source #
type Rep FplExt
Instance details Defined in Fpl.ATC_Fpl type Rep FplExt = D1 ('MetaData "FplExt" "Fpl.As" "main" 'False) (C1 ('MetaCons "FplSortItems" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted FplSortItem]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "FplOpItems" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted FplOpItem]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

data FplSortItem Source #

Constructors

FreeType DATATYPE_DECL
CaslSortItem (SORT_ITEM TermExt)

Instances

Instances details

Data FplSortItem Source #
Instance details Defined in Fpl.As 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 :: forall r r'. (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 #
Instance details Defined in Fpl.As Methods showsPrec :: Int -> FplSortItem -> ShowS show :: FplSortItem -> String showList :: [FplSortItem] -> ShowS
Generic FplSortItem
Instance details Defined in Fpl.ATC_Fpl Associated Types type Rep FplSortItem :: Type -> Type Methods from :: FplSortItem -> Rep FplSortItem x to :: Rep FplSortItem x -> FplSortItem
GetRange FplSortItem Source #
Instance details Defined in Fpl.As Methods getRange :: FplSortItem -> Range Source # rangeSpan :: FplSortItem -> [Pos] Source #
FromJSON FplSortItem
Instance details Defined in Fpl.ATC_Fpl Methods parseJSON :: Value -> Parser FplSortItem parseJSONList :: Value -> Parser [FplSortItem]
ToJSON FplSortItem
Instance details Defined in Fpl.ATC_Fpl Methods toJSON :: FplSortItem -> Value toEncoding :: FplSortItem -> Encoding toJSONList :: [FplSortItem] -> Value toEncodingList :: [FplSortItem] -> Encoding
ShATermConvertible FplSortItem
Instance details Defined in Fpl.ATC_Fpl Methods toShATermAux :: ATermTable -> FplSortItem -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FplSortItem] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FplSortItem) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FplSortItem])
Pretty FplSortItem Source #
Instance details Defined in Fpl.As Methods pretty :: FplSortItem -> Doc Source # pretties :: [FplSortItem] -> Doc Source #
ListCheck FplSortItem Source #
Instance details Defined in Fpl.As Methods innerList :: FplSortItem -> [()] Source #
type Rep FplSortItem
Instance details Defined in Fpl.ATC_Fpl type Rep FplSortItem = D1 ('MetaData "FplSortItem" "Fpl.As" "main" 'False) (C1 ('MetaCons "FreeType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DATATYPE_DECL)) :+: C1 ('MetaCons "CaslSortItem" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SORT_ITEM TermExt))))

data FplOpItem Source #

Constructors

FunOp FunDef
CaslOpItem (OP_ITEM TermExt)

Instances

Instances details

Data FplOpItem Source #
Instance details Defined in Fpl.As 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 :: forall r r'. (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 #
Instance details Defined in Fpl.As Methods showsPrec :: Int -> FplOpItem -> ShowS show :: FplOpItem -> String showList :: [FplOpItem] -> ShowS
Generic FplOpItem
Instance details Defined in Fpl.ATC_Fpl Associated Types type Rep FplOpItem :: Type -> Type Methods from :: FplOpItem -> Rep FplOpItem x to :: Rep FplOpItem x -> FplOpItem
GetRange FplOpItem Source #
Instance details Defined in Fpl.As Methods getRange :: FplOpItem -> Range Source # rangeSpan :: FplOpItem -> [Pos] Source #
FromJSON FplOpItem
Instance details Defined in Fpl.ATC_Fpl Methods parseJSON :: Value -> Parser FplOpItem parseJSONList :: Value -> Parser [FplOpItem]
ToJSON FplOpItem
Instance details Defined in Fpl.ATC_Fpl Methods toJSON :: FplOpItem -> Value toEncoding :: FplOpItem -> Encoding toJSONList :: [FplOpItem] -> Value toEncodingList :: [FplOpItem] -> Encoding
ShATermConvertible FplOpItem
Instance details Defined in Fpl.ATC_Fpl Methods toShATermAux :: ATermTable -> FplOpItem -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FplOpItem] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FplOpItem) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FplOpItem])
Pretty FplOpItem Source #
Instance details Defined in Fpl.As Methods pretty :: FplOpItem -> Doc Source # pretties :: [FplOpItem] -> Doc Source #
ListCheck FplOpItem Source #
Instance details Defined in Fpl.As Methods innerList :: FplOpItem -> [()] Source #
type Rep FplOpItem
Instance details Defined in Fpl.ATC_Fpl type Rep FplOpItem = D1 ('MetaData "FplOpItem" "Fpl.As" "main" 'False) (C1 ('MetaCons "FunOp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FunDef)) :+: C1 ('MetaCons "CaslOpItem" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (OP_ITEM TermExt))))

prepPunctBar :: [Doc] -> [Doc] Source #

printDD :: DATATYPE_DECL -> Doc Source #

data FunDef Source #

Constructors

FunDef OP_NAME OP_HEAD (Annoted FplTerm) Range

Instances

Instances details

Eq FunDef Source #
Instance details Defined in Fpl.As Methods (==) :: FunDef -> FunDef -> Bool (/=) :: FunDef -> FunDef -> Bool
Data FunDef Source #
Instance details Defined in Fpl.As 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 :: forall r r'. (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 #
Instance details Defined in Fpl.As 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 #
Instance details Defined in Fpl.As Methods showsPrec :: Int -> FunDef -> ShowS show :: FunDef -> String showList :: [FunDef] -> ShowS
Generic FunDef
Instance details Defined in Fpl.ATC_Fpl Associated Types type Rep FunDef :: Type -> Type Methods from :: FunDef -> Rep FunDef x to :: Rep FunDef x -> FunDef
GetRange FunDef Source #
Instance details Defined in Fpl.As Methods getRange :: FunDef -> Range Source # rangeSpan :: FunDef -> [Pos] Source #
FromJSON FunDef
Instance details Defined in Fpl.ATC_Fpl Methods parseJSON :: Value -> Parser FunDef parseJSONList :: Value -> Parser [FunDef]
ToJSON FunDef
Instance details Defined in Fpl.ATC_Fpl Methods toJSON :: FunDef -> Value toEncoding :: FunDef -> Encoding toJSONList :: [FunDef] -> Value toEncodingList :: [FunDef] -> Encoding
ShATermConvertible FunDef
Instance details Defined in Fpl.ATC_Fpl Methods toShATermAux :: ATermTable -> FunDef -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FunDef] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FunDef) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FunDef])
Pretty FunDef Source #
Instance details Defined in Fpl.As Methods pretty :: FunDef -> Doc Source # pretties :: [FunDef] -> Doc Source #
type Rep FunDef
Instance details Defined in Fpl.ATC_Fpl type Rep FunDef = D1 ('MetaData "FunDef" "Fpl.As" "main" 'False) (C1 ('MetaCons "FunDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OP_NAME) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OP_HEAD)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Annoted FplTerm)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

kindHead :: OpKind -> OP_HEAD -> OP_HEAD 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.

Constructors

FixDef FunDef	formula
Case FplTerm [(FplTerm, FplTerm)] Range
Let FunDef FplTerm Range
IfThenElse FplTerm FplTerm FplTerm Range
EqTerm FplTerm FplTerm Range
BoolTerm FplTerm

Instances

Instances details

Eq TermExt Source #
Instance details Defined in Fpl.As Methods (==) :: TermExt -> TermExt -> Bool (/=) :: TermExt -> TermExt -> Bool
Data TermExt Source #
Instance details Defined in Fpl.As 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 :: forall r r'. (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 #
Instance details Defined in Fpl.As 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 #
Instance details Defined in Fpl.As Methods showsPrec :: Int -> TermExt -> ShowS show :: TermExt -> String showList :: [TermExt] -> ShowS
Generic TermExt
Instance details Defined in Fpl.ATC_Fpl Associated Types type Rep TermExt :: Type -> Type Methods from :: TermExt -> Rep TermExt x to :: Rep TermExt x -> TermExt
GetRange TermExt Source #
Instance details Defined in Fpl.As Methods getRange :: TermExt -> Range Source # rangeSpan :: TermExt -> [Pos] Source #
FromJSON TermExt
Instance details Defined in Fpl.ATC_Fpl Methods parseJSON :: Value -> Parser TermExt parseJSONList :: Value -> Parser [TermExt]
ToJSON TermExt
Instance details Defined in Fpl.ATC_Fpl Methods toJSON :: TermExt -> Value toEncoding :: TermExt -> Encoding toJSONList :: [TermExt] -> Value toEncodingList :: [TermExt] -> Encoding
ShATermConvertible TermExt
Instance details Defined in Fpl.ATC_Fpl Methods toShATermAux :: ATermTable -> TermExt -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TermExt] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TermExt) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TermExt])
Pretty TermExt Source #
Instance details Defined in Fpl.As Methods pretty :: TermExt -> Doc Source # pretties :: [TermExt] -> Doc Source #
FormExtension TermExt Source #
Instance details Defined in Fpl.As Methods isQuantifierLike :: TermExt -> Bool Source # prefixExt :: TermExt -> Doc -> Doc Source #
TermExtension TermExt Source #
Instance details Defined in Fpl.StatAna Methods freeVarsOfExt :: Sign TermExt e -> TermExt -> VarSet Source # optTermSort :: TermExt -> Maybe SORT Source # sortOfTerm :: TermExt -> SORT Source # termToFormula :: TERM TermExt -> Result (FORMULA TermExt) Source #
TermParser TermExt Source #
Instance details Defined in Fpl.As Methods termParser :: Bool -> AParser st TermExt Source #
Sentences Fpl FplForm FplSign FplMor Symbol Source #
Instance details Defined in Fpl.Logic_Fpl Methods map_sen :: Fpl -> FplMor -> FplForm -> Result FplForm Source # simplify_sen :: Fpl -> FplSign -> FplForm -> FplForm Source # negation :: Fpl -> FplForm -> Maybe FplForm Source # print_sign :: Fpl -> FplSign -> Doc Source # print_named :: Fpl -> Named FplForm -> Doc Source # sym_of :: Fpl -> FplSign -> [Set Symbol] Source # mostSymsOf :: Fpl -> FplSign -> [Symbol] Source # symmap_of :: Fpl -> FplMor -> EndoMap Symbol Source # sym_name :: Fpl -> Symbol -> Id Source # sym_label :: Fpl -> Symbol -> Maybe String Source # fullSymName :: Fpl -> Symbol -> String Source # symKind :: Fpl -> Symbol -> String Source # symsOfSen :: Fpl -> FplSign -> FplForm -> [Symbol] Source # pair_symbols :: Fpl -> Symbol -> Symbol -> Result Symbol Source #
Syntax Fpl FplBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in Fpl.Logic_Fpl Methods parsersAndPrinters :: Fpl -> Map String (PrefixMap -> AParser st FplBasicSpec, FplBasicSpec -> Doc) Source # parse_basic_spec :: Fpl -> Maybe (PrefixMap -> AParser st FplBasicSpec) Source # parseSingleSymbItem :: Fpl -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: Fpl -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: Fpl -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: Fpl -> FplBasicSpec -> Item Source # symb_items_name :: Fpl -> SYMB_ITEMS -> [String] Source #
StaticAnalysis Fpl FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol Source #
Instance details Defined in Fpl.Logic_Fpl 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 #
Instance details Defined in Fpl.Logic_Fpl 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 # sublogicOfTheo :: Fpl -> (FplSign, [FplForm]) -> () Source #
type Rep TermExt
Instance details Defined in Fpl.ATC_Fpl type Rep TermExt = D1 ('MetaData "TermExt" "Fpl.As" "main" 'False) ((C1 ('MetaCons "FixDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FunDef)) :+: (C1 ('MetaCons "Case" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FplTerm) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(FplTerm, FplTerm)]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Let" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FunDef) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FplTerm) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))) :+: (C1 ('MetaCons "IfThenElse" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FplTerm) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FplTerm)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FplTerm) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "EqTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FplTerm) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FplTerm) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "BoolTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FplTerm)))))

fplReservedWords :: [String] Source #

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

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

constBool :: AParser st FplTerm 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 #

fplSortItem :: [String] -> AParser st FplSortItem Source #

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

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