Qcert.Translation.LambdaNRAtoNRAEnv

Section LambdaNRAtoNRAEnv.


  Context {fruntime:foreign_runtime}.

  Fixpoint nraenv_of_lnra (op:lnra) : nraenv :=
    match op with
    | LNRAVar x ⇒ NRAEnvUnop (ADot x) NRAEnvEnv
    | LNRATable x ⇒ NRAEnvGetConstant x
    | LNRAConst d ⇒ NRAEnvConst d
    | LNRABinop b op1 op2 ⇒ NRAEnvBinop b (nraenv_of_lnra op1) (nraenv_of_lnra op2)
    | LNRAUnop u op1 ⇒ NRAEnvUnop u (nraenv_of_lnra op1)
    | LNRAMap lop1 op2 ⇒ NRAEnvMap (nraenv_of_lnra_lambda lop1) (nraenv_of_lnra op2)
    | LNRAMapConcat lop1 op2 ⇒ NRAEnvMapConcat (nraenv_of_lnra_lambda lop1) (nraenv_of_lnra op2)
    | LNRAProduct op1 op2 ⇒ NRAEnvProduct (nraenv_of_lnra op1) (nraenv_of_lnra op2)
    | LNRAFilter lop1 op2 ⇒ NRAEnvSelect (nraenv_of_lnra_lambda lop1) (nraenv_of_lnra op2)
    end
  with nraenv_of_lnra_lambda (lop:lnra_lambda) : nraenv :=
    match lop with
    | LNRALambda x op ⇒
      NRAEnvAppEnv (nraenv_of_lnra op) (NRAEnvBinop AConcat NRAEnvEnv (NRAEnvUnop (ARec x) NRAEnvID))
    end.

  Context (h:brand_relation_t).
  Context (global_env:list (string×data)).

  Theorem nraenv_of_lnra_lambda_correct :
    ∀ env:bindings, ∀ lop:lnra_lambda, ∀ d:data,
      lnra_lambda_eval h global_env env lop d =
      nraenv_eval h global_env
                  (nraenv_of_lnra_lambda lop) (drec env) d.

  Definition eval_nraenv_q (Qe:nraenv) (input:data) : option data :=
    nraenv_eval h global_env Qe (drec nil) input.

  Theorem eval_nraenv_q_correct (Q:lnra → lnra) (input:data) :
    eval_q h global_env Q input = eval_nraenv_q (nraenv_of_lnra_lambda (q_to_lambda Q)) input.

End LambdaNRAtoNRAEnv.