0N/A{- HetCATS/DGToSpec.hs

0N/A $Id$

0N/A Till Mossakowski

0N/A

0N/A Convert development graph back to structured specification

0N/A

0N/A Todo:

0N/A

0N/A-}

0N/A

0N/A

0N/Amodule DGToSpec

0N/Awhere

0N/A

0N/Aimport Data.Maybe

0N/Aimport Logic

0N/Aimport LogicRepr

0N/Aimport Grothendieck

0N/Aimport Common.Lib.Graph

0N/Aimport DevGraph

0N/Aimport AS_Structured

0N/Aimport AS_Annotation

0N/Aimport GlobalAnnotations

0N/Aimport GlobalAnnotationsFunctions

0N/Aimport Result

0N/Aimport Id

0N/Aimport Common.Lib.Set

0N/Aimport FiniteMap

0N/Aimport Data.List

0N/Aimport PrettyPrint

0N/A

0N/AemptyAnno x = Annoted x [] [] []

0N/A

0N/AdgToSpec :: DGraph -> Node -> Result SPEC

0N/AdgToSpec dg node = do

0N/A let (_,_,n,preds) = context node dg

0N/A predSps <- sequence (map (dgToSpec dg . snd) preds)

0N/A let apredSps = map emptyAnno predSps

0N/A pos = map (\_ -> nullPos) predSps

0N/A case n of

0N/A (DGNode _ (G_sign lid1 sigma) (G_l_sentence lid2 sen) DGBasic) ->

0N/A do sen' <- rcoerce lid1 lid2 nullPos sen

0N/A let b = Basic_spec (G_basic_spec lid1 (sign_to_basic_spec lid1 sigma sen'))

0N/A if null apredSps

0N/A then return b

0N/A else return (Extension (apredSps++[emptyAnno b]) pos)

0N/A (DGNode _ _ _ DGExtension) ->

0N/A return (Extension apredSps pos)

0N/A (DGNode _ _ _ DGUnion) ->

0N/A return (Union apredSps pos)

0N/A (DGNode _ _ _ DGTranslation) ->

0N/A return (Translation (head apredSps) (Renaming [] []))

0N/A (DGNode _ _ _ DGHiding) ->

0N/A return (Reduction (head apredSps) (Hidden [] []))

0N/A (DGNode _ _ _ DGRevealing) ->

0N/A return (Reduction (head apredSps) (Hidden [] []))

0N/A (DGNode _ _ _ DGFree) ->

0N/A return (Free_spec (head apredSps) pos)

0N/A (DGNode _ _ _ DGCofree) ->

0N/A return (Cofree_spec (head apredSps) pos)

0N/A (DGNode _ _ _ (DGSpecInst name)) ->

0N/A return (Spec_inst name [] pos)

0N/A (DGRef (Just name) _ _) -> return (Spec_inst name [] pos)

0N/A otherwise -> return (Extension apredSps pos)

0N/A