termcode.mli 2.95 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

12 13 14 15 16
(** Explanations *)

val goal_expl_task:
  root:bool -> Task.task -> Ident.ident * string option * Task.task

17 18 19 20 21 22 23 24
val search_labels :
  (Ident.Slab.t -> 'a list) -> Term.term -> 'a list
  (* [search_labels callback f] traverses [f] in a top-down manner and calls the
     [callback] on the label set of all encountered nodes. As soon as the
     callback returns a non-empty list, the traversal is stopped and that list
     is returned. Raises exception Exit if the entire term has been traversed.
   *)

25
(** Shapes *)
MARCHE Claude's avatar
MARCHE Claude committed
26

27 28
val reset_dict : unit -> unit

29
val current_shape_version : int
30 31 32 33

type shape
val string_of_shape: shape -> string
val shape_of_string: string -> shape
34
val equal_shape: shape -> shape -> bool
35 36 37
(* unused
val print_shape: Format.formatter -> shape -> unit
*)
38

39 40 41 42
(* val t_shape_buf : ?version:int -> Term.term -> shape *)
  (** returns the shape of a given term *)
val t_shape_task: ?version:int -> Task.task -> shape
  (** returns the shape of a given task *)
MARCHE Claude's avatar
MARCHE Claude committed
43

44
(** Checksums *)
MARCHE Claude's avatar
MARCHE Claude committed
45

46 47 48 49 50 51
type checksum
val print_checksum: Format.formatter -> checksum -> unit
val string_of_checksum: checksum -> string
val checksum_of_string: string -> checksum
val equal_checksum: checksum -> checksum -> bool
val dumb_checksum: checksum
52

53 54
val buffer_checksum : Buffer.t -> checksum

55 56
val task_checksum : ?version:int -> Task.task -> checksum

57
(** Pairing algorithm *)
58 59

module type S = sig
60 61 62 63
  type 'a t
  val checksum : 'a t -> checksum option
  val shape    : 'a t -> shape
  val name     : 'a t -> Ident.ident
64 65
end

66
module Pairing(Old: S)(New: S) : sig
67
  val associate:
68 69
    use_shapes:bool -> 'a Old.t list -> 'b New.t list ->
    ('b New.t * ('a Old.t * bool) option) list * 'a Old.t list
70 71
    (** Associate new goals to (possibly) old goals
        Each new goal is mapped either to
72 73
        - [None]: no old goal associated
        - [Some (h, false)]: the matching is exact (same checksums)
74
        - [Some (h, true)]: inexact matching (thus proofs for the new goal
75 76 77 78
          must be assumed obsolete)

        if [use_shapes] is set, the clever algorithm matching shapes is used,
        otherwise a simple association in the given order of goals is done.
79

80 81 82 83 84
        Note: in the output, goals appear in the same order as in [newgoals]

        the second list returned is the list of non-associated old goals.

     *)
85

86
end