Changeset 12811

Timestamp:

09.11.2009 18:34:06 (4 months ago)

Author:

csliam

Message:

fixed bug with sort name, and axiom name conversion to Isabelle where
the special characters like square brackets were not encoded properly.

Location:

trunk/CspCASLProver

Files:

• Consts.hs (modified) (2 diffs)
• Utils.hs (modified) (4 diffs)

trunk/CspCASLProver/Consts.hs

@@ -68 +68 @@
 import Isabelle.IsaConsts (binVNameAppl, conDouble, mkFunType, termAppl)
 import Isabelle.IsaSign (BaseSig(..), Term, Typ(..), VName(..))
-import Isabelle.Translate(showIsaTypeT)
+import Isabelle.Translate(showIsaTypeT, transString)
 
 -- | Name for the CspCASLProver's Alphabet
@@ -110 +110 @@
 -- | Convert a SORT to a string
 convertSort2String :: SORT -> String
-convertSort2String s = showIsaTypeT s Main_thy
+convertSort2String s = transString $ showIsaTypeT s Main_thy
 
 -- | Convert a process name to a string

trunk/CspCASLProver/Utils.hs

@@ -60 +60 @@
 import Isabelle.IsaConsts
 import Isabelle.IsaSign
+import Isabelle.Translate(transString)
 
 -------------------------------------------------------------------------
@@ -784 +785 @@
 getCollectionEmbInjAx :: [(SORT,SORT)] -> [String]
 getCollectionEmbInjAx sortRel =
-    let mkName (s,s') = mkEmbInjName s s'
+    let mkName (s,s') = transString $ mkEmbInjName s s'
     in map mkName sortRel
 
 -- | Return the list of strings of all ga_notDefBottom axioms.
 getCollectionNotDefBotAx :: [SORT] -> [String]
-getCollectionNotDefBotAx = map mkNotDefBotAxiomName
+getCollectionNotDefBotAx = map $ transString . mkNotDefBotAxiomName
 
 -- | Return the list of string of all decomposition theorem names that we
@@ -825 +826 @@
             (Set.member s' $ CASLSign.supersortsOf s caslSign) &&
             (Set.member s'' $ CASLSign.supersortsOf s' caslSign) && (s /= s'')
-    in [mkTransAxiomName s s' s''
+    in [transString $ mkTransAxiomName s s' s''
             | s <- sorts, s' <- sorts, s'' <- sorts, allSupers s s' s'']
 
@@ -835 +836 @@
         isomorphic s s' = (Set.member s $ CASLSign.supersortsOf s' caslSign) &&
                           (Set.member s' $ CASLSign.supersortsOf s caslSign)
-    in [mkIdAxiomName s s' | s <- sorts, s' <- sorts, isomorphic s s']
+    in [transString $ mkIdAxiomName s s'
+            | s <- sorts, s' <- sorts, isomorphic s s']