Module ErgoSpec.Common.Ast

Require Import String.
Require Import ErgoSpec.Backend.QLib.
Require Import ErgoSpec.Common.Names.
Require Import ErgoSpec.Common.Provenance.

Section Ast.
  Section Imports.
    Section Defn.
      Context {A:Set}.
      Context {N:Set}.

      Inductive import_decl : Set :=
      | ImportAll : A -> namespace_name -> import_decl
      | ImportSelf : A -> namespace_name -> import_decl
      | ImportName : A -> namespace_name -> local_name -> import_decl.

      Definition import_annot (i:import_decl) :=
        match i with
        | ImportAll a _ => a
        | ImportSelf a _ => a
        | ImportName a _ _ => a
        end.

      Definition extends : Set := option N.
    End Defn.

    Definition limport_decl : Set := @import_decl provenance.
    
    Definition rextends : Set := @extends relative_name.
    Definition aextends : Set := @extends absolute_name.
  End Imports.

  Section Abstract.
    Definition is_abstract : Set := bool.
    
  End Abstract.

  Section Patterns.
    Section Defn.
      Local Open Scope string.

      Context {A:Set}.
      Context {N:Set}.
  
      Definition type_annotation : Set := option N.

      Inductive ergo_pattern :=
      | CaseData : A -> QcertData.data -> ergo_pattern (* match against value *)
      | CaseEnum : A -> N -> ergo_pattern (* match against enum *)
      | CaseWildcard : A -> type_annotation -> ergo_pattern (* match anything *)
      | CaseLet : A -> string -> type_annotation -> ergo_pattern (* match against type *)
      | CaseLetOption : A -> string -> type_annotation -> ergo_pattern (* match against type *)
      .
    End Defn.

    Definition rergo_pattern {A} := @ergo_pattern A relative_name.
    Definition aergo_pattern {A} := @ergo_pattern A absolute_name.

    Definition lrergo_pattern := @ergo_pattern provenance relative_name.
    Definition laergo_pattern := @ergo_pattern provenance absolute_name.
  End Patterns.

  Section Operators.
    Local Open Scope string.

    Inductive ergo_unary_operator :=
    | EOpUMinus : ergo_unary_operator
    | EOpDot : string -> ergo_unary_operator
    .

    Global Instance ToString_ergo_unary_operator : ToString ergo_unary_operator
      := {toString :=
            fun (op:ergo_unary_operator) =>
              match op with
              | EOpUMinus => "-"
              | EOpDot a => "." ++ a
              end
         }.

    Inductive ergo_binary_operator :=
    | EOpPlus : ergo_binary_operator
    | EOpMinus : ergo_binary_operator
    | EOpMultiply : ergo_binary_operator
    | EOpDivide : ergo_binary_operator
    | EOpRemainder : ergo_binary_operator
    | EOpGe : ergo_binary_operator
    | EOpGt : ergo_binary_operator
    | EOpLe : ergo_binary_operator
    | EOpLt : ergo_binary_operator
    .

    Global Instance ToString_ergo_binary_operator : ToString ergo_binary_operator
      := {toString :=
            fun (op:ergo_binary_operator) =>
              match op with
              | EOpPlus => "+"
              | EOpMinus => "-"
              | EOpMultiply => "*"
              | EOpDivide => "/"
              | EOpRemainder => "%"
              | EOpGe => ">="
              | EOpGt => ">"
              | EOpLe => "<="
              | EOpLt => "<"
              end
         }.

  End Operators.
End Ast.