Module Qcert.Compiler.Lib.QCAMP

Require Import CompilerRuntime.
Require String BrandRelation.
Require CAMPRuntime.

Require QOperators QData.

Module QCAMP(runtime:CompilerRuntime).

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

  Definition camp : Set
    := CAMP.camp.
  Definition t : Set
    := camp.
  
  Definition pconst : Data.t -> camp
    := CAMP.pconst.
  Definition punop : Ops.Unary.op -> camp -> camp
    := CAMP.punop.
  Definition pbinop : Ops.Binary.op -> camp -> camp -> camp
    := CAMP.pbinop.
  Definition pmap : camp -> camp
    := CAMP.pmap.
  Definition passert : camp -> camp
    := CAMP.passert.
  Definition porelse : camp -> camp -> camp
    := CAMP.porElse.
  Definition pit : camp
    := CAMP.pit.
  Definition pletit : camp -> camp -> camp
    := CAMP.pletIt.
  Definition pgetConstant : String.string -> camp
    := CAMP.pgetConstant.
  Definition penv : camp
    := CAMP.penv.
  Definition pletenv : camp -> camp -> camp
    := CAMP.pletEnv.
  Definition pleft : camp
    := CAMP.pleft.
  Definition pright : camp
    := CAMP.pright.

  Definition pnow : camp
    := CAMPSugar.pnow.

  Definition pnull : camp
    := CAMPSugar.pnull.

  Definition pbdot : String.string -> camp -> camp
    := CAMPSugar.pbdot.

  Definition pbsomedot : String.string -> camp -> camp
    := CAMPSugar.pbsomedot.

  Definition returnVariables : list String.string -> camp
    := CAMPSugar.returnVariables.

  Definition stringConcat : camp -> camp -> camp
    := CAMPSugar.stringConcat.

  Definition toString : camp -> camp
    := CAMPSugar.toString.

  Definition camp_binop_reduce : Ops.Binary.op -> list camp -> camp
    := CAMPSugar.camp_binop_reduce.

  Definition pvarwith : String.string -> camp -> camp
    := CAMPSugar.pvarwith.

  Definition withVar : String.string -> camp -> camp
    := CAMPSugar.withVar.

  Definition pIS : String.string -> camp -> camp
    := CAMPSugar.pIS.

  Definition lookup : String.string -> camp
    := CAMPSugar.lookup.
  
End QCAMP.