content: {- |
  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 = "logics/propositional/syntax/base.elf"
  
  baseM :: MODULE
  baseM = "Base"
  
  o :: Symbol
  o = Symbol baseB baseM "o"
  
  ded :: Symbol
  ded = Symbol baseB baseM "ded"
  
  baseSig :: Sign
  baseSig = Sign baseB baseM
               [ Def o Type Nothing
               , Def ded (Func [Const o] Type) Nothing ]
  
  sen_type_symbol :: Symbol
  sen_type_symbol = o
  
  {- ---------------------------------------------------------------
  --------------------------------------------------------------- -}
  
  writeLogic :: String -> String
  writeLogic l =
    let basic_specC = "BASIC_SPEC"
        symb_itemsC = "SYMB_ITEMS"
        symb_map_itemsC = "SYMB_MAP_ITEMS"
        signC = "Sign"
        sentenceC = "Sentence"
        morphismC = "Morphism"
        symbolC = "Symbol"
        raw_symbolC = "RAW_SYM"
        sublogicsC = "()"
        proof_treeC = "()"
        ml = "LF"
  
        -- module declaration
        comp_opt = mkCompOpt [multiOpt, synOpt]
        mod_decl = mkModDecl $ l ++ "." ++ "Logic_" ++ l
  
        -- imports
        impts1 = mkImports ["Logic.Logic"]
        impts2 = mkImports ["LF.AS", "LF.Sign", "LF.Morphism",
                            "LF.Logic_LF", "LF.ImplOL"]
        impts3 = mkImports [l ++ "." ++ "Syntax", l ++ "." ++ "Proof",
                            l ++ "." ++ "Model"]
  
        -- lid
        lid = mkLid l
  
        -- language
        descriptionI = mkImpl "description" l "\"User-defined logic.\""
        lang = mkInst "Language" l [] [descriptionI]
  
        -- syntax
        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]
  
        -- sentences
        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
        logic = mkInst "Logic" l [sublogicsC, basic_specC, sentenceC,
                  symb_itemsC, symb_map_itemsC, signC, morphismC,
                  symbolC, raw_symbolC, proof_treeC] []
  
        -- static analysis
        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]
  
        -- file
        header = comp_opt
        body = intercalate "\n\n"
                 [mod_decl, impts1, impts2, impts3, lid, lang, syntax,
                  sentences, logic, analysis]
        in header ++ "\n" ++ body
  
  {- -----------------------------------------------------------------------------
  ----------------------------------------------------------------------------- -}
  
  writeSyntax :: String -> Morphism -> String
  writeSyntax l ltruth =
    let -- module declaration
        mod_decl = mkModDecl $ l ++ "." ++ "Syntax"
  
        -- imports
        impts1 = mkImports ["LF.Sign", "LF.Morphism"]
        impts2 = mkImports ["Data.Map"]
  
        -- ltruth declaration
        ltruth_decl = mkDecl "ltruth" "Morphism" $ show ltruth
  
        in intercalate "\n\n" [mod_decl, impts1, impts2, ltruth_decl]
  
  
  writeProof :: String -> Morphism -> String
  writeProof l lpf =
    let -- module declaration
        mod_decl = mkModDecl $ l ++ "." ++ "Proof"
  
        -- imports
        impts1 = mkImports ["LF.Sign", "LF.Morphism"]
        impts2 = mkImports ["Data.Map"]
  
        -- lpf declaration
        lpf_decl = mkDecl "lpf" "Morphism" $ show lpf
  
    in intercalate "\n\n" [mod_decl, impts1, impts2, lpf_decl]
  
  
  writeModel :: String -> Morphism -> String
  writeModel l lmod =
       let -- module declaration
           mod_decl = mkModDecl $ l ++ "." ++ "Model"
  
           -- imports
           impts1 = mkImports ["LF.Sign", "LF.Morphism"]
           impts2 = mkImports ["Data.Map"]
  
           -- lpf declaration
           lmod_decl = mkDecl "lmod" "Morphism" $ show lmod
  
       in intercalate "\n\n" [mod_decl, impts1, impts2, lmod_decl]
  
  {- -----------------------------------------------------------------------------
  ----------------------------------------------------------------------------- -}
  
  writeComorphism :: String -> String -> String
                      -> Morphism -> Morphism -> Morphism
                      -> String
  writeComorphism c s t syn pf model =
    let slC = s ++ "." ++ "Logic_" ++ s
        tlC = t ++ "." ++ "Logic_" ++ t
        sublogicsC = "()"
        basic_specC = "BASIC_SPEC"
        sentenceC = "Sentence"
        symb_itemsC = "SYMB_ITEMS"
        symb_map_itemsC = "SYMB_MAP_ITEMS"
        signC = "Sign"
        morphismC = "Morphism"
        symbolC = "Symbol"
        raw_symbolC = "RAW_SYM"
        proof_treeC = "()"
  -- mlC = "LF"
  
        -- module declaration
        comp_opt = mkCompOpt [multiOpt, synOpt]
        mod_decl = mkModDecl $ "Comorphisms" ++ "." ++ c ++
                               " (" ++ c ++ " (..)" ++ ")"
  
        -- imports
        impts1 = mkImports ["Logic.Logic" , "Logic.Comorphism"]
        impts2 = mkImports [s ++ ".Logic_" ++ s, s ++ ".Syntax",
                            s ++ ".Proof", s ++ ".Model"]
        impts3 = mkImports [t ++ ".Logic_" ++ t, t ++ ".Syntax",
                            t ++ ".Proof", t ++ ".Model"]
        impts4 = mkImports ["LF.Logic_LF", "LF.Morphism", "LF.AS", "LF.Sign",
                            "LF.ComorphFram"]
  -- impts5 = mkImports ["Common. " ...]
  
        -- lid
        lid = mkLid c
  
        -- language
        lang_nameI = mkImpl "language_name" c $ "\"" ++ c ++ "\""
        descriptionI = mkImpl "description" c "\"User-defined comorphism\""
        lang = mkInst "Language" c [] [lang_nameI, descriptionI]
  
        -- comorphism
        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
                      [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]
  
         -- the morphisms
        synMorphC = mkDecl "cSyn" "Morphism" $ show syn
        proofMorphC = mkDecl "cPf" "Morphism" $ show pf
        modelMorphC = mkDecl "cMod" "Morphism" $ show model
  
        -- file
        header = comp_opt
        body = intercalate "\n\n"
                   [mod_decl, impts1, impts2, impts3, impts4, lid, lang, comorphism,
                        synMorphC, proofMorphC, modelMorphC]
    in header ++ "\n" ++ body
  