Module ErgoSpec.Common.Utils.Ast

Require Import String.
Require Import ErgoSpec.Backend.ErgoBackend.
Require Import ErgoSpec.Common.Utils.Names.
Require Import ErgoSpec.Common.Utils.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 -> ErgoData.data -> ergo_pattern (* match against value *)
      | 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.
  
End Ast.