From e2565e9f5bafadb7adb5160c948622338431308f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Tue, 6 Oct 2020 11:54:59 +0200
Subject: [PATCH] Attempt to use polymorphic variants as a more flexible
encoding.
---
src/BuiltinBool.ml | 41 +++++++++-
src/BuiltinExn.ml | 2 +
src/BuiltinInt.ml | 21 +++--
src/Engine.ml | 36 ++++++---
src/Monolith.mli | 191 ++++++++++++++++++++++++++-------------------
src/Ops.mli | 4 +-
src/Spec.ml | 51 ++++++++----
7 files changed, 227 insertions(+), 119 deletions(-)
diff --git a/src/BuiltinBool.ml b/src/BuiltinBool.ml
index 1c8b51f..41403d4 100644
--- a/src/BuiltinBool.ml
+++ b/src/BuiltinBool.ml
@@ -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 }
+ )
diff --git a/src/BuiltinExn.ml b/src/BuiltinExn.ml
index b1f97bd..bbdb3c6 100644
--- a/src/BuiltinExn.ml
+++ b/src/BuiltinExn.ml
@@ -45,3 +45,5 @@ let equal =
let exn =
SpecDeconstructible { equal; print }
+
+(* See BuiltinBool for comments about the value restriction. *)
diff --git a/src/BuiltinInt.ml b/src/BuiltinInt.ml
index b7831f2..c2b9969 100644
--- a/src/BuiltinInt.ml
+++ b/src/BuiltinInt.ml
@@ -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)
diff --git a/src/Engine.ml b/src/Engine.ml
index 94b36d9..b694eb0 100644
--- a/src/Engine.ml
+++ b/src/Engine.ml
@@ -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
(* -------------------------------------------------------------------------- *)
diff --git a/src/Monolith.mli b/src/Monolith.mli
index 1e6ce6c..1ca3777 100644
--- a/src/Monolith.mli
+++ b/src/Monolith.mli
@@ -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
diff --git a/src/Ops.mli b/src/Ops.mli
index 6abd715..85ef040 100644
--- a/src/Ops.mli
+++ b/src/Ops.mli
@@ -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. *)
diff --git a/src/Spec.ml b/src/Spec.ml
index 1777758..5c7dfdc 100644
--- a/src/Spec.ml
+++ b/src/Spec.ml
@@ -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
-type nonconstructible
+(* At an occurrence that requires a constructible specification, the upper
+ bound [< `Constructible] is imposed on the index ['con].
+
+ At a specification that is not constructible, the lower bound
+ [> `NonConstructible] is imposed on the index ['con].
+
+ At a product or a sum, the ['con] parameters of the components are unified.
+
+ Therefore, a type error occurs if one descendant of a must-be-constructible
+ occurrence is found to be nonconstructible.
+
+ This encoding, based on polymorphic variants, does not require the index
+ ['con] to be universally quantified. It therefore works even in the face
+ of the value restriction. *)
+
+type 'a constructible = [< `Constructible ] as 'a
+type 'a nonconstructible = [> `NonConstructible ] as 'a
type ('r, 'c, 'con) spec =
@@ -140,7 +149,7 @@ type ('r, 'c, 'con) spec =
| SpecNondet :
('r, 'c, _) spec ->
- ('c -> 'r diagnostic, 'c, nonconstructible) spec
+ ('c -> 'r diagnostic, 'c, _ nonconstructible) spec
(* A deconstructible type is an OCaml type that is equipped with an equality
test and a printer. This must be a concrete type: the types ['r] and ['c]
@@ -152,23 +161,27 @@ type ('r, 'c, 'con) spec =
| SpecDeconstructible :
{ equal : ('t -> 't -> bool) code; print : 't -> PPrint.document } ->
- ('t, 't, nonconstructible) spec
+ ('t, 't, _ nonconstructible) spec
(* [SpecTop] describes an output that must be ignored. *)
(* It is not constructible. *)
| SpecTop :
- ('r, 'c, nonconstructible) spec
+ ('r, 'c, _ nonconstructible) spec
(* Arrows. *)
(* An arrow is not constructible: this reflects the fact that we cannot
generate a function. *)
+ (* The left-hand side of an arrow must be constructible: this reflects
+ the fact that we need to generate an argument for a function that
+ we wish to invoke. *)
+
| SpecArrow :
- ('r1, 'c1, _) spec * ('r2, 'c2, _) spec ->
- ('r1 -> 'r2, 'c1 -> 'c2, nonconstructible) spec
+ ('r1, 'c1, _ constructible) spec * ('r2, 'c2, _) spec ->
+ ('r1 -> 'r2, 'c1 -> 'c2, _ nonconstructible) spec
(* A dependent arrow allows the codomain to depend on a value of the domain.
This allows naming an argument and referring to this name in the rest of
@@ -179,9 +192,13 @@ type ('r, 'c, 'con) spec =
(* A dependent arrow is not constructible. *)
+ (* The left-hand side of a dependent arrow must be constructible: this
+ reflects the fact that we need to generate an argument for a function
+ that we wish to invoke. *)
+
| SpecDependentArrow :
- ('r1, 'c1, _) spec * ('r1 -> ('r2, 'c2, _) spec) ->
- ('r1 -> 'r2, 'c1 -> 'c2, nonconstructible) spec
+ ('r1, 'c1, _ constructible) spec * ('r1 -> ('r2, 'c2, _) spec) ->
+ ('r1 -> 'r2, 'c1 -> 'c2, _ nonconstructible) spec
(* [SpecMapInto] indicates that the user provides a value of type ['r1, 'c1]
but wishes it to be transformed on the fly to a value of type ['r2, 'c2].
@@ -197,7 +214,7 @@ type ('r, 'c, 'con) spec =
('r1 -> 'r2) *
('c1 -> 'c2) code *
('r2, 'c2, _) spec ->
- ('r1, 'c1, nonconstructible) spec
+ ('r1, 'c1, _ nonconstructible) spec
(* [SpecMapOutof] indicates that the user provides a value of type ['r1, 'c1]
but wishes it to be transformed on the fly to a value of type ['r2, 'c2].
@@ -220,7 +237,7 @@ type ('r, 'c, 'con) spec =
(* Its left-hand side must be constructible, and it is constructible. *)
| SpecIfPol :
- ('r, 'c, constructible) spec * ('r, 'c, _) spec ->
+ ('r, 'c, _ constructible) spec * ('r, 'c, _) spec ->
('r, 'c, _) spec
(* [SpecDeferred] allows constructing recursive (cyclic) specifications. *)
--
GitLab