Qcert.Translation.CAMPtoNRA
Section CAMPtoNRA.
Context {fruntime:foreign_runtime}.
Definition lift_failure d :=
match d with
| TerminalError ⇒ None
| RecoverableError ⇒ Some (dcoll nil)
| Success d' ⇒ Some (dcoll (d'::nil))
end.
Translation from CAMP to NRA
Fixpoint nra_of_pat (p:pat) : nra :=
match p with
| pconst d' ⇒ pat_match (AConst d')
| punop uop p₁ ⇒ AMap (AUnop uop AID) (nra_of_pat p₁)
| pbinop bop p₁ p₂ ⇒
AMap (ABinop bop (AUnop (ADot "a1") AID) (AUnop (ADot "a2") AID))
(AProduct (AMap (AUnop (ARec "a1") AID) (nra_of_pat p₁))
(AMap (AUnop (ARec "a2") AID) (nra_of_pat p₂)))
| pmap p₁ ⇒
pat_match
(AUnop AFlatten
(AMap
(nra_of_pat p₁)
(unnest_two
"a1"
"PDATA"
(AUnop AColl (pat_wrap_a1 (AUnop (ADot "PDATA") AID))))))
| passert p₁ ⇒ AMap (AConst (drec nil)) (ASelect AID (nra_of_pat p₁))
| porElse p₁ p₂ ⇒ ADefault (nra_of_pat p₁) (nra_of_pat p₂)
| pit ⇒ pat_match pat_data
| pletIt p₁ p₂ ⇒
AUnop AFlatten
(AMap (nra_of_pat p₂)
(unnest_two
"a1"
"PDATA"
(AUnop AColl
(pat_wrap_a1 (nra_of_pat p₁)))))
| pgetconstant s ⇒ pat_match (AUnop (ADot s) pat_const_env)
| penv ⇒ pat_match pat_bind
| pletEnv p₁ p₂ ⇒
AUnop AFlatten
(AMap
(nra_of_pat p₂)
(unnest_two
"PBIND1"
"PBIND"
(AMap (ABinop AConcat
(AUnop (ARec "PDATA") (AUnop (ADot "PDATA") AID))
(ABinop AConcat
(AUnop (ARec "PCONST") (AUnop (ADot "PCONST") AID))
(AUnop (ARec "PBIND1") (ABinop AMergeConcat
(AUnop (ADot "PBIND") AID)
(AUnop (ADot "PBIND1") AID)))))
(unnest_two
"a1"
"PBIND1"
(AUnop AColl
(ABinop AConcat
AID
(AUnop (ARec "a1") (nra_of_pat p₁))))))))
| pleft ⇒
AApp (AEither (pat_match AID) (pat_fail)) pat_data
| pright ⇒
AApp (AEither (pat_fail) (pat_match AID)) pat_data
end.
top level version sets up the appropriate input
(with an empty context)
Definition nra_of_pat_top c p :=
AUnop AFlatten
(AMap (nra_of_pat p)
(AUnop AColl
(pat_context (AConst (drec c)) (AConst (drec nil)) AID))).
Auxiliary lemmas -- all used inside pmap proof
Lemma rmap_lift (l:list data) :
rmap (fun x : data ⇒ Some (drec (("PDATA", x) :: nil))) l =
Some (map (fun x ⇒ (drec (("PDATA", x) :: nil))) l).
Lemma rmap_lift2 c bind (l l':list data):
(rmap
(fun x : data ⇒
match x with
| drec r1 ⇒
Some
(drec
(rec_concat_sort
(("PBIND", drec bind)
:: ("PCONST", c)
:: ("a1", dcoll l') :: nil) r1))
| _ ⇒ None
end)
(map (fun x : data ⇒ drec (("PDATA", x) :: nil)) l)) =
Some (map (fun x :data ⇒ (drec
(rec_concat_sort
(("PBIND", drec bind)
:: ("PCONST", c)
:: ("a1", dcoll l') :: nil) (("PDATA", x) :: nil)))) l).
Lemma rmap_lift3 c bind (l l':list data):
rmap
(fun x : data ⇒
match x with
| drec r ⇒ Some (drec (rremove r "a1"))
| _ ⇒ None
end)
(map
(fun x : data ⇒
drec
(rec_concat_sort
(("PBIND", drec bind)
:: ("PCONST", c)
:: ("a1", dcoll l') :: nil)
(("PDATA", x) :: nil))) l ++ nil)
=
Some (map (fun x : data ⇒
drec
(rec_concat_sort
(("PBIND", drec bind) :: ("PCONST", c) :: nil)
(("PDATA", x) :: nil))) l ++ nil).
Lemma rflatten_lift1 (l:option (list data)):
(olift
(fun d1 : data ⇒
lift_oncoll (fun l0 : list data ⇒ lift dcoll (rflatten l0)) d1)
(lift dcoll
(lift (fun t' : list data ⇒ dcoll nil :: t') l))) =
(olift
(fun d1 : data ⇒
lift_oncoll (fun l0 : list data ⇒ lift dcoll (rflatten l0)) d1)
(lift dcoll l)).
Theorem 4.2: lemma of translation correctness for patterns
Theorem pat_trans_correct {h:brand_relation_t} c p bind d:
lift_failure (interp h c p bind d) = nra_eval h (nra_of_pat p) (pat_context_data (drec (rec_sort c)) (drec bind) d).
Lemma pat_trans_yields_coll {h:brand_relation_t} p d d0:
nra_eval h (nra_of_pat p) d = Some d0 →
{x | d0 = dcoll x}.
Lemma pat_trans_top_pat_context {h:brand_relation_t} c p d:
Forall (fun x ⇒ data_normalized h (snd x)) c →
nra_eval h (nra_of_pat_top c p) d
= nra_eval h (nra_of_pat p) (pat_context_data (drec (rec_sort c)) (drec nil) d).
Lemma pat_trans_top_correct {h:brand_relation_t} c p d:
Forall (fun x ⇒ data_normalized h (snd x)) c →
lift_failure (interp h c p nil d) = nra_eval h (nra_of_pat_top c p) d.
Definition lift_pat_failure (d : option data) :=
match d with
| Some (dcoll nil) ⇒ RecoverableError
| Some (dcoll (l::nil)) ⇒ Success l
| _ ⇒ TerminalError
end.
Lemma pat_trans_correct_r {h:brand_relation_t} c p bind d:
interp h c p bind d =
lift_pat_failure (nra_eval h (nra_of_pat p) (pat_context_data (drec (rec_sort c)) (drec bind) d)).
Lemma pat_trans_top_correct_r {h:brand_relation_t} c p d:
Forall (fun x ⇒ data_normalized h (snd x)) c →
interp h c p nil d =
lift_pat_failure (nra_eval h (nra_of_pat_top c p) d).
Section size.
Proof showing linear size translation
Lemma pat_trans_size p :
nra_size (nra_of_pat p) ≤ 41 × pat_size p.
End size.
Section sugar.
Definition nra_of_pand (p1 p2:pat) : nra :=
nra_of_pat (pand p1 p2).
Definition nra_for_pand (q1 q2:nra) : nra :=
(♯flatten(χ⟨q2
⟩( unnest_two "PBIND1" "PBIND"
(χ⟨‵[| ("PDATA", (ID) · "PDATA")|]
⊕ (‵[| ("PCONST", (ID) · "PCONST")|]
⊕ ‵[| ("PBIND1", (ID) · "PBIND" ⊗ (ID) · "PBIND1")|])
⟩( unnest_two "a1" "PBIND1"
(‵{|ID
⊕ ‵[| ("a1",
χ⟨‵[||] ⟩( σ⟨ID ⟩( q1)))|]|}))))))%nra.
Lemma nra_of_pand_works (p1 p2:pat) :
nra_of_pat (pand p1 p2) = nra_for_pand (nra_of_pat p1) (nra_of_pat p2).
Definition nra_of_WW (p:pat) :=
nra_of_pat (WW p).
End sugar.
End CAMPtoNRA.
nra_size (nra_of_pat p) ≤ 41 × pat_size p.
End size.
Section sugar.
Definition nra_of_pand (p1 p2:pat) : nra :=
nra_of_pat (pand p1 p2).
Definition nra_for_pand (q1 q2:nra) : nra :=
(♯flatten(χ⟨q2
⟩( unnest_two "PBIND1" "PBIND"
(χ⟨‵[| ("PDATA", (ID) · "PDATA")|]
⊕ (‵[| ("PCONST", (ID) · "PCONST")|]
⊕ ‵[| ("PBIND1", (ID) · "PBIND" ⊗ (ID) · "PBIND1")|])
⟩( unnest_two "a1" "PBIND1"
(‵{|ID
⊕ ‵[| ("a1",
χ⟨‵[||] ⟩( σ⟨ID ⟩( q1)))|]|}))))))%nra.
Lemma nra_of_pand_works (p1 p2:pat) :
nra_of_pat (pand p1 p2) = nra_for_pand (nra_of_pat p1) (nra_of_pat p2).
Definition nra_of_WW (p:pat) :=
nra_of_pat (WW p).
End sugar.
End CAMPtoNRA.