Qcert.Compiler.QLib.QLambdaNRA

Module QLambdaNRA(runtime:CompilerRuntime).

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

  Definition expr : Set
    := LambdaNRA.lnra.
  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.data → expr
    := LambdaNRA.LNRAConst.
  Definition ltable : 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 lamapconcat : lambda_expr → expr → expr
    := LambdaNRA.LNRAMapConcat.
  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 latableify : expr → expr
    := LambdaNRASugar.la_tableify.

End QLambdaNRA.