Changeset 12794

Timestamp:

06.11.2009 18:39:28 (2 weeks ago)

Author:

maeder

Message:

made CASL2TopSort more usable

Location:

trunk

Files:

• Comorphisms/CASL2TopSort.hs (modified) (9 diffs)
• utils/nightly/cronjob.sh (modified) (1 diff)

trunk/Comorphisms/CASL2TopSort.hs

@@ -10 +10 @@
 Coding out subsorting into unary predicates.
    New concept for proving Ontologies.
+
+generatedness via non-injective datatype constructors
+(i.e. proper data constructors) is simply ignored
 -}
 
@@ -56 +59 @@
                Symbol RawSymbol ProofTree where
     sourceLogic CASL2TopSort = CASL
-    sourceSublogic CASL2TopSort = SL.top
+    sourceSublogic CASL2TopSort = SL.caslTop
         { sub_features = LocFilSub
-        , which_logic = FOL
-        , cons_features = SortGen
-            { emptyMapping = True
-            , onlyInjConstrs = True }}
+        , cons_features = emptyMapConsFeature }
     targetLogic CASL2TopSort = CASL
     mapSublogic CASL2TopSort sub =
@@ -145 +145 @@
 
 transSig :: Sign () e -> Result (Sign () e, [Named (FORMULA ())])
-transSig sig = if Rel.null sortRels then
-        hint (sig, [])
-        "CASL2TopSort.transSig: Signature is unchanged (no subsorting present)"
-        nullRange
+transSig sig = if Rel.null sortRels then return (sig, [])
     else do
     subSortMap <- generateSubSortMap sortRels (predMap sig)
-    let (dias2, newPredMap) = Map.mapAccum (\ ds (un, ds1) -> (ds ++ ds1, un))
-          [] $ Map.unionWithKey repError (transPredMap subSortMap
+    let newPredMap = Map.unionWith Set.union (transPredMap subSortMap
                   $ predMap sig) $ newPreds subSortMap
-    Result dias2 $ Just ()
     axs <- generateAxioms subSortMap (predMap sig) (opMap sig)
     return (sig
@@ -165 +160 @@
         }, axs ++ symmetryAxioms subSortMap sortRels)
     where sortRels = Rel.transClosure $ sortRel sig
-          repError k (v1, d1) (v2, d2) =
-              (Set.union v1 v2,
-               Diag Warning
-                     ("CASL2TopSort.transSig: generating " ++
-                      "overloading: Predicate " ++ show k ++
-                      " gets additional type(s): " ++ show v2) nullRange
-               : d1 ++ d2 )
           newPreds =
               foldr (\ pI -> Map.insert (predicatePI pI)
                                            (Set.singleton
-                                            (PredType [topSortPI pI]),[]))
+                                            (PredType [topSortPI pI])))
                     Map.empty . Map.elems
 
 transPredMap :: SubSortMap -> Map.Map PRED_NAME (Set.Set PredType)
-             -> Map.Map PRED_NAME (Set.Set PredType, [Diagnosis])
-transPredMap subSortMap = Map.map (\ s -> (Set.map transType s, []))
+             -> Map.Map PRED_NAME (Set.Set PredType)
+transPredMap subSortMap = Map.map $ Set.map transType
     where transType t = t
             { predArgs = map (\ s -> maybe s topSortPI
@@ -217 +205 @@
 symmetryAxioms ssMap sortRels =
     let symSets = Rel.sccOfClosure sortRels
-        toAxioms symSet = concatMap
+        toAxioms = concatMap
           (\ s ->
             let ts = lkupTop ssMap s
@@ -227 +215 @@
                    [makeNamed (show ts ++ "_symmetric_with_" ++ show symS)
                    $ mkForall [vd] (Predication psy [vt] nullRange) nullRange]
-          ) $ Set.toList symSet
+          ) . Set.toList
     in concatMap toAxioms symSets
 
@@ -292 +280 @@
               where joinedList = opArgs ot ++ [opRes ot]
                     fKind = opKind ot
-                    dias' = [ Diag Warning
-                                        ("Please, check if operation \"" ++
-                                         show opName ++
-                                         "\" is still partial as intended,\
-                                          \ since a joining of types could\
-                                         \ have made it total!!")
-                                        nullRange
+                    dias' = [ mkDiag Hint "partial op" opName
                               | fKind == Partial ]
           pt2topSorts = map (lkupTop ssm)
@@ -385 +367 @@
 transSen :: (Show f) => Sign f e -> FORMULA f -> Result (FORMULA f)
 transSen sig f = let sortRels = Rel.transClosure $ sortRel sig in
-    if Rel.null sortRels then
-        Result [Diag Hint
-        "CASL2TopSort.transSen: Sentence is unchanged (no subsorting present)"
-        nullRange ] (Just f)
+    if Rel.null sortRels then return f
     else do
     ssm <- generateSubSortMap sortRels (predMap sig)
@@ -489 +468 @@
                         $ conjunct $ map genImpl groupedInjOps
                     _ -> error "CASL2TopSort.genEitherAxiom.groupedInjOps"
-               else Result [Diag Error
-                                  "CASL2TopSort: Cannot handle \
-                                  \datatype constructors; only subsort \
-                                  \embeddings are allowed with free and \
-                                  \generated types!" nullRange] Nothing
+               else Result [mkDiag Warning
+                            "ignoring generating constructors"
+                            constrs]
+                    $ Just $ True_atom nullRange
           isInjOp ops =
               case ops of

trunk/utils/nightly/cronjob.sh

@@ -296 +296 @@
 }
 
+topSortCheck ()
+{
+cd $HETS_LIB
+date
+\rm Basic/*.th
+\rm Basic/*.thy
+for i in Basic/*.casl;
+    do ./hets -v2 -o th,thy -t CASL2PCFOLTopSort $i; done
+date
+for i in Basic/*.th; do ./hets -v2 -o th,pp.het $i; done
+date
+../Hets/utils/nightly/runisabelle.sh Basic/*.thy > ../isa3.log 2>&1
+fgrep \*\*\* ../isa3.log
+}
+
 checkEnvs ()
 {