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:
-
Language: NNRC (Named Nested Relational Calculus)
-
Based on: "Polymorphic type inference for the named nested
relational calculus." Jan Van den Bussche, and Stijn
Vansummeren. ACM Transactions on Computational Logic (TOCL) 9.1
(2007): 3.
-
translating to NNRC: NRAEnv, cNNRC
-
translating from NNRC: cNNRC, NNRCMR, DNNRC, Java, JavaScript
.
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.
intros; reflexivity.
Qed.
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.
induction e; intros; simpl in *; auto.
repeat (split; auto).
Qed.
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.
intros.
induction e; simpl in *.
- reflexivity.
- reflexivity.
- elim H; intros.
rewrite IHe1; auto; rewrite IHe2; auto.
- rewrite IHe; auto.
- elim H; intros.
rewrite IHe1; auto; rewrite IHe2; auto.
- elim H; intros.
rewrite IHe1; auto; rewrite IHe2; auto.
- elim H; intros.
elim H1; intros.
rewrite IHe1; auto; rewrite IHe2; auto; rewrite IHe3; auto.
- elim H; intros.
elim H1; intros.
rewrite IHe1; auto; rewrite IHe2; auto; rewrite IHe3; auto.
- contradiction.
Qed.
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.
induction e;
simpl;
try reflexivity.
-
rewrite IHe1;
rewrite IHe2;
reflexivity.
-
assumption.
-
rewrite IHe1;
rewrite IHe2;
reflexivity.
-
rewrite IHe1;
rewrite IHe2;
reflexivity.
-
rewrite IHe1;
rewrite IHe2;
rewrite IHe3;
reflexivity.
-
rewrite IHe1;
rewrite IHe2;
rewrite IHe3;
reflexivity.
-
rewrite app_nil_r.
assumption.
Qed.
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.
induction e;
simpl;
unfold not in *;
intros.
-
auto.
-
auto.
-
intuition.
rewrite in_app_iff in H.
rewrite in_app_iff.
elim H;
intros;
auto.
-
intuition.
-
intuition.
rewrite in_app_iff in H0.
rewrite in_app_iff.
elim H0;
intros;
auto.
-
intuition.
rewrite in_app_iff in H0.
rewrite in_app_iff.
elim H0;
intros;
auto.
-
rewrite in_app_iff in H.
rewrite in_app_iff in H.
rewrite in_app_iff.
rewrite in_app_iff.
elim H;
clear H;
intros;
auto.
elim H;
clear H;
intros;
auto.
-
rewrite in_app_iff in H.
rewrite in_app_iff in H.
rewrite in_app_iff.
rewrite in_app_iff.
elim H;
clear H;
intros;
auto.
elim H;
clear H;
intros;
auto.
elim H;
clear H;
intros;
auto.
elim H;
clear H;
intros;
auto.
right.
right.
auto.
right.
right.
auto.
-
specialize (
IHe H).
right.
rewrite in_app_iff.
auto.
Qed.
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.
induction e1;
simpl;
try reflexivity.
-
destruct (
equiv_dec v v1);
reflexivity.
-
rewrite IHe1_1;
rewrite IHe1_2;
reflexivity.
-
rewrite IHe1;
reflexivity.
-
rewrite IHe1_1.
destruct (
equiv_dec v v1);
try reflexivity.
rewrite IHe1_2;
reflexivity.
-
rewrite IHe1_1.
destruct (
equiv_dec v v1);
try reflexivity.
rewrite IHe1_2;
reflexivity.
-
rewrite IHe1_1;
rewrite IHe1_2;
rewrite IHe1_3;
reflexivity.
-
rewrite IHe1_1.
destruct (
equiv_dec v v1);
destruct (
equiv_dec v0 v1);
try reflexivity.
rewrite IHe1_3;
reflexivity.
rewrite IHe1_2;
reflexivity.
rewrite IHe1_2;
rewrite IHe1_3;
reflexivity.
-
unfold nnrc_group_by.
rewrite IHe1.
unfold var in *.
destruct (
equiv_dec "$
group0"%
string v1);
try congruence;
try reflexivity.
destruct (
equiv_dec "$
group1"%
string v1);
try congruence;
try reflexivity.
destruct (
equiv_dec "$
group2"%
string v1);
try congruence;
try reflexivity.
destruct (
equiv_dec "$
group3"%
string v1);
try congruence;
try reflexivity.
destruct (
equiv_dec "$
group2"%
string v1);
try congruence;
try reflexivity.
destruct (
equiv_dec "$
group3"%
string v1);
try congruence;
try reflexivity.
Qed.
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.