Changeset 11873

Timestamp:

03.07.2009 16:16:41 (9 months ago)

Author:

maeder

Message:

fully close type environment of formulas (considering down sets)

Location:

trunk/HasCASL

Files:

• VarDecl.hs (modified) (2 diffs)
• test/Subtype.hascasl.output (modified) (1 diff)

trunk/HasCASL/VarDecl.hs

@@ -23 +23 @@
 import qualified Data.Set as Set
 import Common.Id
+import Common.Lib.Rel (setToMap)
 import Common.Lib.State
 import Common.Result
@@ -45 +46 @@
 mkEnvForall :: Env -> Term -> Range -> Term
 mkEnvForall e t ps =
-  let tys = Set.fromList $ map (fst . snd) $ concatMap (leaves (>= 0))
-            $ getAllTypes t
-      tyVs = map ( \ (i, TypeVarDefn v vk rk c) -> GenTypeVarDecl $
-                   TypeArg i v vk rk c Other ps) $ Map.toList
-             $ Map.filterWithKey ( \ i _ -> Set.member i tys) $ localTypeVars e
+  let tys = getAllTypes t
+      tyVs = map GenTypeVarDecl $ getTypeVars (localTypeVars e) tys ps
       vs = tyVs ++ map GenVarDecl (Set.toList $ freeVars t)
   in if null vs then t else QuantifiedTerm Universal vs t ps
+
+getTypeVars :: LocalTypeVars -> [Type] -> Range -> [TypeArg]
+getTypeVars e tys ps =
+  let is = Set.unions $ map (idsOf (>= 0)) tys
+      tyVs = Map.intersection e $ setToMap is
+      dTys = Map.fold (\ (TypeVarDefn _ vk _ _) l -> case vk of
+             Downset ty -> ty : l
+             _ -> l) [] tyVs
+      dis = Set.unions $ map (idsOf (>= 0)) dTys
+  in if Set.isSubsetOf dis is then
+          map ( \ (i, TypeVarDefn v vk rk c) -> TypeArg i v vk rk c Other ps)
+          $ Map.toList tyVs
+     else getTypeVars e (dTys ++ tys) ps
 
 anaStarType :: Type -> State Env (Maybe Type)

trunk/HasCASL/test/Subtype.hascasl.output

@@ -59 +59 @@
 forall a < b : Type; b < c : Type; c : Type; x : a
 . up (up x : b) = (up x : c)
-forall a < b : Type; b < c : Type; x : a . up x = (x : b)
+forall a < b : Type; b < c : Type; c : Type; x : a . up x = (x : b)
 forall e : Type; f : Type; f : e -> f
 . (up f : e ->? f) = \ x : e . f x