differentiated renaming types for speed up

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

HasCASL/AsUtils.hs

@@ -53,7 +53,7 @@ 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
+            replTypeVar ( \ 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

HasCASL/FoldType.hs

@@ -50,18 +50,24 @@ foldType r t = case t of
     BracketType k ts p -> foldBracketType r t k (map (foldType r) ts) p
     MixfixType ts -> foldMixfixType r t $ map (foldType r) ts
 
--- | recursively substitute type names within a type
-rename :: (Id -> RawKind -> Int -> Type) -> Type -> Type
-rename m = foldType mapTypeRec
-  { foldTypeName = \ _ -> m
-  , foldTypeAbs = \ (TypeAbs v1@(TypeArg i _ _ _ c _ _) ty p) _ _ _ ->
-        TypeAbs v1 (rename ( \ j k n -> if (j, n) == (i, c) then
-                      TypeName j k n else  m j k n) ty) p
-  , foldExpandedType = \ (ExpandedType t1 _) r1 r2 -> case (t1, r1) of
+typeRenameRec :: (Id -> RawKind -> Int -> Type) -> FoldTypeRec Type
+typeRenameRec m = mapTypeRec { foldTypeName = \ _ -> m }
+
+-- | recursively substitute type alias names within a type
+replAlias :: (Id -> RawKind -> Int -> Type) -> Type -> Type
+replAlias m = foldType (typeRenameRec m)
+    { foldExpandedType = \ (ExpandedType t1 _) r1 r2 -> case (t1, r1) of
         (TypeName _ _ _, ExpandedType t3 _) | t1 == t3 ->
             ExpandedType t1 r2
-        _ -> ExpandedType r1 r2
-  }
+        _ -> ExpandedType r1 r2 }
+
+-- | recursively substitute type variable names within a type
+replTypeVar :: (Id -> RawKind -> Int -> Type) -> Type -> Type
+replTypeVar m = foldType (typeRenameRec m)
+  { foldTypeAbs = \ (TypeAbs v1@(TypeArg i _ _ _ c _ _) ty p) _ _ _ ->
+        TypeAbs v1 (replTypeVar ( \ j k n -> if (j, n) == (i, c) then
+                      TypeName j k n else  m j k n) ty) p
+  , foldExpandedType = \ (ExpandedType t1 _) _ r2 -> ExpandedType t1 r2 }
 
 -- | the type name components of a type
 leaves :: (Int -> Bool) -> Type -> [(Int, (Id, RawKind))]

HasCASL/Le.hs

@@ -90,7 +90,7 @@ starTypeInfo = TypeInfo rStar (Set.singleton universe) Set.empty NoTypeDefn
 -- | rename the type according to identifier map (for comorphisms)
 mapType :: IdMap -> Type -> Type
 mapType m ty = if Map.null m then ty else
-    rename ( \ i k n ->
+    replAlias ( \ i k n ->
                let t = TypeName i k n in
                if n == 0 then
                   case Map.lookup i m of

HasCASL/TypeAna.hs

@@ -220,7 +220,7 @@ 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 ->
+expandAux tm ty = replAlias ( \ i k n ->
                  case Map.lookup i tm of
                       Just TypeInfo {typeDefn = AliasTypeDefn s} ->
                           ExpandedType (TypeName i k n) s

HasCASL/Unify.hs

@@ -207,7 +207,7 @@ subsume tm a b =
     isJust $ maybeResult $ match tm (==) (False, a) (True, b)
 
 subst :: Subst -> Type -> Type
-subst m = rename (\ i k n ->
+subst m = if Map.null m then id else replTypeVar (\ i k n ->
                case Map.lookup n m of
                Just s -> s
                _ -> TypeName i k n)