# HG changeset patch # User wenzelm # Date 1467746601 -7200 # Node ID a528d24826c54e2b0f247b77fdb443ff21e66049 # Parent c22928719e198a58fd796f6b0aee6262119d9ed4# Parent ae07cd27ebf1886877b950315be77d1247613edd merged diff -r c22928719e19 -r a528d24826c5 src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Tue Jul 05 20:29:58 2016 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Tue Jul 05 21:23:21 2016 +0200 @@ -572,7 +572,7 @@ val forced_rhs = force_rty_type lthy rty_forced rhs val lhs = Free (Binding.name_of binding, qty) val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs) - val (_, prop') = Local_Defs.cert_def lthy prop + val (_, prop') = Local_Defs.cert_def lthy (K []) prop val (_, newrhs) = Local_Defs.abs_def prop' val var = ((#notes config = false ? Binding.concealed) binding, mx) val def_name = Thm.make_def_binding (#notes config) (#1 var) diff -r c22928719e19 -r a528d24826c5 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue Jul 05 20:29:58 2016 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Jul 05 21:23:21 2016 +0200 @@ -96,7 +96,8 @@ (Binding.empty_atts, definition_term) lthy |>> (snd #> snd); fun raw_def lthy = let - val ((_, rhs), prove) = Local_Defs.derived_def lthy {conditional = true} definition_term; + val ((_, rhs), prove) = + Local_Defs.derived_def lthy (K []) {conditional = true} definition_term; val ((_, (_, raw_th)), lthy) = Local_Theory.define ((Binding.concealed pcrel_name, NoSyn), (Binding.empty_atts, rhs)) lthy; diff -r c22928719e19 -r a528d24826c5 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Tue Jul 05 20:29:58 2016 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Tue Jul 05 21:23:21 2016 +0200 @@ -58,7 +58,7 @@ val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (rty, qty) $ rhs val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm)) - val (_, prop') = Local_Defs.cert_def lthy prop + val (_, prop') = Local_Defs.cert_def lthy (K []) prop val (_, newrhs) = Local_Defs.abs_def prop' val ((trm, (_ , def_thm)), lthy') = diff -r c22928719e19 -r a528d24826c5 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Tue Jul 05 20:29:58 2016 +0200 +++ b/src/HOL/Tools/inductive.ML Tue Jul 05 21:23:21 2016 +0200 @@ -1039,7 +1039,7 @@ let val _ = Binding.is_empty name andalso null atts orelse error "Abbreviations may not have names or attributes"; - val ((x, T), rhs) = Local_Defs.abs_def (snd (Local_Defs.cert_def ctxt1 t)); + val ((x, T), rhs) = Local_Defs.abs_def (snd (Local_Defs.cert_def ctxt1 (K []) t)); val var = (case find_first (fn ((c, _), _) => Binding.name_of c = x) cnames_syn of NONE => error ("Undeclared head of abbreviation " ^ quote x) diff -r c22928719e19 -r a528d24826c5 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Tue Jul 05 20:29:58 2016 +0200 +++ b/src/Pure/Isar/element.ML Tue Jul 05 21:23:21 2016 +0200 @@ -492,7 +492,7 @@ let val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs; val asms = defs' |> map (fn (b, (t, ps)) => - let val (_, t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *) + let val (_, t') = Local_Defs.cert_def ctxt (K []) t (* FIXME adapt ps? *) in (t', (b, [(t', ps)])) end); val (_, ctxt') = ctxt |> fold Variable.auto_fixes (map #1 asms) @@ -517,7 +517,8 @@ (case (map_ctxt_attrib o map) Token.init_assignable elem of Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => - ((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt t)))) a, atts), + ((Thm.def_binding_optional + (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt (K []) t)))) a, atts), (t, ps)))) | e => e); val ctxt' = Context.proof_map (init elem') ctxt; diff -r c22928719e19 -r a528d24826c5 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Tue Jul 05 20:29:58 2016 +0200 +++ b/src/Pure/Isar/expression.ML Tue Jul 05 21:23:21 2016 +0200 @@ -330,7 +330,7 @@ Assumes asms => Assumes (asms |> map (fn (a, propps) => (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) => - let val ((c, _), t') = Local_Defs.cert_def ctxt (close_frees t) + let val ((c, _), t') = Local_Defs.cert_def ctxt (K []) (close_frees t) in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end)) | e => e) end; @@ -540,7 +540,7 @@ fun bind_def ctxt eq (xs, env, eqs) = let - val _ = Local_Defs.cert_def ctxt eq; + val _ = Local_Defs.cert_def ctxt (K []) eq; val ((y, T), b) = Local_Defs.abs_def eq; val b' = norm_term env b; fun err msg = error (msg ^ ": " ^ quote y); diff -r c22928719e19 -r a528d24826c5 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Tue Jul 05 20:29:58 2016 +0200 +++ b/src/Pure/Isar/local_defs.ML Tue Jul 05 21:23:21 2016 +0200 @@ -6,7 +6,7 @@ signature LOCAL_DEFS = sig - val cert_def: Proof.context -> term -> (string * typ) * term + val cert_def: Proof.context -> (string -> Position.T list) -> term -> (string * typ) * term val abs_def: term -> (string * typ) * term val expand: cterm list -> thm -> thm val def_export: Assumption.export @@ -33,8 +33,8 @@ val unfold0_tac: Proof.context -> thm list -> tactic val fold: Proof.context -> thm list -> thm -> thm val fold_tac: Proof.context -> thm list -> tactic - val derived_def: Proof.context -> {conditional: bool} -> term -> - ((string * typ) * term) * (Proof.context -> thm -> thm) + val derived_def: Proof.context -> (string -> Position.T list) -> {conditional: bool} -> + term -> ((string * typ) * term) * (Proof.context -> thm -> thm) end; structure Local_Defs: LOCAL_DEFS = @@ -44,12 +44,12 @@ (* prepare defs *) -fun cert_def ctxt eq = +fun cert_def ctxt get_pos eq = let fun err msg = cat_error msg ("The error(s) above occurred in definition:\n" ^ quote (Syntax.string_of_term ctxt eq)); - val ((lhs, _), eq') = eq + val ((lhs, _), args, eq') = eq |> Sign.no_vars ctxt |> Primitive_Defs.dest_def ctxt {check_head = Term.is_Free, @@ -57,6 +57,9 @@ check_free_rhs = if Variable.is_body ctxt then K true else Variable.is_fixed ctxt, check_tfree = K true} handle TERM (msg, _) => err msg | ERROR msg => err msg; + val _ = + Context_Position.reports ctxt + (maps (fn Free (x, _) => Syntax_Phases.reports_of_scope (get_pos x) | _ => []) args); in (Term.dest_Free (Term.head_of lhs), eq') end; val abs_def = Primitive_Defs.abs_def #>> Term.dest_Free; @@ -121,7 +124,7 @@ |> Variable.declare_term rhs |> Proof_Context.add_fixes [(x, SOME T, mx)]; val lhs = Free (x', T); - val _ = cert_def ctxt' (Logic.mk_equals (lhs, rhs)); + val _ = cert_def ctxt' (K []) (Logic.mk_equals (lhs, rhs)); fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]); val (_, ctxt'') = Assumption.add_assms abbrev_export [] ctxt'; in ((lhs, rhs), ctxt'') end; @@ -240,14 +243,14 @@ (* derived defs -- potentially within the object-logic *) -fun derived_def ctxt {conditional} prop = +fun derived_def ctxt get_pos {conditional} prop = let val ((c, T), rhs) = prop |> Thm.cterm_of ctxt |> meta_rewrite_conv ctxt |> (snd o Logic.dest_equals o Thm.prop_of) |> conditional ? Logic.strip_imp_concl - |> (abs_def o #2 o cert_def ctxt); + |> (abs_def o #2 o cert_def ctxt get_pos); fun prove ctxt' def = Goal.prove ctxt' ((not (Variable.is_body ctxt') ? Variable.add_free_names ctxt' prop) []) [] prop diff -r c22928719e19 -r a528d24826c5 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Tue Jul 05 20:29:58 2016 +0200 +++ b/src/Pure/Isar/proof.ML Tue Jul 05 21:23:21 2016 +0200 @@ -862,7 +862,7 @@ (if null more_decls then "" else " ") ^ "wrt. definitions " ^ commas (map (show_term o Free o #1 o #1) more_defs)); - val derived_def = Local_Defs.derived_def ctxt {conditional = false}; + val derived_def = Local_Defs.derived_def ctxt (K []) {conditional = false}; val defs1 = map (derived_def o Logic.close_prop (map #2 fixes) []) (flat propss); val defs2 = match_defs decls defs1; val (defs3, defs_ctxt) = Local_Defs.define defs2 ctxt; diff -r c22928719e19 -r a528d24826c5 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Tue Jul 05 20:29:58 2016 +0200 +++ b/src/Pure/Isar/specification.ML Tue Jul 05 21:23:21 2016 +0200 @@ -11,11 +11,11 @@ term list * Proof.context val check_spec_open: (binding * typ option * mixfix) list -> (binding * typ option * mixfix) list -> term list -> term -> Proof.context -> - ((binding * typ option * mixfix) list * string list * (string -> Position.T) * term) * + ((binding * typ option * mixfix) list * string list * (string -> Position.T list) * term) * Proof.context val read_spec_open: (binding * string option * mixfix) list -> (binding * string option * mixfix) list -> string list -> string -> Proof.context -> - ((binding * typ option * mixfix) list * string list * (string -> Position.T) * term) * + ((binding * typ option * mixfix) list * string list * (string -> Position.T list) * term) * Proof.context type multi_specs = ((Attrib.binding * term) * term list * (binding * typ option * mixfix) list) list @@ -93,6 +93,19 @@ (* prepare specification *) +fun get_positions ctxt x = + let + fun get Cs (Const ("_type_constraint_", C) $ t) = get (C :: Cs) t + | get Cs (Free (y, T)) = + if x = y then + map_filter Term_Position.decode_positionT + (T :: map (Type.constraint_type ctxt) Cs) + else [] + | get _ (t $ u) = get [] t @ get [] u + | get _ (Abs (_, _, t)) = get [] t + | get _ _ = []; + in get [] end; + local fun prep_decls prep_var raw_vars ctxt = @@ -109,7 +122,12 @@ in ((vars, xs), ctxt'') end; fun close_form ctxt ys prems concl = - let val xs = rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) (rev ys)); + let + val xs = rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) (rev ys)); + + val pos_props = Logic.strip_imp_concl concl :: Logic.strip_imp_prems concl @ prems; + fun get_pos x = maps (get_positions ctxt x) pos_props; + val _ = Context_Position.reports ctxt (maps (Syntax_Phases.reports_of_scope o get_pos) xs); in Logic.close_prop_constraint (Variable.default_type ctxt) (xs ~~ xs) prems concl end; fun dummy_frees ctxt xs tss = @@ -120,19 +138,6 @@ val (tss', _) = (fold_map o fold_map) Term.free_dummy_patterns tss names; in tss' end; -fun get_positions ctxt x = - let - fun get Cs (Const ("_type_constraint_", C) $ t) = get (C :: Cs) t - | get _ (t $ u) = get [] t @ get [] u - | get _ (Abs (_, _, t)) = get [] t - | get Cs (Free (y, T)) = - if x = y then - map_filter Term_Position.decode_positionT - (T :: map (Type.constraint_type ctxt) Cs) - else [] - | get _ _ = []; - in get [] end; - fun prep_spec_open prep_var parse_prop raw_vars raw_params raw_prems raw_concl ctxt = let val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt; @@ -146,10 +151,7 @@ val spec = Logic.list_implies (prems, concl); val spec_ctxt = Variable.declare_term spec params_ctxt; - fun get_pos x = - (case maps (get_positions spec_ctxt x) props of - [] => Position.none - | pos :: _ => pos); + fun get_pos x = maps (get_positions spec_ctxt x) props; in ((vars, xs, get_pos, spec), spec_ctxt) end; fun prep_specs prep_var parse_prop prep_att raw_vars raw_specss ctxt = @@ -240,13 +242,13 @@ let val atts = map (prep_att lthy) raw_atts; - val ((vars, xs, get_pos, spec), spec_ctxt) = lthy + val ((vars, xs, get_pos, spec), _) = lthy |> prep_spec (the_list raw_var) raw_params raw_prems raw_spec; - val (((x, T), rhs), prove) = Local_Defs.derived_def lthy {conditional = true} spec; + val (((x, T), rhs), prove) = Local_Defs.derived_def lthy get_pos {conditional = true} spec; val _ = Name.reject_internal (x, []); val (b, mx) = (case (vars, xs) of - ([], []) => (Binding.make (x, get_pos x), NoSyn) + ([], []) => (Binding.make (x, (case get_pos x of [] => Position.none | p :: _ => p)), NoSyn) | ([(b, _, mx)], [y]) => if x = y then (b, mx) else @@ -279,14 +281,14 @@ fun gen_abbrev prep_spec mode raw_var raw_params raw_spec int lthy = let val lthy1 = lthy |> Proof_Context.set_syntax_mode mode; - val ((vars, xs, get_pos, spec), spec_ctxt) = lthy + val ((vars, xs, get_pos, spec), _) = lthy |> Proof_Context.set_mode Proof_Context.mode_abbrev |> prep_spec (the_list raw_var) raw_params [] raw_spec; - val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 spec)); + val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 get_pos spec)); val _ = Name.reject_internal (x, []); val (b, mx) = (case (vars, xs) of - ([], []) => (Binding.make (x, get_pos x), NoSyn) + ([], []) => (Binding.make (x, (case get_pos x of [] => Position.none | p :: _ => p)), NoSyn) | ([(b, _, mx)], [y]) => if x = y then (b, mx) else diff -r c22928719e19 -r a528d24826c5 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Tue Jul 05 20:29:58 2016 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Tue Jul 05 21:23:21 2016 +0200 @@ -7,6 +7,7 @@ signature SYNTAX_PHASES = sig + val reports_of_scope: Position.T list -> Position.report list val decode_sort: term -> sort val decode_typ: term -> typ val decode_term: Proof.context -> @@ -77,6 +78,20 @@ +(** reports of implicit variable scope **) + +fun reports_of_scope [] = [] + | reports_of_scope (def_pos :: ps) = + let + val id = serial (); + fun entity def = (Markup.entityN, Position.entity_properties_of def id def_pos); + in + map (rpair Markup.bound) (def_pos :: ps) @ + ((def_pos, entity true) :: map (rpair (entity false)) ps) + end; + + + (** decode parse trees **) (* decode_sort *) diff -r c22928719e19 -r a528d24826c5 src/Pure/primitive_defs.ML --- a/src/Pure/primitive_defs.ML Tue Jul 05 20:29:58 2016 +0200 +++ b/src/Pure/primitive_defs.ML Tue Jul 05 21:23:21 2016 +0200 @@ -11,7 +11,7 @@ check_free_lhs: string -> bool, check_free_rhs: string -> bool, check_tfree: string -> bool} -> - term -> (term * term) * term + term -> (term * term) * term list * term val abs_def: term -> term * term end; @@ -68,7 +68,8 @@ else if exists_subterm (fn t => t aconv head) rhs then err "Entity to be defined occurs on rhs" else - ((lhs, rhs), fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs))))) + ((lhs, rhs), args, + fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs))))) end; (*!!x. c x == t[x] to c == %x. t[x]*) diff -r c22928719e19 -r a528d24826c5 src/Pure/theory.ML --- a/src/Pure/theory.ML Tue Jul 05 20:29:58 2016 +0200 +++ b/src/Pure/theory.ML Tue Jul 05 21:23:21 2016 +0200 @@ -291,7 +291,7 @@ fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs = let val name = Sign.full_name thy b; - val ((lhs, rhs), _) = + val ((lhs, rhs), _, _) = Primitive_Defs.dest_def ctxt {check_head = Term.is_Const, check_free_lhs = K true,