Qcert.Translation.TOQLtoNRAEnv

Section TOQLtoNRAEnv.

  Context {m:basic_model}.

    Lemma nraenv_of_oql_expr_type_preserve_f τconstant τdefls pfd τenv pfe e τout:
      oql_expr_type (rec_concat_sort τ constant τ defls) τ env e τ out →
      nraenv_type τ constant (nraenv_of_oql_expr (domain τ defls) e) (Rec Closed τ defls pfd) (Rec Closed τ env pfe) τ out.

    Lemma nraenv_of_oql_query_program_type_preserve_f τconstant τdefls pfd τenv pfe oq τout:
      oql_query_program_type τ constant τ defls τ env oq τ out →
      nraenv_type τ constant (nraenv_of_oql_query_program (domain τ defls) oq) (Rec Closed τ defls pfd) (Rec Closed τ env pfe) τ out.

    Theorem nraenv_of_oql_type_preserve_f τconstant oq τout :
      oql_type τ constant oq τ out →
      ∀ τenv τdata,
      nraenv_type τ constant (nraenv_of_oql oq) τ env τ data τ out.

End TOQLtoNRAEnv.