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