Section TNRA.
Require Import String.
Require Import List.
Require Import Compare_dec.
Require Import Program.
Require Import Utils BasicSystem.
Require Import NRA.
Typing for NRA
Section typ.
Context {
m:
basic_model}.
Context (τ
constants:
tbindings).
Inductive nra_type :
nra ->
rtype ->
rtype ->
Prop :=
|
ATID {τ} :
nra_type AID τ τ
|
ATConst {τ
in τ
out}
c :
data_type (
normalize_data brand_relation_brands c) τ
out ->
nra_type (
AConst c) τ
in τ
out
|
ATBinop {τ
in τ₁ τ₂ τ
out}
b op1 op2 :
binOp_type b τ₁ τ₂ τ
out ->
nra_type op1 τ
in τ₁ ->
nra_type op2 τ
in τ₂ ->
nra_type (
ABinop b op1 op2) τ
in τ
out
|
ATUnop {τ
in τ τ
out}
u op :
unaryOp_type u τ τ
out ->
nra_type op τ
in τ ->
nra_type (
AUnop u op) τ
in τ
out
|
ATMap {τ
in τ₁ τ₂}
op1 op2 :
nra_type op1 τ₁ τ₂ ->
nra_type op2 τ
in (
Coll τ₁) ->
nra_type (
AMap op1 op2) τ
in (
Coll τ₂)
|
ATMapConcat {τ
in τ₁ τ₂ τ₃}
op1 op2 pf1 pf2 pf3 :
nra_type op1 (
Rec Closed τ₁
pf1) (
Coll (
Rec Closed τ₂
pf2)) ->
nra_type op2 τ
in (
Coll (
Rec Closed τ₁
pf1)) ->
rec_concat_sort τ₁ τ₂ = τ₃ ->
nra_type (
AMapConcat op1 op2) τ
in (
Coll (
Rec Closed τ₃
pf3))
|
ATProduct {τ
in τ₁ τ₂ τ₃}
op1 op2 pf1 pf2 pf3 :
nra_type op1 τ
in (
Coll (
Rec Closed τ₁
pf1)) ->
nra_type op2 τ
in (
Coll (
Rec Closed τ₂
pf2)) ->
rec_concat_sort τ₁ τ₂ = τ₃ ->
nra_type (
AProduct op1 op2) τ
in (
Coll (
Rec Closed τ₃
pf3))
|
ATSelect {τ
in τ}
op1 op2 :
nra_type op1 τ
Bool ->
nra_type op2 τ
in (
Coll τ) ->
nra_type (
ASelect op1 op2) τ
in (
Coll τ)
|
ATDefault {τ
in τ}
op1 op2 :
nra_type op1 τ
in (
Coll τ) ->
nra_type op2 τ
in (
Coll τ) ->
nra_type (
ADefault op1 op2) τ
in (
Coll τ)
|
ATEither {τ
l τ
r τ
out}
opl opr :
nra_type opl τ
l τ
out ->
nra_type opr τ
r τ
out ->
nra_type (
AEither opl opr) (
Either τ
l τ
r) τ
out
|
ATEitherConcat {τ
in rll pfl rlr pfr rlo pfo lo ro}
op1 op2 pflo pfro :
nra_type op1 τ
in (
Either (
Rec Closed rll pfl) (
Rec Closed rlr pfr)) ->
nra_type op2 τ
in (
Rec Closed rlo pfo) ->
rec_concat_sort rll rlo =
lo ->
rec_concat_sort rlr rlo =
ro ->
nra_type (
AEitherConcat op1 op2) τ
in (
Either (
Rec Closed lo pflo) (
Rec Closed ro pfro))
|
ATApp {τ
in τ1 τ2}
op1 op2 :
nra_type op2 τ
in τ1 ->
nra_type op1 τ1 τ2 ->
nra_type (
AApp op1 op2) τ
in τ2
|
ATGetConstant {τ
in τ
out}
s :
tdot τ
constants s =
Some τ
out ->
nra_type (
AGetConstant s) τ
in τ
out.
End typ.
Notation "
Op ▷
A >=>
B ⊣
C" := (
nra_type C Op A B) (
at level 70) .
Type lemmas for individual algebraic expressions
Context {
m:
basic_model}.
Lemma rmap_typed {τ
c} {τ₁ τ₂ :
rtype}
c (
op1 :
nra) (
dl :
list data) :
(
bindings_type c τ
c) ->
(
Forall (
fun d :
data =>
data_type d τ₁)
dl) ->
(
op1 ▷ τ₁ >=> τ₂ ⊣ τ
c) ->
(
forall d :
data,
data_type d τ₁ ->
exists x :
data,
brand_relation_brands ⊢
op1 @ₐ
d ⊣
c =
Some x /\
data_type x τ₂) ->
exists x :
list data, (
rmap (
nra_eval brand_relation_brands c op1)
dl =
Some x) /\
data_type (
dcoll x) (
Coll τ₂).
Proof.
intros Hcenv.
intros.
induction dl;
simpl;
intros.
-
exists (@
nil data);
split; [
reflexivity|
apply dtcoll;
apply Forall_nil].
-
inversion H;
clear H.
elim (
H1 a H4);
intros.
elim H;
intros;
clear H.
rewrite H6;
clear H6.
specialize (
IHdl H5);
clear H5.
elim IHdl;
intros;
clear IHdl.
elim H;
intros;
clear H.
dependent induction H6.
rewrite H5.
exists (
x0 ::
x1).
split;
try reflexivity.
apply dtcoll.
apply Forall_cons;
try assumption.
assert (
r = τ₂)
by (
apply rtype_fequal;
assumption).
rewrite <-
H2;
assumption.
Qed.
Lemma recover_rec k d r τ
pf:
data_type d r ->
`
r =
Rec₀
k
(
map
(
fun x :
string * {τ₀ :
rtype₀ |
wf_rtype₀ τ₀ =
true} =>
(
fst x, ` (
snd x))) τ) ->
data_type d (
Rec k τ
pf).
Proof.
intros.
assert (
Rec k τ
pf =
r).
unfold Rec.
apply rtype_fequal.
rewrite H0.
reflexivity.
rewrite H1;
assumption.
Qed.
Lemma recover_rec_forall k l r τ
pf:
Forall (
fun d :
data =>
data_type d r)
l ->
`
r =
Rec₀
k
(
map
(
fun x :
string * {τ₀ :
rtype₀ |
wf_rtype₀ τ₀ =
true} =>
(
fst x, ` (
snd x))) τ) ->
Forall (
fun d :
data =>
data_type d (
Rec k τ
pf))
l.
Proof.
Lemma omap_concat_typed
(τ₁ τ₂ τ₃:
list (
string *
rtype)) (
dl2:
list data)
(
x :
list (
string *
data))
pf1 pf2 pf3:
(
forall x :
data,
In x dl2 ->
data_type x (
Rec Closed τ₂
pf2)) ->
rec_concat_sort τ₁ τ₂ = τ₃ ->
data_type (
drec x) (
Rec Closed τ₁
pf1) ->
(
exists y :
list data,
rmap (
fun x1 :
data =>
orecconcat (
drec x)
x1)
dl2
=
Some y /\
data_type (
dcoll y) (
Coll (
Rec Closed τ₃
pf3))).
Proof.
Lemma rproduct_typed {τ₁ τ₂ τ₃:
list (
string *
rtype)} (
dl dl0:
list data)
pf1 pf2 pf3:
Forall (
fun d :
data =>
data_type d (
Rec Closed τ₂
pf2))
dl0 ->
Forall (
fun d :
data =>
data_type d (
Rec Closed τ₁
pf1))
dl ->
rec_concat_sort τ₁ τ₂ = τ₃ ->
exists x :
list data, (
rproduct dl dl0 =
Some x) /\
data_type (
dcoll x) (
Coll (
Rec Closed τ₃
pf3)).
Proof.
Lemma data_type_concat l1 l2 τ:
data_type (
dcoll l1) (
Coll τ) ->
data_type (
dcoll l2) (
Coll τ) ->
data_type (
dcoll (
l1 ++
l2)) (
Coll τ).
Proof.
intros.
dependent induction H.
dependent induction H0.
apply dtcoll.
apply Forall_app;
rewrite Forall_forall in *;
assert (
r = τ)
by (
apply rtype_fequal;
assumption);
assert (
r0 = τ)
by (
apply rtype_fequal;
assumption);
rewrite H1 in H;
rewrite H2 in H0;
assumption.
Qed.
Lemma rmap_concat_typed {τ
c} {τ₁ τ₂ τ₃ :
list (
string *
rtype)} (
op1 :
nra)
c (
dl:
list data)
pf1 pf2 pf3:
bindings_type c τ
c ->
rec_concat_sort τ₁ τ₂ = τ₃ ->
Forall (
fun d :
data =>
data_type d (
Rec Closed τ₁
pf1))
dl ->
(
op1 ▷
Rec Closed τ₁
pf1 >=>
Coll (
Rec Closed τ₂
pf2) ⊣ τ
c) ->
(
forall d :
data,
data_type d (
Rec Closed τ₁
pf1) ->
exists x :
data,
brand_relation_brands ⊢
op1 @ₐ
d ⊣
c =
Some x /\
data_type x (
Coll (
Rec Closed τ₂
pf2))) ->
exists x :
list data, (
rmap_concat (
nra_eval brand_relation_brands c op1)
dl =
Some x) /\
data_type (
dcoll x) (
Coll (
Rec Closed τ₃
pf3)).
Proof.
Lemma rmap_concat_typed2 {τ
c} {τ₁ τ₂ τ₃ :
list (
string *
rtype)} τ
in (
op1 :
nra)
c y (
dl:
list data)
pf1 pf2 pf3:
bindings_type c τ
c ->
rec_concat_sort τ₁ τ₂ = τ₃ ->
Forall (
fun d :
data =>
data_type d (
Rec Closed τ₁
pf1))
dl ->
(
op1 ▷ τ
in >=>
Coll (
Rec Closed τ₂
pf2) ⊣ τ
c) ->
(
forall d :
data,
data_type d (
Rec Closed τ₁
pf1) ->
exists x :
data,
brand_relation_brands ⊢
op1 @ₐ
y ⊣
c =
Some x /\
data_type x (
Coll (
Rec Closed τ₂
pf2))) ->
exists x :
list data, (
rmap_concat (
fun z =>
brand_relation_brands ⊢
op1@ₐ
y ⊣
c)
dl =
Some x) /\
data_type (
dcoll x) (
Coll (
Rec Closed τ₃
pf3)).
Proof.
Main typing soundness theorem for the NRA
Theorem typed_nra_yields_typed_data {τ
c} {τ
in τ
out}
cenv (
d:
data) (
op:
nra):
bindings_type cenv τ
c ->
(
data_type d τ
in) -> (
op ▷ τ
in >=> τ
out ⊣ τ
c) ->
(
exists x,
brand_relation_brands ⊢
op @ₐ
d ⊣
cenv =
Some x /\ (
data_type x τ
out)).
Proof.
intros Hcenv.
intros.
revert d H.
nra_cases (
dependent induction H0)
Case;
simpl;
intros.
-
Case "
AID"%
string.
exists d;
split; [
reflexivity|
assumption].
-
Case "
AConst"%
string.
exists (
RDataNorm.normalize_data brand_relation_brands c);
split;
try reflexivity.
assumption.
-
Case "
ABinop"%
string.
elim (
IHnra_type1 d H0);
elim (
IHnra_type2 d H0);
intros.
elim H1;
elim H2;
intros;
clear H1 H2.
rewrite H3;
simpl.
rewrite H5;
simpl.
apply (
typed_binop_yields_typed_data x0 x b H4 H6);
assumption.
-
Case "
AUnop"%
string.
elim (
IHnra_type d H1);
intros.
elim H2;
intros;
clear H2.
rewrite H3.
apply (
typed_unop_yields_typed_data x u H4);
assumption.
-
Case "
AMap"%
string.
elim (
IHnra_type2 d H);
intros;
clear H IHnra_type2.
elim H0;
intros;
clear H0.
rewrite H;
clear H.
invcs H1;
rtype_equalizer.
subst.
assert (
exists x :
list data, (
rmap (
nra_eval brand_relation_brands cenv op1)
dl =
Some x)
/\
data_type (
dcoll x) (
Coll τ₂)).
apply (
rmap_typed cenv op1 dl Hcenv H2);
assumption.
destruct H as [? [
eqq dt]].
autorewrite with alg;
rewrite eqq.
exists (
dcoll x);
split; [
reflexivity|
assumption].
-
Case "
AMapConcat"%
string.
elim (
IHnra_type2 d H0);
intros;
clear IHnra_type2 H0.
elim H1;
intros;
clear H1.
destruct (
data_type_Col_inv H2);
subst.
inversion H2;
subst.
generalize (
recover_rec_forall _ _ _ _ pf1 H3 H1);
intros.
rewrite H0;
clear H0.
simpl.
assert (
exists x :
list data, (
rmap_concat (
nra_eval brand_relation_brands cenv op1)
x0 =
Some x) /\
data_type (
dcoll x) (
Coll (
Rec Closed (
rec_concat_sort τ₁ τ₂)
pf3))).
apply (
rmap_concat_typed op1 cenv x0 pf1 pf2 pf3 Hcenv);
try assumption;
try reflexivity.
elim H0;
intros;
clear H0.
elim H4;
intros;
clear H4.
autorewrite with alg;
rewrite H0.
simpl.
exists (
dcoll x);
split; [
reflexivity|
assumption].
-
Case "
AProduct"%
string.
elim (
IHnra_type1 d H0);
intros;
clear IHnra_type1.
elim H1;
intros;
clear H1.
rewrite H2;
clear H2.
invcs H3.
assert (
exists x :
list data, (
rmap_concat (
fun _ :
data =>
brand_relation_brands ⊢
op2 @ₐ
d ⊣
cenv)
dl =
Some x) /\
data_type (
dcoll x) (
Coll (
Rec Closed (
rec_concat_sort τ₁ τ₂)
pf3))).
apply (
rmap_concat_typed2 τ
in op2 cenv d dl pf1 pf2 pf3 Hcenv);
try assumption;
try reflexivity.
apply (
recover_rec_forall _ _ _ _ pf1 H4);
trivial.
destruct (
IHnra_type2 d H0)
as [? [
eqq dt]];
intros.
rewrite eqq;
clear eqq.
exists x;
split; [
reflexivity|
assumption].
destruct H as [? [
eqq dt]].
simpl;
rewrite eqq;
exists (
dcoll x);
simpl.
split; [
reflexivity|
assumption].
-
Case "
ASelect"%
string.
elim (
IHnra_type2 d H);
intros;
clear IHnra_type2.
elim H0;
intros;
clear H0.
rewrite H1;
clear H1 H0_0.
invcs H2;
rtype_equalizer.
subst.
assert (
exists c2,
(
lift_filter
(
fun x' :
data =>
match brand_relation_brands ⊢
op1 @ₐ
x' ⊣
cenv with
|
Some (
dbool b) =>
Some b
|
_ =>
None
end)
dl) =
Some c2 /\
Forall (
fun d :
data =>
data_type d τ)
c2).
+
induction dl.
*
exists (@
nil data).
split.
reflexivity.
apply Forall_nil.
*
rewrite Forall_forall in *;
intros.
simpl in H3.
assert (
forall x :
data,
In x dl ->
data_type x τ)
by intuition.
assert (
data_type a τ)
by (
apply (
H3 a);
left;
reflexivity).
destruct (
IHnra_type1 a H1)
as [? [
eqq dt]];
intros.
simpl.
rewrite eqq.
dtype_inverter.
destruct (
IHdl H0)
as [? [
eqq2 dt2]].
rewrite eqq2.
{
destruct x0.
-
eexists;
split;
try reflexivity.
eauto.
-
eexists;
split;
try reflexivity.
eauto.
}
+
simpl.
destruct H0 as [? [
eqq dt]].
rewrite eqq.
simpl.
eexists;
split;
try reflexivity.
constructor;
trivial.
-
Case "
ADefault"%
string.
elim (
IHnra_type1 d H);
elim (
IHnra_type2 d H);
intros.
elim H0;
elim H1;
intros;
clear H0 H1 H.
rewrite H2.
rewrite H4.
clear H2 H4.
simpl.
invcs H3.
invcs H5.
rtype_equalizer.
subst.
destruct dl.
+
eexists;
split;
try reflexivity.
constructor;
trivial.
+
eexists;
split;
try reflexivity.
constructor;
trivial.
-
Case "
AEither"%
string.
inversion H;
rtype_equalizer.
+
subst;
eauto.
+
subst;
eauto.
-
Case "
AEitherConcat"%
string.
destruct (
IHnra_type1 _ H1)
as [
x[
xeval xtyp]].
destruct (
IHnra_type2 _ H1)
as [
y[
yeval ytyp]].
rewrite xeval,
yeval.
destruct (
data_type_Rec_inv ytyp);
subst.
destruct (
data_type_Either_inv xtyp)
as [[
dd[?
ddtyp]]|[
dd[?
ddtyp]]];
subst.
+
destruct (
data_type_Rec_inv ddtyp);
subst.
eexists;
split;
try reflexivity.
econstructor.
eapply dtrec_rec_concat_sort;
eauto.
+
destruct (
data_type_Rec_inv ddtyp);
subst.
eexists;
split;
try reflexivity.
econstructor.
eapply dtrec_rec_concat_sort;
eauto.
-
Case "
AApp"%
string.
elim (
IHnra_type1 d H);
intros.
elim H0;
intros;
clear H0 H.
rewrite H1;
simpl.
elim (
IHnra_type2 x H2);
intros.
elim H;
intros;
clear H.
rewrite H0;
simpl.
exists x0;
split;[
reflexivity|
assumption].
-
Case "
AGetConstant"%
string.
unfold tdot in *.
unfold edot in *.
destruct (
Forall2_lookupr_some _ _ _ _ Hcenv H)
as [? [
eqq1 eqq2]].
rewrite eqq1.
eauto.
Qed.
Corrolaries of the main type soudness theorem
Definition typed_nra_total {τ
c} {τ
in τ
out} (
op:
nra) (
HOpT:
op ▷ τ
in >=> τ
out ⊣ τ
c)
c (
d:
data)
(
dt_c:
bindings_type c τ
c) :
(
data_type d τ
in) -> {
x:
data |
data_type x τ
out }.
Proof.
Lemma typed_nra_total_eq_matches_eval {τ
c} {τ
in τ
out} (
op:
nra) (
HOpT:
op ▷ τ
in >=> τ
out ⊣ τ
c)
c (
d:
data)
(
dt_c:
bindings_type c τ
c)
(
pf:
data_type d τ
in) :
(
brand_relation_brands ⊢
op @ₐ
d ⊣
c) =
Some (
proj1_sig (
typed_nra_total op HOpT c d dt_c pf)).
Proof.
Definition tnra_eval {τ
c} {τ
in τ
out} (
op:
nra) (
HOpT:
op ▷ τ
in >=> τ
out ⊣ τ
c)
c (
d:
data) (
dt_c:
bindings_type c τ
c):
(
data_type d τ
in) ->
data.
Proof.
intros HdT.
destruct (
typed_nra_total op HOpT c d dt_c HdT).
exact x.
Defined.
End TNRA.
Notation "
Op ▷
A >=>
B ⊣
C" := (
nra_type C Op A B) (
at level 70).