tuned interface of unify, param;
authorwenzelm
Tue Dec 18 02:18:38 2001 +0100 (2001-12-18 ago)
changeset 12528b8bc541a4544
parent 12527 d6c91bc3e49c
child 12529 d99716a53f59
tuned interface of unify, param;
added paramify_dummies to turn TypeInfer.anyT into unifiable parameter;
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Tue Dec 18 02:17:20 2001 +0100
     1.2 +++ b/src/Pure/type.ML	Tue Dec 18 02:18:38 2001 +0100
     1.3 @@ -62,14 +62,15 @@
     1.4  
     1.5    (*type unification*)
     1.6    exception TUNIFY
     1.7 -  val unify: type_sig -> int -> typ Vartab.table -> typ * typ -> typ Vartab.table * int
     1.8 +  val unify: type_sig -> typ Vartab.table * int -> typ * typ -> typ Vartab.table * int
     1.9    val raw_unify: typ * typ -> bool
    1.10  
    1.11    (*type inference*)
    1.12    val get_sort: type_sig -> (indexname -> sort option) -> (sort -> sort)
    1.13      -> (indexname * sort) list -> indexname -> sort
    1.14    val constrain: term -> typ -> term
    1.15 -  val param: string list -> string * sort -> typ
    1.16 +  val param: int -> string * sort -> typ
    1.17 +  val paramify_dummies: int * typ -> int * typ
    1.18    val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T)
    1.19      -> type_sig -> (string -> typ option) -> (indexname -> typ option)
    1.20      -> (indexname -> sort option) -> (string -> string) -> (typ -> typ)
    1.21 @@ -760,9 +761,10 @@
    1.22  fun add_env (vT as (v, T), tab) = Vartab.update_new (vT, Vartab.map
    1.23    (fn (U as (TVar (w, S))) => if eq_ix (v, w) then T else U | U => U) tab);
    1.24  
    1.25 +
    1.26  (* unify *)
    1.27  
    1.28 -fun unify (tsig as TySg {classrel, arities, ...}) maxidx tyenv TU =
    1.29 +fun unify (tsig as TySg {classrel, arities, ...}) (tyenv, maxidx) TU =
    1.30    let
    1.31      val tyvar_count = ref maxidx;
    1.32      fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
    1.33 @@ -803,16 +805,14 @@
    1.34            if a <> b then raise TUNIFY
    1.35            else foldr unif (Ts ~~ Us, tye)
    1.36        | (T, U) => if T = U then tye else raise TUNIFY);
    1.37 -  in
    1.38 -    (unif (TU, tyenv), ! tyvar_count)
    1.39 -  end;
    1.40 +  in (unif (TU, tyenv), ! tyvar_count) end;
    1.41  
    1.42  
    1.43  (* raw_unify *)
    1.44  
    1.45  (*purely structural unification -- ignores sorts*)
    1.46  fun raw_unify (ty1, ty2) =
    1.47 -  (unify tsig0 0 Vartab.empty (rem_sorts ty1, rem_sorts ty2); true)
    1.48 +  (unify tsig0 (Vartab.empty, 0) (rem_sorts ty1, rem_sorts ty2); true)
    1.49      handle TUNIFY => false;
    1.50  
    1.51  
    1.52 @@ -855,7 +855,13 @@
    1.53  (* user parameters *)
    1.54  
    1.55  fun is_param (x, _) = size x > 0 andalso ord x = ord "?";
    1.56 -fun param used (x, S) = TVar ((variant used ("?" ^ x), 0), S);
    1.57 +fun param i (x, S) = TVar (("?" ^ x, i), S);
    1.58 +
    1.59 +fun paramify_dummies (i, TFree ("'_dummy_", S)) = (i + 1, param i ("'dummy", S))
    1.60 +  | paramify_dummies (i, Type (a, Ts)) =
    1.61 +      let val (i', Ts') = foldl_map paramify_dummies (i, Ts)
    1.62 +      in (i', Type (a, Ts')) end
    1.63 +  | paramify_dummies arg = arg;
    1.64  
    1.65  
    1.66  (* decode_types *)