Hets - the Heterogeneous Tool Set

Copyright(c) Kristina Sojakova DFKI Bremen 2009
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerk.sojakova@jacobs-university.de
Stabilityexperimental
Portabilityportable
Safe HaskellSafe

LF.Sign

Description

 

Documentation

type VAR = String Source #

type NAME = String Source #

type MODULE = String Source #

type BASE = String Source #

data Symbol Source #

Constructors

Symbol 

Instances

Eq Symbol Source # 

Methods

(==) :: Symbol -> Symbol -> Bool

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

Data Symbol Source # 

Methods

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

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

toConstr :: Symbol -> Constr

dataTypeOf :: Symbol -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Symbol Source # 

Methods

compare :: Symbol -> Symbol -> Ordering

(<) :: Symbol -> Symbol -> Bool

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

(>) :: Symbol -> Symbol -> Bool

(>=) :: Symbol -> Symbol -> Bool

max :: Symbol -> Symbol -> Symbol

min :: Symbol -> Symbol -> Symbol

Show Symbol Source # 

Methods

showsPrec :: Int -> Symbol -> ShowS

show :: Symbol -> String

showList :: [Symbol] -> ShowS

GetRange Symbol Source # 
Pretty Symbol Source # 
Sentences LF Sentence Sign Morphism Symbol Source # 
Syntax LF BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
StaticAnalysis LF BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RAW_SYM Source # 

Methods

basic_analysis :: LF -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence])) Source #

sen_analysis :: LF -> Maybe ((BASIC_SPEC, Sign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: LF -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: LF -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RAW_SYM) Source #

stat_symb_items :: LF -> Sign -> [SYMB_ITEMS] -> Result [RAW_SYM] Source #

convertTheory :: LF -> Maybe ((Sign, [Named Sentence]) -> BASIC_SPEC) Source #

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

quotient_term_algebra :: LF -> Morphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: LF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

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

symbol_to_raw :: LF -> Symbol -> RAW_SYM Source #

id_to_raw :: LF -> Id -> RAW_SYM Source #

matches :: LF -> Symbol -> RAW_SYM -> Bool Source #

empty_signature :: LF -> Sign Source #

add_symb_to_sign :: LF -> Sign -> Symbol -> Result Sign Source #

signature_union :: LF -> Sign -> Sign -> Result Sign Source #

signatureDiff :: LF -> Sign -> Sign -> Result Sign Source #

intersection :: LF -> Sign -> Sign -> Result Sign Source #

final_union :: LF -> Sign -> Sign -> Result Sign Source #

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

is_subsig :: LF -> Sign -> Sign -> Bool Source #

subsig_inclusion :: LF -> Sign -> Sign -> Result Morphism Source #

generated_sign :: LF -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: LF -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: LF -> EndoMap RAW_SYM -> Sign -> Result Morphism Source #

induced_from_to_morphism :: LF -> EndoMap RAW_SYM -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

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

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

theory_to_taxonomy :: LF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: LF -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: LF -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: LF -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

LogicalFramework LF () BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RAW_SYM () Source # 

Methods

base_sig :: LF -> Sign Source #

write_logic :: LF -> String -> String Source #

write_syntax :: LF -> String -> Morphism -> String Source #

write_proof :: LF -> String -> Morphism -> String Source #

write_model :: LF -> String -> Morphism -> String Source #

read_morphism :: LF -> FilePath -> Morphism Source #

write_comorphism :: LF -> String -> String -> String -> Morphism -> Morphism -> Morphism -> String Source #

Logic LF () BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RAW_SYM () Source # 

Methods

parse_basic_sen :: LF -> Maybe (BASIC_SPEC -> AParser st Sentence) Source #

stability :: LF -> Stability Source #

data_logic :: LF -> Maybe AnyLogic Source #

top_sublogic :: LF -> () Source #

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

bottomSublogic :: LF -> Maybe () Source #

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

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

proj_sublogic_epsilon :: LF -> () -> Sign -> Morphism Source #

provers :: LF -> [Prover Sign Sentence Morphism () ()] Source #

default_prover :: LF -> String Source #

cons_checkers :: LF -> [ConsChecker Sign Sentence () Morphism ()] Source #

conservativityCheck :: LF -> [ConservativityChecker Sign Sentence Morphism] Source #

empty_proof_tree :: LF -> () Source #

syntaxTable :: LF -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: LF -> Maybe OMCD Source #

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

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

export_theoryToOmdoc :: LF -> SigMap Symbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

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

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

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

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

type RAW_SYM = String Source #

data EXP Source #

Instances

Eq EXP Source # 

Methods

(==) :: EXP -> EXP -> Bool

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

Data EXP Source # 

Methods

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

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

toConstr :: EXP -> Constr

dataTypeOf :: EXP -> DataType

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

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

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

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

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

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

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

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

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

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

Ord EXP Source # 

Methods

compare :: EXP -> EXP -> Ordering

(<) :: EXP -> EXP -> Bool

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

(>) :: EXP -> EXP -> Bool

(>=) :: EXP -> EXP -> Bool

max :: EXP -> EXP -> EXP

min :: EXP -> EXP -> EXP

Show EXP Source # 

Methods

showsPrec :: Int -> EXP -> ShowS

show :: EXP -> String

showList :: [EXP] -> ShowS

GetRange EXP Source # 
Pretty EXP Source # 

Methods

pretty :: EXP -> Doc Source #

pretties :: [EXP] -> Doc Source #

Sentences LF Sentence Sign Morphism Symbol Source # 
StaticAnalysis LF BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RAW_SYM Source # 

Methods

basic_analysis :: LF -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence])) Source #

sen_analysis :: LF -> Maybe ((BASIC_SPEC, Sign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: LF -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: LF -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RAW_SYM) Source #

stat_symb_items :: LF -> Sign -> [SYMB_ITEMS] -> Result [RAW_SYM] Source #

convertTheory :: LF -> Maybe ((Sign, [Named Sentence]) -> BASIC_SPEC) Source #

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

quotient_term_algebra :: LF -> Morphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: LF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

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

symbol_to_raw :: LF -> Symbol -> RAW_SYM Source #

id_to_raw :: LF -> Id -> RAW_SYM Source #

matches :: LF -> Symbol -> RAW_SYM -> Bool Source #

empty_signature :: LF -> Sign Source #

add_symb_to_sign :: LF -> Sign -> Symbol -> Result Sign Source #

signature_union :: LF -> Sign -> Sign -> Result Sign Source #

signatureDiff :: LF -> Sign -> Sign -> Result Sign Source #

intersection :: LF -> Sign -> Sign -> Result Sign Source #

final_union :: LF -> Sign -> Sign -> Result Sign Source #

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

is_subsig :: LF -> Sign -> Sign -> Bool Source #

subsig_inclusion :: LF -> Sign -> Sign -> Result Morphism Source #

generated_sign :: LF -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: LF -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: LF -> EndoMap RAW_SYM -> Sign -> Result Morphism Source #

induced_from_to_morphism :: LF -> EndoMap RAW_SYM -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

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

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

theory_to_taxonomy :: LF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: LF -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: LF -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: LF -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

LogicalFramework LF () BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RAW_SYM () Source # 

Methods

base_sig :: LF -> Sign Source #

write_logic :: LF -> String -> String Source #

write_syntax :: LF -> String -> Morphism -> String Source #

write_proof :: LF -> String -> Morphism -> String Source #

write_model :: LF -> String -> Morphism -> String Source #

read_morphism :: LF -> FilePath -> Morphism Source #

write_comorphism :: LF -> String -> String -> String -> Morphism -> Morphism -> Morphism -> String Source #

Logic LF () BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RAW_SYM () Source # 

Methods

parse_basic_sen :: LF -> Maybe (BASIC_SPEC -> AParser st Sentence) Source #

stability :: LF -> Stability Source #

data_logic :: LF -> Maybe AnyLogic Source #

top_sublogic :: LF -> () Source #

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

bottomSublogic :: LF -> Maybe () Source #

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

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

proj_sublogic_epsilon :: LF -> () -> Sign -> Morphism Source #

provers :: LF -> [Prover Sign Sentence Morphism () ()] Source #

default_prover :: LF -> String Source #

cons_checkers :: LF -> [ConsChecker Sign Sentence () Morphism ()] Source #

conservativityCheck :: LF -> [ConservativityChecker Sign Sentence Morphism] Source #

empty_proof_tree :: LF -> () Source #

syntaxTable :: LF -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: LF -> Maybe OMCD Source #

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

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

export_theoryToOmdoc :: LF -> SigMap Symbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

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

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

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

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

type CONTEXT = [(VAR, EXP)] Source #

data DEF Source #

Constructors

Def 

Fields

Instances

Eq DEF Source # 

Methods

(==) :: DEF -> DEF -> Bool

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

Data DEF Source # 

Methods

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

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

toConstr :: DEF -> Constr

dataTypeOf :: DEF -> DataType

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

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

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

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

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

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

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

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

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

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

Ord DEF Source # 

Methods

compare :: DEF -> DEF -> Ordering

(<) :: DEF -> DEF -> Bool

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

(>) :: DEF -> DEF -> Bool

(>=) :: DEF -> DEF -> Bool

max :: DEF -> DEF -> DEF

min :: DEF -> DEF -> DEF

Show DEF Source # 

Methods

showsPrec :: Int -> DEF -> ShowS

show :: DEF -> String

showList :: [DEF] -> ShowS

Pretty DEF Source # 

Methods

pretty :: DEF -> Doc Source #

pretties :: [DEF] -> Doc Source #

data Sign Source #

Constructors

Sign 

Fields

Instances

Eq Sign Source # 

Methods

(==) :: Sign -> Sign -> Bool

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

Data Sign Source # 

Methods

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

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

toConstr :: Sign -> Constr

dataTypeOf :: Sign -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Sign Source # 

Methods

compare :: Sign -> Sign -> Ordering

(<) :: Sign -> Sign -> Bool

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

(>) :: Sign -> Sign -> Bool

(>=) :: Sign -> Sign -> Bool

max :: Sign -> Sign -> Sign

min :: Sign -> Sign -> Sign

Show Sign Source # 

Methods

showsPrec :: Int -> Sign -> ShowS

show :: Sign -> String

showList :: [Sign] -> ShowS

Pretty Sign Source # 

Methods

pretty :: Sign -> Doc Source #

pretties :: [Sign] -> Doc Source #

Sentences LF Sentence Sign Morphism Symbol Source # 
StaticAnalysis LF BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RAW_SYM Source # 

Methods

basic_analysis :: LF -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence])) Source #

sen_analysis :: LF -> Maybe ((BASIC_SPEC, Sign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: LF -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: LF -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RAW_SYM) Source #

stat_symb_items :: LF -> Sign -> [SYMB_ITEMS] -> Result [RAW_SYM] Source #

convertTheory :: LF -> Maybe ((Sign, [Named Sentence]) -> BASIC_SPEC) Source #

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

quotient_term_algebra :: LF -> Morphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: LF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

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

symbol_to_raw :: LF -> Symbol -> RAW_SYM Source #

id_to_raw :: LF -> Id -> RAW_SYM Source #

matches :: LF -> Symbol -> RAW_SYM -> Bool Source #

empty_signature :: LF -> Sign Source #

add_symb_to_sign :: LF -> Sign -> Symbol -> Result Sign Source #

signature_union :: LF -> Sign -> Sign -> Result Sign Source #

signatureDiff :: LF -> Sign -> Sign -> Result Sign Source #

intersection :: LF -> Sign -> Sign -> Result Sign Source #

final_union :: LF -> Sign -> Sign -> Result Sign Source #

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

is_subsig :: LF -> Sign -> Sign -> Bool Source #

subsig_inclusion :: LF -> Sign -> Sign -> Result Morphism Source #

generated_sign :: LF -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: LF -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: LF -> EndoMap RAW_SYM -> Sign -> Result Morphism Source #

induced_from_to_morphism :: LF -> EndoMap RAW_SYM -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

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

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

theory_to_taxonomy :: LF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: LF -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: LF -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: LF -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

LogicalFramework LF () BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RAW_SYM () Source # 

Methods

base_sig :: LF -> Sign Source #

write_logic :: LF -> String -> String Source #

write_syntax :: LF -> String -> Morphism -> String Source #

write_proof :: LF -> String -> Morphism -> String Source #

write_model :: LF -> String -> Morphism -> String Source #

read_morphism :: LF -> FilePath -> Morphism Source #

write_comorphism :: LF -> String -> String -> String -> Morphism -> Morphism -> Morphism -> String Source #

Logic LF () BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RAW_SYM () Source # 

Methods

parse_basic_sen :: LF -> Maybe (BASIC_SPEC -> AParser st Sentence) Source #

stability :: LF -> Stability Source #

data_logic :: LF -> Maybe AnyLogic Source #

top_sublogic :: LF -> () Source #

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

bottomSublogic :: LF -> Maybe () Source #

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

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

proj_sublogic_epsilon :: LF -> () -> Sign -> Morphism Source #

provers :: LF -> [Prover Sign Sentence Morphism () ()] Source #

default_prover :: LF -> String Source #

cons_checkers :: LF -> [ConsChecker Sign Sentence () Morphism ()] Source #

conservativityCheck :: LF -> [ConservativityChecker Sign Sentence Morphism] Source #

empty_proof_tree :: LF -> () Source #

syntaxTable :: LF -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: LF -> Maybe OMCD Source #

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

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

export_theoryToOmdoc :: LF -> SigMap Symbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

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

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

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

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

isSym :: RAW_SYM -> Bool Source #

gen_base :: String Source #

gen_module :: String Source #

isConstant :: Symbol -> Sign -> Bool Source #

isLocalSym :: Symbol -> Sign -> Bool Source #

getSymType :: Symbol -> Sign -> Maybe EXP Source #

isSubsig :: Sign -> Sign -> Bool Source #