Abstract Syntax

Require Import String.
Require Import ErgoSpec.Utils.Misc.
Require Import ErgoSpec.Types.ErgoType.
Require Import ErgoSpec.Backend.QLib.

Section ErgoNNRC.

  Section Syntax.

    Definition nnrc_expr := QcertCodeGen.nnrc_expr.
    Definition nnrc_type := laergo_type.

    Record lambdan :=
      mkLambdaN
        { lambdan_params: list (string * nnrc_type);
          lambdan_output : option nnrc_type;
          lambdan_body : nnrc_expr; }.

    Record nnrc_function :=
      mkFuncN
        { functionn_name : string;
          functionn_lambda : lambdan; }.

    Record nnrc_function_table :=
      mkFuncTableN
        { function_tablen_name : string;
          function_tablen_funs : list nnrc_function; }.

    Inductive nnrc_declaration :=
    | DNExpr : nnrc_expr -> nnrc_declaration
    | DNConstant : string -> nnrc_expr -> nnrc_declaration
    | DNFunc : nnrc_function -> nnrc_declaration
    | DNFuncTable : nnrc_function_table -> nnrc_declaration.

    Record nnrc_module :=
      mkModuleN
        { modulen_namespace : string;
          modulen_declarations : list nnrc_declaration; }.

  End Syntax.

  Record result_file :=
    mkResultFile {
        res_contract_name : option string;
        res_file : string;
        res_nnrc : nnrc_module;
        res_content : nstring;
      }.

  Section Semantics.
  End Semantics.

  Section Evaluation.
  End Evaluation.
End ErgoNNRC.