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

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

15 16 17 18
(*******************************)
(*          explanations       *)
(*******************************)

19 20 21 22 23 24
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")
25

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
46
let search_attrs callback =
47 48
  let rec aux acc f =
    if f.t_ty <> None then acc
Andrei Paskevich's avatar
Andrei Paskevich committed
49
    else if Ident.Sattr.mem Term.stop_split f.Term.t_attrs then acc
50
    else
Andrei Paskevich's avatar
Andrei Paskevich committed
51
      let res = callback f.Term.t_attrs in
52 53 54 55 56 57 58 59 60 61
      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 []
62

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

let goal_expl_task ~root task =
  let gid = (Task.task_goal task).Decl.pr_name in
  let info =
70 71 72 73
    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
74
       else collect_expls gid.Ident.id_attrs)
75
  in
76 77 78
  let info =
    match info with
      | Some i -> i
79
      | None -> ""
80
  in
81 82
  gid, info, task

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

85
(*
86 87
let dict_table = Hashtbl.create 17
let dict_count = ref 0
88 89 90 91 92 93 94 95
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
96
 *)
97 98

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

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

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

151
(*
152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169
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
170
*)
171

172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210
module Common = struct

let sign fmt n =
  if n then Format.pp_print_char fmt '-'

let const_v1 fmt c =
  match c with
  | ConstInt { il_kind=k; il_int=i } ->
      sign fmt (BigInt.lt i BigInt.zero);
      let i = BigInt.abs i in
      begin match k with
      | ILitUnk | ILitDec -> Format.pp_print_string fmt (BigInt.to_string i)
      | ILitHex -> Format.fprintf fmt "0x%a" (Number.print_in_base 16 None) i
      | ILitOct -> Format.fprintf fmt "0o%a" (Number.print_in_base 8 None) i
      | ILitBin -> Format.fprintf fmt "0b%a" (Number.print_in_base 2 None) i
      end
  | ConstReal { rl_kind=k; rl_real={ rv_sig=i; rv_pow2=p2; rv_pow5=p5 } } ->
      (* not the actual encoding *)
      sign fmt (BigInt.lt i BigInt.zero);
      let i = BigInt.abs i in
      begin match k with
      | RLitUnk | RLitDec _ ->
          Format.fprintf fmt "%s.0e%sp%s"
            (BigInt.to_string i) (BigInt.to_string p5) (BigInt.to_string p2)
      | RLitHex _ ->
          Format.fprintf fmt "%a.0p%se%s"
            (Number.print_in_base 16 None) i (BigInt.to_string p2) (BigInt.to_string p5)
      end

let const_v2 fmt c =
  match c with
  | ConstInt { il_kind=_; il_int=i } ->
      Format.pp_print_string fmt (BigInt.to_string i)
  | ConstReal { rl_kind=_; rl_real={ rv_sig=i; rv_pow2=p2; rv_pow5=p5 } } ->
      Format.fprintf fmt "%s.p%se%s"
        (BigInt.to_string i) (BigInt.to_string p2) (BigInt.to_string p5)

end

211
(* {2 Shapes} *)
212

213
type shape = string
214

215
let string_of_shape s = s
216

217
let shape_of_string s = s
218

219
let equal_shape (x:string) y = x = y
220

221
let debug = Debug.register_info_flag "session_pairing"
Andrei Paskevich's avatar
Andrei Paskevich committed
222 223
  ~desc:"Print@ debugging@ messages@ about@ reconstruction@ of@ \
         session@ trees@ after@ modification@ of@ source@ files."
224

225
let current_shape_version = 6
226

227
type shape_version = SV1 | SV2 | SV3 | SV4 | SV5
MARCHE Claude's avatar
MARCHE Claude committed
228

229 230
module Shape = struct

231
(* similarity code of terms, or of "shapes"
232

233
example:
234 235 236 237 238

  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
239 240
*)

241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259
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'

260 261
exception ShapeTooLong

262 263
let shape_buffer = Buffer.create 17

264 265 266
let check () =
  if Buffer.length shape_buffer >= 1024 then raise ShapeTooLong

267 268
let push s =
  Buffer.add_string shape_buffer s;
269
  check ()
270 271 272

let pushc c =
  Buffer.add_char shape_buffer c;
273
  check ()
274

275 276 277 278 279 280 281 282 283 284 285 286 287
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
288

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

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

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

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

303 304 305 306 307 308 309 310
let const_shape v c =
  let fmt = Format.formatter_of_buffer shape_buffer in
  begin match v with
  | SV1 | SV2 | SV3 | SV4 -> Common.const_v1 fmt c
  | SV5 -> Common.const_v2 fmt c
  end;
  Format.pp_print_flush fmt ();
  check ()
311 312

let rec pat_shape c m p : 'a =
313
  match p.pat_node with
314 315
    | Pwild -> pushc tag_wild
    | Pvar _ -> pushc tag_var
316
    | Papp (f, l) ->
317 318 319 320
       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
321
    | Por (p, q) ->
322
       pat_shape c m q; pushc tag_or; pat_shape c m p
MARCHE Claude's avatar
MARCHE Claude committed
323

324 325
let rec t_shape ~version c m t =
  let fn = t_shape ~version c m in
MARCHE Claude's avatar
MARCHE Claude committed
326
  match t.t_node with
327
    | Tconst c -> pushc tag_const; const_shape version c
328
    | Tvar v -> pushc tag_var; ident m v.vs_name
MARCHE Claude's avatar
MARCHE Claude committed
329
    | Tapp (s,l) ->
330 331 332
       pushc tag_app;
       ident m s.ls_name;
       List.iter fn l
333 334
    | Tif (f,t1,t2) ->
      begin match version with
335
      | SV1 | SV2 -> pushc tag_if; fn f; fn t1; fn t2
336
      | SV3 | SV4 | SV5 -> pushc tag_if; fn t2; fn t1; fn f
337
      end
MARCHE Claude's avatar
MARCHE Claude committed
338
    | Tcase (t1,bl) ->
339
        let br_shape b =
MARCHE Claude's avatar
MARCHE Claude committed
340
          let p,t2 = t_open_branch b in
341
          match version with
342
          | SV1 | SV2 ->
343 344 345
            pat_shape c m p;
            pat_rename_alpha c m p;
            t_shape ~version c m t2
346
          | SV3 | SV4 | SV5 ->
347 348 349
            pat_rename_alpha c m p;
            t_shape ~version c m t2;
            pat_shape c m p
MARCHE Claude's avatar
MARCHE Claude committed
350
        in
351
        begin match version with
352
        | SV1 | SV2 ->
353 354 355
                 pushc tag_case;
                 fn t1;
                 List.iter br_shape bl
356
        | SV3 | SV4 | SV5 ->
357 358 359
           pushc tag_case;
           List.iter br_shape bl;
           fn t1
360
        end
MARCHE Claude's avatar
MARCHE Claude committed
361
    | Teps b ->
362
        pushc tag_eps;
MARCHE Claude's avatar
MARCHE Claude committed
363
        let u,f = t_open_bound b in
364 365
        vs_rename_alpha c m u;
        t_shape ~version c m f
MARCHE Claude's avatar
MARCHE Claude committed
366
    | Tquant (q,b) ->
367
        let vl,triggers,f1 = t_open_quant b in
368
        vl_rename_alpha c m vl;
369 370
        (* argument first, intentionally, to give more weight on A in
           forall x,A *)
371 372 373 374 375 376 377 378 379
        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
380
    | Tbinop (o,f,g) ->
381 382 383 384 385 386 387 388 389 390
       (* 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
391 392
    | Tlet (t1,b) ->
        let u,t2 = t_open_bound b in
393
        vs_rename_alpha c m u;
MARCHE Claude's avatar
MARCHE Claude committed
394 395
        begin
          match version with
396
            | SV1 ->
397
               pushc tag_let; fn t1; t_shape ~version c m t2
398
            | SV2 | SV3 | SV4 | SV5 ->
399 400
                     (* t2 first, intentionally *)
                     t_shape ~version c m t2; pushc tag_let; fn t1
MARCHE Claude's avatar
MARCHE Claude committed
401
        end
402 403
    | Tnot f ->
      begin match version with
404
      | SV1 | SV2 -> fn f; pushc tag_not
405
      | SV3 | SV4 | SV5 -> pushc tag_not; fn f
406
      end
407 408
    | Ttrue -> pushc tag_true
    | Tfalse -> pushc tag_false
MARCHE Claude's avatar
MARCHE Claude committed
409

410 411
let t_shape_task ~version ~expl t =
  Buffer.clear shape_buffer;
412
  let f = Task.task_goal_fmla t in
413 414
  let c = ref (-1) in
  let m = ref Ident.Mid.empty in
415 416
  let () =
    try
417 418 419
      (* expl *)
      begin match version with
      | SV1 | SV2 -> ()
420
      | SV3 | SV4 | SV5 -> push expl end;
421 422 423 424 425
      (* goal shape *)
      t_shape ~version c m f;
      (* introduced premises shape *)
      begin match version with
      | SV1 | SV2 | SV3 -> ()
426
      | SV4 | SV5 ->
427 428
         let open Decl in
         let introduced id = Ident.Sattr.mem
MARCHE Claude's avatar
MARCHE Claude committed
429
                               Inlining.intro_attr
430 431 432 433 434 435 436 437 438 439 440 441 442 443
                               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 -> ()
444 445
  in
  Buffer.contents shape_buffer
446

447 448
end

449 450 451
(*
let time = ref 0.0
 *)
452

453
let t_shape_task ?(version=current_shape_version) ~expl t =
454
  let version = match version with
455
    | 1 -> SV1 | 2 -> SV2 | 3 | 4 -> SV3 | 5 -> SV4 | 6 -> SV5
456 457
    | _ -> assert false
  in
458 459 460
(*
  let tim = Unix.gettimeofday () in
 *)
461
  let s = Shape.t_shape_task ~version ~expl t in
462 463 464 465 466 467
(*
  let tim = Unix.gettimeofday () -. tim in
  time := !time +. tim;
  Format.eprintf "[Shape times] %f/%f@." tim !time;
*)
  s
468

469 470 471 472 473 474 475 476 477
(* 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 = ""

478 479 480 481
let buffer_checksum b =
  let s = Buffer.contents b in
  Digest.to_hex (Digest.string s)

482
type checksum_version = CV1 | CV2 | CV3
483

484 485
module Checksum = struct

486 487 488 489 490
  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 '"'
491
  let option e b = function None -> char b 'n' | Some x -> char b 's'; e b x
492
  let list e b l = char b '['; List.iter (e b) l; char b ']'
493

494
  let ident_v1, clear_ident_v1 =
495
    let hident = Ident.Hid.create 17 in
496
    let c = ref 0 in
497
    (fun b id ->
498
      int b (try Ident.Hid.find hident id
499 500
        with Not_found -> incr c; Ident.Hid.add hident id !c; !c)),
    (fun () -> Ident.Hid.clear hident; c := 0)
501

502 503 504 505 506 507 508 509 510
  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
511
    | CV2 | CV3 -> ident_v2 b id
Clément Fumex's avatar
Clément Fumex committed
512

513 514 515 516 517 518 519
  let const (v,_,_,buf) c =
    let fmt = Format.formatter_of_buffer buf in
    begin match v with
    | CV1 | CV2 -> Common.const_v1 fmt c
    | CV3 -> Common.const_v2 fmt c
    end;
    Format.pp_print_flush fmt ()
520 521 522 523 524 525 526

  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

527 528
  let vsymbol (v,_,_,_ as b) vs = match v with
    | CV1 -> ty b vs.vs_ty
529
    | CV2 | CV3 -> ident b vs.vs_name; ty b vs.vs_ty
530 531 532 533 534 535 536 537 538 539

  (* 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 *)
540
  let rec term b t = match t.t_node with
541
    | Tconst c -> const b c
542 543 544
    | 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
545 546 547
    | Tcase (t1, bl) ->
        let branch b br =
          let p, t2 = t_open_branch br in
548
          pat b p; term b t2
549
        in
550
        char b 'm'; term b t1; list branch b bl
551 552
    | Teps bf ->
        let vs, f = t_open_bound bf in
553
        char b 'e'; vsymbol b vs; term b f
554 555 556 557
    | 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;
558 559
        list (list term) b triggers;
        term b f1
560 561 562 563 564 565 566
    | Tbinop (o, f, g) ->
        let tag = match o with
          | Tand -> 'A'
          | Tor -> 'O'
          | Timplies -> 'I'
          | Tiff -> 'q'
        in
567
        char b tag; term b f; term b g
568 569
    | Tlet (t1, bt) ->
        let vs, t2 = t_open_bound bt in
570 571 572
        char b 'l'; vsymbol b vs; term b t1;
        term b t2
    | Tnot f -> char b 'n'; term b f
573 574 575 576 577 578
    | 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
579 580 581 582 583
    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 *)
584 585 586 587 588 589 590

  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
591
  (* start: T G F D R L I P (C M) *)
592 593 594 595 596 597 598 599 600 601 602 603 604
  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
605 606
          list vsymbol b vl;
          term b t
607 608 609 610
        in
        char b 'L'; list logic_decl b ldl
    | Decl.Dind (s, idl) ->
        let clause b (pr, f) =
611
          ident b pr.Decl.pr_name; term b f in
612 613 614 615 616 617 618 619 620 621 622
        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;
623
        term b t
624 625 626 627 628 629 630 631

  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'
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
632
    | Theory.MTid    -> char b 'd'
633 634 635 636

  let meta b m =
    string b m.Theory.meta_name;
    list meta_arg_type b m.Theory.meta_type;
637
    char b (if m.Theory.meta_excl then 't' else 'f')
638 639 640 641 642 643 644 645

  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
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
646
    | Theory.MAid i -> char b 'd'; ident b i
647

648 649 650 651 652 653 654 655 656 657 658 659 660
  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.

661
  let rec tdecl b d = match d.Theory.td_node with
662
    | Theory.Decl d -> decl b d
663
    | Theory.Use th ->
664 665
      char b 'U'; ident b th.Theory.th_name; list string b th.Theory.th_path;
      string b (theory_v2 th)
666 667
    | Theory.Clone (th, _) ->
        char b 'C'; ident b th.Theory.th_name; list string b th.Theory.th_path
668 669
    | Theory.Meta (m, mal) -> char b 'M'; meta b m; list meta_arg b mal

670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689
  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
690
 *)
691

692
  let task_v1 =
693 694
    let c = ref 0 in
    let m = ref Ident.Mid.empty in
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
695
    let b = Buffer.create 8192 in
696 697 698 699 700 701 702
    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

703
  let task_v2 =
704 705
    let c = ref 0 in
    let m = ref Ident.Mid.empty in
706
    let b = Buffer.create 8192 in
707 708 709
    let task_hd t (cold,mold,dold) =
      c := cold;
      m := mold;
710
      tdecl (CV2,c,m,b) t.Task.task_decl;
711 712 713 714
      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
715 716 717
        | Theory.Decl { Decl.d_news = s } ->
            Ident.Sid.fold (fun id a ->
              Ident.Mid.add id (Ident.Mid.find id !m) a) s mold
718 719 720 721 722 723 724
        | _ -> !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
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
  (* WARNING: The occurence of [Trans.fold] in [task_v3] needs to be executed
     once at initialization in order for all the applications of this
     transformation to share the same Wtask ([h] created on first line of
     [Trans.fold]). In short, the closure is here just so that Trans.fold is
     executed once and shared for all functions.
     So, in particular, don't add arguments to task_v3 here. *)
  let task_v3 =
    let c = ref 0 in
    let m = ref Ident.Mid.empty in
    let b = Buffer.create 8192 in
    let task_hd t (cold,mold,dold) =
      c := cold;
      m := mold;
      tdecl (CV3,c,m,b) t.Task.task_decl;
      Buffer.add_string b (Digest.to_hex dold);
      let dnew = Digest.string (Buffer.contents b) in
      Buffer.clear b;
      let mnew = match t.Task.task_decl.Theory.td_node with
        | Theory.Decl { Decl.d_news = s } ->
            Ident.Sid.fold (fun id a ->
              Ident.Mid.add id (Ident.Mid.find id !m) a) s mold
        | _ -> !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
  let task ~version t = match version with
    | CV1 -> task_v1 t
757 758
    | CV2 -> task_v2 t
    | CV3 -> task_v3 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
    | 6 -> CV3
771 772
    | _ -> assert false
  in
773 774 775 776 777 778 779 780 781 782
(*
  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
783 784

(*************************************************************)
785
(* Pairing of new and old subgoals                           *)
786 787 788 789
(*************************************************************)

(* we have an ordered list of new subgoals

790
     newgoals = [g1; g2; g3; ...]
791 792 793

   and a list of old subgoals

794
     oldgoals = [h1 ; h2 ; ... ]
795

796
   we build a list
797

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

800 801 802 803
   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)
804 805
*)

806
module type S = sig
807 808 809 810
  type 'a t
  val checksum : 'a t -> checksum option
  val shape    : 'a t -> string
  val name     : 'a t -> Ident.ident
811
end
812

813
module Pairing(Old: S)(New: S) = struct
814

815 816 817 818
  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
819 820 821

  open Ident

822 823 824 825 826 827
  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;
  }
828

829
  (* doubly linked lists; left and right bounds point to themselves *)
830 831 832 833

  type node = {
    mutable  prev: node;
            shape: string;
834
              elt: goal_index;
835 836 837 838
    mutable valid: bool;
    mutable  next: node;
  }

839 840 841 842 843 844 845
  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
846 847 848 849 850 851 852

  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)

853 854 855 856 857 858 859
  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

860 861 862 863
  (* priority queues for pairs of nodes *)

  let dprintf = Debug.dprintf debug

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

960
  let simple_associate oldgoals newgoals =
961 962
    let rec aux acc o n =
      match o,n with
963
        | old, [] -> acc,old
964
        | [], n :: rem_n -> aux ((n,None)::acc) [] rem_n
965
        | o :: rem_o, n :: rem_n -> aux ((n,Some(o,true))::acc) rem_o rem_n
966 967 968
    in
    aux [] oldgoals newgoals

969
  let associate ~use_shapes =
970 971 972
    if use_shapes then
      associate
    else
973
      simple_associate
974

975
end