clarified treatment of individual theorems;
authorwenzelm
Fri Aug 16 11:40:13 2019 +0200 (4 days ago)
changeset 705462970fdc230cc
parent 70545 b93ba98e627a
child 70548 87dffe9700bd
child 70550 8bc7e54bead9
clarified treatment of individual theorems;
tuned messages;
src/Pure/facts.ML
     1.1 --- a/src/Pure/facts.ML	Fri Aug 16 10:33:25 2019 +0200
     1.2 +++ b/src/Pure/facts.ML	Fri Aug 16 11:40:13 2019 +0200
     1.3 @@ -44,6 +44,10 @@
     1.4    val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
     1.5    val del: string -> T -> T
     1.6    val hide: bool -> string -> T -> T
     1.7 +  type thm_name = string * int
     1.8 +  val thm_name_ord: thm_name * thm_name -> order
     1.9 +  val single_thm_name: string -> thm_name
    1.10 +  val get_thm: Context.generic -> T -> thm_name * Position.T -> thm
    1.11  end;
    1.12  
    1.13  structure Facts: FACTS =
    1.14 @@ -51,10 +55,18 @@
    1.15  
    1.16  (** fact references **)
    1.17  
    1.18 -fun the_single _ [th] : thm = th
    1.19 -  | the_single (name, pos) ths =
    1.20 -      error ("Expected singleton fact " ^ quote name ^
    1.21 -        " (length " ^ string_of_int (length ths) ^ ")" ^ Position.here pos);
    1.22 +fun length_msg (thms: thm list) pos =
    1.23 +  " (length " ^ string_of_int (length thms) ^ ")" ^ Position.here pos;
    1.24 +
    1.25 +fun err_single (name, pos) thms =
    1.26 +  error ("Expected singleton fact " ^ quote name ^ length_msg thms pos);
    1.27 +
    1.28 +fun err_selection (name, pos) i thms =
    1.29 +  error ("Bad fact selection " ^ quote (name ^ enclose "(" ")" (string_of_int i)) ^
    1.30 +    length_msg thms pos);
    1.31 +
    1.32 +fun the_single _ [thm] = thm
    1.33 +  | the_single name_pos thms = err_single name_pos thms;
    1.34  
    1.35  
    1.36  (* datatype interval *)
    1.37 @@ -108,12 +120,10 @@
    1.38    | select (Named ((name, pos), SOME ivs)) ths =
    1.39        let
    1.40          val n = length ths;
    1.41 -        fun err msg =
    1.42 -          error (msg ^ " for fact " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
    1.43 -            Position.here pos);
    1.44 +        fun err msg = error (msg ^ " for fact " ^ quote name ^ length_msg ths pos);
    1.45          fun sel i =
    1.46 -          if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
    1.47 -          else nth ths (i - 1);
    1.48 +          if i > 0 andalso i <= n then nth ths (i - 1)
    1.49 +          else err_selection (name, pos) i ths;
    1.50          val is = maps (interval n) ivs handle Fail msg => err msg;
    1.51        in map sel is end;
    1.52  
    1.53 @@ -288,4 +298,27 @@
    1.54  fun hide fully name (Facts {facts, props}) =
    1.55    make_facts (Name_Space.hide_table fully name facts) props;
    1.56  
    1.57 +
    1.58 +
    1.59 +(** get individual theorems **)
    1.60 +
    1.61 +type thm_name = string * int;
    1.62 +val thm_name_ord = prod_ord string_ord int_ord;
    1.63 +
    1.64 +fun single_thm_name name : thm_name = (name, 0);
    1.65 +
    1.66 +fun get_thm context facts ((name, i), pos) =
    1.67 +  let
    1.68 +    fun print_name () =
    1.69 +      markup_extern (Context.proof_of context) facts name |-> Markup.markup;
    1.70 +  in
    1.71 +    (case (lookup context facts name, i) of
    1.72 +      (NONE, _) => error ("Undefined fact " ^ quote (print_name ()) ^ Position.here pos)
    1.73 +    | (SOME {thms = [thm], ...}, 0) => thm
    1.74 +    | (SOME {thms, ...}, 0) => err_single (print_name (), pos) thms
    1.75 +    | (SOME {thms, ...}, _) =>
    1.76 +        if i > 0 andalso i <= length thms then nth thms (i - 1)
    1.77 +        else err_selection (print_name (), pos) i thms)
    1.78 +  end;
    1.79 +
    1.80  end;