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