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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
open Ast
exception FoundRedex of expr index
let has_free_var (ast : expr ast) (i : expr index) (name : string) : bool =
let exception FoundIt in
let rec loop (i : expr index) =
match get_subexpr ast i with
| App (f, x) ->
loop f;
loop x
| Cons (hd, tl) ->
loop hd;
loop tl
| Int _ | Nil -> ()
| Lam (x, b) -> if not (String.equal name x) then loop b
| Let (recursive, name', bound, body) ->
if not (String.equal name name') then loop body;
if (not recursive) || not (String.equal name name') then loop bound
| Prim (Add, (l, r)) ->
loop l;
loop r
| Prim (Sub, (l, r)) ->
loop l;
loop r
| Prim (Mul, (l, r)) ->
loop l;
loop r
| Var x -> if String.equal name x then raise FoundIt
in
try
loop i;
false
with FoundIt -> true
let%expect_test "has_free_var shadowing tests" =
let ast = new_ast () in
let add (expr : expr) : expr index =
let index = Arraylist.length ast.subexprs in
Arraylist.push ast.subexprs expr;
{ index }
in
let x = add (Var "x") in
let three = add (Int 3) in
let letx3inx = add (Let (false, "x", three, x)) in
Printf.printf "let x = 3 in x: %b\n" (has_free_var ast letx3inx "x");
let letxxinx = add (Let (false, "x", x, x)) in
Printf.printf "let x = x in x: %b\n" (has_free_var ast letxxinx "x");
let letrecxxinx = add (Let (true, "x", x, x)) in
Printf.printf "let rec x = x in x: %b\n" (has_free_var ast letrecxxinx "x");
[%expect
{|
let x = 3 in x: false
let x = x in x: true
let rec x = x in x: false
|}]
let check_redex (ast : expr ast) (i : expr index) : unit =
match get_subexpr ast i with
| App (f, _) -> (
match get_subexpr ast f with Lam _ -> raise (FoundRedex i) | _ -> ())
| Let (_, _, _, _) -> raise (FoundRedex i)
| Prim (Add, (l, r)) | Prim (Sub, (l, r)) | Prim (Mul, (l, r)) -> (
match (get_subexpr ast l, get_subexpr ast r) with
| Int _, Int _ -> raise (FoundRedex i)
| _ -> ())
| Var _ -> ()
| Cons _ | Int _ | Lam _ | Nil -> ()
let find_redex_cbv_in (ast : expr ast) : expr index -> unit =
let rec loop (i : expr index) : unit =
(match get_subexpr ast i with
| App (f, x) ->
loop f;
loop x
| Let (_, _, bound, _) -> loop bound
| Prim (Add, (l, r)) | Prim (Sub, (l, r)) | Prim (Mul, (l, r)) ->
loop l;
loop r
| Var _ -> ()
| Cons _ | Int _ | Lam _ | Nil -> ());
check_redex ast i
in
loop
let find_redex_cbn_in (ast : expr ast) : expr index -> unit =
let rec loop (i : expr index) : unit =
check_redex ast i;
match get_subexpr ast i with
| App (f, x) ->
loop f;
loop x
| Let (_, _, _, body) -> loop body
| Prim (Add, (l, r)) | Prim (Sub, (l, r)) | Prim (Mul, (l, r)) ->
loop l;
loop r
| Var _ -> ()
| Cons _ | Int _ | Lam _ | Nil -> ()
in
loop
let find_redex_cbv (ast : expr ast) : expr index option =
try
find_redex_cbv_in ast ast.root;
None
with FoundRedex i -> Some i
let find_redex_cbn (ast : expr ast) : expr index option =
try
find_redex_cbn_in ast ast.root;
None
with FoundRedex i -> Some i
exception NotARedex of expr ast
(* TODO: Be capture-avoiding! *)
let subst (ast : expr ast) (from : string) (to_ : expr index) :
expr index -> expr index =
let rec loop (i : expr index) : expr index =
let add (expr : expr) : expr index =
if get_subexpr ast i = expr then i
else
let index = Arraylist.length ast.subexprs in
Arraylist.push ast.subexprs expr;
{ index }
in
match get_subexpr ast i with
| App (f, x) -> add (App (loop f, loop x))
| Cons (hd, tl) -> add (Cons (loop hd, loop tl))
| Int _ | Nil -> i
| Lam (x, b) -> if String.equal from x then i else add (Lam (x, loop b))
| Let (false, name, bound, body) ->
add
(Let (false, name, loop bound, if name = from then body else loop body))
| Let (true, name, bound, body) ->
if name = from then i else add (Let (true, name, loop bound, loop body))
| Prim (Add, (l, r)) -> add (Prim (Add, (loop l, loop r)))
| Prim (Sub, (l, r)) -> add (Prim (Sub, (loop l, loop r)))
| Prim (Mul, (l, r)) -> add (Prim (Mul, (loop l, loop r)))
| Var x -> if String.equal from x then to_ else i
in
loop
let reduce (ast : expr ast) (i : expr index) : expr ast =
let fail () = raise (NotARedex { ast with root = i }) in
let ast = copy ast in
let must_int j = match get_subexpr ast j with Int n -> n | _ -> fail () in
Arraylist.set ast.subexprs i.index
(match get_subexpr ast i with
| App (f, x) -> (
match get_subexpr ast f with
| Lam (x', b) -> get_subexpr ast (subst ast x' x b)
| _ -> fail ())
| Let (_, name, _, body) when not (has_free_var ast body name) ->
get_subexpr ast body
| Let (recursive, name, bound, body) ->
Let (recursive, name, bound, subst ast name bound body)
| Prim (Add, (l, r)) -> Int (must_int l + must_int r)
| Prim (Sub, (l, r)) -> Int (must_int l - must_int r)
| Prim (Mul, (l, r)) -> Int (must_int l * must_int r)
| _ -> fail ());
ast
|
