Hets - the Heterogeneous Tool Set

Copyright(c) Stef Joosten Christian Maeder DFKI GmbH 2010
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable (import Logic.Logic)
Safe HaskellNone

Adl.Logic_Adl

Contents

Description

see Stef Joosten: Deriving Functional Specifications from Business Requirements with Ampersand

and https:/lab.cs.ru.nlBusinessRules/Requirements_engineering

Documentation

data Adl Source #

Constructors

Adl 

Instances

Show Adl Source # 

Methods

showsPrec :: Int -> Adl -> ShowS

show :: Adl -> String

showList :: [Adl] -> ShowS

Language Adl Source # 

Methods

language_name :: Adl -> String Source #

description :: Adl -> String Source #

Sentences Adl Sen Sign Morphism Symbol Source # 
Syntax Adl Context Symbol () () Source # 

Methods

parsersAndPrinters :: Adl -> Map String (PrefixMap -> AParser st Context, Context -> Doc) Source #

parse_basic_spec :: Adl -> Maybe (PrefixMap -> AParser st Context) Source #

parseSingleSymbItem :: Adl -> Maybe (AParser st ()) Source #

parse_symb_items :: Adl -> Maybe (AParser st ()) Source #

parse_symb_map_items :: Adl -> Maybe (AParser st ()) Source #

toItem :: Adl -> Context -> Item Source #

symb_items_name :: Adl -> () -> [String] Source #

StaticAnalysis Adl Context Sen () () Sign Morphism Symbol RawSymbol Source # 

Methods

basic_analysis :: Adl -> Maybe ((Context, Sign, GlobalAnnos) -> Result (Context, ExtSign Sign Symbol, [Named Sen])) Source #

sen_analysis :: Adl -> Maybe ((Context, Sign, Sen) -> Result Sen) Source #

extBasicAnalysis :: Adl -> IRI -> LibName -> Context -> Sign -> GlobalAnnos -> Result (Context, ExtSign Sign Symbol, [Named Sen]) Source #

stat_symb_map_items :: Adl -> Sign -> Maybe Sign -> [()] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Adl -> Sign -> [()] -> Result [RawSymbol] Source #

convertTheory :: Adl -> Maybe ((Sign, [Named Sen]) -> Context) Source #

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

quotient_term_algebra :: Adl -> Morphism -> [Named Sen] -> Result (Sign, [Named Sen]) Source #

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

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

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

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

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

empty_signature :: Adl -> Sign Source #

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

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

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

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

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

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

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

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

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

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

induced_from_morphism :: Adl -> EndoMap RawSymbol -> Sign -> Result Morphism Source #

induced_from_to_morphism :: Adl -> EndoMap RawSymbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

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

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

theory_to_taxonomy :: Adl -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sen] -> Result MMiSSOntology Source #

corresp2th :: Adl -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sen], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

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

extract_module :: Adl -> [IRI] -> (Sign, [Named Sen]) -> Result (Sign, [Named Sen]) Source #

Logic Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree Source # 

Methods

parse_basic_sen :: Adl -> Maybe (Context -> AParser st Sen) Source #

stability :: Adl -> Stability Source #

data_logic :: Adl -> Maybe AnyLogic Source #

top_sublogic :: Adl -> () Source #

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

bottomSublogic :: Adl -> Maybe () Source #

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

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

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

provers :: Adl -> [Prover Sign Sen Morphism () ProofTree] Source #

default_prover :: Adl -> String Source #

cons_checkers :: Adl -> [ConsChecker Sign Sen () Morphism ProofTree] Source #

conservativityCheck :: Adl -> [ConservativityChecker Sign Sen Morphism] Source #

empty_proof_tree :: Adl -> ProofTree Source #

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

omdoc_metatheory :: Adl -> Maybe OMCD Source #

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

export_senToOmdoc :: Adl -> NameMap Symbol -> Sen -> Result TCorOMElement Source #

export_theoryToOmdoc :: Adl -> SigMap Symbol -> Sign -> [Named Sen] -> Result [TCElement] Source #

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

omdocToSen :: Adl -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sen)) Source #

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

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

Comorphism Adl2CASL Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 

Orphan instances