Module ErgoSpec.Ergo.Lang.ErgoSugar


Ergo is a language for expressing contract logic.

Syntactic sugar


Require Import String.
Require Import List.
Require Import ErgoSpec.Common.Names.
Require Import ErgoSpec.Common.Result.
Require Import ErgoSpec.Common.Ast.
Require Import ErgoSpec.Ergo.Lang.Ergo.
Require Import ErgoSpec.Backend.QLib.

Section ErgoSugar.
  Context {A:Set}.
  Context {A':Set}.
  
expr.field is a macro for unbranding followed by field access in a record
  Definition SReturnEmpty (a:A) : @rergo_stmt A A' := SReturn a (EConst a dunit).

  Definition EFunReturnEmpty (a:A) : @rergo_expr A A' := EConst a dunit.

  Definition EOptionalDot (a:A) (pname:string) (e:@rergo_expr A A') :=
    EMatch a
           e
           ((CaseLetOption a "$option" None,
             (ESome a
                    (EUnaryOperator a (EOpDot pname) (EVar a (None,"$option"%string))))) :: nil)
           (ENone a).

  Definition EOptionalDefault (a:A) (e1 e2:@rergo_expr A A') :=
    EMatch a e1
           ((CaseLetOption a "$option" None, EVar a (None,"$option"%string)) :: nil)
           e2.

End ErgoSugar.