text:
From Coq Require Import Arith Psatz Bool String List Nat Program.Equality.

Local Open Scope string_scope.
Local Open Scope nat_scope.
Local Open Scope list_scope.

Require Import DanTrick.StackLanguage DanTrick.StackLangTheorems DanTrick.StackLangEval DanTrick.LogicProp DanTrick.StackLogicGrammar DanTrick.StackExprWellFormed.

(* Now we want to be able to express when you have the stack change size *)

Fixpoint aexp_stack_size_inc (inc: nat) (a: aexp_stack): aexp_stack :=
  match a with
  | Var_Stk k => Var_Stk (k + inc)
  | Plus_Stk a1 a2 => Plus_Stk (aexp_stack_size_inc inc a1)
                              (aexp_stack_size_inc inc a2)
  | Minus_Stk a1 a2 => Minus_Stk (aexp_stack_size_inc inc a1)
                                (aexp_stack_size_inc inc a2)
  | App_Stk f args => App_Stk f (map (aexp_stack_size_inc inc) args)
  | _ => a
  end.

Fixpoint bexp_stack_size_inc (inc: nat) (b: bexp_stack): bexp_stack :=
  match b with
  | Neg_Stk b' => Neg_Stk (bexp_stack_size_inc inc b')
  | And_Stk b1 b2 => And_Stk (bexp_stack_size_inc inc b1)
                            (bexp_stack_size_inc inc b2)
  | Or_Stk b1 b2 => Or_Stk (bexp_stack_size_inc inc b1)
                          (bexp_stack_size_inc inc b2)
  | Leq_Stk a1 a2 => Leq_Stk (aexp_stack_size_inc inc a1)
                            (aexp_stack_size_inc inc a2)
  | Eq_Stk a1 a2 => Eq_Stk (aexp_stack_size_inc inc a1)
                          (aexp_stack_size_inc inc a2)
  | _ => b
  end.

Definition meta_stack_size_inc (inc: nat) (m: MetavarPred): MetavarPred :=
  match m with
  | MetaBool b => MetaBool (transform_prop_exprs b (bexp_stack_size_inc inc))
  | MetaNat a => MetaNat (transform_prop_exprs a (aexp_stack_size_inc inc))
  end.

Definition absstack_stack_size_inc (inc: nat) (a: AbsStack): AbsStack :=
  match a with
  | AbsStkTrue => AbsStkSize inc
  | AbsStkSize n => AbsStkSize (n + inc)
  end.

Fixpoint absstate_stack_size_inc (inc: nat) (a: AbsState): AbsState :=
  let recur := absstate_stack_size_inc inc in
  match a with
  | BaseState s m =>
      BaseState (absstack_stack_size_inc inc s)
                (meta_stack_size_inc inc m)
  | AbsAnd a1 a2 =>
      AbsAnd (recur a1) (recur a2)
  | AbsOr a1 a2 =>
      AbsOr (recur a1) (recur a2)
  end.

Inductive aexp_stk_size_inc_rel: nat -> aexp_stack -> aexp_stack -> Prop :=
| IncConstStk :
  forall (inc: nat) (n: nat),
    aexp_stk_size_inc_rel inc (Const_Stk n) (Const_Stk n)
| IncVarstk :
  forall (inc: nat) (k: stack_index),
    aexp_stk_size_inc_rel inc (Var_Stk k) (Var_Stk (k + inc))
| IncPlusStk :
  forall (inc: nat) (a1 a2 a1' a2': aexp_stack),
    aexp_stk_size_inc_rel inc a1 a1' ->
    aexp_stk_size_inc_rel inc a2 a2' ->
    aexp_stk_size_inc_rel inc (Plus_Stk a1 a2) (Plus_Stk a1' a2')
| IncMinusStk :
  forall (inc: nat) (a1 a2 a1' a2': aexp_stack),
    aexp_stk_size_inc_rel inc a1 a1' ->
    aexp_stk_size_inc_rel inc a2 a2' ->
    aexp_stk_size_inc_rel inc (Minus_Stk a1 a2) (Minus_Stk a1' a2')
| IncAppStk :
  forall (inc: nat) (f: ident) (args args': list aexp_stack),
    args_stk_size_inc_rel inc args args' ->
    aexp_stk_size_inc_rel inc (App_Stk f args) (App_Stk f args')
with args_stk_size_inc_rel : nat -> (list aexp_stack) -> (list aexp_stack) -> Prop :=
| IncArgsStkNil :
  forall (inc: nat),
    args_stk_size_inc_rel inc nil nil
| IncArgsStkCons :
  forall (inc: nat) (arg arg': aexp_stack) (args args': list aexp_stack),
    aexp_stk_size_inc_rel inc arg arg' ->
    args_stk_size_inc_rel inc args args' ->
    args_stk_size_inc_rel inc (arg :: args) (arg' :: args').

Scheme aexp_stk_size_inc_rel_mut_ind := Induction for aexp_stk_size_inc_rel Sort Prop
    with args_stk_size_inc_rel_mut_ind := Induction for args_stk_size_inc_rel Sort Prop.

Combined Scheme aexp_args_size_inc_rel_mut_ind from aexp_stk_size_inc_rel_mut_ind, args_stk_size_inc_rel_mut_ind.

Definition aexp_args_size_inc_rel_mut_ind_theorem (P: nat -> aexp_stack -> aexp_stack -> Prop) (P0: nat -> list aexp_stack -> list aexp_stack -> Prop): Prop :=
  (forall (n: nat) (a a': aexp_stack),
      aexp_stk_size_inc_rel n a a' ->
      P n a a') /\
    (forall (n: nat) (l l': list aexp_stack),
        args_stk_size_inc_rel n l l' ->
        P0 n l l').

Definition aexp_args_size_inc_rel_mut_ind_theorem_P (P: nat -> aexp_stack -> aexp_stack -> Prop) : forall (n : nat) (a a0 : aexp_stack), aexp_stk_size_inc_rel n a a0 -> Prop :=
  fun (n: nat) (a a': aexp_stack) =>
  fun (_: aexp_stk_size_inc_rel n a a') =>
    P n a a'.

Definition aexp_args_size_inc_rel_mut_ind_theorem_P0 (P0: nat -> list aexp_stack -> list aexp_stack -> Prop): forall (n : nat) (l l0 : list aexp_stack), args_stk_size_inc_rel n l l0 -> Prop :=
  fun (n: nat) (l l0 : list aexp_stack) =>
  fun (H: args_stk_size_inc_rel n l l0) =>
    P0 n l l0.

Ltac aexp_args_size_inc_rel_mutual_induction P P0 P_def P0_def :=
  pose (aexp_args_size_inc_rel_mut_ind_theorem_P P_def) as P;
  pose (aexp_args_size_inc_rel_mut_ind_theorem_P0 P0_def) as P0;
  apply (aexp_args_size_inc_rel_mut_ind P P0); unfold P, P0; unfold aexp_args_size_inc_rel_mut_ind_theorem_P, aexp_args_size_inc_rel_mut_ind_theorem_P0; unfold P_def, P0_def.

Local Definition preserves_wf_P (n: nat) (a a': aexp_stack): Prop :=
  aexp_well_formed a ->
  aexp_well_formed a'.

Local Definition preserves_wf_P0 (n: nat) (args args': list aexp_stack): Prop :=
  args_well_formed args ->
  args_well_formed args'.

Theorem aexp_args_size_inc_preserves_wf :
  aexp_args_size_inc_rel_mut_ind_theorem preserves_wf_P preserves_wf_P0.
Proof.
  aexp_args_size_inc_rel_mutual_induction P P0 preserves_wf_P preserves_wf_P0; intros.
  - assumption.
  - invs H. constructor. intuition.
  - invs H1. econstructor.
    + eapply H. assumption.
    + eapply H0; assumption.
  - invs H1; econstructor; [eapply H | eapply H0]; eassumption.
  - invs H0. econstructor. apply H; assumption.
  - assumption.
  - invs H1. econstructor; [eapply H | eapply H0]; eassumption.
Qed.

Lemma aexp_size_inc_preserves_wf :
  forall inc a a',
    aexp_stk_size_inc_rel inc a a' ->
    aexp_well_formed a ->
    aexp_well_formed a'.
Proof.
  pose proof aexp_args_size_inc_preserves_wf.
  unfold preserves_wf_P, preserves_wf_P0 in H.
  unfold aexp_args_size_inc_rel_mut_ind_theorem in H.
  destruct H; auto.
Qed.

Lemma args_size_inc_preserves_wf :
  forall inc args args',
    args_stk_size_inc_rel inc args args' ->
    args_well_formed args ->
    args_well_formed args'.
Proof.
  pose proof aexp_args_size_inc_preserves_wf.
  unfold preserves_wf_P, preserves_wf_P0 in H.
  unfold aexp_args_size_inc_rel_mut_ind_theorem in H.
  destruct H; auto.
Qed.

Inductive bexp_stk_size_inc_rel : nat -> bexp_stack -> bexp_stack -> Prop :=
| IncTrueStk :
  forall (inc: nat),
    bexp_stk_size_inc_rel inc (True_Stk) (True_Stk)
| IncFalseStk :
  forall (inc: nat),
    bexp_stk_size_inc_rel inc (False_Stk) (False_Stk)
| IncNegStk :
  forall (inc: nat) (b b': bexp_stack),
    bexp_stk_size_inc_rel inc b b' ->
    bexp_stk_size_inc_rel inc (Neg_Stk b) (Neg_Stk b')
| IncAndStk :
  forall (inc: nat) (b1 b2 b1' b2': bexp_stack),
    bexp_stk_size_inc_rel inc b1 b1' ->
    bexp_stk_size_inc_rel inc b2 b2' ->
    bexp_stk_size_inc_rel inc (And_Stk b1 b2) (And_Stk b1' b2')
| IncOrStk :
  forall (inc: nat) (b1 b2 b1' b2': bexp_stack),
    bexp_stk_size_inc_rel inc b1 b1' ->
    bexp_stk_size_inc_rel inc b2 b2' ->
    bexp_stk_size_inc_rel inc (Or_Stk b1 b2) (Or_Stk b1' b2')
| IncLeqStk :
  forall (inc: nat) (a1 a2 a1' a2': aexp_stack),
    aexp_stk_size_inc_rel inc a1 a1' ->
    aexp_stk_size_inc_rel inc a2 a2' ->
    bexp_stk_size_inc_rel inc (Leq_Stk a1 a2) (Leq_Stk a1' a2')
| IncEqStk :
  forall (inc: nat) (a1 a2 a1' a2': aexp_stack),
    aexp_stk_size_inc_rel inc a1 a1' ->
    aexp_stk_size_inc_rel inc a2 a2' ->
    bexp_stk_size_inc_rel inc (Eq_Stk a1 a2) (Eq_Stk a1' a2').

Lemma bexp_size_inc_preserves_wf :
  forall inc b b',
    bexp_stk_size_inc_rel inc b b' ->
    bexp_well_formed b ->
    bexp_well_formed b'.
Proof.
  intros inc b b' H. induction H; intros; auto.
  - invs H0. econstructor; eauto.
  - invs H1. econstructor; eauto.
  - invs H1. econstructor; eauto.
  - invs H1. econstructor; eauto; eapply aexp_size_inc_preserves_wf; eauto.
  - invs H1. econstructor; eauto; eapply aexp_size_inc_preserves_wf; eauto.
Qed.

Inductive meta_stk_size_inc : nat -> MetavarPred -> MetavarPred -> Prop :=
| IncMetaBool :
  forall inc b b',
    transformed_prop_exprs (bexp_stk_size_inc_rel inc) b b' ->
    prop_rel bexp_well_formed b ->
    meta_stk_size_inc inc (MetaBool b) (MetaBool b')
| IncMetaNat :
  forall inc a a',
    transformed_prop_exprs (aexp_stk_size_inc_rel inc) a a' ->
    prop_rel aexp_well_formed a ->
    meta_stk_size_inc inc (MetaNat a) (MetaNat a').

Inductive absstack_stk_size_inc : nat -> AbsStack -> AbsStack -> Prop :=
| IncAbsStkTrue :
  forall inc,
    absstack_stk_size_inc inc AbsStkTrue (AbsStkSize inc)
| IncAbsStkSize :
  forall inc size,
    absstack_stk_size_inc inc (AbsStkSize size) (AbsStkSize (size + inc)).

Inductive state_stk_size_inc : nat -> AbsState -> AbsState -> Prop :=
| IncBaseState :
  forall inc s s' m m',
    absstack_stk_size_inc inc s s' ->
    meta_stk_size_inc inc m m' ->
    state_stk_size_inc inc (BaseState s m) (BaseState s' m')
| IncAbsAnd :
  forall inc s1 s2 s1' s2',
    state_stk_size_inc inc s1 s1' ->
    state_stk_size_inc inc s2 s2' ->
    state_stk_size_inc inc (AbsAnd s1 s2) (AbsAnd s1' s2')
| IncAbsOr :
  forall inc s1 s2 s1' s2',
    state_stk_size_inc inc s1 s1' ->
    state_stk_size_inc inc s2 s2' ->
    state_stk_size_inc inc (AbsOr s1 s2) (AbsOr s1' s2').

author: uwplse

repo: potpie

save_path: github-repos/coq/uwplse-potpie


text:
From Coq Require Import ZArith Reals Lia.
From Flocq Require Import Raux Defs Float_prop Operations.
Require Import Gappa_definitions.

Lemma float2_zero :
  forall e : Z, Float2 0 e = 0%R :>R.
Proof.
intro e.
apply F2R_0.
Qed.

Definition Fopp2 (x : float2) :=
  Float2 (- Fnum x) (Fexp x).

Lemma Fopp2_correct :
  forall x : float2,
  Fopp2 x = (- x)%R :>R.
Proof.
intros x.
unfold float2R, Fopp2. simpl.
apply F2R_Zopp.
Qed.

Definition Fmult2 (x y : float2) :=
  Float2 (Fnum x * Fnum y) (Fexp x + Fexp y).

Definition Fmult2_correct :
  forall x y : float2,
  Fmult2 x y = (x * y)%R :>R.
Proof.
intros (mx, ex) (my, ey).
exact (F2R_mult (Float radix2 mx ex) (Float radix2 my ey)).
Qed.

Definition shl (m : Z) (d : positive) :=
 match m with
 | Z0 => Z0
 | Zpos p => Zpos (shift_pos d p)
 | Zneg p => Zneg (shift_pos d p)
 end.

Lemma float2_shl_correct :
  forall m e : Z, forall d : positive,
  Float2 (shl m d) (e - Zpos d) = Float2 m e :>R.
Proof.
intros m e d.
replace (shl m d) with (m * Zpower_pos 2 d)%Z.
unfold float2R.
rewrite (F2R_change_exp _ (e - Zpos d) _ e).
simpl.
now replace (e - (e - Zpos d))%Z with (Zpos d) by ring.
generalize (Zgt_pos_0 d).
lia.
rewrite Zmult_comm.
destruct m as [|m|m] ; simpl.
apply Zmult_0_r.
now rewrite shift_pos_correct.
change (Zneg (shift_pos d m)) with (- Zpos (shift_pos d m))%Z.
rewrite shift_pos_correct.
now rewrite Zopp_mult_distr_r.
Qed.

Definition Fshift2 (x y : float2) :=
 match (Fexp x - Fexp y)%Z with
 | Zpos p => (shl (Fnum x) p, Fnum y, Fexp y)
 | Zneg p => (Fnum x, shl (Fnum y) p, Fexp x)
 | Z0 => (Fnum x, Fnum y, Fexp x)
 end.

Lemma Fshift2_correct :
  forall x y : float2,
  match Fshift2 x y with
  | (mx, my, e) => Float2 mx e = x :>R /\ Float2 my e = y :>R
  end.
Proof.
intros (mx, ex) (my, ey).
unfold Fshift2. simpl.
assert (ex = ex - ey + ey)%Z by ring.
pattern ex at - 1 ; rewrite H.
destruct (ex - ey)%Z as [|d|d] ; repeat split.
rewrite <- (float2_shl_correct mx _ d).
now ring_simplify (Zpos d + ey - Zpos d)%Z.
rewrite Zplus_comm.
apply float2_shl_correct.
Qed.

Definition Fplus2 (x y : float2) :=
 match Fshift2 x y with
 | (mx, my, e) => Float2 (mx + my) e
 end.

Lemma Fplus2_correct :
  forall x y : float2,
  Fplus2 x y = (x + y)%R :>R.
Proof.
intros x y.
unfold Fplus2.
generalize (Fshift2_correct x y).
destruct (Fshift2 x y) as ((mx, my), e).
intros (Hx, Hy).
rewrite <- Hx, <- Hy.
unfold float2R, F2R. simpl.
rewrite plus_IZR.
apply Rmult_plus_distr_r.
Qed.

Definition Fminus2 (x y : float2) :=
 match Fshift2 x y with
 | (mx, my, e) => Float2 (mx - my) e
 end.

Lemma Fminus2_correct :
  forall x y : float2,
  Fminus2 x y = (x - y)%R :>R.
Proof.
intros x y.
unfold Fminus2.
generalize (Fshift2_correct x y).
destruct (Fshift2 x y) as ((mx, my), e).
intros (Hx, Hy).
rewrite <- Hx, <- Hy.
unfold float2R, F2R. simpl.
rewrite minus_IZR.
apply Rmult_minus_distr_r.
Qed.

Definition Fcomp2 (x y : float2) :=
 match Fshift2 x y with
 | (mx, my, _) => (mx ?= my)%Z
 end.

Lemma Fcomp2_correct :
  forall x y : float2,
  Fcomp2 x y = Rcompare x y.
Proof.
intros x y.
unfold Fcomp2.
generalize (Fshift2_correct x y).
destruct (Fshift2 x y) as ((mx, my), e).
intros (Hx, Hy).
rewrite <- Hx, <- Hy.
unfold float2R, F2R. simpl.
rewrite Rcompare_mult_r.
now rewrite Rcompare_IZR.
apply bpow_gt_0.
Qed.

Definition Feq2 (x y : float2) :=
 match Fcomp2 x y with
 | Eq => true
 | _ => false
 end.

Lemma Feq2_correct :
  forall x y : float2,
  Feq2 x y = true -> x = y :>R.
Proof.
intros x y Hb.
apply Rcompare_Eq_inv.
rewrite <- Fcomp2_correct.
revert Hb.
unfold Feq2.
now case Fcomp2.
Qed.

Definition Flt2 (x y : float2) :=
 match Fcomp2 x y with
 | Lt => true
 | _ => false
 end.

Lemma Flt2_correct :
  forall x y : float2,
  Flt2 x y = true -> (x < y)%R.
Proof.
intros x y Hb.
apply Rcompare_Lt_inv.
rewrite <- Fcomp2_correct.
revert Hb.
unfold Flt2.
now case Fcomp2.
Qed.

Definition Fle2 (x y : float2) :=
 match Fcomp2 x y with
 | Gt => false
 | _ => true
 end.

Lemma Fle2_correct :
  forall x y : float2,
  Fle2 x y = true -> (x <= y)%R.
Proof.
intros x y Hb.
apply Rcompare_not_Gt_inv.
rewrite <- Fcomp2_correct.
intros H.
unfold Fle2 in Hb.
now rewrite H in Hb.
Qed.

Inductive Fle2_prop (x y : float2) : bool -> Prop :=
  | Fle2_true : (x <= y)%R -> Fle2_prop x y true
  | Fle2_false : (y < x)%R -> Fle2_prop x y false.

Lemma Fle2_spec :
  forall x y, Fle2_prop x y (Fle2 x y).
Proof.
intros x y.
case_eq (Fle2 x y) ; intros H.
apply Fle2_true.
apply Fle2_correct.
exact H.
generalize H. clear H.
unfold Fle2.
case_eq (Fcomp2 x y) ; try (intros ; discriminate).
intros H _.
apply Fle2_false.
apply Rcompare_Gt_inv.
now rewrite <- Fcomp2_correct.
Qed.

Definition Fis0 (x : float2) :=
 match (Fnum x) with
   Z0 => true
 | _ => false
 end.

Lemma Fis0_correct :
 forall x : float2,
 Fis0 x = true -> x = 0%R :>R.
intros x.
unfold Fis0.
induction x.
induction Fnum ; intro H0 ; try discriminate.
apply float2_zero.
Qed.

Definition Fpos (x : float2) :=
 match (Fnum x) with
   Zpos _ => true
 | _ => false
 end.

Lemma Fpos_correct :
  forall x : float2,
  Fpos x = true -> (0 < x)%R.
Proof.
intros (m, e) H.
unfold float2R.
apply F2R_gt_0. simpl.
revert H.
unfold Fpos. simpl.
now case m.
Qed.

Definition Fneg (x : float2) :=
 match (Fnum x) with
   Zneg _ => true
 | _ => false
 end.

Lemma Fneg_correct :
  forall x : float2,
  Fneg x = true -> (x < 0)%R.
Proof.
intros (m, e) H.
unfold float2R.
apply F2R_lt_0. simpl.
revert H.
unfold Fpos. simpl.
now case m.
Qed.

Definition Fpos0 (x : float2) :=
 match (Fnum x) with
   Zneg _ => false
 | _ => true
 end.

Lemma Fpos0_correct :
  forall x : float2,
  Fpos0 x = true -> (0 <= x)%R.
Proof.
intros (m, e) H.
unfold float2R.
apply F2R_ge_0. simpl.
revert H.
unfold Fpos. simpl.
now case m.
Qed.

Definition Fneg0 (x : float2) :=
 match (Fnum x) with
   Zpos _ => false
 | _ => true
 end.

Lemma Fneg0_correct :
  forall x : float2,
  Fneg0 x = true -> (x <= 0)%R.
Proof.
intros (m, e) H.
unfold float2R.
apply F2R_le_0. simpl.
revert H.
unfold Fpos. simpl.
now case m.
Qed.

Definition Flt2_m1 f :=
  Flt2 (Float2 (-1) 0) f.

Lemma Flt2_m1_correct :
  forall f,
  Flt2_m1 f = true ->
  (-1 < f)%R.
Proof.
intros f Hb.
generalize (Flt2_correct _ _ Hb).
unfold float2R, F2R. simpl.
now rewrite Rmult_1_r.
Qed.

Definition Fle2_m1 f :=
  Fle2 (Float2 (-1) 0) f.

Lemma Fle2_m1_correct :
  forall f,
  Fle2_m1 f = true ->
  (-1 <= f)%R.
Proof.
intros f Hb.
generalize (Fle2_correct _ _ Hb).
unfold float2R, F2R. simpl.
now rewrite Rmult_1_r.
Qed.

author: ejgallego

repo: gappa-coq

save_path: github-repos/coq/ejgallego-gappa-coq


text:
(** Generated by coq-of-ocaml *)
Require Import OCaml.OCaml.

Local Set Primitive Projections.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Local Open Scope type_scope.
Import ListNotations.

Unset Positivity Checking.
Unset Guard Checking.

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Inductive natural : Set :=
| Zero : natural
| Succ : natural -> natural.

Fixpoint plus (plus_arg0 : natural) (plus_arg1 : natural) {struct plus_arg0}
  : natural :=
  match plus_arg0 with
  | Zero => plus_arg1
  | Succ n => Succ (plus n plus_arg1)
  end.

Fixpoint mult (mult_arg0 : natural) (mult_arg1 : natural) {struct mult_arg0}
  : natural :=
  match mult_arg0 with
  | Zero => Zero
  | Succ n => plus (mult n mult_arg1) mult_arg1
  end.

Definition synth (lf1 : natural) (lf3 : natural) (lf2 : natural) : natural :=
  plus lf2 (Succ lf3).

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
From RBT Require Import SpecificationBasedGenerator.
From QuickChick Require Import QuickChick.
Set Warnings "-extraction-opaque-accessed,-extraction".
Axiom num_tests : nat. Extract Constant num_tests => "max_int".
Definition qctest_test_prop_InsertValid := (fun _ : unit => print_extracted_coq_string ("[|{" ++ show (withTime(fun tt => (quickCheckWith (updMaxDiscard (updMaxSuccess (updAnalysis stdArgs true) num_tests) num_tests) test_prop_InsertValid))) ++ "}|]")).
Definition qctest_test_prop_DeleteValid := (fun _ : unit => print_extracted_coq_string ("[|{" ++ show (withTime(fun tt => (quickCheckWith (updMaxDiscard (updMaxSuccess (updAnalysis stdArgs true) num_tests) num_tests) test_prop_DeleteValid))) ++ "}|]")).
Definition qctest_test_prop_InsertPost := (fun _ : unit => print_extracted_coq_string ("[|{" ++ show (withTime(fun tt => (quickCheckWith (updMaxDiscard (updMaxSuccess (updAnalysis stdArgs true) num_tests) num_tests) test_prop_InsertPost))) ++ "}|]")).
Definition qctest_test_prop_DeletePost := (fun _ : unit => print_extracted_coq_string ("[|{" ++ show (withTime(fun tt => (quickCheckWith (updMaxDiscard (updMaxSuccess (updAnalysis stdArgs true) num_tests) num_tests) test_prop_DeletePost))) ++ "}|]")).
Definition qctest_test_prop_InsertModel := (fun _ : unit => print_extracted_coq_string ("[|{" ++ show (withTime(fun tt => (quickCheckWith (updMaxDiscard (updMaxSuccess (updAnalysis stdArgs true) num_tests) num_tests) test_prop_InsertModel))) ++ "}|]")).
Definition qctest_test_prop_DeleteModel := (fun _ : unit => print_extracted_coq_string ("[|{" ++ show (withTime(fun tt => (quickCheckWith (updMaxDiscard (updMaxSuccess (updAnalysis stdArgs true) num_tests) num_tests) test_prop_DeleteModel))) ++ "}|]")).
Definition qctest_test_prop_InsertInsert := (fun _ : unit => print_extracted_coq_string ("[|{" ++ show (withTime(fun tt => (quickCheckWith (updMaxDiscard (updMaxSuccess (updAnalysis stdArgs true) num_tests) num_tests) test_prop_InsertInsert))) ++ "}|]")).
Definition qctest_test_prop_InsertDelete := (fun _ : unit => print_extracted_coq_string ("[|{" ++ show (withTime(fun tt => (quickCheckWith (updMaxDiscard (updMaxSuccess (updAnalysis stdArgs true) num_tests) num_tests) test_prop_InsertDelete))) ++ "}|]")).
Definition qctest_test_prop_DeleteInsert := (fun _ : unit => print_extracted_coq_string ("[|{" ++ show (withTime(fun tt => (quickCheckWith (updMaxDiscard (updMaxSuccess (updAnalysis stdArgs true) num_tests) num_tests) test_prop_DeleteInsert))) ++ "}|]")).
Definition qctest_test_prop_DeleteDelete := (fun _ : unit => print_extracted_coq_string ("[|{" ++ show (withTime(fun tt => (quickCheckWith (updMaxDiscard (updMaxSuccess (updAnalysis stdArgs true) num_tests) num_tests) test_prop_DeleteDelete))) ++ "}|]")).

Parameter OCamlString : Type.
Extract Constant OCamlString => "string".
Axiom qctest_map : OCamlString -> unit.
Extract Constant qctest_map => "
fun test_name ->
  let test_map = [
    (""test_prop_InsertValid"", qctest_test_prop_InsertValid); (""test_prop_DeleteValid"", qctest_test_prop_DeleteValid); (""test_prop_InsertPost"", qctest_test_prop_InsertPost); (""test_prop_DeletePost"", qctest_test_prop_DeletePost); (""test_prop_InsertModel"", qctest_test_prop_InsertModel); (""test_prop_DeleteModel"", qctest_test_prop_DeleteModel); (""test_prop_InsertInsert"", qctest_test_prop_InsertInsert); (""test_prop_InsertDelete"", qctest_test_prop_InsertDelete); (""test_prop_DeleteInsert"", qctest_test_prop_DeleteInsert); (""test_prop_DeleteDelete"", qctest_test_prop_DeleteDelete)
  ] in
  let test = List.assoc test_name test_map in
  test ()

let () =
  Sys.argv.(1) |> qctest_map
".

Extraction "SpecificationBasedGenerator_test_runner.ml" qctest_test_prop_InsertValid qctest_test_prop_DeleteValid qctest_test_prop_InsertPost qctest_test_prop_DeletePost qctest_test_prop_InsertModel qctest_test_prop_DeleteModel qctest_test_prop_InsertInsert qctest_test_prop_InsertDelete qctest_test_prop_DeleteInsert qctest_test_prop_DeleteDelete qctest_map.

repo: etna

sha: master