Changeset 12760

Timestamp:

30.10.2009 15:04:24 (3 weeks ago)

Author:

maeder

Message:

removed inline axioms and created axioms directly

Location:

trunk

Files:

• CASL/Project.hs (modified) (2 diffs)
• CASL/Sign.hs (modified) (3 diffs)
• Comorphisms/CASL2PCFOL.hs (modified) (1 diff)
• Comorphisms/CASL2SubCFOL.hs (moved) (moved from trunk/Comorphisms/CASL2SubCFOL.inline.hs) (12 diffs)
• Makefile (modified) (1 diff)

trunk/CASL/Project.hs

@@ -48 +48 @@
 botTok = genToken "bottom"
 
-bottom :: Id
-bottom = mkId [botTok]
-
 uniqueBotName :: OP_TYPE -> Id
 uniqueBotName t = case t of
@@ -58 +55 @@
 projectUnique :: OpKind -> Range -> TERM f -> SORT -> TERM f
 projectUnique = makeInjOrProj uniqueProjName
-
-rename :: OP_SYMB -> OP_SYMB
-rename o = case o of
-    Qual_op_name i t r -> Qual_op_name
-        (if i == injName then uniqueInjName t
-         else if i == projName then uniqueProjName t
-         else if i == bottom then uniqueBotName t
-              else i) t r
-    _ -> o
-
-renameRecord :: (f -> f) -> Record f (FORMULA f) (TERM f)
-renameRecord mf = (mapRecord mf)
-     { foldApplication = \ _ o args r -> Application (rename o) args r }
-
-renameTerm :: (f -> f) -> TERM f -> TERM f
-renameTerm = foldTerm . renameRecord
-
-renameFormula :: (f -> f) -> FORMULA f -> FORMULA f
-renameFormula = foldFormula . renameRecord

trunk/CASL/Sign.hs

@@ -471 +471 @@
 mkExEq f f' = Existl_equation f f' nullRange
 
+mkStEq :: TERM f -> TERM f -> FORMULA f
+mkStEq u v = Strong_equation u v nullRange
+
+mkEqv :: FORMULA f -> FORMULA f -> FORMULA f
+mkEqv u v = Equivalence u v nullRange
+
 mkAppl :: OP_SYMB -> [TERM f] -> TERM f
 mkAppl op_symb fs = Application op_symb fs nullRange
@@ -485 +491 @@
 conjunct :: [FORMULA f] -> FORMULA f
 conjunct fs = case fs of
-  [] -> False_atom nullRange
+  [] -> True_atom nullRange
   [phi] -> phi
   _ -> Conjunction fs nullRange
@@ -491 +497 @@
 mkVarDeclStr :: String -> SORT -> VAR_DECL
 mkVarDeclStr = mkVarDecl . mkSimpleId
+
+mkAxName :: String -> SORT -> SORT -> String
+mkAxName str s s' = "ga_" ++ str ++ "_" ++ show s ++ "_to_" ++ show s'

trunk/Comorphisms/CASL2PCFOL.hs

@@ -94 +94 @@
           injOpMap setprojOptype
     -- membership predicates are coded out
-
-mkAxName :: String -> SORT -> SORT -> String
-mkAxName str s s' = "ga_" ++ str ++ "_" ++ show s ++ "_to_" ++ show s'
 
 -- | Make the name for the embedding or projecton injectivity axiom

trunk/Comorphisms/CASL2SubCFOL.hs

@@ -2 +2 @@
 Module      :  $Header$
 Description :  coding out partiality
-Copyright   :  (c) Zicheng Wang, C.Maeder Uni Bremen 2002-2006
+Copyright   :  (c) Zicheng Wang, C.Maeder Uni Bremen 2002-2009
 License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
 
@@ -37 +37 @@
 import Common.ProofUtils
 import Common.ProofTree
-
-import Data.List (zip)
+import Common.Utils
 
 -- | determine the need for bottom constants
-data FormulaTreatment = NoMembershipOrCast | FormulaDependent | SubsortBottoms | AllSortBottoms
+data FormulaTreatment =
+    NoMembershipOrCast
+  | FormulaDependent
+  | SubsortBottoms
+  | AllSortBottoms
     deriving Show
 
@@ -141 +144 @@
                     ( \ t -> opKind t == Partial)) ops
         collect given =
-            let more = allSortsWithBottom $
-                       Set.unions $ map (Set.map opRes .
-                                 Set.filter ( \ t -> any
-                                 (flip Set.member given) $ opArgs t)) ops
+            let more = allSortsWithBottom $ Set.unions $ map
+                     (Set.map opRes . Set.filter
+                      (any (flip Set.member given) . opArgs)) ops
             in if Set.isSubsetOf more given then given
                else collect $ Set.union more given
@@ -152 +154 @@
 defPred = genName "defined"
 
-defined :: Set.Set SORT -> TERM f -> SORT -> Range -> FORMULA f
-defined bsorts t s ps =
+defined :: Set.Set SORT -> TERM f -> Range -> FORMULA f
+defined bsorts t ps = let s = sortOfTerm t in
   if Set.member s bsorts then Predication
          (Qual_pred_name defPred (Pred_type [s] nullRange) nullRange) [t] ps
@@ -159 +161 @@
 
 defVards :: Set.Set SORT -> [VAR_DECL] -> FORMULA f
-defVards bs [vs@(Var_decl [_] _ _)] = head $ defVars bs vs
-defVards bs vs = Conjunction (concatMap (defVars bs) vs) nullRange
+defVards bs = conjunct . concatMap (defVars bs)
 
 defVars :: Set.Set SORT -> VAR_DECL -> [FORMULA f]
@@ -166 +167 @@
 
 defVar :: Set.Set SORT -> SORT -> Token -> FORMULA f
-defVar bs s v = defined bs (Qual_var v s nullRange) s nullRange
+defVar bs s v = defined bs (Qual_var v s nullRange) nullRange
 
 totalizeOpSymb :: OP_SYMB -> OP_SYMB
@@ -189 +190 @@
     c { opSymbs = map ( \ (o, is) -> (totalizeOpSymb o, is)) $ opSymbs c }
 
+botType :: SORT -> OpType
+botType x = OpType {opKind = Total, opArgs = [], opRes = x }
+
 -- | Add projections to the signature
 encodeSig :: Set.Set SORT -> Sign f e -> Sign f e
@@ -194 +198 @@
     sig { opMap = projOpMap, predMap = newpredMap } where
    newTotalMap = Map.map (Set.map $ makeTotal Total) $ opMap sig
-   botType x = OpType {opKind = Total, opArgs = [], opRes = x }
    botOpMap  = Set.fold (\ bt -> addOpTo (uniqueBotName $ toOP_TYPE bt) bt)
        newTotalMap $ Set.map botType bsorts
@@ -208 +211 @@
 
 generateAxioms :: Bool -> Set.Set SORT -> Sign f e -> [Named (FORMULA ())]
-generateAxioms b bsorts sig = filter (not . is_True_atom . sentence) $
-  map (mapNamed $ simplifyFormula id . rmDefs bsorts id) $
-    map (mapNamed $ renameFormula id) $ concat $
-    [inlineAxioms CASL
-      " sort s < s'     \
-      \ op pr : s'->s   \
-      \ pred d:s        \
-      \ forall x,y:s'. d(pr(x)) /\\ d(pr(y)) /\\ pr(x)=pr(y) => x=y \
-      \ %(ga_projection_injectivity)% "
-    ++ inlineAxioms CASL
-     " sort s < s'      \
-      \ op pr : s'->s   \
-      \ pred d:s        \
-      \ forall x:s . d(x) => pr(x)=x %(ga_projection)% "
-      | s <- sortList, let y = mkSimpleId "y",
-        s' <- minSupers s]
-    ++ [inlineAxioms CASL
-      " sort s          \
-      \ pred d:s        \
-      \ . exists x:s.d(x) %(ga_nonEmpty)%" ++
-     (if b then
-     inlineAxioms CASL
-      " sort s          \
-      \ op bottom:s     \
-      \ pred d:s        \
-      \ . forall x:s . not d(x) <=> x=bottom %(ga_notDefBottom)%"
-      else
-     inlineAxioms CASL
-      " sort s          \
-      \ op bottom:s     \
-      \ pred d:s        \
-      \ . not d(bottom) %(ga_notDefBottom)%")
-        | s <- sortList ] ++
-    [inlineAxioms CASL
-      " sort t          \
-      \ sorts s_i       \
-      \ op f:s_i->t     \
-      \ forall y_k:s_i . def f(y_k) <=> def y_k /\\ def y_k %(ga_totality)%"
-        | (f,typ) <- opList, opKind typ == Total,
-          let s=opArgs typ; t=opRes typ; y= mkVars (length s) ] ++
-    [inlineAxioms CASL
-      " sort t          \
-      \ sorts s_i       \
-      \ op f:s_i->t     \
-      \ forall y_k:s_i . def f(y_k) => def y_k /\\ def y_k %(ga_strictness)%"
-        | (f,typ) <- opList, opKind typ == Partial,
-          let s=opArgs typ; t=opRes typ; y= mkVars (length s) ] ++
-    [inlineAxioms CASL
-      " sorts s_i       \
-      \ pred p:s_i      \
-      \ forall y_k:s_i . p(y_k) => def y_k /\\ def y_k \
-      \ %(ga_predicate_strictness)%"
-        | (p,typ) <- predList, let s=predArgs typ; y=mkVars (length s) ]
+generateAxioms uniqBot bsorts sig = concatMap (\ s -> let
+      vx = mkVarDeclStr "x" s
+      xt = toQualVar vx
+      hasBot = Set.member s bsorts
+      prj z = projectUnique Total nullRange z s
+      df z = defined bsorts z nullRange
+      in concatMap (\ s' ->
+      [makeNamed (mkAxName "projection_injectivity" s' s)
+      $ let xv = mkVarDeclStr "x" s'
+            yv = mkVarDeclStr "y" s'
+            tx = toQualVar xv
+            ty = toQualVar yv
+            px = prj tx
+            py = prj ty
+            epxy = mkStEq px py
+      -- forall x,y:s' . d(pr(x)) /\\ d(pr(y)) /\\ pr(x)=pr(y) => x=y
+        in mkForall [xv, yv]
+           (mkImpl (if hasBot then conjunct [df px, df py, epxy]
+                    else epxy) $ mkStEq tx ty)
+           nullRange
+            -- forall x:s . d(x) => pr(x)=x
+      , makeNamed (mkAxName "projection" s' s)
+      $ let eq = mkStEq (prj $ Sorted_term xt s' nullRange) xt
+        in mkForall [vx]
+               (if hasBot then mkImpl (df xt) eq else eq)
+               nullRange]) (minSupers s)
+         -- exists x:s . d(x)
+      ++ [makeNamed ("ga_nonEmpty_" ++ show s)
+         $ Quantification Existential [vx] (df xt) nullRange
+         | hasBot]
+      ++ [makeNamed ("ga_notDefBottom_" ++ show s)
+         $ let bty = toOP_TYPE $ botType s
+               bt = mkAppl (Qual_op_name (uniqueBotName bty) bty nullRange) []
+           in if uniqBot then
+              -- forall x:s . not d(x) <=> x=bottom
+              mkForall [vx]
+              (mkEqv (Negation (df xt) nullRange)
+               $ mkStEq xt bt) nullRange
+              else Negation (df bt) nullRange -- not d(bottom)
+         | hasBot]) sortList
+   ++ filter (not . is_True_atom . sentence)
+   (map (mapNamed $ simplifyFormula id)
+    $ map (\ (f, typ) ->
+      let vs = map (\ (s, i) -> mkVarDeclStr ("x_" ++ show i) s)
+              $ number $ opArgs typ
+      in makeNamed ("ga_totality_" ++ show f)
+      -- forall x_i:s_i . d f(x_1, ..., x_n) {<}=> d x_1 /\\ ... /\\ d x_n
+         $ mkForall vs
+           ((if opKind typ == Total then mkEqv else mkImpl)
+            (defined bsorts (mkAppl (Qual_op_name f (toOP_TYPE typ) nullRange)
+                      $ map toQualVar vs) nullRange)
+            $ defVards bsorts vs) nullRange) opList
+    ++ map (\ (p, typ) ->
+      let vs = map (\ (s, i) -> mkVarDeclStr ("x_" ++ show i) s)
+              $ number $ predArgs typ
+      in makeNamed ("ga_predicate_strictness_" ++ show p)
+      -- forall x_i:s_i . p(x_1, ..., x_n) => d x_1 /\\ ... /\\ d x_n
+         $ mkForall vs
+           (mkImpl
+            (Predication (Qual_pred_name p (toPRED_TYPE typ) nullRange)
+                      (map toQualVar vs) nullRange)
+            $ defVards bsorts vs) nullRange) predList)
     where
-        x = mkSimpleId "x"
-        pr = projName
         minSupers so = keepMinimals sig id $ Set.toList $ Set.delete so
                            $ supersortsOf so sig
-        d = defPred
         sortList = Set.toList bsorts
         opList = [(f,t) | (f,types) <- Map.toList $ opMap sig,
@@ -272 +281 @@
         predList = [(p,t) | (p,types) <- Map.toList $ predMap sig,
                     t <- Set.toList types ]
-        mkVars n = [mkSimpleId ("x_"++show i) | i<-[1..n]]
 
 codeRecord :: Bool -> Set.Set SORT -> (f -> f) -> Record f (FORMULA f) (TERM f)
@@ -281 +289 @@
           Quantification q vs (Implication (defVards bsrts vs) qf True ps) ps
       _ -> Quantification q vs (Conjunction [defVards bsrts vs, qf] ps) ps
-    , foldDefinedness = \ _ t ps -> defined bsrts t (sortOfTerm t) ps
+    , foldDefinedness = const $ defined bsrts
     , foldExistl_equation = \ _ t1 t2 ps ->
       Conjunction[Strong_equation t1 t2 ps,
-                  defined bsrts t1 (sortOfTerm t1) ps] ps
+                  defined bsrts t1 ps] ps
     , foldMembership = \ _ t s ps ->
-          defined bsrts (projectUnique Total ps t s) s ps
+          defined bsrts (projectUnique Total ps t s) ps
     , foldSort_gen_ax = \ _ cs b -> if uniBot then
-          Sort_gen_ax (map (totalizeConstraint bsrts) cs) $
-              if not uniBot || Set.null (Set.intersection bsrts
-                $ Set.fromList $ map newSort cs) then b else False
+          Sort_gen_ax (map (totalizeConstraint bsrts) cs)
+              $ Set.null (Set.intersection bsrts
+                $ Set.fromList $ map newSort cs) && b
           else error "SubPFOL2SubFOL: unexpected Sort_gen_ax"
-    , foldApplication = \ _ o args ps -> Application (totalizeOpSymb o) args ps
+    , foldApplication = const $ Application . totalizeOpSymb
     , foldCast = \ _ t s ps -> projectUnique Total ps t s }
 
@@ -300 +308 @@
 codeTerm :: Bool -> Set.Set SORT -> TERM () -> TERM ()
 codeTerm b bsorts = foldTerm (codeRecord b bsorts $ error "CASL2SubCFol")
-
-rmDefsRecord :: Set.Set SORT -> (f -> f) ->  Record f (FORMULA f) (TERM f)
-rmDefsRecord  bsrts mf = (mapRecord mf)
-    { foldDefinedness = \ _ t ps -> defined bsrts t (sortOfTerm t) ps }
-
-rmDefs :: Set.Set SORT -> (f -> f) -> FORMULA f -> FORMULA f
-rmDefs bsrts = foldFormula . rmDefsRecord bsrts
 
 -- | find sorts that need a bottom in membership formulas and casts

trunk/Makefile

@@ -363 +363 @@
 
 # files to be processed by utils/InlineAxioms
-inline_axiom_files = Comorphisms/Modal2CASL.hs \
-    Comorphisms/CASL2SubCFOL.hs CASL_DL/PredefinedSign.hs
+inline_axiom_files = Comorphisms/Modal2CASL.hs CASL_DL/PredefinedSign.hs
 
 gen_inline_axiom_files = $(patsubst %.hs,%.inline.hs, $(inline_axiom_files))