termcode.ml 25 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   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
let collect_expls lab =
  Ident.Slab.fold
    (fun lab acc ->
       let lab = lab.Ident.lab_string in
23
       try
24
         let s = Strings.remove_prefix "expl:" lab in s :: acc
25
       with Not_found -> acc)
26 27 28 29 30 31 32 33
    lab
    []

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

34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54

let search_labels callback =
  let rec aux acc f =
    if f.t_ty <> None then acc
    else if Ident.Slab.mem Split_goal.stop_split f.Term.t_label then acc
    else
      let res = callback f.Term.t_label in
      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 []

let get_expls_fmla =
  let search = search_labels collect_expls in
  fun f -> try search f with Exit -> []
55 56 57 58

let goal_expl_task ~root task =
  let gid = (Task.task_goal task).Decl.pr_name in
  let info =
59 60 61 62 63
    let res = get_expls_fmla (Task.task_goal_fmla task) in
    concat_expls
      (if res <> [] && not root
       then res
       else collect_expls gid.Ident.id_label)
64 65 66
  in
  gid, info, task

67
(* {2 ident dictionaries for shapes} *)
68 69 70

let dict_table = Hashtbl.create 17
let dict_count = ref 0
71 72 73 74 75 76 77 78 79 80
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

(* {3 direct table to read shapes from strings} *)
81 82 83 84 85 86 87 88 89 90 91 92


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;
93 94 95
(*
    Format.eprintf "%d -> %s@." !dict_count id;
*)
96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111
    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 ->
112 113
      invalid_arg
        ("Termcode.get_num: invalid ident number " ^ string_of_int !n)
114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129

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

130

131
(*
132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149
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
150
*)
151 152

(* {2 Shapes} *)
153

154
type shape = string
155

156 157
let string_of_shape s = s
(*
158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174
  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
175
*)
176

177
let shape_of_string s =
178
  try
179 180 181 182 183 184 185 186 187
  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
188 189 190
  with e ->
    Format.eprintf "Error while reading shape [%s]@." s;
    raise e
191 192 193 194 195 196 197 198

(* 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)"
*)

199
let equal_shape (x:string) y = x = y
200
(* unused
201
let print_shape fmt s = Format.pp_print_string fmt (string_of_shape s)
202
*)
203

204
let debug = Debug.register_info_flag "session_pairing"
Andrei Paskevich's avatar
Andrei Paskevich committed
205 206
  ~desc:"Print@ debugging@ messages@ about@ reconstruction@ of@ \
         session@ trees@ after@ modification@ of@ source@ files."
207

208 209 210
let current_shape_version = 4

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

212
(* similarity code of terms, or of "shapes"
213

214
example:
215 216 217 218 219

  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
220 221 222
*)

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

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

226 227 228 229 230 231
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
232 233

let tag_and = "A"
234 235 236 237 238 239 240
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
241
let tag_impl = "I"
242
let tag_if = "i"
MARCHE Claude's avatar
MARCHE Claude committed
243 244 245
let tag_let = "L"
let tag_not = "N"
let tag_or = "O"
246 247
let tag_iff = "q"
let tag_true = "t"
MARCHE Claude's avatar
MARCHE Claude committed
248
let tag_var = "V"
249 250
let tag_wild = "w"
let tag_as = "z"
MARCHE Claude's avatar
MARCHE Claude committed
251

252

253
let id_string_shape ~push id acc =
254 255
  push id acc
(*
256 257 258 259 260 261 262 263 264 265 266 267
  let l = String.length id in
  if l <= 4 then push id acc else
  (* sanity check *)
  if (match String.get id 0 with
      | '0'..'9' -> true
      | _ ->
        try
          let (_:int) = String.index id ')' in
          true
        with Not_found -> false)
    then push id acc
    else push ")" (push id (push "(" acc))
268
*)
269 270 271

let ident_shape ~push id acc =
  id_string_shape ~push id.Ident.id_string acc
272

273
let const_shape ~push acc c =
274 275
  Format.fprintf Format.str_formatter "%a" Pretty.print_const c;
  push (Format.flush_str_formatter ()) acc
MARCHE Claude's avatar
MARCHE Claude committed
276

277 278 279 280 281 282
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)
283
          (ident_shape ~push f.ls_name (push tag_app acc))
284 285 286 287
          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
288

MARCHE Claude's avatar
MARCHE Claude committed
289 290
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
291 292 293 294
  match t.t_node with
    | Tconst c -> const_shape ~push (push tag_const acc) c
    | Tvar v ->
        let x =
295 296
          try string_of_int (Mvs.find v m)
          with Not_found -> v.vs_name.Ident.id_string
MARCHE Claude's avatar
MARCHE Claude committed
297 298 299 300
        in
        push x (push tag_var acc)
    | Tapp (s,l) ->
        List.fold_left fn
301
          (ident_shape ~push s.ls_name (push tag_app acc))
MARCHE Claude's avatar
MARCHE Claude committed
302
          l
303 304
    | Tif (f,t1,t2) ->
      begin match version with
305 306
      | SV1 | SV2 -> fn (fn (fn (push tag_if acc) f) t1) t2
      | SV3 -> fn (fn (fn (push tag_if acc) t2) t1) f
307
      end
MARCHE Claude's avatar
MARCHE Claude committed
308 309 310
    | Tcase (t1,bl) ->
        let br_shape acc b =
          let p,t2 = t_open_branch b in
311
          match version with
312
          | SV1 | SV2 ->
313 314 315
            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
316
          | SV3 ->
317 318 319
            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
320
        in
321
        begin match version with
322
        | SV1 | SV2 ->
323
          List.fold_left br_shape (fn (push tag_case acc) t1) bl
324
        | SV3 ->
325 326 327 328
          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
329 330 331
    | 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
332
        t_shape ~version ~push c m (push tag_eps acc) f
MARCHE Claude's avatar
MARCHE Claude committed
333
    | Tquant (q,b) ->
334
        let vl,triggers,f1 = t_open_quant b in
MARCHE Claude's avatar
MARCHE Claude committed
335 336
        let m = vl_rename_alpha c m vl in
        let hq = match q with Tforall -> tag_forall | Texists -> tag_exists in
337 338
        (* argument first, intentionally, to give more weight on A in
           forall x,A *)
MARCHE Claude's avatar
MARCHE Claude committed
339
        let acc = push hq (t_shape ~version ~push c m acc f1) in
340 341 342 343
        List.fold_right
          (fun trigger acc ->
             List.fold_right
               (fun t acc ->
MARCHE Claude's avatar
MARCHE Claude committed
344
                  t_shape ~version ~push c m acc t)
345 346
               trigger acc)
          triggers acc
347 348 349 350 351 352 353 354 355
    | 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
356 357 358 359 360
    | Tlet (t1,b) ->
        let u,t2 = t_open_bound b in
        let m = vs_rename_alpha c m u in
        begin
          match version with
361
            | SV1 ->
MARCHE Claude's avatar
MARCHE Claude committed
362
              t_shape ~version ~push c m (fn (push tag_let acc) t1) t2
363
            | SV2 | SV3 ->
MARCHE Claude's avatar
MARCHE Claude committed
364 365 366
              (* t2 first, intentionally *)
              fn (push tag_let (t_shape ~version ~push c m acc t2)) t1
        end
367 368
    | Tnot f ->
      begin match version with
369 370
      | SV1 | SV2 -> push tag_not (fn acc f)
      | SV3 -> fn (push tag_not acc) f
371
      end
372 373
    | Ttrue -> push tag_true acc
    | Tfalse -> push tag_false acc
MARCHE Claude's avatar
MARCHE Claude committed
374

MARCHE Claude's avatar
MARCHE Claude committed
375
(* dead code
MARCHE Claude's avatar
MARCHE Claude committed
376
let t_shape_buf ?(version=current_shape_version) t =
MARCHE Claude's avatar
MARCHE Claude committed
377 378
  let b = Buffer.create 17 in
  let push t () = Buffer.add_string b t in
MARCHE Claude's avatar
MARCHE Claude committed
379
  let () = t_shape ~version ~push (ref (-1)) Mvs.empty () t in
MARCHE Claude's avatar
MARCHE Claude committed
380
  Buffer.contents b
MARCHE Claude's avatar
MARCHE Claude committed
381
*)
MARCHE Claude's avatar
MARCHE Claude committed
382

383
let t_shape_task ~version t =
384 385
  let b = Buffer.create 17 in
  let push t () = Buffer.add_string b t in
386
  begin match version with
387 388
  | SV1 | SV2 -> ()
  | SV3 ->
389
    let _, expl, _ = goal_expl_task ~root:false t in
390 391
    match expl with
      | None -> ()
392
      | Some expl -> id_string_shape ~push expl ()
393
  end;
394 395 396
  let f = Task.task_goal_fmla t in
  let () = t_shape ~version ~push (ref (-1)) Mvs.empty () f in
  Buffer.contents b
397

398 399 400 401 402 403 404
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

405 406 407 408 409 410 411 412 413
(* 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 = ""

414 415 416 417
let buffer_checksum b =
  let s = Buffer.contents b in
  Digest.to_hex (Digest.string s)

418 419
type checksum_version = CV1 | CV2

420 421
module Checksum = struct

422 423 424 425 426
  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 '"'
427
  let option e b = function None -> char b 'n' | Some x -> char b 's'; e b x
428
  let list e b l = char b '['; List.iter (e b) l; char b ']'
429

430
  let ident_v1, clear_ident_v1 =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
431
    let hident = Ident.Hid.create 17 in
432
    let c = ref 0 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
433
    (fun b id ->
434
      int b (try Ident.Hid.find hident id
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
435 436
        with Not_found -> incr c; Ident.Hid.add hident id !c; !c)),
    (fun () -> Ident.Hid.clear hident; c := 0)
437

438 439 440 441 442 443 444 445 446 447 448
  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

449 450 451
  let const b c =
      Format.fprintf Format.str_formatter "%a" Pretty.print_const c;
      let s = Format.flush_str_formatter () in
452
      string b s
453 454 455 456 457 458 459

  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

460 461 462
  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
463 464 465 466 467 468 469 470 471 472

  (* 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 *)
473
  let rec term b t = match t.t_node with
474
    | Tconst c -> const b c
475 476 477
    | 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
478 479 480
    | Tcase (t1, bl) ->
        let branch b br =
          let p, t2 = t_open_branch br in
481
          pat b p; term b t2
482
        in
483
        char b 'm'; term b t1; list branch b bl
484 485
    | Teps bf ->
        let vs, f = t_open_bound bf in
486
        char b 'e'; vsymbol b vs; term b f
487 488 489 490
    | 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;
491 492
        list (list term) b triggers;
        term b f1
493 494 495 496 497 498 499
    | Tbinop (o, f, g) ->
        let tag = match o with
          | Tand -> 'A'
          | Tor -> 'O'
          | Timplies -> 'I'
          | Tiff -> 'q'
        in
500
        char b tag; term b f; term b g
501 502
    | Tlet (t1, bt) ->
        let vs, t2 = t_open_bound bt in
503 504 505
        char b 'l'; vsymbol b vs; term b t1;
        term b t2
    | Tnot f -> char b 'n'; term b f
506 507 508 509 510 511 512 513 514 515 516 517 518 519 520
    | 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

521
  (* start: T D R L I P (C M) *)
522 523 524 525 526 527 528 529 530 531 532 533 534
  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
535 536
          list vsymbol b vl;
          term b t
537 538 539 540
        in
        char b 'L'; list logic_decl b ldl
    | Decl.Dind (s, idl) ->
        let clause b (pr, f) =
541
          ident b pr.Decl.pr_name; term b f in
542 543 544 545 546 547 548 549 550 551 552 553
        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;
554
        term b t
555 556 557 558 559 560 561 562 563 564 565 566

  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;
567
    char b (if m.Theory.meta_excl then 't' else 'f')
568 569 570 571 572 573 574 575 576

  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

577
  let rec tdecl b d = match d.Theory.td_node with
578
    | Theory.Decl d -> decl b d
579
    | Theory.Use th ->
580 581
      char b 'U'; ident b th.Theory.th_name; list string b th.Theory.th_path;
      string b (theory_v2 th)
582 583
    | Theory.Clone (th, _) ->
        char b 'C'; ident b th.Theory.th_name; list string b th.Theory.th_path
584 585
    | Theory.Meta (m, mal) -> char b 'M'; meta b m; list meta_arg b mal

586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602
  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

603
(* not used anymore
604 605 606
  let theory ~version t = match version with
    | CV1 -> assert false
    | CV2 -> theory_v2 t
607
 *)
608

609
  let task_v1 =
610 611
    let c = ref 0 in
    let m = ref Ident.Mid.empty in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
612
    let b = Buffer.create 8192 in
613 614 615 616 617 618 619 620 621 622
    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
623
    let b = Buffer.create 8192 in
624 625 626 627 628 629 630 631
    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
632 633 634
        | Theory.Decl { Decl.d_news = s } ->
            Ident.Sid.fold (fun id a ->
              Ident.Mid.add id (Ident.Mid.find id !m) a) s mold
635 636 637 638 639 640 641
        | _ -> !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
642

643

644 645 646
  let task ~version t = match version with
    | CV1 -> task_v1 t
    | CV2 -> task_v2 t
647

648 649
end

650 651 652 653 654 655 656
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
657

658
(* not used anymore
659 660 661 662 663 664 665
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
666
 *)
667

668
(*************************************************************)
669
(* Pairing of new and old subgoals                           *)
670 671 672 673
(*************************************************************)

(* we have an ordered list of new subgoals

674
     newgoals = [g1; g2; g3; ...]
675 676 677

   and a list of old subgoals

678
     oldgoals = [h1 ; h2 ; ... ]
679

680
   we build a list
681

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

684 685 686 687
   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)
688 689
*)

690
module type S = sig
691 692 693 694
  type 'a t
  val checksum : 'a t -> checksum option
  val shape    : 'a t -> string
  val name     : 'a t -> Ident.ident
695
end
696

697
module Pairing(Old: S)(New: S) = struct
698

699 700 701 702
  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
703 704 705

  open Ident

706 707 708 709 710 711
  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;
  }
712

713
  (* doubly linked lists; left and right bounds point to themselves *)
714 715 716 717

  type node = {
    mutable  prev: node;
            shape: string;
718
              elt: goal_index;
719 720 721 722
    mutable valid: bool;
    mutable  next: node;
  }

723 724 725 726 727 728 729
  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
730 731 732 733 734 735 736

  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)

737 738 739 740 741 742 743
  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

744 745 746 747 748 749 750 751 752 753
  (* 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

754
  let associate oldgoals newgoals =
755 756 757 758 759
    let table = {
      table_old = Array.of_list oldgoals;
      table_new = Array.of_list newgoals;
    }
    in
760 761 762 763 764
    (* 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 =
765 766 767 768
        Hid.add new_goal_index (New.name newg) i; (newg, None)
      in
      Array.mapi make table.table_new
    in
769 770 771 772 773
    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
774
    let old_goals_without_checksum =
775 776 777 778 779 780 781
      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
782
    in
783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798
    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;
             result.(new_goal_index newg) <- (newg, Some (oldg, false))
        with Not_found ->
          acc := mk_node table (New newi) :: !acc
      done;
      !acc
799
    in
800
    let add _ oldg acc = mk_node table (Old oldg) :: acc in
801
    let allgoals = Hashtbl.fold add old_checksums newgoals in
802 803
    Hashtbl.clear old_checksums;
    (* phase 2: pair goals according to shapes *)
804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820
    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@.";
821 822 823
          let newg = table.table_new.(n) in
          let oldg = table.table_old.(o) in
          result.(new_goal_index newg) <- newg, Some (oldg, true);
824
          if x.prev != x && y.next != y then add x.prev y.next;
825 826
          remove x;
          remove y
827 828 829
        end
      done
    end;
830 831 832 833 834
    let detached =
      List.fold_left
        (fun acc x ->
         if x.valid then
           match x.elt with
835
           | Old g -> table.table_old.(g) :: acc
836 837 838 839 840 841
           | New _ -> acc
         else acc)
        [] allgoals
    in
    Debug.dprintf debug "[assoc] %d detached goals@." (List.length detached);
    Array.to_list result, detached
842

843
  let simple_associate oldgoals newgoals =
844 845
    let rec aux acc o n =
      match o,n with
846
        | old, [] -> acc,old
847
        | [], n :: rem_n -> aux ((n,None)::acc) [] rem_n
848
        | o :: rem_o, n :: rem_n -> aux ((n,Some(o,true))::acc) rem_o rem_n
849 850 851
    in
    aux [] oldgoals newgoals

852
  let associate ~use_shapes =
853 854 855
    if use_shapes then
      associate
    else
856
      simple_associate
857

858
end