--- a/src/HOL/Tools/Lifting/lifting_def.ML Tue Jul 05 10:32:25 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Tue Jul 05 14:20:27 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)
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue Jul 05 10:32:25 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Jul 05 14:20:27 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;
--- a/src/HOL/Tools/Quotient/quotient_def.ML Tue Jul 05 10:32:25 2016 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Tue Jul 05 14:20:27 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') =
--- a/src/HOL/Tools/inductive.ML Tue Jul 05 10:32:25 2016 +0200
+++ b/src/HOL/Tools/inductive.ML Tue Jul 05 14:20:27 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)
--- a/src/Pure/Isar/element.ML Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/Isar/element.ML Tue Jul 05 14:20:27 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;
--- a/src/Pure/Isar/expression.ML Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/Isar/expression.ML Tue Jul 05 14:20:27 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);
--- a/src/Pure/Isar/local_defs.ML Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/Isar/local_defs.ML Tue Jul 05 14:20:27 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
--- a/src/Pure/Isar/proof.ML Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/Isar/proof.ML Tue Jul 05 14:20:27 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;
--- a/src/Pure/Isar/specification.ML Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/Isar/specification.ML Tue Jul 05 14:20:27 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
@@ -146,10 +146,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 =
@@ -242,11 +239,11 @@
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
@@ -282,11 +279,11 @@
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
--- a/src/Pure/Syntax/syntax_phases.ML Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Tue Jul 05 14:20:27 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 *)
--- a/src/Pure/primitive_defs.ML Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/primitive_defs.ML Tue Jul 05 14:20:27 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]*)
--- a/src/Pure/theory.ML Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/theory.ML Tue Jul 05 14:20:27 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,