termcode.ml 14.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
(* Shapes *)
15

16
type shape = string
17
18
19
20
let print_shape = Format.pp_print_string
let string_of_shape x = x
let shape_of_string x = x

21
let debug = Debug.register_info_flag "session_pairing"
Andrei Paskevich's avatar
Andrei Paskevich committed
22
23
  ~desc:"Print@ debugging@ messages@ about@ reconstruction@ of@ \
         session@ trees@ after@ modification@ of@ source@ files."
24

MARCHE Claude's avatar
MARCHE Claude committed
25
26
let current_shape_version = 2

27
(* similarity code of terms, or of "shapes"
28

29
example:
30
31
32
33
34

  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
35
36
37
*)

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

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

41
42
43
44
45
46
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
47
48

let tag_and = "A"
49
50
51
52
53
54
55
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
56
let tag_impl = "I"
57
let tag_if = "i"
MARCHE Claude's avatar
MARCHE Claude committed
58
59
60
let tag_let = "L"
let tag_not = "N"
let tag_or = "O"
61
62
let tag_iff = "q"
let tag_true = "t"
MARCHE Claude's avatar
MARCHE Claude committed
63
let tag_var = "V"
64
65
let tag_wild = "w"
let tag_as = "z"
MARCHE Claude's avatar
MARCHE Claude committed
66

67
68
let ident_shape ~push id acc = push id.Ident.id_string acc

69
70
71
72
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
73

74
75
76
77
78
79
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)
80
          (ident_shape ~push f.ls_name (push tag_app acc))
81
82
83
84
          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
85

MARCHE Claude's avatar
MARCHE Claude committed
86
87
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
88
89
90
91
  match t.t_node with
    | Tconst c -> const_shape ~push (push tag_const acc) c
    | Tvar v ->
        let x =
92
93
          try string_of_int (Mvs.find v m)
          with Not_found -> v.vs_name.Ident.id_string
MARCHE Claude's avatar
MARCHE Claude committed
94
95
96
97
        in
        push x (push tag_var acc)
    | Tapp (s,l) ->
        List.fold_left fn
98
          (ident_shape ~push s.ls_name (push tag_app acc))
MARCHE Claude's avatar
MARCHE Claude committed
99
100
101
102
103
          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
104
105
          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
106
          t_shape ~version ~push c m acc t2
MARCHE Claude's avatar
MARCHE Claude committed
107
108
109
110
111
        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
112
        t_shape ~version ~push c m (push tag_eps acc) f
MARCHE Claude's avatar
MARCHE Claude committed
113
    | Tquant (q,b) ->
114
        let vl,triggers,f1 = t_open_quant b in
MARCHE Claude's avatar
MARCHE Claude committed
115
116
        let m = vl_rename_alpha c m vl in
        let hq = match q with Tforall -> tag_forall | Texists -> tag_exists in
117
118
        (* argument first, intentionally, to give more weight on A in
           forall x,A *)
MARCHE Claude's avatar
MARCHE Claude committed
119
        let acc = push hq (t_shape ~version ~push c m acc f1) in
120
121
122
123
        List.fold_right
          (fun trigger acc ->
             List.fold_right
               (fun t acc ->
MARCHE Claude's avatar
MARCHE Claude committed
124
                  t_shape ~version ~push c m acc t)
125
126
               trigger acc)
          triggers acc
127
128
129
130
131
132
133
134
135
    | 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
136
137
138
139
140
141
142
143
144
145
146
147
    | 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
148
149
150
    | 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
151

MARCHE Claude's avatar
MARCHE Claude committed
152
let t_shape_buf ?(version=current_shape_version) t =
MARCHE Claude's avatar
MARCHE Claude committed
153
154
  let b = Buffer.create 17 in
  let push t () = Buffer.add_string b t in
MARCHE Claude's avatar
MARCHE Claude committed
155
  let () = t_shape ~version ~push (ref (-1)) Mvs.empty () t in
MARCHE Claude's avatar
MARCHE Claude committed
156
157
  Buffer.contents b

158

159
160
161
162
163
164
165
166
167
(* 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 = ""

168
169
170
module Checksum = struct

  let char = Buffer.add_char
171
  let int b i = char b 'i'; Buffer.add_string b (string_of_int i)
172
173
174
  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
175
  let list e b l = char b '['; List.iter (e b) l; char b ']'
176

177
178
179
180
181
182
183
184
  (* let ident_printer = Ident.create_ident_printer [] *)
  (* let ident b id = string b (Ident.id_unique ident_printer id) *)
  let hident = Ident.Hid.create 17
  let ident =
    let c = ref 0 in
    fun b id ->
      int b (try Ident.Hid.find hident id
        with Not_found -> incr c; Ident.Hid.add hident id !c; !c)
185
186
187
188

  let const b c =
    let buf = Buffer.create 17 in
    Format.bprintf buf "%a" Pretty.print_const c;
189
    string b (Buffer.contents buf)
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208

  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 *)
209
  let rec term b t = match t.t_node with
210
    | Tconst c -> const b c
211
212
213
    | 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
214
215
216
    | Tcase (t1, bl) ->
        let branch b br =
          let p, t2 = t_open_branch br in
217
          pat b p; term b t2
218
        in
219
        char b 'm'; term b t1; list branch b bl
220
221
    | Teps bf ->
        let vs, f = t_open_bound bf in
222
        char b 'e'; vsymbol b vs; term b f
223
224
225
226
    | 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;
227
228
        list (list term) b triggers;
        term b f1
229
230
231
232
233
234
235
    | Tbinop (o, f, g) ->
        let tag = match o with
          | Tand -> 'A'
          | Tor -> 'O'
          | Timplies -> 'I'
          | Tiff -> 'q'
        in
236
        char b tag; term b f; term b g
237
238
    | Tlet (t1, bt) ->
        let vs, t2 = t_open_bound bt in
239
240
241
        char b 'l'; vsymbol b vs; term b t1;
        term b t2
    | Tnot f -> char b 'n'; term b f
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
    | 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

257
  (* start: T D R L I P (C M) *)
258
259
260
261
262
263
264
265
266
267
268
269
270
  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
271
272
          list vsymbol b vl;
          term b t
273
274
275
276
        in
        char b 'L'; list logic_decl b ldl
    | Decl.Dind (s, idl) ->
        let clause b (pr, f) =
277
          ident b pr.Decl.pr_name; term b f in
278
279
280
281
282
283
284
285
286
287
288
289
        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;
290
        term b t
291
292
293
294
295
296
297
298
299
300
301
302

  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;
303
    char b (if m.Theory.meta_excl then 't' else 'f')
304
305
306
307
308
309
310
311
312
313
314

  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
315
316
317
    | Theory.Use _ -> assert false
    | Theory.Clone (th, _) ->
        char b 'C'; ident b th.Theory.th_name; list string b th.Theory.th_path
318
319
320
    | Theory.Meta (m, mal) -> char b 'M'; meta b m; list meta_arg b mal

  let task t =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
321
    let b = Buffer.create 8192 in
322
    (* Ident.forget_all ident_printer; *)
323
    Task.task_iter (tdecl b) t;
324
    Ident.Hid.clear hident;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
325
326
    let s = Buffer.contents b in
    Digest.to_hex (Digest.string s)
327
328
329

end

330
let task_checksum ?(version=0) t = ignore version; Checksum.task t
MARCHE Claude's avatar
MARCHE Claude committed
331

332
333

(*************************************************************)
334
(* Pairing of new and old subgoals                           *)
335
336
337
338
(*************************************************************)

(* we have an ordered list of new subgoals

339
     newgoals = [g1; g2; g3; ...]
340
341
342

   and a list of old subgoals

343
     oldgoals = [h1 ; h2 ; ... ]
344

345
   we build a list
346

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

349
350
351
352
   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)
353
354
*)

355
356
357
358
359
module type S = sig
  type t
  val checksum : t -> string
  val shape    : t -> string
  val name     : t -> Ident.ident
360
end
361

362
module Pairing(Old: S)(New: S) = struct
363

364
365
366
367
  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
368
369
370

  open Ident

371
372
  type any_goal = Old of Old.t | New of New.t

373
  (* doubly linked lists; left and right bounds point to themselves *)
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392

  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)

393
394
395
396
397
398
399
  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

400
401
402
403
404
405
406
407
408
409
  (* 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

410
411
412
413
414
415
  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 =
416
        Hid.add new_goal_index (New.name newg) i; (newg, None) in
417
418
419
420
421
422
423
424
425
426
427
428
429
      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;
430
        result.(new_goal_index newg) <- (newg, Some (oldg, false));
431
432
        acc
      with Not_found ->
433
        mk_node (New newg) :: acc
434
435
    in
    let newgoals = List.fold_left collect [] newgoals in
436
437
    let add _ oldg acc = mk_node (Old oldg) :: acc in
    let allgoals = Hashtbl.fold add old_checksums newgoals in
438
439
    Hashtbl.clear old_checksums;
    (* phase 2: pair goals according to shapes *)
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
    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@.";
457
          result.(new_goal_index n) <- n, Some (o, true);
458
          if x.prev != x && y.next != y then add x.prev y.next;
459
460
          remove x;
          remove y
461
462
463
        end
      done
    end;
464
465
466
    Array.to_list result

end