Module ErgoSpec.ErgoC.Lang.ErgoC

ErgoC is an intermediate language for the Ergo compiler in which:

Clauses have been resolved to functions
This* expressions have been eliminated
Foreach expressions have only one dimension and no condition
Match expressions have only two branches

Abstract Syntax

Require Import String.
Require Import ErgoSpec.Common.Utils.Provenance.
Require Import ErgoSpec.Common.Utils.Result.
Require Import ErgoSpec.Common.Utils.Names.
Require Import ErgoSpec.Common.Types.ErgoType.
Require Import ErgoSpec.Backend.ErgoBackend.
Require Import ErgoSpec.Ergo.Lang.Ergo.

Section ErgoC.

Section Syntax.

Expression

    Definition ergoc_expr := laergo_expr.

    Record sigc :=
      mkSigC
        { sigc_params: list (string * laergo_type);
          sigc_output : option laergo_type; }.

Function

    Record ergoc_function :=
      mkFuncC
        { functionc_annot : provenance;
          functionc_sig : sigc;
          functionc_body : option ergoc_expr; }.

    Definition bodyc_annot (f:ergoc_function) : provenance :=
      match f.(functionc_body) with
      | None => f.(functionc_annot)
      | Some e => expr_annot e
      end.

Contract

    Record ergoc_contract :=
      mkContractC
        { contractc_annot : provenance;
          contractc_clauses : list (local_name * ergoc_function); }.

Declaration

    Inductive ergoc_declaration :=
    | DCExpr : provenance -> ergoc_expr -> ergoc_declaration
    | DCConstant : provenance -> absolute_name -> option laergo_type -> ergoc_expr -> ergoc_declaration
    | DCFunc : provenance -> absolute_name -> ergoc_function -> ergoc_declaration
    | DCContract : provenance -> absolute_name -> ergoc_contract -> ergoc_declaration.

Module.

    Record ergoc_module :=
      mkModuleC
        { modulec_annot : provenance;
          modulec_namespace : string;
          modulec_declarations : list ergoc_declaration; }.

  End Syntax.

  Section Semantics.

  End Semantics.

  Section Evaluation.
  End Evaluation.

End ErgoC.