transition to using TypeAbs

git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@7961 cec4b9c1-7d33-0410-9eda-942365e851bb

HasCASL/AsUtils.hs

@@ -45,7 +45,9 @@ getTypeAppl ty = let (t, args) = getTyAppl ty in
    (t, reverse args) where
     getTyAppl typ = case typ of
         TypeAppl t1 t2 -> let (t, args) = getTyAppl t1 in (t, t2 : args)
-        ExpandedType _ t -> getTyAppl t
+        ExpandedType _ te -> let (t, args) = getTyAppl te
+                             in if null args then (typ, [])
+                                    else (t, args)
         KindedType t _ _ -> getTyAppl t
         _ -> (typ, [])
 

HasCASL/Constrain.hs

@@ -27,6 +27,7 @@ import HasCASL.Unify
 import HasCASL.As
 import HasCASL.AsUtils
 import HasCASL.Le
+import HasCASL.PrintLe()
 import HasCASL.TypeAna
 import HasCASL.ClassAna
 
@@ -63,8 +64,8 @@ data Constrain = Kinding Type Kind
 
 instance Pretty Constrain where
     pretty c = case c of
-       Kinding ty k -> fsep [pretty ty, colon, pretty k]
-       Subtyping t1 t2 -> fsep [pretty t1, less, pretty t2]
+       Kinding ty k -> pretty $ KindedType ty k nullRange
+       Subtyping t1 t2 -> fsep [pretty t1, less <+> pretty t2]
 
 instance PosItem Constrain where
   getRange c = case c of
@@ -154,10 +155,10 @@ shapeMgu te cs =
                                        (TypeName _ _ _, TypeName _ _ _) -> True
                                        _ -> False) cs
     in if null structs then return atoms else
-    let p@(t1, t2) = head structs
+    let (t1, t2) = head structs
         tl = tail structs
         rest = tl ++ atoms
-    in case p of
+    in case (betaReduce t1, betaReduce t2) of
     (ExpandedType _ t, _) -> shapeMgu te $ (t, t2) : rest
     (_, ExpandedType _ t) -> shapeMgu te $ (t1, t) : rest
     (TypeAppl (TypeName l _ _) t, _) | l == lazyTypeId ->
@@ -166,7 +167,7 @@ shapeMgu te cs =
         shapeMgu te $ (t1, t) : rest
     (KindedType t _ _, _) -> shapeMgu te $ (t, t2) : rest
     (_, KindedType t _ _) -> shapeMgu te $ (t1, t) : rest
-    (TypeName _ _ v1, TypeAppl f a) -> if (v1 > 0) then do
+    (TypeName _ _ v1, TypeAppl f a) -> if v1 > 0 then do
              vf <- toPairState $ freshTypeVarT f
              va <- toPairState $ freshTypeVarT a
              let s = Map.singleton v1 (TypeAppl vf va)
@@ -176,16 +177,33 @@ shapeMgu te cs =
                  FunKind ContraVar _ _ _ -> [(a, va)]
                  _ -> [(a, va), (va, a)]) ++ substPairList s rest
        else error ("shapeMgu1: " ++ showDoc t1 " < " ++ showDoc t2 "")
-    (_, TypeName _ _ _) -> do ats <- shapeMgu te ((t2, t1) : map swap rest)
-                              return $ map swap ats
-    (TypeAppl f1 a1, TypeAppl f2 a2) ->
-         shapeMgu te $ (f1, f2) : case (rawKindOfType f1, rawKindOfType f2) of
+    (TypeName _ _ v1, TypeAbs _ _ _) -> if v1 > 0 then do
+             let s = Map.singleton v1 t2
+             addSubst s
+             shapeMgu te $ substPairList s rest
+       else error ("shapeMgu1: " ++ showDoc t1 " < " ++ showDoc t2 "")
+    (_, TypeName _ _ _) -> do 
+      ats <- shapeMgu te ((t2, t1) : map swap rest)
+      return $ map swap ats
+    (TypeAppl f1 a1, TypeAppl f2 a2) -> let
+        Result _ ms1 = if hasRedex t1 then
+              shapeMatch (typeMap te) (redStep t1) t2 else fail "shapeMatch1"
+        Result _ ms2 = if hasRedex t2 then
+              shapeMatch (typeMap te) t1 (redStep t2) else fail "shapeMatch2"
+        res = shapeMgu te $ (f1, f2) : 
+           case (rawKindOfType f1, rawKindOfType f2) of
               (FunKind CoVar _ _ _,
                FunKind CoVar _ _ _) -> (a1, a2) : rest
               (FunKind ContraVar _ _ _,
                FunKind ContraVar _ _ _) -> (a2, a1) : rest
               _ -> (a1, a2) : (a2, a1) : rest
-    _ -> error ("shapeMgu2: " ++ showDoc t1 " < " ++ showDoc t2 "")
+        in case ms1 of
+               Nothing -> case ms2 of
+                   Nothing -> res 
+                   Just _ -> shapeMgu te $ (t1, redStep t2) : rest
+               Just _ -> shapeMgu te $ (redStep t1, t2) : rest
+    _ -> if t1 == t2 then shapeMgu te rest else 
+         error ("shapeMgu2: " ++ showDoc t1 " < " ++ showDoc t2 "")
 
 shapeUnify :: TypeEnv -> [(Type, Type)] -> State Int (Subst, [(Type, Type)])
 shapeUnify te l = do
@@ -268,7 +286,7 @@ shapeRel te cs =
 -- | compute monotonicity of a type variable
 monotonic :: TypeEnv -> Int -> Type -> (Bool, Bool)
 monotonic te v t =
-     case t of
+     case betaReduce t of
            TypeName _ _ i -> (True, i /= v)
            TypeAppl t1 t2 -> let
                 (a1, a2) = monotonic te v t2
@@ -277,7 +295,7 @@ monotonic te v t =
                    FunKind CoVar _ _ _ -> (f1 && a1, f2 && a2)
                    FunKind ContraVar _ _ _ -> (f1 && a2, f2 && a1)
                    _ -> (f1 && a1 && a2, f2 && a1 && a2)
-           _ -> monotonic te v (stripType t)
+           _ -> monotonic te v (stripType "monotonic" t)
 
 -- | find monotonicity based instantiation
 monoSubst :: TypeEnv -> Rel.Rel Type -> Type -> Subst

HasCASL/Le.hs

@@ -78,7 +78,9 @@ rename :: (TypeId -> RawKind -> Int -> Type) -> Type -> Type
 rename m t = case t of
            TypeName i k n -> m i k n
            TypeAppl t1 t2 -> TypeAppl (rename m t1) (rename m t2)
-           TypeAbs v1 t2 ps -> TypeAbs v1 (rename m t2) ps
+           TypeAbs v1@(TypeArg i _ _ _ c _ _) t2 ps -> TypeAbs v1 (rename 
+                 ( \ j k n -> if (j, n) == (i, c) then 
+                      TypeName j k n else  m j k n) t2) ps
            ExpandedType t1 t2 -> ExpandedType (rename m t1) (rename m t2)
            TypeToken _ -> t
            BracketType b l ps ->

HasCASL/Sublogic.hs

@@ -59,6 +59,7 @@ import Common.Id
 
 import HasCASL.As
 import HasCASL.AsUtils
+import HasCASL.TypeAna
 import HasCASL.Le
 import HasCASL.Builtin
 import HasCASL.FoldTerm
@@ -543,7 +544,7 @@ sl_Basictype ty = case ty of
     KindedType t k _ -> sublogic_max (sl_Basictype t) $ sl_kind k
     ExpandedType _ t -> sl_Basictype t
     BracketType Parens [t] _ -> sl_Basictype t
-    _ -> case getTypeAppl ty of
+    _ -> case getTypeAppl $ betaReduce ty of
          (TypeName ide _ _, args) -> comp_list $
             (if isArrow ide || ide == lazyTypeId then need_hol else
                 need_type_constructors) : map sl_Basictype args

HasCASL/SubtypeDecl.hs

@@ -37,7 +37,7 @@ anaKind k = do mrk <- fromResult $ anaKindM k . classMap
 -- | add a supertype to a given type id
 addSuperType :: Type -> Kind -> (Id, [TypeArg]) -> State Env ()
 addSuperType t ak p@(i, nAs) =
-    case t of
+    case betaReduce t of
     TypeName j _ v -> if v /= 0 then
          addDiags[mkDiag Error
                 ("illegal type variable as supertype") j]
@@ -65,7 +65,7 @@ addSuperType t ak p@(i, nAs) =
             addTypeId False (AliasTypeDefn newSc)
                   Plain ark fullKind i
             return ()
-    _ -> addSuperType (stripType t) ak p
+    _ -> addSuperType (stripType "addSuperType" t) ak p
 
 generalizeT :: TypeScheme -> State Env TypeScheme
 generalizeT (TypeScheme args ty p) = do

HasCASL/Symbol.hs

@@ -77,6 +77,7 @@ subSyms e t = case t of
            TypeAppl t1 t2 -> Set.union (subSyms e t1) (subSyms e t2)
            ExpandedType _ t1 -> subSyms e t1
            KindedType tk _ _ -> subSyms e tk
+           TypeAbs _ b _ -> subSyms e b
            _ -> error ("subSyms: " ++ show t)
 
 subSymsOf :: Symbol -> SymbolSet

HasCASL/TypeAna.hs

@@ -89,12 +89,10 @@ inferKinds b ty te@Env{classMap = cm} = case ty of
        ((rk, ks), t3) <- inferKinds b t1 te
        case rk of
            FunKind v _ rr _ -> do
-               ((_, l), t4) <- case v of
-                            ContraVar ->
-                                inferKinds (fmap not b) t2 te
-                            CoVar ->
-                                inferKinds b t2 te
-                            InVar -> inferKinds Nothing t2 te
+               ((_, l), t4) <- inferKinds (case v of
+                            ContraVar -> fmap not b
+                            CoVar -> b
+                            InVar -> Nothing) t2 te
                kks <- mapM (getFunKinds cm) ks
                rs <- mapM ( \ fk -> case fk of
                     FunKind _ arg res _ -> do
@@ -105,7 +103,7 @@ inferKinds b ty te@Env{classMap = cm} = case ty of
            _ -> mkError "unexpected type argument" t2
     TypeAbs ta@(TypeArg _ v k r _ _ q) t ps -> do
         let newEnv = execState (addTypeVarDecl False ta) te
-        ((rk, ks), nt) <- inferKinds b t newEnv
+        ((rk, ks), nt) <- inferKinds Nothing t newEnv
         return ((FunKind v r rk q, map (\ j -> FunKind v (toKind k) j q) ks)
                , TypeAbs ta nt ps)
     KindedType kt kind ps -> do
@@ -119,17 +117,17 @@ inferKinds b ty te@Env{classMap = cm} = case ty of
         (kp, t4) <- inferKinds b t2 te
         return (kp, case mk of
                 Just (_, t3) -> ExpandedType t3 t4
-                Nothing -> t4)
+                Nothing -> ExpandedType t1 t4)
     _ -> error "inferKinds"
 
 -- * converting type terms
 
 -- | throw away alias or kind information
-stripType :: Type -> Type
-stripType ty = case ty of
+stripType :: String -> Type -> Type
+stripType msg ty = case ty of
     ExpandedType _ t -> t
     KindedType t _ _ -> t
-    _ -> error "stripType"
+    _ -> error $ "stripType " ++ msg
 
 -- * subtyping relation
 
@@ -142,11 +140,11 @@ rawKindOfType ty = case ty of
         _ -> error "rawKindOfType"
     TypeAbs (TypeArg _ v _ r _ _ _) t ps ->
         FunKind v r (rawKindOfType t) ps
-    _ -> rawKindOfType $ stripType ty
+    _ -> rawKindOfType $ stripType "rawKindOfType" ty
 
 -- | subtyping relation
 lesserType :: TypeEnv -> Type -> Type -> Bool
-lesserType te t1 t2 = case (t1, t2) of
+lesserType te t1 t2 = case (betaReduce t1, betaReduce t2) of
     (TypeAppl c1 a1, TypeAppl c2 a2) ->
         let b1 = lesserType te a1 a2
             b2 = lesserType te a2 a1
@@ -169,10 +167,13 @@ lesserType te t1 t2 = case (t1, t2) of
             Downset t -> lesserType te t t2
             _ -> False
     (TypeAppl _ _, TypeName _ _ _) -> False
+    (TypeAppl _ _, TypeAbs _ _ _) -> False
+    (TypeAbs _ _ _, TypeName _ _ _) -> False
     (KindedType t _ _, _) -> lesserType te t t2
     (ExpandedType _ t, _) -> lesserType te t t2
-    (TypeAbs _ _ _, _) -> False
-    _ -> lesserType te t1 $ stripType t2
+    (_, KindedType t _ _) -> lesserType te t1 t
+    (_, ExpandedType _ t) -> lesserType te t1 t
+    (t3, t4) -> t3 == t4
 
 -- * leaves of types and substitution
 
@@ -184,8 +185,9 @@ leaves b t =
                              then [(i, (j, k))]
                              else []
            TypeAppl t1 t2 -> leaves b t1 `List.union` leaves b t2
-           TypeAbs _ ty _ -> leaves b ty
-           _ -> leaves b $ stripType t
+           TypeAbs (TypeArg i _ _ r c _ _) ty _ -> 
+               List.delete (c, (i, r)) $ leaves b ty
+           _ -> leaves b $ stripType "leaves" t
 
 -- | type identifiers of a type
 idsOf :: (Int -> Bool) -> Type -> Set.Set TypeId
@@ -221,15 +223,40 @@ schemeToTypeAbs (TypeScheme l ty ps) = case l of
     [] -> ty
     hd : tl -> TypeAbs hd (schemeToTypeAbs $ TypeScheme tl ty ps) ps
 
+{- | single step beta reduce type abstractions -}
+redStep :: Type -> Type
+redStep ty = case ty of
+    TypeAppl t1 t2 -> case t1 of
+        TypeAbs (TypeArg i _ _ _ c _ _) b _ -> 
+            rename ( \ j k n -> if (j, n) == (i, c) then t2
+                                else TypeName j k n) b
+        ExpandedType _ t -> redStep $ TypeAppl t t2 
+        KindedType t _ _ -> redStep $ TypeAppl t t2 
+        _ -> TypeAppl (redStep t1) t2
+    ExpandedType e t -> ExpandedType e $ redStep t
+    KindedType t k ps -> KindedType (redStep t) k ps
+    _ -> ty
+
+hasRedex :: Type -> Bool
+hasRedex ty = case ty of 
+    TypeAppl f a -> case f of 
+        TypeAbs _ _ _ -> True
+        ExpandedType _ t -> hasRedex $ TypeAppl t a
+        KindedType t _ _ -> hasRedex $ TypeAppl t a
+        _ -> hasRedex f
+    ExpandedType _ t -> hasRedex t
+    KindedType t _ _ -> hasRedex t
+    _ -> False
+
 {- | beta reduce type abstractions -}
 bRed :: Type -> Type
 bRed ty = case ty of
     TypeAppl t1 t2 -> let a = bRed t2 in case bRed t1 of
         TypeAbs (TypeArg i _ _ _ c _ _) b _ ->
           rename ( \ j k n -> if (j, n) == (i, c) then a else TypeName j k n)
                  $ bRed b
-        ExpandedType _ t -> bRed $ TypeAppl t1 t
-        KindedType t _ _ ->  bRed $ TypeAppl t1 t
+        ExpandedType _ t -> bRed $ TypeAppl t a
+        KindedType t _ _ ->  bRed $ TypeAppl t a
         f -> TypeAppl f a
     ExpandedType e t -> ExpandedType e $ bRed t
     KindedType t k ps -> KindedType (bRed t) k ps
@@ -278,6 +305,13 @@ expandAliases tm = if Map.null tm then id else expandAux tm
 
 -- | expand aliases in a type
 expandAux :: TypeMap -> Type -> Type
+expandAux tm ty = rename ( \ i k n ->
+                 case Map.lookup i tm of
+                      Just TypeInfo {typeDefn = AliasTypeDefn sc} -> 
+                          ExpandedType (TypeName i k n) $ schemeToTypeAbs sc
+                      _ -> TypeName i k n) ty
+
+{-
 expandAux tm t =
   let expandAppl ty = case ty of
         TypeAppl t1 t2 -> TypeAppl (expandAux tm t1) $ expandAux tm t2
@@ -298,6 +332,7 @@ expandAux tm t =
               _ -> expandAppl t
             _ -> expandAppl t
     _ -> expandAppl t
+-}
 
 -- | find unexpanded alias identifier
 hasAlias :: TypeMap -> Type -> [Diagnosis]

HasCASL/TypeDecl.hs

@@ -52,7 +52,7 @@ anaFormula ga at =
 anaVars :: TypeEnv -> Vars -> Type -> Result [VarDecl]
 anaVars _ (Var v) t = return [VarDecl v t Other nullRange]
 anaVars te (VarTuple vs _) t =
-    let (topTy, ts) = getTypeAppl t
+    let (topTy, ts) = getTypeAppl $ betaReduce t
         n = length ts
     in if n > 1 && lesserType te topTy (toType $ productId n) then
                if n == length vs then

HasCASL/Unify.hs

@@ -99,8 +99,8 @@ flatKind = mapKindV (const InVar) id . rawKindOfType
 
 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
+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
     (_, TypeAppl (TypeName l _ _) t2) | l == lazyTypeId ->
@@ -114,7 +114,7 @@ match tm rel p1@(b1, ty1) p2@(b2, ty2) = if flatKind ty1 == flatKind ty2
            then return eps
         else if v1 > 0 && b1 then return $ Map.singleton v1 ty2
         else if v2 > 0 && b2 then return $ Map.singleton v2 ty1
-{- the following two condition only guarantee that instScheme also matches for
+{- the following two conditions only guarantee that instScheme also matches for
    a partial function that is mapped to a total one.
    Maybe a subtype condition is better. -}
         else if not b1 && b2 && v1 == 0 && v2 == 0 && Set.member i1
@@ -130,12 +130,25 @@ match tm rel p1@(b1, ty1) p2@(b2, ty2) = if flatKind ty1 == flatKind ty2
         else uniResult "typename" ty1
                             "is not unifiable with type" ty2
     (_, TypeName _ _ _) -> match tm rel p2 p1
-    (TypeAppl f1 a1, TypeAppl f2 a2) -> do
-        s1 <- match tm rel (b1, f1) (b2, f2)
-        s2 <- match tm rel (b1, if b1 then subst s1 a1 else a1)
-                  (b2, if b2 then subst s1 a2 else a2)
-        return $ compSubst s1 s2
-    _ -> uniResult "type" ty1 "is not unifiable with type" ty2
+    (TypeAppl f1 a1, TypeAppl f2 a2) -> 
+      let res = do
+            s1 <- match tm rel (b1, f1) (b2, f2)
+            s2 <- match tm rel (b1, if b1 then subst s1 a1 else a1)
+                   (b2, if b2 then subst s1 a2 else a2)
+            return $ compSubst s1 s2
+          res1@(Result _ ms1) = if hasRedex ty1 then
+              match tm rel (b1, redStep ty1) (b2, ty2)
+              else fail "match1"
+          res2@(Result _ ms2) = if hasRedex ty2 then
+              match tm rel (b1, ty1) (b2, redStep ty2)
+              else fail "match2"
+      in case ms1 of
+               Nothing -> case ms2 of
+                   Nothing -> res 
+                   Just _ -> res2
+               Just _ -> res1
+    _ -> if ty1 == ty2 then return eps else 
+             uniResult "type" ty1 "is not unifiable with type" ty2
   else uniResult "type" ty1 "is not unifiable with differently kinded type" ty2
 
 -- | most general unifier via 'match'

HasCASL/VarDecl.hs

@@ -210,8 +210,8 @@ addOpId i oldSc attrs dfn =
            tm = typeMap e
            TypeScheme _ ty _ = sc
            ds = if placeCount i > 1 then
-                let (fty, fargs) = getTypeAppl ty in
-                   if lesserType e fty (toType $ arrowId PFunArr)
+                let (fty, fargs) = getTypeAppl $ betaReduce ty in
+                   if lesserType e  fty (toType $ arrowId PFunArr)
                       && length fargs == 2 then
                      let (pty, ts) = getTypeAppl (head fargs)
                          n = length ts in

HasCASL/test/Alias.hascasl.output

@@ -49,7 +49,7 @@ s  : Type %(var_1)%
 *** Error 19.9, unknown type variable  'a'
 *** Error 21.9, unknown type variable  'a'
 *** Error 23.9, unknown type variable  'a'
-*** Error 21.14-23.22, illegal recursive type synonym 'a7 a -> Unit'
+*** Error 21.9-23.22, illegal recursive type synonym 'a7 a -> Unit'
 *** Error 25.6, incompatible kind of: a2
   expected: Type -> Type -> Type
      found: Type -> Type