Changeset 12757

Timestamp:

30.10.2009 10:41:42 (3 weeks ago)

Author:

maeder

Message:

re-ordered and renamed generated axioms

Files:

• trunk/Comorphisms/CASL2PCFOL.hs (modified) (4 diffs)

trunk/Comorphisms/CASL2PCFOL.hs

@@ -108 +108 @@
 -- | Make the name for the projection injectivity axiom
 mkProjInjName :: SORT -> SORT -> String
-mkProjInjName s s' = mkInjectivityName "projection" s' s
+mkProjInjName = mkInjectivityName "projection"
 
 -- | create a quantified injectivity implication
@@ -138 +138 @@
 mkProjInjAxiom :: SORT -> SORT -> Named (FORMULA ())
 mkProjInjAxiom s s' =
-    makeNamed (mkProjInjName s s')
+    makeNamed (mkProjInjName s' s)
       $ mkInjectivity (projectTo s) (mkVarDeclStr "x" s') $ mkVarDeclStr "y" s'
 
@@ -155 +155 @@
 --   i.e., forall x:s . pr(inj(x))=e=x
 mkProjAxiom:: SORT -> SORT -> Named (FORMULA ())
-mkProjAxiom s s' = makeNamed (mkProjName s s')
+mkProjAxiom s s' = makeNamed (mkProjName s' s)
     $ mkXExEq s (projectTo s . injectTo s') id
 
@@ -180 +180 @@
 
 generateAxioms :: Sign f e -> [Named (FORMULA ())]
-generateAxioms sig = concat
-    $ [[mkEmbInjAxiom s s'] ++ [mkProjInjAxiom s s'] ++ [mkProjAxiom s s']
-      | s <- sorts,
-        s' <- realSupers s]
-    ++ [[mkTransAxiom s s' s'']
-          | s <- sorts,
-            s' <- realSupers s,
-            s'' <- realSupers s',
-            s'' /= s]
-    ++ [[mkIdAxiom s s']
-          | s <- sorts,
-            s' <- realSupers s,
-            Set.member s $ supersortsOf s' sig]
+generateAxioms sig = concatMap (\ s ->
+    concatMap (\ s' ->
+      [mkIdAxiom s s' | Set.member s $ supersortsOf s' sig ]
+      ++ mkEmbInjAxiom s s' : mkProjInjAxiom s s' : mkProjAxiom s s'
+      : map (mkTransAxiom  s s') (realSupers s'))
+    $ realSupers s) $ Set.toList $ sortSet sig
     where
         realSupers so = Set.toList $ supersortsOf so sig
-        sorts = Set.toList $ sortSet sig
 
 f2Formula :: FORMULA f -> FORMULA f