5056N/ADescription : Functions for defining LF as a logical framework
5056N/ACopyright : (c) Kristina Sojakova, DFKI Bremen 2010
5056N/AMaintainer : k.sojakova@jacobs-university.de
5056N/Aded = Symbol baseB baseM "ded"
5056N/A , Def ded (Func [Const o] Type) Nothing ]
5056N/A{- ---------------------------------------------------------------
5056N/A--------------------------------------------------------------- -}
5056N/AwriteLogic :: String -> String
5152N/A let basic_specC = "BASIC_SPEC"
5056N/A symb_map_itemsC = "SYMB_MAP_ITEMS"
comp_opt = mkCompOpt [multiOpt, synOpt]
mod_decl = mkModDecl $ l ++ "." ++ "Logic_" ++ l
impts3 = mkImports [l ++ "." ++ "Syntax", l ++ "." ++ "Proof",
descriptionI = mkImpl "description" l "\"User-defined logic.\""
lang = mkInst "Language" l [] [descriptionI]
parse_basic_specI = inheritImpl "parse_basic_spec" l ml
parse_symb_itemsI = inheritImpl "parse_symb_items" l ml
parse_symb_map_itemsI = inheritImpl "parse_symb_map_items" l ml
syntax = mkInst "Syntax" l
[basic_specC, symb_itemsC, symb_map_itemsC]
[parse_basic_specI, parse_symb_itemsI, parse_symb_map_itemsI]
map_senI = inheritImpl "map_sen" l ml
sym_ofI = inheritImpl "sym_of" l ml
sentences = mkInst "Sentences" l [sentenceC, signC, morphismC,
symbolC] [map_senI, sym_ofI]
logic = mkInst "Logic" l [sublogicsC, basic_specC, sentenceC,
symb_itemsC, symb_map_itemsC, signC, morphismC,
symbolC, raw_symbolC, proof_treeC] []
basic_analysisI = mkImpl "basic_analysis" l
"Just $ basicAnalysisOL ltruth"
stat_symb_itemsI = inheritImpl "stat_symb_items" l ml
stat_symb_map_itemsI = inheritImpl "stat_symb_map_items" l ml
symbol_to_rawI = inheritImpl "symbol_to_raw" l ml
matchesI = inheritImpl "matches" l ml
empty_signatureI = mkImpl "empty_signature" l "cod $ ltruth"
is_subsigI = inheritImpl "is_subsig" l ml
subsig_inclusionI = inheritImpl "subsig_inclusion" l ml
signature_unionI = inheritImpl "signature_union" l ml
intersectionI = inheritImpl "intersection" l ml
generated_signI = inheritImpl "generated_sign" l ml
cogenerated_signI = inheritImpl "cogenerated_sign" l ml
induced_from_to_morphismI = mkImpl "induced_from_to_morphism" l
"inducedFromToMorphismOL ltruth"
induced_from_morphismI = inheritImpl "induced_from_morphism" l ml
analysis = mkInst "StaticAnalysis" l
[basic_specC, sentenceC, symb_itemsC, symb_map_itemsC,
signC, morphismC, symbolC, raw_symbolC]
[basic_analysisI, stat_symb_itemsI, stat_symb_map_itemsI,
symbol_to_rawI, matchesI, empty_signatureI, is_subsigI,
subsig_inclusionI, signature_unionI, intersectionI,
generated_signI, cogenerated_signI,
induced_from_to_morphismI, induced_from_morphismI]
body = intercalate "\n\n"
[mod_decl, impts1, impts2, impts3, lid, lang, syntax,
sentences, logic, analysis]
in header ++ "\n" ++ body
{- -----------------------------------------------------------------------------
----------------------------------------------------------------------------- -}
writeSyntax :: String -> Morphism -> String
let -- module declaration
mod_decl = mkModDecl $ l ++ "." ++ "Syntax"
ltruth_decl = mkDecl "ltruth" "Morphism" $ show ltruth
in intercalate "\n\n" [mod_decl, impts1, impts2, ltruth_decl]
writeProof :: String -> Morphism -> String
let -- module declaration
mod_decl = mkModDecl $ l ++ "." ++ "Proof"
lpf_decl = mkDecl "lpf" "Morphism" $ show lpf
in intercalate "\n\n" [mod_decl, impts1, impts2, lpf_decl]
writeModel :: String -> Morphism -> String
let -- module declaration
mod_decl = mkModDecl $ l ++ "." ++ "Model"
lmod_decl = mkDecl "lmod" "Morphism" $ show lmod
in intercalate "\n\n" [mod_decl, impts1, impts2, lmod_decl]
{- -----------------------------------------------------------------------------
----------------------------------------------------------------------------- -}
writeComorphism :: String -> String -> String
-> Morphism -> Morphism -> Morphism
writeComorphism c s t syn pf model =
let slC = s ++ "." ++ "Logic_" ++ s
tlC = t ++ "." ++ "Logic_" ++ t
basic_specC = "BASIC_SPEC"
symb_itemsC = "SYMB_ITEMS"
symb_map_itemsC = "SYMB_MAP_ITEMS"
comp_opt = mkCompOpt [multiOpt, synOpt]
mod_decl = mkModDecl $ "Comorphisms" ++ "." ++ c ++
" (" ++ c ++ " (..)" ++ ")"
impts2 = mkImports [s ++ ".Logic_" ++ s, s ++ ".Syntax",
s ++ ".Proof", s ++ ".Model"]
impts3 = mkImports [t ++ ".Logic_" ++ t, t ++ ".Syntax",
t ++ ".Proof", t ++ ".Model"]
-- impts5 = mkImports ["Common. " ...]
lang_nameI = mkImpl "language_name" c $ "\"" ++ c ++ "\""
descriptionI = mkImpl "description" c "\"User-defined comorphism\""
lang = mkInst "Language" c [] [lang_nameI, descriptionI]
sourceLogicC = mkImpl "sourceLogic" c slC
sourceSublogicC = mkImpl "sourceSublogic" c "()"
targetLogicC = mkImpl "targetLogic" c tlC
mapSublogicC = mkImpl "mapSublogic" c "()"
map_theoryC = mkImpl "map_theory" c "mapTheory cSyn"
map_morphismC = mkImpl "map_morphism" c "mapMor cSyn" -- TODO
map_sentenceC = mkImpl "map_sentence" c "mapSen cSyn"
map_symbolC = mkImpl "map_symbol" c "mapSymb cSyn"
comorphism = mkInst "Comorphism" c
slC, sublogicsC, basic_specC, sentenceC, symb_itemsC,
symb_map_itemsC, signC, morphismC, symbolC,
raw_symbolC, proof_treeC,
tlC, sublogicsC, basic_specC, sentenceC, symb_itemsC,
symb_map_itemsC, signC, morphismC, symbolC,
raw_symbolC, proof_treeC]
[sourceLogicC, sourceSublogicC, targetLogicC, mapSublogicC,
map_theoryC, map_morphismC, map_sentenceC, map_symbolC]
synMorphC = mkDecl "cSyn" "Morphism" $ show syn
proofMorphC = mkDecl "cPf" "Morphism" $ show pf
modelMorphC = mkDecl "cMod" "Morphism" $ show model
body = intercalate "\n\n"
[mod_decl, impts1, impts2, impts3, impts4, lid, lang, comorphism,
synMorphC, proofMorphC, modelMorphC]
in header ++ "\n" ++ body