# HG changeset patch # User wenzelm # Date 1408026014 -7200 # Node ID e5bec882fdd0cd45ff85085c0e853266a28a3714 # Parent 57200bdc2aa78072059ea86e1adbeccab5d656ea more informative Token.Fact: retain name of dynamic fact (without selection); diff -r 57200bdc2aa7 -r e5bec882fdd0 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Thu Aug 14 14:28:11 2014 +0200 +++ b/src/Pure/Isar/args.ML Thu Aug 14 16:20:14 2014 +0200 @@ -51,7 +51,7 @@ val named_text: (string -> string) -> string parser val named_typ: (string -> typ) -> typ parser val named_term: (string -> term) -> term parser - val named_fact: (string -> thm list) -> thm list parser + val named_fact: (string -> string option * thm list) -> thm list parser val named_attribute: (string * Position.T -> morphism -> attribute) -> (morphism -> attribute) parser val typ_abbrev: typ context_parser @@ -106,7 +106,7 @@ | SOME (Token.Text s) => Pretty.str (quote s) | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T | SOME (Token.Term t) => Syntax.pretty_term ctxt t - | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) + | SOME (Token.Fact (_, ths)) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) | _ => Pretty.mark_str (Token.markup arg, Token.unparse arg)); in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end; @@ -130,7 +130,7 @@ fun transform_values phi = map_args (Token.map_value (fn Token.Typ T => Token.Typ (Morphism.typ phi T) | Token.Term t => Token.Term (Morphism.term phi t) - | Token.Fact ths => Token.Fact (Morphism.fact phi ths) + | Token.Fact (a, ths) => Token.Fact (a, Morphism.fact phi ths) | Token.Attribute att => Token.Attribute (Morphism.transform phi att) | tok => tok)); @@ -212,15 +212,17 @@ val internal_text = value (fn Token.Text s => s); val internal_typ = value (fn Token.Typ T => T); val internal_term = value (fn Token.Term t => t); -val internal_fact = value (fn Token.Fact ths => ths); +val internal_fact = value (fn Token.Fact (_, ths) => ths); val internal_attribute = value (fn Token.Attribute att => att); fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of); fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.inner_syntax_of); fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of); -fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) || - alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of); +fun named_fact get = + internal_fact || + named >> evaluate Token.Fact (get o Token.content_of) >> #2 || + alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of) >> #2; fun named_attribute att = internal_attribute || diff -r 57200bdc2aa7 -r e5bec882fdd0 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Thu Aug 14 14:28:11 2014 +0200 +++ b/src/Pure/Isar/attrib.ML Thu Aug 14 16:20:14 2014 +0200 @@ -245,7 +245,9 @@ let val get = Proof_Context.get_fact_generic context; val get_fact = get o Facts.Fact; - fun get_named pos name = get (Facts.Named ((name, pos), NONE)); + fun get_named is_sel pos name = + let val (a, ths) = get (Facts.Named ((name, pos), NONE)) + in (if is_sel then NONE else a, ths) end; in Parse.$$$ "[" |-- Args.attribs (check_name_generic context) --| Parse.$$$ "]" >> (fn srcs => let @@ -255,9 +257,9 @@ || (Scan.ahead Args.alt_name -- Args.named_fact get_fact >> (fn (s, fact) => ("", Facts.Fact s, fact)) || - Scan.ahead (Parse.position fact_name) :|-- (fn (name, pos) => - Args.named_fact (get_named pos) -- Scan.option thm_sel - >> (fn (fact, sel) => (name, Facts.Named ((name, pos), sel), fact)))) + Scan.ahead (Parse.position fact_name -- Scan.option thm_sel) :|-- (fn ((name, pos), sel) => + Args.named_fact (get_named (is_some sel) pos) --| Scan.option thm_sel + >> (fn fact => (name, Facts.Named ((name, pos), sel), fact)))) -- Args.opt_attribs (check_name_generic context) >> (fn ((name, thmref, fact), srcs) => let val ths = Facts.select thmref fact; diff -r 57200bdc2aa7 -r e5bec882fdd0 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Aug 14 14:28:11 2014 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Aug 14 16:20:14 2014 +0200 @@ -121,7 +121,7 @@ (term list list * (Proof.context -> Proof.context)) * Proof.context val fact_tac: Proof.context -> thm list -> int -> tactic val some_fact_tac: Proof.context -> int -> tactic - val get_fact_generic: Context.generic -> Facts.ref -> thm list + val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list val get_fact: Proof.context -> Facts.ref -> thm list val get_fact_single: Proof.context -> Facts.ref -> thm val get_thms: Proof.context -> xstring -> thm list @@ -948,22 +948,27 @@ [thm] => thm | [] => err "Failed to retrieve literal fact" | _ => err "Ambiguous specification of literal fact"); - in pick ("", Position.none) [thm] end - | retrieve pick context (Facts.Named ((xname, pos), ivs)) = + in pick true ("", Position.none) [thm] end + | retrieve pick context (Facts.Named ((xname, pos), sel)) = let val thy = Context.theory_of context; - val (name, thms) = + fun immediate thm = {name = xname, static = true, thms = [Thm.transfer thy thm]}; + val {name, static, thms} = (case xname of - "" => (xname, [Thm.transfer thy Drule.dummy_thm]) - | "_" => (xname, [Thm.transfer thy Drule.asm_rl]) + "" => immediate Drule.dummy_thm + | "_" => immediate Drule.asm_rl | _ => retrieve_generic context (xname, pos)); - in pick (name, pos) (Facts.select (Facts.Named ((name, pos), ivs)) thms) end; + val thms' = Facts.select (Facts.Named ((name, pos), sel)) thms; + in pick (static orelse is_some sel) (name, pos) thms' end; in -val get_fact_generic = retrieve (K I); -val get_fact = retrieve (K I) o Context.Proof; -val get_fact_single = retrieve Facts.the_single o Context.Proof; +val get_fact_generic = + retrieve (fn static => fn (name, _) => fn thms => + (if static then NONE else SOME name, thms)); + +val get_fact = retrieve (K (K I)) o Context.Proof; +val get_fact_single = retrieve (K Facts.the_single) o Context.Proof; fun get_thms ctxt = get_fact ctxt o Facts.named; fun get_thm ctxt = get_fact_single ctxt o Facts.named; diff -r 57200bdc2aa7 -r e5bec882fdd0 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Thu Aug 14 14:28:11 2014 +0200 +++ b/src/Pure/Isar/token.ML Thu Aug 14 16:20:14 2014 +0200 @@ -12,7 +12,8 @@ Error of string | Sync | EOF type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T} datatype value = - Literal of bool * Markup.T | Text of string | Typ of typ | Term of term | Fact of thm list | + Literal of bool * Markup.T | Text of string | Typ of typ | Term of term | + Fact of string option * thm list | Attribute of morphism -> attribute | Files of file Exn.result list type T val str_of_kind: kind -> string @@ -57,7 +58,7 @@ val mk_text: string -> T val mk_typ: typ -> T val mk_term: term -> T - val mk_fact: thm list -> T + val mk_fact: string option * thm list -> T val mk_attribute: (morphism -> attribute) -> T val init_assignable: T -> T val assign: value option -> T -> unit @@ -91,7 +92,7 @@ Text of string | Typ of typ | Term of term | - Fact of thm list | + Fact of string option * thm list | (*optional name for dynamic fact, i.e. fact "variable"*) Attribute of morphism -> attribute | Files of file Exn.result list; diff -r 57200bdc2aa7 -r e5bec882fdd0 src/Pure/facts.ML --- a/src/Pure/facts.ML Thu Aug 14 14:28:11 2014 +0200 +++ b/src/Pure/facts.ML Thu Aug 14 16:20:14 2014 +0200 @@ -29,7 +29,8 @@ val extern: Proof.context -> T -> string -> xstring val markup_extern: Proof.context -> T -> string -> Markup.T * xstring val lookup: Context.generic -> T -> string -> (bool * thm list) option - val retrieve: Context.generic -> T -> xstring * Position.T -> string * thm list + val retrieve: Context.generic -> T -> xstring * Position.T -> + {name: string, static: bool, thms: thm list} val defined: T -> string -> bool val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a val dest_static: bool -> T list -> T -> (string * thm list) list @@ -176,14 +177,18 @@ fun retrieve context facts (xname, pos) = let val name = check context facts (xname, pos); - val thms = + val (static, thms) = (case lookup context facts name of SOME (static, thms) => (if static then () else Context_Position.report_generic context pos (Markup.dynamic_fact name); - thms) + (static, thms)) | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos)); - in (name, map (Thm.transfer (Context.theory_of context)) thms) end; + in + {name = name, + static = static, + thms = map (Thm.transfer (Context.theory_of context)) thms} + end; (* static content *) diff -r 57200bdc2aa7 -r e5bec882fdd0 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Thu Aug 14 14:28:11 2014 +0200 +++ b/src/Pure/global_theory.ML Thu Aug 14 16:20:14 2014 +0200 @@ -72,7 +72,7 @@ (* retrieve theorems *) fun get_thms thy xname = - #2 (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none)); + #thms (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none)); fun get_thm thy xname = Facts.the_single (xname, Position.none) (get_thms thy xname);