Module Qcert.Compiler.Lib.QDriver

Require Import String.
Require Import DataSystem.
Require Import NRARuntime.
Require Import NRAEnvRuntime.
Require Import NNRCRuntime.
Require Import NNRSRuntime.
Require Import NNRCMRRuntime.
Require Import DNNRCRuntime.
Require Import tDNNRCRuntime.
Require Import CAMPRuntime.
Require Import OQLRuntime.
Require Import CompEnv.
Require Import CompLang.
Require Import CompConfig.
Require Import CompDriver.
Require Import CompCustom.
Require Import CompilerRuntime.
Require Import JSON.

Module QDriver(runtime:CompilerRuntime).

  Local Open Scope list_scope.

  Section QD.
    Definition optim_config := optim_config.
    Definition optim_config_default : optim_config
      := optim_config_default.
    Definition optim_config_to_json : optim_config -> json
      := optim_config_to_json.
    Definition json_to_optim_config : json -> string + optim_config
      := json_to_optim_config.

    Definition optim_config_list_to_json : json
      := optim_config_list_to_json.
    
    Definition optim_config_default_to_json : json
      := optim_config_default_to_json.
    
    Context {bm:brand_model}.
    Context {ftyping: foreign_typing}.

    Definition driver : Set := driver.
    Definition compile : driver -> query -> list query := compile.

    Definition language_of_driver : driver -> language := language_of_driver.
    Definition name_of_driver : driver -> string := name_of_driver.


    Definition driver_config := driver_config.
    Definition driver_of_path : driver_config -> list language -> driver :=
      driver_of_path.

    Definition get_path_from_source_target : language -> language -> list language :=
      get_path_from_source_target.


    Definition optim_config_list := optim_config_list.


    Definition constants_config := constants_config.
    Definition mk_constant_config := mkConstantConfig.
    
    Definition get_driver_from_source_target
      : driver_config -> language -> language -> driver
      := get_driver_from_source_target.


    Definition default_dv_config := default_dv_config.
    Definition compile_from_source_target :
      driver_config -> language -> language -> query -> query
      := compile_from_source_target.

    Definition compile_nraenv_to_imp_data_verified :
      driver_config -> query -> query
      := compile_nraenv_to_imp_data_verified.

    Definition compile_nraenv_to_imp_ejson_verified :
      driver_config -> query -> query
      := compile_nraenv_to_imp_ejson_verified.

    Definition compile_nnrc_to_javascript_ast :
      driver_config -> query -> query
      := compile_nnrc_to_javascript_ast.

    Definition camp_rule_to_nraenv_optim : camp_rule -> nraenv := camp_rule_to_nraenv_optim.
    Definition camp_rule_to_nnrc_optim : camp_rule -> nnrc := camp_rule_to_nnrc_optim.

    Definition nraenv_optim_to_nnrc_optim : nraenv -> nnrc := nraenv_optim_to_nnrc_optim.
    Definition nraenv_optim_to_nnrc_optim_to_dnnrc :
      vdbindings -> nraenv -> dnnrc
      := nraenv_optim_to_nnrc_optim_to_dnnrc.
    Definition nraenv_optim_to_nnrc_optim_to_nnrcmr_optim : vdbindings -> nraenv -> nnrcmr
      := nraenv_optim_to_nnrc_optim_to_nnrcmr_optim.

    Definition nraenv_core_to_nraenv : nraenv_core -> nraenv := nraenv_core_to_nraenv.
    
    Definition camp_rule_to_nraenv_to_nnrc_optim : camp_rule -> nnrc := camp_rule_to_nraenv_to_nnrc_optim.
    Definition camp_rule_to_nraenv_to_nnrc_optim_to_dnnrc :
      vdbindings -> camp_rule -> dnnrc := camp_rule_to_nraenv_to_nnrc_optim_to_dnnrc.
    Definition camp_rule_to_nnrcmr : vdbindings -> camp_rule -> nnrcmr := camp_rule_to_nnrcmr.

  End QD.
End QDriver.