Qcert.Translation.cNNRCtoCAMP
Auxiliary definitions and lemmas
Definition loop_var (n:string):string := append "loop$" n.
Lemma loop_var_inj x y : loop_var x = loop_var y → x = y.
Definition let_var (n:string):string := append "let$" n.
Lemma let_var_inj x y : let_var x = let_var y → x = y.
Fixpoint let_vars (p:pat) : list string :=
match p with
| pconst _ ⇒ nil
| punop uop p ⇒
match uop with
| ARec f ⇒ f::nil
| _ ⇒ nil
end ++ let_vars p
| pbinop bop p₁ p₂ ⇒ let_vars p₁ ++ let_vars p₂
| pmap p ⇒ let_vars p
| passert p ⇒ let_vars p
| porElse p₁ p₂ ⇒ let_vars p₁ ++ let_vars p₂
| pit ⇒ nil
| pletIt p₁ p₂ ⇒ let_vars p₁ ++ let_vars p₂
| pletEnv p₁ p₂ ⇒ let_vars p₁ ++ let_vars p₂
| penv ⇒ nil
| pUnbrand ⇒ nil
end.
Translation from NNRC to CAMP.
This assumes that there is no shadowing
Fixpoint nnrcToPat_ns (n:cNNRC.nnrc) : pat
:= match n with
| cNNRC.NNRCVar v ⇒ lookup (loop_var v)
| cNNRC.NNRCConst d ⇒ pconst d
| cNNRC.NNRCBinop op n1 n2 ⇒ pbinop op (nnrcToPat_ns n1) (nnrcToPat_ns n2)
| cNNRC.NNRCUnop op n1 ⇒ punop op (nnrcToPat_ns n1)
| cNNRC.NNRCLet v bind body ⇒
pletIt (nnrcToPat_ns bind)
(pletEnv (pvar (loop_var v))
(nnrcToPat_ns body))
| cNNRC.NNRCFor v iter body ⇒
pletIt (nnrcToPat_ns iter)
(mapall
(pletEnv (pvar (loop_var v))
(nnrcToPat_ns body)))
| cNNRC.NNRCIf c n1 n2 ⇒
let ctrans := (nnrcToPat_ns c) in
let n1trans := (nnrcToPat_ns n1) in
let n2trans := (nnrcToPat_ns n2) in
(porElse
(pand (pbinop AAnd ‵true ctrans) n1trans)
(pand (punop ANeg ctrans) n2trans))
| cNNRC.NNRCEither nd xl nl xr nr ⇒
pletIt (nnrcToPat_ns nd)
(porElse (pletIt pleft (pletEnv (pvar (loop_var xl)) (nnrcToPat_ns nl))) (pletIt pright (pletEnv (pvar (loop_var xr)) (nnrcToPat_ns nr))))
| cNNRC.NNRCGroupBy g sl n ⇒
pfail
end.
:= match n with
| cNNRC.NNRCVar v ⇒ lookup (loop_var v)
| cNNRC.NNRCConst d ⇒ pconst d
| cNNRC.NNRCBinop op n1 n2 ⇒ pbinop op (nnrcToPat_ns n1) (nnrcToPat_ns n2)
| cNNRC.NNRCUnop op n1 ⇒ punop op (nnrcToPat_ns n1)
| cNNRC.NNRCLet v bind body ⇒
pletIt (nnrcToPat_ns bind)
(pletEnv (pvar (loop_var v))
(nnrcToPat_ns body))
| cNNRC.NNRCFor v iter body ⇒
pletIt (nnrcToPat_ns iter)
(mapall
(pletEnv (pvar (loop_var v))
(nnrcToPat_ns body)))
| cNNRC.NNRCIf c n1 n2 ⇒
let ctrans := (nnrcToPat_ns c) in
let n1trans := (nnrcToPat_ns n1) in
let n2trans := (nnrcToPat_ns n2) in
(porElse
(pand (pbinop AAnd ‵true ctrans) n1trans)
(pand (punop ANeg ctrans) n2trans))
| cNNRC.NNRCEither nd xl nl xr nr ⇒
pletIt (nnrcToPat_ns nd)
(porElse (pletIt pleft (pletEnv (pvar (loop_var xl)) (nnrcToPat_ns nl))) (pletIt pright (pletEnv (pvar (loop_var xr)) (nnrcToPat_ns nr))))
| cNNRC.NNRCGroupBy g sl n ⇒
pfail
end.
Definition with shadowing
Additional auxiliary lemmas to reason about domains and environments
Definition nnrc_to_pat_env {A:Type} (env:list (string×A)) : list (string × A)
:= map (fun xy ⇒ (loop_var (fst xy), snd xy)) env.
Lemma env_lookup_edot {A} (env:list (string×A)) (v:string) :
NoDup (domain env) →
RAssoc.lookup equiv_dec env v =
edot (nnrc_to_pat_env env) (loop_var v).
Lemma compatible_nin v (env:list (string×data)) a :
¬ In v (domain env) → RCompat.compatible (nnrc_to_pat_env env) ((loop_var v, a) :: nil) = true.
Lemma nnrc_to_pat_nodup {A env} :
NoDup (@domain _ A env) → NoDup (domain (nnrc_to_pat_env env)).
Lemma compatible_drec_sort_nin v (env: bindings) a :
NoDup (domain env) →
¬ In v (domain env) →
RCompat.compatible (rec_sort (nnrc_to_pat_env env)) ((loop_var v, a) :: nil) = true.
Lemma nnrcToPat_data_indep h cenv d d' b n:
interp h cenv (nnrcToPat_ns n) b d = interp h cenv (nnrcToPat_ns n) b d'.
Lemma gather_successes_le {A B} (f:A→presult B) l a :
(gather_successes (map f l)) = Success a →
(RBag.bcount a) ≤
(RBag.bcount l).
Lemma gather_successes_not_recoverable {A:Type} (l:list (presult A)) :
gather_successes l ≠ RecoverableError.
Lemma bcount_false1 {A} (l1 l2: list A) :
(RBag.bcount l2 ≤ RBag.bcount l1)%nat →
Z.of_nat (S (RBag.bcount l1)) = Z.of_nat (RBag.bcount l2) →
False.
Lemma interp_mapall_cons h cenv p bind a l :
RSort.is_list_sorted ODT_lt_dec (domain bind) = true →
interp h cenv (mapall p) bind (dcoll (a::l)) =
match interp h cenv p bind a, (interp h cenv (mapall p) bind (dcoll l)) with
| Success x', Success (dcoll l') ⇒ Success (dcoll (x'::l'))
| RecoverableError, Success (dcoll l') ⇒ RecoverableError
| Success a, RecoverableError ⇒ RecoverableError
| RecoverableError, RecoverableError ⇒ RecoverableError
| TerminalError, _ ⇒ TerminalError
| _, TerminalError ⇒ TerminalError
| RecoverableError , Success _ ⇒ TerminalError
| Success _, Success _ ⇒ TerminalError
end.
Fixpoint prmapM {A:Type} (os:list (presult A)) : presult (list A)
:= match os with
| nil ⇒ Success nil
| (TerminalError)::xs ⇒ TerminalError
| (RecoverableError)::xs ⇒
match prmapM xs with
| TerminalError ⇒ TerminalError
| _ ⇒ RecoverableError
end
| (Success a)::xs ⇒ liftpr (cons a) (prmapM xs)
end.
Lemma interp_mapall h cenv p bind l :
RSort.is_list_sorted ODT_lt_dec (domain bind) = true →
interp h cenv (mapall p) bind (dcoll l) = liftpr dcoll (prmapM (map (interp h cenv p bind) l)).
Lemma interp_pletIt_eq h cenv p₁ p₂ bind d :
interp h cenv (pletIt p₁ p₂) bind d=
bindpr (interp h cenv p₁ bind d) (interp h cenv p₂ bind).
Maps the input/output(s) between NNRC and CAMP
Definition pr2op {A:Type} (pr:presult A) : option A
:= match pr with
| Success a ⇒ Some a
| _ ⇒ None
end.
Lemma pr2op_op2tpr {A:Type} (op:option A) :
pr2op (op2tpr op) = op.
Lemma pr2op_op2rpr {A:Type} (op:option A) :
pr2op (op2rpr op) = op.
Definition isRecoverableError {A:Type} (pr:presult A)
:= match pr with
| RecoverableError ⇒ true
| _ ⇒ false
end.
Lemma op2tpr_not_recoverable {A:Type} (op:option A) :
isRecoverableError (op2tpr op) = false.
Lemma isRecoverableError_liftpr {A B:Type} (f:A→B) (pr:presult A)
: isRecoverableError (liftpr f pr) = isRecoverableError pr.
our translation will never yield a recoverable error.
There are only two sources of recoverable errors in the pattern lanugage:
passert and pletEnv.
1) passert: this only used by the translation in two places:
(a) if statements and (b) for loops (inside of mapall).
1a) if statements use porElse to "catch" the recoverable error created by passert
1b) a recoverable error is thrown only if the size of the result is not the same as the size
of the original collection. But that only happens if the translation of the sub-pattern
resulted in a recoverable error, which (by induction) does not happen.
2) pletEnv: we use pletEnv to introduce loop variables for For, but we are careful that
any such variable is "free" with respect to the current environment (that is the point
of the shadow_free predicate), so merge_bindings always succeeds.
Lemma nnrcToPat_norecoverable_ns h cenv n env :
nnrcIsCore n →
shadow_free n = true →
NoDup (domain env) →
(∀ x, In x (domain env) → ¬ In x (nnrc_bound_vars n)) →
isRecoverableError (interp h cenv (nnrcToPat_ns n) (rec_sort (nnrc_to_pat_env env)) dunit) = false.
Lemma nnrcToPat_norecoverable_top_ns h cenv n :
nnrcIsCore n →
shadow_free n = true →
isRecoverableError (interp h cenv (nnrcToPat_ns n) nil dunit) = false.
Theorem nnrcToPat_norecoverable_top h cenv avoid n :
nnrcIsCore n →
isRecoverableError (interp h cenv (nnrcToPat avoid n) nil dunit) = false.
Lemma pr2op_liftpr {A B:Type} (f:A→B) (pr:presult A) :
pr2op (liftpr f pr) = lift f (pr2op pr).
Lemma in_loop_var_nnrc_to_pat_env {B} v (env:list (string×B)) :
In (loop_var v) (domain (nnrc_to_pat_env env)) ↔ In v (domain env).
nnrcIsCore n →
shadow_free n = true →
NoDup (domain env) →
(∀ x, In x (domain env) → ¬ In x (nnrc_bound_vars n)) →
isRecoverableError (interp h cenv (nnrcToPat_ns n) (rec_sort (nnrc_to_pat_env env)) dunit) = false.
Lemma nnrcToPat_norecoverable_top_ns h cenv n :
nnrcIsCore n →
shadow_free n = true →
isRecoverableError (interp h cenv (nnrcToPat_ns n) nil dunit) = false.
Theorem nnrcToPat_norecoverable_top h cenv avoid n :
nnrcIsCore n →
isRecoverableError (interp h cenv (nnrcToPat avoid n) nil dunit) = false.
Lemma pr2op_liftpr {A B:Type} (f:A→B) (pr:presult A) :
pr2op (liftpr f pr) = lift f (pr2op pr).
Lemma in_loop_var_nnrc_to_pat_env {B} v (env:list (string×B)) :
In (loop_var v) (domain (nnrc_to_pat_env env)) ↔ In v (domain env).
Note that since the translation never yields recoverable errors,
any errors are terminal, which nicely aligns with errors in NNRC (which are terminal)
Lemma nnrcToPat_sem_correct_ns h cenv n env :
nnrcIsCore n →
shadow_free n = true →
NoDup (domain env) →
(∀ x, In x (domain env) → ¬ In x (nnrc_bound_vars n)) →
cNNRC.nnrc_core_eval h env n = pr2op (interp h cenv (nnrcToPat_ns n) (rec_sort (nnrc_to_pat_env env)) dunit).
Lemma nnrcToPat_sem_correct_top_ns h cenv n :
nnrcIsCore n →
shadow_free n = true →
cNNRC.nnrc_core_eval h nil n = pr2op (interp h cenv (nnrcToPat_ns n) nil dunit).
Theorem nnrcToPat_sem_correct_top h cenv avoid n :
nnrcIsCore n →
cNNRC.nnrc_core_eval h nil n = pr2op (interp h cenv (nnrcToPat avoid n) nil dunit).
Section trans_let.
Section fresh.
Definition option_to_list {A:Type} (o:option A)
:= match o with
| Some x ⇒ x::nil
| None ⇒ nil
end.
Definition gather_opt_successes {A:Type} (os:list (option A)) : list A
:= flat_map option_to_list os.
Definition fresh_let_var (pre:string) (l:list string)
:= (fresh_var (append "let$" pre) l).
Lemma fresh_let_var_fresh pre (l:list string) :
¬ In (fresh_let_var pre l) l.
Lemma fresh_let_var_as_let (pre:string) (l:list string) :
fresh_let_var pre l = append "let$" (
let problems := filter (prefix (append "let$" pre)) l in
let problemEnds :=
map
(fun x : string ⇒
substring (String.length (append "let$" pre)) (String.length x - String.length (append "let$" pre)) x) problems in
(pre ++ find_fresh_string problemEnds))%string.
End fresh.
Definition fresh_bindings (vars:list string) (p:pat) :=
∀ x, In (let_var x) vars → ¬ In (let_var x) (let_vars p).
Instance fresh_bindings_equiv_proper :
Proper (equivlist ==> eq ==> iff) fresh_bindings.
Lemma fresh_bindings_pbinop l b p₁ p₂:
fresh_bindings l (pbinop b p₁ p₂) ↔
(fresh_bindings l p₁ ∧ fresh_bindings l p₂).
Lemma fresh_bindings_punop l u p:
fresh_bindings l (punop u p) ↔
(match u with
| ARec f ⇒ ∀ n, f = let_var n → ¬ In f l
| _ ⇒ True
end ∧ fresh_bindings l p).
Lemma fresh_bindings_pletIt l p₁ p₂ :
fresh_bindings l (pletIt p₁ p₂) ↔
(fresh_bindings l p₁ ∧ fresh_bindings l p₂).
Lemma fresh_bindings_pmap l p :
fresh_bindings l (pmap p) ↔
fresh_bindings l p.
Lemma fresh_bindings_mapall l p :
fresh_bindings l (mapall p) ↔
(fresh_bindings l p).
Lemma fresh_bindings_pletEnv l p₁ p₂ :
fresh_bindings l (pletEnv p₁ p₂) ↔
(fresh_bindings l p₁ ∧ fresh_bindings l p₂).
Lemma fresh_bindings_pvar l f :
fresh_bindings l (pvar (let_var f)) ↔
¬ In (let_var f) l.
Lemma fresh_bindings_porElse l p₁ p₂ :
fresh_bindings l (porElse p₁ p₂) ↔
(fresh_bindings l p₁ ∧ fresh_bindings l p₂).
Lemma fresh_bindings_passert l p :
fresh_bindings l (passert p) ↔
fresh_bindings l p.
Lemma fresh_bindings_pand l p₁ p₂ :
fresh_bindings l (pand p₁ p₂) ↔
(fresh_bindings l p₁ ∧ fresh_bindings l p₂).
Lemma fresh_bindings_plookup l f :
fresh_bindings l (lookup f) ↔ True.
Lemma fresh_bindings_domain_drec_sort {A} l p :
fresh_bindings (domain (@rec_sort _ _ A l)) p
↔ fresh_bindings (domain l) p.
Lemma fresh_bindings_app l₁ l₂ p :
fresh_bindings (l₁ ++ l₂) p
↔ (fresh_bindings l₁ p ∧
fresh_bindings l₂ p).
Lemma fresh_bindings_cons a l p :
fresh_bindings ((let_var a)::l) p
↔ (¬ In (let_var a) (let_vars p) ∧
fresh_bindings l p).
Lemma fresh_bindings_nil p :
fresh_bindings nil p ↔ True.
Definition mapall_let p :=
let freshVar := fresh_let_var "ma$" (let_vars p) in
((pletEnv (punop (ARec freshVar) (pmap p))
(pletEnv (punop ACount pit ≐ punop ACount (lookup freshVar))
(lookup freshVar))))%rule.
Fixpoint nnrcToPat_ns_let (n:cNNRC.nnrc) : pat
:= match n with
| cNNRC.NNRCVar v ⇒ lookup (loop_var v)
| cNNRC.NNRCConst d ⇒ pconst d
| cNNRC.NNRCBinop op n1 n2 ⇒ pbinop op (nnrcToPat_ns_let n1) (nnrcToPat_ns_let n2)
| cNNRC.NNRCUnop op n1 ⇒ punop op (nnrcToPat_ns_let n1)
| cNNRC.NNRCLet v bind body ⇒
pletIt (nnrcToPat_ns_let bind)
(pletEnv (pvar (loop_var v))
(nnrcToPat_ns_let body))
| cNNRC.NNRCFor v iter body ⇒
pletIt (nnrcToPat_ns_let iter)
(mapall_let
(pletEnv (pvar (loop_var v))
(nnrcToPat_ns_let body)))
| cNNRC.NNRCIf c n1 n2 ⇒
let ctrans := (nnrcToPat_ns_let c) in
let n1trans := (nnrcToPat_ns_let n1) in
let n2trans := (nnrcToPat_ns_let n2) in
let freshVar := fresh_let_var "if$" (let_vars ctrans ++ let_vars n1trans ++ let_vars n2trans) in
pletEnv (punop (ARec freshVar) ctrans)
(porElse
(pand (pbinop AAnd ‵true (lookup freshVar)) n1trans)
(pand (punop ANeg (lookup freshVar)) n2trans))
| cNNRC.NNRCEither nd xl nl xr nr ⇒
pletIt (nnrcToPat_ns_let nd)
(porElse (pletIt pleft (pletEnv (pvar (loop_var xl)) (nnrcToPat_ns_let nl))) (pletIt pright (pletEnv (pvar (loop_var xr)) (nnrcToPat_ns_let nr))))
| cNNRC.NNRCGroupBy g sl n ⇒
pfail
end.
Definition nnrcToPat_let avoid (n:cNNRC.nnrc) : pat
:= nnrcToPat_ns_let (unshadow_simpl avoid n).
Lemma loop_let_var_distinct x y :
loop_var x ≠ let_var y.
Instance In_equivlist_proper {A}:
Proper (eq ==> equivlist ==> iff) (@In A).
Lemma interp_nnrcToPat_ns_ignored_let_binding h cenv b x xv d n :
shadow_free n = true →
RSort.is_list_sorted ODT_lt_dec (domain b) = true →
fresh_bindings (domain b) (nnrcToPat_ns n) →
(∀ x, In x (domain b) → ¬ In x (map loop_var (nnrc_bound_vars n))) →
NoDup (domain b) →
¬ In (let_var x) (let_vars (nnrcToPat_ns n)) →
¬ In (let_var x) (domain b) →
(interp h cenv (nnrcToPat_ns n)
(rec_concat_sort b
((let_var x, xv)::nil)) d)
=
(interp h cenv (nnrcToPat_ns n)
(rec_sort b) d).
Lemma interp_mapall_let_cons h cenv p bind a l :
RSort.is_list_sorted ODT_lt_dec (domain bind) = true →
fresh_bindings (domain bind) (mapall_let p) →
NoDup (domain bind) →
interp h cenv (mapall_let p) bind (dcoll (a::l)) =
match interp h cenv p bind a, (interp h cenv (mapall_let p) bind (dcoll l)) with
| Success x', Success (dcoll l') ⇒ Success (dcoll (x'::l'))
| RecoverableError, Success (dcoll l') ⇒ RecoverableError
| Success a, RecoverableError ⇒ RecoverableError
| RecoverableError, RecoverableError ⇒ RecoverableError
| TerminalError , _ ⇒ TerminalError
| _, TerminalError ⇒ TerminalError
| RecoverableError, Success _ ⇒ TerminalError
| Success _, Success _ ⇒ TerminalError
end.
Lemma interp_mapall_let h cenv p bind l :
RSort.is_list_sorted ODT_lt_dec (domain bind) = true →
fresh_bindings (domain bind) (mapall_let p) →
NoDup (domain bind) →
interp h cenv (mapall_let p) bind (dcoll l) = liftpr dcoll (prmapM (map (interp h cenv p bind) l)).
Lemma interp_mapall_let_mapall h cenv p b d:
RSort.is_list_sorted ODT_lt_dec (domain b) = true →
fresh_bindings (domain b) (mapall_let p) →
NoDup (domain b) →
(interp h cenv (mapall_let p) b d) = (interp h cenv (mapall p) b d).
Lemma let_vars_let_to_naive x n :
In (let_var x) (let_vars (nnrcToPat_ns n)) →
In (let_var x) (let_vars (nnrcToPat_ns_let n)).
Lemma fresh_bindings_let_to_naive l n :
fresh_bindings l (nnrcToPat_ns_let n) →
fresh_bindings l (nnrcToPat_ns n).
Instance map_forall2_prop {A B} (f:B→B→Prop) (g:A→B) : Proper (Forall2 (fun x y ⇒ f (g x) (g y)) ==> (Forall2 f)) (map g).
Lemma nnrcToPat_ns_let_equiv h cenv n b d :
RSort.is_list_sorted ODT_lt_dec (domain b) = true →
fresh_bindings (domain b) (nnrcToPat_ns_let n) →
NoDup (domain b) →
shadow_free n = true →
(∀ x, In x (domain b) → ¬ In x (map loop_var (nnrc_bound_vars n))) →
interp h cenv (nnrcToPat_ns_let n) b d = interp h cenv (nnrcToPat_ns n) b d.
Lemma fresh_bindings_from_nnrc {A} e l :
fresh_bindings (domain (@nnrc_to_pat_env A e)) l.
nnrcIsCore n →
shadow_free n = true →
NoDup (domain env) →
(∀ x, In x (domain env) → ¬ In x (nnrc_bound_vars n)) →
cNNRC.nnrc_core_eval h env n = pr2op (interp h cenv (nnrcToPat_ns n) (rec_sort (nnrc_to_pat_env env)) dunit).
Lemma nnrcToPat_sem_correct_top_ns h cenv n :
nnrcIsCore n →
shadow_free n = true →
cNNRC.nnrc_core_eval h nil n = pr2op (interp h cenv (nnrcToPat_ns n) nil dunit).
Theorem nnrcToPat_sem_correct_top h cenv avoid n :
nnrcIsCore n →
cNNRC.nnrc_core_eval h nil n = pr2op (interp h cenv (nnrcToPat avoid n) nil dunit).
Section trans_let.
Section fresh.
Definition option_to_list {A:Type} (o:option A)
:= match o with
| Some x ⇒ x::nil
| None ⇒ nil
end.
Definition gather_opt_successes {A:Type} (os:list (option A)) : list A
:= flat_map option_to_list os.
Definition fresh_let_var (pre:string) (l:list string)
:= (fresh_var (append "let$" pre) l).
Lemma fresh_let_var_fresh pre (l:list string) :
¬ In (fresh_let_var pre l) l.
Lemma fresh_let_var_as_let (pre:string) (l:list string) :
fresh_let_var pre l = append "let$" (
let problems := filter (prefix (append "let$" pre)) l in
let problemEnds :=
map
(fun x : string ⇒
substring (String.length (append "let$" pre)) (String.length x - String.length (append "let$" pre)) x) problems in
(pre ++ find_fresh_string problemEnds))%string.
End fresh.
Definition fresh_bindings (vars:list string) (p:pat) :=
∀ x, In (let_var x) vars → ¬ In (let_var x) (let_vars p).
Instance fresh_bindings_equiv_proper :
Proper (equivlist ==> eq ==> iff) fresh_bindings.
Lemma fresh_bindings_pbinop l b p₁ p₂:
fresh_bindings l (pbinop b p₁ p₂) ↔
(fresh_bindings l p₁ ∧ fresh_bindings l p₂).
Lemma fresh_bindings_punop l u p:
fresh_bindings l (punop u p) ↔
(match u with
| ARec f ⇒ ∀ n, f = let_var n → ¬ In f l
| _ ⇒ True
end ∧ fresh_bindings l p).
Lemma fresh_bindings_pletIt l p₁ p₂ :
fresh_bindings l (pletIt p₁ p₂) ↔
(fresh_bindings l p₁ ∧ fresh_bindings l p₂).
Lemma fresh_bindings_pmap l p :
fresh_bindings l (pmap p) ↔
fresh_bindings l p.
Lemma fresh_bindings_mapall l p :
fresh_bindings l (mapall p) ↔
(fresh_bindings l p).
Lemma fresh_bindings_pletEnv l p₁ p₂ :
fresh_bindings l (pletEnv p₁ p₂) ↔
(fresh_bindings l p₁ ∧ fresh_bindings l p₂).
Lemma fresh_bindings_pvar l f :
fresh_bindings l (pvar (let_var f)) ↔
¬ In (let_var f) l.
Lemma fresh_bindings_porElse l p₁ p₂ :
fresh_bindings l (porElse p₁ p₂) ↔
(fresh_bindings l p₁ ∧ fresh_bindings l p₂).
Lemma fresh_bindings_passert l p :
fresh_bindings l (passert p) ↔
fresh_bindings l p.
Lemma fresh_bindings_pand l p₁ p₂ :
fresh_bindings l (pand p₁ p₂) ↔
(fresh_bindings l p₁ ∧ fresh_bindings l p₂).
Lemma fresh_bindings_plookup l f :
fresh_bindings l (lookup f) ↔ True.
Lemma fresh_bindings_domain_drec_sort {A} l p :
fresh_bindings (domain (@rec_sort _ _ A l)) p
↔ fresh_bindings (domain l) p.
Lemma fresh_bindings_app l₁ l₂ p :
fresh_bindings (l₁ ++ l₂) p
↔ (fresh_bindings l₁ p ∧
fresh_bindings l₂ p).
Lemma fresh_bindings_cons a l p :
fresh_bindings ((let_var a)::l) p
↔ (¬ In (let_var a) (let_vars p) ∧
fresh_bindings l p).
Lemma fresh_bindings_nil p :
fresh_bindings nil p ↔ True.
Definition mapall_let p :=
let freshVar := fresh_let_var "ma$" (let_vars p) in
((pletEnv (punop (ARec freshVar) (pmap p))
(pletEnv (punop ACount pit ≐ punop ACount (lookup freshVar))
(lookup freshVar))))%rule.
Fixpoint nnrcToPat_ns_let (n:cNNRC.nnrc) : pat
:= match n with
| cNNRC.NNRCVar v ⇒ lookup (loop_var v)
| cNNRC.NNRCConst d ⇒ pconst d
| cNNRC.NNRCBinop op n1 n2 ⇒ pbinop op (nnrcToPat_ns_let n1) (nnrcToPat_ns_let n2)
| cNNRC.NNRCUnop op n1 ⇒ punop op (nnrcToPat_ns_let n1)
| cNNRC.NNRCLet v bind body ⇒
pletIt (nnrcToPat_ns_let bind)
(pletEnv (pvar (loop_var v))
(nnrcToPat_ns_let body))
| cNNRC.NNRCFor v iter body ⇒
pletIt (nnrcToPat_ns_let iter)
(mapall_let
(pletEnv (pvar (loop_var v))
(nnrcToPat_ns_let body)))
| cNNRC.NNRCIf c n1 n2 ⇒
let ctrans := (nnrcToPat_ns_let c) in
let n1trans := (nnrcToPat_ns_let n1) in
let n2trans := (nnrcToPat_ns_let n2) in
let freshVar := fresh_let_var "if$" (let_vars ctrans ++ let_vars n1trans ++ let_vars n2trans) in
pletEnv (punop (ARec freshVar) ctrans)
(porElse
(pand (pbinop AAnd ‵true (lookup freshVar)) n1trans)
(pand (punop ANeg (lookup freshVar)) n2trans))
| cNNRC.NNRCEither nd xl nl xr nr ⇒
pletIt (nnrcToPat_ns_let nd)
(porElse (pletIt pleft (pletEnv (pvar (loop_var xl)) (nnrcToPat_ns_let nl))) (pletIt pright (pletEnv (pvar (loop_var xr)) (nnrcToPat_ns_let nr))))
| cNNRC.NNRCGroupBy g sl n ⇒
pfail
end.
Definition nnrcToPat_let avoid (n:cNNRC.nnrc) : pat
:= nnrcToPat_ns_let (unshadow_simpl avoid n).
Lemma loop_let_var_distinct x y :
loop_var x ≠ let_var y.
Instance In_equivlist_proper {A}:
Proper (eq ==> equivlist ==> iff) (@In A).
Lemma interp_nnrcToPat_ns_ignored_let_binding h cenv b x xv d n :
shadow_free n = true →
RSort.is_list_sorted ODT_lt_dec (domain b) = true →
fresh_bindings (domain b) (nnrcToPat_ns n) →
(∀ x, In x (domain b) → ¬ In x (map loop_var (nnrc_bound_vars n))) →
NoDup (domain b) →
¬ In (let_var x) (let_vars (nnrcToPat_ns n)) →
¬ In (let_var x) (domain b) →
(interp h cenv (nnrcToPat_ns n)
(rec_concat_sort b
((let_var x, xv)::nil)) d)
=
(interp h cenv (nnrcToPat_ns n)
(rec_sort b) d).
Lemma interp_mapall_let_cons h cenv p bind a l :
RSort.is_list_sorted ODT_lt_dec (domain bind) = true →
fresh_bindings (domain bind) (mapall_let p) →
NoDup (domain bind) →
interp h cenv (mapall_let p) bind (dcoll (a::l)) =
match interp h cenv p bind a, (interp h cenv (mapall_let p) bind (dcoll l)) with
| Success x', Success (dcoll l') ⇒ Success (dcoll (x'::l'))
| RecoverableError, Success (dcoll l') ⇒ RecoverableError
| Success a, RecoverableError ⇒ RecoverableError
| RecoverableError, RecoverableError ⇒ RecoverableError
| TerminalError , _ ⇒ TerminalError
| _, TerminalError ⇒ TerminalError
| RecoverableError, Success _ ⇒ TerminalError
| Success _, Success _ ⇒ TerminalError
end.
Lemma interp_mapall_let h cenv p bind l :
RSort.is_list_sorted ODT_lt_dec (domain bind) = true →
fresh_bindings (domain bind) (mapall_let p) →
NoDup (domain bind) →
interp h cenv (mapall_let p) bind (dcoll l) = liftpr dcoll (prmapM (map (interp h cenv p bind) l)).
Lemma interp_mapall_let_mapall h cenv p b d:
RSort.is_list_sorted ODT_lt_dec (domain b) = true →
fresh_bindings (domain b) (mapall_let p) →
NoDup (domain b) →
(interp h cenv (mapall_let p) b d) = (interp h cenv (mapall p) b d).
Lemma let_vars_let_to_naive x n :
In (let_var x) (let_vars (nnrcToPat_ns n)) →
In (let_var x) (let_vars (nnrcToPat_ns_let n)).
Lemma fresh_bindings_let_to_naive l n :
fresh_bindings l (nnrcToPat_ns_let n) →
fresh_bindings l (nnrcToPat_ns n).
Instance map_forall2_prop {A B} (f:B→B→Prop) (g:A→B) : Proper (Forall2 (fun x y ⇒ f (g x) (g y)) ==> (Forall2 f)) (map g).
Lemma nnrcToPat_ns_let_equiv h cenv n b d :
RSort.is_list_sorted ODT_lt_dec (domain b) = true →
fresh_bindings (domain b) (nnrcToPat_ns_let n) →
NoDup (domain b) →
shadow_free n = true →
(∀ x, In x (domain b) → ¬ In x (map loop_var (nnrc_bound_vars n))) →
interp h cenv (nnrcToPat_ns_let n) b d = interp h cenv (nnrcToPat_ns n) b d.
Lemma fresh_bindings_from_nnrc {A} e l :
fresh_bindings (domain (@nnrc_to_pat_env A e)) l.
Main lemmas for the correctness of the translation
Lemma nnrcToPat_let_ns_correct h cenv n env d :
nnrcIsCore n →
shadow_free n = true →
NoDup (domain env) →
(∀ x, In x (domain env) → ¬ In x (nnrc_bound_vars n)) →
(∀ x, In x (domain (nnrc_to_pat_env env)) → ¬ In x (map loop_var (nnrc_bound_vars n))) →
cNNRC.nnrc_core_eval h env n = pr2op (interp h cenv (nnrcToPat_ns_let n) (rec_sort (nnrc_to_pat_env env)) d).
Lemma nnrcToPat_let_correct_messy h cenv avoid n env d :
nnrcIsCore n →
NoDup (domain env) →
(∀ x, In x (domain env) → ¬ In x (nnrc_bound_vars (unshadow_simpl avoid n))) →
(∀ x, In x (domain (nnrc_to_pat_env env)) → ¬ In x (map loop_var (nnrc_bound_vars (unshadow_simpl avoid n)))) →
cNNRC.nnrc_core_eval h env n = pr2op (interp h cenv (nnrcToPat_let avoid n) (rec_sort (nnrc_to_pat_env env)) d).
This corresponds to Theorem 6.1
Theorem nnrcToPat_let_correct h cenv n env d :
nnrcIsCore n →
NoDup (domain env) →
cNNRC.nnrc_core_eval h env n
= pr2op (interp h cenv (nnrcToPat_let (domain env) n)
(rec_sort (nnrc_to_pat_env env)) d).
Lemma nnrcToPat_let_sem_correct_top_ns h cenv n :
nnrcIsCore n →
shadow_free n = true →
cNNRC.nnrc_core_eval h nil n = pr2op (interp h cenv (nnrcToPat_ns_let n) nil dunit).
Theorem nnrcToPat_let_sem_correct_top h cenv n :
nnrcIsCore n →
cNNRC.nnrc_core_eval h nil n = pr2op (interp h cenv (nnrcToPat_let nil n) nil dunit).
nnrcIsCore n →
NoDup (domain env) →
cNNRC.nnrc_core_eval h env n
= pr2op (interp h cenv (nnrcToPat_let (domain env) n)
(rec_sort (nnrc_to_pat_env env)) d).
Lemma nnrcToPat_let_sem_correct_top_ns h cenv n :
nnrcIsCore n →
shadow_free n = true →
cNNRC.nnrc_core_eval h nil n = pr2op (interp h cenv (nnrcToPat_ns_let n) nil dunit).
Theorem nnrcToPat_let_sem_correct_top h cenv n :
nnrcIsCore n →
cNNRC.nnrc_core_eval h nil n = pr2op (interp h cenv (nnrcToPat_let nil n) nil dunit).
Lemma and proof for the linear size of the translation
Lemma nnrc_subst_var_size n v v' :
nnrc_size (nnrc_subst n v (cNNRC.NNRCVar v')) = nnrc_size n.
Lemma nnrc_rename_lazy_size n v v' :
nnrc_size (nnrc_rename_lazy n v v') = nnrc_size n.
Lemma unshadow_size sep renamer avoid n :
nnrc_size (unshadow sep renamer avoid n) = nnrc_size n.
Lemma unshadow_simpl_size avoid n :
nnrc_size (unshadow_simpl avoid n) = nnrc_size n.
Lemma nnrcToPat_ns_let_size n :
pat_size (nnrcToPat_ns_let n) ≤ 25 × nnrc_size n.
Theorem nnrcToPat_let_size avoid n :
pat_size (nnrcToPat_let avoid n) ≤ 25 × nnrc_size n.
End trans_let.
End NNRCtoCAMP.