Framework.hs revision b3bacd257ffcdd346b70ab690f03b28ad5f33fdc
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseModule : $Header$
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseDescription : Functions for defining LF as a logical framework
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseCopyright : (c) Kristina Sojakova, DFKI Bremen 2010
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseLicense : GPLv2 or higher, see LICENSE.txt
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseMaintainer : k.sojakova@jacobs-university.de
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BoseStability : experimental
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BosePortability : portable
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BosebaseB :: BASE
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BosebaseB = "Framework/specs/logics/propositional/syntax/base.elf"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BosebaseM :: MODULE
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BosebaseM = "Base"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseo = Symbol baseB baseM "o"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseded :: Symbol
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Boseded = Symbol baseB baseM "ded"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BosebaseSig :: Sign
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BosebaseSig = Sign baseB baseM
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose [ Def o Type Nothing
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose , Def ded (Func [Const o] Type) Nothing ]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bosesen_type_symbol :: Symbol
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bosesen_type_symbol = o
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-----------------------------------------------------------------
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-----------------------------------------------------------------
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BosewriteLogic :: String -> String
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BosewriteLogic l =
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose let basic_specC = "BASIC_SPEC"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose symb_itemsC = "SYMB_ITEMS"
e9c42ec738c213bd5f351567c20d404a280b32d0Sumit Bose symb_map_itemsC = "SYMB_MAP_ITEMS"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose signC = "Sign"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sentenceC = "Sentence"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose morphismC = "Morphism"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose symbolC = "Symbol"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose raw_symbolC = "RAW_SYM"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sublogicsC = "()"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose proof_treeC = "()"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- module declaration
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose comp_opt = mkCompOpt [multiOpt,synOpt]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose mod_decl = mkModDecl $ l ++ "." ++ "Logic_" ++ l
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose impts1 = mkImports ["Logic.Logic"]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose impts2 = mkImports ["LF.AS", "LF.Sign", "LF.Morphism",
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose impts3 = mkImports [l ++ "." ++ "Syntax"]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose lid = mkLid l
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose descriptionI = mkImpl "description" l "\"User-defined logic.\""
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose lang = mkInst "Language" l [] [descriptionI]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose parse_basic_specI = inheritImpl "parse_basic_spec" l ml
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose parse_symb_itemsI = inheritImpl "parse_symb_items" l ml
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose parse_symb_map_itemsI = inheritImpl "parse_symb_map_items" l ml
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose syntax = mkInst "Syntax" l
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose [basic_specC, symb_itemsC, symb_map_itemsC]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose [parse_basic_specI, parse_symb_itemsI, parse_symb_map_itemsI]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- sentences
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose map_senI = inheritImpl "map_sen" l ml
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sym_ofI = inheritImpl "sym_of" l ml
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sentences = mkInst "Sentences" l [sentenceC, signC, morphismC,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose symbolC] [map_senI, sym_ofI]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose logic = mkInst "Logic" l [sublogicsC, basic_specC, sentenceC,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose symb_itemsC, symb_map_itemsC, signC, morphismC,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose symbolC, raw_symbolC, proof_treeC] []
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- static analysis
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose basic_analysisI = mkImpl "basic_analysis" l
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose "Just $ basicAnalysisOL ltruth"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose stat_symb_itemsI = inheritImpl "stat_symb_items" l ml
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose stat_symb_map_itemsI = inheritImpl "stat_symb_map_items" l ml
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose symbol_to_rawI = inheritImpl "symbol_to_raw" l ml
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose matchesI = inheritImpl "matches" l ml
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose empty_signatureI = mkImpl "empty_signature" l "cod $ ltruth"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose is_subsigI = inheritImpl "is_subsig" l ml
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose subsig_inclusionI = inheritImpl "subsig_inclusion" l ml
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose signature_unionI = inheritImpl "signature_union" l ml
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose intersectionI = inheritImpl "intersection" l ml
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose generated_signI = mkImpl "generated_sign" l "genSigOL ltruth"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose cogenerated_signI = inheritImpl "cogenerated_sign" l ml
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose induced_from_to_morphismI = mkImpl "induced_from_to_morphism" l
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose "inducedFromToMorphismOL ltruth"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose analysis = mkInst "StaticAnalysis" l
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose [basic_specC, sentenceC, symb_itemsC, symb_map_itemsC,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose signC, morphismC, symbolC, raw_symbolC]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose [basic_analysisI, stat_symb_itemsI, stat_symb_map_itemsI,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose symbol_to_rawI, matchesI, empty_signatureI, is_subsigI,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose subsig_inclusionI, signature_unionI, intersectionI,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose generated_signI, cogenerated_signI,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose induced_from_to_morphismI]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose header = comp_opt
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose body = intercalate "\n\n" $
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose [mod_decl, impts1, impts2, impts3, lid, lang, syntax,
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose sentences, logic, analysis]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose in header ++ "\n" ++ body
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-----------------------------------------------------------------
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose-----------------------------------------------------------------
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BosewriteSyntax :: String -> Morphism -> String
a8d887323f83984679a7d9b827a70146656bb7b2Sumit BosewriteSyntax l ltruth =
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose let -- module declaration
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose mod_decl = mkModDecl $ l ++ "." ++ "Syntax"
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose impts2 = mkImports ["Data.Map"]
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose -- ltruth declaration
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose ltruth_decl = mkDecl "ltruth" "Morphism" $ show ltruth
a8d887323f83984679a7d9b827a70146656bb7b2Sumit Bose in intercalate "\n\n" [mod_decl, impts1, impts2, ltruth_decl]