Changeset 11215 for trunk/CspCASL/Trans_CspProver.hs

Timestamp:

05.01.2009 15:46:06 (11 months ago)

Author:

csliam

Message:

Large commit - improved static analysis of cspcasl and translation of cspcasl to isabelle

Files:

• trunk/CspCASL/Trans_CspProver.hs (modified) (5 diffs)

trunk/CspCASL/Trans_CspProver.hs

@@ -15 +15 @@
 module CspCASL.Trans_CspProver where
 
-import CASL.AS_Basic_CASL (SORT, VAR)
+import qualified CASL.AS_Basic_CASL as CASL_AS_Basic_CASL
+import qualified CASL.Fold as CASL_Fold
+import qualified CASL.Sign as CASL_Sign
 
 import Common.Id
+
+import qualified Comorphisms.CFOL2IsabelleHOL as CFOL2IsabelleHOL
 
 import CspCASL.AS_CspCASL_Process
@@ -26 +30 @@
 import Isabelle.IsaConsts
 
-transProcess :: PROCESS -> Term
-transProcess pr = case pr of
+transProcess :: CASL_Sign.Sign () () -> PROCESS -> Term
+transProcess caslSign pr = case pr of
     -- precedence 0
     Skip _ -> cspProver_skipOp
@@ -41 +45 @@
     -- precedence 1
     ConditionalProcess _ p q _ ->
-        cspProver_conditionalOp true (transProcess p) (transProcess q)
+        cspProver_conditionalOp true (transProcess caslSign p)
+                                     (transProcess caslSign q)
     -- precedence 2
     Hiding p es _ ->
-        cspProver_hidingOp (transProcess p) (transEventSet es)
+        cspProver_hidingOp (transProcess caslSign p) (transEventSet es)
     RenamingProcess p r _ ->
-        cspProver_renamingOp (transProcess p) (transRenaming r)
+        cspProver_renamingOp (transProcess caslSign p) (transRenaming r)
     -- precedence 3
     Sequential p q _ ->
-        cspProver_sequenceOp (transProcess p) (transProcess q)
+        cspProver_sequenceOp (transProcess caslSign p) (transProcess caslSign q)
     PrefixProcess ev p _ ->
-        cspProver_action_prefixOp (transEvent ev) (transProcess p)
+        cspProver_action_prefixOp (transEvent caslSign ev)
+                                  (transProcess caslSign p)
     InternalPrefixProcess v s p _ ->
         cspProver_internal_prefix_choiceOp (transVar v)
                                            (transSort s)
-                                           (transProcess p)
+                                           (transProcess caslSign p)
     ExternalPrefixProcess v s p _ ->
         cspProver_external_prefix_choiceOp (transVar v)
                                            (transSort s)
-                                           (transProcess p)
+                                           (transProcess caslSign p)
     -- precedence 4
     InternalChoice p q _ ->
-        cspProver_internal_choiceOp (transProcess p) (transProcess q)
+        cspProver_internal_choiceOp (transProcess caslSign p)
+                                    (transProcess caslSign q)
     ExternalChoice p q _ ->
-        cspProver_external_choiceOp (transProcess p) (transProcess q)
+        cspProver_external_choiceOp (transProcess caslSign p)
+                                    (transProcess caslSign q)
     -- precedence 5
     Interleaving p q _ ->
-        cspProver_interleavingOp (transProcess p) (transProcess q)
+        cspProver_interleavingOp (transProcess caslSign p)
+                                 (transProcess caslSign q)
     SynchronousParallel p q _ ->
-        cspProver_synchronousOp (transProcess p) (transProcess q)
+        cspProver_synchronousOp (transProcess caslSign p)
+                                (transProcess caslSign q)
     GeneralisedParallel p es q _ ->
-        cspProver_general_parallelOp (transProcess p)
+        cspProver_general_parallelOp (transProcess caslSign p)
                                      (transEventSet es)
-                                     (transProcess q)
+                                     (transProcess caslSign q)
 
     AlphabetisedParallel p les res q _ ->
-        cspProver_alphabetised_parallelOp (transProcess p)
+        cspProver_alphabetised_parallelOp (transProcess caslSign p)
                                           (transEventSet les)
                                           (transEventSet res)
-                                          (transProcess q)
+                                          (transProcess caslSign q)
+    -- BUG not done right yet
+    FQProcess p _ _ ->
+        transProcess caslSign p
 
 transEventSet :: EVENT_SET -> Term
@@ -88 +101 @@
          EventSet commTypes _ -> Set $ FixedSet $ map tranCommType commTypes
 
-transEvent :: EVENT -> Term
-transEvent ev =
+transEvent :: CASL_Sign.Sign () () -> EVENT -> Term
+transEvent caslSign ev =
     case ev of
-      TermEvent _caslTerm _ -> conDouble "not yet done"
-      ChanSend _ _ _ -> conDouble "not yet done"
-      ChanNonDetSend _ _ _ _ -> conDouble "not yet done"
-      ChanRecv _ _ _ _ -> conDouble "not yet done"
+      TermEvent caslTerm _ -> transTerm_with_class caslSign caslTerm
+      ChanSend _ _ _ -> conDouble "ChanSendNotYetDone"
+      ChanNonDetSend _ _ _ _ -> conDouble "ChanNonDetSendNotYetDone"
+      ChanRecv _ _ _ _ -> conDouble "ChanRecvNotYetDone"
 
-transVar :: VAR -> Term
+transVar :: CASL_AS_Basic_CASL.VAR -> Term
 transVar v = conDouble $ tokStr v
 
-transSort :: SORT -> Term
+transSort :: CASL_AS_Basic_CASL.SORT -> Term
 transSort sort = let sortBarString = convertSort2String sort ++ barExtS
                  in conDouble  sortBarString
@@ -105 +118 @@
 transRenaming :: RENAMING -> Term
 transRenaming _ = conDouble "not yet done"
+
+
+
+-- BUG - I dont think these functions are correct
+transTerm_with_class :: CASL_Sign.Sign () () -> CASL_AS_Basic_CASL.TERM () ->
+                        Term
+transTerm_with_class caslSign caslTerm =
+    case caslTerm of
+      -- if the term is just a variable then we just translate the
+      -- variable to isabelle
+      CASL_AS_Basic_CASL.Qual_var _ _ _ -> transCaslTerm caslSign caslTerm
+      -- otherwise we add a classOp around it and translate the inside of
+      -- it with the translator that adds a chooseOp
+      _ -> classOp (transTerm_with_choose caslSign caslTerm)
+
+transTerm_with_choose :: CASL_Sign.Sign () () -> CASL_AS_Basic_CASL.TERM () ->
+                        Term
+transTerm_with_choose caslSign caslTerm =
+    case caslTerm of
+      -- if the term is just a variable then we need to apply the choose
+      -- function
+      CASL_AS_Basic_CASL.Qual_var _ _ _ -> termAppl (conDouble "choose")
+                                 (transCaslTerm caslSign caslTerm)
+      -- otherwise we just translate it to Isabelle
+      _ -> transCaslTerm caslSign caslTerm
+
+-- | Translate a CASL Term to an Isabelle Term using the exact
+--   translation as is done in the comorphism composition
+--   CASL2PCFOL;defaultCASL2SubCFOL;CFOL2IsabelleHOL
+transCaslTerm :: CASL_Sign.Sign () () -> CASL_AS_Basic_CASL.TERM () -> Term
+transCaslTerm caslSign caslTerm =
+    let tyToks = CFOL2IsabelleHOL.typeToks caslSign
+        trForm = CFOL2IsabelleHOL.formTrCASL
+        strs = CFOL2IsabelleHOL.getAssumpsToks caslSign
+    in CASL_Fold.foldTerm (CFOL2IsabelleHOL.transRecord
+                                           caslSign tyToks trForm strs) caslTerm
+
+
+-- My own version of transRecord
+-- transRecord_Term :: CASL.Sign.Sign f e -> Set.Set String -> FormulaTranslator f e
+--             -> Set.Set String -> Record f Term Term
+-- transRecord_Term sign tyToks tr toks = Record
+--     { foldSimpleId = error "transRecord_Term: Simple_id"
+--     , foldQual_var = \ _ v _ _ -> mkFree $ transVar toks v
+--     , foldApplication = \ _ opsymb args _ ->
+--           foldl termAppl (con $ transOP_SYMB sign tyToks opsymb) args
+--     , foldSorted_term = \ _ t _ _ -> t -- no subsorting assumed
+--     , foldCast = \ _ t _ _ -> t -- no subsorting assumed
+--     , foldConditional = \ _  t1 phi t2 _ -> -- equal types assumed
+--           If phi t1 t2 NotCont
+--     , foldMixfix_qual_pred = error "transRecord_Term: Mixfix_qual_pred"
+--     , foldMixfix_term = error "transRecord_Term: Mixfix_term"
+--     , foldMixfix_token = error "transRecord_Term: Mixfix_token"
+--     , foldMixfix_sorted_term = error "transRecord_Term: Mixfix_sorted_term"
+--     , foldMixfix_cast = error "transRecord_Term: Mixfix_cast"
+--     , foldMixfix_parenthesized = error "transRecord_Term: Mixfix_parenthesized"
+--     , foldMixfix_bracketed = error "transRecord_Term: Mixfix_bracketed"
+--     , foldMixfix_braced = error "transRecord_Term: Mixfix_braced"
+--     }
+
+-- transVar :: Set.Set String -> VAR -> String
+-- transVar toks v = let
+--     s = showIsaConstT (simpleIdToId v) baseSign
+--     renVar t = if Set.member t toks then renVar $ "X_" ++ t else t
+--     in renVar s
+