Rigid casl

CASL/Formula.hs

@@ -61,6 +61,8 @@ module CASL.Formula
     , qualPredName
     , implKey
     , ifKey
+    , orKey
+    , andKey
     ) where
 
 import Common.AnnoState

CASL/Logic_CASL.hs

@@ -47,7 +47,7 @@ import CASL.OMDocExport
 import CASL.Freeness
 
 -- test
-import CASL.Formula (formula)
+import CASL.Formula (formula, primFormula)
 
 #ifdef UNI_PACKAGE
 import CASL.QuickCheck
@@ -225,10 +225,13 @@ instance Sentences CASL CASLFORMULA CASLSign CASLMor Symbol where
       symmap_of CASL = morphismToSymbMap
       sym_name CASL = symName
       symKind CASL = show . pretty . symbolKind . symbType
+      extSymKind CASL = extSymbolKind . symbType
       symsOfSen CASL _ = Set.toList
         . foldFormula (symbolsRecord $ const Set.empty)
       simplify_sen CASL = simplifyCASLSen
       print_named CASL = printTheoryFormula
+      -- test nominals
+      is_nominal_sen CASL = isNominalSen 
 
 instance StaticAnalysis CASL CASLBasicSpec CASLFORMULA
                SYMB_ITEMS SYMB_MAP_ITEMS
@@ -237,6 +240,7 @@ instance StaticAnalysis CASL CASLBasicSpec CASLFORMULA
                Symbol RawSymbol where
          basic_analysis CASL = Just basicCASLAnalysis
          sen_analysis CASL = Just cASLsen_analysis
+         convertTheory CASL = Just convertCASLTheory
          stat_symb_map_items CASL = statSymbMapItems
          stat_symb_items CASL = statSymbItems
          signature_colimit CASL diag = return $ signColimit diag extCASLColimit
@@ -246,13 +250,16 @@ instance StaticAnalysis CASL CASLBasicSpec CASLFORMULA
 
          qualify CASL = qualifySig
          symbol_to_raw CASL = symbolToRaw
+         raw_to_symbol CASL = rawToSymbol
          id_to_raw CASL = idToRaw
          matches CASL = CASL.Morphism.matches
          is_transportable CASL = isSortInjective
          is_injective CASL = isInjective
+         raw_to_var CASL = rawToVar 
 
          empty_signature CASL = emptySign ()
          add_symb_to_sign CASL = addSymbToSign
+         add_noms_to_sign CASL = addNomsToSign
 
          signature_union CASL s = return . addSig const s
          signatureDiff CASL s = return . diffSig const s
@@ -275,6 +282,7 @@ instance Logic CASL CASL_Sublogics
          stability CASL = Stable
          -- for Hybridization
          parse_basic_sen CASL = Just $ \ _ -> formula []
+         parse_prim_formula CASL = Just $ const (primFormula [])
 
          proj_sublogic_epsilon CASL = pr_epsilon ()
          all_sublogics CASL = sublogics_all []
@@ -292,6 +300,20 @@ instance Logic CASL CASL_Sublogics
          addOMadtToTheory CASL = OMI.addOMadtToTheory
          addOmdocToTheory CASL = OMI.addOmdocToTheory
          syntaxTable CASL = Just . getSyntaxTable
+         constr_to_sens CASL = constrToSens
+         -- helpers for hybridization
+           -- for each type, its name and the file where it is defined
+         sublogicsTypeName CASL = ("CASL_Sublogics","CASL.Sublogic")
+         basicSpecTypeName CASL = ("CASLBasicSpec","CASL.Logic_CASL")
+         sentenceTypeName CASL = ("CASLFORMULA","CASL.AS_Basic_CASL")
+         symbItemsTypeName CASL = ("SYMB_ITEMS","CASL.AS_Basic_CASL")
+         symbMapItemsTypeName CASL = ("SYMB_MAP_ITEMS","CASL.AS_Basic_CASL")
+         signTypeName CASL = ("CASLSign","CASL.Sign")
+         morphismTypeName CASL = ("CASLMor","CASL.Morphism")
+         symbolTypeName CASL = ("Symbol","")
+         rawSymbolTypeName CASL = ("RawSymbol","CASL.Morphism")
+         proofTreeTypeName CASL = ("ProofTree","Common.ProofTree") 
+
 #ifdef UNI_PACKAGE
          provers CASL = [quickCheckProver]
 #endif

CASL/Morphism.hs

@@ -49,6 +49,8 @@ module CASL.Morphism
   , idToRaw
   , typedSymbKindToRaw
   , symbolToRaw
+  , rawToSymbol
+  , rawToVar
   , insertRsys
   , mapSort
   , mapOpSym
@@ -208,6 +210,17 @@ mapCASLMor e me m =
 symbolToRaw :: Symbol -> RawSymbol
 symbolToRaw = ASymbol
 
+rawToSymbol :: RawSymbol -> Maybe Symbol
+rawToSymbol (ASymbol s) = Just s
+rawToSymbol (AKindedSymb k i) = 
+   case k of
+    Sorts_kind -> Just $ Symbol i SortAsItemType
+    _ -> Nothing 
+
+rawToVar :: RawSymbol -> Maybe (Token, Id)
+rawToVar (ASymbol (Symbol n (OpAsItemType (OpType Total [] s)))) = Just (idToSimpleId n, s)
+rawToVar _ = Nothing
+
 idToRaw :: Id -> RawSymbol
 idToRaw = AKindedSymb Implicit
 

CASL/Sign.hs

@@ -34,7 +34,7 @@ import Common.DocUtils
 import Data.Data
 import Data.Maybe (fromMaybe)
 import Data.List (isPrefixOf)
-import Control.Monad (when, unless)
+import Control.Monad (when, unless, foldM)
 
 -- constants have empty argument lists
 data OpType = OpType {opKind :: OpKind, opArgs :: [SORT], opRes :: SORT}
@@ -81,6 +81,15 @@ symbolKind t = case t of
   PredAsItemType _ -> Preds_kind
   _ -> Sorts_kind
 
+extSymbolKind :: SymbType -> String
+extSymbolKind t = case t of 
+  OpAsItemType (OpType k l _) -> 
+     case (k, l) of 
+      (Total, []) -> "const"
+      _ -> "op"
+  PredAsItemType _ -> "pred"
+  _ -> "sort"
+
 data Symbol = Symbol {symName :: Id, symbType :: SymbType}
               deriving (Show, Eq, Ord, Typeable, Data)
 
@@ -591,8 +600,16 @@ addSymbToSign sig sy =
         PredAsItemType pt -> return $ addPred' sig' n pt
         OpAsItemType ot -> return $ addOp' sig' n ot
 
+addNomsToSign :: Sign e f -> Set.Set Id -> Result (Sign e f)
+addNomsToSign sig noms = do 
+ -- add a fake sort for nominals
+ sig0 <- addSymbToSign sig $ Symbol (genName "ST") SortAsItemType
+ sig' <- foldM (\aSig nom -> addSymbToSign aSig $ Symbol nom $ 
+                              PredAsItemType $ PredType []) 
+         sig0 $ Set.toList noms
+ return sig'
 
--- The function below belong in a different file. But I put them here for now.
+-- TODO: The function below belong in a different file. But I put them here for now.
 -- dual of a quantifier
 
 dualQuant :: QUANTIFIER -> QUANTIFIER

CASL/StaticAna.hs

@@ -54,6 +54,8 @@ import qualified Data.Set as Set
 import Data.Maybe
 import Data.List
 
+import Logic.SemConstr
+
 checkPlaces :: [SORT] -> Id -> [Diagnosis]
 checkPlaces args i = let n = placeCount i in
     [mkDiag Error "wrong number of places" i | n > 0 && n /= length args ]
@@ -869,6 +871,14 @@ anaTerm mef mixIn sign msrt pos t = do
       (\ srt -> Sorted_term resT srt pos) msrt
     return (resT, anaT)
 
+getAllIds :: (FormExtension f, TermExtension f) =>
+             BASIC_SPEC b s f -> Mix b s f e -> Sign f e -> IdSets
+getAllIds bs mix inSig =
+                 unite $ ids_BASIC_SPEC (getBaseIds mix) (getSigIds mix) bs
+                 : getExtIds mix (extendedInfo inSig) :
+                  [mkIdSets (allConstIds inSig) (allOpIds inSig)
+                  $ allPredIds inSig]
+
 basicAnalysis :: (FormExtension f, TermExtension f)
               => Min f e -- ^ type analysis of f
               -> Ana b b s f e  -- ^ static analysis of basic item b
@@ -879,10 +889,7 @@ basicAnalysis :: (FormExtension f, TermExtension f)
             {- ^ (BS with analysed mixfix formulas for pretty printing,
             differences to input Sig,accumulated Sig,analysed Sentences) -}
 basicAnalysis mef anab anas mix (bs, inSig, ga) =
-    let allIds = unite $ ids_BASIC_SPEC (getBaseIds mix) (getSigIds mix) bs
-                 : getExtIds mix (extendedInfo inSig) :
-                  [mkIdSets (allConstIds inSig) (allOpIds inSig)
-                  $ allPredIds inSig]
+    let allIds = getAllIds bs mix inSig
         (newBs, accSig) = runState (ana_BASIC_SPEC mef anab anas
                mix { mixRules = makeRules ga allIds }
                bs) inSig { globAnnos = addAssocs inSig ga }
@@ -908,15 +915,161 @@ basicCASLAnalysis = basicAnalysis (const return) (const return)
 
 -- | extra
 cASLsen_analysis ::
-        (BASIC_SPEC () () (), Sign () (), FORMULA ()) -> Result (FORMULA ())
+        (BASIC_SPEC () () (), Sign () (), FORMULA ()) ->
+        Result (FORMULA (), FORMULA ())
 cASLsen_analysis (bs, s, f) = let
                          mix = emptyMix
-                         allIds = unite $
-                                ids_BASIC_SPEC (getBaseIds mix)
-                                               (getSigIds mix) bs
-                                : getExtIds mix (extendedInfo s) :
-                                [mkIdSets (allConstIds s) (allOpIds s)
-                                $ allPredIds s]
+                         allIds = getAllIds bs mix s
                          mix' = mix { mixRules = makeRules emptyGlobalAnnos
                                                            allIds }
-                         in liftM fst $ anaForm (const return) mix' s f
+                         in anaForm (const return) mix' s f
+
+-- | convert theory
+
+convertCASLTheory :: (Sign f e, [Named (FORMULA f)]) -> BASIC_SPEC b s f
+convertCASLTheory (sig, nsens) =
+ case (sig, nsens) of
+  (_, []) -> Basic_spec [] -- TODO: the sig should be empty
+  _ -> error "convert theory nyi for CASL logic"
+
+-- | test nominal sen
+
+isNominalSen :: Set.Set Id -> FORMULA f -> (Bool, Maybe Id)
+isNominalSen noms aSen =
+     case aSen of
+      Mixfix_formula (Mixfix_token p) ->
+        let pId = simpleIdToId p
+        in if Set.member pId noms then (True, Just pId) else (False, Nothing)
+      _ -> (False, Nothing)
+
+-- | CASL hybridization: constraints to CASL sentences
+
+constrToSens :: Sign () () -> String -> SemanticConstraint ->
+                Result [Named (FORMULA ())]
+constrToSens sig cname sc =
+ let
+   st = genName $ "ST_" ++ cname
+   domain = genName $ "domain_" ++ cname
+   defined = genName "defined"
+   (totals, partials) = partition (\(_, ot) -> opKind ot == Total) $
+                                  MapSet.toPairList $ opMap sig
+ in
+ case sc of
+  SameInterpretation "sort" ->
+    return $
+    map (\s -> makeNamed ("ga_sem_constr_"++show s)
+                $ mkForall [mkVarDecl (genToken "w1") st,
+                            mkVarDecl (genToken "w2") st,
+                            mkVarDecl (genToken "x") s]
+                $ mkEqv
+                  (mkPredication
+                     (mkQualPred domain $ Pred_type [st, s] nullRange)
+                     [Qual_var (genToken "w1") st nullRange,
+                      Qual_var (genToken "x") s nullRange])
+                  (mkPredication
+                     (mkQualPred domain $ Pred_type [st, s] nullRange)
+                      [Qual_var (genToken "w2") st nullRange,
+                       Qual_var (genToken "x") s nullRange])
+          )
+                $ Set.toList $ sortSet sig
+  SameInterpretation "const" -> error "nyi for const"
+  SameInterpretation "op" ->
+   let
+      xs ot = zip (opArgs ot) [1::Int ..]
+      extOt i ot = Qual_op_name
+                    i
+                    (Op_type Total (st:opArgs ot) (opRes ot) nullRange)
+                    nullRange
+    in return $
+        map (\(i,ot) -> makeNamed ("ga_sem_constr_" ++ show i)
+                $ mkForall
+                  ( [mkVarDecl (genToken "w1") st,
+                     mkVarDecl (genToken "w2") st]
+                    ++
+                    (map (\(si, ii) ->
+                       mkVarDecl (genToken $ "x" ++ show ii) si) $ xs ot)
+                    )
+                    $ mkStEq
+                       (mkAppl (extOt i ot) $ map (\(a,b) -> mkVarTerm a b) $
+                         (genToken "w1", st):
+                         (map (\(si, ii) -> (genToken $ "x" ++ show ii, si)) $
+                              xs ot))
+                       (mkAppl (extOt i ot) $ map (\(a,b) -> mkVarTerm a b) $
+                         (genToken "w2", st):
+                         (map (\(si, ii) -> (genToken $ "x" ++ show ii, si)) $
+                              xs ot))
+          ) totals
+  SameInterpretation "pred" ->
+    let
+      xs pt = zip (predArgs pt) [1::Int ..]
+      extPt (Pred_type ss r) = Pred_type (st:ss) r
+    in return $
+        map (\(i, pt) -> makeNamed ("ga_sem_constr_" ++ show i) $
+                          mkForall
+                           ( [mkVarDecl (genToken "w1") st,
+                              mkVarDecl (genToken "w2") st]
+                              ++
+                              (map (\(si, ii) ->
+                                    mkVarDecl (genToken $ "x" ++ show ii) si)
+                                   $ xs pt)
+                           )
+                           $ mkEqv
+                              (mkPredication
+                                 (mkQualPred i $ extPt $ toPRED_TYPE pt) $
+                                map (\(a,b) -> mkVarTerm a b) $
+                                 (genToken "w1", st):
+                                 (map (\(si, ii) ->
+                                        (genToken $ "x" ++ show ii, si))
+                                      $ xs pt))
+                              (mkPredication
+                                 (mkQualPred i $ extPt $ toPRED_TYPE pt) $
+                                map (\(a,b) -> mkVarTerm a b) $
+                                (genToken "w2", st):
+                                (map (\(si, ii) ->
+                                       (genToken $ "x" ++ show ii, si))
+                                     $ xs pt))
+            ) $ MapSet.toPairList $ predMap sig
+  SameDomain False -> let
+      xs ot = zip (opArgs ot) [1::Int ..]
+      extOt i ot = Qual_op_name
+                     i
+                     (Op_type Total (st:opArgs ot) (opRes ot) nullRange)
+                     nullRange
+    in return $
+     map (\(i,ot) -> makeNamed ("ga_sem_constr_" ++ show i)
+                $ mkForall
+                   ( [mkVarDecl (genToken "w1") st,
+                      mkVarDecl (genToken "w2") st]
+                     ++
+                     (map (\(si, ii) ->
+                           mkVarDecl (genToken $ "x" ++ show ii) si)
+                          $ xs ot)
+                   )
+                   $ mkEqv
+                      (mkPredication
+                        (mkQualPred defined $
+                           Pred_type [st, opRes ot] nullRange) $
+                         [mkVarTerm (genToken "w1") st,
+                          mkAppl (extOt i ot) $
+                           map (\(a,b) -> mkVarTerm a b) $
+                            (genToken "w1", st):
+                            (map (\(si, ii) ->
+                                   (genToken $ "x" ++ show ii, si))
+                                 $ xs ot)
+                         ]
+                      )
+                      (mkPredication
+                         (mkQualPred defined $
+                            Pred_type [st, opRes ot] nullRange) $
+                        [mkVarTerm (genToken "w2") st,
+                         mkAppl (extOt i ot) $
+                          map (\(a,b) -> mkVarTerm a b) $
+                           (genToken "w2", st):
+                           (map (\(si, ii) ->
+                                  (genToken $ "x" ++ show ii, si))
+                                $ xs ot)
+                        ]
+                      )
+          )
+                partials
+  _ -> error $ "Constraint not supported for CASL logic:" ++ show sc

CoCASL/StatAna.hs

@@ -59,7 +59,7 @@ basicCoCASLAnalysis =
 -- analyses cocasl sentences only
 co_sen_analysis ::
         (BASIC_SPEC C_BASIC_ITEM C_SIG_ITEM C_FORMULA, CSign, FORMULA C_FORMULA)
-        -> Result (FORMULA C_FORMULA)
+        -> Result (FORMULA C_FORMULA, FORMULA C_FORMULA)
 co_sen_analysis (bs, s, f) = let
                         mix = emptyMix
                         allIds = unite $
@@ -68,7 +68,7 @@ co_sen_analysis (bs, s, f) = let
                                 [mkIdSets (allConstIds s) (allOpIds s)
                                 $ allPredIds s]
                         mix' = mix { mixRules = makeRules emptyGlobalAnnos allIds}
-                        in liftM fst $ anaForm minExpForm mix' s f
+                        in anaForm minExpForm mix' s f
 
 
 ana_CMix :: Mix C_BASIC_ITEM C_SIG_ITEM C_FORMULA CoCASLSign

Common/AnnoState.hs

@@ -214,6 +214,9 @@ equalT :: AParser st Token
 equalT = wrapAnnos $ pToken $ reserved [exEqual]
          (choice (map (keySign . string) [exEqual, equalS]) <?> show equalS)
 
+doubleColonT :: AParser st Token
+doubleColonT = asKey "::"
+
 colonT :: AParser st Token
 colonT = asKey colonS