Qcert.Compiler.Model.TrivialModel

Program Instance trivial_foreign_data : foreign_data
  := mk_foreign_data Empty_set _ _ _ _ _ _.

Program Instance trivial_foreign_unary_op
        {fdata:foreign_data}:
  foreign_unary_op
  := mk_foreign_unary_op fdata Empty_set _ _ _ _.

  Program Instance trivial_foreign_binary_op
            {fdata:foreign_data}:
      foreign_binary_op
    := mk_foreign_binary_op fdata Empty_set _ _ _ _.

  Instance trivial_foreign_runtime :
    foreign_runtime
  := mk_foreign_runtime
       trivial_foreign_data
       trivial_foreign_unary_op
       trivial_foreign_binary_op.

  Program Instance trivial_foreign_type : foreign_type
    := mk_foreign_type Empty_set _ _ _ _ _ _ _.

  Program Instance trivial_foreign_data_typing :
    @foreign_data_typing trivial_foreign_data trivial_foreign_type
    := mk_foreign_data_typing
         trivial_foreign_data
         trivial_foreign_type
         _ _ _ _ _ _ _ _.

  Program Instance trivial_foreign_unary_op_typing
          {model:brand_model} :
    @foreign_unary_op_typing
      trivial_foreign_data
      trivial_foreign_unary_op
      trivial_foreign_type
      trivial_foreign_data_typing
      model
    := mk_foreign_unary_op_typing
         _ _ _ _ _ _
         _ _ _ _ _ _.

  Program Instance trivial_foreign_binary_op_typing
          {model:brand_model} :
    @foreign_binary_op_typing
      trivial_foreign_data
      trivial_foreign_binary_op
      trivial_foreign_type
      trivial_foreign_data_typing
      model
    := mk_foreign_binary_op_typing
         _ _ _ _ _ _
         _ _ _ _ _ _.

  Instance trivial_foreign_typing {model:brand_model}:
    @foreign_typing
      trivial_foreign_runtime
      trivial_foreign_type
      model
  := mk_foreign_typing
       trivial_foreign_runtime
       trivial_foreign_type
       model
       trivial_foreign_data_typing
       trivial_foreign_unary_op_typing
       trivial_foreign_binary_op_typing.

  Instance trivial_basic_model {model:brand_model} :
    basic_model
    := mk_basic_model
         trivial_foreign_runtime
         trivial_foreign_type
         model
         trivial_foreign_typing.

  Program Instance trivial_foreign_to_java :
    @foreign_to_java trivial_foreign_runtime
    := mk_foreign_to_java
         trivial_foreign_runtime
         _ _ _.

  Program Instance trivial_foreign_to_javascript :
    @foreign_to_javascript trivial_foreign_runtime
    := mk_foreign_to_javascript
         trivial_foreign_runtime
         _ _ _.

  Program Instance trivial_foreign_to_scala :
    @foreign_to_scala trivial_foreign_runtime trivial_foreign_type
    := mk_foreign_to_scala
         trivial_foreign_runtime trivial_foreign_type
         _ _.

  Program Instance trivial_foreign_to_JSON : foreign_to_JSON
    := mk_foreign_to_JSON trivial_foreign_data _ _.

  Program Instance trivial_foreign_type_to_JSON : foreign_type_to_JSON
    := mk_foreign_type_to_JSON trivial_foreign_type _ _.

  Program Instance trivial_foreign_reduce_op
            {fdata:foreign_data}:
      foreign_reduce_op
    := mk_foreign_reduce_op fdata Empty_set _ _ _ _.

  Program Instance trivial_foreign_to_reduce_op :
      foreign_to_reduce_op
    := mk_foreign_to_reduce_op trivial_foreign_runtime trivial_foreign_reduce_op _ _ _ _.

  Program Instance trivial_foreign_to_spark : foreign_to_spark
  := mk_foreign_to_spark trivial_foreign_runtime trivial_foreign_reduce_op _ _.

  Program Instance trivial_foreign_to_cloudant : foreign_to_cloudant
    := mk_foreign_to_cloudant trivial_foreign_runtime trivial_foreign_reduce_op _ _ _ _.

Instance trivial_foreign_cloudant : foreign_cloudant
  := mk_foreign_cloudant
       trivial_foreign_runtime
       ASum
       ANumMin
       ANumMax.


  Module TrivialRuntime <: CompilerRuntime.
    Definition compiler_foreign_type : foreign_type
      := trivial_foreign_type.
    Definition compiler_foreign_runtime : foreign_runtime
      := trivial_foreign_runtime.
    Definition compiler_foreign_to_java : foreign_to_java
      := trivial_foreign_to_java.
    Definition compiler_foreign_to_javascript : foreign_to_javascript
      := trivial_foreign_to_javascript.
    Definition compiler_foreign_to_scala : foreign_to_scala
      := trivial_foreign_to_scala.
    Definition compiler_foreign_to_JSON : foreign_to_JSON
      := trivial_foreign_to_JSON.
    Definition compiler_foreign_type_to_JSON : foreign_type_to_JSON
      := trivial_foreign_type_to_JSON.
    Definition compiler_foreign_reduce_op : foreign_reduce_op
      := trivial_foreign_reduce_op.
    Definition compiler_foreign_to_reduce_op : foreign_to_reduce_op
      := trivial_foreign_to_reduce_op.
    Definition compiler_foreign_to_spark : foreign_to_spark
      := trivial_foreign_to_spark.
    Definition compiler_foreign_cloudant : foreign_cloudant
      := trivial_foreign_cloudant.
    Definition compiler_foreign_to_cloudant : foreign_to_cloudant
      := trivial_foreign_to_cloudant.
    Definition compiler_nraenv_optimizer_logger : optimizer_logger string nraenv
      := silent_optimizer_logger string nraenv.
    Definition compiler_nnrc_optimizer_logger : optimizer_logger string nnrc
      := silent_optimizer_logger string nnrc.
    Definition compiler_dnnrc_optimizer_logger {br:brand_relation}: optimizer_logger string (dnnrc (type_annotation unit) dataset)
      := silent_optimizer_logger string (dnnrc (type_annotation unit) dataset).
    Definition compiler_foreign_data_typing : foreign_data_typing
      := trivial_foreign_data_typing.

  End TrivialRuntime.

  Module TrivialForeignType <: CompilerForeignType.
    Definition compiler_foreign_type : foreign_type
      := trivial_foreign_type.
  End TrivialForeignType.

  Module TrivialModel(bm:CompilerBrandModel(TrivialForeignType)) <: CompilerModel.
    Definition compiler_foreign_type : foreign_type
      := trivial_foreign_type.
    Definition compiler_basic_model : @basic_model
      := @trivial_basic_model bm.compiler_brand_model.
    Definition compiler_model_foreign_to_java : foreign_to_java
      := trivial_foreign_to_java.
    Definition compiler_model_foreign_to_javascript : foreign_to_javascript
      := trivial_foreign_to_javascript.
    Definition compiler_model_foreign_to_scala : foreign_to_scala
      := trivial_foreign_to_scala.
    Definition compiler_model_foreign_to_JSON : foreign_to_JSON
      := trivial_foreign_to_JSON.
    Definition compiler_model_foreign_type_to_JSON : foreign_type_to_JSON
      := trivial_foreign_type_to_JSON.
    Definition compiler_model_foreign_reduce_op : foreign_reduce_op
      := trivial_foreign_reduce_op.
    Definition compiler_model_foreign_to_reduce_op : foreign_to_reduce_op
      := trivial_foreign_to_reduce_op.
    Definition compiler_model_foreign_to_spark : foreign_to_spark
      := trivial_foreign_to_spark.
    Definition compiler_model_foreign_cloudant : foreign_cloudant
      := trivial_foreign_cloudant.
    Definition compiler_model_foreign_to_cloudant : foreign_to_cloudant
      := trivial_foreign_to_cloudant.
    Definition compiler_model_nraenv_optimizer_logger : optimizer_logger string nraenv
      := silent_optimizer_logger string nraenv.
    Definition compiler_model_nnrc_optimizer_logger : optimizer_logger string nnrc
      := silent_optimizer_logger string nnrc.
    Definition compiler_model_dnnrc_optimizer_logger {br:brand_relation}: optimizer_logger string (dnnrc (type_annotation unit) dataset)
      := silent_optimizer_logger string (dnnrc (type_annotation unit) dataset).
 Definition compiler_model_foreign_data_typing : foreign_data_typing
      := trivial_foreign_data_typing.
  End TrivialModel.