Module Qcert.Compiler.Lib.QLambdaNRA

Require Import CompilerRuntime.
Require String.
Require QData.
Require QOperators.
Require LambdaNRA.
Require LambdaNRASugar.

Module QLambdaNRA(runtime:CompilerRuntime).

  Module Data := QData.QData runtime.
  Module Ops := QOperators.QOperators runtime.

  Definition expr : Set
    := LambdaNRA.lambda_nra.
  Definition lambda_expr : Set
    := LambdaNRA.lnra_lambda.
  Definition t : Set
    := expr.
  Definition var : Set
    := String.string.

  Definition lalambda : var -> expr -> lambda_expr
    := LambdaNRA.LNRALambda.
  Definition lavar : var -> expr
    := LambdaNRA.LNRAVar.
  Definition laconst : Data.qdata -> expr
    := LambdaNRA.LNRAConst.
  Definition latable : String.string -> expr
    := LambdaNRA.LNRATable.
  Definition labinop : Ops.Binary.op -> expr -> expr -> expr
    := LambdaNRA.LNRABinop.
  Definition launop : Ops.Unary.op -> expr -> expr
    := LambdaNRA.LNRAUnop.
  Definition lamap : lambda_expr -> expr -> expr
    := LambdaNRA.LNRAMap.
  Definition lafilter : lambda_expr -> expr -> expr
    := LambdaNRA.LNRAFilter.
  Definition lamapproduct : lambda_expr -> expr -> expr
    := LambdaNRA.LNRAMapProduct.
  Definition laproduct : expr -> expr -> expr
    := LambdaNRA.LNRAProduct.

  Definition ladot : String.string -> expr -> expr
    := LambdaNRASugar.LNRADot.
  Definition laarrow : String.string -> expr -> expr
    := LambdaNRASugar.LNRAArrow.
  Definition lastruct : list (String.string * expr) -> expr
    := LambdaNRASugar.LNRAStruct.
  Definition laflatmap : lambda_expr -> expr -> expr
    := LambdaNRASugar.LNRAFlatMap.

  Definition latableify : expr -> expr
    := LambdaNRASugar.la_tableify.

End QLambdaNRA.