1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7(*
8 * Insulin.thy: regulate sugar in terms, thms and proof goals.
9 *
10 * Usage:
11 * This theory provides the improper commands
12 *   desugar_term <term> <str> <str>...
13 *   desugar_thm <thm> <str> <str>...
14 *   desugar_goal [<goal_num>] <str> <str>...
15 * which print the term, thm or subgoal(s) with the syntax <str> replaced by the
16 * underlying constants.
17 *
18 * For example:
19 *   > thm fun_upd_apply
20 *   (?f(?x := ?y)) ?z = (if ?z = ?x then ?y else ?f ?z)
21 *
22 * But what is this ":="?
23 *   > desugar_thm fun_upd_apply ":="
24 *   Fun.fun_upd ?f ?x ?y ?z = (if ?z = ?x then ?y else ?f ?z)
25 *
26 * Remove all sugar:
27 *   > desugar_thm fun_upd_apply "=" "if"
28 *   HOL.eq (Fun.fun_upd ?f ?x ?y ?z)
29 *     (HOL.If (HOL.eq ?z ?x) ?y (?f ?z))
30 *
31 * Desugar only one subterm:
32 *   > desugar_thm fun_upd_apply "?z = ?x"
33 *   (?f(?x := ?y)) ?z = (if HOL.eq ?z ?x then ?y else ?f ?z)
34 *
35 * Another example (l4v libraries):
36 *   > desugar_term "\<lbrace> P and Q \<rbrace> f \<lbrace> \<lambda>r _. r \<in> {0..<5} \<rbrace>!" "\<lbrace>"
37 *   NonDetMonad.validNF (P and Q) f (\<lambda>r _. r \<in> {0\<Colon>'b..<5\<Colon>'b})
38 *
39 * Desugar multiple operators:
40 *   > desugar_term "\<lbrace> P and Q \<rbrace> f \<lbrace> \<lambda>r _. r \<in> {0..<5} \<rbrace>!" "\<lbrace>" "and" ".."
41 *   NonDetMonad.validNF (Lib.pred_conj P Q) f
42 *     (\<lambda>r _. r \<in> Set_Interval.ord_class.atLeastLessThan (0\<Colon>'b) (5\<Colon>'b))
43 *
44 *
45 * Known problems:
46 * - The output may have bad indentation. This is because the mangled constant
47 *   name has a different length compared to the original.
48 *
49 * - May not work with exotic syntax translations (e.g. ML-defined syntax).
50 *
51 * - May not work with terms that contain the magic string "dsfjdssdfsd".
52 *
53 * - Naive algorithm, takes \<approx>quadratic time.
54 *)
55
56theory Insulin
57imports
58  Pure
59keywords
60  "desugar_term" "desugar_thm" "desugar_goal" :: diag
61begin
62
63(*
64 * Isabelle syntax rules are invoked based on constants appearing in a term.
65 * Insulin works by replacing each constant with a free variable, which is
66 * displayed without triggering syntax translations.
67 * It tries each constant in the term to find the ones that produce a given
68 * syntax fragment, then limits the replacement to those constants only.
69 *
70 * The tricky bit is determining which constants contribute to the proscribed
71 * syntax fragment. We do this somewhat naively by trying each constant
72 * one-at-a-time, then replacing those which reduce the *number of occurrences*
73 * of the proscribed syntax.
74 * Since syntax translations are arbitrary, it is possible that the final result
75 * still contains unwanted syntax, so we iterate this process.
76 *
77 * This one-at-a-time approach fails for syntax that can be triggered by any of
78 * several constants in a term. I don't know any examples of this, though.
79 *)
80
81ML \<open>
82structure Insulin = struct
83
84val desugar_random_tag = "dsfjdssdfsd"
85fun fresh_substring s = let
86  fun next [] = [#"a"]
87    | next (#"z" :: n) = #"a" :: next n
88    | next (c :: n) = Char.succ c :: n
89  fun fresh n = let
90    val ns = String.implode n
91    in if String.isSubstring ns s then fresh (next n) else ns end
92  in fresh [#"a"] end
93
94(* Encode a (possibly qualified) constant name as an (expected-to-be-)unused name.
95 * The encoded name will be treated as a free variable. *)
96fun escape_const c = let
97  val delim = fresh_substring c
98  in desugar_random_tag ^ delim ^ "_" ^
99       String.concat (case Long_Name.explode c of
100                        (a :: b :: xs) => a :: map (fn x => delim ^ x) (b :: xs)
101                      | xs => xs)
102  end
103(* Decode; if it fails, return input string *)
104fun unescape_const s =
105  if not (String.isPrefix desugar_random_tag s) then s else
106  let val cs = String.extract (s, String.size desugar_random_tag, NONE) |> String.explode
107      fun readDelim d (#"_" :: cs) = (d, cs)
108        | readDelim d (c :: cs) = readDelim (d @ [c]) cs
109      val (delim, cs) = readDelim [] cs
110      val delimlen = length delim
111      fun splitDelim name cs =
112            if take delimlen cs = delim then name :: splitDelim [] (drop delimlen cs)
113              else case cs of [] => if null name then [] else [name]
114                            | (c::cs) => splitDelim (name @ [c]) cs
115      val names = splitDelim [] cs
116  in Long_Name.implode (map String.implode names) end
117  handle Match => s
118
119fun dropQuotes s = if String.isPrefix "\"" s andalso String.isSuffix "\"" s
120                       then String.substring (s, 1, String.size s - 2) else s
121
122(* Translate markup from consts-encoded-as-free-variables to actual consts *)
123fun desugar_reconst ctxt (tr as XML.Elem ((tag, attrs), children))
124  = if tag = "fixed" orelse tag = "intensify" then
125      let val s = XML.content_of [tr]
126          val name = unescape_const s
127          fun get_entity_attrs (XML.Elem (("entity", attrs), _)) = SOME attrs
128            | get_entity_attrs (XML.Elem (_, body)) =
129                find_first (K true) (List.mapPartial get_entity_attrs body)
130            | get_entity_attrs (XML.Text _) = NONE
131      in
132        if name = s then tr else
133          (* try to look up the const's info *)
134          case Syntax.read_term ctxt name
135               |> Thm.cterm_of ctxt
136               |> Proof_Display.pp_cterm (fn _ => Proof_Context.theory_of ctxt)
137               |> Pretty.string_of
138               |> dropQuotes
139               |> YXML.parse
140               |> get_entity_attrs of
141              SOME attrs =>
142                XML.Elem (("entity", attrs), [XML.Text name])
143            | _ =>
144                XML.Elem (("entity", [("name", name), ("kind", "constant")]),
145                          [XML.Text name]) end
146    else XML.Elem ((tag, attrs), map (desugar_reconst ctxt) children)
147  | desugar_reconst _ (t as XML.Text _) = t
148
149fun term_to_string ctxt no_markup =
150  Syntax.pretty_term ctxt
151  #> Pretty.string_of
152  #> YXML.parse_body
153  #> map (desugar_reconst ctxt)
154  #> (if no_markup then XML.content_of else YXML.string_of_body)
155  #> dropQuotes
156
157(* Strip constant names from a term.
158 * A term is split to a "term_unconst" and a "string list" of the
159 * const names in tree preorder. *)
160datatype term_unconst =
161    UCConst of typ |
162    UCAbs of string * typ * term_unconst |
163    UCApp of term_unconst * term_unconst |
164    UCVar of term
165
166fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"'"
167
168fun term_to_unconst (Const (name, typ)) =
169    (* some magical constants have strange names, such as ==>; ignore them *)
170      if forall is_ident_char (String.explode name) then (UCConst typ, [name])
171        else (UCVar (Const (name, typ)), [])
172  | term_to_unconst (Abs (var, typ, body)) = let
173      val (body', consts) = term_to_unconst body
174      in (UCAbs (var, typ, body'), consts) end
175  | term_to_unconst (f $ x) = let
176      val (f', consts1) = term_to_unconst f
177      val (x', consts2) = term_to_unconst x
178      in (UCApp (f', x'), consts1 @ consts2) end
179  | term_to_unconst t = (UCVar t, [])
180
181fun term_from_unconst (UCConst typ) (name :: consts) =
182      ((if unescape_const name = name then Const else Free) (name, typ), consts)
183  | term_from_unconst (UCAbs (var, typ, body)) consts = let
184      val (body', consts) = term_from_unconst body consts
185      in (Abs (var, typ, body'), consts) end
186  | term_from_unconst (UCApp (f, x)) consts = let
187      val (f', consts) = term_from_unconst f consts
188      val (x', consts) = term_from_unconst x consts
189      in (f' $ x', consts) end
190  | term_from_unconst (UCVar v) consts = (v, consts)
191
192(* Count occurrences of bad strings.
193 * Bad strings are allowed to overlap, but for each string, non-overlapping occurrences are counted.
194 * Note that we search on string lists, to deal with symbols correctly. *)
195fun count_matches (haystack: ''a list) (needles: ''a list list): int list =
196  let (* Naive algorithm. Probably ok, given that we're calling the term printer a lot elsewhere. *)
197      fun try_match xs [] = SOME xs
198        | try_match (x::xs) (y::ys) = if x = y then try_match xs ys else NONE
199        | try_match _ _ = NONE
200      fun count [] = 0
201        | count needle = let
202            fun f [] occs = occs
203              | f haystack' occs = case try_match haystack' needle of
204                                       NONE => f (tl haystack') occs
205                                     | SOME tail => f tail (occs + 1)
206            in f haystack 0 end
207  in map count needles end
208
209fun focus_list (xs: 'a list): ('a list * 'a * 'a list) list =
210  let fun f head x [] = [(head, x, [])]
211        | f head x (tail as x'::tail') = (head, x, tail) :: f (head @ [x]) x' tail'
212  in case xs of [] => []
213              | (x::xs) => f [] x xs end
214
215(* Do one rewrite pass: try every constant in sequence, then collect the ones which
216 * reduced the occurrences of bad strings *)
217fun rewrite_pass ctxt (t: term) (improved: term -> bool) (escape_const: string -> string): term =
218  let val (ucterm, consts) = term_to_unconst t
219      fun rewrite_one (prev, const, rest) =
220            let val (t', []) = term_from_unconst ucterm (prev @ [escape_const const] @ rest)
221            in improved t' end
222      val consts_to_rewrite = focus_list consts |> map rewrite_one
223      val consts' = map2 (fn rewr => fn const => if rewr then escape_const const else const) consts_to_rewrite consts
224      val (t', []) = term_from_unconst ucterm consts'
225  in t' end
226
227(* Do rewrite passes until bad strings are gone or no more rewrites are possible *)
228fun desugar ctxt (t0: term) (bads: string list): term =
229  let fun count t = count_matches (Symbol.explode (term_to_string ctxt true t)) (map Symbol.explode bads)
230      val _ = if null bads then error "Nothing to desugar" else ()
231      fun rewrite t = let
232        val counts0 = count t
233        fun improved t' = exists (<) (count t' ~~ counts0)
234        val t' = rewrite_pass ctxt t improved escape_const
235        in if forall (fn c => c = 0) (count t') (* bad strings gone *)
236           then t'
237           else if t = t' (* no more rewrites *)
238             then let
239               val bads' = filter (fn (c, _) => c > 0) (counts0 ~~ bads) |> map snd
240               val _ = warning ("Sorry, failed to desugar " ^ commas_quote bads')
241               in t end
242             else rewrite t'
243         end
244  in rewrite t0 end
245
246fun span _ [] = ([],[])
247  | span p (a::s) =
248      if p a then let val (y, n) = span p s in (a::y, n) end else ([], a::s)
249
250fun check_desugar s = let
251  fun replace [] = []
252    | replace xs =
253        if take (String.size desugar_random_tag) xs = String.explode desugar_random_tag
254          then case span is_ident_char xs of
255                   (v, xs) => String.explode (unescape_const (String.implode v)) @ replace xs
256          else hd xs :: replace (tl xs)
257  val desugar_string = String.implode o replace o String.explode
258  in if not (String.isSubstring desugar_random_tag s) then s
259       else desugar_string s end
260
261fun desugar_term ctxt t s =
262  desugar ctxt t s |> term_to_string ctxt false |> check_desugar
263
264fun desugar_thm ctxt thm s = desugar_term ctxt (Thm.prop_of thm) s
265
266fun desugar_goal ctxt goal n s = let
267  val subgoals = goal |> Thm.prems_of
268  val subgoals = if n = 0 then subgoals else
269                 if n < 1 orelse n > length subgoals then
270                      (* trigger error *) [Logic.get_goal (Thm.term_of (Thm.cprop_of goal)) n]
271                 else [nth subgoals (n - 1)]
272  val results = map (fn t => (NONE, desugar_term ctxt t s)
273                             handle ex as TERM _ => (SOME ex, term_to_string ctxt false t))
274                    subgoals
275  in if null results
276        then error "No subgoals to desugar"
277     else if forall (Option.isSome o fst) results
278        then raise the (fst (hd results))
279     else map snd results
280  end
281
282end
283\<close>
284
285ML \<open>
286Outer_Syntax.command @{command_keyword "desugar_term"}
287  "term str str2... -> desugar str in term"
288  (Parse.term -- Scan.repeat1 Parse.string >> (fn (t, s) =>
289    Toplevel.keep (fn state => let val ctxt = Toplevel.context_of state in
290      Insulin.desugar_term ctxt (Syntax.read_term ctxt t) s
291      |> writeln end)))
292\<close>
293
294ML \<open>
295Outer_Syntax.command @{command_keyword "desugar_thm"}
296  "thm str str2... -> desugar str in thm"
297  (Parse.thm -- Scan.repeat1 Parse.string >> (fn (t, s) =>
298    Toplevel.keep (fn state => let val ctxt = Toplevel.context_of state in
299      Insulin.desugar_thm ctxt (Attrib.eval_thms ctxt [t] |> hd) s |> writeln end)))
300\<close>
301
302ML \<open>
303fun print_subgoals (x::xs) n = (writeln (Int.toString n ^ ". " ^ x); print_subgoals xs (n+1))
304  | print_subgoals [] _ = ();
305Outer_Syntax.command @{command_keyword "desugar_goal"}
306  "goal_num str str2... -> desugar str in goal"
307  (Scan.option Parse.int -- Scan.repeat1 Parse.string >> (fn (n, s) =>
308    Toplevel.keep (fn state => let val ctxt = Toplevel.context_of state in
309      Insulin.desugar_goal ctxt (Toplevel.proof_of state |> Proof.raw_goal |> #goal) (Option.getOpt (n, 0)) s
310      |> (fn xs => case xs of
311            [x] => writeln x
312            | _ => print_subgoals xs 1) end)))
313\<close>
314
315end
316