Changeset 12741

Timestamp:

27.10.2009 15:36:41 (4 weeks ago)

Author:

mcodescu

Message:

removed node M'

Location:

trunk

Files:

• CASL/Freeness.hs (modified) (3 diffs)
• Logic/Logic.hs (modified) (1 diff)
• Proofs/NormalForm.hs (modified) (4 diffs)

trunk/CASL/Freeness.hs

@@ -37 +37 @@
                     -> [Named CASLFORMULA] -- Th(M)
                     -> Result (CASLSign, -- SigmaK
-                               CASLMor, -- iota : SigmaM' -> SigmaK
+                               -- CASLMor, -- iota : SigmaM' -> SigmaK
                                [Named CASLFORMULA] -- Ax(K)
                               )
@@ -46 +46 @@
                     ss_0 = sortSet sigma_0
                     sigma_m = mtarget sigma
-                    iota_mor = create_iota_mor ss_0 sigma_m
-                    sigma_k = mtarget iota_mor
+                    sigma_k = create_sigma_k ss_0 sigma_m
                     axs = create_axs ss_0 sigma_m sigma_k sens
-                  in return (sigma_k, iota_mor, axs)
+                  in return (sigma_k, axs)
 
 horn_clauses :: [Named CASLFORMULA] -> Bool
@@ -496 +495 @@
                        showSepList (showString "_") showId sortList "") f
 
--- | given the signature in M the function computes the morphism from M' to K
-create_iota_mor :: Set.Set SORT -> CASLSign -> CASLMor
-create_iota_mor ss sg_m = Morphism iota_sg usg' sm om pm ()
+-- | given the signature in M the function computes the signature K
+create_sigma_k :: Set.Set SORT -> CASLSign -> CASLSign
+create_sigma_k ss sg_m = usg'
       where iota_sg = totalSignCopy sg_m
             usg = addSig const sg_m iota_sg
-            sm = iota_sort_map_mor $ sortSet sg_m
-            om = iota_op_map_mor $ opMap sg_m
-            pm = iota_pred_map_mor $ predMap sg_m
             om' = homomorphism_ops (sortSet sg_m) (opMap usg)
             om'' = make_ops ss om'

trunk/Logic/Logic.hs

@@ -361 +361 @@
              -> Result
                  (sign, -- SigmaK
-                  morphism, -- iota : SigmaM' -> SigmaK
                   [Named sentence] -- Ax(K)
                  )

trunk/Proofs/NormalForm.hs

@@ -265 +265 @@
           let res = quotient_term_algebra lid mor $ toNamedList sen
           case maybeResult res of
-           Just (sigK, iota, axK) -> do
+           Just (sigK, axK) -> do
                -- success in logic lid
             let thK = G_theory lid (makeExtSign lid sigK)
                              startSigId (toThSens axK) startThId
-            let thM' = noSensGTheory lid sig startSigId
-                iotaM' = gEmbed $ mkG_morphism lid iota
             incl <- subsig_inclusion lid (plainSign sig) sigK
             let inclM = gEmbed $ mkG_morphism lid incl
-      -- m' with signature = sig, no sentences
       -- remove x
       -- add nodes
       -- k  with signature = sigK, sentences axK
-      -- global def links from m and m' to k, mapped with incl, resp iota
+      -- global def link from m to k, labeled with inclusion
       -- hiding def link from k to n, labeled with inclusion
-                m' = getNewNodeDG dg -- new node
+              --   m' = getNewNodeDG dg -- new node
                 nodelab = labDG dg m
                 info = nodeInfo nodelab
                 ConsStatus c _ _ = node_cons_status info
-                labelM' = newInfoNodeLab
-                  (extName "NormalForm" $ dgn_name nodelab)
-                  info
-                  { node_origin = DGNormalForm m
-                  , node_cons_status = mkConsStatus c }
-                  thM'
-            -- insert the new node and add edges from the predecessors
-                insM' = InsertNode (m', labelM')
-                k = (getNewNodeDG dg) + 1
+                k = (getNewNodeDG dg)
                 labelK = newInfoNodeLab
                    (extName "NormalForm" $ dgn_name nodelab)
@@ -304 +293 @@
                                                , dgl_id = defaultEdgeId
                                                }),
-                       InsertEdge (m',k,DGLink { dgl_morphism = iotaM'
-                                              , dgl_type = globalDef
-                                              , dgl_origin = DGLinkProof
-                                              , dgl_id = defaultEdgeId
-                                              }),
                        InsertEdge (k, n,DGLink { dgl_morphism = inclM
                                               , dgl_type = HidingDefLink
@@ -315 +299 @@
                                               })]
                 del = DeleteEdge edge
-                allChanges = del:insM' : insK : insE
+                allChanges = del: insK : insE
             return $ changesDGH dg allChanges
            _ -> do
@@ -327 +311 @@
                 (m', dgM) <- translateFree dg edge com
                 foldM handleEdge dgM $ out (dgBody dgM) m'
-                --return dgM
      _ -> return dg