1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory AutoLevity_Theory_Report 8imports AutoLevity_Base 9begin 10 11ML \<open> 12(* An antiquotation for creating json-like serializers for 13 simple records. Serializers for primitive types are automatically used, 14 while serializers for complex types are given as parameters. *) 15val JSON_string_encode: string -> string = 16 String.translate ( 17 fn #"\\" => "\\\\" 18 | #"\n" => "\\n" 19 | x => if Char.isPrint x then String.str x else 20 "\\u" ^ align_right "0" 4 (Int.fmt StringCvt.HEX (Char.ord x))) 21 #> quote; 22 23fun JSON_int_encode (i: int): string = 24 if i < 0 then "-" ^ Int.toString (~i) else Int.toString i 25 26val _ = Theory.setup( 27ML_Antiquotation.inline @{binding string_record} 28 (Scan.lift 29 (Parse.name --| 30 Parse.$$$ "=" -- 31 Parse.position Parse.string) >> 32 (fn (name,(source,pos)) => 33 34 let 35 36 val entries = 37 let 38 val chars = String.explode source 39 |> filter_out (fn #"\n" => true | _ => false) 40 41 val trim = 42 String.explode 43 #> chop_prefix (fn #" " => true | _ => false) 44 #> snd 45 #> chop_suffix (fn #" " => true | _ => false) 46 #> fst 47 #> String.implode 48 49 val str = String.implode chars 50 |> String.fields (fn #"," => true | #":" => true | _ => false) 51 |> map trim 52 53 54 fun pairify [] = [] 55 | pairify (a::b::l) = ((a,b) :: pairify l) 56 | pairify _ = error ("Record syntax error" ^ Position.here pos) 57 58 in 59 pairify str 60 end 61 62 val typedecl = 63 "type " ^ name ^ "= { " 64 ^ (map (fn (nm,typ) => nm ^ ":" ^ typ) entries |> String.concatWith ",") 65 ^ "};" 66 67 val base_typs = ["string","int","bool", "string list"] 68 69 70 val encodes = map snd entries |> distinct (op =) 71 |> filter_out (member (op =) base_typs) 72 73 val sanitize = String.explode 74 #> map (fn #" " => #"_" 75 | #"." => #"_" 76 | #"*" => #"P" 77 | #"(" => #"B" 78 | #")" => #"R" 79 | x => x) 80 #> String.implode 81 82 fun mk_encode typ = 83 if typ = "string" 84 then "JSON_string_encode" 85 else if typ = "int" 86 then "JSON_int_encode" 87 else if typ = "bool" 88 then "Bool.toString" 89 else if typ = "string list" 90 then "(fn xs => (enclose \"[\" \"]\" (String.concatWith \", \" (map JSON_string_encode xs))))" 91 else (sanitize typ) ^ "_encode" 92 93 94 fun mk_elem nm _ value = 95 (ML_Syntax.print_string (JSON_string_encode nm) ^ "^ \" : \" ") ^ "^ (" ^ value ^ ")" 96 97 fun mk_head body = 98 "(\"" ^ "{\" ^ String.concatWith \", \" (" ^ body ^ ") ^ \"}\")" 99 100 101 val global_head = if (null encodes) then "" else 102 "fn (" ^ (map mk_encode encodes |> String.concatWith ",") ^ ") => " 103 104 105 val encode_body = 106 "fn {" ^ (map fst entries |> String.concatWith ",") ^ "} : " ^ name ^ " => " ^ 107 mk_head 108 (ML_Syntax.print_list (fn (field,typ) => mk_elem field typ (mk_encode typ ^ " " ^ field)) entries) 109 110 111 val val_expr = 112 "val (" ^ name ^ "_encode) = (" 113 ^ global_head ^ "(" ^ encode_body ^ "))" 114 115 val _ = @{print} val_expr 116 117 in 118 typedecl ^ val_expr 119 end))) 120\<close> 121 122ML \<open> 123 124@{string_record deps = "consts : string list, types: string list"} 125@{string_record lemma_deps = "consts: string list, types: string list, lemmas: string list"} 126@{string_record location = "file : string, start_line : int, end_line : int"} 127@{string_record levity_tag = "tag : string, location : location"} 128@{string_record apply_dep = "name : string, attribs : string list"} 129 130@{string_record proof_command = 131 "command_name : string, location : location, subgoals : int, depth : int, 132 apply_deps : apply_dep list" } 133 134@{string_record lemma_entry = 135 "name : string, command_name : string, levity_tag : levity_tag option, location : location, 136 proof_commands : proof_command list, 137 deps : lemma_deps"} 138 139@{string_record dep_entry = 140 "name : string, command_name : string, levity_tag : levity_tag option, location: location, 141 deps : deps"} 142 143@{string_record theory_entry = 144 "name : string, file : string"} 145 146@{string_record log_entry = 147 "errors : string list, location : location"} 148 149fun encode_list enc x = "[" ^ (String.concatWith ", " (map enc x)) ^ "]" 150 151fun encode_option enc (SOME x) = enc x 152 | encode_option _ NONE = "{}" 153 154val opt_levity_tag_encode = encode_option (levity_tag_encode location_encode); 155 156val proof_command_encode = proof_command_encode (location_encode, encode_list apply_dep_encode); 157 158val lemma_entry_encode = lemma_entry_encode 159 (opt_levity_tag_encode, location_encode, encode_list proof_command_encode, lemma_deps_encode) 160 161val dep_entry_encode = dep_entry_encode 162 (opt_levity_tag_encode, location_encode, deps_encode) 163 164val log_entry_encode = log_entry_encode (location_encode) 165 166\<close> 167 168ML \<open> 169 170signature AUTOLEVITY_THEORY_REPORT = 171sig 172val get_reports_for_thy: theory -> 173 string * log_entry list * theory_entry list * lemma_entry list * dep_entry list * dep_entry list 174 175val string_reports_of: 176 string * log_entry list * theory_entry list * lemma_entry list * dep_entry list * dep_entry list 177 -> string list 178 179end; 180 181structure AutoLevity_Theory_Report : AUTOLEVITY_THEORY_REPORT = 182struct 183 184fun map_pos_line f pos = 185let 186 val line = Position.line_of pos |> the; 187 val file = Position.file_of pos |> the; 188 189 val line' = f line; 190 191 val _ = if line' < 1 then raise Option else (); 192 193in SOME (Position.line_file_only line' file) end handle Option => NONE 194 195 196(* A Position.T table based on offsets (Postab_strict) can be collapsed into a line-based one 197 with lists of entries on for each line. This function searches such a table 198 for the closest entry, either backwards (LESS) or forwards (GREATER) from 199 the given position. *) 200 201(* TODO: If everything is sane then the search depth shouldn't be necessary. In practice 202 entries won't be more than one or two lines apart, but if something has gone wrong in the 203 collection phase we might end up wasting a lot of time looking for an entry that doesn't exist. *) 204 205fun search_by_lines depth ord_kind f h pos = if depth = 0 then NONE else 206 let 207 val line_change = case ord_kind of LESS => ~1 | GREATER => 1 | _ => raise Fail "Bad relation" 208 val idx_change = case ord_kind of GREATER => 1 | _ => 0; 209 in 210 case f pos of 211 SOME x => 212 let 213 val i = find_index (fn e => h (pos, e) = ord_kind) x; 214 in if i > ~1 then SOME (List.nth(x, i + idx_change)) else SOME (hd x) end 215 216 | NONE => 217 (case (map_pos_line (fn i => i + line_change) pos) of 218 SOME pos' => search_by_lines (depth - 1) ord_kind f h pos' 219 | NONE => NONE) 220 end 221 222fun location_from_range (start_pos, end_pos) = 223 let 224 val start_file = Position.file_of start_pos |> the; 225 val end_file = Position.file_of end_pos |> the; 226 val _ = if start_file = end_file then () else raise Option; 227 val start_line = Position.line_of start_pos |> the; 228 val end_line = Position.line_of end_pos |> the; 229 in 230 SOME ({file = start_file, start_line = start_line, end_line = end_line} : location) end 231 handle Option => NONE 232 233(* Here we collapse our proofs (lemma foo .. done) into single entries with start/end positions. *) 234 235fun get_command_ranges_of keywords thy_nm = 236let 237 fun is_ignored nm' = nm' = "<ignored>" 238 fun is_levity_tag nm' = nm' = "levity_tag" 239 240 fun is_proof_cmd nm' = nm' = "apply" orelse nm' = "by" orelse nm' = "proof" 241 242 (* All top-level transactions for the given theory *) 243 244 val (transactions, log) = 245 Symtab.lookup (AutoLevity_Base.get_transactions ()) thy_nm 246 |> the_default (Postab_strict.empty, Postab_strict.empty) 247 ||> Postab_strict.dest 248 |>> Postab_strict.dest 249 250 (* Line-based position table of all apply statements for the given theory *) 251 252 val applytab = 253 Symtab.lookup (AutoLevity_Base.get_applys ()) thy_nm 254 |> the_default Postab_strict.empty 255 |> Postab_strict.dest 256 |> map (fn (pos,e) => (pos, (pos,e))) 257 |> Postab.make_list 258 |> Postab.map (fn _ => sort (fn ((pos,_),(pos', _)) => pos_ord true (pos, pos'))) 259 260 261 (* A special "ignored" command lets us find the real end of commands which span 262 multiple lines. After finding a real command, we assume the last "ignored" one 263 was part of the syntax for that command *) 264 265 fun find_cmd_end last_pos ((pos', (nm', ext)) :: rest) = 266 if is_ignored nm' then 267 find_cmd_end pos' rest 268 else (last_pos, ((pos', (nm', ext)) :: rest)) 269 | find_cmd_end last_pos [] = (last_pos, []) 270 271 fun change_level nm level = 272 if Keyword.is_proof_open keywords nm then level + 1 273 else if Keyword.is_proof_close keywords nm then level - 1 274 else if Keyword.is_qed_global keywords nm then ~1 275 else level 276 277 278 fun make_apply_deps lemma_deps = 279 map (fn (nm, atts) => {name = nm, attribs = atts} : apply_dep) lemma_deps 280 281 (* For a given apply statement, search forward in the document for the closest method to retrieve 282 its lemma dependencies *) 283 284 fun find_apply pos = if Postab.is_empty applytab then [] else 285 search_by_lines 5 GREATER (Postab.lookup applytab) (fn (pos, (pos', _)) => pos_ord true (pos, pos')) pos 286 |> Option.map snd |> the_default [] |> make_apply_deps 287 288 fun find_proof_end level ((pos', (nm', ext)) :: rest) = 289 let val level' = change_level nm' level in 290 if level' > ~1 then 291 let 292 val (cmd_end, rest') = find_cmd_end pos' rest; 293 val ((prf_cmds, prf_end), rest'') = find_proof_end level' rest' 294 in (({command_name = nm', location = location_from_range (pos', cmd_end) |> the, 295 depth = level, apply_deps = if is_proof_cmd nm' then find_apply pos' else [], 296 subgoals = #subgoals ext} :: prf_cmds, prf_end), rest'') end 297 else 298 let 299 val (cmd_end, rest') = find_cmd_end pos' rest; 300 in (([{command_name = nm', location = location_from_range (pos', cmd_end) |> the, 301 apply_deps = if is_proof_cmd nm' then find_apply pos' else [], 302 depth = level, subgoals = #subgoals ext}], cmd_end), rest') end 303 end 304 | find_proof_end _ _ = (([], Position.none), []) 305 306 307 fun find_ends tab tag ((pos,(nm, ext)) :: rest) = 308 let 309 val (cmd_end, rest') = find_cmd_end pos rest; 310 311 val ((prf_cmds, pos'), rest'') = 312 if Keyword.is_theory_goal keywords nm 313 then find_proof_end 0 rest' 314 else (([],cmd_end),rest'); 315 316 val tab' = Postab.cons_list (pos, (pos, (nm, pos', tag, prf_cmds))) tab; 317 318 val tag' = 319 if is_levity_tag nm then Option.map (rpair (pos,pos')) (#levity_tag ext) else NONE; 320 321 in find_ends tab' tag' rest'' end 322 | find_ends tab _ [] = tab 323 324 val command_ranges = find_ends Postab.empty NONE transactions 325 |> Postab.map (fn _ => sort (fn ((pos,_),(pos',_)) => pos_ord true (pos, pos'))) 326 327in (command_ranges, log) end 328 329 330 331fun make_deps (const_deps, type_deps): deps = 332 {consts = distinct (op =) const_deps, types = distinct (op =) type_deps} 333 334fun make_lemma_deps (const_deps, type_deps, lemma_deps): lemma_deps = 335 { 336 consts = distinct (op =) const_deps, 337 types = distinct (op =) type_deps, 338 lemmas = distinct (op =) lemma_deps 339 } 340 341fun make_tag (SOME (tag, range)) = (case location_from_range range 342 of SOME rng => SOME ({tag = tag, location = rng} : levity_tag) 343 | NONE => NONE) 344 | make_tag NONE = NONE 345 346 347 348fun add_deps (((Defs.Const, nm), _) :: rest) = 349 let val (consts, types) = add_deps rest in 350 (nm :: consts, types) end 351 | add_deps (((Defs.Type, nm), _) :: rest) = 352 let val (consts, types) = add_deps rest in 353 (consts, nm :: types) end 354 | add_deps _ = ([], []) 355 356fun get_deps ({rhs, ...} : Defs.spec) = add_deps rhs 357 358fun typs_of_typ (Type (nm, Ts)) = nm :: (map typs_of_typ Ts |> flat) 359 | typs_of_typ _ = [] 360 361fun typs_of_term t = Term.fold_types (append o typs_of_typ) t [] 362 363fun deps_of_thm thm = 364let 365 val consts = Term.add_const_names (Thm.prop_of thm) []; 366 val types = typs_of_term (Thm.prop_of thm); 367in (consts, types) end 368 369fun file_of_thy thy = 370 let 371 val path = Resources.master_directory thy; 372 val name = Context.theory_name thy; 373 val path' = Path.append path (Path.basic (name ^ ".thy")) 374 in Path.smart_implode path' end; 375 376fun entry_of_thy thy = ({name = Context.theory_name thy, file = file_of_thy thy} : theory_entry) 377 378fun used_facts thy thm = 379 AutoLevity_Base.used_named_props_of thm 380 |> map_filter (AutoLevity_Base.disambiguate_indices (Proof_Context.init_global thy)) 381 |> List.map fst; 382 383fun get_reports_for_thy thy = 384 let 385 val thy_nm = Context.theory_name thy; 386 val all_facts = Global_Theory.facts_of thy; 387 val fact_space = Facts.space_of all_facts; 388 389 val (tab, log) = get_command_ranges_of (Thy_Header.get_keywords thy) thy_nm; 390 391 val parent_facts = map Global_Theory.facts_of (Theory.parents_of thy); 392 393 val search_backwards = search_by_lines 5 LESS (Postab.lookup tab) 394 (fn (pos, (pos', _)) => pos_ord true (pos, pos')) 395 #> the 396 397 val lemmas = Facts.dest_static false parent_facts (Global_Theory.facts_of thy) 398 |> map_filter (fn (xnm, thms) => 399 let 400 val {theory_long_name, pos, ...} = Name_Space.the_entry fact_space xnm; 401 in 402 if theory_long_name = thy_nm then 403 let 404 val thms' = map (Thm.transfer thy) thms; 405 406 val (real_start, (cmd_name, end_pos, tag, prf_cmds)) = search_backwards pos 407 408 val lemma_deps = 409 if cmd_name = "datatype" 410 then [] 411 else map (used_facts thy) thms' |> flat |> distinct (op =); 412 413 val (consts, types) = map deps_of_thm thms' |> ListPair.unzip |> apply2 flat 414 val deps = make_lemma_deps (consts, types, lemma_deps) 415 416 val location = location_from_range (real_start, end_pos) |> the; 417 418 val (lemma_entry : lemma_entry) = 419 {name = xnm, command_name = cmd_name, levity_tag = make_tag tag, 420 location = location, proof_commands = prf_cmds, deps = deps} 421 422 in SOME (pos, lemma_entry) end 423 else NONE end handle Option => NONE) 424 |> Postab_strict.make_list 425 |> Postab_strict.dest |> map snd |> flat 426 427 val defs = Theory.defs_of thy; 428 429 fun get_deps_of kind space xnms = xnms 430 |> map_filter (fn xnm => 431 let 432 val {theory_long_name, pos, ...} = Name_Space.the_entry space xnm; 433 in 434 if theory_long_name = thy_nm then 435 let 436 val specs = Defs.specifications_of defs (kind, xnm); 437 438 val deps = 439 map get_deps specs 440 |> ListPair.unzip 441 |> (apply2 flat #> make_deps); 442 443 val (real_start, (cmd_name, end_pos, tag, _)) = search_backwards pos 444 445 val loc = location_from_range (real_start, end_pos) |> the; 446 447 val entry = 448 ({name = xnm, command_name = cmd_name, levity_tag = make_tag tag, 449 location = loc, deps = deps} : dep_entry) 450 451 in SOME (pos, entry) end 452 else NONE end handle Option => NONE) 453 |> Postab_strict.make_list 454 |> Postab_strict.dest |> map snd |> flat 455 456 val {const_space, constants, ...} = Consts.dest (Sign.consts_of thy); 457 458 val consts = get_deps_of Defs.Const const_space (map fst constants); 459 460 val {types, ...} = Type.rep_tsig (Sign.tsig_of thy); 461 462 val type_space = Name_Space.space_of_table types; 463 val type_names = Name_Space.fold_table (fn (xnm, _) => cons xnm) types []; 464 465 val types = get_deps_of Defs.Type type_space type_names; 466 467 val thy_parents = map entry_of_thy (Theory.parents_of thy); 468 469 val logs = log |> 470 map (fn (pos, errs) => {errors = errs, location = location_from_range (pos, pos) |> the} : log_entry) 471 472 in (thy_nm, logs, thy_parents, lemmas, consts, types) end 473 474fun add_commas (s :: s' :: ss) = s ^ "," :: (add_commas (s' :: ss)) 475 | add_commas [s] = [s] 476 | add_commas _ = [] 477 478 479fun string_reports_of (thy_nm, logs, thy_parents, lemmas, consts, types) = 480 ["{\"theory_name\" : " ^ JSON_string_encode thy_nm ^ ","] @ 481 ["\"logs\" : ["] @ 482 add_commas (map (log_entry_encode) logs) @ 483 ["],","\"theory_imports\" : ["] @ 484 add_commas (map (theory_entry_encode) thy_parents) @ 485 ["],","\"lemmas\" : ["] @ 486 add_commas (map (lemma_entry_encode) lemmas) @ 487 ["],","\"consts\" : ["] @ 488 add_commas (map (dep_entry_encode) consts) @ 489 ["],","\"types\" : ["] @ 490 add_commas (map (dep_entry_encode) types) @ 491 ["]}"] 492 |> map (fn s => s ^ "\n") 493 494end 495\<close> 496 497end 498