Qcert.Compiler.QLib.QCAMP

Module QCAMP(runtime:CompilerRuntime).


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

  Definition expr : Set
    := CAMP.pat.
  Definition pat : Set
    := expr.
  Definition t : Set
    := expr.

  Definition pconst : Data.t → expr
    := CAMP.pconst.
  Definition punop : Ops.Unary.op → expr → expr
    := CAMP.punop.
  Definition pbinop : Ops.Binary.op → expr → expr → expr
    := CAMP.pbinop.
  Definition pmap : expr → expr
    := CAMP.pmap.
  Definition passert : expr → expr
    := CAMP.passert.
  Definition porelse : expr → expr → expr
    := CAMP.porElse.
  Definition pit : expr
    := CAMP.pit.
  Definition pletit : expr → expr → expr
    := CAMP.pletIt.
  Definition pgetconstant : String.string → expr
    := CAMP.pgetconstant.
  Definition penv : expr
    := CAMP.penv.
  Definition pletenv : expr → expr → expr
    := CAMP.pletEnv.
  Definition pleft : expr
    := CAMP.pleft.
  Definition pright : expr
    := CAMP.pright.

  Definition pnow : expr
    := CAMPSugar.pnow.

  Definition pnull : expr
    := CAMPSugar.pnull.

  Definition pbdot : String.string → expr → expr
    := CAMPSugar.pbdot.

  Definition pbsomedot : String.string → expr → expr
    := CAMPSugar.pbsomedot.

  Definition returnVariables : list String.string → expr
    := CAMPSugar.returnVariables.

  Definition stringConcat : expr → expr → expr
    := CAMPSugar.stringConcat.

  Definition toString : expr → expr
    := CAMPSugar.toString.

  Definition pat_binop_reduce : Ops.Binary.op → list expr → expr
    := CAMPSugar.pat_binop_reduce.

  Definition pvarwith : String.string → expr → expr
    := CAMPSugar.pvarwith.

  Definition withVar : String.string → expr → expr
    := CAMPSugar.withVar.

  Definition pIS : String.string → expr → expr
    := CAMPSugar.pIS.

  Definition lookup : String.string → expr
    := CAMPSugar.lookup.

End QCAMP.