src/Pure/type_infer.ML
changeset 14828 15d12761ba54
parent 14788 9776f0c747c8
child 14854 61bdf2ae4dc5
     1.1 --- a/src/Pure/type_infer.ML	Sat May 29 15:02:35 2004 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Sat May 29 15:03:59 2004 +0200
     1.3 @@ -10,14 +10,13 @@
     1.4    val anyT: sort -> typ
     1.5    val logicT: typ
     1.6    val polymorphicT: typ -> typ
     1.7 -  val appl_error: (term -> Pretty.T) -> (typ -> Pretty.T)
     1.8 -    -> string -> term -> typ -> term -> typ -> string list
     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 get_sort: Type.tsig -> (indexname -> sort option) -> (sort -> sort)
    1.14      -> (indexname * sort) list -> indexname -> sort
    1.15 -  val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T)
    1.16 +  val infer_types: Pretty.pp
    1.17      -> Type.tsig -> (string -> typ option) -> (indexname -> typ option)
    1.18      -> (indexname -> sort option) -> (string -> string) -> (typ -> typ)
    1.19      -> (sort -> sort) -> string list -> bool -> typ list -> term list
    1.20 @@ -253,16 +252,16 @@
    1.21  exception NO_UNIFIER of string;
    1.22  
    1.23  
    1.24 -fun unify classes arities =
    1.25 +fun unify pp classes arities =
    1.26    let
    1.27  
    1.28      (* adjust sorts of parameters *)
    1.29  
    1.30      fun not_in_sort x S' S =
    1.31 -      "Variable " ^ x ^ "::" ^ Sorts.str_of_sort S' ^ " not of sort " ^
    1.32 -        Sorts.str_of_sort S ^ ".";
    1.33 +      "Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^
    1.34 +        Pretty.string_of_sort pp S;
    1.35  
    1.36 -    fun no_domain (a, c) = "No way to get " ^ a ^ "::" ^ c ^ ".";
    1.37 +    fun no_domain (a, c) = "No way to get " ^ Pretty.string_of_arity pp (a, [], [c]);
    1.38  
    1.39      fun meet (_, []) = ()
    1.40        | meet (Link (r as (ref (Param S'))), S) =
    1.41 @@ -304,7 +303,7 @@
    1.42        | unif (T, Link (ref U)) = unif (T, U)
    1.43        | unif (PType (a, Ts), PType (b, Us)) =
    1.44            if a <> b then
    1.45 -            raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b ^ ".")
    1.46 +            raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b)
    1.47            else seq2 unif (Ts, Us)
    1.48        | unif (T, U) = if T = U then () else raise NO_UNIFIER "";
    1.49  
    1.50 @@ -314,24 +313,26 @@
    1.51  
    1.52  (** type inference **)
    1.53  
    1.54 -fun appl_error prt prT why t T u U =
    1.55 +fun appl_error pp why t T u U =
    1.56   ["Type error in application: " ^ why,
    1.57    "",
    1.58    Pretty.string_of (Pretty.block
    1.59 -    [Pretty.str "Operator:", Pretty.brk 2, prt t, Pretty.str " ::", Pretty.brk 1, prT T]),
    1.60 +    [Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t,
    1.61 +      Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]),
    1.62    Pretty.string_of (Pretty.block
    1.63 -    [Pretty.str "Operand:", Pretty.brk 3, prt u, Pretty.str " ::", Pretty.brk 1, prT U]),
    1.64 +    [Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u,
    1.65 +      Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]),
    1.66    ""];
    1.67  
    1.68  
    1.69  (* infer *)                                     (*DESTRUCTIVE*)
    1.70  
    1.71 -fun infer prt prT classes arities =
    1.72 +fun infer pp classes arities =
    1.73    let
    1.74      (* errors *)
    1.75  
    1.76      fun unif_failed msg =
    1.77 -      "Type unification failed" ^ (if msg = "" then "." else ": " ^ msg) ^ "\n";
    1.78 +      "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n";
    1.79  
    1.80      fun prep_output bs ts Ts =
    1.81        let
    1.82 @@ -349,10 +350,9 @@
    1.83          val ([t', u'], [T', U']) = prep_output bs [t, u] [T, U];
    1.84          val why =
    1.85            (case T' of
    1.86 -            Type ("fun", _) => "Incompatible operand type."
    1.87 -          | _ => "Operator not of function type.");
    1.88 -        val text = unif_failed msg ^
    1.89 -                   cat_lines (appl_error prt prT why t' T' u' U');
    1.90 +            Type ("fun", _) => "Incompatible operand type"
    1.91 +          | _ => "Operator not of function type");
    1.92 +        val text = unif_failed msg ^ cat_lines (appl_error pp why t' T' u' U');
    1.93        in raise TYPE (text, [T', U'], [t', u']) end;
    1.94  
    1.95      fun err_constraint msg bs t T U =
    1.96 @@ -361,17 +361,17 @@
    1.97          val text = cat_lines
    1.98           [unif_failed msg,
    1.99            "Cannot meet type constraint:", "",
   1.100 -          Pretty.string_of
   1.101 -           (Pretty.block [Pretty.str "Term:", Pretty.brk 2, prt t',
   1.102 -                          Pretty.str " ::", Pretty.brk 1, prT T']),
   1.103 -          Pretty.string_of
   1.104 -           (Pretty.block [Pretty.str "Type:", Pretty.brk 2, prT U']), ""];
   1.105 +          Pretty.string_of (Pretty.block
   1.106 +           [Pretty.str "Term:", Pretty.brk 2, Pretty.term pp t',
   1.107 +            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T']),
   1.108 +          Pretty.string_of (Pretty.block
   1.109 +           [Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp U']), ""];
   1.110        in raise TYPE (text, [T', U'], [t']) end;
   1.111  
   1.112  
   1.113      (* main *)
   1.114  
   1.115 -    val unif = unify classes arities;
   1.116 +    val unif = unify pp classes arities;
   1.117  
   1.118      fun inf _ (PConst (_, T)) = T
   1.119        | inf _ (PFree (_, T)) = T
   1.120 @@ -397,7 +397,7 @@
   1.121  
   1.122  (* basic_infer_types *)
   1.123  
   1.124 -fun basic_infer_types prt prT const_type classes arities used freeze is_param ts Ts =
   1.125 +fun basic_infer_types pp const_type classes arities used freeze is_param ts Ts =
   1.126    let
   1.127      (*convert to preterms/typs*)
   1.128      val (Tps, Ts') = pretyps_of (K true) ([], Ts);
   1.129 @@ -405,7 +405,7 @@
   1.130  
   1.131      (*run type inference*)
   1.132      val tTs' = ListPair.map Constraint (ts', Ts');
   1.133 -    val _ = seq (fn t => (infer prt prT classes arities t; ())) tTs';
   1.134 +    val _ = seq (fn t => (infer pp classes arities t; ())) tTs';
   1.135  
   1.136      (*collect result unifier*)
   1.137      fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); None)
   1.138 @@ -452,11 +452,9 @@
   1.139        xi = xi' andalso Type.eq_sort tsig (S, S');
   1.140  
   1.141      val env = gen_distinct eq (map (apsnd map_sort) raw_env);
   1.142 -    val _ =
   1.143 -      (case gen_duplicates eq_fst env of
   1.144 -        [] => ()
   1.145 -      | dups => error ("Inconsistent sort constraints for type variable(s) " ^
   1.146 -          commas (map (quote o Syntax.string_of_vname' o fst) dups)));
   1.147 +    val _ = (case gen_duplicates eq_fst env of [] => ()
   1.148 +      | dups => error ("Inconsistent sort constraints for type variable(s) "
   1.149 +          ^ commas_quote (map (Syntax.string_of_vname' o fst) dups)));
   1.150  
   1.151      fun get xi =
   1.152        (case (assoc (env, xi), def_sort xi) of
   1.153 @@ -516,7 +514,7 @@
   1.154    used: list of already used type variables
   1.155    freeze: if true then generated parameters are turned into TFrees, else TVars*)
   1.156  
   1.157 -fun infer_types prt prT tsig const_type def_type def_sort
   1.158 +fun infer_types pp tsig const_type def_type def_sort
   1.159      map_const map_type map_sort used freeze pat_Ts raw_ts =
   1.160    let
   1.161      val {classes, arities, ...} = Type.rep_tsig tsig;
   1.162 @@ -524,7 +522,7 @@
   1.163      val is_const = is_some o const_type;
   1.164      val raw_ts' =
   1.165        map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;
   1.166 -    val (ts, Ts, unifier) = basic_infer_types prt prT const_type
   1.167 +    val (ts, Ts, unifier) = basic_infer_types pp const_type
   1.168        classes arities used freeze is_param raw_ts' pat_Ts';
   1.169    in (ts, unifier) end;
   1.170