src/Pure/type_infer.ML
changeset 18339 64cb06a0bb50
parent 17496 26535df536ae
child 18939 18e2a2676d80
     1.1 --- a/src/Pure/type_infer.ML	Fri Dec 02 22:54:47 2005 +0100
     1.2 +++ b/src/Pure/type_infer.ML	Fri Dec 02 22:54:48 2005 +0100
     1.3 @@ -9,11 +9,12 @@
     1.4  sig
     1.5    val anyT: sort -> typ
     1.6    val logicT: typ
     1.7 +  val mixfixT: Syntax.mixfix -> typ
     1.8    val polymorphicT: typ -> typ
     1.9    val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list
    1.10    val constrain: term -> typ -> term
    1.11    val param: int -> string * sort -> typ
    1.12 -  val paramify_dummies: int * typ -> int * typ
    1.13 +  val paramify_dummies: typ -> int -> typ * int
    1.14    val get_sort: Type.tsig -> (indexname -> sort option) -> (sort -> sort)
    1.15      -> (indexname * sort) list -> indexname -> sort
    1.16    val infer_types: Pretty.pp
    1.17 @@ -105,6 +106,10 @@
    1.18  fun anyT S = TFree ("'_dummy_", S);
    1.19  val logicT = anyT [];
    1.20  
    1.21 +fun mixfixT (Binder _) = (logicT --> logicT) --> logicT
    1.22 +  | mixfixT mx = replicate (Syntax.mixfix_args mx) logicT ---> logicT;
    1.23 +
    1.24 +
    1.25  (*indicate polymorphic Vars*)
    1.26  fun polymorphicT T = Type ("_polymorphic_", [T]);
    1.27  
    1.28 @@ -436,12 +441,17 @@
    1.29  fun is_param (x, _) = size x > 0 andalso ord x = ord "?";
    1.30  fun param i (x, S) = TVar (("?" ^ x, i), S);
    1.31  
    1.32 -fun paramify_dummies (maxidx, TFree ("'_dummy_", S)) =
    1.33 -      (maxidx + 1, param (maxidx + 1) ("'dummy", S))
    1.34 -  | paramify_dummies (maxidx, Type (a, Ts)) =
    1.35 -      let val (maxidx', Ts') = foldl_map paramify_dummies (maxidx, Ts)
    1.36 -      in (maxidx', Type (a, Ts')) end
    1.37 -  | paramify_dummies arg = arg;
    1.38 +val paramify_dummies =
    1.39 +  let
    1.40 +    fun dummy S maxidx = (param (maxidx + 1) ("'dummy", S), maxidx + 1);
    1.41 +
    1.42 +    fun paramify (TFree ("'_dummy_", S)) maxidx = dummy S maxidx
    1.43 +      | paramify (Type ("dummy", _)) maxidx = dummy [] maxidx
    1.44 +      | paramify (Type (a, Ts)) maxidx =
    1.45 +          let val (Ts', maxidx') = fold_map paramify Ts maxidx
    1.46 +          in (Type (a, Ts'), maxidx') end
    1.47 +      | paramify T maxidx = (T, maxidx);
    1.48 +  in paramify end;
    1.49  
    1.50  
    1.51  (* decode sort constraints *)