{- |
Module      :  ./LF/Framework.hs
Description :  Functions for defining LF as a logical framework
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable
-}

module LF.Framework where

import LF.Sign
import LF.Morphism

import Framework.WriteLogicUtils

import Data.List

baseB :: BASE
baseB :: BASE
baseB = "logics/propositional/syntax/base.elf"

baseM :: MODULE
baseM :: BASE
baseM = "Base"

o :: Symbol
o :: Symbol
o = BASE -> BASE -> BASE -> Symbol
Symbol BASE
baseB BASE
baseM "o"

ded :: Symbol
ded :: Symbol
ded = BASE -> BASE -> BASE -> Symbol
Symbol BASE
baseB BASE
baseM "ded"

baseSig :: Sign
baseSig :: Sign
baseSig = BASE -> BASE -> [DEF] -> Sign
Sign BASE
baseB BASE
baseM
             [ Symbol -> EXP -> Maybe EXP -> DEF
Def Symbol
o EXP
Type Maybe EXP
forall a. Maybe a
Nothing
             , Symbol -> EXP -> Maybe EXP -> DEF
Def Symbol
ded ([EXP] -> EXP -> EXP
Func [Symbol -> EXP
Const Symbol
o] EXP
Type) Maybe EXP
forall a. Maybe a
Nothing ]

sen_type_symbol :: Symbol
sen_type_symbol :: Symbol
sen_type_symbol = Symbol
o

{- ---------------------------------------------------------------
--------------------------------------------------------------- -}

writeLogic :: String -> String
writeLogic :: BASE -> BASE
writeLogic l :: BASE
l =
  let basic_specC :: BASE
basic_specC = "BASIC_SPEC"
      symb_itemsC :: BASE
symb_itemsC = "SYMB_ITEMS"
      symb_map_itemsC :: BASE
symb_map_itemsC = "SYMB_MAP_ITEMS"
      signC :: BASE
signC = "Sign"
      sentenceC :: BASE
sentenceC = "Sentence"
      morphismC :: BASE
morphismC = "Morphism"
      symbolC :: BASE
symbolC = "Symbol"
      raw_symbolC :: BASE
raw_symbolC = "RAW_SYM"
      sublogicsC :: BASE
sublogicsC = "()"
      proof_treeC :: BASE
proof_treeC = "()"
      ml :: BASE
ml = "LF"

      -- module declaration
      comp_opt :: BASE
comp_opt = [BASE] -> BASE
mkCompOpt [BASE
multiOpt, BASE
synOpt]
      mod_decl :: BASE
mod_decl = BASE -> BASE
mkModDecl (BASE -> BASE) -> BASE -> BASE
forall a b. (a -> b) -> a -> b
$ BASE
l BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "." BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "Logic_" BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ BASE
l

      -- imports
      impts1 :: BASE
impts1 = [BASE] -> BASE
mkImports ["Logic.Logic"]
      impts2 :: BASE
impts2 = [BASE] -> BASE
mkImports ["LF.AS", "LF.Sign", "LF.Morphism",
                          "LF.Logic_LF", "LF.ImplOL"]
      impts3 :: BASE
impts3 = [BASE] -> BASE
mkImports [BASE
l BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "." BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "Syntax", BASE
l BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "." BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "Proof",
                          BASE
l BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "." BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "Model"]

      -- lid
      lid :: BASE
lid = BASE -> BASE
mkLid BASE
l

      -- language
      descriptionI :: BASE
descriptionI = BASE -> BASE -> BASE -> BASE
mkImpl "description" BASE
l "\"User-defined logic.\""
      lang :: BASE
lang = BASE -> BASE -> [BASE] -> [BASE] -> BASE
mkInst "Language" BASE
l [] [BASE
descriptionI]

      -- syntax
      parse_basic_specI :: BASE
parse_basic_specI = BASE -> BASE -> BASE -> BASE
inheritImpl "parse_basic_spec" BASE
l BASE
ml
      parse_symb_itemsI :: BASE
parse_symb_itemsI = BASE -> BASE -> BASE -> BASE
inheritImpl "parse_symb_items" BASE
l BASE
ml
      parse_symb_map_itemsI :: BASE
parse_symb_map_itemsI = BASE -> BASE -> BASE -> BASE
inheritImpl "parse_symb_map_items" BASE
l BASE
ml

      syntax :: BASE
syntax = BASE -> BASE -> [BASE] -> [BASE] -> BASE
mkInst "Syntax" BASE
l
                [BASE
basic_specC, BASE
symb_itemsC, BASE
symb_map_itemsC]
                [BASE
parse_basic_specI, BASE
parse_symb_itemsI, BASE
parse_symb_map_itemsI]

      -- sentences
      map_senI :: BASE
map_senI = BASE -> BASE -> BASE -> BASE
inheritImpl "map_sen" BASE
l BASE
ml
      sym_ofI :: BASE
sym_ofI = BASE -> BASE -> BASE -> BASE
inheritImpl "sym_of" BASE
l BASE
ml

      sentences :: BASE
sentences = BASE -> BASE -> [BASE] -> [BASE] -> BASE
mkInst "Sentences" BASE
l [BASE
sentenceC, BASE
signC, BASE
morphismC,
                    BASE
symbolC] [BASE
map_senI, BASE
sym_ofI]

      -- logic
      logic :: BASE
logic = BASE -> BASE -> [BASE] -> [BASE] -> BASE
mkInst "Logic" BASE
l [BASE
sublogicsC, BASE
basic_specC, BASE
sentenceC,
                BASE
symb_itemsC, BASE
symb_map_itemsC, BASE
signC, BASE
morphismC,
                BASE
symbolC, BASE
raw_symbolC, BASE
proof_treeC] []

      -- static analysis
      basic_analysisI :: BASE
basic_analysisI = BASE -> BASE -> BASE -> BASE
mkImpl "basic_analysis" BASE
l
         "Just $ basicAnalysisOL ltruth"
      stat_symb_itemsI :: BASE
stat_symb_itemsI = BASE -> BASE -> BASE -> BASE
inheritImpl "stat_symb_items" BASE
l BASE
ml
      stat_symb_map_itemsI :: BASE
stat_symb_map_itemsI = BASE -> BASE -> BASE -> BASE
inheritImpl "stat_symb_map_items" BASE
l BASE
ml
      symbol_to_rawI :: BASE
symbol_to_rawI = BASE -> BASE -> BASE -> BASE
inheritImpl "symbol_to_raw" BASE
l BASE
ml
      matchesI :: BASE
matchesI = BASE -> BASE -> BASE -> BASE
inheritImpl "matches" BASE
l BASE
ml
      empty_signatureI :: BASE
empty_signatureI = BASE -> BASE -> BASE -> BASE
mkImpl "empty_signature" BASE
l "cod $ ltruth"
      is_subsigI :: BASE
is_subsigI = BASE -> BASE -> BASE -> BASE
inheritImpl "is_subsig" BASE
l BASE
ml
      subsig_inclusionI :: BASE
subsig_inclusionI = BASE -> BASE -> BASE -> BASE
inheritImpl "subsig_inclusion" BASE
l BASE
ml
      signature_unionI :: BASE
signature_unionI = BASE -> BASE -> BASE -> BASE
inheritImpl "signature_union" BASE
l BASE
ml
      intersectionI :: BASE
intersectionI = BASE -> BASE -> BASE -> BASE
inheritImpl "intersection" BASE
l BASE
ml
      generated_signI :: BASE
generated_signI = BASE -> BASE -> BASE -> BASE
inheritImpl "generated_sign" BASE
l BASE
ml
      cogenerated_signI :: BASE
cogenerated_signI = BASE -> BASE -> BASE -> BASE
inheritImpl "cogenerated_sign" BASE
l BASE
ml
      induced_from_to_morphismI :: BASE
induced_from_to_morphismI = BASE -> BASE -> BASE -> BASE
mkImpl "induced_from_to_morphism" BASE
l
         "inducedFromToMorphismOL ltruth"
      induced_from_morphismI :: BASE
induced_from_morphismI = BASE -> BASE -> BASE -> BASE
inheritImpl "induced_from_morphism" BASE
l BASE
ml

      analysis :: BASE
analysis = BASE -> BASE -> [BASE] -> [BASE] -> BASE
mkInst "StaticAnalysis" BASE
l
                   [BASE
basic_specC, BASE
sentenceC, BASE
symb_itemsC, BASE
symb_map_itemsC,
                    BASE
signC, BASE
morphismC, BASE
symbolC, BASE
raw_symbolC]
                   [BASE
basic_analysisI, BASE
stat_symb_itemsI, BASE
stat_symb_map_itemsI,
                    BASE
symbol_to_rawI, BASE
matchesI, BASE
empty_signatureI, BASE
is_subsigI,
                    BASE
subsig_inclusionI, BASE
signature_unionI, BASE
intersectionI,
                    BASE
generated_signI, BASE
cogenerated_signI,
                    BASE
induced_from_to_morphismI, BASE
induced_from_morphismI]

      -- file
      header :: BASE
header = BASE
comp_opt
      body :: BASE
body = BASE -> [BASE] -> BASE
forall a. [a] -> [[a]] -> [a]
intercalate "\n\n"
               [BASE
mod_decl, BASE
impts1, BASE
impts2, BASE
impts3, BASE
lid, BASE
lang, BASE
syntax,
                BASE
sentences, BASE
logic, BASE
analysis]
      in BASE
header BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "\n" BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ BASE
body

{- -----------------------------------------------------------------------------
----------------------------------------------------------------------------- -}

writeSyntax :: String -> Morphism -> String
writeSyntax :: BASE -> Morphism -> BASE
writeSyntax l :: BASE
l ltruth :: Morphism
ltruth =
  let -- module declaration
      mod_decl :: BASE
mod_decl = BASE -> BASE
mkModDecl (BASE -> BASE) -> BASE -> BASE
forall a b. (a -> b) -> a -> b
$ BASE
l BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "." BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "Syntax"

      -- imports
      impts1 :: BASE
impts1 = [BASE] -> BASE
mkImports ["LF.Sign", "LF.Morphism"]
      impts2 :: BASE
impts2 = [BASE] -> BASE
mkImports ["Data.Map"]

      -- ltruth declaration
      ltruth_decl :: BASE
ltruth_decl = BASE -> BASE -> BASE -> BASE
mkDecl "ltruth" "Morphism" (BASE -> BASE) -> BASE -> BASE
forall a b. (a -> b) -> a -> b
$ Morphism -> BASE
forall a. Show a => a -> BASE
show Morphism
ltruth

      in BASE -> [BASE] -> BASE
forall a. [a] -> [[a]] -> [a]
intercalate "\n\n" [BASE
mod_decl, BASE
impts1, BASE
impts2, BASE
ltruth_decl]


writeProof :: String -> Morphism -> String
writeProof :: BASE -> Morphism -> BASE
writeProof l :: BASE
l lpf :: Morphism
lpf =
  let -- module declaration
      mod_decl :: BASE
mod_decl = BASE -> BASE
mkModDecl (BASE -> BASE) -> BASE -> BASE
forall a b. (a -> b) -> a -> b
$ BASE
l BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "." BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "Proof"

      -- imports
      impts1 :: BASE
impts1 = [BASE] -> BASE
mkImports ["LF.Sign", "LF.Morphism"]
      impts2 :: BASE
impts2 = [BASE] -> BASE
mkImports ["Data.Map"]

      -- lpf declaration
      lpf_decl :: BASE
lpf_decl = BASE -> BASE -> BASE -> BASE
mkDecl "lpf" "Morphism" (BASE -> BASE) -> BASE -> BASE
forall a b. (a -> b) -> a -> b
$ Morphism -> BASE
forall a. Show a => a -> BASE
show Morphism
lpf

  in BASE -> [BASE] -> BASE
forall a. [a] -> [[a]] -> [a]
intercalate "\n\n" [BASE
mod_decl, BASE
impts1, BASE
impts2, BASE
lpf_decl]


writeModel :: String -> Morphism -> String
writeModel :: BASE -> Morphism -> BASE
writeModel l :: BASE
l lmod :: Morphism
lmod =
     let -- module declaration
         mod_decl :: BASE
mod_decl = BASE -> BASE
mkModDecl (BASE -> BASE) -> BASE -> BASE
forall a b. (a -> b) -> a -> b
$ BASE
l BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "." BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "Model"

         -- imports
         impts1 :: BASE
impts1 = [BASE] -> BASE
mkImports ["LF.Sign", "LF.Morphism"]
         impts2 :: BASE
impts2 = [BASE] -> BASE
mkImports ["Data.Map"]

         -- lpf declaration
         lmod_decl :: BASE
lmod_decl = BASE -> BASE -> BASE -> BASE
mkDecl "lmod" "Morphism" (BASE -> BASE) -> BASE -> BASE
forall a b. (a -> b) -> a -> b
$ Morphism -> BASE
forall a. Show a => a -> BASE
show Morphism
lmod

     in BASE -> [BASE] -> BASE
forall a. [a] -> [[a]] -> [a]
intercalate "\n\n" [BASE
mod_decl, BASE
impts1, BASE
impts2, BASE
lmod_decl]

{- -----------------------------------------------------------------------------
----------------------------------------------------------------------------- -}

writeComorphism :: String -> String -> String
                    -> Morphism -> Morphism -> Morphism
                    -> String
writeComorphism :: BASE -> BASE -> BASE -> Morphism -> Morphism -> Morphism -> BASE
writeComorphism c :: BASE
c s :: BASE
s t :: BASE
t syn :: Morphism
syn pf :: Morphism
pf model :: Morphism
model =
  let slC :: BASE
slC = BASE
s BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "." BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "Logic_" BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ BASE
s
      tlC :: BASE
tlC = BASE
t BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "." BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "Logic_" BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ BASE
t
      sublogicsC :: BASE
sublogicsC = "()"
      basic_specC :: BASE
basic_specC = "BASIC_SPEC"
      sentenceC :: BASE
sentenceC = "Sentence"
      symb_itemsC :: BASE
symb_itemsC = "SYMB_ITEMS"
      symb_map_itemsC :: BASE
symb_map_itemsC = "SYMB_MAP_ITEMS"
      signC :: BASE
signC = "Sign"
      morphismC :: BASE
morphismC = "Morphism"
      symbolC :: BASE
symbolC = "Symbol"
      raw_symbolC :: BASE
raw_symbolC = "RAW_SYM"
      proof_treeC :: BASE
proof_treeC = "()"
-- mlC = "LF"

      -- module declaration
      comp_opt :: BASE
comp_opt = [BASE] -> BASE
mkCompOpt [BASE
multiOpt, BASE
synOpt]
      mod_decl :: BASE
mod_decl = BASE -> BASE
mkModDecl (BASE -> BASE) -> BASE -> BASE
forall a b. (a -> b) -> a -> b
$ "Comorphisms" BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "." BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ BASE
c BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++
                             " (" BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ BASE
c BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ " (..)" BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ ")"

      -- imports
      impts1 :: BASE
impts1 = [BASE] -> BASE
mkImports ["Logic.Logic" , "Logic.Comorphism"]
      impts2 :: BASE
impts2 = [BASE] -> BASE
mkImports [BASE
s BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ ".Logic_" BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ BASE
s, BASE
s BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ ".Syntax",
                          BASE
s BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ ".Proof", BASE
s BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ ".Model"]
      impts3 :: BASE
impts3 = [BASE] -> BASE
mkImports [BASE
t BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ ".Logic_" BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ BASE
t, BASE
t BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ ".Syntax",
                          BASE
t BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ ".Proof", BASE
t BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ ".Model"]
      impts4 :: BASE
impts4 = [BASE] -> BASE
mkImports ["LF.Logic_LF", "LF.Morphism", "LF.AS", "LF.Sign",
                          "LF.ComorphFram"]
-- impts5 = mkImports ["Common. " ...]

      -- lid
      lid :: BASE
lid = BASE -> BASE
mkLid BASE
c

      -- language
      lang_nameI :: BASE
lang_nameI = BASE -> BASE -> BASE -> BASE
mkImpl "language_name" BASE
c (BASE -> BASE) -> BASE -> BASE
forall a b. (a -> b) -> a -> b
$ "\"" BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ BASE
c BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "\""
      descriptionI :: BASE
descriptionI = BASE -> BASE -> BASE -> BASE
mkImpl "description" BASE
c "\"User-defined comorphism\""
      lang :: BASE
lang = BASE -> BASE -> [BASE] -> [BASE] -> BASE
mkInst "Language" BASE
c [] [BASE
lang_nameI, BASE
descriptionI]

      -- comorphism
      sourceLogicC :: BASE
sourceLogicC = BASE -> BASE -> BASE -> BASE
mkImpl "sourceLogic" BASE
c BASE
slC
      sourceSublogicC :: BASE
sourceSublogicC = BASE -> BASE -> BASE -> BASE
mkImpl "sourceSublogic" BASE
c "()"
      targetLogicC :: BASE
targetLogicC = BASE -> BASE -> BASE -> BASE
mkImpl "targetLogic" BASE
c BASE
tlC
      mapSublogicC :: BASE
mapSublogicC = BASE -> BASE -> BASE -> BASE
mkImpl "mapSublogic" BASE
c "()"
      map_theoryC :: BASE
map_theoryC = BASE -> BASE -> BASE -> BASE
mkImpl "map_theory" BASE
c "mapTheory cSyn"
      map_morphismC :: BASE
map_morphismC = BASE -> BASE -> BASE -> BASE
mkImpl "map_morphism" BASE
c "mapMor cSyn" -- TODO
      map_sentenceC :: BASE
map_sentenceC = BASE -> BASE -> BASE -> BASE
mkImpl "map_sentence" BASE
c "mapSen cSyn"
      map_symbolC :: BASE
map_symbolC = BASE -> BASE -> BASE -> BASE
mkImpl "map_symbol" BASE
c "mapSymb cSyn"
      comorphism :: BASE
comorphism = BASE -> BASE -> [BASE] -> [BASE] -> BASE
mkInst "Comorphism" BASE
c
                    [BASE
c,
                     BASE
slC, BASE
sublogicsC, BASE
basic_specC, BASE
sentenceC, BASE
symb_itemsC,
                          BASE
symb_map_itemsC, BASE
signC, BASE
morphismC, BASE
symbolC,
                          BASE
raw_symbolC, BASE
proof_treeC,
                     BASE
tlC, BASE
sublogicsC, BASE
basic_specC, BASE
sentenceC, BASE
symb_itemsC,
                          BASE
symb_map_itemsC, BASE
signC, BASE
morphismC, BASE
symbolC,
                          BASE
raw_symbolC, BASE
proof_treeC]
                    [BASE
sourceLogicC, BASE
sourceSublogicC, BASE
targetLogicC, BASE
mapSublogicC,
                        BASE
map_theoryC, BASE
map_morphismC, BASE
map_sentenceC, BASE
map_symbolC]

       -- the morphisms
      synMorphC :: BASE
synMorphC = BASE -> BASE -> BASE -> BASE
mkDecl "cSyn" "Morphism" (BASE -> BASE) -> BASE -> BASE
forall a b. (a -> b) -> a -> b
$ Morphism -> BASE
forall a. Show a => a -> BASE
show Morphism
syn
      proofMorphC :: BASE
proofMorphC = BASE -> BASE -> BASE -> BASE
mkDecl "cPf" "Morphism" (BASE -> BASE) -> BASE -> BASE
forall a b. (a -> b) -> a -> b
$ Morphism -> BASE
forall a. Show a => a -> BASE
show Morphism
pf
      modelMorphC :: BASE
modelMorphC = BASE -> BASE -> BASE -> BASE
mkDecl "cMod" "Morphism" (BASE -> BASE) -> BASE -> BASE
forall a b. (a -> b) -> a -> b
$ Morphism -> BASE
forall a. Show a => a -> BASE
show Morphism
model

      -- file
      header :: BASE
header = BASE
comp_opt
      body :: BASE
body = BASE -> [BASE] -> BASE
forall a. [a] -> [[a]] -> [a]
intercalate "\n\n"
                 [BASE
mod_decl, BASE
impts1, BASE
impts2, BASE
impts3, BASE
impts4, BASE
lid, BASE
lang, BASE
comorphism,
                      BASE
synMorphC, BASE
proofMorphC, BASE
modelMorphC]
  in BASE
header BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "\n" BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ BASE
body