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