From a716971174535184da7713ed308423e355a4aa66 Mon Sep 17 00:00:00 2001 From: Christian Maeder Date: Wed, 12 Sep 2007 16:56:40 +0000 Subject: [PATCH] joined redStep and hasStep into a single function git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@8844 cec4b9c1-7d33-0410-9eda-942365e851bb --- HasCASL/AsUtils.hs | 33 +++++++++++++-------------------- HasCASL/Constrain.hs | 25 ++++++++++++++----------- HasCASL/SubtypeDecl.hs | 5 +++-- HasCASL/Unify.hs | 17 +++++++++-------- 4 files changed, 39 insertions(+), 41 deletions(-) diff --git a/HasCASL/AsUtils.hs b/HasCASL/AsUtils.hs index fb2f06a6ae..bdec2cc39a 100644 --- a/HasCASL/AsUtils.hs +++ b/HasCASL/AsUtils.hs @@ -49,32 +49,24 @@ unitTypeId :: Id unitTypeId = simpleIdToId $ mkSimpleId unitTypeS -- | single step beta reduce type abstractions -redStep :: Type -> Type +redStep :: Type -> Maybe Type redStep ty = case ty of TypeAppl t1 t2 -> case t1 of - TypeAbs (TypeArg _ _ _ _ c _ _) b _ -> + TypeAbs (TypeArg _ _ _ _ c _ _) b _ -> Just $ foldType mapTypeRec { foldTypeName = \ t _ _ n -> if n == c then t2 else t , foldTypeAbs = \ t v1@(TypeArg _ _ _ _ n _ _) tb p -> if n == c then t else TypeAbs v1 tb p } 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 - --- | check if redStep will do one beta reduction step -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 + _ -> do + r1 <- redStep t1 + return $ TypeAppl r1 t2 + ExpandedType e t -> fmap (ExpandedType e) $ redStep t + KindedType t k ps -> do + r <- redStep t + return $ KindedType r k ps + _ -> Nothing -- | get top-level type constructor and its arguments and beta reduce getTypeAppl :: Type -> (Type, [Type]) @@ -85,8 +77,9 @@ getTypeApplAux :: Bool -> Type -> (Type, [Type]) getTypeApplAux b ty = let (t, args) = getTyAppl ty in (t, reverse args) where getTyAppl typ = case typ of - TypeAppl t1 t2 -> if b && hasRedex typ then getTyAppl (redStep typ) - else let (t, args) = getTyAppl t1 in (t, t2 : args) + TypeAppl t1 t2 -> case redStep typ of + Just r | b -> getTyAppl r + _ -> let (t, args) = getTyAppl t1 in (t, t2 : args) ExpandedType _ te -> let (t, args) = getTyAppl te in if null args then (typ, []) else (t, args) diff --git a/HasCASL/Constrain.hs b/HasCASL/Constrain.hs index 7fd3f477f7..91ee6c9224 100644 --- a/HasCASL/Constrain.hs +++ b/HasCASL/Constrain.hs @@ -159,9 +159,9 @@ 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 hasRedex t2 then shapeMgu te $ (t1, redStep t2) : rest else - if v1 > 0 then do + (TypeName _ _ v1, TypeAppl f a) -> case redStep t2 of + Just r2 -> shapeMgu te $ (t1, r2) : rest + Nothing -> if v1 > 0 then do vf <- toPairState $ freshTypeVarT f va <- toPairState $ freshTypeVarT a let s = Map.singleton v1 (TypeAppl vf va) @@ -180,10 +180,12 @@ shapeMgu te cs = 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" + (ry1, Result _ ms1) = case redStep t1 of + Just r1 -> (r1, shapeMatch (typeMap te) r1 t2) + Nothing -> (t1, fail "shapeMatch1") + (ry2, Result _ ms2) = case redStep t2 of + Just r2 -> (r2, shapeMatch (typeMap te) t1 r2) + Nothing -> (t2, fail "shapeMatch2") res = shapeMgu te $ (f1, f2) : case (rawKindOfType f1, rawKindOfType f2) of (FunKind CoVar _ _ _, @@ -194,8 +196,8 @@ shapeMgu te cs = in case ms1 of Nothing -> case ms2 of Nothing -> res - Just _ -> shapeMgu te $ (t1, redStep t2) : rest - Just _ -> shapeMgu te $ (redStep t1, t2) : rest + Just _ -> shapeMgu te $ (t1, ry2) : rest + Just _ -> shapeMgu te $ (ry1, t2) : rest _ -> if t1 == t2 then shapeMgu te rest else error ("shapeMgu2: " ++ showDoc t1 " < " ++ showDoc t2 "") @@ -283,8 +285,9 @@ monotonic v = foldType FoldTypeRec { foldTypeName = \ _ _ _ i -> (True, i /= v) , foldTypeAppl = \ t@(TypeAppl tf _) ~(f1, f2) (a1, a2) -> -- avoid evaluation of (f1, f2) if it is not needed by "~" - if hasRedex t then monotonic v $ redStep t else - case rawKindOfType tf of + case redStep t of + Just r -> monotonic v r + Nothing -> case rawKindOfType tf of FunKind CoVar _ _ _ -> (f1 && a1, f2 && a2) FunKind ContraVar _ _ _ -> (f1 && a2, f2 && a1) _ -> (f1 && a1 && a2, f2 && a1 && a2) diff --git a/HasCASL/SubtypeDecl.hs b/HasCASL/SubtypeDecl.hs index d52e22f6a8..1daeda98a1 100644 --- a/HasCASL/SubtypeDecl.hs +++ b/HasCASL/SubtypeDecl.hs @@ -67,8 +67,9 @@ addSuperType t ak p@(i, nAs) = case t of Nothing -> case t of TypeAppl (TypeName l _ _) tl | l == lazyTypeId -> addSuperType tl ak p - TypeAppl t1 t2 -> if hasRedex t then addSuperType (redStep t) ak p - else do + TypeAppl t1 t2 -> case redStep t of + Just r -> addSuperType r ak p + Nothing -> do j <- newTypeIdentifier i let rk = rawKindOfType t1 k = rawToKind rk diff --git a/HasCASL/Unify.hs b/HasCASL/Unify.hs index 0a5400a060..2a2d6041d9 100644 --- a/HasCASL/Unify.hs +++ b/HasCASL/Unify.hs @@ -145,8 +145,9 @@ match tm rel p1@(b1, ty1) p2@(b2, ty2) = else if b1 && not b2 && v1 == 0 && v2 == 0 && Set.member i2 (superIds tm i1) then return eps else uniResult "typename" ty1 "is not unifiable with typename" ty2 - (TypeName _ _ v1, _) -> - if hasRedex ty2 then match tm rel p1 (b2, redStep ty2) else + (TypeName _ _ v1, _) -> case redStep ty2 of + Just ry2 -> match tm rel p1 (b2, ry2) + Nothing -> if v1 > 0 && b1 then if null $ leaves (==v1) ty2 then return $ Map.singleton v1 ty2 @@ -160,12 +161,12 @@ match tm rel p1@(b1, ty1) p2@(b2, ty2) = 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) p2 - else fail "match1" - res2@(Result _ ms2) = if hasRedex ty2 then - match tm rel p1 (b2, redStep ty2) - else fail "match2" + res1@(Result _ ms1) = case redStep ty1 of + Just ry1 -> match tm rel (b1, ry1) p2 + Nothing -> fail "match1" + res2@(Result _ ms2) = case redStep ty2 of + Just ry2 -> match tm rel p1 (b2, ry2) + Nothing -> fail "match2" in case ms1 of Nothing -> case ms2 of Nothing -> res