vm.fail
Alpha equivalence checker for arbitrary lambda terms
1open Ego
2
3let find_corpus () =
4 let candidates =
5 [ "../shared/corpus.json"; "shared/corpus.json";
6 "/home/bulg/projects/ego/shared/corpus.json" ]
7 in
8 match List.find_opt Sys.file_exists candidates with
9 | Some p -> p
10 | None -> failwith "corpus.json not found"
11
12let check_bool name exp got =
13 if got <> exp then
14 failwith
15 (Printf.sprintf "%s: expected %b got %b" name exp got)
16
17let check_raises name f =
18 match f () with
19 | _ -> failwith (name ^ ": expected exception")
20 | exception _ -> ()
21
22let check_with rep t1 t2 =
23 match rep with
24 | `Named -> Named.alpha_equivalent t1 t2
25 | `Debruijn ->
26 Debruijn.alpha_equivalent
27 (Debruijn.convert_from_named t1)
28 (Debruijn.convert_from_named t2)
29 | `Ln ->
30 Locally_nameless.alpha_equivalent
31 (Locally_nameless.convert_from_named t1)
32 (Locally_nameless.convert_from_named t2)
33 | `Subst ->
34 Explicit_subst.alpha_equivalent
35 (Explicit_subst.convert_from_named t1)
36 (Explicit_subst.convert_from_named t2)
37
38let reps = [ `Named; `Debruijn; `Ln; `Subst ]
39
40let test_corpus () =
41 let entries = Json_io.load_corpus (find_corpus ()) in
42 List.iter
43 (fun (e : Json_io.corpus_entry) ->
44 List.iter
45 (fun r ->
46 match e.Json_io.expected with
47 | Some exp ->
48 check_bool
49 (Printf.sprintf "%s [%s]" e.name
50 (match r with
51 | `Named -> "named" | `Debruijn -> "debruijn"
52 | `Ln -> "ln" | `Subst -> "subst"))
53 exp (check_with r e.t1 e.t2)
54 | None -> ())
55 reps)
56 entries
57
58let rng = Random.State.make [| 42 |]
59
60let names = [| "a"; "b"; "c"; "d"; "e"; "f" |]
61let fvs = [| "p"; "q"; "g"; "h" |]
62
63let rec gen scope depth =
64 let pick arr = arr.(Random.State.int rng (Array.length arr)) in
65 if depth <= 0 then
66 match scope with
67 | [] -> Named.Var (pick fvs)
68 | _ ->
69 if Random.State.float rng 1.0 < 0.75 then Named.Var (pick (Array.of_list scope))
70 else Named.Var (pick fvs)
71 else
72 let r = Random.State.float rng 1.0 in
73 if r < 0.45 then
74 let n =
75 if scope <> [] && Random.State.float rng 1.0 < 0.35
76 then pick (Array.of_list scope)
77 else pick names
78 in
79 Named.Lam (n, gen (n :: scope) (depth - 1))
80 else if r < 0.75 then
81 Named.App (gen scope (depth - 1), gen scope (depth - 1))
82 else if r < 0.85 then
83 let n = match scope with [] -> "u" | _ -> pick (Array.of_list scope) in
84 Named.Subst (n, gen scope (depth - 1), gen scope (depth - 1))
85 else
86 match scope with
87 | [] -> Named.Var (pick fvs)
88 | _ -> Named.Var (pick (Array.of_list scope))
89
90let random_term () = gen [] (2 + Random.State.int rng 4)
91
92let test_reflexivity () =
93 for _ = 1 to 200 do
94 let t = random_term () in
95 List.iter
96 (fun r ->
97 check_bool "reflexive" true (check_with r t t))
98 reps
99 done
100
101let test_symmetry () =
102 for _ = 1 to 200 do
103 let t1 = random_term () in
104 let t2 = random_term () in
105 List.iter
106 (fun r ->
107 check_bool "symmetric"
108 (check_with r t1 t2) (check_with r t2 t1))
109 reps
110 done
111
112let test_transitivity () =
113 for _ = 1 to 100 do
114 let t = random_term () in
115 List.iter
116 (fun r ->
117 let norm_named n =
118 match r with
119 | `Named -> Named.normalise n
120 | _ -> Named.normalise n
121 in
122 let a = check_with r t t in
123 let b = check_with r (norm_named t) (norm_named t) in
124 check_bool "transitive-self" a b)
125 reps
126 done
127
128let test_fv_preserved () =
129 for _ = 1 to 200 do
130 let t1 = random_term () in
131 let t2 = random_term () in
132 if Named.alpha_equivalent t1 t2 then
133 check_bool "fv equal" true
134 (Named.SSet.equal (Named.free_variables (Named.normalise t1))
135 (Named.free_variables (Named.normalise t2)))
136 done
137
138let test_roundtrip () =
139 for _ = 1 to 200 do
140 let t = random_term () in
141 let t' = Debruijn.convert_to_named (Debruijn.convert_from_named t) in
142 check_bool "roundtrip debruijn" true
143 (Named.alpha_equivalent t' t);
144 let t'' =
145 Locally_nameless.convert_to_named
146 (Locally_nameless.convert_from_named t)
147 in
148 check_bool "roundtrip ln" true
149 (Named.alpha_equivalent t'' t);
150 let t''' =
151 Explicit_subst.convert_to_named
152 (Explicit_subst.convert_from_named t)
153 in
154 check_bool "roundtrip subst" true
155 (Named.alpha_equivalent t''' t)
156 done
157
158let test_cross_rep_normalise () =
159 for _ = 1 to 100 do
160 let t = random_term () in
161 let n1 = Named.normalise t in
162 let n2 =
163 Debruijn.convert_to_named
164 (Debruijn.normalise (Debruijn.convert_from_named t))
165 in
166 let n3 =
167 Locally_nameless.convert_to_named
168 (Locally_nameless.normalise (Locally_nameless.convert_from_named t))
169 in
170 let n4 =
171 Explicit_subst.convert_to_named
172 (Explicit_subst.normalise (Explicit_subst.convert_from_named t))
173 in
174 check_bool "named vs debruijn" true
175 (Named.alpha_equivalent n1 n2);
176 check_bool "named vs ln" true
177 (Named.alpha_equivalent n1 n3);
178 check_bool "named vs subst" true
179 (Named.alpha_equivalent n1 n4)
180 done
181
182let test_parse_errors () =
183 List.iter
184 (fun s ->
185 match Syntax.parse_result s with
186 | Ok _ -> failwith ("should reject: " ^ s)
187 | Error _ -> ())
188 [ ""; "\\"; "\\x"; "\\x."; "(\\x. x"; "\\x. x)"; "[x := ] x"; "[ := y] x";
189 "((x"; "[x := y]"; "."; "\\. x" ]
190
191let test_malformed () =
192 let open Locally_nameless in
193 check_bool "dangling bvar" false (lc (BVar 0));
194 check_bool "closed lam" true (lc (Lam (BVar 0)));
195 check_bool "dangling deep" false
196 (lc (Lam (Lam (BVar 2))));
197 check_raises "convert raises"
198 (fun () -> ignore (convert_to_named (BVar 3)));
199 check_raises "alpha raises"
200 (fun () -> ignore (alpha_equivalent (BVar 1) (BVar 1)))
201
202let test_debruijn_scope () =
203 let open Debruijn in
204 check_bool "well scoped" true (well_scoped 0 (Lam (Var 0)));
205 check_bool "ill scoped" false (well_scoped 0 (Var 0));
206 check_raises "to_named raises"
207 (fun () -> ignore (convert_to_named (Lam (Var 2))))
208
209let test_capture_avoidance () =
210 let parse s =
211 match Syntax.parse_result s with
212 | Ok t -> t
213 | Error m -> failwith m
214 in
215 let cases =
216 [ ("[x := z] \\z. x", "\\w. z", true);
217 ("[x := z] \\z. x", "\\z. z", false);
218 ("[x := q] \\x. x", "\\x. x", true);
219 ("[x := y] \\y. x y", "\\w. y w", true);
220 ("[x := f y] \\y. \\z. x z", "\\a. \\b. f y b", true);
221 ("[x := a] [y := b] x y", "a b", true) ]
222 in
223 List.iter
224 (fun (s1, s2, exp) ->
225 let t1 = parse s1 in
226 let t2 = parse s2 in
227 List.iter
228 (fun r ->
229 check_bool (s1 ^ " ~ " ^ s2) exp (check_with r t1 t2))
230 reps)
231 cases
232
233let test_explicit_susp () =
234 let open Explicit_subst in
235 let t = of_named (Named.Subst ("x", Named.Var "z", Named.Lam ("z", Named.Var "x"))) in
236 let n = normalise t in
237 (match n with
238 | Lam (y, Var z) ->
239 check_bool "binder renamed" true (y <> "z");
240 check_bool "body is free z" true (z = "z")
241 | _ -> failwith "expected renamed lambda");
242 check_bool "susp agrees with normal" true
243 (alpha_equivalent_susp t (normalise t))
244
245let () =
246 let tests =
247 [ ("corpus", test_corpus);
248 ("reflexivity", test_reflexivity);
249 ("symmetry", test_symmetry);
250 ("transitivity", test_transitivity);
251 ("fv preserved", test_fv_preserved);
252 ("roundtrip", test_roundtrip);
253 ("cross-rep normalise", test_cross_rep_normalise);
254 ("parse errors", test_parse_errors);
255 ("local closure", test_malformed);
256 ("de bruijn scope", test_debruijn_scope);
257 ("capture avoidance", test_capture_avoidance);
258 ("suspended subst", test_explicit_susp) ]
259 in
260 List.iter
261 (fun (name, f) ->
262 f ();
263 Printf.printf "ok %s\n" name)
264 tests