Module Checker.Syntax

the module holding definitions of the surface syntax of the demo language, including expressions, programs, and syntactic types.

type mutability =
| Imm
| Mut
val min_mutability : mutability -> mutability -> mutability

min_mutability calculates the minimum of two mutabilities w.r.t. the relation: Imm < Mut.

val mutability_has_conflict : mutability -> mutability -> bool

mutability_has_conflict decides if two mutabilities have conflict, i.e. two access to the same location with these mutabilities cannot coexist

type permission =
| Owner
| Borrow of mutability
val min_permission : permission -> permission -> permission

min_permission calculates the minimum of two permissions w.r.t. the relation:: Borrow Imm < Borrow Mut < Owner.

val permission_has_conflict : permission -> permission -> bool

permission_has_conflict decides if two permissions have conflict, i.e. two access to the same location with these permissions cannot coexist

type span = {
pos_s : Stdlib.Lexing.position;
pos_e : Stdlib.Lexing.position;
}
type identifier = {
id_name : string;
id_span : span;
}
type expr = {
shape : expr_shape;
span : span;
}
and expr_shape =
| E_Int of int
| E_Var of string
| E_Assign of expr * expr
| E_Borrow of mutability * expr
| E_Deref of expr
| E_Field of expr * int
| E_Tuple of expr list
| E_Let of identifier * expr * expr
| E_If of expr * expr * expr
| E_App of expr * expr list
| E_While of expr * expr
type passing_mode =
| PM_AsIs
| PM_Borrow of mutability * passing_mode
| PM_Deref of passing_mode

passing_mode indicates how an argument of a function should be passed. Before an argument is passed to a function, it will be decorated depending on the passing mode of the function. This can be used to automatically insert borrows and dereferences.

type typ =
| T_Int
| T_Tuple of typ list
| T_Borrow of mutability * typ
| T_Function of (passing_mode * typ) list * typ
type function_def = {
span : span;
name : string;
params : (identifier * passing_mode * typ) list;
body : expr;
}
type function_typ = {
param_typs : (passing_mode * typ) list;
ret_typ : typ;
}