Hets - the Heterogeneous Tool Set

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

Framework.AS

Description

 

Documentation

type NAME = IRI Source #

data FRAM Source #

Constructors

LF 
Isabelle 
Maude 

Instances

Eq FRAM Source # 

Methods

(==) :: FRAM -> FRAM -> Bool

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

Data FRAM Source # 

Methods

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

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

toConstr :: FRAM -> Constr

dataTypeOf :: FRAM -> DataType

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

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

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

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

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

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

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

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

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

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

Ord FRAM Source # 

Methods

compare :: FRAM -> FRAM -> Ordering

(<) :: FRAM -> FRAM -> Bool

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

(>) :: FRAM -> FRAM -> Bool

(>=) :: FRAM -> FRAM -> Bool

max :: FRAM -> FRAM -> FRAM

min :: FRAM -> FRAM -> FRAM

Show FRAM Source # 

Methods

showsPrec :: Int -> FRAM -> ShowS

show :: FRAM -> String

showList :: [FRAM] -> ShowS

Pretty FRAM Source # 

Methods

pretty :: FRAM -> Doc Source #

pretties :: [FRAM] -> Doc Source #

data LogicDef Source #

Instances

Eq LogicDef Source # 

Methods

(==) :: LogicDef -> LogicDef -> Bool

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

Data LogicDef Source # 

Methods

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

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

toConstr :: LogicDef -> Constr

dataTypeOf :: LogicDef -> DataType

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

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

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

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

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

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

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

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

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

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

Ord LogicDef Source # 

Methods

compare :: LogicDef -> LogicDef -> Ordering

(<) :: LogicDef -> LogicDef -> Bool

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

(>) :: LogicDef -> LogicDef -> Bool

(>=) :: LogicDef -> LogicDef -> Bool

max :: LogicDef -> LogicDef -> LogicDef

min :: LogicDef -> LogicDef -> LogicDef

Show LogicDef Source # 

Methods

showsPrec :: Int -> LogicDef -> ShowS

show :: LogicDef -> String

showList :: [LogicDef] -> ShowS

GetRange LogicDef Source # 
Pretty LogicDef Source # 
Sentences Framework () LogicDef Morphism () Source # 

Methods

map_sen :: Framework -> Morphism -> () -> Result () Source #

simplify_sen :: Framework -> LogicDef -> () -> () Source #

negation :: Framework -> () -> Maybe () Source #

print_sign :: Framework -> LogicDef -> Doc Source #

print_named :: Framework -> Named () -> Doc Source #

sym_of :: Framework -> LogicDef -> [Set ()] Source #

mostSymsOf :: Framework -> LogicDef -> [()] Source #

symmap_of :: Framework -> Morphism -> EndoMap () Source #

sym_name :: Framework -> () -> Id Source #

sym_label :: Framework -> () -> Maybe String Source #

fullSymName :: Framework -> () -> String Source #

symKind :: Framework -> () -> String Source #

symsOfSen :: Framework -> LogicDef -> () -> [()] Source #

pair_symbols :: Framework -> () -> () -> Result () Source #

Syntax Framework LogicDef () () () Source # 
StaticAnalysis Framework LogicDef () () () LogicDef Morphism () () Source # 

Methods

basic_analysis :: Framework -> Maybe ((LogicDef, LogicDef, GlobalAnnos) -> Result (LogicDef, ExtSign LogicDef (), [Named ()])) Source #

sen_analysis :: Framework -> Maybe ((LogicDef, LogicDef, ()) -> Result ()) Source #

extBasicAnalysis :: Framework -> IRI -> LibName -> LogicDef -> LogicDef -> GlobalAnnos -> Result (LogicDef, ExtSign LogicDef (), [Named ()]) Source #

stat_symb_map_items :: Framework -> LogicDef -> Maybe LogicDef -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: Framework -> LogicDef -> [()] -> Result [()] Source #

convertTheory :: Framework -> Maybe ((LogicDef, [Named ()]) -> LogicDef) Source #

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

quotient_term_algebra :: Framework -> Morphism -> [Named ()] -> Result (LogicDef, [Named ()]) Source #

signature_colimit :: Framework -> Gr LogicDef (Int, Morphism) -> Result (LogicDef, Map Int Morphism) Source #

qualify :: Framework -> SIMPLE_ID -> LibName -> Morphism -> LogicDef -> Result (Morphism, [Named ()]) Source #

symbol_to_raw :: Framework -> () -> () Source #

id_to_raw :: Framework -> Id -> () Source #

matches :: Framework -> () -> () -> Bool Source #

empty_signature :: Framework -> LogicDef Source #

add_symb_to_sign :: Framework -> LogicDef -> () -> Result LogicDef Source #

signature_union :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source #

signatureDiff :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source #

intersection :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source #

final_union :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source #

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

is_subsig :: Framework -> LogicDef -> LogicDef -> Bool Source #

subsig_inclusion :: Framework -> LogicDef -> LogicDef -> Result Morphism Source #

generated_sign :: Framework -> Set () -> LogicDef -> Result Morphism Source #

cogenerated_sign :: Framework -> Set () -> LogicDef -> Result Morphism Source #

induced_from_morphism :: Framework -> EndoMap () -> LogicDef -> Result Morphism Source #

induced_from_to_morphism :: Framework -> EndoMap () -> ExtSign LogicDef () -> ExtSign LogicDef () -> Result Morphism Source #

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

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

theory_to_taxonomy :: Framework -> TaxoGraphKind -> MMiSSOntology -> LogicDef -> [Named ()] -> Result MMiSSOntology Source #

corresp2th :: Framework -> String -> Bool -> LogicDef -> LogicDef -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (LogicDef, [Named ()], LogicDef, LogicDef, EndoMap (), EndoMap ()) Source #

equiv2cospan :: Framework -> LogicDef -> LogicDef -> [()] -> [()] -> Result (LogicDef, LogicDef, LogicDef, EndoMap (), EndoMap ()) Source #

extract_module :: Framework -> [IRI] -> (LogicDef, [Named ()]) -> Result (LogicDef, [Named ()]) Source #

Logic Framework () LogicDef () () () LogicDef Morphism () () () Source # 

Methods

parse_basic_sen :: Framework -> Maybe (LogicDef -> AParser st ()) Source #

stability :: Framework -> Stability Source #

data_logic :: Framework -> Maybe AnyLogic Source #

top_sublogic :: Framework -> () Source #

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

bottomSublogic :: Framework -> Maybe () Source #

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

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

proj_sublogic_epsilon :: Framework -> () -> LogicDef -> Morphism Source #

provers :: Framework -> [Prover LogicDef () Morphism () ()] Source #

default_prover :: Framework -> String Source #

cons_checkers :: Framework -> [ConsChecker LogicDef () () Morphism ()] Source #

conservativityCheck :: Framework -> [ConservativityChecker LogicDef () Morphism] Source #

empty_proof_tree :: Framework -> () Source #

syntaxTable :: Framework -> LogicDef -> Maybe SyntaxTable Source #

omdoc_metatheory :: Framework -> Maybe OMCD Source #

export_symToOmdoc :: Framework -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: Framework -> NameMap () -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: Framework -> SigMap () -> LogicDef -> [Named ()] -> Result [TCElement] Source #

omdocToSym :: Framework -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: Framework -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source #

addOMadtToTheory :: Framework -> SigMapI () -> (LogicDef, [Named ()]) -> [[OmdADT]] -> Result (LogicDef, [Named ()]) Source #

addOmdocToTheory :: Framework -> SigMapI () -> (LogicDef, [Named ()]) -> [TCElement] -> Result (LogicDef, [Named ()]) Source #

data ComorphismDef Source #

Instances

Eq ComorphismDef Source # 
Data ComorphismDef Source # 

Methods

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

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

toConstr :: ComorphismDef -> Constr

dataTypeOf :: ComorphismDef -> DataType

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

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

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

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

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

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

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

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

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

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

Ord ComorphismDef Source # 
Show ComorphismDef Source # 

Methods

showsPrec :: Int -> ComorphismDef -> ShowS

show :: ComorphismDef -> String

showList :: [ComorphismDef] -> ShowS

GetRange ComorphismDef Source # 
Pretty ComorphismDef Source # 
Sentences FrameworkCom () ComorphismDef MorphismCom () Source # 
Syntax FrameworkCom ComorphismDef () () () Source # 
StaticAnalysis FrameworkCom ComorphismDef () () () ComorphismDef MorphismCom () () Source # 

Methods

basic_analysis :: FrameworkCom -> Maybe ((ComorphismDef, ComorphismDef, GlobalAnnos) -> Result (ComorphismDef, ExtSign ComorphismDef (), [Named ()])) Source #

sen_analysis :: FrameworkCom -> Maybe ((ComorphismDef, ComorphismDef, ()) -> Result ()) Source #

extBasicAnalysis :: FrameworkCom -> IRI -> LibName -> ComorphismDef -> ComorphismDef -> GlobalAnnos -> Result (ComorphismDef, ExtSign ComorphismDef (), [Named ()]) Source #

stat_symb_map_items :: FrameworkCom -> ComorphismDef -> Maybe ComorphismDef -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: FrameworkCom -> ComorphismDef -> [()] -> Result [()] Source #

convertTheory :: FrameworkCom -> Maybe ((ComorphismDef, [Named ()]) -> ComorphismDef) Source #

ensures_amalgamability :: FrameworkCom -> ([CASLAmalgOpt], Gr ComorphismDef (Int, MorphismCom), [(Int, MorphismCom)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: FrameworkCom -> MorphismCom -> [Named ()] -> Result (ComorphismDef, [Named ()]) Source #

signature_colimit :: FrameworkCom -> Gr ComorphismDef (Int, MorphismCom) -> Result (ComorphismDef, Map Int MorphismCom) Source #

qualify :: FrameworkCom -> SIMPLE_ID -> LibName -> MorphismCom -> ComorphismDef -> Result (MorphismCom, [Named ()]) Source #

symbol_to_raw :: FrameworkCom -> () -> () Source #

id_to_raw :: FrameworkCom -> Id -> () Source #

matches :: FrameworkCom -> () -> () -> Bool Source #

empty_signature :: FrameworkCom -> ComorphismDef Source #

add_symb_to_sign :: FrameworkCom -> ComorphismDef -> () -> Result ComorphismDef Source #

signature_union :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source #

signatureDiff :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source #

intersection :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source #

final_union :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source #

morphism_union :: FrameworkCom -> MorphismCom -> MorphismCom -> Result MorphismCom Source #

is_subsig :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Bool Source #

subsig_inclusion :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result MorphismCom Source #

generated_sign :: FrameworkCom -> Set () -> ComorphismDef -> Result MorphismCom Source #

cogenerated_sign :: FrameworkCom -> Set () -> ComorphismDef -> Result MorphismCom Source #

induced_from_morphism :: FrameworkCom -> EndoMap () -> ComorphismDef -> Result MorphismCom Source #

induced_from_to_morphism :: FrameworkCom -> EndoMap () -> ExtSign ComorphismDef () -> ExtSign ComorphismDef () -> Result MorphismCom Source #

is_transportable :: FrameworkCom -> MorphismCom -> Bool Source #

is_injective :: FrameworkCom -> MorphismCom -> Bool Source #

theory_to_taxonomy :: FrameworkCom -> TaxoGraphKind -> MMiSSOntology -> ComorphismDef -> [Named ()] -> Result MMiSSOntology Source #

corresp2th :: FrameworkCom -> String -> Bool -> ComorphismDef -> ComorphismDef -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (ComorphismDef, [Named ()], ComorphismDef, ComorphismDef, EndoMap (), EndoMap ()) Source #

equiv2cospan :: FrameworkCom -> ComorphismDef -> ComorphismDef -> [()] -> [()] -> Result (ComorphismDef, ComorphismDef, ComorphismDef, EndoMap (), EndoMap ()) Source #

extract_module :: FrameworkCom -> [IRI] -> (ComorphismDef, [Named ()]) -> Result (ComorphismDef, [Named ()]) Source #

Logic FrameworkCom () ComorphismDef () () () ComorphismDef MorphismCom () () () Source # 

Methods

parse_basic_sen :: FrameworkCom -> Maybe (ComorphismDef -> AParser st ()) Source #

stability :: FrameworkCom -> Stability Source #

data_logic :: FrameworkCom -> Maybe AnyLogic Source #

top_sublogic :: FrameworkCom -> () Source #

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

bottomSublogic :: FrameworkCom -> Maybe () Source #

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

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

proj_sublogic_epsilon :: FrameworkCom -> () -> ComorphismDef -> MorphismCom Source #

provers :: FrameworkCom -> [Prover ComorphismDef () MorphismCom () ()] Source #

default_prover :: FrameworkCom -> String Source #

cons_checkers :: FrameworkCom -> [ConsChecker ComorphismDef () () MorphismCom ()] Source #

conservativityCheck :: FrameworkCom -> [ConservativityChecker ComorphismDef () MorphismCom] Source #

empty_proof_tree :: FrameworkCom -> () Source #

syntaxTable :: FrameworkCom -> ComorphismDef -> Maybe SyntaxTable Source #

omdoc_metatheory :: FrameworkCom -> Maybe OMCD Source #

export_symToOmdoc :: FrameworkCom -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: FrameworkCom -> NameMap () -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: FrameworkCom -> SigMap () -> ComorphismDef -> [Named ()] -> Result [TCElement] Source #

omdocToSym :: FrameworkCom -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: FrameworkCom -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source #

addOMadtToTheory :: FrameworkCom -> SigMapI () -> (ComorphismDef, [Named ()]) -> [[OmdADT]] -> Result (ComorphismDef, [Named ()]) Source #

addOmdocToTheory :: FrameworkCom -> SigMapI () -> (ComorphismDef, [Named ()]) -> [TCElement] -> Result (ComorphismDef, [Named ()]) Source #