Permalink
Fetching contributors…
Cannot retrieve contributors at this time
244 lines (217 sloc) 5.28 KB
open import Pervasives
open import Lib
(* Literal constants *)
type lit =
| IntLit of integer
| Char of char
| StrLit of string
| Word8 of word8
| Word64 of word64
(* Built-in binary operations *)
type opn = Plus | Minus | Times | Divide | Modulo
type opb = Lt | Gt | Leq | Geq
type opw = Andw | Orw | Xor | Add | Sub
type shift = Lsl | Lsr | Asr
(* Module names *)
type modN = string
(* Identifiers *)
type id 'a =
| Short of 'a
| Long of modN * 'a
(* Variable names *)
type varN = string
(* Constructor names (from datatype definitions) *)
type conN = string
(* Type names *)
type typeN = string
(* Type variable names *)
type tvarN = string
val mk_id : forall 'a. maybe modN -> 'a -> id 'a
let mk_id mn_opt n =
match mn_opt with
| Nothing -> Short n
| Just mn -> Long mn n
end
val id_to_n : forall 'a. id 'a -> 'a
let id_to_n id =
match id with
| Short n -> n
| Long _ n -> n
end
type word_size = W8 | W64
type op =
(* Operations on integers *)
| Opn of opn
| Opb of opb
(* Operations on words *)
| Opw of word_size * opw
| Shift of word_size * shift * nat
| Equality
(* Function application *)
| Opapp
(* Reference operations *)
| Opassign
| Opref
| Opderef
(* Word8Array operations *)
| Aw8alloc
| Aw8sub
| Aw8length
| Aw8update
(* Word/integer conversions *)
| WordFromInt of word_size
| WordToInt of word_size
(* Char operations *)
| Ord
| Chr
| Chopb of opb
(* String operations *)
| Implode
| Strsub
| Strlen
(* Vector operations *)
| VfromList
| Vsub
| Vlength
(* Array operations *)
| Aalloc
| Asub
| Alength
| Aupdate
(* Call a given foreign function *)
| FFI of string
(* Logical operations *)
type lop =
| And
| Or
(* Type constructors.
* 0-ary type applications represent unparameterised types (e.g., num or string)
*)
type tctor =
(* User defined types *)
| TC_name of id typeN
(* Built-in types *)
| TC_int
| TC_char
| TC_string
| TC_ref
| TC_word8
| TC_word64
| TC_word8array
| TC_fn
| TC_tup
| TC_exn
| TC_vector
| TC_array
(* Types *)
type t =
(* Type variables that the user writes down ('a, 'b, etc.) *)
| Tvar of tvarN
(* deBruijn indexed type variables.
The type system uses these internally. *)
| Tvar_db of nat
| Tapp of list t * tctor
(* Some abbreviations *)
let Tint = Tapp [] TC_int
let Tchar = Tapp [] TC_char
let Tstring = Tapp [] TC_string
let Tref t = Tapp [t] TC_ref
let rec TC_word W8 = TC_word8
and TC_word W64 = TC_word64
let Tword wz = Tapp [] (TC_word wz)
let Tword8 = Tword W8
let Tword64 = Tword W64
let Tword8array = Tapp [] TC_word8array
let Tfn t1 t2 = Tapp [t1;t2] TC_fn
let Texn = Tapp [] TC_exn
(* Patterns *)
type pat =
| Pvar of varN
| Plit of lit
(* Constructor applications.
A Nothing constructor indicates a tuple pattern. *)
| Pcon of maybe (id conN) * list pat
| Pref of pat
| Ptannot of pat * t
(* Expressions *)
type exp =
| Raise of exp
| Handle of exp * list (pat * exp)
| Lit of lit
(* Constructor application.
A Nothing constructor indicates a tuple pattern. *)
| Con of maybe (id conN) * list exp
| Var of id varN
| Fun of varN * exp
(* Application of a primitive operator to arguments.
Includes function application. *)
| App of op * list exp
(* Logical operations (and, or) *)
| Log of lop * exp * exp
| If of exp * exp * exp
(* Pattern matching *)
| Mat of exp * list (pat * exp)
(* A let expression
A Nothing value for the binding indicates that this is a
sequencing expression, that is: (e1; e2). *)
| Let of maybe varN * exp * exp
(* Local definition of (potentially) mutually recursive
functions.
The first varN is the function's name, and the second varN
is its parameter. *)
| Letrec of list (varN * varN * exp) * exp
| Tannot of exp * t
type type_def = list (list tvarN * typeN * list (conN * list t))
(* Declarations *)
type dec =
(* Top-level bindings
* The pattern allows several names to be bound at once *)
| Dlet of pat * exp
(* Mutually recursive function definition *)
| Dletrec of list (varN * varN * exp)
(* Type definition
Defines several data types, each of which has several
named variants, which can in turn have several arguments.
*)
| Dtype of type_def
(* Type abbreviations *)
| Dtabbrev of list tvarN * typeN * t
(* New exceptions *)
| Dexn of conN * list t
type decs = list dec
(* Specifications
For giving the signature of a module *)
type spec =
| Sval of varN * t
| Stype of type_def
| Stabbrev of list tvarN * typeN * t
| Stype_opq of list tvarN * typeN
| Sexn of conN * list t
type specs = list spec
type top =
| Tmod of modN * maybe specs * decs
| Tdec of dec
type prog = list top
(* Accumulates the bindings of a pattern *)
val pat_bindings : pat -> list varN -> list varN
let rec
pat_bindings (Pvar n) already_bound =
n::already_bound
and
pat_bindings (Plit l) already_bound =
already_bound
and
pat_bindings (Pcon _ ps) already_bound =
pats_bindings ps already_bound
and
pat_bindings (Pref p) already_bound =
pat_bindings p already_bound
and
pat_bindings (Ptannot p _) already_bound =
pat_bindings p already_bound
and
pats_bindings [] already_bound =
already_bound
and
pats_bindings (p::ps) already_bound =
pats_bindings ps (pat_bindings p already_bound)