Module Qcert.NNRCimpish.Lang.NNRCimpish


NNRCimpish is a variant of the named nested relational calculus (NNRC) that is meant to be more imperative in feel. It is used as an intermediate language between NNRC and more imperative / statement oriented backends

Section NNRCimpish.
  Require Import String.
  Require Import List.
  Require Import Arith.
  Require Import EquivDec.
  Require Import Morphisms.
  Require Import Arith.
  Require Import Max.
  Require Import Bool.
  Require Import Peano_dec.
  Require Import EquivDec.
  Require Import Decidable.
  Require Import Utils.
  Require Import CommonRuntime.

  Section Syntax.

    Context {fruntime:foreign_runtime}.
    
    Inductive nnrc_impish_expr :=
    | NNRCimpishGetConstant : var -> nnrc_impish_expr (* global variable lookup ($$v) *)
    | NNRCimpishVar : var -> nnrc_impish_expr (* local variable lookup ($v) *)
    | NNRCimpishConst : data -> nnrc_impish_expr (* constant data (d) *)
    | NNRCimpishBinop : binary_op -> nnrc_impish_expr -> nnrc_impish_expr -> nnrc_impish_expr (* binary operator (e₁ ⊠ e) *)
    | NNRCimpishUnop : unary_op -> nnrc_impish_expr -> nnrc_impish_expr (* unary operator (e) *)
    | NNRCimpishGroupBy : string -> list string -> nnrc_impish_expr -> nnrc_impish_expr (* group by expression (e groupby g fields) -- only in full NNRC *)
    .

    Inductive nnrc_impish_stmt :=
    | NNRCimpishSeq : nnrc_impish_stmt -> nnrc_impish_stmt -> nnrc_impish_stmt (* sequence (s₁; s]) *)
    | NNRCimpishLet : var -> nnrc_impish_expr -> nnrc_impish_stmt -> nnrc_impish_stmt (* variable declaration (var $v := e₁; s) *)
    | NNRCimpishLetMut : var -> nnrc_impish_stmt -> nnrc_impish_stmt -> nnrc_impish_stmt (* variable declaration (var $v; s₁; s) *)
    | NNRCimpishLetMutColl : var -> nnrc_impish_stmt -> nnrc_impish_stmt -> nnrc_impish_stmt (* mutable collection declaration (var $v := {}; s1 ; s2) *)
    | NNRCimpishAssign : var -> nnrc_impish_expr -> nnrc_impish_stmt (* variable assignent ($v := e) *)
    | NNRCimpishPush : var -> nnrc_impish_expr -> nnrc_impish_stmt (* push item in mutable collection (push e in $v) *)
    | NNRCimpishFor : var -> nnrc_impish_expr -> nnrc_impish_stmt -> nnrc_impish_stmt (* for loop (for ($v in e₁) { s₂ }) *)
    | NNRCimpishIf : nnrc_impish_expr -> nnrc_impish_stmt -> nnrc_impish_stmt -> nnrc_impish_stmt (* conditional (if e₁ { s₂ } else { s₃ }) *)
    | NNRCimpishEither : nnrc_impish_expr (* case expression (either e case left $v₁ { s₁ } case right $v₂ { s₂ }) *)
                      -> var -> nnrc_impish_stmt
                      -> var -> nnrc_impish_stmt -> nnrc_impish_stmt
    .

nnrc_impish is composed of the statement evaluating the query and the variable containing the result of the evaluation
    Definition nnrc_impish : Set := (nnrc_impish_stmt * var).

  End Syntax.

  Section dec.
    Context {fruntime:foreign_runtime}.

    Global Instance nnrc_impish_expr_eqdec : EqDec nnrc_impish_expr eq.
Proof.
      change (forall x y : nnrc_impish_expr, {x = y} + {x <> y}).
      decide equality;
        try solve [apply binary_op_eqdec | apply unary_op_eqdec
                   | apply data_eqdec | apply string_eqdec].
      - decide equality; apply string_dec.
    Defined.

    Global Instance nnrc_impish_stmt_eqdec : EqDec nnrc_impish_stmt eq.
Proof.
      change (forall x y : nnrc_impish_stmt, {x = y} + {x <> y}).
      decide equality;
        try solve [apply nnrc_impish_expr_eqdec | apply string_eqdec].
    Defined.

    Global Instance nnrc_impish_eqdec : EqDec nnrc_impish eq.
Proof.
      intros [s1 r1] [s2 r2].
      destruct (r1 == r2).
      - destruct (s1 == s2).
        + left; congruence.
        + right; congruence.
      - right; congruence.
    Defined.
  End dec.

  Section Core.

    Context {fruntime:foreign_runtime}.

    Fixpoint nnrc_impish_exprIsCore (e:nnrc_impish_expr) : Prop :=
      match e with
      | NNRCimpishGetConstant _ => True
      | NNRCimpishVar _ => True
      | NNRCimpishConst _ => True
      | NNRCimpishBinop _ e1 e2 => nnrc_impish_exprIsCore e1 /\ nnrc_impish_exprIsCore e2
      | NNRCimpishUnop _ e1 => nnrc_impish_exprIsCore e1
      | NNRCimpishGroupBy _ _ _ => False
      end.

    Fixpoint nnrc_impish_stmtIsCore (s:nnrc_impish_stmt) : Prop :=
      match s with
      | NNRCimpishSeq s1 s2 =>
        nnrc_impish_stmtIsCore s1 /\ nnrc_impish_stmtIsCore s2
      | NNRCimpishLet _ e s1 =>
        nnrc_impish_exprIsCore e /\ nnrc_impish_stmtIsCore s1
      | NNRCimpishLetMut _ s1 s2 =>
        nnrc_impish_stmtIsCore s1 /\ nnrc_impish_stmtIsCore s2
      | NNRCimpishLetMutColl _ s1 s2 =>
        nnrc_impish_stmtIsCore s1 /\ nnrc_impish_stmtIsCore s2
      | NNRCimpishAssign _ e =>
        nnrc_impish_exprIsCore e
      | NNRCimpishPush _ e =>
        nnrc_impish_exprIsCore e
      | NNRCimpishFor _ e s1 =>
        nnrc_impish_exprIsCore e /\ nnrc_impish_stmtIsCore s1
      | NNRCimpishIf e s1 s2 =>
        nnrc_impish_exprIsCore e /\ nnrc_impish_stmtIsCore s1 /\ nnrc_impish_stmtIsCore s2
      | NNRCimpishEither e _ s1 _ s2 =>
        nnrc_impish_exprIsCore e /\ nnrc_impish_stmtIsCore s1 /\ nnrc_impish_stmtIsCore s2
      end .

    Definition nnrc_impishIsCore (sr:nnrc_impish) := nnrc_impish_stmtIsCore (fst sr).

    Definition nnrc_impish_core : Set := {sr:nnrc_impish | nnrc_impishIsCore sr}.

    Definition nnrc_impish_core_to_nnrc_impish (sr:nnrc_impish_core) : nnrc_impish :=
      proj1_sig sr.

    Section ext.

      Lemma nnrc_impish_exprIsCore_ext (e:nnrc_impish_expr) (pf1 pf2:nnrc_impish_exprIsCore e) : pf1 = pf2.
Proof.
        induction e; simpl in *;
          try (destruct pf1; destruct pf2; trivial);
          try f_equal; auto.
      Qed.

      Lemma nnrc_impish_stmtIsCore_ext (s:nnrc_impish_stmt) (pf1 pf2:nnrc_impish_stmtIsCore s) : pf1 = pf2.
Proof.
        induction s; simpl in *;
          try (destruct pf1; destruct pf2; trivial);
          try (destruct a; destruct a0);
          try f_equal; eauto;
            try eapply nnrc_impish_exprIsCore_ext; eauto
            ; try f_equal; eauto.
      Qed.

      Lemma nnrc_impishIsCore_ext (e:nnrc_impish) (pf1 pf2:nnrc_impishIsCore e) : pf1 = pf2.
Proof.
        apply nnrc_impish_stmtIsCore_ext.
      Qed.

      Lemma nnrc_impish_core_ext e (pf1 pf2:nnrc_impishIsCore e) :
        exist _ e pf1 = exist _ e pf2.
Proof.
        f_equal; apply nnrc_impishIsCore_ext.
      Qed.

      Lemma nnrc_impish_core_fequal (e1 e2:nnrc_impish_core) :
        proj1_sig e1 = proj1_sig e2 -> e1 = e2.
Proof.
        destruct e1; destruct e2; simpl; intros eqq.
        destruct eqq.
        apply nnrc_impish_core_ext.
      Qed.

    End ext.
    
    Section dec.

      Lemma nnrc_impish_exprIsCore_dec (e:nnrc_impish_expr) :
        {nnrc_impish_exprIsCore e} + {~ nnrc_impish_exprIsCore e}.
Proof.
        induction e; simpl; try eauto 3.
        destruct IHe1.
        - destruct IHe2; [left|right]; intuition.
        - right; intuition.
      Defined.

      Lemma nnrc_impish_stmtIsCore_dec (s:nnrc_impish_stmt) :
        {nnrc_impish_stmtIsCore s} + {~ nnrc_impish_stmtIsCore s}.
Proof.
        induction s; simpl.
        - destruct IHs1.
          + destruct IHs2; [left|right]; intuition.
          + right; intuition.
        - destruct (nnrc_impish_exprIsCore_dec n).
          + destruct IHs; [left|right]; intuition.
          + right; intuition.
        - destruct IHs1.
          + destruct IHs2; [left|right]; intuition.
          + right; intuition.
        - destruct IHs1.
          + destruct IHs2; [left|right]; intuition.
          + right; intuition.
        - apply (nnrc_impish_exprIsCore_dec n).
        - apply (nnrc_impish_exprIsCore_dec n).
        - destruct (nnrc_impish_exprIsCore_dec n).
          + destruct IHs; [left|right]; intuition.
          + right; intuition.
        - destruct (nnrc_impish_exprIsCore_dec n).
          + destruct IHs1.
            * destruct IHs2; [left|right]; intuition.
            * right; intuition.
          + right; intuition.
        - destruct (nnrc_impish_exprIsCore_dec n).
          + destruct IHs1.
            * destruct IHs2; [left|right]; intuition.
            * right; intuition.
          + right; intuition.
      Defined.

      Lemma nnrc_impishIsCore_dec (sr:nnrc_impish) :
        {nnrc_impishIsCore sr} + {~ nnrc_impishIsCore sr}.
Proof.
        apply nnrc_impish_stmtIsCore_dec.
      Defined.

      Global Instance nnrc_impish_core_eqdec : EqDec nnrc_impish_core eq.
Proof.
      intros x y.
      destruct x as [x xpf]; destruct y as [y ypf].
      destruct (x == y).
      - left. apply nnrc_impish_core_fequal; simpl; trivial.
      - right. inversion 1; congruence.
    Defined.

    End dec.

End Core.

Section Env.
  Context {fruntime:foreign_runtime}.

  Definition pd_bindings := list (string*option data).
  Definition mc_bindings := list (string*list data).
  Definition md_bindings := list (string*option data).

End Env.

End NNRCimpish.

Tactic Notation "nnrc_impish_expr_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "NNRCimpishGetConstant"%string
  | Case_aux c "NNRCimpishVar"%string
  | Case_aux c "NNRCimpishConst"%string
  | Case_aux c "NNRCimpishBinop"%string
  | Case_aux c "NNRCimpishUnop"%string
  | Case_aux c "NNRCimpishGroupBy"%string].

Tactic Notation "nnrc_impish_stmt_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "NNRCimpishSeq"%string
  | Case_aux c "NNRCimpishLet"%string
  | Case_aux c "NNRCimpishLetMut"%string
  | Case_aux c "NNRCimpishLetMutColl"%string
  | Case_aux c "NNRCimpishAssign"%string
  | Case_aux c "NNRCimpishPush"%string
  | Case_aux c "NNRCimpishFor"%string
  | Case_aux c "NNRCimpishIf"%string
  | Case_aux c "NNRCimpishEither"%string].

Delimit Scope nnrc_impish with nnrc_impish_scope.