@@ -71,21 +71,23 @@ module Symbols : sig
71
71
val show : D.State .t -> D .constant -> string
72
72
73
73
type table
74
+ type pruned_table
74
75
val pp_table : Format .formatter -> table -> unit
76
+ val pp_pruned_table : Format .formatter -> pruned_table -> unit
75
77
val table : table D.State .component
76
78
val compile_table : table -> D .symbol_table
77
79
val lock : table -> table
78
80
val locked : table -> bool
79
81
val equal : table -> table -> bool
80
- val size : table -> int
81
- val prune : table -> alive :D .Constants .Set .t -> table
82
+ val size : pruned_table -> int
83
+ val prune : table -> alive :D .Constants .Set .t -> pruned_table
82
84
(* debug *)
83
- val symbols : table -> string list
85
+ val symbols : pruned_table -> string list
84
86
85
87
val global_table : unit -> table
86
88
val uuid : table -> UUID .t
87
89
88
- val build_shift : ?lock_base : bool -> flags :flags -> base :D .State .t -> table -> (D.State .t * D .constant D.Constants.Map .t , string ) Stdlib.Result .t
90
+ val build_shift : ?lock_base : bool -> flags :flags -> base :D .State .t -> pruned_table -> (D.State .t * D .constant D.Constants.Map .t , string ) Stdlib.Result .t
89
91
90
92
end = struct
91
93
@@ -103,22 +105,26 @@ type table = {
103
105
uuid : Util.UUID .t ;
104
106
} [@@ deriving show ]
105
107
108
+ type pruned_table = {
109
+ c2s0 : string D.Constants.Map .t ;
110
+ c2t0 : D .term D.Constants.Map .t ;
111
+ } [@@ deriving show ]
112
+
106
113
let locked { locked } = locked
107
114
let lock t = { t with locked = true }
108
115
let uuid { uuid } = uuid
109
116
let equal t1 t2 =
110
117
locked t1 && locked t2 && uuid t1 = uuid t2
111
118
112
- let size t = D.Constants.Map. cardinal t.c2t
119
+ let size t = D.Constants.Map. cardinal t.c2t0
113
120
114
- let symbols { c2s } =
115
- List. map (fun (c ,s ) -> s ^ " :" ^ string_of_int c) (D.Constants.Map. bindings c2s )
121
+ let symbols { c2s0 } =
122
+ List. map (fun (c ,s ) -> s ^ " :" ^ string_of_int c) (D.Constants.Map. bindings c2s0 )
116
123
117
124
let prune t ~alive =
118
- { t with
119
- c2s = D.Constants.Map. filter (fun k _ -> D.Constants.Set. mem k alive) t.c2s;
120
- c2t = D.Constants.Map. filter (fun k _ -> D.Constants.Set. mem k alive) t.c2t;
121
- ast2ct = F.Map. filter (fun _ (k ,_ ) -> D.Constants.Set. mem k alive) t.ast2ct;
125
+ {
126
+ c2s0 = D.Constants.Map. filter (fun k _ -> D.Constants.Set. mem k alive) t.c2s;
127
+ c2t0 = D.Constants.Map. filter (fun k _ -> D.Constants.Set. mem k alive) t.c2t;
122
128
}
123
129
124
130
let table = D.State. declare
@@ -243,7 +249,7 @@ let build_shift ?(lock_base=false) ~flags:{ print_units } ~base symbols =
243
249
heuristic in unfolding) *)
244
250
List. fold_left (fun (base ,shift as acc ) (v , t ) ->
245
251
if v < 0 then
246
- let name = Map. find v symbols.c2s in
252
+ let name = Map. find v symbols.c2s0 in
247
253
try
248
254
let c, _ = F.Map. find (F. from_string name) base.ast2ct in
249
255
if c == v then acc
@@ -262,7 +268,7 @@ let build_shift ?(lock_base=false) ~flags:{ print_units } ~base symbols =
262
268
let base = { base with c2t = Map. add v t base.c2t } in
263
269
base, shift
264
270
)
265
- (base,Map. empty) (List. rev (Map. bindings symbols.c2t )))
271
+ (base,Map. empty) (List. rev (Map. bindings symbols.c2t0 )))
266
272
267
273
let build_shift ?lock_base ~flags ~base symbols =
268
274
try Stdlib.Result. Ok (build_shift ?lock_base ~flags ~base symbols)
@@ -516,7 +522,7 @@ let empty = {
516
522
end
517
523
518
524
type compilation_unit = {
519
- symbol_table : Symbols .table ;
525
+ symbol_table : Symbols .pruned_table ;
520
526
version : string ;
521
527
code : Flat .program ;
522
528
}
0 commit comments