Module ErgoSpec.Backend.ForeignErgo

Require Import String.
Require Import Qcert.Utils.Closure.
Require Import Qcert.Data.DataSystem.
Require Import Qcert.NNRC.Lang.NNRC.

Section ForeignErgo.
  Context {fruntime:foreign_runtime}.

  Definition backend_closure : Set := @closure nnrc unit.
  Definition backend_lookup_table : Set := string -> option backend_closure.

  Class foreign_ergo : Type
    := mk_foreign_ergo {
           foreign_table : backend_lookup_table
         }.

End ForeignErgo.