Changeset 12761

Timestamp:

30.10.2009 15:28:02 (3 weeks ago)

Author:

maeder

Message:

use different names

Files:

• trunk/Comorphisms/CASL2SubCFOL.hs (modified) (5 diffs)

trunk/Comorphisms/CASL2SubCFOL.hs

@@ -218 +218 @@
       df z = defined bsorts z nullRange
       in concatMap (\ s' ->
-      [makeNamed (mkAxName "projection_injectivity" s' s)
+      [makeNamed (mkAxName "total_projection_injectivity" s' s)
       $ let xv = mkVarDeclStr "x" s'
             yv = mkVarDeclStr "y" s'
@@ -232 +232 @@
            nullRange
             -- forall x:s . d(x) => pr(x)=x
-      , makeNamed (mkAxName "projection" s' s)
+      , makeNamed (mkAxName "total_projection" s' s)
       $ let eq = mkStEq (prj $ Sorted_term xt s' nullRange) xt
         in mkForall [vx]
@@ -243 +243 @@
       ++ [makeNamed ("ga_notDefBottom_" ++ show s)
          $ let bty = toOP_TYPE $ botType s
-               bt = mkAppl (Qual_op_name (uniqueBotName bty) bty nullRange) []
+               bt = mkAppl (mkQualOp (uniqueBotName bty) bty) []
            in if uniqBot then
               -- forall x:s . not d(x) <=> x=bottom
               mkForall [vx]
-              (mkEqv (Negation (df xt) nullRange)
-               $ mkStEq xt bt) nullRange
-              else Negation (df bt) nullRange -- not d(bottom)
+              (mkEqv (mkNeg $ df xt) $ mkStEq xt bt) nullRange
+              else mkNeg $ df bt -- not d(bottom)
          | hasBot]) sortList
    ++ filter (not . is_True_atom . sentence)
@@ -260 +259 @@
          $ mkForall vs
            ((if opKind typ == Total then mkEqv else mkImpl)
-            (defined bsorts (mkAppl (Qual_op_name f (toOP_TYPE typ) nullRange)
+            (defined bsorts (mkAppl (mkQualOp f $ toOP_TYPE typ)
                       $ map toQualVar vs) nullRange)
             $ defVards bsorts vs) nullRange) opList
@@ -274 +273 @@
             $ defVards bsorts vs) nullRange) predList)
     where
+        mkQualOp f ty = Qual_op_name f ty nullRange
+        mkNeg f = Negation f nullRange
         minSupers so = keepMinimals sig id $ Set.toList $ Set.delete so
                            $ supersortsOf so sig