Module Qcert.Driver.CompEval

Require Import String.
Require Import Equivalence.
Require Import EquivDec.

Require Import Utils.
Require Import DataSystem.

Require Import SQLRuntime.
Require Import OQLRuntime.
Require Import LambdaNRARuntime.
Require Import CAMPRuleRuntime.
Require Import TechRuleRuntime.
Require Import DesignerRuleRuntime.
Require Import NRARuntime.
Require Import NRAEnvRuntime.
Require Import NNRCRuntime.
Require Import NNRSRuntime.
Require Import NNRSimpRuntime.
Require Import ImpRuntime.
Require Import NNRCMRRuntime.
Require Import DNNRCRuntime.
Require Import tDNNRCRuntime.
Require Import CAMPRuntime.
Require Import JavaScriptAstRuntime.
Require Import JavaScriptRuntime.
Require Import JavaRuntime.
Require Import SparkDFRuntime.
Require Import WasmAst.
Require Import WasmBinary.

Require Import ForeignDataToEJson.
Require Import ForeignToReduceOps.
Require Import ForeignToSpark.

Require Import CompLang.
Require Import CompEnv.

Section CompEval.
  Local Open Scope list_scope.


  Context {fruntime:foreign_runtime}.
  Context {foreign_ejson_model:Set}.
  Context {fejson:foreign_ejson foreign_ejson_model}.
  Context {foreign_ejson_runtime_op : Set}.
  Context {ftejson:foreign_to_ejson foreign_ejson_model foreign_ejson_runtime_op}.
  Context {fredop:foreign_reduce_op}.
  Context {ft:foreign_type}.
  Context {bm:brand_model}.

  Definition h := brand_relation_brands.

  Section EvalFunctions.

    Definition eval_camp_rule (q:camp_rule) (cenv: bindings) : option data :=
      CAMPRule.camp_rule_eval_top h q cenv.
    Definition eval_camp_rule_debug (debug:bool) (q:camp_rule) (cenv: bindings) : string :=
      CAMPRule.camp_rule_eval_top_debug h debug q cenv.

    Definition eval_camp (q:camp) (cenv: bindings) : option data :=
      CAMP.camp_eval_top h q cenv.
    Definition eval_camp_debug (debug:bool) (q:camp) (cenv: bindings) : string :=
      CAMP.camp_eval_top_debug h debug q cenv.

    Definition eval_oql (q:oql) (cenv: bindings) : option data :=
      OQL.oql_eval_top h q cenv.

    Definition eval_lambda_nra (q:lambda_nra) (cenv: bindings) : option data :=
      LambdaNRA.lambda_nra_eval_top h q cenv.

    Definition eval_nra (q:nra) (cenv: bindings) : option data :=
      NRA.nra_eval_top h q cenv.

    Definition eval_nraenv_core (q:nraenv_core) (cenv: bindings) : option data :=
      cNRAEnv.nraenv_core_eval_top h q cenv.

    Definition eval_nraenv (q:nraenv) (cenv: bindings) : option data :=
      NRAEnv.nraenv_eval_top h q cenv.

    Definition eval_nnrc_core (q:nnrc_core) (cenv: bindings) : option data :=
      cNNRC.nnrc_core_eval_top h q cenv.

    Definition eval_nnrc (q:nnrc) (cenv: bindings) : option data :=
      NNRC.nnrc_eval_top h q cenv.

    Definition eval_nnrs_core (q:nnrs_core) (cenv: bindings) : option data :=
      NNRSEval.nnrs_core_eval_top h cenv q.

    Definition eval_nnrs (q:nnrs) (cenv: bindings) : option data :=
      NNRSEval.nnrs_eval_top h cenv q.

    Definition eval_nnrs_imp (q:nnrs_imp) (cenv: bindings) : option data :=
      NNRSimpEval.nnrs_imp_eval_top h cenv q.

    Definition eval_imp_data (q:imp_data) (cenv: bindings) : option data :=
      ImpDataEval.imp_data_eval_top h cenv q.

    Definition eval_imp_ejson (q:imp_ejson) (cenv: bindings) : option data :=
      ImpEJsonEval.imp_ejson_eval_top h cenv q.

    Definition eval_nnrcmr (q:nnrcmr) (dcenv: dbindings) : option data :=
      NNRCMR.nnrcmr_eval_top h init_vinit q dcenv.

    Definition eval_dnnrc (q:dnnrc) (cenv: dbindings) : option data :=
      DNNRC.dnnrc_eval_top h q cenv.

    Definition eval_dnnrc_typed (q:dnnrc_typed) (cenv: dbindings) : option data :=
      tDNNRC.dnnrc_typed_eval_top h q cenv.

    Definition eval_wasm_ast (q:wasm_ast) (cenv: bindings) : option data :=
      WasmAst.wasm_ast_eval_top cenv q.

    Definition eval_wasm (q:wasm) (cenv: bindings) : option data :=
      WasmBinary.wasm_eval_top cenv q.

  End EvalFunctions.

  Section EvalDriver.
    Definition eval_input : Set := dbindings.

    Definition lift_input (ev_in:eval_input) : bindings :=
      unlocalize_constants ev_in.

    Inductive eval_output : Set :=
    | Ev_out_unsupported : string -> eval_output
    | Ev_out_failed : eval_output
    | Ev_out_returned : data -> eval_output
    | Ev_out_returned_debug : string -> eval_output
    .

    Definition lift_output (result:option data) :=
      match result with
      | None => Ev_out_failed
      | Some d => Ev_out_returned d
      end.

    Definition query : Type := @query ft bm fruntime foreign_ejson_model foreign_ejson_runtime_op _.
    Definition eval_query (q:query) (ev_in:eval_input) : eval_output :=
      match q with
      | Q_camp_rule q => lift_output (eval_camp_rule q (lift_input ev_in))
      | Q_tech_rule _ => Ev_out_unsupported ("No evaluation support for "++(name_of_language (language_of_query q)))
      | Q_designer_rule _ => Ev_out_unsupported ("No evaluation support for "++(name_of_language (language_of_query q)))
      | Q_camp q => lift_output (eval_camp q (lift_input ev_in))
      | Q_oql q => lift_output (eval_oql q (lift_input ev_in))
      | Q_sql _ => Ev_out_unsupported ("No evaluation support for "++(name_of_language (language_of_query q)))
      | Q_sqlpp q => Ev_out_unsupported "SQL++ eval not yet implemented"
      | Q_lambda_nra q => lift_output (eval_lambda_nra q (lift_input ev_in))
      | Q_nra q => lift_output (eval_nra q (lift_input ev_in))
      | Q_nraenv_core q => lift_output (eval_nraenv_core q (lift_input ev_in))
      | Q_nraenv q => lift_output (eval_nraenv q (lift_input ev_in))
      | Q_nnrc_core q => lift_output (eval_nnrc_core q (lift_input ev_in))
      | Q_nnrc q => lift_output (eval_nnrc q (lift_input ev_in))
      | Q_nnrs_core q => lift_output (eval_nnrs_core q (lift_input ev_in))
      | Q_nnrs q => lift_output (eval_nnrs q (lift_input ev_in))
      | Q_nnrs_imp q => lift_output (eval_nnrs_imp q (lift_input ev_in))
      | Q_imp_data q => lift_output (eval_imp_data q (lift_input ev_in))
      | Q_imp_ejson q => lift_output (eval_imp_ejson q (lift_input ev_in))
      | Q_nnrcmr q => lift_output (eval_nnrcmr q ev_in)
      | Q_dnnrc q => lift_output (eval_dnnrc q ev_in)
      | Q_dnnrc_typed q => lift_output (eval_dnnrc_typed q ev_in)
      | Q_js_ast _ => Ev_out_unsupported ("No evaluation support for "++(name_of_language (language_of_query q)))
      | Q_javascript _ => Ev_out_unsupported ("No evaluation support for "++(name_of_language (language_of_query q)))
      | Q_java _ => Ev_out_unsupported ("No evaluation support for "++(name_of_language (language_of_query q)))
      | Q_spark_df _ => Ev_out_unsupported ("No evaluation support for "++(name_of_language (language_of_query q)))
      | Q_wasm_ast q => lift_output (eval_wasm_ast q (lift_input ev_in))
      | Q_wasm q => lift_output (eval_wasm q (lift_input ev_in))
      | Q_error err => Ev_out_unsupported ("No evaluation support for "++(name_of_language (language_of_query q)))
      end.

    Definition eval_query_debug (q:query) (ev_in:eval_input) : eval_output :=
      match q with
      | Q_camp_rule q => Ev_out_returned_debug (eval_camp_rule_debug true q (lift_input ev_in))
      | Q_tech_rule _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_designer_rule _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_camp q => Ev_out_returned_debug (eval_camp_debug true q (lift_input ev_in))
      | Q_oql _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_sql _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_sqlpp _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_lambda_nra _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_nra _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_nraenv_core _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_nraenv _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_nnrc_core _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_nnrc _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_nnrs_core _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_nnrs _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_nnrs_imp _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_imp_data _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_imp_ejson _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_nnrcmr _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_dnnrc _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_dnnrc_typed _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_js_ast _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_javascript _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_java _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_spark_df _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_wasm_ast _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_wasm _ => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      | Q_error err => Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
      end.

    Definition equal_outputs o1 o2 :=
      match (o1,o2) with
      | (Ev_out_unsupported _, Ev_out_unsupported _) => True
      | (Ev_out_failed,Ev_out_failed) => True
      | (Ev_out_returned d1, Ev_out_returned d2) => if data_eq_dec d1 d2 then True else False
      | (Ev_out_returned_debug _, Ev_out_returned_debug _) => True
      | (_,_) => False
      end.

    Global Instance equal_outputs_equiv : Equivalence equal_outputs.

    Global Instance equal_outputs_eqdec : EqDec eval_output equal_outputs.

  End EvalDriver.

  Section EvalWorld.
    Definition eval_camp_rule_world (r:camp_rule) (world:list data) : option data :=
      eval_camp_rule r (mkWorld world).
    Definition eval_camp_rule_world_debug (debug:bool) (r:camp_rule) (world:list data) : string :=
      eval_camp_rule_debug debug r (mkWorld world).

    Definition eval_camp_world (q:camp) (world:list data) : option data :=
      eval_camp q (mkWorld world).
    Definition eval_camp_world_debug (debug:bool) (q:camp) (world:list data) : string :=
      eval_camp_debug debug q (mkWorld world).

    Definition eval_oql_world (q:oql) (world:list data) : option data :=
      eval_oql q (mkWorld world).

    Definition eval_lambda_nra_world (q:lambda_nra) (world:list data) : option data :=
      eval_lambda_nra q (mkWorld world).

    Definition eval_nra_world (q:nra) (world:list data) : option data :=
      eval_nra q (mkWorld world).

    Definition eval_nraenv_core_world (q:nraenv_core) (world:list data) : option data :=
      eval_nraenv_core q (mkWorld world).

    Definition eval_nraenv_world (q:nraenv) (world:list data) : option data :=
      eval_nraenv q (mkWorld world).

    Definition eval_nnrc_core_world (q:nnrc_core) (world:list data) : option data :=
      eval_nnrc_core q (mkWorld world).

    Definition eval_nnrc_world (q:nnrc) (world:list data) : option data :=
      eval_nnrc q (mkWorld world).

    Definition eval_nnrs_core_world (q:nnrs_core) (world:list data) : option data :=
      eval_nnrs_core q (mkWorld world).

    Definition eval_nnrs_world (q:nnrs) (world:list data) : option data :=
      eval_nnrs q (mkWorld world).

    Definition eval_nnrs_imp_world (q:nnrs_imp) (world:list data) : option data :=
      eval_nnrs_imp q (mkWorld world).

    Definition eval_nnrcmr_world (q:nnrcmr) (world:list data) : option data :=
      eval_nnrcmr q (mkDistWorld world).

    Definition eval_dnnrc_world (q:dnnrc) (world:list data) : option data :=
      eval_dnnrc q (mkDistWorld world).

    Definition eval_dnnrc_typed_world (q:dnnrc) (world:list data) : option data :=
      eval_dnnrc q (mkDistWorld world).

  End EvalWorld.

  Section Util.
    Lemma lift_input_idem d:
      (lift_input (List.map (fun xy : string * data => (fst xy, Dlocal (snd xy))) d)) = d.
    
  End Util.
End CompEval.