# HG changeset patch # User wenzelm # Date 1176640309 -7200 # Node ID 1e057a3f087d4f02105f2bf9a77072c4f31ba298 # Parent 290454649b8cdcd6201fd892786f84f35710bb6a proper ProofContext.infer_types; diff -r 290454649b8c -r 1e057a3f087d TFL/tfl.ML --- a/TFL/tfl.ML Sun Apr 15 14:31:47 2007 +0200 +++ b/TFL/tfl.ML Sun Apr 15 14:31:49 2007 +0200 @@ -367,9 +367,8 @@ (*For Isabelle, the lhs of a definition must be a constant.*) fun mk_const_def sign (c, Ty, rhs) = - Sign.infer_types (Sign.pp sign) sign (Sign.consts_of sign) (K NONE) (K NONE) Name.context false - ([Const("==",dummyT) $ Const(c,Ty) $ rhs], propT) - |> #1; + #1 (singleton (ProofContext.infer_types (ProofContext.init sign)) + (Const("==",dummyT) $ Const(Sign.full_name sign c,Ty) $ rhs, propT)); (*Make all TVars available for instantiation by adding a ? to the front*) fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts) diff -r 290454649b8c -r 1e057a3f087d src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Sun Apr 15 14:31:47 2007 +0200 +++ b/src/HOL/Nominal/nominal_primrec.ML Sun Apr 15 14:31:49 2007 +0200 @@ -206,10 +206,11 @@ val frees = ls @ x :: rs; val rhs = list_abs_free (frees, list_comb (Const (rec_name, dummyT), fs @ [Free x])) - val defpair = (Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def", - Logic.mk_equals (Const (fname, dummyT), rhs)); - val defpair' as (_, _ $ _ $ t) = Theory.inferT_axm thy defpair - in (defpair', subst_bounds (rev (map Free frees), strip_abs_body t)) end; + val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def"; + val def_prop as _ $ _ $ t = + singleton (ProofContext.infer_types (ProofContext.init thy)) + (Logic.mk_equals (Const (fname, dummyT), rhs), propT) |> #1; + in ((def_name, def_prop), subst_bounds (rev (map Free frees), strip_abs_body t)) end; (* find datatypes which contain all datatypes in tnames' *) diff -r 290454649b8c -r 1e057a3f087d src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Sun Apr 15 14:31:47 2007 +0200 +++ b/src/HOL/Tools/primrec_package.ML Sun Apr 15 14:31:49 2007 +0200 @@ -16,6 +16,7 @@ -> theory -> thm list * theory val add_primrec_unchecked_i: string -> ((bstring * term) * attribute list) list -> theory -> thm list * theory + (* FIXME !? *) val gen_primrec: ((bstring * attribute list) * thm list -> theory -> (bstring * thm list) * theory) -> ((bstring * attribute list) * term -> theory -> (bstring * thm) * theory) -> string -> ((bstring * attribute list) * term) list @@ -42,16 +43,16 @@ (* preprocessing of equations *) -fun process_eqn thy eq rec_fns = +fun process_eqn thy eq rec_fns = let - val (lhs, rhs) = + val (lhs, rhs) = if null (term_vars eq) then HOLogic.dest_eq (HOLogic.dest_Trueprop eq) handle TERM _ => raise RecError "not a proper equation" else raise RecError "illegal schematic variable(s)"; val (recfun, args) = strip_comb lhs; - val fnameT = dest_Const recfun handle TERM _ => + val fnameT = dest_Const recfun handle TERM _ => raise RecError "function is not declared as constant in theory"; val (ls', rest) = take_prefix is_Free args; @@ -73,7 +74,7 @@ fun check_vars _ [] = () | check_vars s vars = raise RecError (s ^ commas_quote (map fst vars)) in - if length middle > 1 then + if length middle > 1 then raise RecError "more than one non-variable in pattern" else (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees); @@ -147,14 +148,14 @@ let val recs = filter (is_rec_type o snd) (cargs' ~~ cargs); val rargs = map fst recs; - val subs = map (rpair dummyT o fst) + val subs = map (rpair dummyT o fst) (rev (rename_wrt_term rhs rargs)); - val (rhs', (fnameTs'', fnss'')) = + val (rhs', (fnameTs'', fnss'')) = (subst (map (fn ((x, y), z) => (Free x, (body_index y, Free z))) (recs ~~ subs)) rhs (fnameTs', fnss')) handle RecError s => primrec_eq_err thy s eq - in (fnameTs'', fnss'', + in (fnameTs'', fnss'', (list_abs_free (cargs' @ subs @ ls @ rs, rhs'))::fns) end) @@ -166,7 +167,7 @@ let val (_, _, eqns) = the (AList.lookup (op =) rec_eqns fnameT); val (fnameTs', fnss', fns) = fold_rev (trans eqns) constrs - ((i, fnameT)::fnameTs, fnss, []) + ((i, fnameT)::fnameTs, fnss, []) in (fnameTs', (i, (fname, #1 (snd (hd eqns)), fns))::fnss') end @@ -200,9 +201,11 @@ ((map snd ls) @ [dummyT]) (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 ::(length ls downto 1)))) - val defpair = (Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def", - Logic.mk_equals (Const (fname, dummyT), rhs)) - in Theory.inferT_axm thy defpair end; + val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def"; + val def_prop = + singleton (ProofContext.infer_types (ProofContext.init thy)) + (Logic.mk_equals (Const (fname, dummyT), rhs), propT) |> #1; + in (def_name, def_prop) end; (* find datatypes which contain all datatypes in tnames' *) @@ -236,12 +239,12 @@ val rec_eqns = fold_rev (process_eqn thy o snd) eqns [] ; val tnames = distinct (op =) (map (#1 o snd) rec_eqns); val dts = find_dts dt_info tnames tnames; - val main_fns = + val main_fns = map (fn (tname, {index, ...}) => - (index, + (index, (fst o the o find_first (fn f => (#1 o snd) f = tname)) rec_eqns)) dts; - val {descr, rec_names, rec_rewrites, ...} = + val {descr, rec_names, rec_rewrites, ...} = if null dts then primrec_err ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive") else snd (hd dts); @@ -308,7 +311,7 @@ fun gen_primrec note def alt_name specs = gen_primrec_i note def alt_name (map (fn ((name, t), atts) => ((name, atts), t)) specs); -end; (*local*) +end; (* outer syntax *) @@ -334,6 +337,4 @@ end; - end; - diff -r 290454649b8c -r 1e057a3f087d src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Sun Apr 15 14:31:47 2007 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Sun Apr 15 14:31:49 2007 +0200 @@ -282,12 +282,7 @@ vt0 holds the initial sort constraints, from the conjecture clauses.*) fun clause_of_strees_aux ctxt vt0 ts = let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts - val infer = Sign.infer_types (ProofContext.pp ctxt) (ProofContext.theory_of ctxt) - (ProofContext.consts_of ctxt) (Variable.def_type ctxt false) - (Variable.def_sort ctxt) (Variable.names_of ctxt) true - in - #1(infer ([fix_sorts vt dt], HOLogic.boolT)) - end; + in #1 (singleton (ProofContext.infer_types ctxt) (fix_sorts vt dt, HOLogic.boolT)) end; (*Quantification over a list of Vars. FUXNE: for term.ML??*) fun list_all_var ([], t: term) = t diff -r 290454649b8c -r 1e057a3f087d src/Pure/Isar/rule_insts.ML --- a/src/Pure/Isar/rule_insts.ML Sun Apr 15 14:31:47 2007 +0200 +++ b/src/Pure/Isar/rule_insts.ML Sun Apr 15 14:31:49 2007 +0200 @@ -131,8 +131,8 @@ let val ctxt' = ctxt |> Variable.declare_thm thm |> fold (fn a => Variable.declare_internal (Logic.mk_type (TFree (a, [])))) (Drule.add_used thm []); (* FIXME tmp *) - val tvars = Drule.fold_terms Term.add_tvars thm []; - val vars = Drule.fold_terms Term.add_vars thm []; + val tvars = Thm.fold_terms Term.add_tvars thm []; + val vars = Thm.fold_terms Term.add_vars thm []; val ((type_insts, term_insts), insts) = read_insts ctxt' (map snd mixed_insts) (tvars, vars); val _ = (*assign internalized values*) diff -r 290454649b8c -r 1e057a3f087d src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Sun Apr 15 14:31:47 2007 +0200 +++ b/src/Pure/Isar/theory_target.ML Sun Apr 15 14:31:49 2007 +0200 @@ -213,8 +213,8 @@ val nprems = Thm.nprems_of th' - Thm.nprems_of th; (*export fixes*) - val tfrees = map TFree (Drule.fold_terms Term.add_tfrees th' []); - val frees = map Free (Drule.fold_terms Term.add_frees th' []); + val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []); + val frees = map Free (Thm.fold_terms Term.add_frees th' []); val (th'' :: vs) = (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees)) |> Variable.export ctxt thy_ctxt |> Drule.zero_var_indexes_list; diff -r 290454649b8c -r 1e057a3f087d src/Pure/Tools/nbe.ML --- a/src/Pure/Tools/nbe.ML Sun Apr 15 14:31:47 2007 +0200 +++ b/src/Pure/Tools/nbe.ML Sun Apr 15 14:31:49 2007 +0200 @@ -148,8 +148,8 @@ error ("Illegal schematic type variables in normalized term: " ^ setmp show_types true (Sign.string_of_term thy) t); val ty = type_of t; - fun constrain t = Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy) - (K NONE) (K NONE) Name.context false ([t], ty) |> fst; + fun constrain t = (* FIXME really pat? *) + #1 (singleton (ProofContext.infer_types_pat (ProofContext.init thy)) (t, ty)); val _ = ensure_funs thy funcgr t; in t