-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathsyntax.ml
112 lines (101 loc) · 4.79 KB
/
syntax.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
(** Abstract syntax *)
(** The type of variable names. *)
type name = string
(** Levy types are separated into value types and computation types, but
it is convenient to have a single datatype for all of them. *)
type ltype =
| VInt (** integer [int] *)
| VBool (** booleans [bool] *)
| VForget of ctype (** thunked type [U t] *)
| CFree of vtype (** free type [F s] *)
| CArrow of vtype * ctype (** Function type [s -> t] *)
and vtype = ltype
and ctype = ltype
(** Levy expressions. We actually use the same type for values
and computations because it makes the code shorter and produces
more reasonable error messages during type checking. *)
type value = expr
and expr =
| Var of name (** variable *)
| Int of int (** integer constant *)
| Bool of bool (** boolean constant *)
| Times of value * value (** product [v1 * v2] *)
| Plus of value * value (** sum [v1 + v2] *)
| Minus of value * value (** difference [v1 - v2] *)
| Equal of value * value (** integer equality [v1 = v2] *)
| Less of value * value (** integer comparison [v1 < v2] *)
| Thunk of expr (** thunk [thunk e] *)
| Force of value (** [force v] *)
| Return of value (** [return v] *)
| To of expr * name * expr (** sequencing [e1 to x . e2] *)
| Let of name * value * expr (** let-binding [let x = v in e] *)
| If of value * expr * expr (** conditional [if v then e1 else e2] *)
| Fun of name * ltype * expr (** function [fun x:s -> e] *)
| Apply of expr * value (** application [e v] *)
| Rec of name * ltype * expr (** recursion [rec x : t is e] *)
(** Toplevel commands *)
type toplevel_cmd =
| Expr of expr (** an expression to be evaluated *)
| Def of name * expr (** toplevel definition [let x = e] *)
| RunDef of name * expr (** toplevel definition [do x = e] *)
| Use of string (** load a file [$use "<filename>"] *)
| Quit (** exit toplevel [$quit] *)
(** Conversion from a type to a string *)
let string_of_type ty =
let rec to_str n ty =
let (m, str) =
match ty with
| VInt -> (3, "int")
| VBool -> (3, "bool")
| VForget ty -> (2, "U " ^ to_str 1 ty)
| CFree ty -> (2, "F " ^ to_str 1 ty)
| CArrow (ty1, ty2) -> (1, (to_str 1 ty1) ^ " -> " ^ (to_str 0 ty2))
in
if m > n then str else "(" ^ str ^ ")"
in
to_str (-1) ty
(** Conversion from an expression to a string *)
let string_of_expr e =
let rec to_str n e =
let (m, str) =
match e with
| Int n -> (10, string_of_int n)
| Bool b -> (10, string_of_bool b)
| Var x -> (10, x)
| Return e -> ( 9, "return " ^ (to_str 9 e))
| Force e -> ( 9, "force " ^ (to_str 9 e))
| Thunk e -> ( 9, "thunk " ^ (to_str 9 e))
| Apply (e1, e2) -> ( 9, (to_str 8 e1) ^ " " ^ (to_str 9 e2))
| Times (e1, e2) -> ( 8, (to_str 7 e1) ^ " * " ^ (to_str 8 e2))
| Plus (e1, e2) -> ( 7, (to_str 6 e1) ^ " + " ^ (to_str 7 e2))
| Minus (e1, e2) -> ( 7, (to_str 6 e1) ^ " - " ^ (to_str 7 e2))
| Equal (e1, e2) -> ( 5, (to_str 5 e1) ^ " = " ^ (to_str 5 e2))
| Less (e1, e2) -> ( 5, (to_str 5 e1) ^ " < " ^ (to_str 5 e2))
| If (e1, e2, e3) -> ( 4, "if " ^ (to_str 4 e1) ^ " then " ^ (to_str 4 e2) ^ " else " ^ (to_str 4 e3))
| Fun (x, ty, e) -> ( 2, "fun " ^ x ^ " : " ^ (string_of_type ty) ^ " -> " ^ (to_str 0 e))
| Rec (x, ty, e) -> ( 2, "rec " ^ x ^ " : " ^ (string_of_type ty) ^ " is " ^ (to_str 0 e))
| Let (x, e1, e2) ->( 1, "let " ^ x ^ " = " ^ to_str 1 e1 ^ " in " ^ to_str 0 e2)
| To (e1, x, e2) -> ( 1, to_str 1 e1 ^ " to " ^ x ^ " . " ^ to_str 0 e2)
in
if m > n then str else "(" ^ str ^ ")"
in
to_str (-1) e
(** [subst [(x1,e1);...;(xn;en)] e] replaces in [e] free occurrences
of variables [x1], ..., [xn] with expressions [e1], ..., [en]. *)
let rec subst s = function
| (Var x) as e -> (try List.assoc x s with Not_found -> e)
| (Int _ | Bool _) as e -> e
| Times (e1, e2) -> Times (subst s e1, subst s e2)
| Plus (e1, e2) -> Plus (subst s e1, subst s e2)
| Minus (e1, e2) -> Minus (subst s e1, subst s e2)
| Equal (e1, e2) -> Equal (subst s e1, subst s e2)
| Less (e1, e2) -> Less (subst s e1, subst s e2)
| If (e1, e2, e3) -> If (subst s e1, subst s e2, subst s e3)
| Fun (x, ty, e) -> let s' = List.remove_assoc x s in Fun (x, ty, subst s' e)
| Let (x, e1, e2) -> Let (x, subst s e1, subst (List.remove_assoc x s) e2)
| To (e1, x, e2) -> To (subst s e1, x, subst (List.remove_assoc x s) e2)
| Return e -> Return (subst s e)
| Force e -> Force (subst s e)
| Thunk e -> Thunk (subst s e)
| Apply (e1, e2) -> Apply (subst s e1, subst s e2)
| Rec (x, ty, e) -> let s' = List.remove_assoc x s in Rec (x, ty, subst s' e)