Changeset 11216

Timestamp:

06.01.2009 16:49:44 (10 months ago)

Author:

maeder

Message:

extended symbol kinds i.e. for CspCASL

Location:

trunk

Files:

• CASL/AS_Basic_CASL.der.hs (modified) (1 diff)
• CASL/Sign.hs (modified) (1 diff)
• Comorphisms/CASL2CspCASL.hs (modified) (1 diff)
• Comorphisms/CspCASL2IsabelleHOL.hs (modified) (2 diffs)
• Comorphisms/CspCASL2Modal.hs (modified) (2 diffs)
• CspCASL/Logic_CspCASL.hs (modified) (3 diffs)
• CspCASL/StatAnaCSP.hs (modified) (2 diffs)

trunk/CASL/AS_Basic_CASL.der.hs

@@ -323 +323 @@
 
 data SYMB_KIND = Implicit | Sorts_kind
-               | Ops_kind | Preds_kind
+               | Ops_kind | Preds_kind | OtherKinds String
                  deriving (Show, Eq, Ord)
 

trunk/CASL/Sign.hs

@@ -40 +40 @@
 
 data SymbType = SortAsItemType
+              | OtherTypeKind String
               | OpAsItemType OpType
                 -- since symbols do not speak about totality, the totality
                 -- information in OpType has to be ignored
               | PredAsItemType PredType
-                deriving Show
-
--- Ordering and equality of symbol types has to ingore totality information
-instance Ord SymbType where
-  compare st1 st2 = case (st1, st2) of
-    (SortAsItemType, SortAsItemType) -> EQ
-    (SortAsItemType, _) -> LT
-    (OpAsItemType ot1, OpAsItemType ot2) ->
-      compare (opArgs ot1, opRes ot1) (opArgs ot2, opRes ot2)
-    (OpAsItemType _, SortAsItemType) -> GT
-    (OpAsItemType _, PredAsItemType _) -> LT
-    (PredAsItemType pt1, PredAsItemType pt2) -> compare pt1 pt2
-    (PredAsItemType _, _) -> GT
-
-instance Eq SymbType where
-  t1 == t2 = compare t1 t2 == EQ
+                deriving (Show, Eq, Ord)
 
 data Symbol = Symbol {symName :: Id, symbType :: SymbType}

trunk/Comorphisms/CASL2CspCASL.hs

@@ -44 +44 @@
                CspCASLSign
                CspMorphism
-               () () () where
+               Symbol RawSymbol () where
     sourceLogic CASL2CspCASL = CASL
     sourceSublogic CASL2CspCASL = SL.top

trunk/Comorphisms/CspCASL2IsabelleHOL.hs

@@ -18 +18 @@
 
 import CASL.AS_Basic_CASL
+import CASL.Sign (Symbol)
+import CASL.Morphism (RawSymbol)
 import qualified CASL.Inject as CASLInject
 import qualified CASL.Sign as CASLSign
@@ -53 +55 @@
                CspCASLSign
                CspMorphism
-               () () ()
+               Symbol RawSymbol ()
                Isabelle () () IsaSign.Sentence () ()
                IsaSign.Sign

trunk/Comorphisms/CspCASL2Modal.hs

@@ -45 +45 @@
                CspCASLSign
                CspMorphism
-               () () ()
+               Symbol RawSymbol ()
                Modal ()
                M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
@@ -77 +77 @@
 
 
-mapSym :: () -> Symbol
+mapSym :: Symbol -> Symbol
 mapSym = error "CspCASL2Modal.mapSym not yet implemented"
    -- needs to be changed once modal symbols are added

trunk/CspCASL/Logic_CspCASL.hs

@@ -75 +75 @@
     SignCSP.CspCASLSign     -- signature
     SignCSP.CspMorphism     -- morphism
-    ()                      -- symbol (?)
+    Symbol               -- symbol
     where
       parse_sentence CspCASL = Nothing
@@ -107 +107 @@
     SignCSP.CspCASLSign         -- signature
     SignCSP.CspMorphism     -- morphism
-    ()                      -- symbol (missing)
-    ()                      -- raw_symbol (missing)
+    Symbol
+    RawSymbol
     ()                      -- proof_tree (missing)
     where
@@ -123 +123 @@
     SignCSP.CspCASLSign         -- signature
     SignCSP.CspMorphism     -- morphism
-    ()                      -- symbol (missing)
-    ()                      -- raw_symbol (missing)
+    Symbol
+    RawSymbol
     where
       basic_analysis CspCASL =

trunk/CspCASL/StatAnaCSP.hs

@@ -30 +30 @@
 import CASL.Overload (minExpFORMULA, oneExpTerm)
 import CASL.Sign
+import CASL.Morphism (RawSymbol)
 import CASL.StaticAna (allOpIds, allPredIds)
 import Common.AS_Annotation
@@ -49 +50 @@
 
 basicAnalysisCspCASL :: (CspBasicSpec, CspCASLSign, GlobalAnnos)
-        -> Result (CspBasicSpec, ExtSign CspCASLSign (),
+        -> Result (CspBasicSpec, ExtSign CspCASLSign Symbol,
                    [Named CspCASLSen])
 basicAnalysisCspCASL (cc, sigma, ga) =