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