keep alias names for type abstractions

git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8012 cec4b9c1-7d33-0410-9eda-942365e851bb
spechub · Jun 11, 2007 · 9c03fbe · 9c03fbe
1 parent 60f7db8
commit 9c03fbe
Show file tree

Hide file tree

Showing 4 changed files with 27 additions and 6 deletions.
diff --git a/HasCASL/Constrain.hs b/HasCASL/Constrain.hs
@@ -148,6 +148,12 @@ swap (a, b) = (b, a)
 substPairList :: Subst -> [(Type, Type)] -> [(Type, Type)]
 substPairList s = map ( \ (a, b) -> (subst s a, subst s b))
 
+absOrExpandedAbs :: Type -> Bool
+absOrExpandedAbs t = case t of
+    TypeAbs _ _ _ -> True
+    ExpandedType _ (TypeAbs _ _ _) -> True
+    _ -> False
+
 -- pre: shapeMatch succeeds
 shapeMgu :: TypeEnv -> [(Type, Type)] -> State (Int, Subst) [(Type, Type)]
 shapeMgu te cs =
@@ -159,8 +165,8 @@ shapeMgu te cs =
         tl = tail structs
         rest = tl ++ atoms
     in case (t1, t2) of
-    (ExpandedType _ t, _) -> shapeMgu te $ (t, t2) : rest
-    (_, ExpandedType _ t) -> shapeMgu te $ (t1, t) : rest
+    (ExpandedType _ t, _) | noAbs t -> shapeMgu te $ (t, t2) : rest
+    (_, ExpandedType _ t) | noAbs t -> shapeMgu te $ (t1, t) : rest
     (TypeAppl (TypeName l _ _) t, _) | l == lazyTypeId ->
         shapeMgu te $ (t, t2) : rest
     (_, TypeAppl (TypeName l _ _) t) | l == lazyTypeId ->
@@ -179,7 +185,7 @@ shapeMgu te cs =
                  FunKind ContraVar _ _ _ -> [(a, va)]
                  _ -> [(a, va), (va, a)]) ++ substPairList s rest
        else error ("shapeMgu1: " ++ showDoc t1 " < " ++ showDoc t2 "")
-    (TypeName _ _ v1, TypeAbs _ _ _) -> if v1 > 0 then do
+    (TypeName _ _ v1, _) | absOrExpandedAbs t2 -> if v1 > 0 then do
              let s = Map.singleton v1 t2
              addSubst s
              shapeMgu te $ substPairList s rest

diff --git a/HasCASL/Unify.hs b/HasCASL/Unify.hs
@@ -97,12 +97,18 @@ eps = Map.empty
 flatKind :: Type -> RawKind
 flatKind = mapKindV (const InVar) id . rawKindOfType
 
+
+noAbs :: Type -> Bool
+noAbs t = case t of
+    TypeAbs _ _ _ -> False
+    _ -> True
+
 match :: TypeMap -> (TypeId -> TypeId -> Bool)
           -> (Bool, Type) -> (Bool, Type) -> Result Subst
 match tm rel p1@(b1, ty1) p2@(b2, ty2) =
   if flatKind ty1 == flatKind ty2 then case (ty1, ty2) of
-    (_, ExpandedType _ t2) -> match tm rel p1 (b2, t2)
-    (ExpandedType _ t1, _) -> match tm rel (b1, t1) p2
+    (_, ExpandedType _ t2) | noAbs t2 -> match tm rel p1 (b2, t2)
+    (ExpandedType _ t1, _) | noAbs t1 -> match tm rel (b1, t1) p2
     (_, TypeAppl (TypeName l _ _) t2) | l == lazyTypeId ->
               match tm rel p1 (b2, t2)
     (TypeAppl (TypeName l _ _) t1, _) | l == lazyTypeId ->

diff --git a/HasCASL/VarDecl.hs b/HasCASL/VarDecl.hs
@@ -127,6 +127,15 @@ addTypeKind warn d i rk k =
                        Just newDefn -> do
                            putTypeMap $ Map.insert i
                                (TypeInfo ok insts sups newDefn) tm
+                           case newDefn of
+                             AliasTypeDefn (TypeScheme [arg] 
+                                (ExpandedType (Typename j rkj 0)
+                                              (TypeAbs _ _ _)) _) ->
+                                addTypeId False NoTypeDefn Instance rkj
+                                    (case k of 
+                                       FunKind _ _ ek _ -> ek
+                                       _ -> error "addTypeKind") j
+                             _ -> return True
                            return True
                        Nothing -> do
                            addDiags $ map (improveDiag i) ds

diff --git a/HasCASL/test/XUnion.hascasl.output b/HasCASL/test/XUnion.hascasl.output
@@ -32,5 +32,5 @@ g' : Graph N E
 ### Hint 8.15, not a kind 'Graph N E'
 ### Hint, in type of '((var g : Graph N E), (var g' : Graph N E))'
   type 'Graph N' (8.23)
-  is not unifiable with type '\ S : Type . S ->? Unit' (2.23)
+  is not unifiable with type 'Set' (6.47)