cleaned up Freeness

git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@13406 cec4b9c1-7d33-0410-9eda-942365e851bb
spechub · Apr 29, 2010 · 3cca22b · 3cca22b
1 parent 81324b7
commit 3cca22b
Show file tree

Hide file tree

Showing 3 changed files with 125 additions and 125 deletions.
diff --git a/Interfaces/CmdAction.hs b/Interfaces/CmdAction.hs
@@ -15,7 +15,7 @@ module Interfaces.CmdAction where
 
 import Proofs.QualifyNames (qualifyLibEnv)
 import Proofs.DGFlattening
-import Proofs.Freeness(freeness, theoremFreeShift)
+import Proofs.Freeness(freeness)
 import Proofs.NormalForm (normalForm)
 import Proofs.Automatic(automatic)
 import Proofs.Global (globSubsume, globDecomp)
@@ -51,7 +51,8 @@ globLibResultAct =
   , (Colimit, computeColimit)
   , (NormalForm, normalForm)
   , (Freeness, freeness)
-  , (ThmFreeShift, theoremFreeShift) ]
+--  , (ThmFreeShift, theoremFreeShift)
+  ]
 
 globResultAct :: [(GlobCmd, LibEnv -> Result LibEnv)]
 globResultAct =

diff --git a/Proofs/Freeness.hs b/Proofs/Freeness.hs
@@ -13,8 +13,6 @@ compute normal forms
 
 module Proofs.Freeness
     ( freeness
-    , theoremFreeShift
-    , theoremFreeShiftFromList
     ) where
 
 import Logic.Logic
@@ -29,20 +27,20 @@ import Static.GTheory
 import Static.DevGraph
 import Static.History
 
-import Proofs.EdgeUtils
+--import Proofs.EdgeUtils
 import Common.ExtSign
 import Common.LibName
 import Common.Result
 
 import Data.Graph.Inductive.Graph as Graph
 import qualified Data.Map as Map
 import Control.Monad
-import Comorphisms.LogicGraph
+--import Comorphisms.LogicGraph
 import Data.List(nub)
 import Common.Lib.Graph
 
 import Data.Maybe
-import Proofs.SimpleTheoremHideShift(getInComingGlobalUnprovenEdges)
+--import Proofs.SimpleTheoremHideShift(getInComingGlobalUnprovenEdges)
 
 freenessRule :: DGRule
 freenessRule = DGRule "Freeness"
@@ -116,16 +114,17 @@ handleEdge libEnv dg edge@(m,n,x) = do
                          map (\(y,ly) -> SetNodeLab ly
                                          (y, ly{labelHasHiding = True})) succs
             return $ changesDGH newDG $ labCh
-           _ -> do
-               -- failed in logic lid, look for comorphism and translate
-               -- then recursive call
-              let look = lookupQTA_in_LG $ language_name lid
-              case maybeResult look of
-               Nothing -> return dg
-                  -- can't translate to a logic where qta is implemented
-               Just com -> do
-                (m', dgM) <- translateFree libEnv dg edge com
-                foldM (handleEdge libEnv) dgM $ out (dgBody dgM) m'
+           _ -> return dg
+              --  do
+              --  -- failed in logic lid, look for comorphism and translate
+              --  -- then recursive call
+              -- let look = lookupQTA_in_LG $ language_name lid
+              -- case maybeResult look of
+              --  Nothing -> return dg
+              --     -- can't translate to a logic where qta is implemented
+              --  Just com -> do
+              --   (m', dgM) <- translateFree libEnv dg edge com
+              --   foldM (handleEdge libEnv) dgM $ out (dgBody dgM) m'
      _ -> return dg
 
 descs :: Gr a b -> Node -> [Node]
@@ -143,124 +142,124 @@ descs graph node = let
  in d [node] []
 
 
-translateFree :: LibEnv -> DGraph -> LEdge DGLinkLab -> AnyComorphism ->
-                 Result (Node, DGraph)
-translateFree le dg edge@(m,n,x) com = do
- (m', dg') <- translateNode le dg m (dgn_theory $ labDG dg m) com
- (n', dg'') <- translateNode le dg' n (dgn_theory $ labDG dg n) com
- dg''' <- translateEdge dg'' edge (dgl_morphism x) com m' n'
- return (m', dg''')
+-- translateFree :: LibEnv -> DGraph -> LEdge DGLinkLab -> AnyComorphism ->
+--                  Result (Node, DGraph)
+-- translateFree le dg edge@(m,n,x) com = do
+--  (m', dg') <- translateNode le dg m (dgn_theory $ labDG dg m) com
+--  (n', dg'') <- translateNode le dg' n (dgn_theory $ labDG dg n) com
+--  dg''' <- translateEdge dg'' edge (dgl_morphism x) com m' n'
+--  return (m', dg''')
 
-translateEdge :: DGraph -> LEdge DGLinkLab -> GMorphism -> AnyComorphism ->
-              Node -> Node -> Result DGraph
-translateEdge dg _edge (GMorphism cid _sig _i1 mor1 _i2)
-              (Comorphism cid') m n = do
- let
-  lidS = sourceLogic cid'
-  lidT = targetLogic cid'
- mor2 <- coerceMorphism (targetLogic cid) lidS "" mor1
- mor3 <- map_morphism cid' mor2
- let
-   gm = gEmbed $ mkG_morphism lidT mor3
-   --del = DeleteEdge edge
-   edge' = defDGLink gm
-             (FreeOrCofreeDefLink Free $ EmptyNode $ Logic lidT)  DGLinkProof
-   ins = InsertEdge (m, n, edge')
- return $ changesDGH dg  [ins]
+-- translateEdge :: DGraph -> LEdge DGLinkLab -> GMorphism -> AnyComorphism ->
+--               Node -> Node -> Result DGraph
+-- translateEdge dg _edge (GMorphism cid _sig _i1 mor1 _i2)
+--               (Comorphism cid') m n = do
+--  let
+--   lidS = sourceLogic cid'
+--   lidT = targetLogic cid'
+--  mor2 <- coerceMorphism (targetLogic cid) lidS "" mor1
+--  mor3 <- map_morphism cid' mor2
+--  let
+--    gm = gEmbed $ mkG_morphism lidT mor3
+--    --del = DeleteEdge edge
+--    edge' = defDGLink gm
+--              (FreeOrCofreeDefLink Free $ EmptyNode $ Logic lidT)  DGLinkProof
+--    ins = InsertEdge (m, n, edge')
+--  return $ changesDGH dg  [ins]
 
-translateNode :: LibEnv -> DGraph -> Node -> G_theory -> AnyComorphism ->
-                 Result (Node, DGraph)
-translateNode libEnv dg n s@(G_theory lid sig _ _ _) com@(Comorphism cid) = do
- let
-   m' = getNewNodeDG dg -- new node
-   nodelab = labDG dg n
-   info = nodeInfo nodelab
-   ConsStatus cs _ _ = node_cons_status info
-   lidS = sourceLogic cid
-   lidT = targetLogic cid
- sig' <- coerceSign lid lidS "" sig
- (sig'',sen'') <- wrapMapTheory cid (plainSign sig', [])
- let
-    gth = G_theory lidT (mkExtSign sig'') startSigId
-                  (toThSens sen'') startThId
-    labelM' = newInfoNodeLab
-                  (extName "Freeness" $ dgn_name nodelab)
-                  info
-                  { node_origin = DGNormalForm n
-                  , node_cons_status = mkConsStatus cs }
-                  gth
-    insM' = InsertNode (m', labelM')
- gMor <- gEmbedComorphism com (signOf s)
- let insE = InsertEdge (n,m', globDefLink gMor DGLinkProof)
-     changeLabel = SetNodeLab nodelab
-                  (n, nodelab{dgn_freenf = Just m', dgn_phi = Just gMor})
-     newDG = changesDGH dg [insM', insE, changeLabel]
- return $ (m', changeDGH newDG $ SetNodeLab labelM' (m', labelM'
-              { globalTheory = computeLabelTheory libEnv newDG
-                               (m', labelM') }))
+-- translateNode :: LibEnv -> DGraph -> Node -> G_theory -> AnyComorphism ->
+--                  Result (Node, DGraph)
+-- translateNode libEnv dg n s@(G_theory lid sig _ _ _) com@(Comorphism cid) = do
+--  let
+--    m' = getNewNodeDG dg -- new node
+--    nodelab = labDG dg n
+--    info = nodeInfo nodelab
+--    ConsStatus cs _ _ = node_cons_status info
+--    lidS = sourceLogic cid
+--    lidT = targetLogic cid
+--  sig' <- coerceSign lid lidS "" sig
+--  (sig'',sen'') <- wrapMapTheory cid (plainSign sig', [])
+--  let
+--     gth = G_theory lidT (mkExtSign sig'') startSigId
+--                   (toThSens sen'') startThId
+--     labelM' = newInfoNodeLab
+--                   (extName "Freeness" $ dgn_name nodelab)
+--                   info
+--                   { node_origin = DGNormalForm n
+--                   , node_cons_status = mkConsStatus cs }
+--                   gth
+--     insM' = InsertNode (m', labelM')
+--  gMor <- gEmbedComorphism com (signOf s)
+--  let insE = InsertEdge (n,m', globDefLink gMor DGLinkProof)
+--      changeLabel = SetNodeLab nodelab
+--                   (n, nodelab{dgn_freenf = Just m', dgn_phi = Just gMor})
+--      newDG = changesDGH dg [insM', insE, changeLabel]
+--  return $ (m', changeDGH newDG $ SetNodeLab labelM' (m', labelM'
+--               { globalTheory = computeLabelTheory libEnv newDG
+--                                (m', labelM') }))
 
-thmFreeShift :: DGRule
-thmFreeShift = DGRule "TheoremFreeShift"
+-- thmFreeShift :: DGRule
+-- thmFreeShift = DGRule "TheoremFreeShift"
 
 ------------------------------------------------
 -- Theorem free shift and  auxiliaries
 -- moves theorem links to nodes with incoming free dfn links
 -- to their freeness normal form (must be computed before)
 -----------------------------------------------
 
-theoremFreeShift :: LibName -> LibEnv -> Result LibEnv
-theoremFreeShift ln  = return .
-  Map.adjust (\ dg -> theoremFreeShiftAux (labNodesDG dg) dg) ln
+-- theoremFreeShift :: LibName -> LibEnv -> Result LibEnv
+-- theoremFreeShift ln  = return .
+--   Map.adjust (\ dg -> theoremFreeShiftAux (labNodesDG dg) dg) ln
 
--- | assume that the normal forms a commputed already.
--- return Nothing if nothing changed
-theoremFreeShiftAux :: [LNode DGNodeLab] -> DGraph -> DGraph
-theoremFreeShiftAux  ns dg = let
-  nodesWFree = map fst $ filter
-           (\ (_, lbl) -> labelHasFree lbl && isJust (dgn_freenf lbl)
-           && isJust (dgn_phi lbl)) ns
-     -- all nodes with incoming hiding links
-     -- all the theorem links entering these nodes
-     -- have to replaced by theorem links with the same origin
-     -- but pointing to the normal form of the former target node
-  ingoingEdges = concatMap (getInComingGlobalUnprovenEdges dg) nodesWFree
-  in foldl theoremFreeShiftForEdge
-                              dg ingoingEdges
+-- -- | assume that the normal forms a commputed already.
+-- -- return Nothing if nothing changed
+-- theoremFreeShiftAux :: [LNode DGNodeLab] -> DGraph -> DGraph
+-- theoremFreeShiftAux  ns dg = let
+--   nodesWFree = map fst $ filter
+--            (\ (_, lbl) -> labelHasFree lbl && isJust (dgn_freenf lbl)
+--            && isJust (dgn_phi lbl)) ns
+--      -- all nodes with incoming hiding links
+--      -- all the theorem links entering these nodes
+--      -- have to replaced by theorem links with the same origin
+--      -- but pointing to the normal form of the former target node
+--   ingoingEdges = concatMap (getInComingGlobalUnprovenEdges dg) nodesWFree
+--   in foldl theoremFreeShiftForEdge
+--                               dg ingoingEdges
 
-theoremFreeShiftForEdge :: DGraph -> LEdge DGLinkLab -> DGraph
-theoremFreeShiftForEdge dg edge@(source, target, edgeLab) =
-  case maybeResult $ theoremFreeShiftForEdgeAux dg edge of
-   Nothing -> error "theoremFreeShiftForEdgeAux"
-   Just (dg', pbasis) -> let
-    provenEdge = (source, target, edgeLab
-        { dgl_type = setProof (Proven thmFreeShift pbasis) $ dgl_type edgeLab
-        , dgl_origin = DGLinkProof
-        , dgl_id = defaultEdgeId })
-    in insertDGLEdge provenEdge $ changeDGH dg' $ DeleteEdge edge
+-- theoremFreeShiftForEdge :: DGraph -> LEdge DGLinkLab -> DGraph
+-- theoremFreeShiftForEdge dg edge@(source, target, edgeLab) =
+--   case maybeResult $ theoremFreeShiftForEdgeAux dg edge of
+--    Nothing -> error "theoremFreeShiftForEdgeAux"
+--    Just (dg', pbasis) -> let
+--     provenEdge = (source, target, edgeLab
+--         { dgl_type = setProof (Proven thmFreeShift pbasis) $ dgl_type edgeLab
+--         , dgl_origin = DGLinkProof
+--         , dgl_id = defaultEdgeId })
+--     in insertDGLEdge provenEdge $ changeDGH dg' $ DeleteEdge edge
 
-theoremFreeShiftForEdgeAux :: DGraph -> LEdge DGLinkLab
-                           -> Result (DGraph, ProofBasis)
-theoremFreeShiftForEdgeAux dg (sn, tn, llab) = do
-  let tlab = labDG dg tn
-      Just nfNode = dgn_freenf tlab
-      phi = dgl_morphism llab
-      Just muN = dgn_phi tlab
-  let cmor1  = composeMorphisms phi muN
-  case maybeResult cmor1 of
-   Nothing -> error "composition"
-   Just cmor -> do
-    let newEdge =(sn, nfNode, defDGLink cmor globalThm DGLinkProof)
-    case tryToGetEdge newEdge dg of
-          Nothing -> let
-           newGraph = changeDGH dg $ InsertEdge newEdge
-           finalEdge = case getLastChange newGraph of
-             InsertEdge final_e -> final_e
-             _ -> error "Proofs.Global.globDecompForOneEdgeAux"
-           in return
-              (newGraph, addEdgeId emptyProofBasis $ getEdgeId finalEdge)
-          Just e -> return (dg, addEdgeId emptyProofBasis $ getEdgeId e)
+-- theoremFreeShiftForEdgeAux :: DGraph -> LEdge DGLinkLab
+--                            -> Result (DGraph, ProofBasis)
+-- theoremFreeShiftForEdgeAux dg (sn, tn, llab) = do
+--   let tlab = labDG dg tn
+--       Just nfNode = dgn_freenf tlab
+--       phi = dgl_morphism llab
+--       Just muN = dgn_phi tlab
+--   let cmor1  = composeMorphisms phi muN
+--   case maybeResult cmor1 of
+--    Nothing -> error "composition"
+--    Just cmor -> do
+--     let newEdge =(sn, nfNode, defDGLink cmor globalThm DGLinkProof)
+--     case tryToGetEdge newEdge dg of
+--           Nothing -> let
+--            newGraph = changeDGH dg $ InsertEdge newEdge
+--            finalEdge = case getLastChange newGraph of
+--              InsertEdge final_e -> final_e
+--              _ -> error "Proofs.Global.globDecompForOneEdgeAux"
+--            in return
+--               (newGraph, addEdgeId emptyProofBasis $ getEdgeId finalEdge)
+--           Just e -> return (dg, addEdgeId emptyProofBasis $ getEdgeId e)
 
-theoremFreeShiftFromList :: LibName -> [LNode DGNodeLab] -> LibEnv
-                         -> Result LibEnv
-theoremFreeShiftFromList ln ls =
-  return . Map.adjust (theoremFreeShiftAux ls) ln
+-- theoremFreeShiftFromList :: LibName -> [LNode DGNodeLab] -> LibEnv
+--                          -> Result LibEnv
+-- theoremFreeShiftFromList ln ls =
+--   return . Map.adjust (theoremFreeShiftAux ls) ln
diff --git a/doc/UserGuide.tex b/doc/UserGuide.tex
@@ -1899,7 +1899,7 @@ \section{Architecture of Hets}
 Besides the authors, the following people have been involved
 in the implementation of \Hets:
 Katja Abu-Dib,
-Liliana Codruta,
+Codru\c ta G\^ arlea,
 Dominik Dietrich,
 Elena Digor,
 Carsten Fischer,