Module ErgoSpec.Backend.ErgoBackend

Require Export Qcert.Utils.Utils.
Require Export Qcert.Common.TypingRuntime.

Require ErgoSpec.Backend.Model.ErgoEnhancedModel.
Require ErgoSpec.Backend.Model.ErgoBackendRuntime.
Require ErgoSpec.Backend.Lib.ECType.
Require ErgoSpec.Backend.Lib.EData.
Require ErgoSpec.Backend.Lib.EOperators.
Require ErgoSpec.Backend.Lib.ECodeGen.

Module ErgoEnhancedBackend := ErgoBackendRuntime.ErgoBackendRuntime <+ ErgoEnhancedModel.CompEnhanced.
Module ErgoData := EData.EData(ErgoEnhancedBackend).
Module ErgoOps := EOperators.EOperators(ErgoEnhancedBackend).
Module ErgoCodeGen := ECodeGen.ECodeGen(ErgoEnhancedBackend).
Module ErgoCTypes := ECType.ECType(ErgoEnhancedBackend).

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