1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory AutoLevity (* FIXME: broken *) 8imports "ProofGraph" 9begin 10ML \<open>val infoflow_file = "~~/../lib/proof_counting/Noninterference_Refinement_graphs.xml"\<close> 11ML \<open>val (full_spec,proof_spec_raw,thy_deps) = Proof_Graph.read_graph_spec_from infoflow_file\<close> 12 13ML \<open>val proof_spec = Proof_Graph.merge_multi_thms proof_spec_raw\<close> 14 15(* Extracts "general" lemmas from proof graph and produces lemma buckets from them *) 16(* Does theory and lemma dependency management. Might be better to produce a report and 17 have a bash/perl script consume this, rather than doing the file manipulation in ML *) 18(* Cleanup: Not really using name spaces properly *) 19 20 21(*TODO: Can possibly extract lemmas from the middle of locales *) 22ML \<open> 23 24fun range (beg,fin) l = List.take (List.drop (l,beg),fin - beg) 25 26fun map_range f (beg,fin) l = 27let 28 fun do_clear (h :: l') i = if beg <= i andalso i <= fin then (f h) :: (do_clear l' (i + 1)) else h :: (do_clear l' (i + 1)) 29 | do_clear [] i = [] 30in 31 do_clear l 0 end 32 33fun add_thy thy_deps thy thys' = 34let 35 fun reachable i j = 36 let 37 val deps = Option.map snd (Symtab.lookup thy_deps i) 38 in 39 case deps of SOME deps => member (=) deps j | NONE => false end 40 41 val thys = distinct (=) thys' 42 43in 44 if exists (fn ex_thy => reachable ex_thy thy) thys then thys else 45 thys 46 |> filter_out (fn ex_thy => reachable thy ex_thy) 47 |> cons thy 48end 49 50fun thy_list thy_deps thys = fold (add_thy thy_deps) thys [] 51 |> sort_wrt I 52 53fun add_thy_consts spec_graph (e : Proof_Graph.proof_entry) = 54 let 55 val thys' = map (Int_Graph.get_node spec_graph #> #theory) (#contains e) 56 in 57 (union (=) thys') end 58 59 60 61fun sort_lemmas (proof_graph,spec_graph : Spec_Graph.graph_entry Int_Graph.T,thy_deps) spec_theories facts = 62let 63 64 fun do_sort (nm,e) (thy_names,thy_imports) = 65 let 66 val thy_list = thy_list thy_deps (add_thy_consts spec_graph e []) 67 val i = (space_implode "__" thy_list) ^ "_Bucket" 68 in 69 (Symtab.update_new (nm,i) thy_names, 70 Symtab.update (i,thy_list) thy_imports) end 71 72 val (thy_names,thy_imports) = fold do_sort facts (Symtab.empty,Symtab.empty) 73 74 75 fun extra_deps (nm,e) (thm_deps,thytab) = 76 let 77 val thy_name = Symtab.lookup thy_names nm |> the 78 79 val all_succs = String_Graph.all_succs proof_graph [nm] 80 81 82 fun get_dep nm' b = 83 let 84 val thyn = Long_Name.explode nm' |> hd 85 fun warn _ = if not (Symtab.defined thy_names nm') then (warning (nm ^ " depends on " ^ nm' ^ " which is not marked for levitation and is outside theory import chain. NOT levitating.");true) else b 86 87 in if member (=) spec_theories thyn then (NONE,warn ()) else (SOME thyn,b) end 88 89 val (deps,rem) = fold_map get_dep all_succs false 90 |>> map_filter I 91 |>> append (map_filter (Symtab.lookup thy_names) all_succs) 92 |>> remove (=) thy_name 93 94 val imm_succs = String_Graph.immediate_succs proof_graph nm 95 96 97 in 98 (if rem then (thm_deps,thytab) else 99 (Symtab.update (nm,(e,imm_succs)) thm_deps,fold (fn dep => Symtab.insert_list (=) (thy_name,dep)) deps thytab)) end 100 101 fun rem_cycles (thy_names,thy_imports) = 102 let 103 val thy_graph = thy_imports 104 |> Symtab.dest 105 |> map (fn (id,e) => ((id,()),filter (Symtab.defined thy_imports) e)) 106 |> String_Graph.make 107 108 fun merge_deps (n :: l) (thy_names,thy_graph) = 109 let 110 111 112 val thy_graph' = 113 Proof_Graph.restrict_subgraph (fn (i,_) => not (member (=) l i)) thy_graph 114 115 val thy_names' = Symtab.map (fn _ => fn thyn => if member (=) l thyn then n else thyn) thy_names 116 in 117 (thy_names',thy_graph') end; 118 119 fun cycles_of i = 120 fold (fn j => append (String_Graph.irreducible_paths thy_graph (j,i))) (String_Graph.immediate_succs thy_graph i) [] 121 122 val cycles = map (flat o cycles_of) (String_Graph.keys thy_graph) 123 |> filter_out null 124 |> map (sort_wrt I #> distinct (=) #> rev) 125 |> distinct (=) 126 127 val thy_graph = thy_imports 128 |> Symtab.dest 129 |> map (fn (id,e) => ((id,()),e)) 130 |> append (map (fn (id,(_,e)) => ((id,()),e)) (Symtab.dest thy_deps)) 131 |> String_Graph.make 132 133 val (thy_names',thy_graph') = fold merge_deps cycles (thy_names,thy_graph) 134 135 val thy_imports' = map (fn i => (i,String_Graph.all_succs thy_graph' [i] |> remove (=) i)) (String_Graph.keys thy_graph') 136 |> filter (fn (i,_) => Symtab.defined thy_imports i) 137 |> Symtab.make 138 139 in 140 (thy_names',thy_imports') end 141 142 val (thm_deps,thy_imports) = fold extra_deps facts (Symtab.empty,thy_imports) 143 144 val (thy_names',thy_imports') = rem_cycles (thy_names,thy_imports) 145 ||> Symtab.map (K (thy_list thy_deps)) 146 147 val order = String_Graph.topological_order proof_graph 148 |> (fn l => fold_map (fn nm => fn i => ((nm,i),i+1)) l 0) 149 |> fst 150 |> Symtab.make 151 152 fun do_lookup e tab nm = (Symtab.lookup tab nm |> the) handle Option => error ("No entry " ^ nm ^ " in symtab:\n" ^ e) 153 154 val compare_facts = make_ord (fn ((nm,_),(nm',_)) => (do_lookup "order" order nm) < (do_lookup "order" order nm')) 155 156 157 val thys = Symtab.fold (fn (nm,e) => Symtab.insert_list (K false) (do_lookup "thy_names" thy_names' nm,(nm,e))) thm_deps Symtab.empty 158 |> Symtab.map (K (sort compare_facts)) 159 |> Symtab.map (fn i => fn e => (do_lookup "thy_imports" thy_imports' i,e)) 160 |> Symtab.dest 161 162 val base_thy = 163 let 164 val all_imports = thy_imports' 165 |> Symtab.dest 166 |> map snd 167 |> flat 168 |> distinct (=) 169 |> filter_out (member (=) (Symtab.keys thy_imports')) 170 |> thy_list thy_deps 171 |> map (fn n => "\"" ^ (Symtab.lookup thy_deps n |> the |> fst) ^ "/" ^ n ^ "\"") 172 |> distinct (=) 173 in 174 ("AutoLevity_Base",(all_imports,[])) end 175 176 val toplevel_thy = ("AutoLevity_Top",(thy_list thy_deps (Symtab.keys thy_imports'),[])) 177 178in 179 (toplevel_thy :: base_thy :: thys) end 180 181(*TODO: Have a more sensible way of generating this list*) 182val declare_attribs = ["simp","wp","intro","intro!","elim","elim!"] 183 184fun get_attribs str = 185let 186 val toks = (Outer_Syntax.scan Position.none str 187 |> filter (Token.is_proper) 188 ) @ ([Token.eof]) 189 190 val ((nm,attribs),_) = 191 (Parse.command |-- Parse_Spec.opt_thm_name ":") toks handle _ => error ("Failed to parse lemma attributes" ^ str) 192in 193 map (fst o fst o Args.dest_src) attribs 194 |> filter (member (=) declare_attribs) end 195 196fun parse_attribs sorted = 197let 198 fun do_parse (id,(e : Proof_Graph.proof_entry,thm_deps)) = 199 let 200 val thy_file = File.read_lines (Path.explode (#file e)) 201 val (begin,fin) = (#lines e) 202 val text = range (begin -1,fin) thy_file 203 |> space_implode "\n" 204 205 val new_attribs = get_attribs text 206 in 207 (id,(e,thm_deps,new_attribs)) end 208in 209 map (fn (file,(deps,lemmas)) => (file,(deps,map do_parse lemmas))) sorted end 210 211 212 213fun get_raw_proofs debug (id : string,(e : Proof_Graph.proof_entry,thm_deps,attribs)) = 214 let 215 val thy_file = File.read_lines (Path.explode (#file e)) 216 val (begin,fin) = (#lines e) 217 val text = range (begin -1,fin) thy_file 218 |> space_implode "\n" 219 220 val new_attribs = attribs 221 |> map (fn s => s ^ " del") 222 |> space_implode "," 223 224 225 val text' = text ^ (if new_attribs = "" then "" else ("\ndeclare " ^ (#name e) ^ "[" ^ new_attribs ^ "]")) 226 ^ (if debug then "\n(* THM_DEPS: " ^ space_implode " " thm_deps ^ "*)\n" else "") 227 228 (* Make sure we don't have any ride-alongs *) 229 val _ = if (String.isSubstring "method_setup" text) then warning ("Found method setup" ^ (@{make_string} (id,e)) ^ "\n" ^ text) else () 230 in 231 cons (#file e,text') end 232 233 234fun add_buffer (f,text) (cur_f,buf) = 235let 236 val buf' = buf 237 |> Buffer.add (if f = cur_f then "" else "\n(* " ^ f ^ " *)\n\n") 238 |> Buffer.add ("\n" ^ text ^ "\n") 239in 240 (f,buf') end 241 242fun get_thy debug (nm,(imports,lemmas)) = 243let 244 245 val lemma_text = fold (get_raw_proofs debug) lemmas [] 246 247 val buf = Buffer.empty 248 |> Buffer.add ("theory " ^ nm ^ "\nimports ") 249 |> Buffer.add (space_implode " " imports) 250 |> Buffer.add ("\nbegin\n") 251 |> (fn b => fold add_buffer lemma_text ("",b)) 252 |> snd 253 |> Buffer.add ("\nend") 254 255in 256 (nm,buf) end 257 258 259 260fun write_thys debug sorted base_path = 261let 262 val bufs = map (get_thy debug) sorted 263in 264 (map (fn (nm,buf) => (File.write_buffer (Path.append base_path (Path.explode (nm ^ ".thy"))) buf)) bufs;()) end 265 266 267 268fun remove_lemma thy_nm (nm,(e : Proof_Graph.proof_entry,thm_deps,attribs)) (new_deps,cache) = 269let 270 val (beg',fin) = #lines e 271 val beg = beg' -1 272 273 val thy_file = case Symtab.lookup cache (#file e) of SOME s => s | NONE => File.read_lines (Path.explode (#file e)) |> map SOME 274 275 276 277 val header = "(* " ^ #name e ^ " moved to " ^ thy_nm ^ " *)" 278 279 val new_attribs = attribs 280 |> space_implode "," 281 282 val declare = if new_attribs = "" then "" else "\ndeclare " ^ thy_nm ^ "." ^ (#name e) ^ "[" ^ new_attribs ^ "]" 283 284 val thy_file' = thy_file 285 |> map_range (K NONE) (beg,fin-1) 286 |> map_range (K (SOME (header ^ declare) )) (beg,beg) 287 288in 289 (Symtab.insert_list (=) (#file e,thy_nm) new_deps,Symtab.update (#file e,thy_file') cache) end 290 291(*TODO: Auto-generate thy dependencies or assume everyone will import us?*) 292fun remove_thy (thy_nm,(deps,lemmas)) cache = fold (remove_lemma thy_nm) lemmas cache 293 294 295fun clear_thys thy_deps sorted = 296let 297 val (new_deps,cache) = fold remove_thy sorted (Symtab.empty,Symtab.empty) 298 299 fun thy_to_file thy_nm = (Symtab.lookup thy_deps thy_nm |> the |> fst) ^ "/" ^ thy_nm ^ ".thy" 300 301 val file_deps = map (fn (thy,(f,deps)) => (thy_to_file thy,map thy_to_file deps)) (Symtab.dest thy_deps) 302 |> Symtab.make 303 304 fun is_already_imported file_nm dep = 305 let 306 val deps = Symtab.lookup file_deps file_nm |> the 307 |> remove (=) file_nm 308 in 309 exists (fn d => case (Symtab.lookup new_deps d) of SOME deps' => member (=) deps' dep | NONE => false) deps end 310 311 fun add_deps file_nm file = 312 let 313 val deps = Symtab.lookup new_deps file_nm |> the 314 |> filter_out (is_already_imported file_nm) 315 316 317 val index_line = find_index (fn (SOME s) => String.isPrefix "imports" s | NONE => false) file 318 319 val new_dep_line = if null deps then "" else " " ^ (space_implode " " deps) 320 321 val file' = 322 map_range (fn SOME s => SOME (s ^ new_dep_line) | NONE => error ("No import line in file " ^ file_nm)) (index_line,index_line) file 323 in 324 file' end 325 326 val cache' = Symtab.map add_deps cache 327in 328 (Symtab.map (fn file => fn body => File.write_list (Path.explode file) (map (fn SOME s => s ^ "\n" | NONE => "") body)) cache';()) end; 329 330 331\<close> 332 333end 334 335 336