more informative Token.Fact: retain name of dynamic fact (without selection);
authorwenzelm
Thu Aug 14 16:20:14 2014 +0200 (2014-08-14)
changeset 57942e5bec882fdd0
parent 57941 57200bdc2aa7
child 57943 52c68f8126a8
more informative Token.Fact: retain name of dynamic fact (without selection);
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/token.ML
src/Pure/facts.ML
src/Pure/global_theory.ML
     1.1 --- a/src/Pure/Isar/args.ML	Thu Aug 14 14:28:11 2014 +0200
     1.2 +++ b/src/Pure/Isar/args.ML	Thu Aug 14 16:20:14 2014 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4    val named_text: (string -> string) -> string parser
     1.5    val named_typ: (string -> typ) -> typ parser
     1.6    val named_term: (string -> term) -> term parser
     1.7 -  val named_fact: (string -> thm list) -> thm list parser
     1.8 +  val named_fact: (string -> string option * thm list) -> thm list parser
     1.9    val named_attribute:
    1.10      (string * Position.T -> morphism -> attribute) -> (morphism -> attribute) parser
    1.11    val typ_abbrev: typ context_parser
    1.12 @@ -106,7 +106,7 @@
    1.13        | SOME (Token.Text s) => Pretty.str (quote s)
    1.14        | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T
    1.15        | SOME (Token.Term t) => Syntax.pretty_term ctxt t
    1.16 -      | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
    1.17 +      | SOME (Token.Fact (_, ths)) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
    1.18        | _ => Pretty.mark_str (Token.markup arg, Token.unparse arg));
    1.19    in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
    1.20  
    1.21 @@ -130,7 +130,7 @@
    1.22  fun transform_values phi = map_args (Token.map_value
    1.23    (fn Token.Typ T => Token.Typ (Morphism.typ phi T)
    1.24      | Token.Term t => Token.Term (Morphism.term phi t)
    1.25 -    | Token.Fact ths => Token.Fact (Morphism.fact phi ths)
    1.26 +    | Token.Fact (a, ths) => Token.Fact (a, Morphism.fact phi ths)
    1.27      | Token.Attribute att => Token.Attribute (Morphism.transform phi att)
    1.28      | tok => tok));
    1.29  
    1.30 @@ -212,15 +212,17 @@
    1.31  val internal_text = value (fn Token.Text s => s);
    1.32  val internal_typ = value (fn Token.Typ T => T);
    1.33  val internal_term = value (fn Token.Term t => t);
    1.34 -val internal_fact = value (fn Token.Fact ths => ths);
    1.35 +val internal_fact = value (fn Token.Fact (_, ths) => ths);
    1.36  val internal_attribute = value (fn Token.Attribute att => att);
    1.37  
    1.38  fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
    1.39  fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.inner_syntax_of);
    1.40  fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of);
    1.41  
    1.42 -fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
    1.43 -  alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of);
    1.44 +fun named_fact get =
    1.45 +  internal_fact ||
    1.46 +  named >> evaluate Token.Fact (get o Token.content_of) >> #2 ||
    1.47 +  alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of) >> #2;
    1.48  
    1.49  fun named_attribute att =
    1.50    internal_attribute ||
     2.1 --- a/src/Pure/Isar/attrib.ML	Thu Aug 14 14:28:11 2014 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Thu Aug 14 16:20:14 2014 +0200
     2.3 @@ -245,7 +245,9 @@
     2.4    let
     2.5      val get = Proof_Context.get_fact_generic context;
     2.6      val get_fact = get o Facts.Fact;
     2.7 -    fun get_named pos name = get (Facts.Named ((name, pos), NONE));
     2.8 +    fun get_named is_sel pos name =
     2.9 +      let val (a, ths) = get (Facts.Named ((name, pos), NONE))
    2.10 +      in (if is_sel then NONE else a, ths) end;
    2.11    in
    2.12      Parse.$$$ "[" |-- Args.attribs (check_name_generic context) --| Parse.$$$ "]" >> (fn srcs =>
    2.13        let
    2.14 @@ -255,9 +257,9 @@
    2.15      ||
    2.16      (Scan.ahead Args.alt_name -- Args.named_fact get_fact
    2.17        >> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
    2.18 -     Scan.ahead (Parse.position fact_name) :|-- (fn (name, pos) =>
    2.19 -      Args.named_fact (get_named pos) -- Scan.option thm_sel
    2.20 -        >> (fn (fact, sel) => (name, Facts.Named ((name, pos), sel), fact))))
    2.21 +     Scan.ahead (Parse.position fact_name -- Scan.option thm_sel) :|-- (fn ((name, pos), sel) =>
    2.22 +      Args.named_fact (get_named (is_some sel) pos) --| Scan.option thm_sel
    2.23 +        >> (fn fact => (name, Facts.Named ((name, pos), sel), fact))))
    2.24      -- Args.opt_attribs (check_name_generic context) >> (fn ((name, thmref, fact), srcs) =>
    2.25        let
    2.26          val ths = Facts.select thmref fact;
     3.1 --- a/src/Pure/Isar/proof_context.ML	Thu Aug 14 14:28:11 2014 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Aug 14 16:20:14 2014 +0200
     3.3 @@ -121,7 +121,7 @@
     3.4      (term list list * (Proof.context -> Proof.context)) * Proof.context
     3.5    val fact_tac: Proof.context -> thm list -> int -> tactic
     3.6    val some_fact_tac: Proof.context -> int -> tactic
     3.7 -  val get_fact_generic: Context.generic -> Facts.ref -> thm list
     3.8 +  val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list
     3.9    val get_fact: Proof.context -> Facts.ref -> thm list
    3.10    val get_fact_single: Proof.context -> Facts.ref -> thm
    3.11    val get_thms: Proof.context -> xstring -> thm list
    3.12 @@ -948,22 +948,27 @@
    3.13              [thm] => thm
    3.14            | [] => err "Failed to retrieve literal fact"
    3.15            | _ => err "Ambiguous specification of literal fact");
    3.16 -      in pick ("", Position.none) [thm] end
    3.17 -  | retrieve pick context (Facts.Named ((xname, pos), ivs)) =
    3.18 +      in pick true ("", Position.none) [thm] end
    3.19 +  | retrieve pick context (Facts.Named ((xname, pos), sel)) =
    3.20        let
    3.21          val thy = Context.theory_of context;
    3.22 -        val (name, thms) =
    3.23 +        fun immediate thm = {name = xname, static = true, thms = [Thm.transfer thy thm]};
    3.24 +        val {name, static, thms} =
    3.25            (case xname of
    3.26 -            "" => (xname, [Thm.transfer thy Drule.dummy_thm])
    3.27 -          | "_" => (xname, [Thm.transfer thy Drule.asm_rl])
    3.28 +            "" => immediate Drule.dummy_thm
    3.29 +          | "_" => immediate Drule.asm_rl
    3.30            | _ => retrieve_generic context (xname, pos));
    3.31 -      in pick (name, pos) (Facts.select (Facts.Named ((name, pos), ivs)) thms) end;
    3.32 +        val thms' = Facts.select (Facts.Named ((name, pos), sel)) thms;
    3.33 +      in pick (static orelse is_some sel) (name, pos) thms' end;
    3.34  
    3.35  in
    3.36  
    3.37 -val get_fact_generic = retrieve (K I);
    3.38 -val get_fact = retrieve (K I) o Context.Proof;
    3.39 -val get_fact_single = retrieve Facts.the_single o Context.Proof;
    3.40 +val get_fact_generic =
    3.41 +  retrieve (fn static => fn (name, _) => fn thms =>
    3.42 +    (if static then NONE else SOME name, thms));
    3.43 +
    3.44 +val get_fact = retrieve (K (K I)) o Context.Proof;
    3.45 +val get_fact_single = retrieve (K Facts.the_single) o Context.Proof;
    3.46  
    3.47  fun get_thms ctxt = get_fact ctxt o Facts.named;
    3.48  fun get_thm ctxt = get_fact_single ctxt o Facts.named;
     4.1 --- a/src/Pure/Isar/token.ML	Thu Aug 14 14:28:11 2014 +0200
     4.2 +++ b/src/Pure/Isar/token.ML	Thu Aug 14 16:20:14 2014 +0200
     4.3 @@ -12,7 +12,8 @@
     4.4      Error of string | Sync | EOF
     4.5    type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
     4.6    datatype value =
     4.7 -    Literal of bool * Markup.T | Text of string | Typ of typ | Term of term | Fact of thm list |
     4.8 +    Literal of bool * Markup.T | Text of string | Typ of typ | Term of term |
     4.9 +    Fact of string option * thm list |
    4.10      Attribute of morphism -> attribute | Files of file Exn.result list
    4.11    type T
    4.12    val str_of_kind: kind -> string
    4.13 @@ -57,7 +58,7 @@
    4.14    val mk_text: string -> T
    4.15    val mk_typ: typ -> T
    4.16    val mk_term: term -> T
    4.17 -  val mk_fact: thm list -> T
    4.18 +  val mk_fact: string option * thm list -> T
    4.19    val mk_attribute: (morphism -> attribute) -> T
    4.20    val init_assignable: T -> T
    4.21    val assign: value option -> T -> unit
    4.22 @@ -91,7 +92,7 @@
    4.23    Text of string |
    4.24    Typ of typ |
    4.25    Term of term |
    4.26 -  Fact of thm list |
    4.27 +  Fact of string option * thm list |  (*optional name for dynamic fact, i.e. fact "variable"*)
    4.28    Attribute of morphism -> attribute |
    4.29    Files of file Exn.result list;
    4.30  
     5.1 --- a/src/Pure/facts.ML	Thu Aug 14 14:28:11 2014 +0200
     5.2 +++ b/src/Pure/facts.ML	Thu Aug 14 16:20:14 2014 +0200
     5.3 @@ -29,7 +29,8 @@
     5.4    val extern: Proof.context -> T -> string -> xstring
     5.5    val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
     5.6    val lookup: Context.generic -> T -> string -> (bool * thm list) option
     5.7 -  val retrieve: Context.generic -> T -> xstring * Position.T -> string * thm list
     5.8 +  val retrieve: Context.generic -> T -> xstring * Position.T ->
     5.9 +    {name: string, static: bool, thms: thm list}
    5.10    val defined: T -> string -> bool
    5.11    val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
    5.12    val dest_static: bool -> T list -> T -> (string * thm list) list
    5.13 @@ -176,14 +177,18 @@
    5.14  fun retrieve context facts (xname, pos) =
    5.15    let
    5.16      val name = check context facts (xname, pos);
    5.17 -    val thms =
    5.18 +    val (static, thms) =
    5.19        (case lookup context facts name of
    5.20          SOME (static, thms) =>
    5.21            (if static then ()
    5.22             else Context_Position.report_generic context pos (Markup.dynamic_fact name);
    5.23 -           thms)
    5.24 +           (static, thms))
    5.25        | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
    5.26 -  in (name, map (Thm.transfer (Context.theory_of context)) thms) end;
    5.27 +  in
    5.28 +   {name = name,
    5.29 +    static = static,
    5.30 +    thms = map (Thm.transfer (Context.theory_of context)) thms}
    5.31 +  end;
    5.32  
    5.33  
    5.34  (* static content *)
     6.1 --- a/src/Pure/global_theory.ML	Thu Aug 14 14:28:11 2014 +0200
     6.2 +++ b/src/Pure/global_theory.ML	Thu Aug 14 16:20:14 2014 +0200
     6.3 @@ -72,7 +72,7 @@
     6.4  (* retrieve theorems *)
     6.5  
     6.6  fun get_thms thy xname =
     6.7 -  #2 (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none));
     6.8 +  #thms (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none));
     6.9  
    6.10  fun get_thm thy xname =
    6.11    Facts.the_single (xname, Position.none) (get_thms thy xname);