Theory ExportInfo

1theory ExportInfo
2  imports AOT_misc
3begin
4
5local_setup‹fn ctxt =>
6let
7val thmToItems : (Symtab.set) Thmtab.table = Thmtab.empty
8val thy = Proof_Context.theory_of ctxt
9val global_facts = Global_Theory.facts_of thy;
10
11val thmToItems = (Facts.dest_all (Context.Proof ctxt) false [] global_facts |>
12  filter (fn (n, thms) => List.all (AOT_Theorems.member ctxt) thms andalso
13    (Option.isSome (AOT_get_item_number (Binding.name_of (Binding.qualified_name n)))))
14  |> fold (fn (n, thms) => fn thmtab => let
15    val name = Binding.name_of (Binding.qualified_name n)
16    val item = the (AOT_get_item_number name)
17    val thmtab = fold (fn thm => fn thmtab => let
18      in Thmtab.map_default (thm, Symtab.empty) (Symtab.insert_set item) thmtab end) thms thmtab
19  in
20    thmtab
21  end)) Thmtab.empty
22
23val thy = Proof_Context.theory_of ctxt
24fun get_aot_facts ctxt =
25let
26val global_facts = Global_Theory.facts_of thy;
27in
28Facts.dest_all (Context.Proof ctxt) false [] global_facts |>
29  map (fn (n, thms) => let
30    val {theory_long_name = thy_name, pos = pos, ...} =
31      Name_Space.the_entry (Facts.space_of global_facts) n
32    val name = Binding.name_of (Binding.qualified_name n)
33    val items = Symtab.keys (fold (fn thm => fn set =>
34        case Thmtab.lookup thmToItems thm of SOME set' => Symtab.merge (op=) (set,set')
35        | _ => set) thms Symtab.empty)
36    val items = if name = "AOT" orelse name = "AOT_defs" then [] else items
37  in
38    (Binding.name_of (Binding.qualified_name thy_name), name, items, pos)
39  end) |> filter (fn (_, _, items,_) => length items > 0 andalso length items < 10)
40end
41
42val facts = get_aot_facts ctxt
43val blob = XML.blob (maps (fn (thyname,key,items,pos) =>
44  [thyname,"|",key,"|"]@[String.concatWith " " items]@["\n"]) facts)
45val blob2 = XML.blob (maps (fn (thyname,key,items,pos) =>
46  [thyname,"|",key,"|", case Position.line_of pos of SOME x => Int.toString(x) | _ => "NONE"]@["\n"]) facts)
47in
48(Export.export thy (Path.binding0 (Path.make ["info"])) blob;
49 Export.export thy (Path.binding0 (Path.make ["info2"])) blob2; ctxt)
50end
51›
52
53end