Qcert.Compiler.Driver.CompEval
Section CompEval.
Context {fruntime:foreign_runtime}. Context {fredop:foreign_reduce_op}. Context {fcloudant:foreign_cloudant}. Context {ft:foreign_type}. Context {bm:brand_model}.
Context {h:list(string×string)}.
Section EvalFunctions.
Definition eval_rule (q:rule) (cenv: list (string×data)) : option data :=
match interp h (rec_sort cenv) (rule_to_pattern q) nil dunit with
| Success l ⇒ Some (dcoll (l::nil))
| RecoverableError ⇒ Some (dcoll nil)
| TerminalError ⇒ None
end.
Definition eval_rule_debug (debug:bool) (q:rule) (cenv: list (string×data)) : string
:= let pp := rule_to_pattern q in
print_presult_debug pp
(interp_debug h
(rec_sort cenv)
debug nil pp nil dunit).
Definition eval_camp (q:camp) (cenv: list (string×data)) : option data
:= match interp h (rec_sort cenv) q nil dunit with
| Success l ⇒ Some (dcoll (l::nil))
| RecoverableError ⇒ Some (dcoll nil)
| TerminalError ⇒ None
end.
Definition eval_camp_debug (debug:bool) (q:camp) (cenv: list (string×data)) : string
:= print_presult_debug q
(interp_debug h
(rec_sort cenv)
debug nil q nil dunit).
Definition eval_oql (q:oql) (cenv: list (string×data)) : option data
:= oql_interp h (rec_sort cenv) q.
Definition eval_sql (q:sql) (cenv: list (string×data)) : option data
:= NRAEnv.nraenv_eval h (rec_sort cenv) (sql_to_nraenv q) (drec nil) dunit.
Definition eval_lambda_nra (q:lambda_nra) (cenv: list (string×data)) : option data
:= NRAEnv.nraenv_eval h (rec_sort cenv) (nraenv_of_lnra q) (drec nil) dunit.
Definition eval_nra (q:nra) (cenv: list (string×data)) : option data
:= nra_eval h q (drec (rec_sort cenv)).
Definition eval_nraenv_core (q:nraenv_core) (cenv: list (string×data)) : option data
:= cnraenv_eval h (rec_sort cenv) q (drec nil) dunit.
Definition eval_nraenv (q:nraenv) (cenv: list (string×data)) : option data
:= NRAEnv.nraenv_eval h (rec_sort cenv) q (drec nil) dunit.
Definition eval_nnrc_core (q:nnrc_core) (cenv: list (string×data)) : option data
:= lift_nnrc_core (@nnrc_core_eval _ h (mkConstants (rec_sort cenv))) q.
Definition eval_nnrc (q:nnrc) (cenv: list (string×data)) : option data
:= @nnrc_ext_eval _ h (mkConstants (rec_sort cenv)) q.
Definition eval_nnrcmr (q:nnrcmr) (cenv: list (string×data)) : option data
:= let cenv := mkConstants (rec_sort cenv) in
let loc_cenv := mkDistLocs cenv in
match load_init_env init_vinit loc_cenv cenv with
| Some mr_env ⇒ nnrcmr_eval h mr_env q
| None ⇒ None
end.
Definition eval_cldmr (q:cldmr) (cenv: list (string×data)) : option data
:= let cenv := mkConstants (rec_sort cenv) in
match cld_load_init_env init_vinit cenv with
| Some cenv ⇒ cld_mrl_eval h cenv q
| None ⇒ None
end.
Definition eval_dnnrc_dataset
(q:dnnrc_dataset) (cenv: list (string×data)) : option data :=
let cenv := mkConstants (rec_sort cenv) in
let loc_cenv := mkDistLocs (rec_sort cenv) in
match mkDistConstants loc_cenv cenv with
| Some cenv ⇒ lift localize_data (@dnnrc_eval _ _ _ h SparkIRPlug cenv q)
| None ⇒ None
end.
End EvalFunctions.
Section EvalDriver.
Definition eval_input : Set := list (string×ddata).
Definition lift_input (ev_in:eval_input) : list (string×data) :=
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 eval_query (q:query) (ev_in:eval_input) : eval_output :=
let cenv := lift_input ev_in in
match q with
| Q_rule q ⇒ lift_output (eval_rule q cenv)
| Q_camp q ⇒ lift_output (eval_camp q cenv)
| Q_oql q ⇒ lift_output (eval_oql q cenv)
| Q_sql q ⇒ lift_output (eval_sql q cenv)
| Q_lambda_nra q ⇒ lift_output (eval_lambda_nra q cenv)
| Q_nra q ⇒ lift_output (eval_nra q cenv)
| Q_nraenv_core q ⇒ lift_output (eval_nraenv_core q cenv)
| Q_nraenv q ⇒ lift_output (eval_nraenv q cenv)
| Q_nnrc_core q ⇒ lift_output (eval_nnrc_core q cenv)
| Q_nnrc q ⇒ lift_output (eval_nnrc q cenv)
| Q_nnrcmr q ⇒ lift_output (eval_nnrcmr q cenv)
| Q_cldmr q ⇒ lift_output (eval_cldmr q cenv)
| Q_dnnrc_dataset q ⇒ lift_output (eval_dnnrc_dataset q cenv)
| Q_dnnrc_typed_dataset _ ⇒ 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_rdd _ ⇒ Ev_out_unsupported ("No evaluation support for "++(name_of_language (language_of_query q)))
| Q_spark_dataset _ ⇒ Ev_out_unsupported ("No evaluation support for "++(name_of_language (language_of_query q)))
| Q_cloudant _ ⇒ Ev_out_unsupported ("No evaluation support for "++(name_of_language (language_of_query q)))
| 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 :=
let cenv := lift_input ev_in in
match q with
| Q_rule q ⇒ Ev_out_returned_debug (eval_rule_debug true q cenv)
| Q_camp q ⇒ Ev_out_returned_debug (eval_camp_debug true q cenv)
| 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_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_nnrcmr _ ⇒ Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
| Q_cldmr _ ⇒ Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
| Q_dnnrc_dataset _ ⇒ Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
| Q_dnnrc_typed_dataset _ ⇒ 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_rdd _ ⇒ Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
| Q_spark_dataset _ ⇒ Ev_out_unsupported ("No debug evaluation support for "++(name_of_language (language_of_query q)))
| Q_cloudant _ ⇒ 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.
End EvalDriver.
Section EvalWorld.
Definition eval_rule_world (r:rule) (world:list data) : option data :=
eval_rule r (mkWorld world).
Definition eval_rule_world_debug (debug:bool) (r:rule) (world:list data) : string :=
eval_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_sql_world (q:sql) (world:list data) : option data :=
eval_sql 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_nnrcmr_world (q:nnrcmr) (world:list data) : option data :=
eval_nnrcmr q (mkWorld world).
Definition eval_cldmr_world (q:cldmr) (world:list data) : option data :=
eval_cldmr q (mkWorld world).
Definition eval_dnnrc_dataset_world (q:dnnrc_dataset) (world:list data) : option data :=
eval_dnnrc_dataset q (mkWorld world).
End EvalWorld.
End CompEval.