Require Import Program.

Inductive OrdOp := EqOP | LeOP.

Inductive BoolOp := AndOP | OrOP.

Inductive NatOp := PlusOP | MinusOP.

Definition SemOrdOp (op : OrdOp) : nat -> nat -> bool :=
  match op with
  | EqOP => Coq.Init.Nat.eqb
  | LeOP => Coq.Init.Nat.leb
  end
.

Definition SemBoolOp (op : BoolOp) : bool -> bool -> bool :=
  match op with
  | AndOP => andb
  | OrOP => orb
  end
.

Definition SemNatOp (op : NatOp) : nat -> nat -> nat :=
  match op with
  | PlusOP => Peano.plus
  | MinusOP => Peano.minus
  end
.

Definition Env := nat.

Inductive Var : Env -> Type :=
| ZVAR : forall E, Var (S E)
| SVAR : forall E, Var E -> Var (S E)
.

Inductive V E :=
| VAR : Var E -> V E
| BOOL : bool -> V E
| NAT : nat -> V E
| FUN : Expr E.+2 -> V E
| VPAIR : V E -> V E -> V E
with Expr E :=
| VAL : V E -> Expr E
| APP : V E -> V E -> Expr E
| OOp : OrdOp -> Expr E -> Expr E -> Expr E
| BOp : BoolOp -> Expr E -> Expr E -> Expr E
| NOp : NatOp -> Expr E -> Expr E -> Expr E
| LET : Expr E -> Expr E.+1 -> Expr E
| IFB : Expr E -> Expr E -> Expr E -> Expr E
| EFST : V E -> Expr E
| ESND : V E -> Expr E
.
Arguments BOOL [E] _.
Arguments NAT [E] _.

Scheme V_induction := Induction for V Sort Prop
  with E_induction := Induction for Expr Sort Prop.
Combined Scheme mutual_VE_induction from V_induction, E_induction.

Inductive FS :=
| Empty : FS
| PUSHLet : FS -> Expr 1 -> FS
| PUSHLOOp : OrdOp -> FS -> Expr 0 -> FS
| PUSHROOp : OrdOp -> FS -> Expr 0 -> FS
| PUSHLBOp : BoolOp -> FS -> Expr 0 -> FS
| PUSHRBOp : BoolOp -> FS -> Expr 0 -> FS
| PUSHLNOp : NatOp -> FS -> Expr 0 -> FS
| PUSHRNOp : NatOp -> FS -> Expr 0 -> FS
| PUSHCond : FS -> Expr 0 -> Expr 0 -> FS
.

Notation "⎣ b ⎦" := (VAL (BOOL b)) (at level 1, no associativity).
Notation "⌊ n ⌋" := (VAL (NAT n)) (at level 1, no associativity).
Notation "'v⎨' v ⎬" := (VAR v) (at level 202, no associativity).
Notation "'e⎨' v ⎬" := (VAL (VAR v)) (at level 202, no associativity).
Notation "'λ' e" := (FUN e) (at level 1, no associativity).
Infix "@" := APP (at level 201, left associativity).

Notation "∅" := Empty.
Infix "⊚" := PUSHLet (at level 1, left associativity).
Notation "fs ∘ ( e ⦓ op ⦔ ⊡ )" := (PUSHRNOp op fs e)
                                 (at level 1, left associativity).
Notation "fs ∘ ( ⊡ ⦓ op ⦔ e )" := (PUSHLNOp op fs e)
                                 (at level 1, left associativity).
Notation "fs ∘ ( e ⇆ e' )" := (PUSHCond fs e e')
                                 (at level 1, left associativity).