Qcert.Compiler.Model.CompilerModel

Module Type CompilerModel.
  Axiom compiler_basic_model : basic_model.
  Axiom compiler_model_foreign_to_java : foreign_to_java.
  Axiom compiler_model_foreign_to_javascript : foreign_to_javascript.
  Axiom compiler_model_foreign_to_scala : foreign_to_scala.
  Axiom compiler_model_foreign_to_JSON : foreign_to_JSON.
  Axiom compiler_model_foreign_type_to_JSON : foreign_type_to_JSON.
  Axiom compiler_model_foreign_reduce_op : foreign_reduce_op.
  Axiom compiler_model_foreign_to_reduce_op : foreign_to_reduce_op.
  Axiom compiler_model_foreign_to_spark : foreign_to_spark.
  Axiom compiler_model_foreign_cloudant : foreign_cloudant.
  Axiom compiler_model_foreign_to_cloudant : foreign_to_cloudant.
  Axiom compiler_model_nraenv_optimizer_logger : optimizer_logger string nraenv.
  Axiom compiler_model_nnrc_optimizer_logger : optimizer_logger string nnrc.
  Axiom compiler_model_dnnrc_optimizer_logger : ∀ {br:brand_relation}, optimizer_logger string (dnnrc (type_annotation unit) dataset).
  Axiom compiler_model_foreign_data_typing : foreign_data_typing.
End CompilerModel.

Module CompilerModelRuntime(model:CompilerModel) <: CompilerRuntime.
  Definition compiler_foreign_type : foreign_type
    := basic_model_foreign_type.
  Definition compiler_foreign_runtime : foreign_runtime
    := basic_model_runtime.
  Definition compiler_foreign_to_javascript : foreign_to_javascript
    := model.compiler_model_foreign_to_javascript.
  Definition compiler_foreign_to_scala : foreign_to_scala
    := model.compiler_model_foreign_to_scala.
  Definition compiler_foreign_to_java : foreign_to_java
    := model.compiler_model_foreign_to_java.
  Definition compiler_foreign_to_JSON : foreign_to_JSON
    := model.compiler_model_foreign_to_JSON.
  Definition compiler_foreign_type_to_JSON : foreign_type_to_JSON
    := model.compiler_model_foreign_type_to_JSON.
  Definition compiler_foreign_reduce_op : foreign_reduce_op
    := model.compiler_model_foreign_reduce_op.
  Definition compiler_foreign_to_reduce_op : foreign_to_reduce_op
    := model.compiler_model_foreign_to_reduce_op.
  Definition compiler_foreign_to_spark : foreign_to_spark
    := model.compiler_model_foreign_to_spark.
  Definition compiler_foreign_cloudant : foreign_cloudant
    := model.compiler_model_foreign_cloudant.
  Definition compiler_foreign_to_cloudant : foreign_to_cloudant
    := model.compiler_model_foreign_to_cloudant.
  Definition compiler_nraenv_optimizer_logger : optimizer_logger string nraenv
    := model.compiler_model_nraenv_optimizer_logger.
  Definition compiler_nnrc_optimizer_logger : optimizer_logger string nnrc
    := model.compiler_model_nnrc_optimizer_logger.
  Definition compiler_dnnrc_optimizer_logger {br:brand_relation}: optimizer_logger string (dnnrc (type_annotation unit) dataset)
    := model.compiler_model_dnnrc_optimizer_logger.
  Definition compiler_foreign_data_typing : foreign_data_typing
    := model.compiler_model_foreign_data_typing.
End CompilerModelRuntime.

Module Type CompilerForeignType.
  Axiom compiler_foreign_type : foreign_type.
End CompilerForeignType.
Module Type CompilerBrandModel(ftype:CompilerForeignType).
  Axiom compiler_brand_model : brand_model.
End CompilerBrandModel.