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

WIP.

parent e3ad4806
Hide whitespace changes
Inline Side-by-side
src/BuiltinBool.ml
View file @ 3e4f17d1
......@@ -12,6 +12,7 @@
(******************************************************************************)
open Spec
open BuiltinConstructible
(* A concrete type: [bool]. *)
......
src/BuiltinConstructible.ml 0 → 100644
View file @ 3e4f17d1
open Spec
let easily_constructible generate print =
let generate () =
let value = generate() in
value, Code.document (print value)
in
constructible generate
src/BuiltinExn.ml
View file @ 3e4f17d1
......@@ -47,4 +47,4 @@ let equal =
exn_eq, Code.infix "=exn=" (* not a value; monomorphic *)
let exn =
SpecDeconstructible { equal; print }
deconstructible ~equal print
src/BuiltinInt.ml
View file @ 3e4f17d1
......@@ -12,6 +12,7 @@
(******************************************************************************)
open Spec
open BuiltinConstructible
(* A concrete type: [int]. *)
......
src/Engine.ml
View file @ 3e4f17d1
......@@ -15,7 +15,7 @@ open Printf
open Misc
open Error
open Eq
open Spec
open SpecInternalView
open Env
open Ops
......
src/Features.ml
View file @ 3e4f17d1
......@@ -11,22 +11,37 @@
(* *)
(******************************************************************************)
type 's universe =
[< `NotConstructible | `NotDeconstructible | `Arrow | `Dummy ] as 's
type 's notconstructible =
[>`NotConstructible] as 's
constraint 's = _ universe
type 's notdeconstructible =
[>`NotDeconstructible] as 's
constraint 's = _ universe
type 's arrow =
[>`Arrow] as 's
constraint 's = _ universe
(**The type abbreviation [_ constructible] is used to require a type to be
constructible. Thus, [`NotConstructible] and [`Arrow] are excluded. *)
type 's constructible =
[<`NotDeconstructible] as 's
[<`NotDeconstructible|`Dummy] as 's
(**The type abbreviation [_ deconstructible] is used to require a type to be
deconstructible. Thus, [`NotDeconstructible] and [`Arrow] are excluded. *)
type 's deconstructible =
[<`NotConstructible] as 's
[<`NotConstructible|`Dummy] as 's
(**The type abbreviation [_ spine] is used to require a type to be either an
arrow or deconstructible. Thus, [`NotDeconstructible] is excluded. *)
type 's spine =
[<`NotConstructible|`Arrow] as 's
[<`NotConstructible|`Arrow|`Dummy] as 's
(**The type abbreviation [_ data] is used to require a type to not be
an arrow. Thus, [`Arrow] is excluded. *)
type 's data =
[<`NotConstructible|`NotDeconstructible] as 's
[<`NotConstructible|`NotDeconstructible|`Dummy] as 's
src/Monolith.ml
View file @ 3e4f17d1
......@@ -17,12 +17,16 @@ type 'a gen = 'a Gen.gen
module Print = Print
type 'a printer = 'a Print.printer
module Support = Support
include Code
include Spec
type ('r, 'c, +'s) spec = ('r, 'c) Spec.spec
include Features
include Ops
include DelayedOutput
include Engine
module Support = Support
include BuiltinConstructible
include BuiltinInt
include BuiltinBool
include BuiltinExn
......@@ -30,6 +34,3 @@ include BuiltinAbstract
include BuiltinArrows
include BuiltinRot
include BuiltinSeq
include Ops
include DelayedOutput
include Engine
src/Monolith.mli
View file @ 3e4f17d1
......@@ -326,25 +326,8 @@ type ('r, 'c, +'s) spec
guess it could be made to work, actually, by arranging for
[deconstructible] and [arrow] to be unifiable. *)
(**The type abbreviation [_ constructible] is used to require a type to be
constructible. Thus, [`NotConstructible] and [`Arrow] are excluded. *)
type 's constructible =
[<`NotDeconstructible] as 's
(**The type abbreviation [_ deconstructible] is used to require a type to be
deconstructible. Thus, [`NotDeconstructible] and [`Arrow] are excluded. *)
type 's deconstructible =
[<`NotConstructible] as 's
(**The type abbreviation [_ spine] is used to require a type to be either an
arrow or deconstructible. Thus, [`NotDeconstructible] is excluded. *)
type 's spine =
[<`NotConstructible|`Arrow] as 's
(**The type abbreviation [_ data] is used to require a type to not be
an arrow. Thus, [`Arrow] is excluded. *)
type 's data =
[<`NotConstructible|`NotDeconstructible] as 's
(* TODO check doc *)
include module type of Features
(* -------------------------------------------------------------------------- *)
......@@ -370,7 +353,7 @@ type 's data =
This specification is constructible. *)
val constructible:
(unit -> 't code) ->
('t, 't, [>`NotDeconstructible]) spec
('t, 't, _ notdeconstructible) spec
(* -------------------------------------------------------------------------- *)
......@@ -388,7 +371,7 @@ val constructible:
val easily_constructible:
't gen ->
't printer ->
('t, 't, [>`NotDeconstructible]) spec
('t, 't, _ notdeconstructible) spec
(* -------------------------------------------------------------------------- *)
......@@ -410,7 +393,7 @@ val easily_constructible:
val deconstructible:
?equal:(('t -> 't -> bool) code) ->
't printer ->
('t, 't, [>`NotConstructible]) spec
('t, 't, _ notconstructible) spec
(* -------------------------------------------------------------------------- *)
......@@ -475,7 +458,7 @@ val bool: (bool, bool, _) spec
This specification is deconstructible. It is {i not} constructible, because
it usually does not make sense to generate an integer in the huge interval
[\[min_int, max_int\]]. *)
val int: (int, int, [>`NotConstructible]) spec
val int: (int, int, _ notconstructible) spec
(**[int_within range] is the basic type [int], equipped with the generator
[range].
......@@ -501,7 +484,7 @@ val sequential: unit -> (int, int, _) spec
(**[exn] represents the base type [exn].
This specification is deconstructible, but not constructible. *)
val exn: (exn, exn, [>`NotConstructible]) spec
val exn: (exn, exn, _ notconstructible) 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
......@@ -517,7 +500,7 @@ val override_exn_eq: ((exn -> exn -> bool) -> (exn -> exn -> bool)) -> unit
(**[ignored] describes a result that should be ignored.
This specification is deconstructible, but not constructible. *)
val ignored: ('r, 'c, [>`NotConstructible]) spec
val ignored: ('r, 'c, _ notconstructible) spec
(* -------------------------------------------------------------------------- *)
......@@ -661,7 +644,7 @@ val nondet:
val (^>):
('r1, 'c1, _ constructible) spec ->
('r2, 'c2, _ spine) spec ->
('r1 -> 'r2, 'c1 -> 'c2, [>`Arrow]) spec
('r1 -> 'r2, 'c1 -> 'c2, _ arrow) spec
(**[^?>] is the nondeterministic arrow combinator. [spec1 ^?> spec2] is a
short-hand for [spec1 ^> nondet spec2].
......@@ -672,7 +655,7 @@ val (^>):
val (^?>):
('r1, 'c1, _ constructible) spec ->
('r2, 'c2, _ deconstructible) spec ->
('r1 -> 'c2 -> 'r2 diagnostic, 'c1 -> 'c2, [>`Arrow]) spec
('r1 -> 'c2 -> 'r2 diagnostic, 'c1 -> 'c2, _ arrow) spec
(**[^!>] is the exceptional arrow combinator. It describes a function that may
raise an exception, and it requests that this exception be caught and
......@@ -687,8 +670,8 @@ val (^?>):
the codomain must be deconstructible. The codomain cannot be an arrow. *)
val (^!>):
('r1, 'c1, _ constructible) spec ->
('r2, 'c2, _ spine) spec ->
('r1 -> 'r2, 'c1 -> 'c2, [>`Arrow]) spec
('r2, 'c2, _ deconstructible) spec ->
('r1 -> 'r2, 'c1 -> 'c2, _ arrow) spec
(**[^!?>] is an arrow combinator that combines the exception effect and the
nondeterminism effect. It describes a function that may raise an exception.
......@@ -712,7 +695,7 @@ val (^!?>):
(
'r1 -> ('c2, exn) result -> ('r2, exn) result diagnostic,
'c1 -> 'c2,
[>`Arrow]
_ arrow
) spec
(**[^>>] is the dependent arrow constructor. It describes a function of one
......@@ -732,7 +715,7 @@ val (^!?>):
val (^>>):
('r1, 'c1, _ constructible) spec ->
('r1 -> ('r2, 'c2, _ spine) spec) ->
('r1 -> 'r2, 'c1 -> 'c2, [>`Arrow]) spec
('r1 -> 'r2, 'c1 -> 'c2, _ arrow) spec
(* -------------------------------------------------------------------------- *)
......
src/Ops.ml
View file @ 3e4f17d1
......@@ -12,7 +12,7 @@
(******************************************************************************)
open Error
open Spec
open SpecInternalView
(* The engine needs a description of the operations. *)
......@@ -48,6 +48,7 @@ let declare name spec rv cv =
| Some _ ->
error "cannot use Monolith.declare after Monolith.main has been called."
| None ->
let spec = (spec : (_, _, _) Spec.spec :> (_, _) spec) in
operations := (name, Value (spec, rv, cv)) :: !operations
(* [pick] freezes the set of operations, if necessary, and picks an operation
......
src/Ops.mli
View file @ 3e4f17d1
......@@ -14,8 +14,8 @@
open Spec
(* See Monolith.mli for documentation. *)
val declare : string -> ('r, 'c) spec -> 'r -> 'c -> unit
val declare : string -> ('r, 'c, _ spine) 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. *)
val pick: unit -> string * value
val pick: unit -> string * SpecInternalView.value
src/Spec.ml
View file @ 3e4f17d1
(******************************************************************************)
(* *)
(* Monolith *)
(* *)
(* François Pottier *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under the *)
(* terms of the GNU Lesser General Public License as published by the Free *)
(* Software Foundation, either version 3 of the License, or (at your *)
(* option) any later version, as described in the file LICENSE. *)
(* *)
(******************************************************************************)
open Code
(* -------------------------------------------------------------------------- *)
(** When the combinator [nondet] is used, the reference implementation has
access to a result of type ['c] produced by the candidate implementation.
It must either accept the candidate's result and produce its own result of
type ['r], or reject the candidate's result and produce a piece of OCaml
code that explains why this result is unacceptable. This code is
represented by a function of type [document -> document]. It receives the
name of a variable, such as [observed], which stands for the candidate's
result. This code could be an OCaml assertion that the observed result
does not satisfy, or it could be just a comment. *)
type 'r diagnostic =
| Valid of 'r
| Invalid of (PPrint.document -> PPrint.document)
(** In the common case where ['r] and ['c] are the same type, the following
type abbreviation is useful. The reference implementation must produce
a result of type ['r nondet] instead of just ['r]. *)
type 'r nondet =
'r -> 'r diagnostic
(* -------------------------------------------------------------------------- *)
(* A value of type [('r, 'c) spec] is a runtime representation of a
specification. This specification describes an operation whose type in the
reference implementation is ['r] and whose type in the candidate
implementation is ['c]. *)
(* In other words, a specification can be thought of a binary (or
relational) type, in contrast with the more common unary types
that describe a single value. *)
(* -------------------------------------------------------------------------- *)
(* The data constructors of the type [(_, _) spec] can be organized in several
groups:
1. The data constructors for "positive" data, that is, data that can be
constructed and deconstructed -- typically most data except functions.
2. The data constructors for "negative" data, typically functions, which
cannot be constructed or deconstructed, but can be used (applied).
3. [SpecMapOutof] describes data that can be constructed, but not
deconstructed or used in any way.
4. [SpecIfPol] is eliminated by [normalize].
5. [SpecDeferred] allows constructing recursive (cyclic) specifications. *)
type (_, _) spec =
(* 1. Positive data. *)
(* A constructible type is an OCaml type that is equipped with a generator.
This must be a concrete type: the types ['r] and ['c] must coincide. *)
| SpecConstructible :
{ generate : unit -> 't code } ->
('t, 't) spec
(* An abstract base type has possibly different representations in the
reference and candidate implementations. Its values are opaque (not
observable). A tag allows testing at runtime whether two abstract base
types are equal; this is used when one wishes to select a variable of
appropriate type in the environment. *)
(* We associate this tag with the product type ['r * c] so that the dynamic
equality of two tags will imply a static type equality both on the
reference side and on the implementation side. This is a situation where
the injectivity of the product type is exploited: the equality of two
product types implies the equality of their components. *)
| SpecBaseAbstract:
('r * 'c) Tag.tag * ('r, 'c) abstract -> ('r, 'c) spec
(* Unit. *)
| SpecUnit:
(unit, unit) spec
(* Pairs. *)
| SpecPair :
('r1, 'c1) spec * ('r2, 'c2) spec -> ('r1 * 'r2, 'c1 * 'c2) spec
(* Options. *)
| SpecOption :
('r, 'c) spec -> ('r option, 'c option) spec
(* Results. *)
| SpecResult :
('r1, 'c1) spec * ('r2, 'c2) spec ->
(('r1, 'r2) result, ('c1, 'c2) result) spec
(* Lists. *)
| SpecList:
int Gen.gen * ('r, 'c) spec ->
('r list, 'c list) spec
(* A subset specification [Spec (spec, p)] restricts the specification
[spec] to the subset of the values that satisfy the predicate [p].
Technically, the predicate [p] applies to a reference-side value. This is
again justified by the fact that we want to rely on the reference
implementation when we determine which arguments are acceptable for an
operation. *)
(* This feature is typically used to require an argument of abstract type to
satisfy a precondition. It can also be used at a concrete type, but this
is not recommended, as one usually prefers to generate a suitable value
directly, rather than first generate a possibly-unsuitable value and then
eliminate it. *)
| SpecSubset :
('r, 'c) spec * ('r -> bool) -> ('r, 'c) spec
(* The mark [SpecNondet] is used to annotate the return type of an operation
whose *specification* is nondeterministic. This indicates that several
results are permitted; therefore, one cannot expect the reference
implementation to produce "the" expected result. Instead, one must run
the candidate implementation first, and give the reference implementation
access to the result produced by the candidate. In many (albeit not all)
situations, this is sufficient for the reference implementation to
determine how it must behave. *)
| SpecNondet :
('r, 'c) spec ->
('c -> 'r diagnostic, 'c) spec
(* 2. Negative data. *)
(* 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]
must coincide. *)
| SpecDeconstructible :
{ equal : ('t -> 't -> bool) code; print : 't -> PPrint.document } ->
('t, 't) spec
(* [SpecTop] describes an output that must be ignored. *)
| SpecTop :
('r, 'c) spec
(* Arrows. *)
| SpecArrow :
('r1, 'c1) spec * ('r2, 'c2) spec -> ('r1 -> 'r2, 'c1 -> 'c2) 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
the specification. Technically, the codomain depends on a value of type
['r1], the left projection of the domain. This is justified by the fact
that we want to rely on the reference implementation when we determine
which arguments are acceptable for an operation. *)
| SpecDependentArrow :
('r1, 'c1) spec * ('r1 -> ('r2, 'c2) spec) -> ('r1 -> 'r2, 'c1 -> 'c2) 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].
To do so, the user provides a wrapper. Technically, the user must provide
the name of this wrapper as well as its implementation on each side. The
user also provides a description of the destination type, hence the name
[SpecMapInto]. *)
| SpecMapInto :
('r1 -> 'r2) *
('c1 -> 'c2) code *
('r2, 'c2) spec ->
('r1, 'c1) spec
(* 3. Special case. *)
(* [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].
To do so, the user provides a wrapper. Technically, the user must provide
the name of this wrapper as well as its implementation on each side. The
user also provides a description of the source type, hence the name
[SpecMapOutof]. *)
| SpecMapOutof :
('r1 -> 'r2) *
('c1 -> 'c2) code *
('r1, 'c1) spec ->
('r2, 'c2) spec
(* 4. Special cases. *)
(* [SpecIfPol (neg, pos)] is a specification that is interpreted differently
depending on whether it appears in a negative or positive position. *)
| SpecIfPol :
('r, 'c) spec * ('r, 'c) spec ->
('r, 'c) spec
(* [SpecDeferred] allows constructing recursive (cyclic) specifications. *)
| SpecDeferred :
('r, 'c) spec Lazy.t ->
('r, 'c) spec
(* -------------------------------------------------------------------------- *)
(* The following information is associated with an abstract base type. *)
and ('r, 'c) abstract = {
(* The base name used for a variable of this type. *)
aty_var : string;
(* A [check] function used to the check the well-formedness of a value
of this type. *)
aty_check : 'r -> ('c -> unit) code;
}
(* -------------------------------------------------------------------------- *)
(* Constructor functions. *)
(* Short public names for the constructors above. *)
let unit =
SpecUnit
let ( *** ) first second =
SpecPair (first, second)
let option spec =
SpecOption spec
let result spec1 spec2 =
SpecResult (spec1, spec2)
let list ?length:(length=Gen.lt 16) spec =
SpecList (length, spec)
let ignored =
SpecTop
let (^>) domain codomain =
SpecArrow (domain, codomain)
let (^>>) domain codomain =
SpecDependentArrow (domain, codomain)
let (%) p spec =
SpecSubset (spec, p)
let nondet spec =
SpecNondet spec
let map_into rwrap cwrap spec =
SpecMapInto (rwrap, cwrap, spec)
let map_outof rwrap cwrap spec =
SpecMapOutof (rwrap, cwrap, spec)
let ifpol neg pos =
SpecIfPol (neg, pos)
let fix f =
let rec spec = SpecDeferred (lazy (f spec)) in
spec
let constructible (generate : unit -> 't code) =
SpecConstructible { generate }
let easily_constructible (generate : unit -> 't) (print : 't -> PPrint.document) =
let generate () =
let value = generate() in
value, Code.document (print value)
in
constructible generate
let deconstructible ?equal:(equal=((=), Code.infix "=")) print =
SpecDeconstructible { equal; print }
(* -------------------------------------------------------------------------- *)
(* A value is a triple of a runtime type representation, a reference value,
and a candidate value. *)
type value =
| Value : ('r, 'c) spec * 'r * 'c -> value
(* -------------------------------------------------------------------------- *)
(* [declare_abstract_type] extends the type [spec] with a new case. The new
type is regarded as abstract: its representation is [r] in the reference
implementation and [c] in the candidate implementation. The new data
constructor has type [(r, c) spec]. *)
let default_check : type r c . r -> (c -> unit) code =
fun _ ->
(fun _ -> ()), Code.constant "(fun _ -> ())"
let default_var =
"x"
let declare_abstract_type
?check:(check=default_check)
?var:(var=default_var)
()
=
(* Create a new tag for this abstract type. *)
let tag = Tag.new_tag () in
(* Done. *)
SpecBaseAbstract (tag, { aty_var = var; aty_check = check })
include Features
include SpecInternalView
type ('r, 'c, +'s) spec = ('r, 'c) SpecInternalView.spec
src/Spec.mli 0 → 100644
View file @ 3e4f17d1
(* This module is a copy of the module Spec where the algebraic data type
[spec] has been turned into an abstract type and has received an extra
type parameter ['s]. *)
(* This abstraction barrier ensures that the Builtin* modules do not have
access to the internal view of the type [spec]. This helps us ensure that
we do not make mistakes in their types. *)
open Gen
open Print
open Code
include module type of Features
type ('r, 'c, +'s) spec = private ('r, 'c) SpecInternalView.spec
val constructible:
(unit -> 't code) ->
('t, 't, _ notdeconstructible) spec
val deconstructible:
?equal:(('t -> 't -> bool) code) ->
't printer ->
('t, 't, _ notconstructible) spec
val declare_abstract_type:
?check: ('r -> ('c -> unit) code) ->
?var: string ->
unit ->
('r, 'c, _) spec
val unit: (unit, unit, _) spec
val ignored: ('r, 'c, _ notconstructible) spec
val ( *** ):
('r1, 'c1, 's data) spec ->
('r2, 'c2, 's data) spec ->
('r1 * 'r2, 'c1 * 'c2, 's) spec
val option:
('r, 'c, 's data) spec ->
('r option, 'c option, 's) spec
val result: