Previous  Up  Next

Module MiniAst (.ml)

module MiniAst: sig .. end
The abstract syntax of MiniML programs.

Abstract syntax trees are generated by the parser defined in MiniSyntacticAnalysis.

type program = binding list
A program in the Mini language is a sequence of toplevel bindings.
type binding =
| BindValue of Positions.position * value_definition list
| BindRecValue of Positions.position * value_definition list
| TypeDec of Positions.position * type_declaration list
A binding is 
type expression =
| EVar of Positions.position * name
| ELambda of Positions.position * pattern * expression
| EApp of Positions.position * expression * expression
| EBinding of Positions.position * binding * expression
| EPrimApp of Positions.position * primitive * expression list
| EForall of Positions.position * tname list * expression
| EExists of Positions.position * tname list * expression
| ETypeConstraint of Positions.position * expression * typ
| EDCon of Positions.position * dname * expression list
| EMatch of Positions.position * expression * clause list
| ERecordEmpty of Positions.position
| ERecordAccess of Positions.position * expression * lname
| ERecordExtend of Positions.position * record_binding list * expression
| ERecordUpdate of Positions.position * expression * lname * expression
| EAssertFalse of Positions.position
An expression in Mini. Here is a description of the abstract syntax tree's nodes with their denotation in the concrete syntax:

Core ML

EVar
A variable is an identifier in the language [azAZ][azAZ_]*.

ELambda
Lambda expressions follow the syntax \pattern. exp. For example, \x. x + 1 is the successor function.

EApp
Application is done by concatenation as in id 0.

EBinding
One can define binding locally using the let keyword. For instance: let id = \x.x in id 0. There is a syntactic sugar that expands: let identifier pat1 ... patn = exp into let identifier = \pat1. ... \patn. exp. Furthermore, a set of rigid universally quantified type variables can be introduced in the typing scope using the syntax: let forall a1 ... an. id = exp. The user can refer to a1 ... an in exp and id.

EPrimApp
The Mini language has builtins like integers or predefined algebraic datatypes. See MiniAst.primitive.

EForall
Universally quantified type variables can be introduced using the syntax: forall a.exp. Such type variables can be used as rigid variables in type annotations, as in: let id = forall a. (\x. x : a -> a)

EExist
Existentially quantified type variables can be introduced using the syntax: exists a.exp. Such type variables can be used as rigid variables in type annotations, as in: let id = exists a. (\x. x : a -> a)

ETypeConstraint
Expression can be annotated by types. As an example: let id = \x. x : int -> int.

Algebraic Datatypes

EDCon
Data constructors are used as usual function expression except that they must be fully applied. Cons 0 Nil is the application of the data constructor Cons to 0 and Nil.

EDMatch
A value whose type is an algebraic datatype can be matched against a set of clause's patterns. The syntax of matching in Mini is 
match exp with clause_1 | clause_2 | ... | clause_n end
For instance, the following function computes the length of a list: 
let rec len l = 

      match exp with

        Nil => 0

      | Cons x xs => 1 + len xs

      end

    

Record

ERecordEmpty
The syntax {} defines an empty record.

ERecordAccess
The syntax expression.l is an access the label l of the record expression.

ERecordExtend
A record can be defined by extension as in { l_1 = exp_1 and l_2 = exp_2 and ... and l_n = exp_n }.

ERecordUpdate
Record provides extension using the syntax expression.l <- expression.

Misc

EAssertFalse
The user can use the syntax assert false to express assumed dead code branches.
type name = Constraint.sname =
| SName of string
Program identifiers.
type tname = MultiEquation.tname
Type variable names.
type dname =
| DName of string
Data constructors.
type lname = CoreAlgebra.lname
Record labels.
type primitive =
| PIntegerConstant of int (*Integer constant.*)
| PCharConstant of char (*Character constant.*)
| PUnit (*Unit constant.*)
Constant.
type clause = Positions.position * pattern * expression
Pattern matching clause.
type record_binding = lname * expression 
type type_declaration = Positions.position * kind * tname * type_definition 
type type_definition =
| DAlgebraic of (Positions.position * dname * tname list * typ) list
Type definitions.

DAlgebraic
Algebraic datatypes are defined by that way: 
type id : kind = 

          forall a1 ... an.  

              K1  : typ 

            | ... 

            | KN  : typ

For example, here is the definition of polymorphic lists: 

type list : * -> * = forall a.

        Nil : list a

      | Cons : a -> list a -> list a

    

type value_definition = Positions.position * tname list * pattern *
       expression
A value definition consists of a list of explicit universal quantifiers, a pattern, and an expression.
type pattern =
| PVar of Positions.position * name
| PWildcard of Positions.position
| PAlias of Positions.position * name * pattern
| PTypeConstraint of Positions.position * pattern * typ
| PPrimitive of Positions.position * primitive
| PData of Positions.position * dname * pattern list
| PAnd of Positions.position * pattern list
| POr of Positions.position * pattern list 
type kind =
| KStar
| KTimes of kind * kind
| KArrow of kind * kind
| KEmptyRow 
type typ =
| TypVar of Positions.position * tname
| TypApp of Positions.position * typ * typ list
| TypRowCons of Positions.position * (lname * typ) list * typ
| TypRowUniform of Positions.position * typ