src/Pure/type_infer.ML
changeset 24504 0edc609e36fd
parent 24485 687bbb686ef9
child 24682 29306b20079b
     1.1 --- a/src/Pure/type_infer.ML	Fri Aug 31 23:17:20 2007 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Fri Aug 31 23:17:22 2007 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    val logicT: typ
     1.5    val polymorphicT: typ -> typ
     1.6    val constrain: term -> typ -> term
     1.7 +  val is_param: indexname -> bool
     1.8    val param: int -> string * sort -> typ
     1.9    val paramify_vars: typ -> typ
    1.10    val paramify_dummies: typ -> int -> typ * int
    1.11 @@ -39,7 +40,7 @@
    1.12  
    1.13  (* user parameters *)
    1.14  
    1.15 -fun is_param_default (x, _) = size x > 0 andalso ord x = ord "?";
    1.16 +fun is_param (x, _: int) = String.isPrefix "?" x;
    1.17  fun param i (x, S) = TVar (("?" ^ x, i), S);
    1.18  
    1.19  val paramify_vars = Term.map_atyps (fn TVar ((x, i), S) => param i (x, S) | T => T);
    1.20 @@ -100,12 +101,12 @@
    1.21  
    1.22  (* pretyp_of *)
    1.23  
    1.24 -fun pretyp_of is_param typ params =
    1.25 +fun pretyp_of is_para typ params =
    1.26    let
    1.27      val params' = fold_atyps
    1.28        (fn TVar (xi as (x, _), S) =>
    1.29            (fn ps =>
    1.30 -            if is_param xi andalso not (Vartab.defined ps xi)
    1.31 +            if is_para xi andalso not (Vartab.defined ps xi)
    1.32              then Vartab.update (xi, mk_param S) ps else ps)
    1.33          | _ => I) typ params;
    1.34  
    1.35 @@ -123,7 +124,7 @@
    1.36  
    1.37  (* preterm_of *)
    1.38  
    1.39 -fun preterm_of const_type is_param tm (vparams, params) =
    1.40 +fun preterm_of const_type is_para tm (vparams, params) =
    1.41    let
    1.42      fun add_vparm xi ps =
    1.43        if not (Vartab.defined ps xi) then
    1.44 @@ -138,7 +139,7 @@
    1.45        tm vparams;
    1.46      fun var_param xi = the (Vartab.lookup vparams' xi);
    1.47  
    1.48 -    val preT_of = pretyp_of is_param;
    1.49 +    val preT_of = pretyp_of is_para;
    1.50      fun polyT_of T = fst (pretyp_of (K true) T Vartab.empty);
    1.51  
    1.52      fun constraint T t ps =
    1.53 @@ -398,7 +399,7 @@
    1.54      (*convert to preterms/typs*)
    1.55      val (Ts', Tps) = fold_map (pretyp_of (K true)) Ts Vartab.empty;
    1.56      val (ts', (vps, ps)) =
    1.57 -      fold_map (preterm_of const_type is_param_default o constrain_vars) ts (Vartab.empty, Tps);
    1.58 +      fold_map (preterm_of const_type is_param o constrain_vars) ts (Vartab.empty, Tps);
    1.59  
    1.60      (*run type inference*)
    1.61      val tTs' = ListPair.map Constraint (ts', Ts');