(**************************************************************************)

(*  Mini, a type inference engine based on constraint solving.            *)
(*  Copyright (C) 2006. François Pottier, Yann Régis-Gianas               *)
(*  and Didier Rémy.                                                      *)
(*                                                                        *)
(*  This program is free software; you can redistribute it and/or modify  *)
(*  it under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation; version 2 of the License.               *)
(*                                                                        *)
(*  This program is distributed in the hope that it will be useful, but   *)
(*  WITHOUT ANY WARRANTY; without even the implied warranty of            *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU     *)
(*  General Public License for more details.                              *)
(*                                                                        *)
(*  You should have received a copy of the GNU General Public License     *)
(*  along with this program; if not, write to the Free Software           *)
(*  Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA         *)
(*  02110-1301 USA                                                        *)
(*                                                                        *)
(**************************************************************************)


(* $Id: miniAst.ml 421 2006-12-22 09:27:42Z regisgia $ *)

(** The abstract syntax of programs *)


open Positions

type program = 
    binding list

and binding =
  | BindValue of position * value_definition list
  | BindRecValue of position * value_definition list
  | TypeDec of position * type_declaration list

and expression =
    
  
  (** Core ML. *)

  | EVar of position * name 
  | ELambda of position * pattern * expression
  | EApp of position * expression * expression
  | EBinding of position * binding * expression
  | EPrimApp of position * primitive * expression list
  | EForall of position * tname list * expression
  | EExists of position * tname list * expression
  
  
  (** Type annotations. *)

  | ETypeConstraint of position * expression * typ
  
  
  (** Algebraic datatypes. *)
 
  | EDCon of position * dname * expression list
  | EMatch of position * expression * (clause list)

  
  (** Records. *)

  | ERecordEmpty of position
  | ERecordAccess of position * expression * lname
  | ERecordExtend of position * record_binding list * expression
  | ERecordUpdate of position * expression * lname * expression

  
  (** Misc. *)

  | EAssertFalse of position

(** Program identifiers. *)

and name = Constraint.sname =
  | SName of string
      
(** Type variable names. *)

and tname =
    MultiEquation.tname

(** Data constructors. *)

and dname =
    DName of string

(** Record labels. *)

and lname =
    CoreAlgebra.lname
  
(** Constant. *)

and primitive =
  | PIntegerConstant of int        
             (** Integer constant. *)

  | PCharConstant of char        
             (** Character constant. *)

  | PUnit                        
                           (** Unit constant. *)


(** Pattern matching clause. *)

and clause =
    position * pattern * expression

and record_binding =
    lname * expression

and type_declaration =
    position * kind * tname * type_definition

and type_definition =
  | DAlgebraic of (position * dname * tname list * typ) list

(** A value definition consists of a list of explicit universal quantifiers, a pattern, and an expression. *)

and value_definition =
    position * tname list * pattern * expression

and pattern =
  | PVar of position * name
  | PWildcard of position 
  | PAlias of position * name * pattern
  | PTypeConstraint of position * pattern * typ
  | PPrimitive of position * primitive
  | PData of position * dname * pattern list
  | PAnd of position * pattern list
  | POr of position * pattern list

and kind = 
  | KStar
  | KTimes of kind * kind
  | KArrow of kind * kind
  | KEmptyRow 

and typ =
  | TypVar of position * tname
  | TypApp of position * typ * typ list 
  | TypRowCons of position * (lname * typ) list * typ
  | TypRowUniform of position * typ