1structure TheoryGraph :> TheoryGraph = 2struct 3 4open Portable Theory 5 6 7type thy = {thyname : string} 8exception NotFound of thy 9val thy_compare : thy * thy -> order = 10 inv_img_cmp #thyname String.compare 11 12type thyset = thy HOLset.set 13 14fun toThy s : thy = {thyname = s} 15val slist_to_thyset = 16 List.foldl (fn (s,acc) => HOLset.add(acc,{thyname = s})) 17 (HOLset.empty thy_compare) 18 19type t = (thy,thyset) Binarymap.dict 20 21val empty : t = Binarymap.mkDict thy_compare 22 23fun member G thy = 24 case Binarymap.peek(G, thy) of 25 NONE => false 26 | SOME _ => true 27 28fun parents G thy = Binarymap.find (G, thy) 29 30fun ancestors G thy = 31 let 32 fun recurse worklist acc = 33 case worklist of 34 [] => acc 35 | thy::rest => 36 let 37 val ps_set = parents G thy 38 in 39 recurse (HOLset.listItems ps_set @ rest) 40 (HOLset.union(acc,ps_set)) 41 end 42 in 43 recurse [thy] (HOLset.empty thy_compare) 44 end 45 46(* GREATER implies that thy1 is a descendent of thy2 *) 47fun ancestor_compare G (thy1,thy2) = 48 if thy1 = thy2 then SOME EQUAL 49 else 50 let 51 val ancs1 = ancestors G thy1 52 in 53 if HOLset.member(ancs1,thy2) then SOME GREATER 54 else 55 let 56 val ancs2 = ancestors G thy2 57 in 58 if HOLset.member(ancs2, thy1) then SOME LESS 59 else NONE 60 end 61 end 62 63fun eliminate_redundant_ancestors G thylist = 64 let 65 fun do1 thy rest acclist all_incomparable = 66 case rest of 67 [] => (thy::acclist, all_incomparable) 68 | thy'::rest' => 69 case ancestor_compare G (thy, thy') of 70 NONE => do1 thy rest' (thy'::acclist) all_incomparable 71 | SOME LESS => (acclist @ rest, false) 72 | SOME EQUAL => (acclist @ rest, false) 73 | SOME GREATER => do1 thy rest' acclist false 74 fun recurse thylist = 75 case thylist of 76 [] => [] 77 | th::rest => 78 let 79 val (rest', all_incomparable) = do1 th rest [] true 80 in 81 if all_incomparable then hd rest' :: recurse (tl rest') 82 else recurse rest' 83 end 84 in 85 recurse thylist 86 end 87 88fun insert (newthy, parents) G = 89 case List.find (not o member G) parents of 90 SOME p => raise NotFound p 91 | NONE => 92 let 93 val ps' = eliminate_redundant_ancestors G parents 94 in 95 Binarymap.insert(G, newthy, HOLset.fromList thy_compare ps') 96 end 97 98fun current () = 99 let 100 fun recurse g thy_s = 101 let 102 val ps = Theory.parents thy_s 103 val g = List.foldl (fn (p,g) => recurse g p) g ps 104 in 105 insert(toThy thy_s, map toThy ps) g 106 end 107 in 108 recurse empty (current_theory()) 109 end 110 111 112 113end 114