type NODE = (BASE,MODULE)
type LINK = (BASE,MODULE,NAME)
type MORPHS =
Map.Map (LINK,NODE,NODE) Morphism
type GRAPH = (SIGS,MORPHS)
type NODE_MAP =
Map.Map NODE (Sign,Node)
type LINK_MAP =
Map.Map LINK Morphism
type GR_MAP = (NODE_MAP,LINK_MAP)
type LibEnvExt = (LibEnv,GR_MAP)
type LibEnvFull = (LibEnvExt,BASE,GRAPH)
openMathNS :: Maybe String
omdocQN = QName "omdoc" omdocNS Nothing
theoryQN = QName "theory" omdocNS Nothing
viewQN = QName "view" omdocNS Nothing
includeQN = QName "include" omdocNS Nothing
structureQN = QName "structure" omdocNS Nothing
constantQN = QName "constant" omdocNS Nothing
aliasQN = QName "alias" omdocNS Nothing
notationQN = QName "notation" omdocNS Nothing
typeQN = QName "type" omdocNS Nothing
definitionQN = QName "definition" omdocNS Nothing
omobjQN = QName "OMOBJ" openMathNS Nothing
omsQN = QName "OMS" openMathNS Nothing
omaQN = QName "OMA" openMathNS Nothing
ombindQN = QName "OMBIND" openMathNS Nothing
ombvarQN = QName "OMBVAR" openMathNS Nothing
omattrQN = QName "OMATTR" openMathNS Nothing
omatpQN = QName "OMATP" openMathNS Nothing
omvQN = QName "OMV" openMathNS Nothing
ommorQN = QName "OMMOR" omdocNS Nothing
conassQN = QName "conass" omdocNS Nothing
strassQN = QName "strass" omdocNS Nothing
Element omsQN [Attr baseQN lfBase,
Attr nameQN "type"] [] Nothing
Element omsQN [Attr baseQN lfBase,
Attr nameQN "arrow"] [] Nothing
Element omsQN [Attr baseQN lfBase,
Attr nameQN "lambda"] [] Nothing
Element omsQN [Attr baseQN lfBase,
Attr nameQN "Pi"] [] Nothing
Element omsQN [Attr baseQN lfBase,
Attr nameQN "implicit_lambda"] [] Nothing
Element omsQN [Attr baseQN lfBase,
Attr nameQN "implicit_Pi"] [] Nothing
Element omsQN [Attr baseQN lfBase,
Attr nameQN "oftype"] [] Nothing
Element omsQN [Attr baseQN mmtBase,
Attr nameQN "composition"] [] Nothing
nameQN = (QName "name" Nothing Nothing)
moduleQN = (QName "module" Nothing Nothing)
baseQN = (QName "base" Nothing Nothing)
fromQN = (QName "from" Nothing Nothing)
toQN = (QName "to" Nothing Nothing)
-- path to the Twelf folder must be set in the environment variable TWELF_LIB
------------------------------------------------------------------------------
------------------------------------------------------------------------------
getNameAttr :: Element -> String
case findAttr nameQN e of
Nothing -> error $ "Element is missing a name." ++ (show e)
getModuleAttr :: Element -> Maybe String
getModuleAttr e = findAttr moduleQN e
getBaseAttr :: Element -> Maybe String
getBaseAttr e = findAttr baseQN e
getFromAttr :: Element -> String
case findAttr fromQN e of
Nothing -> error "Element is missing a \"from\" attribute."
getToAttr :: Element -> String
Nothing -> error "Element is missing a \"to\" attribute."
-- retrieves the base, module, and name attributes
getBMN :: Element -> NODE -> (BASE,MODULE,NAME)
let n = case findAttr nameQN e of
m = case getModuleAttr e of
b = case getBaseAttr e of
Just b' -> replaceExtension (resolve b' base) ".elf"
-- compares two OMS elements
eqOMS :: Element -> Element -> Bool
if (elName e1 /= omsQN || elName e2 /= omsQN)
else and [getNameAttr e1 == getNameAttr e2
,getModuleAttr e1 == getModuleAttr e2
,getBaseAttr e1 == getBaseAttr e2]
-- resolves the first file path wrt to the second
resolve :: FilePath -> FilePath -> FilePath
case parseURIReference fp1 of
Nothing -> error "Invalid file name."
case parseURIReference fp2 of
Nothing -> error "Invalid file name."
case relativeTo uri1 uri2 of
Nothing -> error "Invalid file name."
-- returns the referenced base and module
parseRef :: String -> String -> NODE
case elemIndices '?' ref of
[i] -> let (br,(_:m)) = splitAt i ref
b = replaceExtension (resolve br base) "elf"
_ -> error "Invalid reference."
{- parses the referenced file if needed and imports all signatures
addFromFile :: FilePath -> LibEnvFull -> IO LibEnvFull
addFromFile file libs@(le@(lenv,_),base,gr) =
if (file == base ||
Map.member (emptyLibName file) lenv)
else do le1 <- twelf2DG file le
-- looks up the node number for the given signature reference
lookupNode :: NODE -> LibEnvFull -> Node
lookupNode ref ((_,(sigmap,_)),_,_) =
Nothing -> error $ "Node number cannot be found." ++ (show ref)
-- finds the signature by base and module
lookupSig :: NODE -> LibEnvFull -> Sign
lookupSig ref ((_,(sigmap,_)),_,(sigs,_)) =
Nothing -> error "Signature cannot be found."
-- finds the morphism by base, module, and name
lookupMorph :: LINK -> LibEnvFull -> Morphism
lookupMorph ref ((_,(_,mormap)),_,(_,morphs)) =
_ -> error "Morphism cannot be found."
-- adds the signature to the signature collection
addSigToGraph :: Sign -> LibEnvFull -> LibEnvFull
addSigToGraph sig (le,file,(sigs,morphs)) =
in (le,file,(sigs1,morphs))
-- adds the morphism to the morphism collection
addMorphToGraph :: Morphism -> LibEnvFull -> LibEnvFull
addMorphToGraph m (le,file,(sigs,morphs)) =
l = (morphBase m, morphModule m, morphName m)
s = (sigBase sig1, sigModule sig1)
t = (sigBase sig2, sigModule sig2)
in (le,file,(sigs,morphs1))
-- adds the signature to the node map
addSigToGrMap :: Sign -> Node -> LibEnvFull -> LibEnvFull
addSigToGrMap sig nod ((l,(sigmap,mormap)),file,gr) =
in ((l,(sigmap1,mormap)),file,gr)
-- adds the morphism to the link map
addMorphToGrMap :: Morphism -> LibEnvFull -> LibEnvFull
addMorphToGrMap morph ((l,(sigmap,mormap)),file,gr) =
in ((l,(sigmap,mormap1)),file,gr)
------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- CONSTRUCTING THE DGRAPH
-- analyzes the given Twelf file
anaTwelfFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
dir <- getCurrentDirectory
let file = resolve fp (dir ++ "/")
let name = emptyLibName file
(libs,_) <- twelf2DG file (emptyLibEnv,emptyGrMap)
return $ Just (name,libs)
-- updates the library environment by adding specs from the Twelf file
twelf2DG :: FilePath -> LibEnvExt -> IO LibEnvExt
twelf2DG file le = trace ("Analyzing file: " ++ show file) $ do
libs <- buildGraph file le
-- runs twelf to create an omdoc file
runTwelf :: FilePath -> IO ()
let dir = dropFileName file
twelfdir <- getEnvDef "TWELF_LIB" ""
then error "environment variable TWELF_LIB is not set"
runInteractiveProcess (concat [twelfdir, "/" ,twelf])
exitCode <- waitForProcess pr
error $ "Calling Twelf failed with exitCode: " ++ show i ++
-- generates a library environment from raw libraries
makeLibEnv :: LibEnvFull -> LibEnvExt
let libs1 = addNodes libs
((l,grmap),file,_) = libs2
lname = emptyLibName file
dg = computeDGraphTheories l $ lookupDGraph lname l
-- adds nodes to the library environment
addNodes :: LibEnvFull -> LibEnvFull
addNodes libs@(_,_,(sigs,_)) =
let (nod,dg1) = addSigToDG sig dg
libs2 = addSigToGrMap sig nod libs1
((l,grmap),base,gr) = libs3
-- inserts a signature as a node to the development graph
addSigToDG :: Sign -> DGraph -> (Node,DGraph)
let node = getNewNodeDG dg
nodeName = emptyNodeName { getName = Token m nullRange }
info = newNodeInfo DGBasic
extSign = makeExtSign LF sig
gth = noSensGTheory LF extSign startSigId
nodeLabel = newInfoNodeLab nodeName info gth
dg1 = insNodeDG (node,nodeLabel) dg
-- adds links to the library environment
addLinks :: LibEnvFull -> LibEnvFull
addLinks libs@((l,_),file,(_,morphs)) =
let lname = emptyLibName file
dg = lookupDGraph lname l
let sig = lookupSig t libs1
morph1 = morph { target = sig }
dg2 = addMorphToDG morph1 dg1 libs1
libs2 = addMorphToGrMap morph1 libs1
((l1,grmap),_,gr) = libs3
-- inserts a morphism as a link to the development graph
addMorphToDG :: Morphism -> DGraph -> LibEnvFull -> DGraph
addMorphToDG morph dg libs =
let gmorph = gEmbed $ G_morphism LF morph startMorId
thmStatus = Proven (DGRule "Type-checked") emptyProofBasis
linkKind = case morphType morph of
Postulated -> ThmLink thmStatus
Unknown -> error "Unknown morphism type."
linkType = ScopedLink Global linkKind consStatus
linkLabel = defDGLink gmorph linkType SeeTarget
(node1,dg1) = addRefNode dg (source morph) libs
(node2,dg2) = addRefNode dg1 (target morph) libs
in snd $ insLEdgeDG (node1,node2,linkLabel) dg2
-- constructs a reference node to the specified signature, if needed
addRefNode :: DGraph -> Sign -> LibEnvFull -> (Node,DGraph)
addRefNode dg sig libs@(_,file,_) =
node = lookupNode (b,m) libs
else let info = newRefInfo (emptyLibName b) node
refNodeM = lookupInAllRefNodesDG info dg
Just refNode -> (refNode,dg)
Nothing -> insRefSigToDG sig info dg libs
-- inserts a signature as a reference node to the development graph
insRefSigToDG :: Sign -> DGNodeInfo -> DGraph -> LibEnvFull -> (Node,DGraph)
insRefSigToDG sig info dg ((l,_),_,_) =
let node = getNewNodeDG dg
nodeName = emptyNodeName { getName = Token m nullRange }
extSign = makeExtSign LF sig
gth = noSensGTheory LF extSign startSigId
nodeLabel1 = newInfoNodeLab nodeName info gth
refDG = lookupDGraph (ref_libname info) l
refGlobTh = globalTheory $ labDG refDG $ ref_node info
nodeLabel2 = nodeLabel1 { globalTheory = refGlobTh}
dg1 = insNodeDG (node,nodeLabel2) dg
dg2 = addToRefNodesDG node info dg1
------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- CONSTRUCTING SIGNATURES AND MORPHISMS
-- builds raw development graph libraries
buildGraph :: FilePath -> LibEnvExt -> IO LibEnvFull
let omdoc_file = replaceExtension file "omdoc"
xml <- readFile omdoc_file
let elems = onlyElems $ parseXML xml
let elems1 = filter (\ e -> elName e == omdocQN) elems
in if (n == theoryQN) then addSign e libs else
if (n == viewQN) then addView e libs else
_ -> fail "Not an OMDoc file."
-- transforms a theory element into a signature and adds it to the libraries
addSign :: Element -> LibEnvFull -> IO LibEnvFull
addSign e libs@(_,base,_) = do
let sig = Sign base name []
in if (n == includeQN) then addIncl el ls else
if (n == structureQN) then addStruct el ls else
if (n == constantQN) then addConst el ls else
if (n == aliasQN) then addAlias el ls else
if (n == notationQN) then addNotat el ls else
return $ addSigToGraph sig1 libs1
-- so far views are ignored
addView :: Element -> LibEnvFull -> IO LibEnvFull
addView e libs@(_,file,_) = do
let src = parseRef from file
let tar = parseRef to file
libs1 <- addFromFile (fst src) libs
libs2 <- addFromFile (fst tar) libs1
let srcSig = lookupSig src libs2
let tarSig = lookupSig tar libs2
(morph,libs3) <- getViewMorph name srcSig tarSig (elChildren e) libs2
let libs4 = addMorphToGraph morph libs3
{- constructs the view morphism -}
getViewMorph :: String -> Sign -> Sign -> [Element] -> LibEnvFull ->
getViewMorph name srcSig tarSig els libs@(_,file,_) = do
let m1 = sigModule srcSig
let m2 = sigModule tarSig
(symmap,libs1) <- constructMap els (b1,m1) (b2,m2) libs
let morph = Morphism file name "" srcSig tarSig Postulated symmap
------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- CONSTRUCTING CONSTANTS
-- adds a constant declaration to the signature
addConst :: Element -> (LibEnvFull,Sign) -> IO (LibEnvFull,Sign)
addConst e (lib,sig) = do
let ref@(base,modul) = (sigBase sig, sigModule sig)
let sym = Symbol base modul $ getNameAttr e
let typ = case findChildren typeQN e of
_ -> error "Constant element must have a unique type child."
let val = case findChildren definitionQN e of
[v] -> Just $ definition2exp v ref
_ -> error $ concat ["Constant element must have at most ",
let sig1 = addDef (Def sym typ val) sig
-- converts a type element to an expression
type2exp :: Element -> NODE -> EXP
case findChildren omobjQN e of
[omobj] -> omobj2exp omobj ref
_ -> error "Type element must have a unique OMOBJ child."
-- converts a definition element to an expression
definition2exp :: Element -> NODE -> EXP
case findChildren omobjQN e of
[omobj] -> omobj2exp omobj ref
_ -> error "Definition element must have a unique OMOBJ child."
-- converts an OMOBJ element to an expression
omobj2exp :: Element -> NODE -> EXP
_ -> error "OMOBJ element must have a unique child."
-- converts an Open Math element to an expression
omel2exp :: Element -> NODE -> EXP
in if (name == omsQN) then oms2exp e ref else
if (name == omaQN) then oma2exp e ref else
if (name == ombindQN) then ombind2exp e ref else
if (name == omvQN) then omv2exp e ref else
error $ concat ["Only OMA, OMS, and OMBIND elements correspond "
-- converts an OMS element to an expression
oms2exp :: Element -> NODE -> EXP
else let (b,m,n) = getBMN e ref
-- converts an OMA element to an expression
oma2exp :: Element -> NODE -> EXP
[] -> error "OMA element must have at least one child."
let as1 = map (\ a -> omel2exp a ref) as
concat ["The -> constructor must be applied"
," to at least one argument."]
_ -> Func (init as1) (last as1)
else let f1 = omel2exp f ref
-- converts an OMBIND element to an expression
ombind2exp :: Element -> NODE -> EXP
if (elName d /= ombvarQN)
then error "The second child of OMBIND must be OMBVAR."
else let d1 = ombvar2decls d ref
in if (eqOMS f lambdaOMS) then Lamb d1 b1 else
if (eqOMS f piOMS) then Pi d1 b1 else
{- so far implicit binders are treated
if (eqOMS f impLambdaOMS) then Lamb d1 b1 else
if (eqOMS f impPiOMS) then Pi d1 b1 else
error $ concat ["The first child of OMBIND "
,"must be be Pi or Lambda."]
_ -> error "OMBIND element must have exactly 3 children."
-- converts an OMBVAR element to a list of declaration
ombvar2decls :: Element -> NODE -> [DECL]
let attrs = findChildren omattrQN e
in map (\ a -> omattr2decl a ref) attrs
-- converts an OMATTR element to a declaration
omattr2decl :: Element -> NODE -> DECL
case findChildren omatpQN e of
case findChildren omvQN e of
[omv] -> (getNameAttr omv, omatp2exp omatp ref)
_ -> error "OMATTR element must have a unique OMV child."
_ -> error "OMATTR element must have a unique OMATP child."
-- converts an OMATP element to an expression
omatp2exp :: Element -> NODE -> EXP
else error $ concat ["The first child of OMATP",
"must be the \"oftype\" symbol."]
_ -> error "OMATP element must have exactly two children."
-- converts an OMV element to an expression
omv2exp :: Element -> NODE -> EXP
omv2exp e _ = Var $ getNameAttr e
------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- CONSTRUCTING INCLUSIONS
{- adds declarations arising from an inclusion to the signature
adds the inclusion to the morphism map -}
addIncl :: Element -> (LibEnvFull,Sign) -> IO (LibEnvFull,Sign)
addIncl e (libs@(_,file,_),sig) = do
let src = parseRef from file
libs1 <- addFromFile (fst src) libs
let srcSig = lookupSig src libs1
let tarSig = addInclSyms srcSig sig
let morph = getInclMorph srcSig tarSig
let libs2 = addMorphToGraph morph libs1
-- adds included definitions to the signature
addInclSyms :: Sign -> Sign -> Sign
addInclSyms (Sign _ _ ds) sig =
let syms = getAllSyms sig
-- constructs the inclusion morphism
getInclMorph :: Sign -> Sign -> Morphism
Morphism (sigBase sig2) (sigModule sig2) "" sig1 sig2 Definitional
Map.empty------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- CONSTRUCTING STRUCTURES
{- adds declarations arising from a structure to the signature
adds the structure to the morphism map -}
addStruct :: Element -> (LibEnvFull,Sign) -> IO (LibEnvFull,Sign)
addStruct e (libs@(_,file,_),sig) = do
let src = parseRef from file
libs1 <- addFromFile (fst src) libs
let srcSig = lookupSig src libs1
(tarSig,morph,libs2) <- processStruct name srcSig sig (elChildren e) libs1
let libs3 = addMorphToGraph morph libs2
{- adds the definitions imported by a structure to the signature and
constructs the structure morphism -}
processStruct :: String -> Sign -> Sign -> [Element] -> LibEnvFull ->
IO (Sign,Morphism,LibEnvFull)
processStruct name srcSig tarSig els libs = do
let m1 = sigModule srcSig
let m2 = sigModule tarSig
let rel sym = Symbol b2 m2 $ prefix ++ (symName sym)
(symmap,libs1) <- constructMap els (b1,m1) (b2,m2) libs
Morphism b2 m2 name (Sign b1 m1 []) tarSig Definitional
Map.empty foldl (\ (sig,morph) (Def s t v) ->
let local = isLocalSym s srcSig
defined = isDefinedSym s srcSig
sig1 = if (not local) then sig else
t1 = case translate morph t of
"Structure could not be formed. "
Just v1' -> translate morph v1'
in addDef (Def s1 t1 v1) sig
morph1 = let source1 = addDef (Def s t v) $ source morph
in morph { source = source1
in (sig1, canForm morph1)
return (sig2,morph2,libs1)
-- constructs the translation part of the structure
constructMap :: [Element] -> NODE -> NODE -> LibEnvFull ->
IO (
Map.Map Symbol EXP, LibEnvFull)
constructMap els src tar libs = do
in if (n == conassQN) then conass2map el ml src tar else
if (n == includeQN) then incl2map el ml src tar else
if (n == strassQN) then strass2map el ml src tar else
-- converts the constant assignment into a map
conass2map :: Element -> (
Map.Map Symbol EXP, LibEnvFull) -> NODE ->
NODE -> IO (
Map.Map Symbol EXP, LibEnvFull)
conass2map e (mapp,libs) src tar = do
let (b,m,n) = getBMN e src
case findChildren omobjQN e of
[omobj] -> do let expr = omobj2exp omobj tar
_ -> error "Constant assignment element must have a unique OMMOR child."
-- converts the included morphism into a map
incl2map :: Element -> (
Map.Map Symbol EXP, LibEnvFull) -> NODE ->
NODE -> IO (
Map.Map Symbol EXP, LibEnvFull)
case findChildren ommorQN e of
[ommor] -> do (mor,l1) <- ommor2mor ommor tar l
_ -> error "Include element must have a unique OMMOR child."
-- converts the structure assignment into a map
strass2map :: Element -> (
Map.Map Symbol EXP, LibEnvFull) -> NODE ->
NODE -> IO (
Map.Map Symbol EXP, LibEnvFull)
strass2map e (m,l) src tar =
case findChildren ommorQN e of
[ommor] -> do (mor1,l1) <- retrieveMorph (getBMN e src) l
(mor2,l2) <- ommor2mor ommor tar l1
let m1 =
Map.union m $ combineMorphs mor1 mor2
_ -> error "Structure assignment element must have a unique OMMOR child."
-- converts an OMMOR element to a morphism
ommor2mor :: Element -> NODE -> LibEnvFull -> IO (Morphism,LibEnvFull)
[el] -> omel2mor el ref libs
_ -> error "OMMOR element must have a unique child."
-- converts an Open Math element to a morphism
omel2mor :: Element -> NODE -> LibEnvFull -> IO (Morphism,LibEnvFull)
in if (name == omsQN) then oms2mor e ref libs else
if (name == omaQN) then oma2mor e ref libs else
error "Only OMA and OMS elements correspond to a morphism."
-- converts an OMS element to a morphism
oms2mor :: Element -> NODE -> LibEnvFull -> IO (Morphism,LibEnvFull)
oms2mor e ref libs = retrieveMorph (getBMN e ref) libs
-- converts an OMA element to a morphism
oma2mor :: Element -> NODE -> LibEnvFull -> IO (Morphism,LibEnvFull)
then do (mor1,l1) <- omel2mor m1 ref l
(mor2,l2) <- omel2mor m2 ref l1
let morR = compMorph (mor1 { target = source mor2 }) mor2
Result _ (Just mor') -> mor'
_ -> error "Morphism cannot be retrieved."
else error "The first child of OMA in OMMOR must be composition."
_ -> error "OMA in OMMOR must have exactly three children."
-- retrieves a morphism by the link name
retrieveMorph :: LINK -> LibEnvFull -> IO (Morphism,LibEnvFull)
retrieveMorph (b,m,n) l = do
l1 <- addFromFile (replaceExtension b "elf") l
let mor = lookupMorph (b,m,n) l1
let (n1,(_:n2)) = splitAt i n
let mor1 = lookupMorph (b,m,n1) l1
(mor2,l2) <- retrieveMorph (b1,m1,n2) l1
let morR = compMorph (mor2 { target = sig }) mor1
Result _ (Just mor') -> mor'
_ -> error "Morphism cannot be retrieved."
-- combines two morphisms according to the structure assignment
combineMorphs :: Morphism -> Morphism ->
Map.Map Symbol EXP
combineMorphs mor1 mor2 =
let local = getLocalSyms $ source mor1
declared = getDeclaredSyms $ source mor1
let s1 = case mapSymbol s mor1 of
_ -> error $ "Morphisms cannot be combined."
e1 = case mapSymbol s mor2 of
_ -> error $ "Morphisms cannot be combined."
------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- CONSTRUCTING ALIASES AND NOTATIONS
-- so far aliases are ignored
addAlias :: Element -> (LibEnvFull,Sign) -> IO (LibEnvFull,Sign)
addAlias _ ls = return ls
-- so far notations are ignored
addNotat :: Element -> (LibEnvFull,Sign) -> IO (LibEnvFull,Sign)
addNotat _ ls = return ls