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.

Module ErgoSpec.Ergo.Lang.ErgoSugar