Test files for quickchick

meow1.v

Require Import Strings.String.
Require Import Strings.Ascii.

Open Scope string_scope.

Require Import Bool.
Require Import Omega.
Require Import Nat.

Require Import ssreflect.

Definition Var := (string * nat)%type.

Inductive STLCA : Type :=
  | unit : STLCA
  | arr (A : STLCA) (b : STLCA) : STLCA.

Inductive STLCE : Type :=
| varex (v : Var) : STLCE
| varen (n : nat) : STLCE
| lambdae (A : STLCA) (body : STLCE) : STLCE
| appe (e1 : STLCE) (e2 : STLCE) : STLCE.

Fixpoint var_eqb (x1 x2 : Var) : bool :=
  match x1 with
  | (s1, n1) => match x2 with
                | (s2, n2) => (if (s1 =? s2)%string then
                                 if (n1 =? n2)%nat then
                                   true
                                 else false
                              else false)
                end
  end.

Fixpoint open (x : Var) (e : STLCE) : STLCE :=
  match e with
  | varen 0 => varex x
  | varen (S n) => varen n
  | varex (s , n) => (match x with
                      | (s' , n') => (if (s =? s') then
                                        (if (n' <=? n) then
                                           (varex (s , (S n)))
                                         else
                                        e)
                                      else e)
                     end)
  | lambdae A body => lambdae A (open x body)
  | appe e1 e2 => (appe (open x e1) (open x e2))
  end.

Fixpoint close (x : Var) (e : STLCE) : STLCE :=
  match e with
  | varen n => varen (S n)
  | varex (s , n) => (if (var_eqb (s , n) x) then
                        varen 0
                      else
                        (match x with
                         | (s' , n') => (if (s =? s') then
                                           (if (n' <? n)%nat then
                                              (varex (s , (Nat.pred n)))
                                            else
                                              e)
                                         else
                                           e)
                     end))
  | lambdae A body => lambdae A (close x body)
  | appe e1 e2 => (appe (close x e1) (close x e2))
  end.

Module QuickChicken.
Require Import QuickChick.QuickChick.
Import QcDefaultNotation.
Open Scope qc_scope.
Import GenLow GenHigh.

Fixpoint genSTLCA (sz : nat) : G (STLCA) :=
  match sz with
  | 0 => returnGen unit
  | S x => freq [ (1, returnGen unit) ;
                  (sz, liftGen2 arr (genSTLCA x) (genSTLCA x))]
  end.

Instance show_STLCA : Show STLCA :=
  {| show :=
       let fix loop a :=
           match a with
           | unit => "unit"
           | arr A B => (loop A) ++ "->" ++ (loop B)
           end
       in loop
  |}.



Instance show_STLCE : Show STLCE :=
  {| show :=
       let fix loop a :=
           match a with
           | varex (s , n) => s
           | varen n => show n
           | lambdae A body => "λ :" ++ (show A) ++ "." ++ loop body
           | appe e1 e2 => "(" ++ loop e1 ++ " " ++ loop e2 ++ ")"
           end
       in loop
  |}.

Definition genVar : G Var :=
  liftGen2 pair (oneOf [returnGen "x" ; returnGen "y" ; returnGen "z"])
 (choose(0, 100)).

Fixpoint genSTLCE (sz : nat) : G (STLCE) :=
  match sz with
  | 0 => oneOf [ liftGen varen (choose(0, 100)) ;
                 liftGen varex genVar]
  | S x => freq [ (sz, liftGen2 lambdae (genSTLCA x)
                                (genSTLCE x)) ;
                   (sz, liftGen2 appe (genSTLCE x)
                                (genSTLCE x))]
  end.

Fixpoint stlca_eqb (A B : STLCA) : bool :=
  match (A , B) with
  | (unit , unit) => true
  | ((arr A B) , (arr A' B')) => (stlca_eqb A A') && (stlca_eqb B B')
  | _ => false
  end.

Fixpoint stlc_eqb (e1 e2 : STLCE) : bool :=
  match (e1, e2) with
  | (varen n, varen n') => (n =? n')%nat
  | (varex v , (varex v')) => (var_eqb v v')
  | ((lambdae A e) , (lambdae A' e')) => (stlca_eqb A A') && (stlc_eqb e e')
  | ((appe e1 e2) , (appe e1' e2')) => (stlc_eqb e1 e1') && (stlc_eqb e2 e2')
  | _ => false
  end.

Definition right_identityP x e := (stlc_eqb (close x (open x e)) e).
QuickChick ((forAll genVar) (fun v => (forAll (genSTLCE 5) (right_identityP v)))).
(*
Error: Unbound constructor Unit
Error: Could not compile test program
*)
End QuickChicken.

meow2.v

Require Import Strings.String.
Require Import Strings.Ascii.

Open Scope string_scope.

Require Import Bool.
Require Import Omega.
Require Import Nat.

Require Import ssreflect.

Definition Var := (string * nat)%type.

Inductive STLCA : Type :=
  | unit : STLCA
  | arr (A : STLCA) (b : STLCA) : STLCA.

Inductive STLCE : Type :=
| varex (v : Var) : STLCE
| varen (n : nat) : STLCE
| lambdae (A : STLCA) (body : STLCE) : STLCE
| appe (e1 : STLCE) (e2 : STLCE) : STLCE.

Fixpoint var_eqb (x1 x2 : Var) : bool :=
  match x1 with
  | (s1, n1) => match x2 with
                | (s2, n2) => (if (s1 =? s2)%string then
                                 if (n1 =? n2)%nat then
                                   true
                                 else false
                              else false)
                end
  end.

Fixpoint open (x : Var) (e : STLCE) : STLCE :=
  match e with
  | varen 0 => varex x
  | varen (S n) => varen n
  | varex (s , n) => (match x with
                      | (s' , n') => (if (s =? s') then
                                        (if (n' <=? n) then
                                           (varex (s , (S n)))
                                         else
                                        e)
                                      else e)
                     end)
  | lambdae A body => lambdae A (open x body)
  | appe e1 e2 => (appe (open x e1) (open x e2))
  end.

Fixpoint close (x : Var) (e : STLCE) : STLCE :=
  match e with
  | varen n => varen (S n)
  | varex (s , n) => (if (var_eqb (s , n) x) then
                        varen 0
                      else
                        (match x with
                         | (s' , n') => (if (s =? s') then
                                           (if (n' <? n)%nat then
                                              (varex (s , (Nat.pred n)))
                                            else
                                              e)
                                         else
                                           e)
                     end))
  | lambdae A body => lambdae A (close x body)
  | appe e1 e2 => (appe (close x e1) (close x e2))
  end.

Require Import QuickChick.QuickChick.
Import QcDefaultNotation.
Open Scope qc_scope.
Import GenLow GenHigh.

Fixpoint genSTLCA (sz : nat) : G (STLCA) :=
  match sz with
  | 0 => returnGen unit
  | S x => freq [ (1, returnGen unit) ;
                  (sz, liftGen2 arr (genSTLCA x) (genSTLCA x))]
  end.

Instance show_STLCA : Show STLCA :=
  {| show :=
       let fix loop a :=
           match a with
           | unit => "unit"
           | arr A B => (loop A) ++ "->" ++ (loop B)
           end
       in loop
  |}.



Instance show_STLCE : Show STLCE :=
  {| show :=
       let fix loop a :=
           match a with
           | varex (s , n) => s
           | varen n => show n
           | lambdae A body => "λ :" ++ (show A) ++ "." ++ loop body
           | appe e1 e2 => "(" ++ loop e1 ++ " " ++ loop e2 ++ ")"
           end
       in loop
  |}.

Definition genVar : G Var :=
  liftGen2 pair (oneOf [returnGen "x" ; returnGen "y" ; returnGen "z"])
 (choose(0, 100)).

Fixpoint genSTLCE (sz : nat) : G (STLCE) :=
  match sz with
  | 0 => oneOf [ liftGen varen (choose(0, 100)) ;
                 liftGen varex genVar]
  | S x => freq [ (sz, liftGen2 lambdae (genSTLCA x)
                                (genSTLCE x)) ;
                   (sz, liftGen2 appe (genSTLCE x)
                                (genSTLCE x))]
  end.

Fixpoint stlca_eqb (A B : STLCA) : bool :=
  match (A , B) with
  | (unit , unit) => true
  | ((arr A B) , (arr A' B')) => (stlca_eqb A A') && (stlca_eqb B B')
  | _ => false
  end.

Fixpoint stlc_eqb (e1 e2 : STLCE) : bool :=
  match (e1, e2) with
  | (varen n, varen n') => (n =? n')%nat
  | (varex v , (varex v')) => (var_eqb v v')
  | ((lambdae A e) , (lambdae A' e')) => (stlca_eqb A A') && (stlc_eqb e e')
  | ((appe e1 e2) , (appe e1' e2')) => (stlc_eqb e1 e1') && (stlc_eqb e2 e2')
  | _ => false
  end.

Definition right_identityP x e := (stlc_eqb (close x (open x e)) e).
QuickChick ((forAll genVar) (fun v => (forAll (genSTLCE 5) (right_identityP v)))).

(*
Warning: The following logical axioms were
encountered: semBindOptSizeMonotonicIncl_r
             semBindOptSizeMonotonicIncl_l.
Having invalid logical
axiom in the environment when extracting may lead to incorrect or
non-terminating ML terms.
 [extraction-logical-axiom,extraction]

ld: warning: URGENT: building for OSX, but linking against dylib (/usr/lib/libSystem.dylib) built for (unknown). Note: This will be an error in the future.
+++ Passed 10000 tests (0 discards)
*)