Skip to content

qc: rename QuickChick Derive commands to QCDerive (not backwards compatible; required for QuickChick master) #23

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
JasonGross wants to merge 1 commit into
base: master
Choose a base branch
from
Open

qc: rename QuickChick Derive commands to QCDerive (not backwards compatible; required for QuickChick master) #23

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions qc-current/QC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1289,7 +1289,7 @@ End DefineGenSized.
[QuickChick] provides some automation for deriving such instances
for simple datatypes automatically! *)

Derive Arbitrary for Tree.
QCDerive Arbitrary for Tree.
(**

===> GenSizedree is defined
Expand All @@ -1298,7 +1298,7 @@ Derive Arbitrary for Tree.
Print GenSizedTree.
Print ShrinkTree.

Derive Show for Tree.
QCDerive Show for Tree.
(**
===> ShowTree is defined
*)
Expand Down
2 changes: 1 addition & 1 deletion qc-current/QuickChickTool.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,7 @@ Inductive exp : Type :=
(** Since [exp] is a simple datatype, QuickChick can derive a generator, a
shrinker, and a printer automatically. *)

Derive (Arbitrary, Show) for exp.
QCDerive (Arbitrary, Show) for exp.

(** The [eval] function evaluates an expression to a number. *)
Fixpoint eval (e : exp) : nat :=
Expand Down
14 changes: 7 additions & 7 deletions qc-current/TImp.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,7 @@ Inductive ty := TBool | TNat.
QuickChick provides a top-level vernacular command to derive such
instances. *)

Derive (Arbitrary, Show) for ty.
QCDerive (Arbitrary, Show) for ty.
(* ==>
GenSizedty is defined
Shrinkty is defined
Expand Down Expand Up @@ -352,7 +352,7 @@ Inductive exp : Type :=

(** To print expressions we derive a [Show] Instance. *)

Derive Show for exp.
QCDerive Show for exp.

(* ================================================================= *)
(** ** Typed Expressions *)
Expand Down Expand Up @@ -699,7 +699,7 @@ Definition gen_typed_has_type :=

Inductive value := VNat : nat -> value | VBool : bool -> value.

Derive Show for value.
QCDerive Show for value.

(** We can also quickly define a typing relation for values, a Dec instance
for it, and a generator for values of a given type. *)
Expand Down Expand Up @@ -862,7 +862,7 @@ Definition expression_soundness_exec :=
(** Let's see what happens if we use the default shrinker for
expressions carelessly. *)

Derive Shrink for exp.
QCDerive Shrink for exp.

Definition expression_soundness_exec_firstshrink :=
let num_vars := 4 in
Expand Down Expand Up @@ -1088,7 +1088,7 @@ Notation "'WHILE' b 'DO' c 'END'" :=
Notation "'TEST' c1 'THEN' c2 'ELSE' c3 'FI'" :=
(CIf c1 c2 c3) (at level 80, right associativity).

Derive Show for com.
QCDerive Show for com.

(** (Of course, the derived [Show] instance is not going to use these
notations!) *)
Expand Down Expand Up @@ -1296,7 +1296,7 @@ Conjecture well_typed_state_never_stuck :
produce such generators -- i.e., generators for data structures
satisfying inductively defined properties! *)

Derive ArbitrarySizedSuchThat for (fun v => has_type_value v T).
QCDerive ArbitrarySizedSuchThat for (fun v => has_type_value v T).
(** ===>
GenSizedSuchThathas_type_value is defined. *)

Expand Down Expand Up @@ -1345,7 +1345,7 @@ Print GenSizedSuchThathas_type_value.

(** Moreover, QuickChick can also derive DecOpt instances automatically, as well as proofs of correctness! *)

Derive DecOpt for (has_type_value v T).
QCDerive DecOpt for (has_type_value v T).

Print DecOpthas_type_value.

Expand Down