1structure SharingTables :> SharingTables =
2struct
3
4open Term Type
5
6structure Map = Binarymap
7
8(* ----------------------------------------------------------------------
9    IDs (also known as Theory-X pairs, where X is a Name for a constant,
10    or Tyops for types)
11   ---------------------------------------------------------------------- *)
12
13type id = {Thy : string, Other : string}
14type idtable = {idsize : int,
15                idmap : (id, int) Map.dict,
16                idlist : id list}
17
18fun make_shared_id (id : id) idtable =
19    case Map.peek(#idmap idtable, id) of
20      SOME i => (i, idtable)
21    | NONE => let
22        val {idsize, idmap, idlist} = idtable
23      in
24        (idsize, {idsize = idsize + 1,
25                  idmap = Map.insert(idmap, id, idsize),
26                  idlist = id :: idlist})
27      end
28fun id_compare ({Other = id1, Thy = thy1}, {Other = id2, Thy = thy2}) =
29    case String.compare(id1, id2) of
30      EQUAL => String.compare(thy1, thy2)
31    | x => x
32
33
34val empty_idtable : idtable = {idsize = 0,
35                               idmap = Map.mkDict id_compare,
36                               idlist = []}
37
38
39val CB = PP.block PP.CONSISTENT 0
40val out = PP.add_string
41val NL = PP.NL
42
43fun output_idtable name (idtable : idtable) = let
44  val idlist = List.rev (#idlist idtable)
45  fun print_id {Thy, Other} =
46    out ("ID(" ^ Lib.mlquote Thy^ ", "^Lib.mlquote Other^")")
47  val print_ids = PP.pr_list print_id [PP.add_break(1,0)]
48in
49  CB [
50    out ("val "^name^" = "), NL,
51    out ("  let fun ID(thy,oth) = {Thy = thy, Other = oth}"), NL,
52    out ("  in Vector.fromList"), NL,
53    out ("["),
54    PP.block PP.INCONSISTENT 0 (print_ids idlist),
55    out "]", NL,
56    out "end;", NL
57  ]
58end
59
60fun theoryout_idtable (idtable : idtable) = let
61  val idlist = List.rev (#idlist idtable)
62  fun print_id {Thy, Other} = out (Lib.mlquote Thy^ " " ^ Lib.mlquote Other)
63  val print_ids = PP.pr_list print_id [PP.add_string ",", PP.add_break(1,0)]
64in
65  CB [out "[",
66      PP.block PP.INCONSISTENT 1 (print_ids idlist),
67      out "]"
68  ]
69end
70
71(* ----------------------------------------------------------------------
72    Types
73   ---------------------------------------------------------------------- *)
74
75datatype shared_type = TYV of string
76                     | TYOP of int list
77
78type typetable = {tysize : int,
79                  tymap : (hol_type, int)Map.dict,
80                  tylist : shared_type list}
81
82fun make_shared_type ty idtable table =
83    case Map.peek(#tymap table, ty) of
84      SOME i => (i, idtable, table)
85    | NONE => let
86      in
87        if is_vartype ty then let
88            val {tysize, tymap, tylist} = table
89          in
90            (tysize, idtable,
91             {tysize = tysize + 1,
92              tymap = Map.insert(tymap, ty, tysize),
93              tylist = TYV (dest_vartype ty) :: tylist})
94          end
95        else let
96            val {Thy, Tyop, Args} = dest_thy_type ty
97            val (id, idtable0) =
98                make_shared_id {Thy = Thy, Other = Tyop} idtable
99            fun foldthis (tyarg, (results, idtable, table)) = let
100              val (result, idtable', table') =
101                  make_shared_type tyarg idtable table
102            in
103              (result::results, idtable', table')
104            end
105            val (newargs, idtable', table') =
106                List.foldr foldthis ([], idtable0, table) Args
107            val {tysize, tymap, tylist} = table'
108          in
109            (tysize, idtable',
110             {tysize = tysize + 1,
111              tymap = Map.insert(tymap, ty, tysize),
112              tylist = TYOP (id :: newargs) :: tylist})
113          end
114      end
115
116val empty_tytable : typetable =
117    {tysize = 0, tymap = Map.mkDict Type.compare, tylist = [] }
118
119fun build_type_vector idv shtylist = let
120  fun build1 (shty, (n, tymap)) =
121      case shty of
122        TYV s => (n + 1, Map.insert(tymap, n, Type.mk_vartype s))
123      | TYOP idargs => let
124          val (id, Args) = valOf (List.getItem idargs)
125          val args = map (fn i => Map.find(tymap, i)) Args
126          val {Thy,Other} = Vector.sub(idv, id)
127        in
128          (n + 1,
129           Map.insert(tymap, n,
130                            Type.mk_thy_type {Thy = Thy, Tyop = Other,
131                                              Args = args}))
132        end
133  val (_, tymap) =
134      List.foldl build1 (0, Map.mkDict Int.compare) shtylist
135in
136  Vector.fromList (map #2 (Map.listItems tymap))
137end
138
139fun output_typetable {idtable_nm,tytable_nm} (tytable : typetable) = let
140  fun output_shtype shty =
141      case shty of
142        TYV s => out ("TYV "^Lib.mlquote s)
143      | TYOP args =>
144        out ("TYOP ["^
145             String.concat (Lib.commafy (map Int.toString args))^ "]")
146  val output_shtypes = PP.pr_list output_shtype [out ",", PP.add_break (1,0)]
147in
148  CB [
149    out "local open SharingTables", NL, out "in", NL,
150    out ("val "^tytable_nm^" = build_type_vector "^idtable_nm), NL,
151    out ("["),
152    PP.block PP.INCONSISTENT 0 (output_shtypes (List.rev (#tylist tytable))),
153    out "]", NL, out "end", NL
154  ]
155end
156
157fun theoryout_typetable (tytable : typetable) = let
158  fun output_shtype shty =
159      case shty of
160        TYV s => out ("TYV "^ Lib.mlquote s)
161      | TYOP args =>
162        out ("TYOP "^ String.concatWith " " (map Int.toString args))
163  val output_shtypes = PP.pr_list output_shtype [out ",", PP.add_break (1,0)]
164in
165  CB [
166    out "[",
167    PP.block PP.INCONSISTENT 1 (output_shtypes (List.rev (#tylist tytable))),
168    out "]"
169  ]
170end
171
172
173(* ----------------------------------------------------------------------
174    Terms
175   ---------------------------------------------------------------------- *)
176
177datatype shared_term = TMV of string * int
178                     | TMC of int * int
179                     | TMAp of int * int
180                     | TMAbs of int * int
181
182type termtable = {termsize : int,
183                  termmap : (term, int)Map.dict,
184                  termlist : shared_term list}
185
186val empty_termtable : termtable =
187    {termsize = 0, termmap = Map.mkDict Term.compare, termlist = [] }
188
189fun make_shared_term tm (tables as (idtable,tytable,tmtable)) =
190    case Map.peek(#termmap tmtable, tm) of
191      SOME i => (i, tables)
192    | NONE => let
193      in
194        if is_var tm then let
195            val (s, ty) = dest_var tm
196            val (ty_i, idtable, tytable) =
197                make_shared_type ty idtable tytable
198            val {termsize, termmap, termlist} = tmtable
199          in
200            (termsize,
201             (idtable, tytable,
202              {termsize = termsize + 1,
203               termmap = Map.insert(termmap, tm, termsize),
204               termlist = TMV (s, ty_i) :: termlist}))
205          end
206        else if is_const tm then let
207            val {Thy,Name,Ty} = dest_thy_const tm
208            val (id_i, idtable) =
209                make_shared_id {Thy = Thy, Other = Name} idtable
210            val (ty_i, idtable, tytable) =
211                make_shared_type Ty idtable tytable
212            val {termsize, termmap, termlist} = tmtable
213          in
214            (termsize,
215             (idtable, tytable,
216              {termsize = termsize + 1,
217               termmap = Map.insert(termmap, tm, termsize),
218               termlist = TMC (id_i, ty_i) :: termlist}))
219          end
220        else if is_comb tm then let
221            val (f, x) = dest_comb tm
222            val (f_i, tables) = make_shared_term f tables
223            val (x_i, tables) = make_shared_term x tables
224            val (idtable, tytable, tmtable) = tables
225            val {termsize, termmap, termlist} = tmtable
226          in
227            (termsize,
228             (idtable, tytable,
229              {termsize = termsize + 1,
230               termmap = Map.insert(termmap, tm, termsize),
231               termlist = TMAp(f_i, x_i) :: termlist}))
232          end
233        else  (* must be an abstraction *) let
234            val (v, body) = dest_abs tm
235            val (v_i, tables) = make_shared_term v tables
236            val (body_i, tables) = make_shared_term body tables
237            val (idtable, tytable, tmtable) = tables
238            val {termsize, termmap, termlist} = tmtable
239          in
240            (termsize,
241             (idtable, tytable,
242              {termsize = termsize + 1,
243               termmap = Map.insert(termmap, tm, termsize),
244               termlist = TMAbs(v_i, body_i) :: termlist}))
245          end
246      end
247
248fun build_term_vector idv tyv shtmlist = let
249  fun build1 (shtm, (n, tmmap)) =
250      case shtm of
251        TMV (s, tyn) => (n + 1,
252                         Map.insert(tmmap, n, mk_var(s, Vector.sub(tyv, tyn))))
253      | TMC (idn, tyn) => let
254          val {Thy, Other} = Vector.sub(idv, idn)
255          val ty = Vector.sub(tyv, tyn)
256        in
257          (n + 1, Map.insert(tmmap, n, mk_thy_const {Name = Other, Thy = Thy,
258                                                     Ty = ty}))
259        end
260      | TMAp (f_n, xn) =>
261        (n + 1, Map.insert(tmmap, n, mk_comb(Map.find(tmmap, f_n),
262                                             Map.find(tmmap, xn))))
263      | TMAbs (vn, bodyn) =>
264        (n + 1, Map.insert(tmmap, n, mk_abs(Map.find(tmmap, vn),
265                                            Map.find(tmmap, bodyn))))
266  val (_, tmmap) = List.foldl build1 (0, Map.mkDict Int.compare) shtmlist
267in
268  Vector.fromList (map #2 (Map.listItems tmmap))
269end
270
271fun output_termtable names (tmtable: termtable) = let
272  val {idtable_nm,tytable_nm,termtable_nm} = names
273  fun ipair_string (x,y) = "("^Int.toString x^", "^Int.toString y^")"
274  fun output_shtm shtm =
275    case shtm of
276        TMV (s, tyn) => out ("TMV(" ^ Lib.mlquote s ^", "^Int.toString tyn^")")
277      | TMC p => out ("TMC"^ipair_string p)
278      | TMAp p => out ("TMAp"^ipair_string p)
279      | TMAbs p => out ("TMAbs"^ipair_string p)
280  val output_shtms = PP.pr_list output_shtm [out ",", PP.add_break(1,0)]
281in
282  CB [
283    out ("local open SharingTables"), NL,
284    out ("in"), NL,
285    out ("val "^termtable_nm^" = build_term_vector "^idtable_nm^" "^
286         tytable_nm), NL,
287    out ("["),
288    PP.block PP.INCONSISTENT 0 (output_shtms (List.rev (#termlist tmtable))),
289    out ("]"), NL,
290    out "end", NL
291  ]
292end;
293
294fun theoryout_termtable (tmtable: termtable) =
295  let
296    fun ipair_string (x,y) = Int.toString x^" "^Int.toString y
297    fun output_shtm shtm =
298      case shtm of
299          TMV (s, tyn) =>
300            out ("TMV " ^ Lib.mlquote s ^" "^Int.toString tyn)
301        | TMC p => out ("TMC "^ipair_string p)
302        | TMAp p => out ("TMAp "^ipair_string p)
303        | TMAbs p => out ("TMAbs "^ipair_string p)
304    val output_shtms = PP.pr_list output_shtm [out ",", PP.add_break(1,0)]
305  in
306    CB [
307      out ("["),
308      PP.block PP.INCONSISTENT 1 (output_shtms (List.rev (#termlist tmtable))),
309      out ("]")
310    ]
311  end
312
313end; (* struct *)
314