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.Sign

Description

signature extension for FPL to keep track of constructors

Documentation

data SignExt Source #

Constructors

SignExt 

Fields

Instances

Eq SignExt Source # 

Methods

(==) :: SignExt -> SignExt -> Bool

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

Data SignExt Source # 

Methods

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

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

toConstr :: SignExt -> Constr

dataTypeOf :: SignExt -> DataType

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

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

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

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

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

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

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

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

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

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

Ord SignExt Source # 

Methods

compare :: SignExt -> SignExt -> Ordering

(<) :: SignExt -> SignExt -> Bool

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

(>) :: SignExt -> SignExt -> Bool

(>=) :: SignExt -> SignExt -> Bool

max :: SignExt -> SignExt -> SignExt

min :: SignExt -> SignExt -> SignExt

Show SignExt Source # 

Methods

showsPrec :: Int -> SignExt -> ShowS

show :: SignExt -> String

showList :: [SignExt] -> ShowS

Pretty SignExt Source # 
Sentences Fpl FplForm FplSign FplMor Symbol 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 #