Library ChargeCore.Open.Open

Require Import ChargeCore.Open.Stack.

Require Import Coq.Lists.List Coq.Logic.FunctionalExtensionality.
Require Import Coq.Classes.RelationClasses.

Require Import ExtLib.Core.RelDec.

Set Implicit Arguments.
Unset Strict Implicit.
Set Maximal Implicit Insertion.

Section Expr.
  Polymorphic Definition OpenType := Type.
  Polymorphic Context {A val : OpenType} {HR : RelDec (@eq A)} {HROk : RelDec_Correct HR}.
  Polymorphic Context {V : ValNull val}.

  Polymorphic Definition open B : Type := stack A val -> B.

  Polymorphic Program Definition lift {A B} (f : A -> B) (a : open A) : open B :=
    fun x => f (a x).

  Polymorphic Definition expr := open val.

  Polymorphic Definition rel_open {X} : open X -> open X -> Prop := fun e1 e2 => forall s, e1 s = e2 s.
  Polymorphic Instance OpenEquivalence {X} : Equivalence (@rel_open X).
  Proof.
    split; intuition congruence.
  Qed.

  Polymorphic Definition open_const {B : Type} (b : B) : open B := fun s => b.

  Polymorphic Definition V_expr (v : val) : expr := fun s => v.
  Polymorphic Definition var_expr (x : A) : expr := fun s => s x.
  Polymorphic Definition empty_open : expr := fun x => null.

  Polymorphic Definition uncurry {A B C} (f : A -> B -> C) : (A * B) -> C :=
    fun x => f (fst x) (snd x).
  Polymorphic Definition curry {A B C} (f : A * B -> C) : A -> B -> C :=
    fun x y => f (x, y).
  Polymorphic Program Definition opair {B C} (b : open B) (c : open C) : open ((B * C)%type) :=
    fun x => (b x, c x).
End Expr.

Section SimultAdd.
  Context {A val} {HR : RelDec (@eq A)} {V: ValNull val}.
End SimultAdd.