{- |
Module      :  ./Framework/Analysis.hs
Description :  Analyzes a logic definition
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 Framework.Analysis
     ( anaLogicDef
     , anaComorphismDef
     , addLogic2LogicList
     ) where

import Framework.AS
import Framework.Logic_Framework

import qualified LF.Logic_LF as Logic_LF
import qualified Isabelle.Logic_Isabelle as Logic_Isabelle
import qualified Maude.Logic_Maude as Logic_Maude

import Data.List
import Data.Maybe
import qualified Data.Map as Map

import Static.DevGraph
import Static.DgUtils
import Static.GTheory

import System.Directory

import Logic.Grothendieck
import Logic.ExtSign
import Logic.Logic
import Logic.Comorphism
import Logic.Coerce

import Common.Result
import Common.Parsec
import Common.AnnoState
import Common.Lexer
import Common.Token
import Common.Id
import Common.IRI (iriToStringUnsecure, nullIRI)
import Common.Keywords
import Common.ExtSign

import Text.ParserCombinators.Parsec

import LF.Framework ()

dynLogicsDir :: FilePath
dynLogicsDir :: FilePath
dynLogicsDir = "Comorphisms"

dynLogicsFile :: FilePath
dynLogicsFile :: FilePath
dynLogicsFile = "DynLogicList.hs"

dynLogicsCon :: String
dynLogicsCon :: FilePath
dynLogicsCon = "dynLogicList"

dynComorphismsDir :: FilePath
dynComorphismsDir :: FilePath
dynComorphismsDir = "Comorphisms"

dynComorphismsFile :: FilePath
dynComorphismsFile :: FilePath
dynComorphismsFile = "DynComorphismList.hs"

dynComorphismsCon :: String
dynComorphismsCon :: FilePath
dynComorphismsCon = "dynComorphismList"

{- ----------------------------------------------------------------------------
Logic analysis -}

-- analyzes a logic definition
anaLogicDef :: LogicDef -> DGraph -> IO DGraph
anaLogicDef :: LogicDef -> DGraph -> IO DGraph
anaLogicDef ld :: LogicDef
ld dg :: DGraph
dg =
  case LogicDef -> FRAM
meta LogicDef
ld of
    LF -> LF -> LogicDef -> DGraph -> IO DGraph
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> LogicDef -> DGraph -> IO DGraph
anaLogicDefH LF
Logic_LF.LF LogicDef
ld DGraph
dg
    Isabelle -> Isabelle -> LogicDef -> DGraph -> IO DGraph
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> LogicDef -> DGraph -> IO DGraph
anaLogicDefH Isabelle
Logic_Isabelle.Isabelle LogicDef
ld DGraph
dg
    Maude -> Maude -> LogicDef -> DGraph -> IO DGraph
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> LogicDef -> DGraph -> IO DGraph
anaLogicDefH Maude
Logic_Maude.Maude LogicDef
ld DGraph
dg

anaLogicDefH :: LogicalFramework lid sublogics basic_spec sentence symb_items
                       symb_map_items sign morphism symbol raw_symbol
                       proof_tree
                => lid -> LogicDef -> DGraph -> IO DGraph
anaLogicDefH :: lid -> LogicDef -> DGraph -> IO DGraph
anaLogicDefH ml :: lid
ml ld :: LogicDef
ld dg :: DGraph
dg =
  case lid
-> LogicDef
-> DGraph
-> Result (morphism, Maybe morphism, Maybe sign, Maybe morphism)
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> LogicDef
-> DGraph
-> Result (morphism, Maybe morphism, Maybe sign, Maybe morphism)
retrieveDiagram lid
ml LogicDef
ld DGraph
dg of
       Result _ (Just (ltruth :: morphism
ltruth, lmod :: Maybe morphism
lmod, found :: Maybe sign
found, lpf :: Maybe morphism
lpf)) -> do
           let l :: FilePath
l = IRI -> FilePath
iriToStringUnsecure (IRI -> FilePath) -> IRI -> FilePath
forall a b. (a -> b) -> a -> b
$ LogicDef -> IRI
newlogicName LogicDef
ld
           lid
-> FilePath
-> morphism
-> Maybe morphism
-> Maybe sign
-> Maybe morphism
-> IO ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> FilePath
-> morphism
-> Maybe morphism
-> Maybe sign
-> Maybe morphism
-> IO ()
buildLogic lid
ml FilePath
l morphism
ltruth Maybe morphism
lmod Maybe sign
found Maybe morphism
lpf
           FilePath -> IO ()
addLogic2LogicList FilePath
l
           DGraph -> IO DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph -> IO DGraph) -> DGraph -> IO DGraph
forall a b. (a -> b) -> a -> b
$ LogicDef -> DGraph -> DGraph
addLogicDef2DG LogicDef
ld DGraph
dg
       _ -> FilePath -> IO DGraph
forall a. HasCallStack => FilePath -> a
error ""

{- constructs the diagram in the signature category of the meta logic
   which represents the object logic -}
retrieveDiagram :: LogicalFramework lid sublogics basic_spec sentence symb_items
                          symb_map_items sign morphism symbol raw_symbol
                          proof_tree
                   => lid -> LogicDef -> DGraph ->
                      Result (morphism, Maybe morphism,
                              Maybe sign, Maybe morphism)
retrieveDiagram :: lid
-> LogicDef
-> DGraph
-> Result (morphism, Maybe morphism, Maybe sign, Maybe morphism)
retrieveDiagram ml :: lid
ml (LogicDef _ _ s :: IRI
s m :: IRI
m f :: IRI
f p :: IRI
p _) dg :: DGraph
dg = do
  morphism
ltruth <- lid -> IRI -> DGraph -> Result morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> IRI -> DGraph -> Result morphism
lookupMorph lid
ml IRI
s DGraph
dg
  Maybe morphism
lmod <- if IRI
m IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
nullIRI
             then Maybe morphism -> Result (Maybe morphism)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe morphism
forall a. Maybe a
Nothing
             else do morphism
v <- lid -> IRI -> DGraph -> Result morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> IRI -> DGraph -> Result morphism
lookupMorph lid
ml IRI
m DGraph
dg
                     Maybe morphism -> Result (Maybe morphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe morphism -> Result (Maybe morphism))
-> Maybe morphism -> Result (Maybe morphism)
forall a b. (a -> b) -> a -> b
$ morphism -> Maybe morphism
forall a. a -> Maybe a
Just morphism
v
  Maybe sign
found <- if IRI
f IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
nullIRI
              then Maybe sign -> Result (Maybe sign)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe sign
forall a. Maybe a
Nothing
              else do sign
v <- lid -> IRI -> DGraph -> Result sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> IRI -> DGraph -> Result sign
lookupSig lid
ml IRI
f DGraph
dg
                      Maybe sign -> Result (Maybe sign)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe sign -> Result (Maybe sign))
-> Maybe sign -> Result (Maybe sign)
forall a b. (a -> b) -> a -> b
$ sign -> Maybe sign
forall a. a -> Maybe a
Just sign
v
  Maybe morphism
lpf <- if IRI
p IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
nullIRI
            then Maybe morphism -> Result (Maybe morphism)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe morphism
forall a. Maybe a
Nothing
            else do morphism
v <- lid -> IRI -> DGraph -> Result morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> IRI -> DGraph -> Result morphism
lookupMorph lid
ml IRI
p DGraph
dg
                    Maybe morphism -> Result (Maybe morphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe morphism -> Result (Maybe morphism))
-> Maybe morphism -> Result (Maybe morphism)
forall a b. (a -> b) -> a -> b
$ morphism -> Maybe morphism
forall a. a -> Maybe a
Just morphism
v
{- if (dom ltruth /= base_sig ml) then
error $ "The morphism " ++ (show s) ++
" must originate from the Base signature for " ++
(show ml) ++ "." else do -}
  if Maybe morphism -> Bool
forall a. Maybe a -> Bool
isJust Maybe morphism
lmod Bool -> Bool -> Bool
&& morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
dom (Maybe morphism -> morphism
forall a. HasCallStack => Maybe a -> a
fromJust Maybe morphism
lmod) sign -> sign -> Bool
forall a. Eq a => a -> a -> Bool
/= morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
ltruth then
     FilePath
-> Result (morphism, Maybe morphism, Maybe sign, Maybe morphism)
forall a. HasCallStack => FilePath -> a
error (FilePath
 -> Result (morphism, Maybe morphism, Maybe sign, Maybe morphism))
-> FilePath
-> Result (morphism, Maybe morphism, Maybe sign, Maybe morphism)
forall a b. (a -> b) -> a -> b
$ "The morphisms " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
s FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
             " and " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
m FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " must be composable."
    else if Maybe morphism -> Bool
forall a. Maybe a -> Bool
isJust Maybe morphism
lpf Bool -> Bool -> Bool
&& morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
dom (Maybe morphism -> morphism
forall a. HasCallStack => Maybe a -> a
fromJust Maybe morphism
lpf) sign -> sign -> Bool
forall a. Eq a => a -> a -> Bool
/= morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
ltruth then
     FilePath
-> Result (morphism, Maybe morphism, Maybe sign, Maybe morphism)
forall a. HasCallStack => FilePath -> a
error (FilePath
 -> Result (morphism, Maybe morphism, Maybe sign, Maybe morphism))
-> FilePath
-> Result (morphism, Maybe morphism, Maybe sign, Maybe morphism)
forall a b. (a -> b) -> a -> b
$ "The morphisms " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
s FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
             " and " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
p FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " must be composable."
    else (morphism, Maybe morphism, Maybe sign, Maybe morphism)
-> Result (morphism, Maybe morphism, Maybe sign, Maybe morphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (morphism
ltruth, Maybe morphism
lmod, Maybe sign
found, Maybe morphism
lpf)

-- creates a node for the logic definition
addLogicDef2DG :: LogicDef -> DGraph -> DGraph
addLogicDef2DG :: LogicDef -> DGraph -> DGraph
addLogicDef2DG ld :: LogicDef
ld dg :: DGraph
dg =
  let node :: Node
node = DGraph -> Node
getNewNodeDG DGraph
dg
      name :: IRI
name = LogicDef -> IRI
newlogicName LogicDef
ld
      nodeName :: NodeName
nodeName = NodeName
emptyNodeName { getName :: IRI
getName = IRI
name }
      info :: DGNodeInfo
info = DGOrigin -> DGNodeInfo
newNodeInfo DGOrigin
DGBasic
      extSign :: ExtSign LogicDef ()
extSign = Framework -> LogicDef -> ExtSign LogicDef ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign Framework
Framework LogicDef
ld
      gth :: G_theory
gth = Framework -> ExtSign LogicDef () -> SigId -> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory Framework
Framework ExtSign LogicDef ()
extSign SigId
startSigId
      nodeLabel :: DGNodeLab
nodeLabel = NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab NodeName
nodeName DGNodeInfo
info G_theory
gth
      dg1 :: DGraph
dg1 = LNode DGNodeLab -> DGraph -> DGraph
insNodeDG (Node
node, DGNodeLab
nodeLabel) DGraph
dg

      emptyNode :: MaybeNode
emptyNode = AnyLogic -> MaybeNode
EmptyNode (AnyLogic -> MaybeNode) -> AnyLogic -> MaybeNode
forall a b. (a -> b) -> a -> b
$ Framework -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic Framework
Framework
      genSig :: GenSig
genSig = MaybeNode -> [NodeSig] -> MaybeNode -> GenSig
GenSig MaybeNode
emptyNode [] MaybeNode
emptyNode
      nodeSig :: NodeSig
nodeSig = Node -> G_sign -> NodeSig
NodeSig Node
node (G_sign -> NodeSig) -> G_sign -> NodeSig
forall a b. (a -> b) -> a -> b
$ Framework -> ExtSign LogicDef () -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign Framework
Framework ExtSign LogicDef ()
extSign SigId
startSigId
      gEntry :: GlobalEntry
gEntry = ExtGenSig -> GlobalEntry
SpecEntry (ExtGenSig -> GlobalEntry) -> ExtGenSig -> GlobalEntry
forall a b. (a -> b) -> a -> b
$ GenSig -> NodeSig -> ExtGenSig
ExtGenSig GenSig
genSig NodeSig
nodeSig
      dg2 :: DGraph
dg2 = DGraph
dg1 { globalEnv :: GlobalEnv
globalEnv = IRI -> GlobalEntry -> GlobalEnv -> GlobalEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
name GlobalEntry
gEntry (GlobalEnv -> GlobalEnv) -> GlobalEnv -> GlobalEnv
forall a b. (a -> b) -> a -> b
$ DGraph -> GlobalEnv
globalEnv DGraph
dg1 }
   in DGraph
dg2

-- constructs the logic instance for the object logic
buildLogic :: LogicalFramework lid sublogics basic_spec sentence symb_items
                    symb_map_items sign morphism symbol raw_symbol proof_tree
              => lid -> String -> morphism -> Maybe morphism ->
                 Maybe sign -> Maybe morphism -> IO ()
buildLogic :: lid
-> FilePath
-> morphism
-> Maybe morphism
-> Maybe sign
-> Maybe morphism
-> IO ()
buildLogic ml :: lid
ml l :: FilePath
l ltruth :: morphism
ltruth maybeMod :: Maybe morphism
maybeMod _ maybePf :: Maybe morphism
maybePf = do
  Bool
exists <- FilePath -> IO Bool
doesDirectoryExist FilePath
l
  if Bool
exists then
     FilePath -> IO ()
forall a. HasCallStack => FilePath -> a
error (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "The directory " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " already exists.\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
             "Please choose a different object logic name." else do
      FilePath -> IO ()
createDirectory FilePath
l
      let logicCl :: FilePath
logicCl = lid -> FilePath -> FilePath
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> FilePath -> FilePath
write_logic lid
ml FilePath
l
      FilePath -> FilePath -> IO ()
writeFile (FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "/" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "Logic_" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ".hs") FilePath
logicCl
      let syntaxCl :: FilePath
syntaxCl = lid -> FilePath -> morphism -> FilePath
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> FilePath -> morphism -> FilePath
write_syntax lid
ml FilePath
l morphism
ltruth
      FilePath -> FilePath -> IO ()
writeFile (FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "/" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "Syntax.hs") FilePath
syntaxCl
      if Maybe morphism -> Bool
forall a. Maybe a -> Bool
isNothing Maybe morphism
maybeMod then
        FilePath -> IO ()
forall a. HasCallStack => FilePath -> a
error (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Please provide a model theory for " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" else do
          let modCl :: FilePath
modCl = lid -> FilePath -> morphism -> FilePath
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> FilePath -> morphism -> FilePath
write_model lid
ml FilePath
l (morphism -> FilePath) -> morphism -> FilePath
forall a b. (a -> b) -> a -> b
$ Maybe morphism -> morphism
forall a. HasCallStack => Maybe a -> a
fromJust Maybe morphism
maybeMod
          FilePath -> FilePath -> IO ()
writeFile (FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "/" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "Model.hs") FilePath
modCl
          if Maybe morphism -> Bool
forall a. Maybe a -> Bool
isNothing Maybe morphism
maybePf then
            FilePath -> IO ()
forall a. HasCallStack => FilePath -> a
error (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Please provide a proof theory for " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" else do
                let proofCl :: FilePath
proofCl = lid -> FilePath -> morphism -> FilePath
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> FilePath -> morphism -> FilePath
write_proof lid
ml FilePath
l (morphism -> FilePath) -> morphism -> FilePath
forall a b. (a -> b) -> a -> b
$ Maybe morphism -> morphism
forall a. HasCallStack => Maybe a -> a
fromJust Maybe morphism
maybePf
                FilePath -> FilePath -> IO ()
writeFile (FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "/" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "Proof.hs") FilePath
proofCl
                () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- includes the newly-defined logic in the logic list
addLogic2LogicList :: String -> IO ()
addLogic2LogicList :: FilePath -> IO ()
addLogic2LogicList l :: FilePath
l = do
  let file :: FilePath
file = FilePath
dynLogicsDir FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "/" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
dynLogicsFile
  FilePath
contentsOld <- FilePath -> IO FilePath
readFile FilePath
file
  let res :: Either ParseError FilePath
res = GenParser Char (AnnoState ()) FilePath
-> AnnoState ()
-> FilePath
-> FilePath
-> Either ParseError FilePath
forall tok st a.
GenParser tok st a
-> st -> FilePath -> [tok] -> Either ParseError a
runParser (FilePath -> GenParser Char (AnnoState ()) FilePath
forall st. FilePath -> AParser st FilePath
parser FilePath
l) (() -> AnnoState ()
forall st. st -> AnnoState st
emptyAnnos ()) "" FilePath
contentsOld
  case Either ParseError FilePath
res of
    Right contentsNew :: FilePath
contentsNew -> if FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf ("import " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ".Logic_" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
l) FilePath
contentsOld
      then
      FilePath -> IO ()
forall a. HasCallStack => FilePath -> a
error (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
forall a. Show a => a -> FilePath
show (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " already in DynLogicList"
      else
      FilePath -> FilePath -> IO ()
writeFile FilePath
file FilePath
contentsNew
    Left er :: ParseError
er -> FilePath -> IO ()
forall a. HasCallStack => FilePath -> a
error (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ ParseError -> FilePath
forall a. Show a => a -> FilePath
show ParseError
er
{- ----------------------------------------------------------------------------
Comorphism analysis -}

anaComorphismDef :: ComorphismDef -> DGraph -> IO DGraph
anaComorphismDef :: ComorphismDef -> DGraph -> IO DGraph
anaComorphismDef cd :: ComorphismDef
cd dg :: DGraph
dg =
  case ComorphismDef -> FRAM
metaC ComorphismDef
cd of
    LF -> LF -> ComorphismDef -> DGraph -> IO DGraph
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ComorphismDef -> DGraph -> IO DGraph
anaComorphismDefH LF
Logic_LF.LF ComorphismDef
cd DGraph
dg
    Isabelle -> Isabelle -> ComorphismDef -> DGraph -> IO DGraph
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ComorphismDef -> DGraph -> IO DGraph
anaComorphismDefH Isabelle
Logic_Isabelle.Isabelle ComorphismDef
cd DGraph
dg
    Maude -> Maude -> ComorphismDef -> DGraph -> IO DGraph
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ComorphismDef -> DGraph -> IO DGraph
anaComorphismDefH Maude
Logic_Maude.Maude ComorphismDef
cd DGraph
dg

anaComorphismDefH :: LogicalFramework lid sublogics basic_spec sentence symb_items
                            symb_map_items sign morphism symbol raw_symbol
                            proof_tree
                     => lid -> ComorphismDef -> DGraph -> IO DGraph
anaComorphismDefH :: lid -> ComorphismDef -> DGraph -> IO DGraph
anaComorphismDefH ml :: lid
ml (ComorphismDef nc :: IRI
nc m :: FRAM
m sL :: IRI
sL tL :: IRI
tL sM :: IRI
sM pM :: IRI
pM mM :: IRI
mM) dg :: DGraph
dg =
   let c :: FilePath
c = IRI -> FilePath
iriToStringUnsecure IRI
nc
       s :: FilePath
s = IRI -> FilePath
iriToStringUnsecure IRI
sL
       t :: FilePath
t = IRI -> FilePath
iriToStringUnsecure IRI
tL
   in case lid
-> ComorphismDef -> DGraph -> Result (morphism, morphism, morphism)
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> ComorphismDef -> DGraph -> Result (morphism, morphism, morphism)
anaComH lid
ml (IRI -> FRAM -> IRI -> IRI -> IRI -> IRI -> IRI -> ComorphismDef
ComorphismDef IRI
nc FRAM
m IRI
sL IRI
tL IRI
sM IRI
pM IRI
mM) DGraph
dg of
        Result _ (Just (symM :: morphism
symM, pfM :: morphism
pfM, modM :: morphism
modM)) -> do
             lid
-> FilePath
-> FilePath
-> FilePath
-> morphism
-> morphism
-> morphism
-> IO ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> FilePath
-> FilePath
-> FilePath
-> morphism
-> morphism
-> morphism
-> IO ()
buildComorphism lid
ml FilePath
c FilePath
s FilePath
t morphism
symM morphism
pfM morphism
modM
             FilePath -> IO ()
addComorphism2ComorphismList FilePath
c
             DGraph -> IO DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph -> IO DGraph) -> DGraph -> IO DGraph
forall a b. (a -> b) -> a -> b
$ ComorphismDef -> DGraph -> DGraph
addComorphismDef2DG (IRI -> FRAM -> IRI -> IRI -> IRI -> IRI -> IRI -> ComorphismDef
ComorphismDef IRI
nc FRAM
m IRI
sL IRI
tL IRI
sM IRI
pM IRI
mM) DGraph
dg
        _ -> FilePath -> IO DGraph
forall a. HasCallStack => FilePath -> a
error ""

anaComH :: LogicalFramework lid sublogics basic_spec sentence symb_items
                            symb_map_items sign morphism symbol raw_symbol
                            proof_tree
                     => lid -> ComorphismDef -> DGraph -> Result (morphism,
                            morphism, morphism)
anaComH :: lid
-> ComorphismDef -> DGraph -> Result (morphism, morphism, morphism)
anaComH ml :: lid
ml (ComorphismDef _ _ sL :: IRI
sL tL :: IRI
tL sM :: IRI
sM pM :: IRI
pM mM :: IRI
mM) dg :: DGraph
dg =
     let sLName :: FilePath
sLName = IRI -> FilePath
iriToStringUnsecure IRI
sL
         tLName :: FilePath
tLName = IRI -> FilePath
iriToStringUnsecure IRI
tL
         sLSyn :: morphism
sLSyn = lid -> FilePath -> FilePath -> morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> FilePath -> FilePath -> morphism
getMorphL lid
ml FilePath
sLName "Syntax"
         sLPf :: morphism
sLPf = lid -> FilePath -> FilePath -> morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> FilePath -> FilePath -> morphism
getMorphL lid
ml FilePath
sLName "Proof"
         sLMod :: morphism
sLMod = lid -> FilePath -> FilePath -> morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> FilePath -> FilePath -> morphism
getMorphL lid
ml FilePath
sLName "Model"
         tLSyn :: morphism
tLSyn = lid -> FilePath -> FilePath -> morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> FilePath -> FilePath -> morphism
getMorphL lid
ml FilePath
tLName "Syntax"
         tLPf :: morphism
tLPf = lid -> FilePath -> FilePath -> morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> FilePath -> FilePath -> morphism
getMorphL lid
ml FilePath
tLName "Proof"
         tLMod :: morphism
tLMod = lid -> FilePath -> FilePath -> morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> FilePath -> FilePath -> morphism
getMorphL lid
ml FilePath
tLName "Model" in do
     morphism
synM <- lid -> IRI -> DGraph -> Result morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> IRI -> DGraph -> Result morphism
lookupMorph lid
ml IRI
sM DGraph
dg
     morphism
pfM <- lid -> IRI -> DGraph -> Result morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> IRI -> DGraph -> Result morphism
lookupMorph lid
ml IRI
pM DGraph
dg
     morphism
modM <- lid -> IRI -> DGraph -> Result morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> IRI -> DGraph -> Result morphism
lookupMorph lid
ml IRI
mM DGraph
dg
     if morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
sLSyn sign -> sign -> Bool
forall a. Eq a => a -> a -> Bool
/= morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
dom morphism
synM then FilePath -> Result (morphism, morphism, morphism)
forall a. HasCallStack => FilePath -> a
error (FilePath -> Result (morphism, morphism, morphism))
-> FilePath -> Result (morphism, morphism, morphism)
forall a b. (a -> b) -> a -> b
$
      "the domain of the syntax morphism has" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
      " to be the syntax of the source logic.\n"
      else if morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
tLSyn sign -> sign -> Bool
forall a. Eq a => a -> a -> Bool
/= morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
synM then FilePath -> Result (morphism, morphism, morphism)
forall a. HasCallStack => FilePath -> a
error (FilePath -> Result (morphism, morphism, morphism))
-> FilePath -> Result (morphism, morphism, morphism)
forall a b. (a -> b) -> a -> b
$
        "the codomain of the syntax morphism has" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
        " to be the syntax of the target logic.\n"
            else if morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
sLPf sign -> sign -> Bool
forall a. Eq a => a -> a -> Bool
/= morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
dom morphism
pfM then FilePath -> Result (morphism, morphism, morphism)
forall a. HasCallStack => FilePath -> a
error (FilePath -> Result (morphism, morphism, morphism))
-> FilePath -> Result (morphism, morphism, morphism)
forall a b. (a -> b) -> a -> b
$
              "the domain of the proof morphism has to be the" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
              " proof theory of the source logic.\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ sign -> FilePath
forall a. Show a => a -> FilePath
show (morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
sLPf) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
              "\n\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ sign -> FilePath
forall a. Show a => a -> FilePath
show (morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
dom morphism
pfM) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n"
                  else if morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
tLPf sign -> sign -> Bool
forall a. Eq a => a -> a -> Bool
/= morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
pfM then FilePath -> Result (morphism, morphism, morphism)
forall a. HasCallStack => FilePath -> a
error (FilePath -> Result (morphism, morphism, morphism))
-> FilePath -> Result (morphism, morphism, morphism)
forall a b. (a -> b) -> a -> b
$
                    "the codomain of the proof morphism has" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                    " to be the proof theory of the target logic.\n"
                            else if morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
sLMod sign -> sign -> Bool
forall a. Eq a => a -> a -> Bool
/= morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
dom morphism
modM
                            then FilePath -> Result (morphism, morphism, morphism)
forall a. HasCallStack => FilePath -> a
error (FilePath -> Result (morphism, morphism, morphism))
-> FilePath -> Result (morphism, morphism, morphism)
forall a b. (a -> b) -> a -> b
$ "the domain of the model morphism" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                            " has to be the model theory of the source logic.\n"
                            FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ sign -> FilePath
forall a. Show a => a -> FilePath
show (morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
sLMod) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ sign -> FilePath
forall a. Show a => a -> FilePath
show (morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
dom morphism
modM)
                            FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n"
                              else if morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
tLMod sign -> sign -> Bool
forall a. Eq a => a -> a -> Bool
/= morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism
modM then FilePath -> Result (morphism, morphism, morphism)
forall a. HasCallStack => FilePath -> a
error (FilePath -> Result (morphism, morphism, morphism))
-> FilePath -> Result (morphism, morphism, morphism)
forall a b. (a -> b) -> a -> b
$
                                "the codomain of the model morphism has" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                                " to be the model theory of the target logic.\n"
                                   else case (morphism -> morphism -> Result morphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
composeMorphisms morphism
synM morphism
tLPf,
                                              morphism -> morphism -> Result morphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
composeMorphisms morphism
sLPf morphism
pfM) of
                                      (Result _ comM1 :: Maybe morphism
comM1, Result _ comM2 :: Maybe morphism
comM2) ->
                                       if Maybe morphism
comM1 Maybe morphism -> Maybe morphism -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe morphism
comM2 then FilePath -> Result (morphism, morphism, morphism)
forall a. HasCallStack => FilePath -> a
error (FilePath -> Result (morphism, morphism, morphism))
-> FilePath -> Result (morphism, morphism, morphism)
forall a b. (a -> b) -> a -> b
$
                                           "the syntax - proof diagram does" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                                           " not commute.\n"
                                       else case (morphism -> morphism -> Result morphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
composeMorphisms morphism
synM morphism
tLMod,
                                                  morphism -> morphism -> Result morphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
composeMorphisms morphism
sLPf morphism
modM) of
                                             (Result _ comM3 :: Maybe morphism
comM3, Result _ comM4 :: Maybe morphism
comM4) ->
                                              if Maybe morphism
comM3 Maybe morphism -> Maybe morphism -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe morphism
comM4 then FilePath -> Result (morphism, morphism, morphism)
forall a. HasCallStack => FilePath -> a
error (FilePath -> Result (morphism, morphism, morphism))
-> FilePath -> Result (morphism, morphism, morphism)
forall a b. (a -> b) -> a -> b
$
                                                "the syntax - model diagram" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                                                " does not commute.\n"
                                              else (morphism, morphism, morphism)
-> Result (morphism, morphism, morphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (morphism
synM, morphism
pfM, morphism
modM)

getMorphL :: LogicalFramework lid sublogics basic_spec sentence symb_items
                            symb_map_items sign morphism symbol raw_symbol
                            proof_tree
                     => lid -> String -> String -> morphism
getMorphL :: lid -> FilePath -> FilePath -> morphism
getMorphL ml :: lid
ml logicName :: FilePath
logicName fileName :: FilePath
fileName =
     let file :: FilePath
file = FilePath
logicName FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "/" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
fileName FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ".hs"
     in lid -> FilePath -> morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> FilePath -> morphism
read_morphism lid
ml FilePath
file

addComorphismDef2DG :: ComorphismDef -> DGraph -> DGraph
addComorphismDef2DG :: ComorphismDef -> DGraph -> DGraph
addComorphismDef2DG cd :: ComorphismDef
cd dg :: DGraph
dg =
  let node :: Node
node = DGraph -> Node
getNewNodeDG DGraph
dg
      name :: IRI
name = ComorphismDef -> IRI
newcomorphismName ComorphismDef
cd
      nodeName :: NodeName
nodeName = NodeName
emptyNodeName { getName :: IRI
getName = IRI
name }
      info :: DGNodeInfo
info = DGOrigin -> DGNodeInfo
newNodeInfo DGOrigin
DGBasic
      extSign :: ExtSign ComorphismDef ()
extSign = FrameworkCom -> ComorphismDef -> ExtSign ComorphismDef ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign FrameworkCom
FrameworkCom ComorphismDef
cd
      gth :: G_theory
gth = FrameworkCom -> ExtSign ComorphismDef () -> SigId -> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory FrameworkCom
FrameworkCom ExtSign ComorphismDef ()
extSign SigId
startSigId
      nodeLabel :: DGNodeLab
nodeLabel = NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab NodeName
nodeName DGNodeInfo
info G_theory
gth
      dg1 :: DGraph
dg1 = LNode DGNodeLab -> DGraph -> DGraph
insNodeDG (Node
node, DGNodeLab
nodeLabel) DGraph
dg

      emptyNode :: MaybeNode
emptyNode = AnyLogic -> MaybeNode
EmptyNode (AnyLogic -> MaybeNode) -> AnyLogic -> MaybeNode
forall a b. (a -> b) -> a -> b
$ FrameworkCom -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic FrameworkCom
FrameworkCom
      genSig :: GenSig
genSig = MaybeNode -> [NodeSig] -> MaybeNode -> GenSig
GenSig MaybeNode
emptyNode [] MaybeNode
emptyNode
      nodeSig :: NodeSig
nodeSig = Node -> G_sign -> NodeSig
NodeSig Node
node (G_sign -> NodeSig) -> G_sign -> NodeSig
forall a b. (a -> b) -> a -> b
$ FrameworkCom -> ExtSign ComorphismDef () -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign FrameworkCom
FrameworkCom ExtSign ComorphismDef ()
extSign SigId
startSigId
      gEntry :: GlobalEntry
gEntry = ExtGenSig -> GlobalEntry
SpecEntry (ExtGenSig -> GlobalEntry) -> ExtGenSig -> GlobalEntry
forall a b. (a -> b) -> a -> b
$ GenSig -> NodeSig -> ExtGenSig
ExtGenSig GenSig
genSig NodeSig
nodeSig
      dg2 :: DGraph
dg2 = DGraph
dg1 { globalEnv :: GlobalEnv
globalEnv = IRI -> GlobalEntry -> GlobalEnv -> GlobalEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
name GlobalEntry
gEntry (GlobalEnv -> GlobalEnv) -> GlobalEnv -> GlobalEnv
forall a b. (a -> b) -> a -> b
$ DGraph -> GlobalEnv
globalEnv DGraph
dg1 }
  in DGraph
dg2


buildComorphism :: LogicalFramework lid sublogics basic_spec sentence symb_items
                    symb_map_items sign morphism symbol raw_symbol proof_tree
              => lid -> String -> String -> String
                   -> morphism -> morphism -> morphism -> IO ()
buildComorphism :: lid
-> FilePath
-> FilePath
-> FilePath
-> morphism
-> morphism
-> morphism
-> IO ()
buildComorphism ml :: lid
ml c :: FilePath
c s :: FilePath
s t :: FilePath
t synM :: morphism
synM pfM :: morphism
pfM modM :: morphism
modM = do
  Bool
exists <- FilePath -> IO Bool
doesFileExist ("Comorphisms" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "/" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
c FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ".hs")
  if Bool
exists
     then FilePath -> IO ()
forall a. HasCallStack => FilePath -> a
error (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "The comorphism " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
c FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "already exists.\n"
     else do
        let comorphismC :: FilePath
comorphismC = lid
-> FilePath
-> FilePath
-> FilePath
-> morphism
-> morphism
-> morphism
-> FilePath
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
LogicalFramework
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> FilePath
-> FilePath
-> FilePath
-> morphism
-> morphism
-> morphism
-> FilePath
write_comorphism lid
ml FilePath
c FilePath
s FilePath
t morphism
synM morphism
pfM morphism
modM
        FilePath -> FilePath -> IO ()
writeFile ("Comorphisms" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "/" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
c FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ".hs") FilePath
comorphismC
        () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

addComorphism2ComorphismList :: String -> IO ()
addComorphism2ComorphismList :: FilePath -> IO ()
addComorphism2ComorphismList c :: FilePath
c = do
  let file :: FilePath
file = FilePath
dynComorphismsDir FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "/" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
dynComorphismsFile
  FilePath
contentsOld <- FilePath -> IO FilePath
readFile FilePath
file
  let res :: Either ParseError FilePath
res = GenParser Char (AnnoState ()) FilePath
-> AnnoState ()
-> FilePath
-> FilePath
-> Either ParseError FilePath
forall tok st a.
GenParser tok st a
-> st -> FilePath -> [tok] -> Either ParseError a
runParser (FilePath -> GenParser Char (AnnoState ()) FilePath
forall st. FilePath -> AParser st FilePath
parserc FilePath
c) (() -> AnnoState ()
forall st. st -> AnnoState st
emptyAnnos ()) "" FilePath
contentsOld  -- !!
  case Either ParseError FilePath
res of
      Right contentsNew :: FilePath
contentsNew -> FilePath -> FilePath -> IO ()
writeFile FilePath
file FilePath
contentsNew
      Left er :: ParseError
er -> FilePath -> IO ()
forall a. HasCallStack => FilePath -> a
error (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ ParseError -> FilePath
forall a. Show a => a -> FilePath
show ParseError
er


{- ----------------------------------------------------------------------------
Auxiliary functions -}

-- looks up a signature by name
lookupSig :: Logic lid sublogics basic_spec sentence symb_items symb_map_items
                   sign morphism symbol raw_symbol proof_tree
             => lid -> SIG_NAME -> DGraph -> Result sign
lookupSig :: lid -> IRI -> DGraph -> Result sign
lookupSig l :: lid
l n :: IRI
n dg :: DGraph
dg = do
  let extSig :: ExtGenSig
extSig = case IRI -> DGraph -> Maybe GlobalEntry
lookupGlobalEnvDG IRI
n DGraph
dg of
                 Just (SpecEntry es :: ExtGenSig
es) -> ExtGenSig
es
                 _ -> FilePath -> ExtGenSig
forall a. HasCallStack => FilePath -> a
error (FilePath -> ExtGenSig) -> FilePath -> ExtGenSig
forall a b. (a -> b) -> a -> b
$ "The signature " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                              " could not be found."
  case ExtGenSig
extSig of
    ExtGenSig _ (NodeSig _ (G_sign l' :: lid
l' (ExtSign sig :: sign
sig _) _)) ->
      if lid -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic lid
l AnyLogic -> AnyLogic -> Bool
forall a. Eq a => a -> a -> Bool
/= lid -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic lid
l'
         then FilePath -> Result sign
forall a. HasCallStack => FilePath -> a
error (FilePath -> Result sign) -> FilePath -> Result sign
forall a b. (a -> b) -> a -> b
$ "The signature " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                      " is not in the logic " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ lid -> FilePath
forall a. Show a => a -> FilePath
show lid
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "."
         else lid -> lid -> FilePath -> sign -> Result sign
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> FilePath -> sign1 -> m sign2
coercePlainSign lid
l' lid
l "" sign
sig

-- looks up a morphism by name
lookupMorph :: Logic lid sublogics basic_spec sentence symb_items symb_map_items
                     sign morphism symbol raw_symbol proof_tree
               => lid -> MORPH_NAME -> DGraph -> Result morphism
lookupMorph :: lid -> IRI -> DGraph -> Result morphism
lookupMorph l :: lid
l n :: IRI
n dg :: DGraph
dg = do
  let extView :: ExtViewSig
extView = case IRI -> DGraph -> Maybe GlobalEntry
lookupGlobalEnvDG IRI
n DGraph
dg of
                  Just (ViewOrStructEntry _ ev :: ExtViewSig
ev) -> ExtViewSig
ev
                  _ -> FilePath -> ExtViewSig
forall a. HasCallStack => FilePath -> a
error (FilePath -> ExtViewSig) -> FilePath -> ExtViewSig
forall a b. (a -> b) -> a -> b
$ "The morphism " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                               " could not be found."
  case ExtViewSig
extView of
    ExtViewSig _ (GMorphism c :: cid
c _ _ morph :: morphism2
morph _) _ -> do
      let l' :: lid2
l' = cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
c
      if lid -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic lid
l AnyLogic -> AnyLogic -> Bool
forall a. Eq a => a -> a -> Bool
/= lid2 -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic lid2
l'
         then FilePath -> Result morphism
forall a. HasCallStack => FilePath -> a
error (FilePath -> Result morphism) -> FilePath -> Result morphism
forall a b. (a -> b) -> a -> b
$ "The morphism " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                      " is not in the logic " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ lid -> FilePath
forall a. Show a => a -> FilePath
show lid
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "."
         else lid2 -> lid -> FilePath -> morphism2 -> Result morphism
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> FilePath -> morphism1 -> m morphism2
coerceMorphism lid2
l' lid
l "" morphism2
morph


parser :: String -> AParser st String
parser :: FilePath -> AParser st FilePath
parser l :: FilePath
l = do
  let l_imp :: FilePath
l_imp = "import " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "." FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "Logic_" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
l
  let l_log :: FilePath
l_log = "Logic " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
l

  FilePath
header <- FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
skipUntil "module"
  FilePath
mod_decl <- do FilePath
m <- FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
asStr "module"
                 FilePath
n <- AParser st FilePath
forall st. AParser st FilePath
moduleName
                 FilePath
w <- FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
asStr "where"
                 FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> AParser st FilePath)
-> FilePath -> AParser st FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
m, FilePath
n, FilePath
w]
  [FilePath]
imps <- AParser st FilePath
-> ParsecT FilePath (AnnoState st) Identity [FilePath]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (AParser st FilePath
 -> ParsecT FilePath (AnnoState st) Identity [FilePath])
-> AParser st FilePath
-> ParsecT FilePath (AnnoState st) Identity [FilePath]
forall a b. (a -> b) -> a -> b
$ do
             FilePath
i <- FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
asStr "import"
             FilePath
n <- AParser st FilePath
forall st. AParser st FilePath
moduleName
             FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> AParser st FilePath)
-> FilePath -> AParser st FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
i, FilePath
n]
  FilePath
log_var_decl <- do FilePath
v <- FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
asStr FilePath
dynLogicsCon
                     FilePath
s <- FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
asStr "::"
                     FilePath
t <- do CharParser (AnnoState st) Token
forall st. CharParser st Token
oBracketT
                             FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
asStr "AnyLogic"
                             CharParser (AnnoState st) Token
forall st. CharParser st Token
cBracketT
                             FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return "[AnyLogic]"
                     FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> AParser st FilePath)
-> FilePath -> AParser st FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
v, FilePath
s, FilePath
t]
  FilePath
log_var_def <- do FilePath
v <- FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
asStr FilePath
dynLogicsCon
                    FilePath
s <- FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
asStr "="
                    FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> AParser st FilePath)
-> FilePath -> AParser st FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
v, FilePath
s]
  [FilePath]
log_list <- do CharParser (AnnoState st) Token
forall st. CharParser st Token
oBracketT
                 (do CharParser (AnnoState st) Token
forall st. CharParser st Token
cBracketT
                     [FilePath] -> ParsecT FilePath (AnnoState st) Identity [FilePath]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
                   ParsecT FilePath (AnnoState st) Identity [FilePath]
-> ParsecT FilePath (AnnoState st) Identity [FilePath]
-> ParsecT FilePath (AnnoState st) Identity [FilePath]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
                   do (xs :: [FilePath]
xs, _) <- AParser st FilePath
forall st. AParser st FilePath
logParser AParser st FilePath
-> CharParser (AnnoState st) Token
-> GenParser Char (AnnoState st) ([FilePath], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` CharParser (AnnoState st) Token
forall st. CharParser st Token
commaT
                      CharParser (AnnoState st) Token
forall st. CharParser st Token
cBracketT
                      [FilePath] -> ParsecT FilePath (AnnoState st) Identity [FilePath]
forall (m :: * -> *) a. Monad m => a -> m a
return [FilePath]
xs

  FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> AParser st FilePath)
-> FilePath -> AParser st FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
header FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
mod_decl FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
           FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate "\n" ([FilePath]
imps [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath
l_imp]) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
           FilePath
log_var_decl FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
log_var_def FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "[" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
           FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate ", " ([FilePath]
log_list [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath
l_log]) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "]"

parserc :: String -> AParser st String
parserc :: FilePath -> AParser st FilePath
parserc c :: FilePath
c = do
     let com_imp :: FilePath
com_imp = "import " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "Comorphisms." FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
c
     let com_c :: FilePath
com_c = "Comorphism " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
c

     FilePath
header <- FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
skipUntil "module"
     FilePath
mod_decl <- do FilePath
m <- FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
asStr "module"
                    FilePath
n <- AParser st FilePath
forall st. AParser st FilePath
moduleName
                    FilePath
w <- FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
asStr "where"
                    FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> AParser st FilePath)
-> FilePath -> AParser st FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
m, FilePath
n, FilePath
w]
     [FilePath]
imps <- AParser st FilePath
-> ParsecT FilePath (AnnoState st) Identity [FilePath]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (AParser st FilePath
 -> ParsecT FilePath (AnnoState st) Identity [FilePath])
-> AParser st FilePath
-> ParsecT FilePath (AnnoState st) Identity [FilePath]
forall a b. (a -> b) -> a -> b
$ do
                FilePath
i <- FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
asStr "import"
                FilePath
n <- AParser st FilePath
forall st. AParser st FilePath
moduleName
                FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> AParser st FilePath)
-> FilePath -> AParser st FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
i, FilePath
n]
     FilePath
com_var_decl <- do FilePath
v <- FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
asStr FilePath
dynComorphismsCon
                        FilePath
s <- FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
asStr "::"
                        FilePath
t <- do CharParser (AnnoState st) Token
forall st. CharParser st Token
oBracketT
                                FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
asStr "AnyComorphism"
                                CharParser (AnnoState st) Token
forall st. CharParser st Token
cBracketT
                                FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return "[AnyComorphism]"
                        FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> AParser st FilePath)
-> FilePath -> AParser st FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
v, FilePath
s, FilePath
t]
     FilePath
com_var_def <- do FilePath
v <- FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
asStr FilePath
dynComorphismsCon
                       FilePath
s <- FilePath -> AParser st FilePath
forall st. FilePath -> AParser st FilePath
asStr "="
                       FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> AParser st FilePath)
-> FilePath -> AParser st FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
v, FilePath
s]
     [FilePath]
com_list <- do CharParser (AnnoState st) Token
forall st. CharParser st Token
oBracketT
                    (do CharParser (AnnoState st) Token
forall st. CharParser st Token
cBracketT
                        [FilePath] -> ParsecT FilePath (AnnoState st) Identity [FilePath]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
                        ParsecT FilePath (AnnoState st) Identity [FilePath]
-> ParsecT FilePath (AnnoState st) Identity [FilePath]
-> ParsecT FilePath (AnnoState st) Identity [FilePath]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
                        do (xs :: [FilePath]
xs, _) <- AParser st FilePath
forall st. AParser st FilePath
comParser AParser st FilePath
-> CharParser (AnnoState st) Token
-> GenParser Char (AnnoState st) ([FilePath], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
`separatedBy` CharParser (AnnoState st) Token
forall st. CharParser st Token
commaT
                           CharParser (AnnoState st) Token
forall st. CharParser st Token
cBracketT
                           [FilePath] -> ParsecT FilePath (AnnoState st) Identity [FilePath]
forall (m :: * -> *) a. Monad m => a -> m a
return [FilePath]
xs
     FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> AParser st FilePath)
-> FilePath -> AParser st FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
header FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
mod_decl FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
              FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate "\n" ([FilePath]
imps [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath
com_imp]) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
              FilePath
com_var_decl FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
              FilePath
com_var_def FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "[" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
              FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate ", " ([FilePath]
com_list [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath
com_c]) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "]"

skipUntil :: String -> AParser st String
skipUntil :: FilePath -> AParser st FilePath
skipUntil lim :: FilePath
lim = do
  [FilePath]
res <- AParser st FilePath
-> ParsecT FilePath (AnnoState st) Identity [FilePath]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (AParser st FilePath
 -> ParsecT FilePath (AnnoState st) Identity [FilePath])
-> AParser st FilePath
-> ParsecT FilePath (AnnoState st) Identity [FilePath]
forall a b. (a -> b) -> a -> b
$ [FilePath] -> AParser st FilePath -> AParser st FilePath
forall st.
[FilePath] -> CharParser st FilePath -> CharParser st FilePath
reserved [FilePath
lim] (ParsecT FilePath (AnnoState st) Identity Char
-> AParser st FilePath
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (ParsecT FilePath (AnnoState st) Identity Char
 -> AParser st FilePath)
-> ParsecT FilePath (AnnoState st) Identity Char
-> AParser st FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> ParsecT FilePath (AnnoState st) Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
FilePath -> ParsecT s u m Char
noneOf FilePath
whiteChars) AParser st FilePath -> AParser st FilePath -> AParser st FilePath
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
                ParsecT FilePath (AnnoState st) Identity Char
-> AParser st FilePath
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (FilePath -> ParsecT FilePath (AnnoState st) Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
FilePath -> ParsecT s u m Char
oneOf FilePath
whiteChars)
  FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> AParser st FilePath)
-> FilePath -> AParser st FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [FilePath]
res

asStr :: String -> AParser st String
asStr :: FilePath -> AParser st FilePath
asStr x :: FilePath
x = do
  Token
res <- FilePath -> AParser st Token
forall st. FilePath -> AParser st Token
asKey FilePath
x
  FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> AParser st FilePath)
-> FilePath -> AParser st FilePath
forall a b. (a -> b) -> a -> b
$ Token -> FilePath
tokStr Token
res

moduleName :: AParser st String
moduleName :: AParser st FilePath
moduleName = do
  Token
m <- GenParser Char (AnnoState st) Token
forall st. CharParser st Token
simpleId
  GenParser Char (AnnoState st) Token
forall st. AParser st Token
dotT
  Token
n <- GenParser Char (AnnoState st) Token
forall st. CharParser st Token
simpleId
  FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> AParser st FilePath)
-> FilePath -> AParser st FilePath
forall a b. (a -> b) -> a -> b
$ Token -> FilePath
tokStr Token
m FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "." FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Token -> FilePath
tokStr Token
n

logParser :: AParser st String
logParser :: AParser st FilePath
logParser = do
  Token
l <- FilePath -> AParser st Token
forall st. FilePath -> AParser st Token
asKey "Logic"
  Token
n <- AParser st Token
forall st. CharParser st Token
simpleId
  FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> AParser st FilePath)
-> FilePath -> AParser st FilePath
forall a b. (a -> b) -> a -> b
$ Token -> FilePath
tokStr Token
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Token -> FilePath
tokStr Token
n

comParser :: AParser st String
comParser :: AParser st FilePath
comParser = do
     Token
c <- FilePath -> AParser st Token
forall st. FilePath -> AParser st Token
asKey "Comorphism"
     Token
n <- AParser st Token
forall st. CharParser st Token
simpleId
     FilePath -> AParser st FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> AParser st FilePath)
-> FilePath -> AParser st FilePath
forall a b. (a -> b) -> a -> b
$ Token -> FilePath
tokStr Token
c FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Token -> FilePath
tokStr Token
n