1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7signature THM_EXTRAS = 8sig 9 datatype adjusted_name = 10 FoundName of ((string * int option) * thm) 11 | UnknownName of (string * term) 12 val adjust_found_thm : adjusted_name -> thm -> adjusted_name 13 val fact_ref_to_name : Facts.ref * thm -> adjusted_name 14 val adjust_thm_name : Proof.context -> string * int option -> term -> adjusted_name 15 val pretty_adjusted_name : Proof.context -> adjusted_name -> Pretty.T 16 val pretty_adjusted_fact : Proof.context -> adjusted_name -> Pretty.T 17 val pretty_fact : bool -> Proof.context -> adjusted_name -> Pretty.T 18 19 val pretty_thm : bool -> Proof.context -> thm -> Pretty.T 20 val pretty_specific_thm : Proof.context -> string -> thm -> Pretty.T 21 val pretty_fact_name : Proof.context -> string -> Pretty.T 22end 23 24structure ThmExtras: THM_EXTRAS = 25struct 26 27datatype adjusted_name = 28 FoundName of ((string * int option) * thm) 29 | UnknownName of (string * term) 30 31fun adjust_found_thm (FoundName (name, _)) thm = FoundName (name, thm) 32 | adjust_found_thm adjusted_name _ = adjusted_name 33 34fun fact_ref_to_name ((Facts.Named ((nm,_), (SOME [Facts.Single i]))),thm) = FoundName ((nm,SOME i),thm) 35 | fact_ref_to_name ((Facts.Named ((nm,_), (NONE))),thm) = FoundName ((nm,NONE),thm) 36 | fact_ref_to_name (_,thm) = UnknownName ("",Thm.prop_of thm) 37 38(* Parse the index of a theorem name in the form "x_1". *) 39fun parse_thm_index name = 40 case (String.tokens (fn c => c = #"_") name |> rev) of 41 (possible_index::xs) => 42 (case Lexicon.read_nat possible_index of 43 SOME n => (space_implode "_" (rev xs), SOME (n - 1)) 44 | NONE => (name, NONE)) 45 | _ => (name, NONE) 46 47(* 48 * Names stored in proof bodies may have the form "x_1" which can either 49 * mean "x(1)" or "x_1". Attempt to determine the correct name for the 50 * given theorem. If we can't find the correct theorem, or it is 51 * ambiguous, return the original name. 52 *) 53fun adjust_thm_name ctxt (name,index) term = 54let 55 val possible_names = case index of NONE => distinct (op =) [(name, NONE), parse_thm_index name] 56 | SOME i => [(name,SOME i)] 57 58 fun match (n, i) = 59 let 60 val idx = the_default 0 i 61 val thms = Proof_Context.get_fact ctxt (Facts.named n) handle ERROR _ => [] 62 in 63 if idx >= 0 andalso length thms > idx then 64 if length thms > 1 then 65 SOME ((n, i), nth thms idx) 66 else 67 SOME ((n,NONE), hd thms) 68 else 69 NONE 70 end 71in 72 case map_filter match possible_names of 73 [x] => FoundName x 74 | _ => UnknownName (name, term) 75end 76 77fun pretty_adjusted_name ctxt (FoundName ((name, idx), _)) = 78 Pretty.block 79 [Pretty.mark_str (Facts.markup_extern ctxt (Proof_Context.facts_of ctxt) name), 80 case idx of 81 SOME n => Pretty.str ("(" ^ string_of_int (n + 1) ^ ")") 82 | NONE => Pretty.str ""] 83 | pretty_adjusted_name _ (UnknownName (name, _)) = 84 Pretty.block [Pretty.str name, Pretty.str "(?)"] 85 86fun pretty_adjusted_fact ctxt (FoundName (_, thm)) = 87 Thm.pretty_thm ctxt thm 88 | pretty_adjusted_fact ctxt (UnknownName (_, prop)) = 89 Syntax.unparse_term ctxt prop 90 91(* Render the given fact, using the given adjusted name. *) 92fun pretty_fact only_names ctxt adjusted_name = 93 Pretty.block 94 (pretty_adjusted_name ctxt adjusted_name :: 95 (if only_names then [] 96 else [Pretty.str ":",Pretty.brk 1, pretty_adjusted_fact ctxt adjusted_name])) 97 98(* Render the given fact. *) 99fun pretty_thm only_names ctxt thm = 100 let 101 val name = Thm.get_name_hint thm 102 val adjusted_name = adjust_thm_name ctxt (name, NONE) (Thm.prop_of thm) 103 in pretty_fact only_names ctxt adjusted_name 104 end 105 106(* Render the given fact, using the given name. The name and fact do not have to match. *) 107fun pretty_specific_thm ctxt name thm = 108 let val adjusted_name = adjust_thm_name ctxt (name, NONE) (Thm.prop_of thm) 109 in pretty_fact false ctxt (adjust_found_thm adjusted_name thm) 110 end 111 112(* Render the given name, with markup if it matches a known fact. *) 113fun pretty_fact_name ctxt name = 114 Pretty.block [Pretty.marks_str (Proof_Context.markup_extern_fact ctxt name)]; 115 116end 117