Qcert.Compiler.QLib.QDriver

Module QDriver(runtime:CompilerRuntime).



  Section QD.
    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 fix_driver : driver → query → driver := fix_driver.

    Definition get_path_from_source_target : language → language → list language :=
      get_path_from_source_target.


    Definition optim_config_list := optim_config_list.
    Definition optim_config_default := optim_config_default.


    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 rule_to_nraenv_optim : rule → nraenv := rule_to_nraenv_optim.
    Definition rule_to_nnrc_optim : rule → nnrc := 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_dataset
      := 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 cldmr_to_cloudant : string → list (string×string) → cldmr → cloudant := cldmr_to_cloudant.
    Definition nnrcmr_to_cldmr : list (string×string) → nnrcmr → cldmr := nnrcmr_to_cldmr.
    Definition nnrcmr_prepared_to_cldmr : list (string×string) → nnrcmr → cldmr := nnrcmr_prepared_to_cldmr.

    Definition nraenv_core_to_nraenv : nraenv_core → nraenv := nraenv_core_to_nraenv.

    Definition rule_to_nraenv_to_nnrc_optim : rule → nnrc := rule_to_nraenv_to_nnrc_optim.
    Definition rule_to_nraenv_to_nnrc_optim_to_dnnrc :
      vdbindings → rule → dnnrc_dataset := rule_to_nraenv_to_nnrc_optim_to_dnnrc.
    Definition rule_to_nraenv_to_nnrc_optim_to_javascript :
      rule → string := rule_to_nraenv_to_nnrc_optim_to_javascript.
    Definition rule_to_nnrcmr : vdbindings → rule → nnrcmr := rule_to_nnrcmr.
    Definition rule_to_cldmr : list (string×string) → vdbindings → rule → cldmr := rule_to_cldmr.

  End QD.
End QDriver.