termcode.ml 24.9 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
type checksum = string
let print_checksum = Format.pp_print_string
let string_of_checksum x = x
let checksum_of_string x = x
François Bobot's avatar
François Bobot committed
18
19
let equal_checksum x y = (x : checksum) = y
let dumb_checksum = ""
20

21
type shape = string
22
23
24
25
let print_shape = Format.pp_print_string
let string_of_shape x = x
let shape_of_string x = x

26
let debug = Debug.register_info_flag "session_pairing"
Andrei Paskevich's avatar
Andrei Paskevich committed
27
28
  ~desc:"Print@ debugging@ messages@ about@ reconstruction@ of@ \
         session@ trees@ after@ modification@ of@ source@ files."
29

MARCHE Claude's avatar
MARCHE Claude committed
30
31
let current_shape_version = 2

32
(* similarity code of terms, or of "shapes"
33

34
example:
35
36
37
38
39

  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
40
41
42
*)

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

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

46
47
48
49
50
51
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
52
53

let tag_and = "A"
54
55
56
let tag_app = "a"
let tag_case = "C"
let tag_const = "c"
57
let tag_Dtype = "Dt"
58
59
let tag_Ddata = "Dd"
let tag_Dparam = "Dv"
60
61
62
let tag_Dlogic = "Dl"
let tag_Dind = "Di"
let tag_Dprop = "Dp"
63
64
65
66
let tag_exists = "E"
let tag_eps = "e"
let tag_forall = "F"
let tag_false = "f"
MARCHE Claude's avatar
MARCHE Claude committed
67
let tag_impl = "I"
68
let tag_if = "i"
MARCHE Claude's avatar
MARCHE Claude committed
69
70
71
let tag_let = "L"
let tag_not = "N"
let tag_or = "O"
72
73
74
75
let tag_Plemma = "Pl"
let tag_Paxiom = "Pa"
let tag_Pgoal = "Pg"
let tag_Pskip = "Ps"
76
77
let tag_iff = "q"
let tag_true = "t"
78
79
80
81
let tag_tDecl = "TD"
let tag_tClone = "TC"
let tag_tUse = "TU"
let tag_tMeta = "TM"
MARCHE Claude's avatar
MARCHE Claude committed
82
let tag_var = "V"
83
84
let tag_wild = "w"
let tag_as = "z"
MARCHE Claude's avatar
MARCHE Claude committed
85

86
87
let ident_shape ~push id acc = push id.Ident.id_string acc

88
89
90
91
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
92

93
94
95
96
97
98
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)
99
          (ident_shape ~push f.ls_name (push tag_app acc))
100
101
102
103
          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
104

MARCHE Claude's avatar
MARCHE Claude committed
105
106
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
107
108
109
110
  match t.t_node with
    | Tconst c -> const_shape ~push (push tag_const acc) c
    | Tvar v ->
        let x =
111
112
          try string_of_int (Mvs.find v m)
          with Not_found -> v.vs_name.Ident.id_string
MARCHE Claude's avatar
MARCHE Claude committed
113
114
115
116
        in
        push x (push tag_var acc)
    | Tapp (s,l) ->
        List.fold_left fn
117
          (ident_shape ~push s.ls_name (push tag_app acc))
MARCHE Claude's avatar
MARCHE Claude committed
118
119
120
121
122
          l
    | Tif (f,t1,t2) -> fn (fn (fn (push tag_if acc) f) t1) t2
    | Tcase (t1,bl) ->
        let br_shape acc b =
          let p,t2 = t_open_branch b in
123
124
          let acc = pat_shape ~push c m acc p in
          let m = pat_rename_alpha c m p in
MARCHE Claude's avatar
MARCHE Claude committed
125
          t_shape ~version ~push c m acc t2
MARCHE Claude's avatar
MARCHE Claude committed
126
127
128
129
130
        in
        List.fold_left br_shape (fn (push tag_case acc) t1) bl
    | 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
131
        t_shape ~version ~push c m (push tag_eps acc) f
MARCHE Claude's avatar
MARCHE Claude committed
132
    | Tquant (q,b) ->
133
        let vl,triggers,f1 = t_open_quant b in
MARCHE Claude's avatar
MARCHE Claude committed
134
135
        let m = vl_rename_alpha c m vl in
        let hq = match q with Tforall -> tag_forall | Texists -> tag_exists in
136
137
        (* argument first, intentionally, to give more weight on A in
           forall x,A *)
MARCHE Claude's avatar
MARCHE Claude committed
138
        let acc = push hq (t_shape ~version ~push c m acc f1) in
139
140
141
142
        List.fold_right
          (fun trigger acc ->
             List.fold_right
               (fun t acc ->
MARCHE Claude's avatar
MARCHE Claude committed
143
                  t_shape ~version ~push c m acc t)
144
145
               trigger acc)
          triggers acc
146
147
148
149
150
151
152
153
154
    | 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
155
156
157
158
159
160
161
162
163
164
165
166
    | Tlet (t1,b) ->
        let u,t2 = t_open_bound b in
        let m = vs_rename_alpha c m u in
        begin
          match version with
            | 1 ->
              t_shape ~version ~push c m (fn (push tag_let acc) t1) t2
            | 2 ->
              (* t2 first, intentionally *)
              fn (push tag_let (t_shape ~version ~push c m acc t2)) t1
            | _ -> assert false
        end
167
168
169
    | Tnot f -> push tag_not (fn acc f)
    | Ttrue -> push tag_true acc
    | Tfalse -> push tag_false acc
MARCHE Claude's avatar
MARCHE Claude committed
170

MARCHE Claude's avatar
MARCHE Claude committed
171
let t_shape_buf ?(version=current_shape_version) t =
MARCHE Claude's avatar
MARCHE Claude committed
172
173
  let b = Buffer.create 17 in
  let push t () = Buffer.add_string b t in
MARCHE Claude's avatar
MARCHE Claude committed
174
  let () = t_shape ~version ~push (ref (-1)) Mvs.empty () t in
MARCHE Claude's avatar
MARCHE Claude committed
175
176
  Buffer.contents b

MARCHE Claude's avatar
MARCHE Claude committed
177
(*
MARCHE Claude's avatar
MARCHE Claude committed
178
179
180
181
182
183
184
let t_shape_list t =
  let push t l = t::l in
  List.rev (t_shape ~push (ref (-1)) Mvs.empty [] t)

let pr_shape_list fmt t =
  List.iter (fun s -> Format.fprintf fmt "%s" s) (t_shape_list t)

MARCHE Claude's avatar
MARCHE Claude committed
185
*)
MARCHE Claude's avatar
MARCHE Claude committed
186

187
188
(* shape of a task *)

189
let param_decl_shape ~(push:string->'a->'a) (acc:'a) ls : 'a =
190
  ident_shape ~push ls.ls_name acc
191

MARCHE Claude's avatar
MARCHE Claude committed
192
let logic_decl_shape ~version ~(push:string->'a->'a) (acc:'a) (ls,def) : 'a =
193
  let acc = ident_shape ~push ls.ls_name acc in
194
195
196
  let vl,t = Decl.open_ls_defn def in
  let c = ref (-1) in
  let m = vl_rename_alpha c Mvs.empty vl in
MARCHE Claude's avatar
MARCHE Claude committed
197
  t_shape ~version ~push c m acc t
198

MARCHE Claude's avatar
MARCHE Claude committed
199
let logic_ind_decl_shape ~version ~(push:string->'a->'a) (acc:'a) (ls,cl) : 'a =
200
  let acc = ident_shape ~push ls.ls_name acc in
201
  List.fold_right
MARCHE Claude's avatar
MARCHE Claude committed
202
    (fun (_,t) acc -> t_shape ~version ~push (ref (-1)) Mvs.empty acc t)
203
204
    cl acc

MARCHE Claude's avatar
MARCHE Claude committed
205
let propdecl_shape ~version ~(push:string->'a->'a) (acc:'a) (k,n,t) : 'a =
206
207
208
209
210
211
212
  let tag = match k with
    | Decl.Plemma -> tag_Plemma
    | Decl.Paxiom -> tag_Paxiom
    | Decl.Pgoal -> tag_Pgoal
    | Decl.Pskip -> tag_Pskip
  in
  let acc = push tag acc in
213
  let acc = ident_shape ~push n.Decl.pr_name acc in
MARCHE Claude's avatar
MARCHE Claude committed
214
  t_shape ~version ~push (ref(-1)) Mvs.empty acc t
215

216
217
218
219
220
221
let constructor_shape ~push (ls, _) acc = ident_shape ~push ls.ls_name acc

let data_decl_shape ~push (tys, cl) acc =
  List.fold_right (constructor_shape ~push)
    cl (ident_shape ~push tys.Ty.ts_name acc)

MARCHE Claude's avatar
MARCHE Claude committed
222
let decl_shape ~version ~(push:string->'a->'a) (acc:'a) d : 'a =
223
  match d.Decl.d_node with
224
225
226
    | Decl.Dtype _ts ->
        push tag_Dtype acc
    | Decl.Ddata tyl ->
227
        List.fold_right (data_decl_shape ~push)
228
229
230
          tyl (push tag_Ddata acc)
    | Decl.Dparam ls ->
        param_decl_shape ~push (push tag_Dparam acc) ls
231
232
    | Decl.Dlogic ldl ->
        List.fold_right
MARCHE Claude's avatar
MARCHE Claude committed
233
          (fun d acc -> logic_decl_shape ~version ~push acc d)
234
          ldl (push tag_Dlogic acc)
235
    | Decl.Dind (_, idl) ->
236
        List.fold_right
MARCHE Claude's avatar
MARCHE Claude committed
237
          (fun d acc -> logic_ind_decl_shape ~version ~push acc d)
238
          idl (push tag_Dind acc)
239
    | Decl.Dprop pdecl ->
MARCHE Claude's avatar
MARCHE Claude committed
240
        propdecl_shape ~version ~push (push tag_Dprop acc) pdecl
241

MARCHE Claude's avatar
MARCHE Claude committed
242
let tdecl_shape ~version ~(push:string->'a->'a) (acc:'a) t : 'a =
243
  match t.Theory.td_node with
MARCHE Claude's avatar
MARCHE Claude committed
244
    | Theory.Decl d -> decl_shape ~version ~push (push tag_tDecl acc) d
245
246
247
248
    | Theory.Meta _ -> push tag_tMeta acc
    | Theory.Clone _ -> push tag_tClone acc
    | Theory.Use _ -> push tag_tUse acc

MARCHE Claude's avatar
MARCHE Claude committed
249
let rec task_shape ~version ~(push:string->'a->'a) (acc:'a) t : 'a =
250
251
252
  match t with
    | None -> acc
    | Some t ->
253
     task_shape ~version ~push (tdecl_shape ~version ~push acc t.Task.task_decl)
254
255
          t.Task.task_prev

MARCHE Claude's avatar
MARCHE Claude committed
256

257
258
259
260
(* checksum of a task
   it is the MD5 digest of the shape
*)

MARCHE Claude's avatar
MARCHE Claude committed
261
let task_checksum ?(version=current_shape_version) t =
262
263
  let b = Buffer.create 257 in
  let push t () = Buffer.add_string b t in
MARCHE Claude's avatar
MARCHE Claude committed
264
  let () = task_shape ~version ~push () t in
265
266
267
268
  let shape = Buffer.contents b in
  Digest.to_hex (Digest.string shape)


269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
module Checksum = struct

  let char = Buffer.add_char
  let int b i = Buffer.add_string b (string_of_int i)
  let string b s =
    char b '"'; Buffer.add_string b (String.escaped s); char b '"'
  let option e b = function None -> char b 'n' | Some x -> char b 's'; e b x
  let list e b l = char b 'l'; List.iter (e b) l; char b 'l'

  let ident_printer = Ident.create_ident_printer []
  let ident b id = string b (Ident.id_unique ident_printer id)

  let const b c =
    let buf = Buffer.create 17 in
    Format.bprintf buf "%a" Pretty.print_const c;
    char b 'c'; string b (Buffer.contents buf)

  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 *)
  let rec term c m b t = match t.t_node with
    | Tconst c -> const b c
    | Tvar v ->
        begin try let x = Mvs.find v m in char b 'V'; int b x
        with Not_found -> char b 'v'; ident b v.vs_name end
    | Tapp (s, l) -> char b 'a'; ident b s.ls_name; list (term c m) b l
    | Tif (f, t1, t2) -> char b 'i'; term c m b f; term c m b t1; term c m b t2
    | Tcase (t1, bl) ->
        let branch b br =
          let p, t2 = t_open_branch br in
          pat b p;
          let m = pat_rename_alpha c m p in
          term c m b t2
        in
        char b 'm'; term c m b t1; list branch b bl
    | Teps bf ->
        let vs, f = t_open_bound bf in
        let m = vs_rename_alpha c m vs in
        char b 'e'; vsymbol b vs; term c m b f
    | Tquant (q, bf) ->
        let vl, triggers, f1 = t_open_quant bf in
        let m = vl_rename_alpha c m vl in
        char b (match q with Tforall -> 'F' | Texists -> 'E');
        list vsymbol b vl;
        list (list (term c m)) b triggers;
        term c m b f1
    | Tbinop (o, f, g) ->
        let tag = match o with
          | Tand -> 'A'
          | Tor -> 'O'
          | Timplies -> 'I'
          | Tiff -> 'q'
        in
        char b tag; term c m b f; term c m b g
    | Tlet (t1, bt) ->
        let vs, t2 = t_open_bound bt in
        char b 'l'; vsymbol b vs; term c m b t1;
        let m = vs_rename_alpha c m vs in
        term c m b t2
    | Tnot f -> char b 'n'; term c m b f
    | 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

  (* start: T D R L I P *)
  let decl b d = match d.Decl.d_node with
    | Decl.Dtype ts ->
        (* FIXME: alpha-equivalence for type variables as well *)
        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
          let c = ref (-1) in
          let m = vl_rename_alpha c Mvs.empty vl in
          list vsymbol b vl; (* FIXME: really needed? (we did lsymbol above) *)
          term c m b t
        in
        char b 'L'; list logic_decl b ldl
    | Decl.Dind (s, idl) ->
        let clause b (pr, f) =
          ident b pr.Decl.pr_name; term (ref (-1)) Mvs.empty b f in
        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;
        term (ref (-1)) Mvs.empty b t

  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;
    char b (if m.Theory.meta_excl then 't' else 'f');
    string b (string_of_format m.Theory.meta_desc) (* FIXME: necessary? *)

  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
    | Theory.Use _ | Theory.Clone _ -> () (* FIXME: OK? *)
    | Theory.Meta (m, mal) -> char b 'M'; meta b m; list meta_arg b mal

  let task t =
    let b = Buffer.create 257 in
    Ident.forget_all ident_printer;
    Task.task_iter (tdecl b) t;
    Buffer.contents b

end

MARCHE Claude's avatar
MARCHE Claude committed
432

433
434
435
436
437
438
439
440
441
442
443
(*************************)
(**       Pairing       **)

(** needed accessor *)
module type S = sig
  type t
  val checksum : t -> string
  val shape    : t -> string
  val name       : t -> Ident.ident
end

444
(*
445
446
447
448
449
450
451
module type Sold = sig
  type t
  val checksum : t -> string
  val shape    : t -> string
  val id       : t -> Ident.ident
(* .goal_name *)
end
452
*)
453

454
(*
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
module type Snew = sig
  type t
  val checksum : t -> string
  val shape    : t -> string
  (* Termcode.t_shape_buf ~version:!current_shape_version *)
  (*   (Task.task_goal_fmla g) *)

  val name     : t -> string (** for debugging *)
(* let id = (Task.task_goal g).Decl.pr_name in *)
(* let goal_name = gname.Ident.id_string ^ "." ^ (string_of_int (i+1)) in *)
(* let goal_name = Ident.id_register (Ident.id_derive goal_name id) in *)

  val id      : t -> Ident.ident
(* let id = (Task.task_goal g).Decl.pr_name in *)

(* let id = (Task.task_goal g).Decl.pr_name in *)
(* let goal_name = gname.Ident.id_string ^ "." ^ (string_of_int (i+1)) in *)
(* let goal_name = Ident.id_register (Ident.id_derive goal_name id) in *)


end
476
*)
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781


(*************************************************************)
(* pairing of new and old subgoals of a given transformation *)
(*************************************************************)

(* we have an ordered list of new subgoals

           subgoals = [g1; g2; g3; ...]

   and a list of old subgoals

          old_subgoals = [h1 ; h2 ; ... ]

   we build a map from each new subgoal g to tuples
       (id,subgoal_name,subtask,sum,old_subgoal,obsolete)

   where
     id = name of the goal of g
     subgoal_name = name of parent goal with "dot n" added
     subtask = the corresponding task
     sum = the checksum of that task
     old_subgoal = ref to an optional old subgoal which is paired with g
     obsolete = true when paired to an old goal with different checksum

*)

module AssoMake (Old : S) (New : S) = struct

type 'a any_goal =
  | New_goal of int
  | Old_goal of Old.t

let array_map_list f l =
  let r = ref l in
  Array.init (List.length l)
    (fun i ->
       match !r with
         | [] -> assert false
         | x::rem -> r := rem; f i x)

let associate (old_goals : Old.t list) new_goals =
  (*
     we make a map of old goals indexed by their checksums
  *)
  let old_goals_map = Hashtbl.create 7 in
  List.iter
    (fun g -> Hashtbl.add old_goals_map (Old.checksum g) g)
    old_goals;
  (*
     we make an array of new goals with their numbers and checksums
  *)
  let new_goals_array =
    array_map_list
      (fun i g -> i,g)
      new_goals
  in
  let pairing_array =
    Array.make (Array.length new_goals_array) None
  in
  let obsolete_array =
    Array.make (Array.length new_goals_array) false
  in
  (*
     Phase 1: we first associate each new goal for which there is an
     old goal with the same checksum.
  *)
  let associate_goals ~obsolete i g =
    pairing_array.(i) <- Some g;
    obsolete_array.(i) <- obsolete;
    Hashtbl.remove old_goals_map (Old.checksum g)
  in
  Array.iter
    (fun (i,g) ->
       try
         let h = Hashtbl.find old_goals_map (New.checksum g) in
         (* an old goal has the same checksum *)
         Debug.dprintf debug
           "Merge phase 1: old goal '%s' -> new goal '%s'@."
           (Old.name h).Ident.id_string (New.name g).Ident.id_string;
         associate_goals ~obsolete:false i h
       with Not_found ->
         Debug.dprintf debug
           "Merge phase 1: no old goal -> new goal '%s'@."
           (New.name g).Ident.id_string;
         ())
    new_goals_array;
  (* Phase 2: we now build a list of all remaining new and old goals,
     ordered by shapes, then by name *)
  let old_goals_without_pairing =
    Hashtbl.fold
      (fun _ g acc ->
         let s = (Old.shape g) in
         if s = "" then
           (* We don't try to associate old goals without shapes:
              they will be paired in order in next phase *)
           acc
         else
           (s,Old_goal g)::acc)
      old_goals_map
      []
  in
  let all_goals_without_pairing =
    Array.fold_left
      (fun acc (i,g) ->
         match pairing_array.(i) with
           | Some _ -> acc
           | None ->
               let shape = New.shape g
                 (* Termcode.t_shape_buf ~version:!current_shape_version *)
                 (*   (Task.task_goal_fmla g) *)
               in
               (* shape_array.(i) <- shape; *)
               (shape,New_goal i)::acc)
      old_goals_without_pairing
      new_goals_array
  in
  let sort_by_shape =
    List.sort (fun (s1,_) (s2,_) -> String.compare s1 s2)
      all_goals_without_pairing
  in
  if Debug.test_flag debug then begin
    Debug.dprintf debug "[Merge] pairing the following shapes:@.";
    List.iter
      (fun (s,g) ->
         match g with
           | New_goal _ ->
               Debug.dprintf debug "new: %s@." s
           | Old_goal _ ->
               Debug.dprintf debug "old: %s@." s)
      sort_by_shape;
  end;
  let rec similarity_shape n s1 s2 =
    if String.length s1 <= n || String.length s2 <= n then n else
      if s1.[n] = s2.[n] then similarity_shape (n+1) s1 s2
      else n
  in
(*  let rec match_shape (opt:int option) goals : bool =
    (* when [opt] is [Some n] then it means [goals] starts with a goal g
       which is already claimed to be associated by the former goal h.
       We return a boolean which is true when that first goal g was also
       claimed by the next goal, with a proximity measure larger than n,
       meaning that the former goal h cannot associate with g
    *)
    match goals with
      | [] -> false
      | (si,New_goal i)::rem ->
          begin match rem with
            | [] -> false
            | (_,New_goal _)::_ ->
                let (_:bool) = match_shape None rem in false
            | (sh,Old_goal h)::_ ->
                try_associate si i sh h opt rem
          end
      | (sh,Old_goal h)::rem ->
          begin match rem with
            | [] -> false
            | (_,Old_goal _)::_ ->
                let (_:bool) = match_shape None rem in false
            | (si,New_goal i)::_ ->
                try_associate si i sh h opt rem
          end
  and try_associate si i sh h opt rem =
    let n = similarity_shape 0 si sh in
    Debug.dprintf debug "[Merge] try_associate: claiming \
      similarity %d for new shape@\n%s@\nand old shape@\n%s@." n si sh;
    if (match opt with
      | None ->
          Debug.dprintf debug "[Merge] try_associate: \
            no previous claim@.";
          true
      | Some m ->
          Debug.dprintf debug "[Merge] try_associate: \
            previous claim was %d@." m;
          m < n)
    then
      (* try to associate i with h *)
      let b = match_shape (Some n) rem in
      if b then
        begin
          (* h or i was already paired in rem *)
          Debug.dprintf debug "[Merge] try_associate: \
            failed because claimed further@.";
          false
        end
      else
        begin
          Debug.dprintf debug "[Merge] try_associate: \
            succeeded to associate new goal@\n%s@\nwith \
            old goal@\n%s@." si sh;
          associate_goals ~obsolete:true i h;
          true
        end
    else
      (* no need to try to associate i with h *)
      begin
        Debug.dprintf debug "[Merge] try_associate: \
          no claim further attempted@.";
        let (_:bool) = match_shape None rem in
        false
      end
  in
  let (_:bool) = match_shape None sort_by_shape in
*)
  let rec match_shape (min:int) goals : bool * (string * 'a any_goal) list =
    (* try to associate in [goals] each pair of old and new goal whose
       similarity is at least [min]. Returns a pair [(b,rem)] where
       [rem] is the sublist of [goals] made of goals which have not
       been paired, and [b] is a boolean telling that the head of
       [rem] is the same has the head of [goals] *)
    match goals with
      | [] -> (true, goals)
      | ((si,New_goal i) as hd)::rem ->
          begin match rem with
            | [] -> (true, goals)
            | (_,New_goal _)::_ ->
                let (b,rem2) = match_shape min rem in
                if b then
                  (true, hd::rem2)
                else
                  match_shape min (hd::rem2)
            | (sh,Old_goal h)::_ ->
                try_associate min si i sh h hd rem
          end
      | ((sh,Old_goal h) as hd)::rem ->
          begin match rem with
            | [] -> (true, goals)
            | (_,Old_goal _)::_ ->
                let (b,rem2) = match_shape min rem in
                if b then
                  (true, hd::rem2)
                else
                  match_shape min (hd::rem2)
            | (si,New_goal i)::_ ->
                try_associate min si i sh h hd rem
          end
            (** si : shape of i
                i  : id of the new goal
                sh : shape of h
                h  : an old goal
                hd : the head
                rem : the tail of the list *)
  and try_associate min si i sh h hd rem =
    let n = similarity_shape 0 si sh in
    Debug.dprintf debug "[Merge] try_associate: claiming \
      similarity %d for new shape@\n%s@\nand old shape@\n%s@." n si sh;
    if n < min then
      begin
        Debug.dprintf debug "[Merge] try_associate: claiming \
          dropped because similarity lower than min = %d@." min;
        let (b,rem2) = match_shape min rem in
        if b then
          (true, hd::rem2)
        else
          match_shape min (hd::rem2)
      end
    else
      match match_shape n rem with
        | false, rem2 ->
            Debug.dprintf debug "[Merge] try_associate: claiming \
              dropped because head was consumed by larger similarity@.";
            match_shape min (hd::rem2)
        | true, [] -> assert false
        | true, _::rem2 ->
            Debug.dprintf debug "[Merge] try_associate: claiming \
              succeeded (similarity %d) for new shape@\n%s@\nand \
              old shape@\n%s@." n si sh;
            associate_goals ~obsolete:true i h;
            let (_,rem3) = match_shape min rem2 in
            (false, rem3)
  in
  let (_b,_rem) = match_shape 0 sort_by_shape in
  (*
     Phase 3: we now associate remaining new goals to the remaining
     old goals in the same order as original
  *)
  Debug.dprintf debug "[Merge] phase 3: associate remaining goals@.";
  let remaining_old_goals =
    Hashtbl.fold
      (fun _ g acc -> (Old.name g,g)::acc)
      old_goals_map
      []
  in
  let remaining_old_goals =
    ref (List.sort (fun (s1,_) (s2,_) ->
      String.compare s1.Ident.id_string s2.Ident.id_string)
           remaining_old_goals)
  in
  Array.iteri
    (fun i opt ->
       match opt with
         | Some _ -> ()
         | None ->
             match !remaining_old_goals with
               | [] -> ()
               | (_,h) :: rem ->
                   remaining_old_goals := rem;
                   associate_goals ~obsolete:true i h)
    pairing_array;

  Array.fold_right
    (fun (i,g) res -> (g, pairing_array.(i), obsolete_array.(i))::res)
    new_goals_array []

end