{- |

Module : $Header$

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 _ fp = do

(libs, bs) <- twelf2GR LATIN fp (Map.empty, [])

let libenv = makeLibEnv libs bs

file <- toAbsoluteURI fp

lname <- toLibName LATIN file

return $ Just (emptyLibName lname, 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 bs = fst $

foldl ( \ (le, nm) b ->

let (sigs, morphs) = Map.findWithDefault

(error "Library cannot be found.") b libs

ln = emptyLibName b

le1 = Map.insert ln emptyDG le

(le2, nm1) = addNodes le1 nm b sigs

le3 = addLinks le2 nm1 b morphs

dg = computeDGraphTheories le3 $ lookupDGraph ln le3

le4 = Map.insert ln dg le3

in (le4, nm1)

) (emptyLibEnv, Map.empty) 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 le nm b sigs =

let ln = emptyLibName b

(dg2, nm1) = Map.foldWithKey

(\ m sig (dg, nmap) ->

let (n, dg1) = addSigToDG sig dg

nmap1 = Map.insert (b, m) n nmap

in (dg1, nmap1)

) (lookupDGraph ln le, nm) sigs

le1 = Map.insert ln dg2 le

in (le1, nm1)

-- inserts a signature as a node to the development graph

addSigToDG :: Sign -> DGraph -> (Node, DGraph)

addSigToDG sig dg =

let node = getNewNodeDG dg

name = simpleIdToIRI $ Token (sigModule sig) nullRange

nodeName = emptyNodeName { getName = name }

info = newNodeInfo DGBasic

extSign = makeExtSign LF sig

gth = noSensGTheory LF extSign startSigId

nodeLabel = newInfoNodeLab nodeName info gth

dg1 = insNodeDG (node, nodeLabel) dg

emptyNode = EmptyNode $ Logic LF

gSig = GenSig emptyNode [] emptyNode

nodeSig = NodeSig node $ G_sign LF extSign startSigId

gEntry = SpecEntry $ ExtGenSig gSig nodeSig

dg2 = dg1 { globalEnv = Map.insert name gEntry $ globalEnv dg1 }

in (node, dg2)

-- adds links to the library environment

addLinks :: LibEnv -> NODE_MAP -> BASE -> MORPHS -> LibEnv

addLinks le nm b morphs =

let ln = emptyLibName b

dg1 = Map.fold (\ morph dg -> addMorphToDG morph dg nm le)

(lookupDGraph ln le) morphs

in Map.insert ln dg1 le

-- inserts a morphism as a link to the development graph

addMorphToDG :: Morphism -> DGraph -> NODE_MAP -> LibEnv -> DGraph

addMorphToDG morph dg nm le =

let b = morphBase morph

m = morphModule morph

n = morphName morph

k = morphType morph

gMorph = gEmbed $ G_morphism LF morph startMorId

thmStatus = Proven (DGRule "Type-checked") emptyProofBasis

linkKind = case k of

Definitional -> DefLink

Postulated -> ThmLink thmStatus

Unknown -> error "Unknown morphism type."

consStatus = ConsStatus Cons.None Cons.None LeftOpen

linkType = ScopedLink Global linkKind consStatus

linkLabel = defDGLink gMorph linkType SeeTarget

(node1, dg1) = addRefNode (source morph) (b, dg) nm le

(node2, dg2) = addRefNode (target morph) (b, dg1) nm le

(_, dg3) = insLEdgeDG (node1, node2, linkLabel) dg2

in if k == Definitional && null n then dg3 else

let n' = if k == Postulated then m else m ++ sigDelimS ++ n

name = simpleIdToIRI $ Token n' nullRange

extSignSrc = makeExtSign LF $ source morph

extSignTar = makeExtSign LF $ target morph

nodeSigSrc = NodeSig node1 $ G_sign LF extSignSrc startSigId

nodeSigTar = NodeSig node2 $ G_sign LF extSignTar startSigId

emptyNode = EmptyNode $ Logic LF

genSigTar = GenSig emptyNode [] emptyNode

extGenSigTar = ExtGenSig genSigTar nodeSigTar

gEntry = ViewOrStructEntry False

$ ExtViewSig nodeSigSrc gMorph extGenSigTar

dg4 = dg3 { globalEnv = Map.insert name gEntry $ globalEnv dg3 }

in dg4

-- constructs a reference node to the specified signature, if needed

addRefNode :: Sign -> (BASE, DGraph) -> NODE_MAP -> LibEnv -> (Node, DGraph)

addRefNode sig (base, dg) nm le =

let b = sigBase sig

m = sigModule sig

nod = Map.findWithDefault (error "Node number cannot be found.") (b, m) nm

in if b == base then (nod, dg) else

let info = newRefInfo (emptyLibName b) nod

refNodeM = lookupInAllRefNodesDG info dg

in case refNodeM of

Just refNode -> (refNode, dg)

Nothing -> insRefSigToDG sig info dg le

-- inserts a signature as a reference node to the development graph

insRefSigToDG :: Sign -> DGNodeInfo -> DGraph -> LibEnv -> (Node, DGraph)

insRefSigToDG sig info dg le =

let node = getNewNodeDG dg

m = sigModule sig

nodeName = emptyNodeName { getName = simpleIdToIRI $ Token m nullRange }

extSign = makeExtSign LF sig

gth = noSensGTheory LF extSign startSigId

nodeLabel1 = newInfoNodeLab nodeName info gth

refDG = lookupDGraph (ref_libname info) le

refGlobTh = globalTheory $ labDG refDG $ ref_node info

nodeLabel2 = nodeLabel1 { globalTheory = refGlobTh}

dg1 = insNodeDG (node, nodeLabel2) dg

in (node, dg1)