Module ErgoSpec.Backend.QLib

Require Export Qcert.Utils.Utils.
Require Export ForeignModel.

Require ErgoSpec.Backend.Qcert.QcertModel.
Require ErgoSpec.Backend.Lib.QBackendRuntime.
Require ErgoSpec.Backend.Lib.QType.
Require ErgoSpec.Backend.Lib.QData.
Require ErgoSpec.Backend.Lib.QOps.
Require ErgoSpec.Backend.Lib.QCodeGen.

Module QcertBackend := QBackendRuntime.QBackendRuntime <+ QcertModel.CompEnhanced.
Module QcertData := QData.QData(QcertBackend).
Module QcertOps := QOps.QOps(QcertBackend).
Module QcertCodeGen := QCodeGen.QCodeGen(QcertBackend).
Module QcertType := QType.QType(QcertBackend).

Section Defs.
  Definition zip {A} {B} : list A -> list B -> option (list (A * B)) := zip.
  Definition ergo_data := QcertData.data.
  Definition ergoc_type {br} := @QcertType.ectype br.
End Defs.