Module Qcert.Compiler.Lib.QUtil

Require Import DataRuntime.
Require Import CompilerRuntime.
Require Import NNRCMRRuntime.
Require Import tDNNRCRuntime.
Require Import ImpRuntime.
Require Import CompEnv.
Require Import Version.

Module QUtil(runtime:CompilerRuntime).

  Definition mr_reduce_empty := mr_reduce_empty.

  Definition type_annotation {br:brand_relation} (A:Set): Set
    := tDNNRC.type_annotation A.

  Definition ta_base {br:brand_relation} (A:Set) (ta:type_annotation A)
    := tDNNRC.ta_base ta.
  Definition ta_inferred {br:brand_relation} (A:Set) (ta:type_annotation A)
    := tDNNRC.ta_inferred ta .
  Definition ta_required {br:brand_relation} (A:Set) (ta:type_annotation A)
    := tDNNRC.ta_required ta.

  Definition validate_lifted_success := validate_lifted_success.
  Definition validate_data := validate_data.

  Definition mkDistWorld env := mkDistWorld env.

  Definition qcert_version := qcert_version.

  Section results.
    Definition qerror {fdata:foreign_data} : Set := DataResult.qerror.
    Definition qresult {fdata:foreign_data} (A:Set) := DataResult.qresult A.

    Definition qsuccess {fdata:foreign_data} (A:Set) : A -> qresult A := DataResult.qsuccess.
    Definition qfailure {fdata:foreign_data} (A:Set) : qerror -> qresult A := DataResult.qfailure.
  End results.

  Definition string_of_ejson_runtime_op := EJsonRuntimeOperators.string_of_ejson_runtime_op.
  Definition ejson_runtime_op_of_string := EJsonRuntimeOperators.ejson_runtime_op_of_string.

End QUtil.