{- |
Module      :  ./LF/Twelf2DG.hs
Description :  Conversion of Twelf files to Development Graphs
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.Twelf2DG ( anaTwelfFile ) where

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

import Logic.Grothendieck
import Logic.ExtSign
import Logic.Logic

import LF.Twelf2GR
import LF.Sign
import LF.Morphism
import LF.Logic_LF

import Data.Graph.Inductive.Graph (Node)
import qualified Data.Map as Map

import Common.LibName
import Common.Id
import Common.IRI (simpleIdToIRI)
import Common.Keywords
import qualified Common.Consistency as Cons

import Driver.Options

type NODE_MAP = Map.Map NODE Node

-- analyzes the given Twelf file
anaTwelfFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaTwelfFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaTwelfFile _ fp :: FilePath
fp = do
  (libs :: LIBS
libs, bs :: [FilePath]
bs) <- Namespace
-> FilePath -> (LIBS, [FilePath]) -> IO (LIBS, [FilePath])
twelf2GR Namespace
LATIN FilePath
fp (LIBS
forall k a. Map k a
Map.empty, [])
  let libenv :: LibEnv
libenv = LIBS -> [FilePath] -> LibEnv
makeLibEnv LIBS
libs [FilePath]
bs
  FilePath
file <- FilePath -> IO FilePath
toAbsoluteURI FilePath
fp
  FilePath
lname <- Namespace -> FilePath -> IO FilePath
toLibName Namespace
LATIN FilePath
file
  Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv)))
-> Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ (LibName, LibEnv) -> Maybe (LibName, LibEnv)
forall a. a -> Maybe a
Just (FilePath -> LibName
emptyLibName FilePath
lname, LibEnv
libenv)

{- generates a library environment from libraries of signatures and morphisms
   the list of library names stores the order in which they were added -}
makeLibEnv :: LIBS -> [BASE] -> LibEnv
makeLibEnv :: LIBS -> [FilePath] -> LibEnv
makeLibEnv libs :: LIBS
libs bs :: [FilePath]
bs = (LibEnv, NODE_MAP) -> LibEnv
forall a b. (a, b) -> a
fst ((LibEnv, NODE_MAP) -> LibEnv) -> (LibEnv, NODE_MAP) -> LibEnv
forall a b. (a -> b) -> a -> b
$
  ((LibEnv, NODE_MAP) -> FilePath -> (LibEnv, NODE_MAP))
-> (LibEnv, NODE_MAP) -> [FilePath] -> (LibEnv, NODE_MAP)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ( \ (le :: LibEnv
le, nm :: NODE_MAP
nm) b :: FilePath
b ->
            let (sigs :: SIGS
sigs, morphs :: MORPHS
morphs) = (SIGS, MORPHS) -> FilePath -> LIBS -> (SIGS, MORPHS)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                    (FilePath -> (SIGS, MORPHS)
forall a. HasCallStack => FilePath -> a
error "Library cannot be found.") FilePath
b LIBS
libs
                ln :: LibName
ln = FilePath -> LibName
emptyLibName FilePath
b
                le1 :: LibEnv
le1 = LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
emptyDG LibEnv
le
                (le2 :: LibEnv
le2, nm1 :: NODE_MAP
nm1) = LibEnv -> NODE_MAP -> FilePath -> SIGS -> (LibEnv, NODE_MAP)
addNodes LibEnv
le1 NODE_MAP
nm FilePath
b SIGS
sigs
                le3 :: LibEnv
le3 = LibEnv -> NODE_MAP -> FilePath -> MORPHS -> LibEnv
addLinks LibEnv
le2 NODE_MAP
nm1 FilePath
b MORPHS
morphs
                dg :: DGraph
dg = LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories LibEnv
le3 LibName
ln (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le3
                le4 :: LibEnv
le4 = LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
dg LibEnv
le3
                in (LibEnv
le4, NODE_MAP
nm1)
        ) (LibEnv
emptyLibEnv, NODE_MAP
forall k a. Map k a
Map.empty) [FilePath]
bs

{- adds nodes to the library environment
   node map returned for reference when adding links -}
addNodes :: LibEnv -> NODE_MAP -> BASE -> SIGS -> (LibEnv, NODE_MAP)
addNodes :: LibEnv -> NODE_MAP -> FilePath -> SIGS -> (LibEnv, NODE_MAP)
addNodes le :: LibEnv
le nm :: NODE_MAP
nm b :: FilePath
b sigs :: SIGS
sigs =
  let ln :: LibName
ln = FilePath -> LibName
emptyLibName FilePath
b
      (dg2 :: DGraph
dg2, nm1 :: NODE_MAP
nm1) = (FilePath -> Sign -> (DGraph, NODE_MAP) -> (DGraph, NODE_MAP))
-> (DGraph, NODE_MAP) -> SIGS -> (DGraph, NODE_MAP)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey
         (\ m :: FilePath
m sig :: Sign
sig (dg :: DGraph
dg, nmap :: NODE_MAP
nmap) ->
            let (n :: Node
n, dg1 :: DGraph
dg1) = Sign -> DGraph -> (Node, DGraph)
addSigToDG Sign
sig DGraph
dg
                nmap1 :: NODE_MAP
nmap1 = (FilePath, FilePath) -> Node -> NODE_MAP -> NODE_MAP
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (FilePath
b, FilePath
m) Node
n NODE_MAP
nmap
                in (DGraph
dg1, NODE_MAP
nmap1)
         ) (LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le, NODE_MAP
nm) SIGS
sigs
      le1 :: LibEnv
le1 = LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
dg2 LibEnv
le
      in (LibEnv
le1, NODE_MAP
nm1)

-- inserts a signature as a node to the development graph
addSigToDG :: Sign -> DGraph -> (Node, DGraph)
addSigToDG :: Sign -> DGraph -> (Node, DGraph)
addSigToDG sig :: Sign
sig dg :: DGraph
dg =
  let node :: Node
node = DGraph -> Node
getNewNodeDG DGraph
dg
      name :: IRI
name = SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ FilePath -> Range -> SIMPLE_ID
Token (Sign -> FilePath
sigModule Sign
sig) Range
nullRange
      nodeName :: NodeName
nodeName = NodeName
emptyNodeName { getName :: IRI
getName = IRI
name }
      info :: DGNodeInfo
info = DGOrigin -> DGNodeInfo
newNodeInfo DGOrigin
DGBasic
      extSign :: ExtSign Sign Symbol
extSign = LF -> Sign -> ExtSign Sign Symbol
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 LF
LF Sign
sig
      gth :: G_theory
gth = LF -> ExtSign Sign Symbol -> 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 LF
LF ExtSign Sign Symbol
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
$ LF -> 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 LF
LF
      gSig :: GenSig
gSig = 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
$ LF -> ExtSign Sign Symbol -> 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 LF
LF ExtSign Sign Symbol
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
gSig 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 (Node
node, DGraph
dg2)

-- adds links to the library environment
addLinks :: LibEnv -> NODE_MAP -> BASE -> MORPHS -> LibEnv
addLinks :: LibEnv -> NODE_MAP -> FilePath -> MORPHS -> LibEnv
addLinks le :: LibEnv
le nm :: NODE_MAP
nm b :: FilePath
b morphs :: MORPHS
morphs =
  let ln :: LibName
ln = FilePath -> LibName
emptyLibName FilePath
b
      dg1 :: DGraph
dg1 = (Morphism -> DGraph -> DGraph) -> DGraph -> MORPHS -> DGraph
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (\ morph :: Morphism
morph dg :: DGraph
dg -> Morphism -> DGraph -> NODE_MAP -> LibEnv -> DGraph
addMorphToDG Morphism
morph DGraph
dg NODE_MAP
nm LibEnv
le)
              (LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le) MORPHS
morphs
      in LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
dg1 LibEnv
le

-- inserts a morphism as a link to the development graph
addMorphToDG :: Morphism -> DGraph -> NODE_MAP -> LibEnv -> DGraph
addMorphToDG :: Morphism -> DGraph -> NODE_MAP -> LibEnv -> DGraph
addMorphToDG morph :: Morphism
morph dg :: DGraph
dg nm :: NODE_MAP
nm le :: LibEnv
le =
  let b :: FilePath
b = Morphism -> FilePath
morphBase Morphism
morph
      m :: FilePath
m = Morphism -> FilePath
morphModule Morphism
morph
      n :: FilePath
n = Morphism -> FilePath
morphName Morphism
morph
      k :: MorphType
k = Morphism -> MorphType
morphType Morphism
morph
      gMorph :: GMorphism
gMorph = G_morphism -> GMorphism
gEmbed (G_morphism -> GMorphism) -> G_morphism -> GMorphism
forall a b. (a -> b) -> a -> b
$ LF -> Morphism -> MorId -> G_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 -> morphism -> MorId -> G_morphism
G_morphism LF
LF Morphism
morph MorId
startMorId
      thmStatus :: ThmLinkStatus
thmStatus = DGRule -> ProofBasis -> ThmLinkStatus
Proven (FilePath -> DGRule
DGRule "Type-checked") ProofBasis
emptyProofBasis
      linkKind :: LinkKind
linkKind = case MorphType
k of
          Definitional -> LinkKind
DefLink
          Postulated -> ThmLinkStatus -> LinkKind
ThmLink ThmLinkStatus
thmStatus
          Unknown -> FilePath -> LinkKind
forall a. HasCallStack => FilePath -> a
error "Unknown morphism type."
      consStatus :: ConsStatus
consStatus = Conservativity -> Conservativity -> ThmLinkStatus -> ConsStatus
ConsStatus Conservativity
Cons.None Conservativity
Cons.None ThmLinkStatus
LeftOpen
      linkType :: DGLinkType
linkType = Scope -> LinkKind -> ConsStatus -> DGLinkType
ScopedLink Scope
Global LinkKind
linkKind ConsStatus
consStatus
      linkLabel :: DGLinkLab
linkLabel = GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink GMorphism
gMorph DGLinkType
linkType DGLinkOrigin
SeeTarget
      (node1 :: Node
node1, dg1 :: DGraph
dg1) = Sign -> (FilePath, DGraph) -> NODE_MAP -> LibEnv -> (Node, DGraph)
addRefNode (Morphism -> Sign
source Morphism
morph) (FilePath
b, DGraph
dg) NODE_MAP
nm LibEnv
le
      (node2 :: Node
node2, dg2 :: DGraph
dg2) = Sign -> (FilePath, DGraph) -> NODE_MAP -> LibEnv -> (Node, DGraph)
addRefNode (Morphism -> Sign
target Morphism
morph) (FilePath
b, DGraph
dg1) NODE_MAP
nm LibEnv
le
      (_, dg3 :: DGraph
dg3) = LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG (Node
node1, Node
node2, DGLinkLab
linkLabel) DGraph
dg2

      in if MorphType
k MorphType -> MorphType -> Bool
forall a. Eq a => a -> a -> Bool
== MorphType
Definitional Bool -> Bool -> Bool
&& FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
n then DGraph
dg3 else
        let n' :: FilePath
n' = if MorphType
k MorphType -> MorphType -> Bool
forall a. Eq a => a -> a -> Bool
== MorphType
Postulated then FilePath
m else FilePath
m FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
sigDelimS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
n
            name :: IRI
name = SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ FilePath -> Range -> SIMPLE_ID
Token FilePath
n' Range
nullRange
            extSignSrc :: ExtSign Sign Symbol
extSignSrc = LF -> Sign -> ExtSign Sign Symbol
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 LF
LF (Sign -> ExtSign Sign Symbol) -> Sign -> ExtSign Sign Symbol
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
source Morphism
morph
            extSignTar :: ExtSign Sign Symbol
extSignTar = LF -> Sign -> ExtSign Sign Symbol
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 LF
LF (Sign -> ExtSign Sign Symbol) -> Sign -> ExtSign Sign Symbol
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
target Morphism
morph
            nodeSigSrc :: NodeSig
nodeSigSrc = Node -> G_sign -> NodeSig
NodeSig Node
node1 (G_sign -> NodeSig) -> G_sign -> NodeSig
forall a b. (a -> b) -> a -> b
$ LF -> ExtSign Sign Symbol -> 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 LF
LF ExtSign Sign Symbol
extSignSrc SigId
startSigId
            nodeSigTar :: NodeSig
nodeSigTar = Node -> G_sign -> NodeSig
NodeSig Node
node2 (G_sign -> NodeSig) -> G_sign -> NodeSig
forall a b. (a -> b) -> a -> b
$ LF -> ExtSign Sign Symbol -> 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 LF
LF ExtSign Sign Symbol
extSignTar SigId
startSigId
            emptyNode :: MaybeNode
emptyNode = AnyLogic -> MaybeNode
EmptyNode (AnyLogic -> MaybeNode) -> AnyLogic -> MaybeNode
forall a b. (a -> b) -> a -> b
$ LF -> 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 LF
LF
            genSigTar :: GenSig
genSigTar = MaybeNode -> [NodeSig] -> MaybeNode -> GenSig
GenSig MaybeNode
emptyNode [] MaybeNode
emptyNode
            extGenSigTar :: ExtGenSig
extGenSigTar = GenSig -> NodeSig -> ExtGenSig
ExtGenSig GenSig
genSigTar NodeSig
nodeSigTar
            gEntry :: GlobalEntry
gEntry = Bool -> ExtViewSig -> GlobalEntry
ViewOrStructEntry Bool
False
              (ExtViewSig -> GlobalEntry) -> ExtViewSig -> GlobalEntry
forall a b. (a -> b) -> a -> b
$ NodeSig -> GMorphism -> ExtGenSig -> ExtViewSig
ExtViewSig NodeSig
nodeSigSrc GMorphism
gMorph ExtGenSig
extGenSigTar
            dg4 :: DGraph
dg4 = DGraph
dg3 { 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
dg3 }
            in DGraph
dg4

-- constructs a reference node to the specified signature, if needed
addRefNode :: Sign -> (BASE, DGraph) -> NODE_MAP -> LibEnv -> (Node, DGraph)
addRefNode :: Sign -> (FilePath, DGraph) -> NODE_MAP -> LibEnv -> (Node, DGraph)
addRefNode sig :: Sign
sig (base :: FilePath
base, dg :: DGraph
dg) nm :: NODE_MAP
nm le :: LibEnv
le =
  let b :: FilePath
b = Sign -> FilePath
sigBase Sign
sig
      m :: FilePath
m = Sign -> FilePath
sigModule Sign
sig
      nod :: Node
nod = Node -> (FilePath, FilePath) -> NODE_MAP -> Node
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (FilePath -> Node
forall a. HasCallStack => FilePath -> a
error "Node number cannot be found.") (FilePath
b, FilePath
m) NODE_MAP
nm
      in if FilePath
b FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
base then (Node
nod, DGraph
dg) else
            let info :: DGNodeInfo
info = LibName -> Node -> DGNodeInfo
newRefInfo (FilePath -> LibName
emptyLibName FilePath
b) Node
nod
                refNodeM :: Maybe Node
refNodeM = DGNodeInfo -> DGraph -> Maybe Node
lookupInAllRefNodesDG DGNodeInfo
info DGraph
dg
                in case Maybe Node
refNodeM of
                        Just refNode :: Node
refNode -> (Node
refNode, DGraph
dg)
                        Nothing -> Sign -> DGNodeInfo -> DGraph -> LibEnv -> (Node, DGraph)
insRefSigToDG Sign
sig DGNodeInfo
info DGraph
dg LibEnv
le

-- inserts a signature as a reference node to the development graph
insRefSigToDG :: Sign -> DGNodeInfo -> DGraph -> LibEnv -> (Node, DGraph)
insRefSigToDG :: Sign -> DGNodeInfo -> DGraph -> LibEnv -> (Node, DGraph)
insRefSigToDG sig :: Sign
sig info :: DGNodeInfo
info dg :: DGraph
dg le :: LibEnv
le =
  let node :: Node
node = DGraph -> Node
getNewNodeDG DGraph
dg
      m :: FilePath
m = Sign -> FilePath
sigModule Sign
sig
      nodeName :: NodeName
nodeName = NodeName
emptyNodeName { getName :: IRI
getName = SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ FilePath -> Range -> SIMPLE_ID
Token FilePath
m Range
nullRange }
      extSign :: ExtSign Sign Symbol
extSign = LF -> Sign -> ExtSign Sign Symbol
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 LF
LF Sign
sig
      gth :: G_theory
gth = LF -> ExtSign Sign Symbol -> 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 LF
LF ExtSign Sign Symbol
extSign SigId
startSigId
      nodeLabel1 :: DGNodeLab
nodeLabel1 = NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab NodeName
nodeName DGNodeInfo
info G_theory
gth
      refDG :: DGraph
refDG = LibName -> LibEnv -> DGraph
lookupDGraph (DGNodeInfo -> LibName
ref_libname DGNodeInfo
info) LibEnv
le
      refGlobTh :: Maybe G_theory
refGlobTh = DGNodeLab -> Maybe G_theory
globalTheory (DGNodeLab -> Maybe G_theory) -> DGNodeLab -> Maybe G_theory
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> DGNodeLab
labDG DGraph
refDG (Node -> DGNodeLab) -> Node -> DGNodeLab
forall a b. (a -> b) -> a -> b
$ DGNodeInfo -> Node
ref_node DGNodeInfo
info
      nodeLabel2 :: DGNodeLab
nodeLabel2 = DGNodeLab
nodeLabel1 { globalTheory :: Maybe G_theory
globalTheory = Maybe G_theory
refGlobTh}
      dg1 :: DGraph
dg1 = LNode DGNodeLab -> DGraph -> DGraph
insNodeDG (Node
node, DGNodeLab
nodeLabel2) DGraph
dg
      in (Node
node, DGraph
dg1)