Module NNRC


NNRC is the named nested relational calculus. It serves as an intermediate language to facilitate code generation for non-functional targets.

NNRC is a thin layer over the core language cNNRC. As cNNRC, NNRC is evaluated within a local environment.

Additional operators in NNRC can be easily expressed in terms of the core cNNRC, but are useful for optimization purposes. The main such operator is group-by.

Summary:

Section NNRC.

  Require Import String.
  Require Import List.
  Require Import Arith.
  Require Import EquivDec.
  Require Import Morphisms.
  Require Import Arith Max.

  Require Import Bool.

  Require Import Peano_dec.
  Require Import EquivDec Decidable.

  Require Import Utils BasicRuntime.
  Require Import cNNRCRuntime.

  Context {fruntime:foreign_runtime}.

Abstract Syntax

  
The full abstract syntax for NNRC is already defined in core cNNRC.

  Definition nnrc := nnrc.

Macros

  
All the additional operators are defined in terms of the core cNNRC.
  
  Section Macros.
    Context {h:brand_relation_t}.

The following macro defines group-by in terms of existing cNNRC expressions.

e groupby[g,keys] == LET $group0 := e IN { [ g: ♯flatten({ IF ($group3 = π[keys]) THEN {$group3} ELSE {} | $group3 ∈ $group0 }) ] | $group2 ∈ ♯distinct({ π[keys]($group1) | $group1 ∈ $group0 }) }

    Definition nnrc_group_by (g:string) (sl:list string) (e:nnrc) : nnrc :=
      let t0 := "$group0"%string in
      let t1 := "$group1"%string in
      let t2 := "$group2"%string in
      let t3 := "$group3"%string in
      NNRCLet
        t0 e
        (NNRCFor t2
                 (NNRCUnop ADistinct
                           (NNRCFor t1 (NNRCVar t0) (NNRCUnop (ARecProject sl) (NNRCVar t1))))
                 (NNRCBinop AConcat
                            (NNRCUnop (ARec g)
                                      (NNRCUnop AFlatten
                                                (NNRCFor t3 (NNRCVar t0)
                                                         (NNRCIf (NNRCBinop AEq
                                                                            (NNRCUnop (ARecProject sl)
                                                                                      (NNRCVar t3))
                                                                            (NNRCVar t2))
                                                                       (NNRCUnop AColl (NNRCVar t3))
                                                                       (NNRCConst (dcoll nil))))))
                            (NNRCVar t2))).

This definition is equivalent to a nested evaluation group by algorithm.
    
    Lemma nnrc_group_by_correct env
          (g:string) (sl:list string)
          (e:nnrc)
          (incoll outcoll:list data):
      nnrc_core_eval h env e = Some (dcoll incoll) ->
      group_by_nested_eval_table g sl incoll = Some outcoll ->
      nnrc_core_eval h env (nnrc_group_by g sl e) = Some (dcoll outcoll).
Proof.

  End Macros.

Evaluation Semantics


  Section Semantics.
    Context {h:brand_relation_t}.

    Fixpoint nnrc_ext_to_nnrc (e:nnrc) : nnrc :=
      match e with
      | NNRCVar v => NNRCVar v
      | NNRCConst d => NNRCConst d
      | NNRCBinop b e1 e2 =>
        NNRCBinop b (nnrc_ext_to_nnrc e1) (nnrc_ext_to_nnrc e2)
      | NNRCUnop u e1 =>
        NNRCUnop u (nnrc_ext_to_nnrc e1)
      | NNRCLet v e1 e2 =>
        NNRCLet v (nnrc_ext_to_nnrc e1) (nnrc_ext_to_nnrc e2)
      | NNRCFor v e1 e2 =>
        NNRCFor v (nnrc_ext_to_nnrc e1) (nnrc_ext_to_nnrc e2)
      | NNRCIf e1 e2 e3 =>
        NNRCIf (nnrc_ext_to_nnrc e1) (nnrc_ext_to_nnrc e2) (nnrc_ext_to_nnrc e3)
      | NNRCEither e1 v2 e2 v3 e3 =>
        NNRCEither (nnrc_ext_to_nnrc e1) v2 (nnrc_ext_to_nnrc e2) v3 (nnrc_ext_to_nnrc e3)
      | NNRCGroupBy g sl e1 =>
        nnrc_group_by g sl (nnrc_ext_to_nnrc e1)
      end.

    Definition nnrc_ext_eval (env:bindings) (e:nnrc) : option data :=
      nnrc_core_eval h env (nnrc_ext_to_nnrc e).
      
    Remark nnrc_ext_to_nnrc_eq (e:nnrc):
      forall env,
        nnrc_ext_eval env e = nnrc_core_eval h env (nnrc_ext_to_nnrc e).
Proof.

Since we rely on cNNRC abstract syntax for the whole NNRC, it is important to check that translating to the core does not reuse the additional operations only present in NNRC.
    
    Lemma nnrc_ext_to_nnrc_is_core (e:nnrc) :
      nnrcIsCore (nnrc_ext_to_nnrc e).
Proof.

The following function effectively returns an abstract syntax tree with the right type for cNNRC.
    
    Program Definition nnrc_to_nnrc_core (e:nnrc) : nnrc_core :=
      nnrc_ext_to_nnrc e.
Next Obligation.

Additional properties of the translation from NNRC to cNNRC.
    
    Lemma core_nnrc_to_nnrc_ext_id (e:nnrc) :
      nnrcIsCore e ->
      (nnrc_ext_to_nnrc e) = e.
Proof.
    
    Lemma core_nnrc_to_nnrc_ext_idempotent (e1 e2:nnrc) :
      e1 = nnrc_ext_to_nnrc e2 ->
      nnrc_ext_to_nnrc e1 = e1.
Proof.

    Corollary core_nnrc_to_nnrc_ext_idempotent_corr (e:nnrc) :
      nnrc_ext_to_nnrc (nnrc_ext_to_nnrc e) = (nnrc_ext_to_nnrc e).
Proof.

    Remark nnrc_to_nnrc_ext_eq (e:nnrc):
      nnrcIsCore e ->
      forall env,
        nnrc_core_eval h env e = nnrc_ext_eval env e.
Proof.
    
we are only sensitive to the environment up to lookup
    Global Instance nnrc_ext_eval_lookup_equiv_prop :
      Proper (lookup_equiv ==> eq ==> eq) nnrc_ext_eval.
Proof.
    
  End Semantics.

Additional Properties


Most of the following properties are useful for shadowing and variable substitution on the full NNRC.
  
  Section Properties.
    Context {h:brand_relation_t}.
    Require Import cNNRCShadow.
    
    Lemma nnrc_ext_to_nnrc_free_vars_same e:
      nnrc_free_vars e = nnrc_free_vars (nnrc_ext_to_nnrc e).
Proof.

    Lemma nnrc_ext_to_nnrc_bound_vars_impl x e:
      In x (nnrc_bound_vars e) -> In x (nnrc_bound_vars (nnrc_ext_to_nnrc e)).
Proof.

    Lemma nnrc_ext_to_nnrc_bound_vars_impl_not x e:
      ~ In x (nnrc_bound_vars (nnrc_ext_to_nnrc e)) -> ~ In x (nnrc_bound_vars e).
Proof.

    Definition really_fresh_in_ext sep oldvar avoid e :=
      really_fresh_in sep oldvar avoid (nnrc_ext_to_nnrc e).
    
    Lemma really_fresh_from_free_ext sep old avoid (e:nnrc) :
      ~ In (really_fresh_in_ext sep old avoid e) (nnrc_free_vars (nnrc_ext_to_nnrc e)).
Proof.

    Lemma nnrc_ext_to_nnrc_subst_comm e1 v1 e2:
      nnrc_subst (nnrc_ext_to_nnrc e1) v1 (nnrc_ext_to_nnrc e2) =
      nnrc_ext_to_nnrc (nnrc_subst e1 v1 e2).
Proof.

    Lemma nnrc_ext_to_nnrc_rename_lazy_comm e v1 v2:
      nnrc_rename_lazy (nnrc_ext_to_nnrc e) v1 v2 =
      nnrc_ext_to_nnrc (nnrc_rename_lazy e v1 v2).
Proof.

Unshadow properties for the full NNRC.
    Lemma unshadow_over_nnrc_ext_idem sep renamer avoid e:
      (nnrc_ext_to_nnrc (unshadow sep renamer avoid (nnrc_ext_to_nnrc e))) =
      (unshadow sep renamer avoid (nnrc_ext_to_nnrc e)).
Proof.

    Lemma nnrc_ext_eval_cons_subst e env v x v' :
      ~ (In v' (nnrc_free_vars e)) ->
      ~ (In v' (nnrc_bound_vars e)) ->
      @nnrc_ext_eval h ((v',x)::env) (nnrc_subst e v (NNRCVar v')) =
      @nnrc_ext_eval h ((v,x)::env) e.
Proof.

  End Properties.

Toplevel

  
Top-level evaluation is used externally by the Q*cert compiler. It takes an NNRC expression and a global environment as input.

  Section Top.
    Context (h:brand_relation_t).
    Definition nnrc_eval_top (q:nnrc) (cenv:bindings) : option data :=
      @nnrc_ext_eval h (rec_sort (mkConstants cenv)) q.
  End Top.
  
End NNRC.