renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
1.1 --- a/NEWS Thu May 27 15:28:23 2010 +0200
1.2 +++ b/NEWS Thu May 27 17:41:27 2010 +0200
1.3 @@ -502,6 +502,7 @@
1.4 OuterParse ~> Parse
1.5 OuterSyntax ~> Outer_Syntax
1.6 SpecParse ~> Parse_Spec
1.7 + TypeInfer ~> Type_Infer
1.8
1.9 Note that "open Legacy" simplifies porting of sources, but forgetting
1.10 to remove it again will complicate porting again in the future.
2.1 --- a/src/HOL/Import/proof_kernel.ML Thu May 27 15:28:23 2010 +0200
2.2 +++ b/src/HOL/Import/proof_kernel.ML Thu May 27 17:41:27 2010 +0200
2.3 @@ -229,7 +229,7 @@
2.4 val str =
2.5 setmp_CRITICAL show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
2.6 val u = Syntax.parse_term ctxt str
2.7 - |> TypeInfer.constrain T |> Syntax.check_term ctxt
2.8 + |> Type_Infer.constrain T |> Syntax.check_term ctxt
2.9 in
2.10 if match u
2.11 then quote str
3.1 --- a/src/HOL/Tools/Function/function.ML Thu May 27 15:28:23 2010 +0200
3.2 +++ b/src/HOL/Tools/Function/function.ML Thu May 27 17:41:27 2010 +0200
3.3 @@ -149,7 +149,7 @@
3.4 end
3.5
3.6 val add_function =
3.7 - gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
3.8 + gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
3.9 val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
3.10
3.11 fun gen_function is_external prep default_constraint fixspec eqns config lthy =
3.12 @@ -163,7 +163,7 @@
3.13 end
3.14
3.15 val function =
3.16 - gen_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
3.17 + gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
3.18 val function_cmd = gen_function true Specification.read_spec "_::type"
3.19
3.20 fun prepare_termination_proof prep_term raw_term_opt lthy =
4.1 --- a/src/HOL/Tools/Function/function_core.ML Thu May 27 15:28:23 2010 +0200
4.2 +++ b/src/HOL/Tools/Function/function_core.ML Thu May 27 17:41:27 2010 +0200
4.3 @@ -879,7 +879,7 @@
4.4 val ranT = range_type fT
4.5
4.6 val default = Syntax.parse_term lthy default_str
4.7 - |> TypeInfer.constrain fT |> Syntax.check_term lthy
4.8 + |> Type_Infer.constrain fT |> Syntax.check_term lthy
4.9
4.10 val (globals, ctxt') = fix_globals domT ranT fvar lthy
4.11
5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu May 27 15:28:23 2010 +0200
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu May 27 17:41:27 2010 +0200
5.3 @@ -254,7 +254,7 @@
5.4 SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
5.5 | NONE =>
5.6 (* Variable from the ATP, say "X1" *)
5.7 - TypeInfer.param 0 (a, HOLogic.typeS)
5.8 + Type_Infer.param 0 (a, HOLogic.typeS)
5.9 end
5.10
5.11 (*Invert the table of translations between Isabelle and ATPs*)
5.12 @@ -453,7 +453,7 @@
5.13 val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us
5.14 in repair_tvar_sorts vt t end
5.15 fun check_formula ctxt =
5.16 - TypeInfer.constrain @{typ bool}
5.17 + Type_Infer.constrain @{typ bool}
5.18 #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
5.19
5.20
6.1 --- a/src/HOL/Tools/hologic.ML Thu May 27 15:28:23 2010 +0200
6.2 +++ b/src/HOL/Tools/hologic.ML Thu May 27 17:41:27 2010 +0200
6.3 @@ -138,7 +138,7 @@
6.4 (* HOL syntax *)
6.5
6.6 val typeS: sort = ["HOL.type"];
6.7 -val typeT = TypeInfer.anyT typeS;
6.8 +val typeT = Type_Infer.anyT typeS;
6.9
6.10
6.11 (* bool and set *)
7.1 --- a/src/HOL/Tools/primrec.ML Thu May 27 15:28:23 2010 +0200
7.2 +++ b/src/HOL/Tools/primrec.ML Thu May 27 17:41:27 2010 +0200
7.3 @@ -197,7 +197,7 @@
7.4 val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t)) (map snd ls @ [dummyT])
7.5 (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
7.6 val rhs = singleton (Syntax.check_terms ctxt)
7.7 - (TypeInfer.constrain varT raw_rhs);
7.8 + (Type_Infer.constrain varT raw_rhs);
7.9 in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end;
7.10
7.11
8.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML Thu May 27 15:28:23 2010 +0200
8.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML Thu May 27 17:41:27 2010 +0200
8.3 @@ -185,7 +185,7 @@
8.4 fun mk_lam (x,T) = Abs(x,dummyT,T);
8.5 fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P);
8.6 fun mk_ex (x,P) = mk_exists (x,dummyT,P);
8.7 -fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (typ --> boolT) (mk_lam(x,P)));
8.8 +fun mk_constrainall (x,typ,P) = %%:"All" $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
8.9 end
8.10
8.11 fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
9.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu May 27 15:28:23 2010 +0200
9.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu May 27 17:41:27 2010 +0200
9.3 @@ -463,7 +463,7 @@
9.4
9.5 fun legacy_infer_term thy t =
9.6 singleton (Syntax.check_terms (ProofContext.init_global thy)) (intern_term thy t);
9.7 - fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
9.8 + fun legacy_infer_prop thy t = legacy_infer_term thy (Type_Infer.constrain propT t);
9.9 fun infer_props thy = map (apsnd (legacy_infer_prop thy));
9.10 fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
9.11 fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
10.1 --- a/src/Pure/Isar/class_target.ML Thu May 27 15:28:23 2010 +0200
10.2 +++ b/src/Pure/Isar/class_target.ML Thu May 27 17:41:27 2010 +0200
10.3 @@ -275,7 +275,7 @@
10.4 of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
10.5 of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
10.6 of SOME (_, ty' as TVar (vi, sort)) =>
10.7 - if TypeInfer.is_param vi
10.8 + if Type_Infer.is_param vi
10.9 andalso Sorts.sort_le algebra (base_sort, sort)
10.10 then SOME (ty', TFree (Name.aT, base_sort))
10.11 else NONE
11.1 --- a/src/Pure/Isar/expression.ML Thu May 27 15:28:23 2010 +0200
11.2 +++ b/src/Pure/Isar/expression.ML Thu May 27 17:41:27 2010 +0200
11.3 @@ -162,9 +162,9 @@
11.4 val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
11.5
11.6 (* type inference and contexts *)
11.7 - val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT_global) parm_types;
11.8 + val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
11.9 val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
11.10 - val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
11.11 + val arg = type_parms @ map2 Type_Infer.constrain parm_types' insts';
11.12 val res = Syntax.check_terms ctxt arg;
11.13 val ctxt' = ctxt |> fold Variable.auto_fixes res;
11.14
11.15 @@ -345,9 +345,9 @@
11.16 let
11.17 val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
11.18 val inst' = prep_inst ctxt parm_names inst;
11.19 - val parm_types' = map (TypeInfer.paramify_vars o
11.20 + val parm_types' = map (Type_Infer.paramify_vars o
11.21 Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global) parm_types;
11.22 - val inst'' = map2 TypeInfer.constrain parm_types' inst';
11.23 + val inst'' = map2 Type_Infer.constrain parm_types' inst';
11.24 val insts' = insts @ [(loc, (prfx, inst''))];
11.25 val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
11.26 val inst''' = insts'' |> List.last |> snd |> snd;
12.1 --- a/src/Pure/Isar/proof_context.ML Thu May 27 15:28:23 2010 +0200
12.2 +++ b/src/Pure/Isar/proof_context.ML Thu May 27 17:41:27 2010 +0200
12.3 @@ -577,7 +577,7 @@
12.4 pattern orelse schematic orelse
12.5 T |> Term.exists_subtype
12.6 (fn TVar (xi, _) =>
12.7 - not (TypeInfer.is_param xi) andalso
12.8 + not (Type_Infer.is_param xi) andalso
12.9 error ("Illegal schematic type variable: " ^ Term.string_of_vname xi)
12.10 | _ => false)
12.11 in T end;
12.12 @@ -599,7 +599,7 @@
12.13
12.14 fun prepare_patterns ctxt =
12.15 let val Mode {pattern, ...} = get_mode ctxt in
12.16 - TypeInfer.fixate_params (Variable.names_of ctxt) #>
12.17 + Type_Infer.fixate_params (Variable.names_of ctxt) #>
12.18 pattern ? Variable.polymorphic ctxt #>
12.19 (map o Term.map_types) (prepare_patternT ctxt) #>
12.20 (if pattern then prepare_dummies else map (check_dummies ctxt))
12.21 @@ -699,7 +699,7 @@
12.22 in Variable.def_type ctxt pattern end;
12.23
12.24 fun standard_infer_types ctxt ts =
12.25 - TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
12.26 + Type_Infer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
12.27 (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt)
12.28 (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts
12.29 handle TYPE (msg, _, _) => error msg;
12.30 @@ -754,11 +754,11 @@
12.31 let
12.32 val {get_sort, map_const, map_free} = term_context ctxt;
12.33
12.34 - val (T', _) = TypeInfer.paramify_dummies T 0;
12.35 + val (T', _) = Type_Infer.paramify_dummies T 0;
12.36 val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
12.37 val (syms, pos) = Syntax.parse_token markup text;
12.38
12.39 - fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
12.40 + fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
12.41 handle ERROR msg => SOME msg;
12.42 val t =
12.43 Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
12.44 @@ -883,7 +883,7 @@
12.45 in
12.46
12.47 fun read_terms ctxt T =
12.48 - map (Syntax.parse_term ctxt #> TypeInfer.constrain T) #> Syntax.check_terms ctxt;
12.49 + map (Syntax.parse_term ctxt #> Type_Infer.constrain T) #> Syntax.check_terms ctxt;
12.50
12.51 val match_bind = gen_bind read_terms;
12.52 val match_bind_i = gen_bind (fn ctxt => fn _ => map (cert_term ctxt));
13.1 --- a/src/Pure/Isar/rule_insts.ML Thu May 27 15:28:23 2010 +0200
13.2 +++ b/src/Pure/Isar/rule_insts.ML Thu May 27 17:41:27 2010 +0200
13.3 @@ -82,7 +82,7 @@
13.4 fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
13.5 val ts = map2 parse Ts ss;
13.6 val ts' =
13.7 - map2 (TypeInfer.constrain o TypeInfer.paramify_vars) Ts ts
13.8 + map2 (Type_Infer.constrain o Type_Infer.paramify_vars) Ts ts
13.9 |> Syntax.check_terms ((schematic ? ProofContext.set_mode ProofContext.mode_schematic) ctxt)
13.10 |> Variable.polymorphic ctxt;
13.11 val Ts' = map Term.fastype_of ts';
14.1 --- a/src/Pure/Isar/specification.ML Thu May 27 15:28:23 2010 +0200
14.2 +++ b/src/Pure/Isar/specification.ML Thu May 27 17:41:27 2010 +0200
14.3 @@ -96,13 +96,13 @@
14.4 (case duplicates (op =) commons of [] => ()
14.5 | dups => error ("Duplicate local variables " ^ commas_quote dups));
14.6 val frees = rev ((fold o fold_aterms) add_free As (rev commons));
14.7 - val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
14.8 + val types = map (Type_Infer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
14.9 val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
14.10
14.11 fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
14.12 | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u
14.13 | abs_body lev y (t as Free (x, T)) =
14.14 - if x = y then TypeInfer.constrain (uniform_typing x) (TypeInfer.constrain T (Bound lev))
14.15 + if x = y then Type_Infer.constrain (uniform_typing x) (Type_Infer.constrain T (Bound lev))
14.16 else t
14.17 | abs_body _ _ a = a;
14.18 fun close (y, U) B =
15.1 --- a/src/Pure/Proof/proof_syntax.ML Thu May 27 15:28:23 2010 +0200
15.2 +++ b/src/Pure/Proof/proof_syntax.ML Thu May 27 17:41:27 2010 +0200
15.3 @@ -212,7 +212,7 @@
15.4 in
15.5 fn ty => fn s =>
15.6 (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
15.7 - |> TypeInfer.constrain ty |> Syntax.check_term ctxt
15.8 + |> Type_Infer.constrain ty |> Syntax.check_term ctxt
15.9 end;
15.10
15.11 fun read_proof thy =
16.1 --- a/src/Pure/ROOT.ML Thu May 27 15:28:23 2010 +0200
16.2 +++ b/src/Pure/ROOT.ML Thu May 27 17:41:27 2010 +0200
16.3 @@ -309,6 +309,7 @@
16.4 structure OuterParse = Parse;
16.5 structure OuterSyntax = Outer_Syntax;
16.6 structure SpecParse = Parse_Spec;
16.7 +structure TypeInfer = Type_Infer;
16.8
16.9 end;
16.10
17.1 --- a/src/Pure/Thy/thy_output.ML Thu May 27 15:28:23 2010 +0200
17.2 +++ b/src/Pure/Thy/thy_output.ML Thu May 27 17:41:27 2010 +0200
17.3 @@ -455,7 +455,7 @@
17.4
17.5 fun pretty_term_typ ctxt (style, t) =
17.6 let val t' = style t
17.7 - in pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t') t') end;
17.8 + in pretty_term ctxt (Type_Infer.constrain (Term.fastype_of t') t') end;
17.9
17.10 fun pretty_term_typeof ctxt (style, t) =
17.11 Syntax.pretty_typ ctxt (Term.fastype_of (style t));
18.1 --- a/src/Pure/old_goals.ML Thu May 27 15:28:23 2010 +0200
18.2 +++ b/src/Pure/old_goals.ML Thu May 27 17:41:27 2010 +0200
18.3 @@ -223,7 +223,7 @@
18.4 |> ProofContext.allow_dummies
18.5 |> ProofContext.set_mode ProofContext.mode_schematic;
18.6 val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
18.7 - in parse ctxt s |> TypeInfer.constrain T |> Syntax.check_term ctxt end;
18.8 + in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
18.9
18.10 fun read_term thy = simple_read_term thy dummyT;
18.11 fun read_prop thy = simple_read_term thy propT;
19.1 --- a/src/Pure/sign.ML Thu May 27 15:28:23 2010 +0200
19.2 +++ b/src/Pure/sign.ML Thu May 27 17:41:27 2010 +0200
19.3 @@ -271,7 +271,7 @@
19.4 val t' = subst_bounds (xs, t);
19.5 val u' = subst_bounds (xs, u);
19.6 val msg = cat_lines
19.7 - (TypeInfer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
19.8 + (Type_Infer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
19.9 in raise TYPE (msg, [T, U], [t', u']) end;
19.10
19.11 fun typ_of (_, Const (_, T)) = T
20.1 --- a/src/Pure/type_infer.ML Thu May 27 15:28:23 2010 +0200
20.2 +++ b/src/Pure/type_infer.ML Thu May 27 17:41:27 2010 +0200
20.3 @@ -20,7 +20,7 @@
20.4 term list -> term list
20.5 end;
20.6
20.7 -structure TypeInfer: TYPE_INFER =
20.8 +structure Type_Infer: TYPE_INFER =
20.9 struct
20.10
20.11
21.1 --- a/src/Pure/variable.ML Thu May 27 15:28:23 2010 +0200
21.2 +++ b/src/Pure/variable.ML Thu May 27 17:41:27 2010 +0200
21.3 @@ -168,7 +168,7 @@
21.4 (case Vartab.lookup types xi of
21.5 NONE =>
21.6 if pattern then NONE
21.7 - else Vartab.lookup binds xi |> Option.map (TypeInfer.polymorphicT o #1)
21.8 + else Vartab.lookup binds xi |> Option.map (Type_Infer.polymorphicT o #1)
21.9 | some => some)
21.10 end;
21.11
22.1 --- a/src/Tools/nbe.ML Thu May 27 15:28:23 2010 +0200
22.2 +++ b/src/Tools/nbe.ML Thu May 27 17:41:27 2010 +0200
22.3 @@ -506,7 +506,7 @@
22.4 val ts' = take_until is_dict ts;
22.5 val c = const_of_idx idx;
22.6 val T = map_type_tvar (fn ((v, i), _) =>
22.7 - TypeInfer.param typidx (v ^ string_of_int i, []))
22.8 + Type_Infer.param typidx (v ^ string_of_int i, []))
22.9 (Sign.the_const_type thy c);
22.10 val typidx' = typidx + 1;
22.11 in of_apps bounds (Term.Const (c, T), ts') typidx' end
22.12 @@ -548,9 +548,9 @@
22.13 let
22.14 val ty' = typ_of_itype program vs0 ty;
22.15 fun type_infer t =
22.16 - singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
22.17 + singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
22.18 (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
22.19 - (TypeInfer.constrain ty' t);
22.20 + (Type_Infer.constrain ty' t);
22.21 fun check_tvars t = if null (Term.add_tvars t []) then t else
22.22 error ("Illegal schematic type variables in normalized term: "
22.23 ^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t);
23.1 --- a/src/ZF/Tools/datatype_package.ML Thu May 27 15:28:23 2010 +0200
23.2 +++ b/src/ZF/Tools/datatype_package.ML Thu May 27 17:41:27 2010 +0200
23.3 @@ -403,7 +403,7 @@
23.4 let
23.5 val ctxt = ProofContext.init_global thy;
23.6 fun read_is strs =
23.7 - map (Syntax.parse_term ctxt #> TypeInfer.constrain @{typ i}) strs
23.8 + map (Syntax.parse_term ctxt #> Type_Infer.constrain @{typ i}) strs
23.9 |> Syntax.check_terms ctxt;
23.10
23.11 val rec_tms = read_is srec_tms;
24.1 --- a/src/ZF/Tools/inductive_package.ML Thu May 27 15:28:23 2010 +0200
24.2 +++ b/src/ZF/Tools/inductive_package.ML Thu May 27 17:41:27 2010 +0200
24.3 @@ -555,7 +555,7 @@
24.4 (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
24.5 let
24.6 val ctxt = ProofContext.init_global thy;
24.7 - val read_terms = map (Syntax.parse_term ctxt #> TypeInfer.constrain Ind_Syntax.iT)
24.8 + val read_terms = map (Syntax.parse_term ctxt #> Type_Infer.constrain Ind_Syntax.iT)
24.9 #> Syntax.check_terms ctxt;
24.10
24.11 val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;
25.1 --- a/src/ZF/ind_syntax.ML Thu May 27 15:28:23 2010 +0200
25.2 +++ b/src/ZF/ind_syntax.ML Thu May 27 17:41:27 2010 +0200
25.3 @@ -66,7 +66,7 @@
25.4
25.5 (*read a constructor specification*)
25.6 fun read_construct ctxt (id: string, sprems, syn: mixfix) =
25.7 - let val prems = map (Syntax.parse_term ctxt #> TypeInfer.constrain FOLogic.oT) sprems
25.8 + let val prems = map (Syntax.parse_term ctxt #> Type_Infer.constrain FOLogic.oT) sprems
25.9 |> Syntax.check_terms ctxt
25.10 val args = map (#1 o dest_mem) prems
25.11 val T = (map (#2 o dest_Free) args) ---> iT