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

@@ -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)

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)

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

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