renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
--- a/NEWS Thu May 27 15:28:23 2010 +0200
+++ b/NEWS Thu May 27 17:41:27 2010 +0200
@@ -502,6 +502,7 @@
OuterParse ~> Parse
OuterSyntax ~> Outer_Syntax
SpecParse ~> Parse_Spec
+ TypeInfer ~> Type_Infer
Note that "open Legacy" simplifies porting of sources, but forgetting
to remove it again will complicate porting again in the future.
--- a/src/HOL/Import/proof_kernel.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Thu May 27 17:41:27 2010 +0200
@@ -229,7 +229,7 @@
val str =
setmp_CRITICAL show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
val u = Syntax.parse_term ctxt str
- |> TypeInfer.constrain T |> Syntax.check_term ctxt
+ |> Type_Infer.constrain T |> Syntax.check_term ctxt
in
if match u
then quote str
--- a/src/HOL/Tools/Function/function.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML Thu May 27 17:41:27 2010 +0200
@@ -149,7 +149,7 @@
end
val add_function =
- gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
+ gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
fun gen_function is_external prep default_constraint fixspec eqns config lthy =
@@ -163,7 +163,7 @@
end
val function =
- gen_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
+ gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
val function_cmd = gen_function true Specification.read_spec "_::type"
fun prepare_termination_proof prep_term raw_term_opt lthy =
--- a/src/HOL/Tools/Function/function_core.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Thu May 27 17:41:27 2010 +0200
@@ -879,7 +879,7 @@
val ranT = range_type fT
val default = Syntax.parse_term lthy default_str
- |> TypeInfer.constrain fT |> Syntax.check_term lthy
+ |> Type_Infer.constrain fT |> Syntax.check_term lthy
val (globals, ctxt') = fix_globals domT ranT fvar lthy
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu May 27 17:41:27 2010 +0200
@@ -254,7 +254,7 @@
SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
| NONE =>
(* Variable from the ATP, say "X1" *)
- TypeInfer.param 0 (a, HOLogic.typeS)
+ Type_Infer.param 0 (a, HOLogic.typeS)
end
(*Invert the table of translations between Isabelle and ATPs*)
@@ -453,7 +453,7 @@
val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us
in repair_tvar_sorts vt t end
fun check_formula ctxt =
- TypeInfer.constrain @{typ bool}
+ Type_Infer.constrain @{typ bool}
#> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
--- a/src/HOL/Tools/hologic.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/HOL/Tools/hologic.ML Thu May 27 17:41:27 2010 +0200
@@ -138,7 +138,7 @@
(* HOL syntax *)
val typeS: sort = ["HOL.type"];
-val typeT = TypeInfer.anyT typeS;
+val typeT = Type_Infer.anyT typeS;
(* bool and set *)
--- a/src/HOL/Tools/primrec.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/HOL/Tools/primrec.ML Thu May 27 17:41:27 2010 +0200
@@ -197,7 +197,7 @@
val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t)) (map snd ls @ [dummyT])
(list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
val rhs = singleton (Syntax.check_terms ctxt)
- (TypeInfer.constrain varT raw_rhs);
+ (Type_Infer.constrain varT raw_rhs);
in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end;
--- a/src/HOLCF/Tools/Domain/domain_library.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Thu May 27 17:41:27 2010 +0200
@@ -185,7 +185,7 @@
fun mk_lam (x,T) = Abs(x,dummyT,T);
fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P);
fun mk_ex (x,P) = mk_exists (x,dummyT,P);
-fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (typ --> boolT) (mk_lam(x,P)));
+fun mk_constrainall (x,typ,P) = %%:"All" $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
end
fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu May 27 17:41:27 2010 +0200
@@ -463,7 +463,7 @@
fun legacy_infer_term thy t =
singleton (Syntax.check_terms (ProofContext.init_global thy)) (intern_term thy t);
- fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
+ fun legacy_infer_prop thy t = legacy_infer_term thy (Type_Infer.constrain propT t);
fun infer_props thy = map (apsnd (legacy_infer_prop thy));
fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
--- a/src/Pure/Isar/class_target.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/Pure/Isar/class_target.ML Thu May 27 17:41:27 2010 +0200
@@ -275,7 +275,7 @@
of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
of SOME (_, ty' as TVar (vi, sort)) =>
- if TypeInfer.is_param vi
+ if Type_Infer.is_param vi
andalso Sorts.sort_le algebra (base_sort, sort)
then SOME (ty', TFree (Name.aT, base_sort))
else NONE
--- a/src/Pure/Isar/expression.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/Pure/Isar/expression.ML Thu May 27 17:41:27 2010 +0200
@@ -162,9 +162,9 @@
val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
(* type inference and contexts *)
- val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT_global) parm_types;
+ val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
- val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
+ val arg = type_parms @ map2 Type_Infer.constrain parm_types' insts';
val res = Syntax.check_terms ctxt arg;
val ctxt' = ctxt |> fold Variable.auto_fixes res;
@@ -345,9 +345,9 @@
let
val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
val inst' = prep_inst ctxt parm_names inst;
- val parm_types' = map (TypeInfer.paramify_vars o
+ val parm_types' = map (Type_Infer.paramify_vars o
Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global) parm_types;
- val inst'' = map2 TypeInfer.constrain parm_types' inst';
+ val inst'' = map2 Type_Infer.constrain parm_types' inst';
val insts' = insts @ [(loc, (prfx, inst''))];
val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
val inst''' = insts'' |> List.last |> snd |> snd;
--- a/src/Pure/Isar/proof_context.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu May 27 17:41:27 2010 +0200
@@ -577,7 +577,7 @@
pattern orelse schematic orelse
T |> Term.exists_subtype
(fn TVar (xi, _) =>
- not (TypeInfer.is_param xi) andalso
+ not (Type_Infer.is_param xi) andalso
error ("Illegal schematic type variable: " ^ Term.string_of_vname xi)
| _ => false)
in T end;
@@ -599,7 +599,7 @@
fun prepare_patterns ctxt =
let val Mode {pattern, ...} = get_mode ctxt in
- TypeInfer.fixate_params (Variable.names_of ctxt) #>
+ Type_Infer.fixate_params (Variable.names_of ctxt) #>
pattern ? Variable.polymorphic ctxt #>
(map o Term.map_types) (prepare_patternT ctxt) #>
(if pattern then prepare_dummies else map (check_dummies ctxt))
@@ -699,7 +699,7 @@
in Variable.def_type ctxt pattern end;
fun standard_infer_types ctxt ts =
- TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
+ Type_Infer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
(try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt)
(Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts
handle TYPE (msg, _, _) => error msg;
@@ -754,11 +754,11 @@
let
val {get_sort, map_const, map_free} = term_context ctxt;
- val (T', _) = TypeInfer.paramify_dummies T 0;
+ val (T', _) = Type_Infer.paramify_dummies T 0;
val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
val (syms, pos) = Syntax.parse_token markup text;
- fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
+ fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
handle ERROR msg => SOME msg;
val t =
Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
@@ -883,7 +883,7 @@
in
fun read_terms ctxt T =
- map (Syntax.parse_term ctxt #> TypeInfer.constrain T) #> Syntax.check_terms ctxt;
+ map (Syntax.parse_term ctxt #> Type_Infer.constrain T) #> Syntax.check_terms ctxt;
val match_bind = gen_bind read_terms;
val match_bind_i = gen_bind (fn ctxt => fn _ => map (cert_term ctxt));
--- a/src/Pure/Isar/rule_insts.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/Pure/Isar/rule_insts.ML Thu May 27 17:41:27 2010 +0200
@@ -82,7 +82,7 @@
fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
val ts = map2 parse Ts ss;
val ts' =
- map2 (TypeInfer.constrain o TypeInfer.paramify_vars) Ts ts
+ map2 (Type_Infer.constrain o Type_Infer.paramify_vars) Ts ts
|> Syntax.check_terms ((schematic ? ProofContext.set_mode ProofContext.mode_schematic) ctxt)
|> Variable.polymorphic ctxt;
val Ts' = map Term.fastype_of ts';
--- a/src/Pure/Isar/specification.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/Pure/Isar/specification.ML Thu May 27 17:41:27 2010 +0200
@@ -96,13 +96,13 @@
(case duplicates (op =) commons of [] => ()
| dups => error ("Duplicate local variables " ^ commas_quote dups));
val frees = rev ((fold o fold_aterms) add_free As (rev commons));
- val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
+ val types = map (Type_Infer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
| abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u
| abs_body lev y (t as Free (x, T)) =
- if x = y then TypeInfer.constrain (uniform_typing x) (TypeInfer.constrain T (Bound lev))
+ if x = y then Type_Infer.constrain (uniform_typing x) (Type_Infer.constrain T (Bound lev))
else t
| abs_body _ _ a = a;
fun close (y, U) B =
--- a/src/Pure/Proof/proof_syntax.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Thu May 27 17:41:27 2010 +0200
@@ -212,7 +212,7 @@
in
fn ty => fn s =>
(if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
- |> TypeInfer.constrain ty |> Syntax.check_term ctxt
+ |> Type_Infer.constrain ty |> Syntax.check_term ctxt
end;
fun read_proof thy =
--- a/src/Pure/ROOT.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/Pure/ROOT.ML Thu May 27 17:41:27 2010 +0200
@@ -309,6 +309,7 @@
structure OuterParse = Parse;
structure OuterSyntax = Outer_Syntax;
structure SpecParse = Parse_Spec;
+structure TypeInfer = Type_Infer;
end;
--- a/src/Pure/Thy/thy_output.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Thu May 27 17:41:27 2010 +0200
@@ -455,7 +455,7 @@
fun pretty_term_typ ctxt (style, t) =
let val t' = style t
- in pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t') t') end;
+ in pretty_term ctxt (Type_Infer.constrain (Term.fastype_of t') t') end;
fun pretty_term_typeof ctxt (style, t) =
Syntax.pretty_typ ctxt (Term.fastype_of (style t));
--- a/src/Pure/old_goals.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/Pure/old_goals.ML Thu May 27 17:41:27 2010 +0200
@@ -223,7 +223,7 @@
|> ProofContext.allow_dummies
|> ProofContext.set_mode ProofContext.mode_schematic;
val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
- in parse ctxt s |> TypeInfer.constrain T |> Syntax.check_term ctxt end;
+ in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
fun read_term thy = simple_read_term thy dummyT;
fun read_prop thy = simple_read_term thy propT;
--- a/src/Pure/sign.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/Pure/sign.ML Thu May 27 17:41:27 2010 +0200
@@ -271,7 +271,7 @@
val t' = subst_bounds (xs, t);
val u' = subst_bounds (xs, u);
val msg = cat_lines
- (TypeInfer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
+ (Type_Infer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
in raise TYPE (msg, [T, U], [t', u']) end;
fun typ_of (_, Const (_, T)) = T
--- a/src/Pure/type_infer.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/Pure/type_infer.ML Thu May 27 17:41:27 2010 +0200
@@ -20,7 +20,7 @@
term list -> term list
end;
-structure TypeInfer: TYPE_INFER =
+structure Type_Infer: TYPE_INFER =
struct
--- a/src/Pure/variable.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/Pure/variable.ML Thu May 27 17:41:27 2010 +0200
@@ -168,7 +168,7 @@
(case Vartab.lookup types xi of
NONE =>
if pattern then NONE
- else Vartab.lookup binds xi |> Option.map (TypeInfer.polymorphicT o #1)
+ else Vartab.lookup binds xi |> Option.map (Type_Infer.polymorphicT o #1)
| some => some)
end;
--- a/src/Tools/nbe.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/Tools/nbe.ML Thu May 27 17:41:27 2010 +0200
@@ -506,7 +506,7 @@
val ts' = take_until is_dict ts;
val c = const_of_idx idx;
val T = map_type_tvar (fn ((v, i), _) =>
- TypeInfer.param typidx (v ^ string_of_int i, []))
+ Type_Infer.param typidx (v ^ string_of_int i, []))
(Sign.the_const_type thy c);
val typidx' = typidx + 1;
in of_apps bounds (Term.Const (c, T), ts') typidx' end
@@ -548,9 +548,9 @@
let
val ty' = typ_of_itype program vs0 ty;
fun type_infer t =
- singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
+ singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
(try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
- (TypeInfer.constrain ty' t);
+ (Type_Infer.constrain ty' t);
fun check_tvars t = if null (Term.add_tvars t []) then t else
error ("Illegal schematic type variables in normalized term: "
^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t);
--- a/src/ZF/Tools/datatype_package.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/ZF/Tools/datatype_package.ML Thu May 27 17:41:27 2010 +0200
@@ -403,7 +403,7 @@
let
val ctxt = ProofContext.init_global thy;
fun read_is strs =
- map (Syntax.parse_term ctxt #> TypeInfer.constrain @{typ i}) strs
+ map (Syntax.parse_term ctxt #> Type_Infer.constrain @{typ i}) strs
|> Syntax.check_terms ctxt;
val rec_tms = read_is srec_tms;
--- a/src/ZF/Tools/inductive_package.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML Thu May 27 17:41:27 2010 +0200
@@ -555,7 +555,7 @@
(raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
let
val ctxt = ProofContext.init_global thy;
- val read_terms = map (Syntax.parse_term ctxt #> TypeInfer.constrain Ind_Syntax.iT)
+ val read_terms = map (Syntax.parse_term ctxt #> Type_Infer.constrain Ind_Syntax.iT)
#> Syntax.check_terms ctxt;
val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;
--- a/src/ZF/ind_syntax.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/ZF/ind_syntax.ML Thu May 27 17:41:27 2010 +0200
@@ -66,7 +66,7 @@
(*read a constructor specification*)
fun read_construct ctxt (id: string, sprems, syn: mixfix) =
- let val prems = map (Syntax.parse_term ctxt #> TypeInfer.constrain FOLogic.oT) sprems
+ let val prems = map (Syntax.parse_term ctxt #> Type_Infer.constrain FOLogic.oT) sprems
|> Syntax.check_terms ctxt
val args = map (#1 o dest_mem) prems
val T = (map (#2 o dest_Free) args) ---> iT