termcode.ml 18.6 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5
6
7
8
9
10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

MARCHE Claude's avatar
MARCHE Claude committed
12
open Term
13

14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
(*******************************)
(*          explanations       *)
(*******************************)

let expl_regexp = Str.regexp "expl:\\(.*\\)"

let check_expl lab acc =
  let lab = lab.Ident.lab_string in
  if Str.string_match expl_regexp lab 0
  then Some (Str.matched_group 1 lab)
  else acc

let check_expl lab =
  if Ident.Slab.mem Split_goal.stop_split lab then None
  else Ident.Slab.fold check_expl lab None

let rec get_expl_fmla acc f =
  if f.t_ty <> None then acc else
  let res = check_expl f.Term.t_label in
  if res = None then match f.t_node with
    | Term.Ttrue | Term.Tfalse | Term.Tapp _ -> acc
    | Term.Tbinop(Term.Timplies,_,f) -> get_expl_fmla acc f
    | Term.Tlet _ | Term.Tcase _ | Term.Tquant (Term.Tforall, _) ->
        Term.t_fold get_expl_fmla acc f
    | _ -> raise Exit
  else if acc = None then res else raise Exit

let get_expl_fmla f = try get_expl_fmla None f with Exit -> None

let goal_expl_task ~root task =
  let gid = (Task.task_goal task).Decl.pr_name in
  let info =
    let fmla = Task.task_goal_fmla task in
    let res = get_expl_fmla fmla in
    if res <> None || not root then res else check_expl gid.Ident.id_label
  in
  gid, info, task

52
(* Shapes *)
53

54
type shape = string
55
56
57
let print_shape = Format.pp_print_string
let string_of_shape x = x
let shape_of_string x = x
58
let equal_shape (x:string) y = x = y
59

60
let debug = Debug.register_info_flag "session_pairing"
Andrei Paskevich's avatar
Andrei Paskevich committed
61
62
  ~desc:"Print@ debugging@ messages@ about@ reconstruction@ of@ \
         session@ trees@ after@ modification@ of@ source@ files."
63

64
65
66
let current_shape_version = 4

type shape_version = SV1 | SV2 | SV3
MARCHE Claude's avatar
MARCHE Claude committed
67

68
(* similarity code of terms, or of "shapes"
69

70
example:
71
72
73
74
75

  shape(forall x:int, x * x >= 0) =
         Forall(Int,App(infix_gteq,App(infix_st,Tvar 0,Tvar 0),Const(0)))
       i.e: de bruijn indexes, first-order term

MARCHE Claude's avatar
MARCHE Claude committed
76
77
78
*)

let vs_rename_alpha c h vs = incr c; Mvs.add vs !c h
79

MARCHE Claude's avatar
MARCHE Claude committed
80
81
let vl_rename_alpha c h vl = List.fold_left (vs_rename_alpha c) h vl

82
83
84
85
86
87
let rec pat_rename_alpha c h p = match p.pat_node with
  | Pvar v -> vs_rename_alpha c h v
  | Pas (p, v) -> pat_rename_alpha c (vs_rename_alpha c h v) p
  | Por (p, _) -> pat_rename_alpha c h p
  | _ -> Term.pat_fold (pat_rename_alpha c) h p

MARCHE Claude's avatar
MARCHE Claude committed
88
89

let tag_and = "A"
90
91
92
93
94
95
96
let tag_app = "a"
let tag_case = "C"
let tag_const = "c"
let tag_exists = "E"
let tag_eps = "e"
let tag_forall = "F"
let tag_false = "f"
MARCHE Claude's avatar
MARCHE Claude committed
97
let tag_impl = "I"
98
let tag_if = "i"
MARCHE Claude's avatar
MARCHE Claude committed
99
100
101
let tag_let = "L"
let tag_not = "N"
let tag_or = "O"
102
103
let tag_iff = "q"
let tag_true = "t"
MARCHE Claude's avatar
MARCHE Claude committed
104
let tag_var = "V"
105
106
let tag_wild = "w"
let tag_as = "z"
MARCHE Claude's avatar
MARCHE Claude committed
107

108
109
let ident_shape ~push id acc = push id.Ident.id_string acc

110
111
112
113
let const_shape ~push acc c =
  let b = Buffer.create 17 in
  Format.bprintf b "%a" Pretty.print_const c;
  push (Buffer.contents b) acc
MARCHE Claude's avatar
MARCHE Claude committed
114

115
116
117
118
119
120
let rec pat_shape ~(push:string->'a->'a) c m (acc:'a) p : 'a =
  match p.pat_node with
    | Pwild -> push tag_wild acc
    | Pvar _ -> push tag_var acc
    | Papp (f, l) ->
        List.fold_left (pat_shape ~push c m)
121
          (ident_shape ~push f.ls_name (push tag_app acc))
122
123
124
125
          l
    | Pas (p, _) -> push tag_as (pat_shape ~push c m acc p)
    | Por (p, q) ->
        pat_shape ~push c m (push tag_or (pat_shape ~push c m acc q)) p
MARCHE Claude's avatar
MARCHE Claude committed
126

MARCHE Claude's avatar
MARCHE Claude committed
127
128
let rec t_shape ~version ~(push:string->'a->'a) c m (acc:'a) t : 'a =
  let fn = t_shape ~version ~push c m in
MARCHE Claude's avatar
MARCHE Claude committed
129
130
131
132
  match t.t_node with
    | Tconst c -> const_shape ~push (push tag_const acc) c
    | Tvar v ->
        let x =
133
134
          try string_of_int (Mvs.find v m)
          with Not_found -> v.vs_name.Ident.id_string
MARCHE Claude's avatar
MARCHE Claude committed
135
136
137
138
        in
        push x (push tag_var acc)
    | Tapp (s,l) ->
        List.fold_left fn
139
          (ident_shape ~push s.ls_name (push tag_app acc))
MARCHE Claude's avatar
MARCHE Claude committed
140
          l
141
142
    | Tif (f,t1,t2) ->
      begin match version with
143
144
      | SV1 | SV2 -> fn (fn (fn (push tag_if acc) f) t1) t2
      | SV3 -> fn (fn (fn (push tag_if acc) t2) t1) f
145
      end
MARCHE Claude's avatar
MARCHE Claude committed
146
147
148
    | Tcase (t1,bl) ->
        let br_shape acc b =
          let p,t2 = t_open_branch b in
149
          match version with
150
          | SV1 | SV2 ->
151
152
153
            let acc = pat_shape ~push c m acc p in
            let m = pat_rename_alpha c m p in
            t_shape ~version ~push c m acc t2
154
          | SV3 ->
155
156
157
            let m1 = pat_rename_alpha c m p in
            let acc = t_shape ~version ~push c m1 acc t2 in
            pat_shape ~push c m acc p
MARCHE Claude's avatar
MARCHE Claude committed
158
        in
159
        begin match version with
160
        | SV1 | SV2 ->
161
          List.fold_left br_shape (fn (push tag_case acc) t1) bl
162
        | SV3 ->
163
164
165
166
          let acc = push tag_case acc in
          let acc = List.fold_left br_shape acc bl in
          fn acc t1
        end
MARCHE Claude's avatar
MARCHE Claude committed
167
168
169
    | Teps b ->
        let u,f = t_open_bound b in
        let m = vs_rename_alpha c m u in
MARCHE Claude's avatar
MARCHE Claude committed
170
        t_shape ~version ~push c m (push tag_eps acc) f
MARCHE Claude's avatar
MARCHE Claude committed
171
    | Tquant (q,b) ->
172
        let vl,triggers,f1 = t_open_quant b in
MARCHE Claude's avatar
MARCHE Claude committed
173
174
        let m = vl_rename_alpha c m vl in
        let hq = match q with Tforall -> tag_forall | Texists -> tag_exists in
175
176
        (* argument first, intentionally, to give more weight on A in
           forall x,A *)
MARCHE Claude's avatar
MARCHE Claude committed
177
        let acc = push hq (t_shape ~version ~push c m acc f1) in
178
179
180
181
        List.fold_right
          (fun trigger acc ->
             List.fold_right
               (fun t acc ->
MARCHE Claude's avatar
MARCHE Claude committed
182
                  t_shape ~version ~push c m acc t)
183
184
               trigger acc)
          triggers acc
185
186
187
188
189
190
191
192
193
    | Tbinop (o,f,g) ->
        let tag = match o with
          | Tand -> tag_and
          | Tor -> tag_or
          | Timplies -> tag_impl
          | Tiff -> tag_iff
        in
        fn (push tag (fn acc g)) f
          (* g first, intentionally, to give more weight on B in A->B *)
MARCHE Claude's avatar
MARCHE Claude committed
194
195
196
197
198
    | Tlet (t1,b) ->
        let u,t2 = t_open_bound b in
        let m = vs_rename_alpha c m u in
        begin
          match version with
199
            | SV1 ->
MARCHE Claude's avatar
MARCHE Claude committed
200
              t_shape ~version ~push c m (fn (push tag_let acc) t1) t2
201
            | SV2 | SV3 ->
MARCHE Claude's avatar
MARCHE Claude committed
202
203
204
              (* t2 first, intentionally *)
              fn (push tag_let (t_shape ~version ~push c m acc t2)) t1
        end
205
206
    | Tnot f ->
      begin match version with
207
208
      | SV1 | SV2 -> push tag_not (fn acc f)
      | SV3 -> fn (push tag_not acc) f
209
      end
210
211
    | Ttrue -> push tag_true acc
    | Tfalse -> push tag_false acc
MARCHE Claude's avatar
MARCHE Claude committed
212

213
(* (* dead code *)
MARCHE Claude's avatar
MARCHE Claude committed
214
let t_shape_buf ?(version=current_shape_version) t =
MARCHE Claude's avatar
MARCHE Claude committed
215
216
  let b = Buffer.create 17 in
  let push t () = Buffer.add_string b t in
MARCHE Claude's avatar
MARCHE Claude committed
217
  let () = t_shape ~version ~push (ref (-1)) Mvs.empty () t in
MARCHE Claude's avatar
MARCHE Claude committed
218
  Buffer.contents b
219
*)
MARCHE Claude's avatar
MARCHE Claude committed
220

221
let t_shape_task ~version t =
222
223
  let b = Buffer.create 17 in
  let push t () = Buffer.add_string b t in
224
  begin match version with
225
226
  | SV1 | SV2 -> ()
  | SV3 ->
227
228
229
    let _, expl, _ = goal_expl_task ~root:false t in
    Opt.iter (Buffer.add_string b) expl
  end;
230
231
232
  let f = Task.task_goal_fmla t in
  let () = t_shape ~version ~push (ref (-1)) Mvs.empty () f in
  Buffer.contents b
233

234
235
236
237
238
239
240
let t_shape_task ?(version=current_shape_version) t =
  let version = match version with
    | 1 -> SV1 | 2 -> SV2 | 3 | 4 -> SV3
    | _ -> assert false
  in
  t_shape_task ~version t

241
242
243
244
245
246
247
248
249
(* Checksums *)

type checksum = string
let print_checksum = Format.pp_print_string
let string_of_checksum x = x
let checksum_of_string x = x
let equal_checksum x y = (x : checksum) = y
let dumb_checksum = ""

250
251
type checksum_version = CV1 | CV2

252
253
module Checksum = struct

254
255
256
257
258
  let char (_,_,_,buf) c = Buffer.add_char buf c
  let int (_,_,_,buf as b) i =
    char b 'i'; Buffer.add_string buf (string_of_int i)
  let string (_,_,_,buf as b) s =
    char b '"'; Buffer.add_string buf (String.escaped s); char b '"'
259
  let option e b = function None -> char b 'n' | Some x -> char b 's'; e b x
260
  let list e b l = char b '['; List.iter (e b) l; char b ']'
261

262
  let ident_v1, clear_ident_v1 =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
263
    let hident = Ident.Hid.create 17 in
264
    let c = ref 0 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
265
    (fun b id ->
266
      int b (try Ident.Hid.find hident id
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
267
268
        with Not_found -> incr c; Ident.Hid.add hident id !c; !c)),
    (fun () -> Ident.Hid.clear hident; c := 0)
269

270
271
272
273
274
275
276
277
278
279
280
  let ident_v2 (_,c,m,_ as b) id =
    let i = match Ident.Mid.find_opt id !m with
      | Some i -> i
      | None -> incr c; m := Ident.Mid.add id !c !m; !c
    in
    int b i

  let ident (v,_,_,_ as b) id = match v with
    | CV1 -> ident_v1 b id
    | CV2 -> ident_v2 b id

281
282
283
  let const b c =
    let buf = Buffer.create 17 in
    Format.bprintf buf "%a" Pretty.print_const c;
284
    string b (Buffer.contents buf)
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303

  let tvsymbol b tv = ident b tv.Ty.tv_name

  let rec ty b t = match t.Ty.ty_node with
    | Ty.Tyvar tv -> char b 'v'; tvsymbol b tv
    | Ty.Tyapp (ts, tyl) -> char b 'a'; ident b ts.Ty.ts_name; list ty b tyl

  (* variable: the type, but not the name (we want alpha-equivalence) *)
  let vsymbol b vs = ty b vs.vs_ty

  (* start: _ V ident a o *)
  let rec pat b p = match p.pat_node with
    | Pwild -> char b '_'
    | Pvar vs -> char b 'v'; vsymbol b vs
    | Papp (f, l) -> char b 'a'; ident b f.ls_name; list pat b l
    | Pas (p, vs) -> char b 's'; pat b p; vsymbol b vs
    | Por (p, q) -> char b 'o'; pat b p; pat b q

  (* start: c V v i m e F E A O I q l n t f *)
304
  let rec term b t = match t.t_node with
305
    | Tconst c -> const b c
306
307
308
    | Tvar v -> char b 'v'; ident b v.vs_name
    | Tapp (s, l) -> char b 'a'; ident b s.ls_name; list term b l
    | Tif (f, t1, t2) -> char b 'i'; term b f; term b t1; term b t2
309
310
311
    | Tcase (t1, bl) ->
        let branch b br =
          let p, t2 = t_open_branch br in
312
          pat b p; term b t2
313
        in
314
        char b 'm'; term b t1; list branch b bl
315
316
    | Teps bf ->
        let vs, f = t_open_bound bf in
317
        char b 'e'; vsymbol b vs; term b f
318
319
320
321
    | Tquant (q, bf) ->
        let vl, triggers, f1 = t_open_quant bf in
        char b (match q with Tforall -> 'F' | Texists -> 'E');
        list vsymbol b vl;
322
323
        list (list term) b triggers;
        term b f1
324
325
326
327
328
329
330
    | Tbinop (o, f, g) ->
        let tag = match o with
          | Tand -> 'A'
          | Tor -> 'O'
          | Timplies -> 'I'
          | Tiff -> 'q'
        in
331
        char b tag; term b f; term b g
332
333
    | Tlet (t1, bt) ->
        let vs, t2 = t_open_bound bt in
334
335
336
        char b 'l'; vsymbol b vs; term b t1;
        term b t2
    | Tnot f -> char b 'n'; term b f
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
    | Ttrue -> char b 't'
    | Tfalse -> char b 'f'

  let tysymbol b ts =
    ident b ts.Ty.ts_name;
    list tvsymbol b ts.Ty.ts_args;
    option ty b ts.Ty.ts_def

  let lsymbol b ls =
    ident b ls.ls_name;
    list ty b ls.ls_args;
    option ty b ls.ls_value;
    list tvsymbol b (Ty.Stv.elements ls.ls_opaque);
    int b ls.ls_constr

352
  (* start: T D R L I P (C M) *)
353
354
355
356
357
358
359
360
361
362
363
364
365
  let decl b d = match d.Decl.d_node with
    | Decl.Dtype ts ->
        char b 'T'; tysymbol b ts
    | Decl.Ddata ddl ->
        let constructor b (ls, l) = lsymbol b ls; list (option lsymbol) b l in
        let data_decl b (ts, cl) = tysymbol b ts; list constructor b cl in
        char b 'D'; list data_decl b ddl
    | Decl.Dparam ls ->
        char b 'R'; lsymbol b ls
    | Decl.Dlogic ldl ->
        let logic_decl b (ls, defn) =
          lsymbol b ls;
          let vl, t = Decl.open_ls_defn defn in
366
367
          list vsymbol b vl;
          term b t
368
369
370
371
        in
        char b 'L'; list logic_decl b ldl
    | Decl.Dind (s, idl) ->
        let clause b (pr, f) =
372
          ident b pr.Decl.pr_name; term b f in
373
374
375
376
377
378
379
380
381
382
383
384
        let ind_decl b (ls, cl) = lsymbol b ls; list clause b cl in
        char b 'I'; char b (match s with Decl.Ind -> 'i' | Decl.Coind -> 'c');
        list ind_decl b idl
    | Decl.Dprop (k,n,t) ->
        let tag = match k with
          | Decl.Plemma -> "PL"
          | Decl.Paxiom -> "PA"
          | Decl.Pgoal  -> "PG"
          | Decl.Pskip  -> "PS"
        in
        string b tag;
        ident b n.Decl.pr_name;
385
        term b t
386
387
388
389
390
391
392
393
394
395
396
397

  let meta_arg_type b = function
    | Theory.MTty       -> char b 'y'
    | Theory.MTtysymbol -> char b 't'
    | Theory.MTlsymbol  -> char b 'l'
    | Theory.MTprsymbol -> char b 'p'
    | Theory.MTstring   -> char b 's'
    | Theory.MTint      -> char b 'i'

  let meta b m =
    string b m.Theory.meta_name;
    list meta_arg_type b m.Theory.meta_type;
398
    char b (if m.Theory.meta_excl then 't' else 'f')
399
400
401
402
403
404
405
406
407
408
409

  let meta_arg b = function
    | Theory.MAty t  -> char b 'y'; ty b t
    | Theory.MAts ts -> char b 't'; ident b ts.Ty.ts_name
    | Theory.MAls ls -> char b 'l'; ident b ls.ls_name
    | Theory.MApr pr -> char b 'p'; ident b pr.Decl.pr_name
    | Theory.MAstr s -> char b 's'; string b s
    | Theory.MAint i -> char b 'i'; int b i

  let tdecl b d = match d.Theory.td_node with
    | Theory.Decl d -> decl b d
410
411
412
    | Theory.Use _ -> assert false
    | Theory.Clone (th, _) ->
        char b 'C'; ident b th.Theory.th_name; list string b th.Theory.th_path
413
414
    | Theory.Meta (m, mal) -> char b 'M'; meta b m; list meta_arg b mal

415
  let task_v1 =
416
417
    let c = ref 0 in
    let m = ref Ident.Mid.empty in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
418
    let b = Buffer.create 8192 in
419
420
421
422
423
424
425
426
427
428
    fun t ->
      Task.task_iter (tdecl (CV1,c,m,b)) t;
      clear_ident_v1 ();
      let dnew = Digest.string (Buffer.contents b) in
      Buffer.clear b;
      Digest.to_hex dnew

  let task_v2 =
    let c = ref 0 in
    let m = ref Ident.Mid.empty in
429
    let b = Buffer.create 8192 in
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
    let task_hd t (cold,mold,dold) =
      c := cold;
      m := mold;
      tdecl (CV2,c,m,b) t.Task.task_decl;
      Buffer.add_string b (Digest.to_hex dold);
      let dnew = Digest.string (Buffer.contents b) in
      Buffer.clear b;
      let mnew = match t.Task.task_decl.Theory.td_node with
        | Theory.Decl d ->
            let m = Ident.Mid.set_inter !m d.Decl.d_news in
            Ident.Mid.set_union mold m
        | _ -> !m in
      !c, mnew, dnew
    in
    let tr = Trans.fold task_hd (0, Ident.Mid.empty, Digest.string "") in
    fun t ->
      let _,_,dnew = Trans.apply tr t in
      Digest.to_hex dnew
448
449
450
451
452
453
454
455
456
457
458
459
460

  let task ~version t = match version with
    | CV1 -> task_v1 t
    | CV2 -> task_v2 t
end

let task_checksum ?(version=current_shape_version) t =
  let version = match version with
    | 1 | 2 | 3 -> CV1
    | 4 -> CV2
    | _ -> assert false
  in
  Checksum.task ~version t
461
462

(*************************************************************)
463
(* Pairing of new and old subgoals                           *)
464
465
466
467
(*************************************************************)

(* we have an ordered list of new subgoals

468
     newgoals = [g1; g2; g3; ...]
469
470
471

   and a list of old subgoals

472
     oldgoals = [h1 ; h2 ; ... ]
473

474
   we build a list
475

476
     [g1, None; g2, Some (h3, false); g3, Some (h2, true); ...]
477

478
479
480
481
   where each new goal is mapped either to
   - None: no pairing at all
   - Some (h, false): exact matching (equal checksums)
   - Some (h, true): inexact matching (goal obsolete)
482
483
*)

484
485
486
487
488
module type S = sig
  type t
  val checksum : t -> string
  val shape    : t -> string
  val name     : t -> Ident.ident
489
end
490

491
module Pairing(Old: S)(New: S) = struct
492

493
494
495
496
  let rec lcp n s1 s2 =
    if String.length s1 <= n || String.length s2 <= n then n
    else if s1.[n] = s2.[n] then lcp (n+1) s1 s2 else n
  let lcp = lcp 0
497
498
499

  open Ident

500
501
  type any_goal = Old of Old.t | New of New.t

502
  (* doubly linked lists; left and right bounds point to themselves *)
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521

  type node = {
    mutable  prev: node;
            shape: string;
              elt: any_goal;
    mutable valid: bool;
    mutable  next: node;
  }

  let mk_node g =
    let s = match g with Old g -> Old.shape g | New g -> New.shape g in
    let rec n = { prev = n; shape = s; elt = g; next = n; valid = true } in n

  let rec iter_pairs f = function
    | [] | [_] -> ()
    | x :: (y :: _ as l) -> f x y; iter_pairs f l

  let build_list = iter_pairs (fun x y -> x.next <- y; y.prev <- x)

522
523
524
525
526
527
528
  let remove x =
    x.valid <- false;
    let p = x.prev and n = x.next in
    if p == x then n.prev <- n (* left bound *)
    else if n == x then p.next <- p (* right bound *)
    else begin p.next <- n; n.prev <- p end

529
530
531
532
533
534
535
536
537
538
  (* priority queues for pairs of nodes *)

  module E = struct
    type t = int * (node * node)
    let compare (v1, _) (v2, _) = Pervasives.compare v2 v1
  end
  module PQ = Pqueue.Make(E)

  let dprintf = Debug.dprintf debug

539
540
541
542
543
544
  let associate oldgoals newgoals =
    (* set up an array [result] containing the solution
       [new_goal_index g] returns the index of goal [g] in that array *)
    let new_goal_index = Hid.create 17 in
    let result =
      let make i newg =
545
        Hid.add new_goal_index (New.name newg) i; (newg, None) in
546
547
548
549
550
551
552
553
554
555
556
557
558
      Array.mapi make (Array.of_list newgoals) in
    let new_goal_index newg =
      try Hid.find new_goal_index (New.name newg)
      with Not_found -> assert false in
    (* phase 1: pair goals with identical checksums *)
    let old_checksums = Hashtbl.create 17 in
    let add oldg = Hashtbl.add old_checksums (Old.checksum oldg) oldg in
    List.iter add oldgoals;
    let collect acc newg =
      let c = New.checksum newg in
      try
        let oldg = Hashtbl.find old_checksums c in
        Hashtbl.remove old_checksums c;
559
        result.(new_goal_index newg) <- (newg, Some (oldg, false));
560
561
        acc
      with Not_found ->
562
        mk_node (New newg) :: acc
563
564
    in
    let newgoals = List.fold_left collect [] newgoals in
565
566
    let add _ oldg acc = mk_node (Old oldg) :: acc in
    let allgoals = Hashtbl.fold add old_checksums newgoals in
567
568
    Hashtbl.clear old_checksums;
    (* phase 2: pair goals according to shapes *)
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
    let compare e1 e2 = Pervasives.compare e1.shape e2.shape in
    let allgoals = List.sort compare allgoals in
    build_list allgoals;
    if allgoals <> [] then begin
      let dummy = let n = List.hd allgoals (* safe *) in 0, (n, n) in
      let pq = PQ.create ~dummy in
      let add x y = match x.elt, y.elt with
        | Old _, New _ | New _, Old _ -> PQ.add pq (lcp x.shape y.shape, (x, y))
        | Old _, Old _ | New _, New _ -> () in
      iter_pairs add allgoals;
      (* FIXME: exit earlier, as soon as we get min(old,new) pairs *)
      while not (PQ.is_empty pq) do
        let _, (x, y) = PQ.extract_min pq in
        if x.valid && y.valid then begin
          let o, n = match x.elt, y.elt with
            | New n, Old o | Old o, New n -> o, n | _ -> assert false in
          dprintf "[assoc] new pairing@.";
586
          result.(new_goal_index n) <- n, Some (o, true);
587
          if x.prev != x && y.next != y then add x.prev y.next;
588
589
          remove x;
          remove y
590
591
592
        end
      done
    end;
593
594
595
    Array.to_list result

end