Qcert.NNRC.Core.cNNRC

Section cNNRC.

  Context {fruntime:foreign_runtime}.

  Definition var := string.

  Inductive nnrc :=
  | NNRCVar : var → nnrc
  | NNRCConst : data → nnrc
  | NNRCBinop : binOp → nnrc → nnrc → nnrc
  | NNRCUnop : unaryOp → nnrc → nnrc
  | NNRCLet : var → nnrc → nnrc → nnrc
  | NNRCFor : var → nnrc → nnrc → nnrc
  | NNRCIf : nnrc → nnrc → nnrc → nnrc
  | NNRCEither : nnrc → var → nnrc → var → nnrc → nnrc
  
  | NNRCGroupBy : string → list string → nnrc → nnrc.

  Fixpoint nnrcIsCore (e:nnrc) : Prop :=
    match e with
    | NNRCVar _ ⇒ True
    | NNRCConst _ ⇒ True
    | NNRCBinop _ e1 e2 ⇒ (nnrcIsCore e1) ∧ (nnrcIsCore e2)
    | NNRCUnop _ e1 ⇒ (nnrcIsCore e1)
    | NNRCLet _ e1 e2 ⇒ (nnrcIsCore e1) ∧ (nnrcIsCore e2)
    | NNRCFor _ e1 e2 ⇒ (nnrcIsCore e1) ∧ (nnrcIsCore e2)
    | NNRCIf e1 e2 e3 ⇒ (nnrcIsCore e1) ∧ (nnrcIsCore e2) ∧ (nnrcIsCore e3)
    | NNRCEither e1 _ e2 _ e3 ⇒ (nnrcIsCore e1) ∧ (nnrcIsCore e2) ∧ (nnrcIsCore e3)
    
    | NNRCGroupBy _ _ _ ⇒ False
    end.

  Tactic Notation "nnrc_cases" tactic(first) ident(c) :=
    first;
    [ Case_aux c "NNRCVar"%string
    | Case_aux c "NNRCConst"%string
    | Case_aux c "NNRCBinop"%string
    | Case_aux c "NNRCUnop"%string
    | Case_aux c "NNRCLet"%string
    | Case_aux c "NNRCFor"%string
    | Case_aux c "NNRCIf"%string
    | Case_aux c "NNRCEither"%string
    | Case_aux c "NNRCGroupBy"%string].

  Global Instance nnrc_eqdec : EqDec nnrc eq.

  Context (h:brand_relation_t).

  Fixpoint nnrc_core_eval (env:bindings) (e:nnrc) : option data :=
    match e with
      | NNRCVar x ⇒
        lookup equiv_dec env x
      | NNRCConst d ⇒
         Some (normalize_data h d)
      | NNRCBinop bop e1 e2 ⇒
        olift2 (fun d1 d2 ⇒ fun_of_binop h bop d1 d2) (nnrc_core_eval env e1) (nnrc_core_eval env e2)
      | NNRCUnop uop e1 ⇒
        olift (fun d1 ⇒ fun_of_unaryop h uop d1) (nnrc_core_eval env e1)
      | NNRCLet x e1 e2 ⇒
        match nnrc_core_eval env e1 with
        | Some d ⇒ nnrc_core_eval ((x,d)::env) e2
        | _ ⇒ None
        end
      | NNRCFor x e1 e2 ⇒
        match nnrc_core_eval env e1 with
        | Some (dcoll c1) ⇒
          let inner_eval d1 :=
              let env' := (x,d1) :: env in nnrc_core_eval env' e2
          in
          lift dcoll (rmap inner_eval c1)
        | _ ⇒ None
        end
      | NNRCIf e1 e2 e3 ⇒
        let aux_if d :=
            match d with
            | dbool b ⇒
              if b then nnrc_core_eval env e2 else nnrc_core_eval env e3
            | _ ⇒ None
            end
        in olift aux_if (nnrc_core_eval env e1)
      | NNRCEither ed xl el xr er ⇒
        match nnrc_core_eval env ed with
        | Some (dleft dl) ⇒
          nnrc_core_eval ((xl,dl)::env) el
        | Some (dright dr) ⇒
          nnrc_core_eval ((xr,dr)::env) er
        | _ ⇒ None
        end
      | NNRCGroupBy _ _ _ ⇒ None
    end.

  Global Instance nnrc_core_eval_lookup_equiv_prop :
    Proper (lookup_equiv ==> eq ==> eq) nnrc_core_eval.

  Section core.
    Definition nnrc_core : Set := {e:nnrc | nnrcIsCore e}.

    Definition nnrc_core_to_nnrc (e:nnrc_core) : nnrc :=
      proj1_sig e.

    Definition lift_nnrc_core {A} (f:nnrc → A) (e:nnrc_core) : A :=
      f (proj1_sig e).

  End core.

End cNNRC.