# HG changeset patch
# User wenzelm
# Date 896123506 -7200
# Node ID 30c49821e61faca0e75550e85b42b04b745a6b57
# Parent  a7538e43896e45b25347a8745e9dd7960369c540
remove seq2, scan (use seq2, foldl_map from library.ML);

diff -r a7538e43896e -r 30c49821e61f src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Mon May 25 21:10:45 1998 +0200
+++ b/src/Pure/type_infer.ML	Mon May 25 21:11:46 1998 +0200
@@ -17,21 +17,6 @@
 struct
 
 
-(** generic utils **)
-
-fun seq2 _ [] [] = ()
-  | seq2 f (x :: xs) (y :: ys) = (f x y; seq2 f xs ys)
-  | seq2 _ _ _ = raise LIST "seq2";
-
-fun scan _ (xs, []) = (xs, [])
-  | scan f (xs, y :: ys) =
-      let
-        val (xs', y') = f (xs, y);
-        val (xs'', ys') = scan f (xs', ys);
-      in (xs'', y' :: ys') end;
-
-
-
 (** term encodings **)
 
 (*
@@ -126,7 +111,7 @@
           else PType (a, map pre_of Ts);
   in (params', pre_of typ) end;
 
-fun pretyps_of is_param = scan (pretyp_of is_param);
+fun pretyps_of is_param = foldl_map (pretyp_of is_param);
 
 
 (* preterm(s)_of *)
@@ -182,7 +167,7 @@
     ((vparams', params'), tm')
   end;
 
-fun preterms_of const_type is_param = scan (preterm_of const_type is_param);
+fun preterms_of const_type is_param = foldl_map (preterm_of const_type is_param);
 
 
 
@@ -232,15 +217,15 @@
 
 fun typs_terms_of used mk_var prfx (Ts, ts) =
   let
-    fun elim (r as ref (Param S)) x = r := mk_var (x, S)
-      | elim _ _ = ();
+    fun elim (r as ref (Param S), x) = r := mk_var (x, S)
+      | elim _ = ();
 
     val used' = foldl add_names (foldl add_namesT (used, Ts), ts);
     val parms = rev (foldl add_parms (foldl add_parmsT ([], Ts), ts));
     val pre_names = replicate (length parms) (prfx ^ "'");
     val names = variantlist (pre_names, prfx ^ "'" :: used');
   in
-    seq2 elim parms names;
+    seq2 elim (parms, names);
     (map simple_typ_of Ts, map simple_term_of ts)
   end;
 
@@ -260,21 +245,21 @@
       "Variable " ^ x ^ "::" ^ Sorts.str_of_sort S' ^ " not of sort " ^
         Sorts.str_of_sort S ^ ".";
 
-    fun meet _ [] = ()
-      | meet (Link (r as (ref (Param S')))) S =
+    fun meet (_, []) = ()
+      | meet (Link (r as (ref (Param S'))), S) =
           if Sorts.sort_le classrel (S', S) then ()
           else r := mk_param (Sorts.inter_sort classrel (S', S))
-      | meet (Link (ref T)) S = meet T S
-      | meet (PType (a, Ts)) S =
-          seq2 meet Ts (Sorts.mg_domain classrel arities a S
+      | meet (Link (ref T), S) = meet (T, S)
+      | meet (PType (a, Ts), S) =
+          seq2 meet (Ts, Sorts.mg_domain classrel arities a S
             handle TYPE (msg, _, _) => raise NO_UNIFIER msg)
-      | meet (PTFree (x, S')) S =
+      | meet (PTFree (x, S'), S) =
           if Sorts.sort_le classrel (S', S) then ()
           else raise NO_UNIFIER (not_in_sort x S' S)
-      | meet (PTVar (xi, S')) S =
+      | meet (PTVar (xi, S'), S) =
           if Sorts.sort_le classrel (S', S) then ()
           else raise NO_UNIFIER (not_in_sort (Syntax.string_of_vname xi) S' S)
-      | meet (Param _) _ = sys_error "meet";
+      | meet (Param _, _) = sys_error "meet";
 
 
     (* occurs check and assigment *)
@@ -288,21 +273,21 @@
     fun assign r T S =
       (case deref T of
         T' as Link (r' as ref (Param _)) =>
-          if r = r' then () else (r := T'; meet T' S)
-      | T' => (occurs_check r T'; r := T'; meet T' S));
+          if r = r' then () else (r := T'; meet (T', S))
+      | T' => (occurs_check r T'; r := T'; meet (T', S)));
 
 
     (* unification *)
 
-    fun unif (Link (r as ref (Param S))) T = assign r T S
-      | unif T (Link (r as ref (Param S))) = assign r T S
-      | unif (Link (ref T)) U = unif T U
-      | unif T (Link (ref U)) = unif T U
-      | unif (PType (a, Ts)) (PType (b, Us)) =
+    fun unif (Link (r as ref (Param S)), T) = assign r T S
+      | unif (T, Link (r as ref (Param S))) = assign r T S
+      | unif (Link (ref T), U) = unif (T, U)
+      | unif (T, Link (ref U)) = unif (T, U)
+      | unif (PType (a, Ts), PType (b, Us)) =
           if a <> b then
             raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b ^ ".")
-          else seq2 unif Ts Us
-      | unif T U = if T = U then () else raise NO_UNIFIER "";
+          else seq2 unif (Ts, Us)
+      | unif (T, U) = if T = U then () else raise NO_UNIFIER "";
 
   in unif end;
 
@@ -378,11 +363,11 @@
             val U = inf bs u;
             val V = mk_param [];
             val U_to_V = PType ("fun", [U, V]);
-            val _ = unif U_to_V T handle NO_UNIFIER msg => err_appl msg bs t T u U;
+            val _ = unif (U_to_V, T) handle NO_UNIFIER msg => err_appl msg bs t T u U;
           in V end
       | inf bs (Constraint (t, U)) =
           let val T = inf bs t in
-            unif T U handle NO_UNIFIER msg => err_constraint msg bs t T U;
+            unif (T, U) handle NO_UNIFIER msg => err_constraint msg bs t T U;
             T
           end;
 
@@ -416,4 +401,5 @@
     (final_ts, final_Ts, final_env)
   end;
 
+
 end;