termcode.ml 28.2 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5
6
7
8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11

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

14
15
16
17
(*******************************)
(*          explanations       *)
(*******************************)

18
19
20
21
22
23
let expl_prefixes = ref ["expl:"]

let arg_extra_expl_prefix =
  ("--extra-expl-prefix",
   Arg.String (fun s -> expl_prefixes := s :: !expl_prefixes),
   "<s> register s as an additional prefix for VC explanations")
24

Andrei Paskevich's avatar
Andrei Paskevich committed
25
26
27
28
let collect_expls attr =
  Ident.Sattr.fold
    (fun attr acc ->
       let attr = attr.Ident.attr_string in
29
30
31
32
33
       let rec aux l =
         match l with
           | [] -> acc
           | p :: r ->
              try
Andrei Paskevich's avatar
Andrei Paskevich committed
34
                let s = Strings.remove_prefix p attr in s :: acc
35
36
              with Not_found -> aux r
       in aux !expl_prefixes)
Andrei Paskevich's avatar
Andrei Paskevich committed
37
    attr
38
39
40
41
42
43
44
    []

let concat_expls = function
  | [] -> None
  | [l] -> Some l
  | l :: ls -> Some (l ^ " (" ^ String.concat ". " ls ^ ")")

Andrei Paskevich's avatar
Andrei Paskevich committed
45
let search_attrs callback =
46
47
  let rec aux acc f =
    if f.t_ty <> None then acc
Andrei Paskevich's avatar
Andrei Paskevich committed
48
    else if Ident.Sattr.mem Term.stop_split f.Term.t_attrs then acc
49
    else
Andrei Paskevich's avatar
Andrei Paskevich committed
50
      let res = callback f.Term.t_attrs in
51
52
53
54
55
56
57
58
59
60
      if res = [] then match f.t_node with
        | Term.Ttrue | Term.Tfalse | Term.Tapp _ -> acc
        | Term.Tbinop (Term.Timplies, _, f) -> aux acc f
        | Term.Tlet _ | Term.Tcase _ | Term.Tquant (Term.Tforall, _) ->
          Term.t_fold aux acc f
        | _ -> raise Exit
      else if acc = [] then res
      else raise Exit
  in
  aux []
61

62
let get_expls_fmla =
Andrei Paskevich's avatar
Andrei Paskevich committed
63
  let search = search_attrs collect_expls in
64
  fun f -> try search f with Exit -> []
65
66
67
68

let goal_expl_task ~root task =
  let gid = (Task.task_goal task).Decl.pr_name in
  let info =
69
70
71
72
    let res = get_expls_fmla (Task.task_goal_fmla task) in
    concat_expls
      (if res <> [] && not root
       then res
Andrei Paskevich's avatar
Andrei Paskevich committed
73
       else collect_expls gid.Ident.id_attrs)
74
  in
75
76
77
  let info =
    match info with
      | Some i -> i
78
      | None -> ""
79
  in
80
81
  gid, info, task

82
(* {2 ident dictionaries for shapes} *)
83

84
(*
85
86
let dict_table = Hashtbl.create 17
let dict_count = ref 0
87
88
89
90
91
92
93
94
let reverse_ident_table = Hashtbl.create 17
let reverse_dict_count = ref 0

let reset_dict () =
  Hashtbl.clear dict_table;
  Hashtbl.clear reverse_ident_table;
  dict_count := 0;
  reverse_dict_count := 0
95
 *)
96
97

(* {3 direct table to read shapes from strings} *)
98

99
(*
100
101
102
103
104
105
106
107
108
109
let get_name s b i =
  try while !i < String.length s do
    match String.get s !i with
      | ')' -> incr i; raise Exit
      | c -> incr i; Buffer.add_char b c
    done;
    invalid_arg "Termcode.get_name: missing closing parenthesis"
  with Exit ->
    let id = Buffer.contents b in
    Hashtbl.add dict_table !dict_count id;
110
111
112
(*
    Format.eprintf "%d -> %s@." !dict_count id;
*)
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
    incr dict_count;
    id

let get_num s n i =
  try while !i < String.length s do
    match String.get s !i with
      | ')' -> incr i; raise Exit
      | '0'..'9' as c ->
        incr i; n := !n * 10 + (Char.code c - Char.code '0')
      | _ ->
        invalid_arg "Termcode.get_num: decimal digit expected"
    done;
    invalid_arg "Termcode.get_num: missing closing parenthesis"
  with Exit ->
    try Hashtbl.find dict_table !n
    with Not_found ->
129
130
      invalid_arg
        ("Termcode.get_num: invalid ident number " ^ string_of_int !n)
131
      *)
132

133
(*
134
135
136
137
138
139
140
141
142
143
144
145
146
147
let get_id s i =
  if !i >= String.length s then
    invalid_arg "Termcode.get_id: missing closing parenthesis";
  match String.get s !i with
    | '0'..'9' as c ->
      let n = ref (Char.code c - Char.code '0') in
      incr i;
      get_num s n i
    | ')' -> invalid_arg "Termcode.get_id: unexpected closing parenthesis"
    | c ->
      let b = Buffer.create 17 in
      Buffer.add_char b c;
      incr i;
      get_name s b i
148
*)
149

150
(*
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
let store_id s i =
  let b = Buffer.create 17 in
  try while !i < String.length s do
    match String.get s !i with
      | ')' -> incr i; raise Exit
      | c -> incr i; Buffer.add_char b c
    done;
    invalid_arg "Termcode.store_id: missing closing parenthesis"
  with Exit ->
    let id = Buffer.contents b in
    try
      let n = Hashtbl.find reverse_ident_table id in
      string_of_int n
    with
        Not_found ->
          Hashtbl.add reverse_ident_table id !reverse_dict_count;
          incr reverse_dict_count;
          id
169
*)
170
171

(* {2 Shapes} *)
172

173
type shape = string
174

175
176
let string_of_shape s = s
(*
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
  try
  let l = String.length s in
  let r = Buffer.create l in
  let i = ref 0 in
  while !i < l do
  match String.get s !i with
    | '(' ->
      Buffer.add_char r '(';
      incr i;
      Buffer.add_string r (store_id s i);
      Buffer.add_char r ')'
    | c -> Buffer.add_char r c; incr i
  done;
  Buffer.contents r
  with e ->
    Format.eprintf "Error while reading shape [%s]@." s;
    raise e
194
*)
195

196
197
let shape_of_string s = s
(*
198
  try
199
200
201
202
203
204
205
206
207
  let l = String.length s in
  let r = Buffer.create l in
  let i = ref 0 in
  while !i < l do
  match String.get s !i with
    | '(' -> incr i; Buffer.add_string r (get_id s i)
    | c -> Buffer.add_char r c; incr i
  done;
  Buffer.contents r
208
209
210
  with e ->
    Format.eprintf "Error while reading shape [%s]@." s;
    raise e
211
 *)
212
213
214
215
216
217
218
219

(* tests
let _ = reset_dict () ; shape_of_string "a(b)cde(0)"
let _ = reset_dict () ; shape_of_string "a(bc)d(e)f(1)g(0)h"
let _ = reset_dict () ; shape_of_string "(abc)(def)(1)(0)(1)"
let _ = reset_dict () ; shape_of_string "(abcde)(fghij)(1)(0)(1)"
*)

220
let equal_shape (x:string) y = x = y
221
(* unused
222
let print_shape fmt s = Format.pp_print_string fmt (string_of_shape s)
223
*)
224

225
let debug = Debug.register_info_flag "session_pairing"
Andrei Paskevich's avatar
Andrei Paskevich committed
226
227
  ~desc:"Print@ debugging@ messages@ about@ reconstruction@ of@ \
         session@ trees@ after@ modification@ of@ source@ files."
228

229
let current_shape_version = 5
230

231
type shape_version = SV1 | SV2 | SV3 | SV4
MARCHE Claude's avatar
MARCHE Claude committed
232

233
(* similarity code of terms, or of "shapes"
234

235
example:
236
237
238
239
240

  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
241
242
*)

243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
let tag_and = 'A'
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'
let tag_impl = 'I'
let tag_if = 'i'
let tag_let = 'L'
let tag_not = 'N'
let tag_or = 'O'
let tag_iff = 'q'
let tag_true = 't'
let tag_var = 'V'
let tag_wild = 'w'
let tag_as = 'z'

262
263
exception ShapeTooLong

264
265
266
267
let shape_buffer = Buffer.create 17

let push s =
  Buffer.add_string shape_buffer s;
268
  if Buffer.length shape_buffer >= 1024 then raise ShapeTooLong
269
270
271

let pushc c =
  Buffer.add_char shape_buffer c;
272
  if Buffer.length shape_buffer >= 1024 then raise ShapeTooLong
273
274
275
276
277
278
279
280
281
282
283
284
285
286

let ident h id =
  let x =
    try Ident.Mid.find id !h
    with Not_found ->
      let s = id.Ident.id_string in
      h := Ident.Mid.add id s !h; s
  in
  push x

let vs_rename_alpha c h vs =
  incr c;
  let s = string_of_int !c in
  h := Ident.Mid.add vs.vs_name s !h
287

288
let vl_rename_alpha c h vl = List.iter (vs_rename_alpha c h) vl
MARCHE Claude's avatar
MARCHE Claude committed
289

290
291
let rec pat_rename_alpha c h p = match p.pat_node with
  | Pvar v -> vs_rename_alpha c h v
292
  | Pas (p, v) -> vs_rename_alpha c h v; pat_rename_alpha c h p
293
  | Por (p, _) -> pat_rename_alpha c h p
294
295
  | _ -> Term.pat_fold (fun () -> pat_rename_alpha c h) () p

296
(*
297
298
299
let id_string_shape id = push id

let ident_shape id = id_string_shape id.Ident.id_string
300
*)
301

302
open Number
303

304
let integer_const_shape = function
305
  | IConstRaw i -> push (BigInt.to_string i)
306
307
308
309
  | IConstDec s -> push s
  | IConstHex s -> push "0x"; push s
  | IConstOct s -> push "0o"; push s
  | IConstBin s -> push "0b"; push s
MARCHE Claude's avatar
MARCHE Claude committed
310

311
312
313
314
315
let real_const_shape = function
  | RConstDec (i,f,None)   -> push i; push "."; push f
  | RConstDec (i,f,Some e) -> push i; push "."; push f; push "e"; push e
  | RConstHex (i,f,Some e) -> push "0x"; push i; push "."; push f; push "p"; push e
  | RConstHex (i,f,None)   -> push "0x"; push i; push "."; push f
316

317
318
let sign_shape is_negative =
  if is_negative then pushc '-'
MARCHE Claude's avatar
MARCHE Claude committed
319

320
321
let const_shape c =
  match c with
322
323
  | ConstInt c -> sign_shape c.ic_negative; integer_const_shape c.ic_abs
  | ConstReal c -> sign_shape c.rc_negative; real_const_shape c.rc_abs
324
325
326


let rec pat_shape c m p : 'a =
327
  match p.pat_node with
328
329
    | Pwild -> pushc tag_wild
    | Pvar _ -> pushc tag_var
330
    | Papp (f, l) ->
331
332
333
334
       pushc tag_app;
       ident m f.ls_name;
       List.iter (pat_shape c m) l
    | Pas (p, _) -> pat_shape c m p; pushc tag_as
335
    | Por (p, q) ->
336
       pat_shape c m q; pushc tag_or; pat_shape c m p
MARCHE Claude's avatar
MARCHE Claude committed
337

338
339
let rec t_shape ~version c m t =
  let fn = t_shape ~version c m in
MARCHE Claude's avatar
MARCHE Claude committed
340
  match t.t_node with
341
342
    | Tconst c -> pushc tag_const; const_shape c
    | Tvar v -> pushc tag_var; ident m v.vs_name
MARCHE Claude's avatar
MARCHE Claude committed
343
    | Tapp (s,l) ->
344
345
346
       pushc tag_app;
       ident m s.ls_name;
       List.iter fn l
347
348
    | Tif (f,t1,t2) ->
      begin match version with
349
      | SV1 | SV2 -> pushc tag_if; fn f; fn t1; fn t2
350
      | SV3 | SV4 -> pushc tag_if; fn t2; fn t1; fn f
351
      end
MARCHE Claude's avatar
MARCHE Claude committed
352
    | Tcase (t1,bl) ->
353
        let br_shape b =
MARCHE Claude's avatar
MARCHE Claude committed
354
          let p,t2 = t_open_branch b in
355
          match version with
356
          | SV1 | SV2 ->
357
358
359
            pat_shape c m p;
            pat_rename_alpha c m p;
            t_shape ~version c m t2
360
          | SV3 | SV4 ->
361
362
363
            pat_rename_alpha c m p;
            t_shape ~version c m t2;
            pat_shape c m p
MARCHE Claude's avatar
MARCHE Claude committed
364
        in
365
        begin match version with
366
        | SV1 | SV2 ->
367
368
369
                 pushc tag_case;
                 fn t1;
                 List.iter br_shape bl
370
        | SV3 | SV4 ->
371
372
373
           pushc tag_case;
           List.iter br_shape bl;
           fn t1
374
        end
MARCHE Claude's avatar
MARCHE Claude committed
375
    | Teps b ->
376
        pushc tag_eps;
MARCHE Claude's avatar
MARCHE Claude committed
377
        let u,f = t_open_bound b in
378
379
        vs_rename_alpha c m u;
        t_shape ~version c m f
MARCHE Claude's avatar
MARCHE Claude committed
380
    | Tquant (q,b) ->
381
        let vl,triggers,f1 = t_open_quant b in
382
        vl_rename_alpha c m vl;
383
384
        (* argument first, intentionally, to give more weight on A in
           forall x,A *)
385
386
387
388
389
390
391
392
393
        t_shape ~version c m f1;
        let hq = match q with Tforall -> tag_forall | Texists -> tag_exists in
        pushc hq;
        List.iter
          (fun trigger ->
             List.iter
               (fun t -> t_shape ~version c m t)
               trigger)
          triggers
394
    | Tbinop (o,f,g) ->
395
396
397
398
399
400
401
402
403
404
       (* g first, intentionally, to give more weight on B in A->B *)
       fn g;
       let tag = match o with
         | Tand -> tag_and
         | Tor -> tag_or
         | Timplies -> tag_impl
         | Tiff -> tag_iff
       in
       pushc tag;
       fn f
MARCHE Claude's avatar
MARCHE Claude committed
405
406
    | Tlet (t1,b) ->
        let u,t2 = t_open_bound b in
407
        vs_rename_alpha c m u;
MARCHE Claude's avatar
MARCHE Claude committed
408
409
        begin
          match version with
410
            | SV1 ->
411
               pushc tag_let; fn t1; t_shape ~version c m t2
412
            | SV2 | SV3 | SV4 ->
413
414
                     (* t2 first, intentionally *)
                     t_shape ~version c m t2; pushc tag_let; fn t1
MARCHE Claude's avatar
MARCHE Claude committed
415
        end
416
417
    | Tnot f ->
      begin match version with
418
      | SV1 | SV2 -> fn f; pushc tag_not
419
      | SV3 | SV4 -> pushc tag_not; fn f
420
      end
421
422
    | Ttrue -> pushc tag_true
    | Tfalse -> pushc tag_false
MARCHE Claude's avatar
MARCHE Claude committed
423

424
425
let t_shape_task ~version ~expl t =
  Buffer.clear shape_buffer;
426
  let f = Task.task_goal_fmla t in
427
428
  let c = ref (-1) in
  let m = ref Ident.Mid.empty in
429
430
  let () =
    try
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
      (* expl *)
      begin match version with
      | SV1 | SV2 -> ()
      | SV3 | SV4 -> push expl end;
      (* goal shape *)
      t_shape ~version c m f;
      (* introduced premises shape *)
      begin match version with
      | SV1 | SV2 | SV3 -> ()
      | SV4 ->
         let open Decl in
         let introduced id = Ident.Sattr.mem
                               Introduction.intro_attr
                               id.Ident.id_attrs in
         let do_td td = match td.Theory.td_node with
           | Theory.Decl d ->
              begin match d.d_node with
              | Dparam _ls -> ()
              | Dprop (_, pr, f) when introduced pr.pr_name ->
                 t_shape ~version c m f
              | _ -> ()
              end
           | _ -> () in
         let _, prev = Task.task_separate_goal t in
         Task.task_iter do_td prev
      end
    with ShapeTooLong -> ()
458
459
  in
  Buffer.contents shape_buffer
460

461
462
463
(*
let time = ref 0.0
 *)
464

465
let t_shape_task ?(version=current_shape_version) ~expl t =
466
  let version = match version with
467
    | 1 -> SV1 | 2 -> SV2 | 3 | 4 -> SV3 | 5 -> SV4
468
469
    | _ -> assert false
  in
470
471
472
473
474
475
476
477
478
479
(*
  let tim = Unix.gettimeofday () in
 *)
  let s = t_shape_task ~version ~expl t in
(*
  let tim = Unix.gettimeofday () -. tim in
  time := !time +. tim;
  Format.eprintf "[Shape times] %f/%f@." tim !time;
*)
  s
480

481
482
483
484
485
486
487
488
489
(* 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 = ""

490
491
492
493
let buffer_checksum b =
  let s = Buffer.contents b in
  Digest.to_hex (Digest.string s)

494
495
type checksum_version = CV1 | CV2

496
497
module Checksum = struct

498
499
500
  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)
501
  let raw_string (_,_,_,buf) s = Buffer.add_string buf s
502
503
  let string (_,_,_,buf as b) s =
    char b '"'; Buffer.add_string buf (String.escaped s); char b '"'
504
  let option e b = function None -> char b 'n' | Some x -> char b 's'; e b x
505
  let list e b l = char b '['; List.iter (e b) l; char b ']'
506

507
  let ident_v1, clear_ident_v1 =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
508
    let hident = Ident.Hid.create 17 in
509
    let c = ref 0 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
510
    (fun b id ->
511
      int b (try Ident.Hid.find hident id
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
512
513
        with Not_found -> incr c; Ident.Hid.add hident id !c; !c)),
    (fun () -> Ident.Hid.clear hident; c := 0)
514

515
516
517
518
519
520
521
522
523
524
525
  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

526
  let integer_const b = function
527
    | IConstRaw i -> raw_string b (BigInt.to_string i)
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
    | IConstDec s -> raw_string b s
    | IConstHex s -> raw_string b "0x"; raw_string b s
    | IConstOct s -> raw_string b "0o"; raw_string b s
    | IConstBin s -> raw_string b "0b"; raw_string b s

  let real_const b = function
    | RConstDec (i,f,None)   ->
       raw_string b i; raw_string b "."; raw_string b f
    | RConstDec (i,f,Some e) ->
       raw_string b i; raw_string b "."; raw_string b f; raw_string b "e"; raw_string b e
    | RConstHex (i,f,Some e) ->
       raw_string b "0x"; raw_string b i; raw_string b "."; raw_string b f;
       raw_string b "p"; raw_string b e
    | RConstHex (i,f,None)   ->
       raw_string b "0x"; raw_string b i; raw_string b "."; raw_string b f
Clément Fumex's avatar
Clément Fumex committed
543

544
545
546
  let sign b is_negative =
    if is_negative then raw_string b "-"

547
  let const b c =
548
    match c with
549
550
    | ConstInt c -> sign b c.ic_negative; integer_const b c.ic_abs
    | ConstReal c -> sign b c.rc_negative; real_const b c.rc_abs
551
552
553
554
555
556
557

  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

558
559
560
  let vsymbol (v,_,_,_ as b) vs = match v with
    | CV1 -> ty b vs.vs_ty
    | CV2 -> ident b vs.vs_name; ty b vs.vs_ty
561
562
563
564
565
566
567
568
569
570

  (* 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 *)
571
  let rec term b t = match t.t_node with
572
    | Tconst c -> const b c
573
574
575
    | 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
576
577
578
    | Tcase (t1, bl) ->
        let branch b br =
          let p, t2 = t_open_branch br in
579
          pat b p; term b t2
580
        in
581
        char b 'm'; term b t1; list branch b bl
582
583
    | Teps bf ->
        let vs, f = t_open_bound bf in
584
        char b 'e'; vsymbol b vs; term b f
585
586
587
588
    | 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;
589
590
        list (list term) b triggers;
        term b f1
591
592
593
594
595
596
597
    | Tbinop (o, f, g) ->
        let tag = match o with
          | Tand -> 'A'
          | Tor -> 'O'
          | Timplies -> 'I'
          | Tiff -> 'q'
        in
598
        char b tag; term b f; term b g
599
600
    | Tlet (t1, bt) ->
        let vs, t2 = t_open_bound bt in
601
602
603
        char b 'l'; vsymbol b vs; term b t1;
        term b t2
    | Tnot f -> char b 'n'; term b f
604
605
606
607
608
609
    | 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;
Clément Fumex's avatar
Clément Fumex committed
610
611
612
613
614
    match ts.Ty.ts_def with
    | Ty.NoDef   -> char b 'n'
    | Ty.Alias x -> char b 's'; ty b x
    | Ty.Range _ -> char b 'r' (* FIXME *)
    | Ty.Float _ -> char b 'f' (* FIXME *)
615
616
617
618
619
620
621

  let lsymbol b ls =
    ident b ls.ls_name;
    list ty b ls.ls_args;
    option ty b ls.ls_value;
    int b ls.ls_constr

Clément Fumex's avatar
Clément Fumex committed
622
  (* start: T G F D R L I P (C M) *)
623
624
625
626
627
628
629
630
631
632
633
634
635
  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
636
637
          list vsymbol b vl;
          term b t
638
639
640
641
        in
        char b 'L'; list logic_decl b ldl
    | Decl.Dind (s, idl) ->
        let clause b (pr, f) =
642
          ident b pr.Decl.pr_name; term b f in
643
644
645
646
647
648
649
650
651
652
653
        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"
        in
        string b tag;
        ident b n.Decl.pr_name;
654
        term b t
655
656
657
658
659
660
661
662
663
664
665
666

  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;
667
    char b (if m.Theory.meta_excl then 't' else 'f')
668
669
670
671
672
673
674
675
676

  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

677
678
679
680
681
682
683
684
685
686
687
688
689
  let tdecl b d = match d.Theory.td_node with
    | Theory.Decl d -> decl b d
    | Theory.Use th
    | Theory.Clone (th, _) ->
        char b 'C'; ident b th.Theory.th_name; list string b th.Theory.th_path
    | Theory.Meta (m, mal) -> char b 'M'; meta b m; list meta_arg b mal

(* not used anymore

  NOTE: if we come back to checksumming theories, use the separate recursive
        [tdecl] function for it. [Use] in a theory requires a recursive call
        (as below), [Use] in a task is just a witness declaration.

690
  let rec tdecl b d = match d.Theory.td_node with
691
    | Theory.Decl d -> decl b d
692
    | Theory.Use th ->
693
694
      char b 'U'; ident b th.Theory.th_name; list string b th.Theory.th_path;
      string b (theory_v2 th)
695
696
    | Theory.Clone (th, _) ->
        char b 'C'; ident b th.Theory.th_name; list string b th.Theory.th_path
697
698
    | Theory.Meta (m, mal) -> char b 'M'; meta b m; list meta_arg b mal

699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
  and theory_v2_aux t =
    let c = ref 0 in
    let m = ref Ident.Mid.empty in
    let b = Buffer.create 8192 in
    List.iter (tdecl (CV2,c,m,b)) t.Theory.th_decls;
    let dnew = Digest.string (Buffer.contents b) in
    Digest.to_hex dnew

  and theory_v2 =
    let table = Ident.Wid.create 17 in
    fun t ->
      try Ident.Wid.find table t.Theory.th_name
      with Not_found ->
        let v = theory_v2_aux t in
        Ident.Wid.set table t.Theory.th_name v;
        v

  let theory ~version t = match version with
    | CV1 -> assert false
    | CV2 -> theory_v2 t
719
 *)
720

721
  let task_v1 =
722
723
    let c = ref 0 in
    let m = ref Ident.Mid.empty in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
724
    let b = Buffer.create 8192 in
725
726
727
728
729
730
731
732
733
734
    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
735
    let b = Buffer.create 8192 in
736
737
738
739
740
741
742
743
    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
744
745
746
        | Theory.Decl { Decl.d_news = s } ->
            Ident.Sid.fold (fun id a ->
              Ident.Mid.add id (Ident.Mid.find id !m) a) s mold
747
748
749
750
751
752
753
        | _ -> !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
754

755

756
757
758
  let task ~version t = match version with
    | CV1 -> task_v1 t
    | CV2 -> task_v2 t
759

760
761
end

762
763
764
765
(*
let time = ref 0.0
 *)

766
767
768
let task_checksum ?(version=current_shape_version) t =
  let version = match version with
    | 1 | 2 | 3 -> CV1
769
    | 4 | 5 -> CV2
770
771
    | _ -> assert false
  in
772
773
774
775
776
777
778
779
780
781
(*
  let tim = Unix.gettimeofday () in
*)
  let s = Checksum.task ~version t in
(*
  let tim = Unix.gettimeofday () -. tim in
  time := !time +. tim;
  Format.eprintf "[Checksum times] %f/%f@." tim !time;
*)
  s
782

783
(* not used anymore
784
785
786
787
788
789
790
let theory_checksum ?(version=current_shape_version) t =
  let version = match version with
    | 1 | 2 | 3 -> CV1
    | 4 -> CV2
    | _ -> assert false
  in
  Checksum.theory ~version t
791
 *)
792

793
(*************************************************************)
794
(* Pairing of new and old subgoals                           *)
795
796
797
798
(*************************************************************)

(* we have an ordered list of new subgoals

799
     newgoals = [g1; g2; g3; ...]
800
801
802

   and a list of old subgoals

803
     oldgoals = [h1 ; h2 ; ... ]
804

805
   we build a list
806

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

809
810
811
812
   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)
813
814
*)

815
module type S = sig
816
817
818
819
  type 'a t
  val checksum : 'a t -> checksum option
  val shape    : 'a t -> string
  val name     : 'a t -> Ident.ident
820
end
821

822
module Pairing(Old: S)(New: S) = struct
823

824
825
826
827
  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
828
829
830

  open Ident

831
832
833
834
835
836
  type goal_index = Old of int | New of int

  type ('a,'b) goal_table = {
    table_old : 'a Old.t array;
    table_new : 'b New.t array;
  }
837

838
  (* doubly linked lists; left and right bounds point to themselves *)
839
840
841
842

  type node = {
    mutable  prev: node;
            shape: string;
843
              elt: goal_index;
844
845
846
847
    mutable valid: bool;
    mutable  next: node;
  }

848
849
850
851
852
853
854
  let mk_node table g =
    let s = match g with
      | Old g -> Old.shape table.table_old.(g)
      | New g -> New.shape table.table_new.(g)
    in
    let rec n = { prev = n; shape = s; elt = g; next = n; valid = true }
    in n
855
856
857
858
859
860
861

  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)

862
863
864
865
866
867
868
  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

869
870
871
872
  (* priority queues for pairs of nodes *)

  let dprintf = Debug.dprintf debug

873
  let associate oldgoals newgoals =
874
875
876
877
878
    let table = {
      table_old = Array.of_list oldgoals;
      table_new = Array.of_list newgoals;
    }
    in
879
880
881
882
883
    (* 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 =
884
885
886
887
        Hid.add new_goal_index (New.name newg) i; (newg, None)
      in
      Array.mapi make table.table_new
    in
888
889
890
891
892
    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
893
    let old_goals_without_checksum =
894
895
896
897
898
899
900
      let acc =ref [] in
      for oldg = 0 to Array.length table.table_old - 1 do
        match Old.checksum table.table_old.(oldg) with
        | None -> acc := mk_node table (Old oldg) :: !acc
        | Some s -> Hashtbl.add old_checksums s oldg
      done;
      !acc
901
    in
902
903
904
905
906
907
908
909
910
911
912
    let newgoals =
      let acc = ref old_goals_without_checksum in
      for newi = 0 to Array.length table.table_new - 1 do
        try
          let newg = table.table_new.(newi) in
          match New.checksum newg with
          | None -> raise Not_found
          | Some c ->
             let oldi = Hashtbl.find old_checksums c in
             let oldg = table.table_old.(oldi) in
             Hashtbl.remove old_checksums c;
913
914
             let obs = Old.shape oldg <> New.shape newg in
             result.(new_goal_index newg) <- (newg, Some (oldg, obs))
915
916
917
918
        with Not_found ->
          acc := mk_node table (New newi) :: !acc
      done;
      !acc
919
    in
920
    let add _ oldg acc = mk_node table (Old oldg) :: acc in
921
    let allgoals = Hashtbl.fold add old_checksums newgoals in
922
923
    Hashtbl.clear old_checksums;
    (* phase 2: pair goals according to shapes *)
924
925
926
927
    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
Mário Pereira's avatar
Mário Pereira committed
928
929
930
931
932
933
934
      let module E = struct
        let dummy = let n = List.hd allgoals (* safe *) in 0, (n, n)
        type t = int * (node * node)
        let compare (v1, _) (v2, _) = Pervasives.compare v2 v1
      end in
      let module PQ = Pqueue.Make(E) in
      let pq = PQ.create () in
935
      let add x y = match x.elt, y.elt with
Mário Pereira's avatar
Mário Pereira committed
936
937
        | Old _, New _ | New _, Old _ ->
            PQ.insert (lcp x.shape y.shape, (x, y)) pq
938
939
940
941
        | 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
Mário Pereira's avatar
Mário Pereira committed
942
        let _, (x, y) = PQ.extract_min_exn pq in
943
944
945
946
        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@.";
947
948
949
          let newg = table.table_new.(n) in
          let oldg = table.table_old.(o) in
          result.(new_goal_index newg) <- newg, Some (oldg, true);
950
          if x.prev != x && y.next != y then add x.prev y.next;
951
952
          remove x;
          remove y
953
954
955
        end
      done
    end;
956
957
958
959
960
    let detached =
      List.fold_left
        (fun acc x ->
         if x.valid then
           match x.elt with
961
           | Old g -> table.table_old.(g) :: acc
962
963
964
965
966
967
           | New _ -> acc
         else acc)
        [] allgoals
    in
    Debug.dprintf debug "[assoc] %d detached goals@." (List.length detached);
    Array.to_list result, detached
968

969
  let simple_associate oldgoals newgoals =
970
971
    let rec aux acc o n =
      match o,n with
972
        | old, [] -> acc,old
973
        | [], n :: rem_n -> aux ((n,None)::acc) [] rem_n
974
        | o :: rem_o, n :: rem_n -> aux ((n,Some(o,true))::acc) rem_o rem_n
975
976
977
    in
    aux [] oldgoals newgoals

978
  let associate ~use_shapes =
979
980
981
    if use_shapes then
      associate
    else
982
      simple_associate
983

984
end