pattern.mli 2.3 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
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

12
(* Pattern compilation *)
13 14 15 16

open Ty
open Term

17
exception ConstructorExpected of lsymbol * ty
18
exception NonExhaustive of pattern list
19

20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
val compile :
  get_constructors:(tysymbol -> lsymbol list) ->
  mk_case:(term -> (pattern * 'a) list -> 'a) ->
  mk_let:(vsymbol -> term -> 'a -> 'a) ->
  term list -> (pattern list * 'a) list -> 'a
  (** [compile get_constructors mk_case mk_let terms branches]
      returns a composition of match- and let-terms equivalent
      to [match terms with branches], where every pattern is
      either a constructor applied to a list of variables, or
      a wildcard pattern.

      Raises [NonExhaustive patterns] where [patterns] is the
      list of non-covered patterns. The check is permissive:
      [match Cons t tl with Cons x xl -> ...] is accepted and
      compiled into [match t, tl with x, xl -> ...]. *)

val compile_bare :
  mk_case:(term -> (pattern * 'a) list -> 'a) ->
  mk_let:(vsymbol -> term -> 'a -> 'a) ->
  term list -> (pattern list * 'a) list -> 'a
40 41
  (** [compile_bare] does not compute non-covered patterns *)

42 43 44 45 46 47 48 49 50 51 52 53
val check_compile :
  get_constructors:(tysymbol -> lsymbol list) ->
  term list -> pattern list list -> unit
  (** [check_compile] verfies that the pattern list is exhaustive
      and raises [NonExhaustive patterns] if it is not. If the term
      list argument is empty, it is treated as a list of variables
      of appropriate types. *)

val is_exhaustive : term list -> pattern list list -> bool
  (** [is_exhaustive] checks if the pattern list is exhaustive.
      If the term list argument is empty, it is treated as a list
      of variables of appropriate types. *)