Skip to content
GitLab
Commit e2565e9f authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Attempt to use polymorphic variants as a more flexible encoding.

parent ecb2ecfd
Hide whitespace changes
Inline Side-by-side
src/BuiltinBool.ml
View file @ e2565e9f
......@@ -15,7 +15,42 @@ open Spec
(* A concrete type: [bool]. *)
let bool =
let generate =
Gen.bool
let print =
Print.bool
(* In order to work around the value restriction, we must either inline away
[ifpol], [constructible_], and [deconstructible], so that [bool] is
recognized as a value; or make [bool] a function that takes a unit
argument. We choose the first approach, which is more painful for us, but
more efficient and less painful for the user. *)
(* The trouble is that the user does not have such a choice when defining her
own constants. She must use the second approach. *)
(* I would have liked to write this:
let bool () =
ifpol
(constructible_ Gen.bool Print.bool)
(deconstructible Print.bool)
(constructible_ generate print)
(deconstructible print)
*)
let appearance =
Code.infix "=" (* not a value; monomorphic *)
let equal =
(=), appearance (* polymorphic *)
let generate () =
let value = generate() in
value, Code.code (print value)
let bool =
SpecIfPol (
SpecConstructible { generate },
SpecDeconstructible { equal; print }
)
src/BuiltinExn.ml
View file @ e2565e9f
......@@ -45,3 +45,5 @@ let equal =
let exn =
SpecDeconstructible { equal; print }
(* See BuiltinBool for comments about the value restriction. *)
src/BuiltinInt.ml
View file @ e2565e9f
......@@ -15,19 +15,30 @@ open Spec
(* A concrete type: [int]. *)
(* We do not equip the type [int] with a default generator, because that
would not make much sense; we have no idea what range is relevant.
Thus, [int] is deconstructible, not constructible. *)
(* We do not equip the type [int] with a default generator, because
that would not make much sense; we have no idea what range is
relevant. Thus, [int] is deconstructible, not constructible. *)
(* See BuiltinBool for comments about the value restriction. *)
let appearance =
Code.infix "=" (* not a value; monomorphic *)
let equal =
(=), appearance (* polymorphic *)
let print =
Print.int
let int =
deconstructible Print.int
SpecDeconstructible { equal; print }
(* Equipping the type [int] with a generator. *)
let int_ (generate : unit -> int) =
ifpol
(constructible_ generate Print.int)
(int)
int
let interval i j =
int_ (Gen.interval i j)
......
src/Engine.ml
View file @ e2565e9f
......@@ -496,7 +496,7 @@ exception ConstructArgFailure of failure
backtrack and try some other instruction. *)
let rec construct_arg
: type r c . env -> (r, c) spec -> (r -> bool) -> arg * r * c
: type r c con . env -> (r, c, con) spec -> (r -> bool) -> arg * r * c
= fun env spec p ->
match spec with
......@@ -540,7 +540,7 @@ let rec construct_arg
if p rv then outcome else Gen.reject()
and construct_arg_aux
: type r c . env -> (r, c) spec -> arg * r * c
: type r c con . env -> (r, c, con) spec -> arg * r * c
= fun env spec ->
match spec with
......@@ -611,6 +611,11 @@ and construct_arg_aux
| SpecDeferred spec ->
construct_arg env (force spec) no_requirement
(* [SpecIfPol] is eliminated on the fly. We are working at a negative
polarity, so the left branch must be selected. *)
| SpecIfPol (spec, _) ->
construct_arg env spec no_requirement
(* We do not expect any of the following cases to arise. *)
| SpecDeconstructible _ ->
assert false
......@@ -624,12 +629,11 @@ and construct_arg_aux
assert false
| SpecMapInto _ ->
assert false
| SpecIfPol _ ->
assert false
and construct_arg_list
: type r c . env -> (r, c) spec -> int ->
arg list -> r list -> c list -> arg list * r list * c list
: type r c con .
env -> (r, c, con) spec -> int ->
arg list -> r list -> c list -> arg list * r list * c list
= fun env spec n args rvs cvs ->
if n = 0 then
args, rvs, cvs
......@@ -675,8 +679,8 @@ let construct_arg env spec =
in this context. *)
let rec use
: type r c .
env -> (r, c) spec -> expr -> r -> c -> expr * (value, failure) result
: type r c con .
env -> (r, c, con) spec -> expr -> r -> c -> expr * (value, failure) result
= fun env spec expr rv cv ->
match spec with
......@@ -736,6 +740,11 @@ let rec use
| SpecDeferred spec ->
use env (force spec) expr rv cv
(* [SpecIfPol] is eliminated on the fly. We are working at a positive
polarity, so the right branch must be selected. *)
| SpecIfPol (_, spec) ->
use env spec expr rv cv
| spec ->
(* Done. *)
log "Done generating a context.\n%!";
......@@ -780,8 +789,8 @@ let generate_instruction env : instruction * (value, failure) result =
problem; if it turned out to be a problem, we could easily reset it to its
initial height. *)
let rec deconstruct : type r c .
env -> r -> c -> (r, c) spec -> bool * pat
let rec deconstruct : type r c con .
env -> r -> c -> (r, c, con) spec -> bool * pat
= fun env rv cv spec ->
match spec, rv, cv with
......@@ -904,6 +913,11 @@ let rec deconstruct : type r c .
| SpecDeferred spec, _, _ ->
deconstruct env rv cv (force spec)
(* [SpecIfPol] is eliminated on the fly. We are working at a positive
polarity, so the right branch must be selected. *)
| SpecIfPol (_, spec), _, _ ->
deconstruct env rv cv spec
(* We do not expect the following cases to arise. *)
| SpecConstructible _, _, _ ->
assert false
......@@ -917,8 +931,6 @@ let rec deconstruct : type r c .
assert false
| SpecMapOutof _, _, _ ->
assert false
| SpecIfPol _, _, _ ->
assert false
(* -------------------------------------------------------------------------- *)
......
src/Monolith.mli
View file @ e2565e9f
......@@ -232,10 +232,21 @@ type 'r nondet =
these arguments should satisfy, what results are produced, what to do with
these results, and so on. *)
(** A specification of type [('r, 'c) spec] describes an operation (or, more
generally, a value) whose type on the reference side is ['r] and whose type
on the candidate side is ['c]. *)
type (_, _) spec
(** A specification of type [('r, 'c, 'con) spec] describes a
family of values whose type on the reference side is ['r] and whose
type on the candidate side is ['c].
The phantom parameter ['con] indicates whether this specification is
constructible, that is, whether Monolith is capable of constructing
the values that inhabit it. A typical example of a nonconstructible
specification is an (ordinary or dependent) function specification.
A typical example of a place where a constructible specification is
required is in the left-hand side of a function. *)
type ('r, 'c, 'con) spec
(** TODO comment must be constructible ; is not constructible *)
type 'a constructible = [< `Constructible ] as 'a
type 'a nonconstructible = [> `NonConstructible ] as 'a
(* -------------------------------------------------------------------------- *)
......@@ -255,7 +266,7 @@ type (_, _) spec
[('t, 't) spec]. *)
val constructible:
(unit -> 't code) ->
('t, 't) spec
('t, 't, _) spec
(** [constructible_ generate print] describes a constructible type.
......@@ -266,7 +277,7 @@ val constructible:
val constructible_:
't Gen.gen ->
't Print.printer ->
('t, 't) spec
('t, 't, _) spec
(** [deconstructible ~equal print] describes a basic deconstructible type,
that is, a type ['t] that is equipped with an equality test and with a
......@@ -278,7 +289,7 @@ val constructible_:
val deconstructible:
?equal:(('t -> 't -> bool) code) ->
('t Print.printer) ->
('t, 't) spec
('t, 't, _ nonconstructible) spec
(** [declare_abstract_type "t"] declares a new abstract type named "t". This
name is used in certain error messages. Which types ['r] and ['c] are
......@@ -311,44 +322,44 @@ val declare_abstract_type:
?check: ('r -> ('c -> unit) code) ->
?var: string ->
(* name: *) string ->
('r, 'c) spec
('r, 'c, _) spec
(** [unit] represents the base type [unit]. This type is constructible
and deconstructible. *)
val unit: (unit, unit) spec
val unit: (unit, unit, _) spec
(** [bool] represents the base type [bool]. This type is constructible
and deconstructible. *)
val bool: (bool, bool) spec
val bool: (bool, bool, _) spec
(** [int] represents the basic deconstructible type [int]. It is {b not}
constructible (that is, not equipped with a generator), because it usually
does not make sense to generate an integer in the huge interval [\[min_int,
max_int\]]. *)
val int: (int, int) spec
val int: (int, int, _ nonconstructible) spec
(** [int_ g] represents the basic type [int], equipped with the generator [g].
This type is both constructible and deconstructible. *)
val int_: int Gen.gen -> (int, int) spec
val int_: int Gen.gen -> (int, int, _) spec
(** [interval i j] is [int_ (Gen.interval i j)]. *)
val interval: int -> int -> (int, int) spec
val interval: int -> int -> (int, int, _) spec
(** [interval_ i j] is [int_ (Gen.interval_ i j)]. *)
val interval_: int -> int -> (int, int) spec
val interval_: int -> int -> (int, int, _) spec
(** [lt j] is [int_ (Gen.lt j)]. *)
val lt: int -> (int, int) spec
val lt: int -> (int, int, _) spec
(** [le j] is [int_ (Gen.le j)]. *)
val le: int -> (int, int) spec
val le: int -> (int, int, _) spec
(** [sequential()] is [int_ (Gen.sequential())]. *)
val sequential: unit -> (int, int) spec
val sequential: unit -> (int, int, _) spec
(** [exn] represents the base type [exn]. This type is deconstructible,
(** [exn()] represents the base type [exn]. This type is deconstructible,
but not constructible. *)
val exn: (exn, exn) spec
val exn: (exn, exn, _ nonconstructible) spec
(** [override_exn_eq f] overrides the notion of equality that is associated
with the type [exn]. This notion of equality is used to compare an
......@@ -362,24 +373,24 @@ val exn: (exn, exn) spec
val override_exn_eq: ((exn -> exn -> bool) -> (exn -> exn -> bool)) -> unit
(** [ignored] is used to describe an output that must be ignored. *)
val ignored: ('r, 'c) spec
val ignored: ('r, 'c, _ nonconstructible) spec
(** [***] is the pair type constructor. *)
val ( *** ):
('r1, 'c1) spec ->
('r2, 'c2) spec ->
('r1 * 'r2, 'c1 * 'c2) spec
('r1, 'c1, 'con) spec ->
('r2, 'c2, 'con) spec ->
('r1 * 'r2, 'c1 * 'c2, 'con) spec
(** [option] is the option type constructor. *)
val option:
('r, 'c) spec ->
('r option, 'c option) spec
('r, 'c, 'con) spec ->
('r option, 'c option, 'con) spec
(** [result] is the result type constructor. *)
val result:
('r1, 'c1) spec ->
('r2, 'c2) spec ->
(('r1, 'r2) result, ('c1, 'c2) result) spec
('r1, 'c1, 'con) spec ->
('r2, 'c2, 'con) spec ->
(('r1, 'r2) result, ('c1, 'c2) result, 'con) spec
(** [list ~length:n] is the list type constructor. It is equipped with a
generator that constructs lists whose length is comprised between 0
......@@ -388,25 +399,26 @@ val result:
irrelevant. *)
val list:
?length: int ->
('r, 'c) spec ->
('r list, 'c list) spec
('r, 'c, 'con) spec ->
('r list, 'c list, 'con) spec
(** [^>] is the ordinary arrow combinator. It is used to describe a function
of one argument. By using it several times, one can also describe curried
functions of several arguments, as is usual in OCaml. This combinator
imposes the absence of exceptions: the reference and candidate
implementations are expected to not raise any exception. *)
(* TODO comment constructibility *)
val (^>):
('r1, 'c1) spec ->
('r2, 'c2) spec ->
('r1 -> 'r2, 'c1 -> 'c2) spec
('r1, 'c1, _ constructible) spec ->
('r2, 'c2, _) spec ->
('r1 -> 'r2, 'c1 -> 'c2, _ nonconstructible) spec
(** [^?>] is the nondeterministic arrow combinator. [spec1 ^?> spec2] is a
short-hand for [spec1 ^> nondet spec2]. *)
val (^?>):
('r1, 'c1) spec ->
('r2, 'c2) spec ->
('r1 -> 'c2 -> 'r2 diagnostic, 'c1 -> 'c2) spec
('r1, 'c1, _ constructible) spec ->
('r2, 'c2, _) spec ->
('r1 -> 'c2 -> 'r2 diagnostic, 'c1 -> 'c2, _ nonconstructible) spec
(** [^!>] is the exceptional arrow combinator. It describes a function that
may raise an exception, and it requests that this exception be caught and
......@@ -415,9 +427,9 @@ val (^?>):
expected to raise comparable exceptions, according to the notion of
equality at type [exn]. *)
val (^!>):
('r1, 'c1) spec ->
('r2, 'c2) spec ->
('r1 -> 'r2, 'c1 -> 'c2) spec
('r1, 'c1, _ constructible) spec ->
('r2, 'c2, _ nonconstructible) spec ->
('r1 -> 'r2, 'c1 -> 'c2, _ nonconstructible) spec
(** [^!?>] is an arrow combinator that combines the exception effect and the
nondeterminism effect. It describes a function that may raise an exception.
......@@ -432,9 +444,13 @@ val (^!>):
then it must return its own behavior as a value of type [('r2, exn)
result]. The reference implementation must never raise an exception. *)
val (^!?>):
('r1, 'c1) spec ->
('r2, 'c2) spec ->
('r1 -> ('c2, exn) result -> ('r2, exn) result diagnostic, 'c1 -> 'c2) spec
('r1, 'c1, _ constructible) spec ->
('r2, 'c2, _ nonconstructible) spec ->
(
'r1 -> ('c2, exn) result -> ('r2, exn) result diagnostic,
'c1 -> 'c2,
_ nonconstructible
) spec
(** [^>>] is the dependent arrow constructor. It is used to describe a
function of one argument and give a name to this argument, which can be
......@@ -447,27 +463,31 @@ val (^!?>):
implementation, so the [length] function must be the one provided by
the reference implementation. *)
val (^>>):
('r1, 'c1) spec ->
('r1 -> ('r2, 'c2) spec) ->
('r1 -> 'r2, 'c1 -> 'c2) spec
('r1, 'c1, _ constructible) spec ->
('r1 -> ('r2, 'c2, _) spec) ->
('r1 -> 'r2, 'c1 -> 'c2, _ nonconstructible) spec
(** [^?>>] is the nondeterministic dependent arrow combinator. *)
val (^?>>):
('r1, 'c1) spec ->
('r1 -> ('r2, 'c2) spec) ->
('r1 -> 'c2 -> 'r2 diagnostic, 'c1 -> 'c2) spec
('r1, 'c1, _ constructible) spec ->
('r1 -> ('r2, 'c2, _) spec) ->
('r1 -> 'c2 -> 'r2 diagnostic, 'c1 -> 'c2, _ nonconstructible) spec
(** [^!>>] is the exceptional dependent arrow combinator. *)
val (^!>>):
('r1, 'c1) spec ->
('r1 -> ('r2, 'c2) spec) ->
('r1 -> 'r2, 'c1 -> 'c2) spec
('r1, 'c1, _ constructible) spec ->
('r1 -> ('r2, 'c2, _ nonconstructible) spec) ->
('r1 -> 'r2, 'c1 -> 'c2, _ nonconstructible) spec
(** [^!?>>] is the exceptional nondeterministic dependent arrow combinator. *)
val (^!?>>):
('r1, 'c1) spec ->
('r1 -> ('r2, 'c2) spec) ->
('r1 -> ('c2, exn) result -> ('r2, exn) result diagnostic, 'c1 -> 'c2) spec
('r1, 'c1, _ constructible) spec ->
('r1 -> ('r2, 'c2, _ nonconstructible) spec) ->
(
'r1 -> ('c2, exn) result -> ('r2, exn) result diagnostic,
'c1 -> 'c2,
_ nonconstructible
) spec
(** [%] is the subset constructor. It is used to restrict the set of
arguments that can be passed to an operation; in other words, it is used
......@@ -477,18 +497,22 @@ val (^!?>>):
(reference) stack is nonempty, and [stack] is the abstract type of
stacks. This constructor currently cannot be applied to the result
of an operation (where it would express a postcondition). *)
val (%): ('r -> bool) -> ('r, 'c) spec -> ('r, 'c) spec
val (%):
('r -> bool) ->
('r, 'c, 'con) spec ->
('r, 'c, 'con) spec
(** [map_into] specifies that a transformation must be applied to a value. The
user must provide the reference side of the transformation, the candidate
side of the transformation (under a displayable form), and a description of
the output type of the transformation. This is typically used to transform
the result of an operation, or an operation itself. *)
(* TODO comment *)
val map_into:
('r1 -> 'r2) ->
('c1 -> 'c2) code ->
('r2, 'c2) spec ->
('r1, 'c1) spec
('r2, 'c2, _) spec ->
('r1, 'c1, _ nonconstructible) spec
(** [map_outof] specifies that a transformation must be applied to a value. The
user must provide the reference side of the transformation, the candidate
......@@ -498,36 +522,36 @@ val map_into:
val map_outof:
('r1 -> 'r2) ->
('c1 -> 'c2) code ->
('r1, 'c1) spec ->
('r2, 'c2) spec
('r1, 'c1, 'con) spec ->
('r2, 'c2, 'con) spec
(** [flip] exchanges the first two arguments of a curried function. *)
val flip:
('r1 -> 'r2 -> 'r3, 'c1 -> 'c2 -> 'c3) spec ->
('r2 -> 'r1 -> 'r3, 'c2 -> 'c1 -> 'c3) spec
('r1 -> 'r2 -> 'r3, 'c1 -> 'c2 -> 'c3, _) spec ->
('r2 -> 'r1 -> 'r3, 'c2 -> 'c1 -> 'c3, _ nonconstructible) spec
(** [rot2] moves the second argument of a curried function to the first
position. It is synonymous with [flip]. *)
val rot2:
('r1 -> 'r2 -> 'r3, 'c1 -> 'c2 -> 'c3) spec ->
('r2 -> 'r1 -> 'r3, 'c2 -> 'c1 -> 'c3) spec
('r1 -> 'r2 -> 'r3, 'c1 -> 'c2 -> 'c3, _) spec ->
('r2 -> 'r1 -> 'r3, 'c2 -> 'c1 -> 'c3, _ nonconstructible) spec
(** [rot3] moves the third argument of a curried function to the first
position. It is synonymous with [flip]. *)
val rot3:
('r3 -> 'r1 -> 'r2 -> 'r4, 'c3 -> 'c1 -> 'c2 -> 'c4) spec ->
('r1 -> 'r2 -> 'r3 -> 'r4, 'c1 -> 'c2 -> 'c3 -> 'c4) spec
('r3 -> 'r1 -> 'r2 -> 'r4, 'c3 -> 'c1 -> 'c2 -> 'c4, _) spec ->
('r1 -> 'r2 -> 'r3 -> 'r4, 'c1 -> 'c2 -> 'c3 -> 'c4, _ nonconstructible) spec
(** [curry] transforms a function that expects a pair into a function that
expects two separate arguments. *)
val curry:
('r1 -> 'r2 -> 'r3, 'c1 -> 'c2 -> 'c3) spec ->
('r1 * 'r2 -> 'r3, 'c1 * 'c2 -> 'c3) spec
('r1 -> 'r2 -> 'r3, 'c1 -> 'c2 -> 'c3, _) spec ->
('r1 * 'r2 -> 'r3, 'c1 * 'c2 -> 'c3, _ nonconstructible) spec
(** [uncurry] performs the reverse transformation. *)
val uncurry:
('r1 * 'r2 -> 'r3, 'c1 * 'c2 -> 'c3) spec ->
('r1 -> 'r2 -> 'r3, 'c1 -> 'c2 -> 'c3) spec
('r1 * 'r2 -> 'r3, 'c1 * 'c2 -> 'c3, _) spec ->
('r1 -> 'r2 -> 'r3, 'c1 -> 'c2 -> 'c3, _ nonconstructible) spec
(** The constructor [nondet] is used to annotate the result of an operation
whose {i specification} is nondeterministic. This indicates that several
......@@ -551,8 +575,8 @@ val uncurry:
same result. It is recommended to use [nondet ignored] instead, which
suppresses the redundant equality check. *)
val nondet:
('r, 'c) spec ->
('c -> 'r diagnostic, 'c) spec
('r, 'c, _) spec ->
('c -> 'r diagnostic, 'c, _ nonconstructible) spec
(** The conditional specification [ifpol neg pos] is interpreted as the
specification [neg] when it is used in a negative position (that is,
......@@ -560,10 +584,15 @@ val nondet:
specification [pos] when it is used in a positive position (that is,
to describe the output of an operation). [ifpol] is a low-level
combinator that can be used to define higher-level abstractions. *)
val ifpol: ('r, 'c) spec -> ('r, 'c) spec -> ('r, 'c) spec
val ifpol:
('r, 'c, _ constructible) spec ->
('r, 'c, _) spec ->
('r, 'c, _) spec
(** [fix] builds a recursive specification. *)
val fix: (('r, 'c) spec -> ('r, 'c) spec) -> ('r, 'c) spec
val fix:
(('r, 'c, 'con) spec -> ('r, 'c, 'con) spec) ->
('r, 'c, 'con) spec
(** The function call [abstract spec] declares a new abstract type [t]
and equips it with a one-way conversion, from [t] to [spec]. It is
......@@ -578,12 +607,14 @@ val fix: (('r, 'c) spec -> ('r, 'c) spec) -> ('r, 'c) spec
that is, before [main] is invoked. This implies that [abstract] cannot
be used under a dependent arrow [^>>]. If you would like to so, then
you must manually hoist the call to [abstract] outside of the arrow. *)
val abstract: ('r, 'c) spec -> ('r, 'c) spec
val abstract:
('r, 'c, _) spec ->
('r, 'c, _ constructible) spec (* TODO not good *)
(* TODO document *)
val affine:
('r Seq.t, 'c Seq.t) spec ->
('r Seq.t, 'c Seq.t) spec
('r Seq.t, 'c Seq.t, 'con) spec ->
('r Seq.t, 'c Seq.t, 'con) spec
(* [declare_seq ~length:n] is a persistent sequence type constructor. It can
be used both in input and output positions. When it is used in input
......@@ -600,8 +631,8 @@ val affine:
all such calls be hoisted to the top level. *)
val declare_seq:
?length: int ->
('r, 'c) spec ->
('r Seq.t, 'c Seq.t) spec
('r, 'c, _ constructible) spec ->
('r Seq.t, 'c Seq.t, _) spec
(* -------------------------------------------------------------------------- *)
......@@ -613,7 +644,7 @@ val declare_seq:
All calls to [declare] must take place before the engine is started,
that is, before [main] is invoked. *)
val declare: string -> ('r, 'c) spec -> 'r -> 'c -> unit
val declare: string -> ('r, 'c, _) spec -> 'r -> 'c -> unit
(** [declare_] is analogous to [declare], but expects a suspension instead of
a string. Such a suspension is typically constructed using [define]. This
......@@ -622,7 +653,7 @@ val declare: string -> ('r, 'c) spec -> 'r -> 'c -> unit
All calls to [declare_] must take place before the engine is started,
that is, before [main] is invoked. *)
val declare_: string Lazy.t -> ('r, 'c) spec -> 'r -> 'c -> unit
val declare_: string Lazy.t -> ('r, 'c, _) spec -> 'r -> 'c -> unit
(** [main fuel] is the main entry point. The parameter [fuel] is the maximum
length of a run (expressed as a number of operations). A small value, such
......
src/Ops.mli
View file @ e2565e9f
......@@ -19,10 +19,10 @@ type op =
string deferred
(* See Monolith.mli for documentation. *)
val declare : string -> ('r, 'c) spec -> 'r -> 'c -> unit
val declare : string -> ('r, 'c, _) spec -> 'r -> 'c -> unit
(* See Monolith.mli for documentation. *)
val declare_ : op -> ('r, 'c) spec -> 'r -> 'c -> unit
val declare_ : op -> ('r, 'c, _) spec -> 'r -> 'c -> unit
(* [pick()] chooses an operation among those that have been declared.
It returns a pair of the operation's name and value. *)
......
src/Spec.ml
View file @ e2565e9f
......@@ -41,14 +41,23 @@ type 'r nondet =
(* See Monolith.mli for an explanation of the parameters of this type. *)
(* The constant [constructible] is used at an occurrence that requires a
constructible type. The constant [nonconstructible] is used to describe
a specification that is not constructible. A product or a sum unifies
the ['con] parameters of its components. Therefore, a type error occurs
if one descendant of a must-be-constructible occurrence is found to be
nonconstructible. *)
type constructible
<