vm.fail
Alpha equivalence checker for arbitrary lambda terms
1open Ego
2
3let reps_of_string = function
4 | "named" -> [ `Named ]
5 | "debruijn" -> [ `Debruijn ]
6 | "ln" -> [ `Ln ]
7 | "subst" -> [ `Subst ]
8 | "all" -> [ `Named; `Debruijn; `Ln; `Subst ]
9 | r -> failwith ("unknown representation: " ^ r)
10
11let rep_name = function
12 | `Named -> "named"
13 | `Debruijn -> "debruijn"
14 | `Ln -> "ln"
15 | `Subst -> "subst"
16
17let check_with rep t1 t2 =
18 match rep with
19 | `Named -> Named.alpha_equivalent t1 t2
20 | `Debruijn ->
21 Debruijn.alpha_equivalent
22 (Debruijn.convert_from_named t1)
23 (Debruijn.convert_from_named t2)
24 | `Ln ->
25 Locally_nameless.alpha_equivalent
26 (Locally_nameless.convert_from_named t1)
27 (Locally_nameless.convert_from_named t2)
28 | `Subst ->
29 Explicit_subst.alpha_equivalent
30 (Explicit_subst.convert_from_named t1)
31 (Explicit_subst.convert_from_named t2)
32
33let cmd_check t1s t2s rep =
34 match (Syntax.parse_result t1s, Syntax.parse_result t2s) with
35 | Error m, _ | _, Error m ->
36 Printf.printf "PARSE-ERROR: %s\n" m;
37 exit 2
38 | Ok t1, Ok t2 ->
39 List.iter
40 (fun r ->
41 let eq = check_with r t1 t2 in
42 Printf.printf "%s: %s\n" (rep_name r) (if eq then "EQUIV" else "NOT-EQUIV"))
43 (reps_of_string rep)
44
45let cmd_corpus path =
46 let entries = Json_io.load_corpus path in
47 let failures = ref 0 in
48 List.iter
49 (fun (e : Json_io.corpus_entry) ->
50 let results =
51 List.map (fun r -> (r, check_with r e.t1 e.t2))
52 [ `Named; `Debruijn; `Ln; `Subst ]
53 in
54 List.iter
55 (fun (r, got) ->
56 match e.expected with
57 | Some exp when got <> exp ->
58 incr failures;
59 Printf.printf "FAIL %s [%s]: expected %s got %s\n" e.name
60 (rep_name r)
61 (if exp then "EQUIV" else "NOT-EQUIV")
62 (if got then "EQUIV" else "NOT-EQUIV")
63 | _ -> ())
64 results;
65 let agree =
66 match results with
67 | (_, a) :: tl -> List.for_all (fun (_, b) -> b = a) tl
68 | [] -> true
69 in
70 if not agree then begin
71 incr failures;
72 let rs =
73 String.concat ", "
74 (List.map (fun (r, g) -> rep_name r ^ "=" ^ string_of_bool g) results)
75 in
76 Printf.printf "DISAGREE %s: %s\n" e.name rs
77 end)
78 entries;
79 if !failures > 0 then begin
80 Printf.printf "%d failure(s)\n" !failures;
81 exit 1
82 end
83 else Printf.printf "corpus: %d entries, 0 failures\n" (List.length entries)
84
85let now_us () = int_of_float (Unix.gettimeofday () *. 1e6)
86
87let median arr =
88 Array.sort compare arr;
89 arr.(Array.length arr / 2)
90
91type bench_result = {
92 alpha_us : int;
93 norm_us : int;
94 traversals : int;
95 max_depth : int;
96}
97
98let json_escape s =
99 let b = Buffer.create (String.length s + 2) in
100 String.iter
101 (function
102 | '"' -> Buffer.add_string b "\\\""
103 | '\\' -> Buffer.add_string b "\\\\"
104 | '\n' -> Buffer.add_string b "\\n"
105 | '\r' -> Buffer.add_string b "\\r"
106 | '\t' -> Buffer.add_string b "\\t"
107 | c -> Buffer.add_char b c)
108 s;
109 Buffer.contents b
110
111let write_results path impl reps =
112 let oc = open_out_bin path in
113 Fun.protect
114 ~finally:(fun () -> close_out_noerr oc)
115 (fun () ->
116 Printf.fprintf oc "{\"%s\":{" (json_escape impl);
117 reps
118 |> List.iteri (fun ri (rep, benches) ->
119 if ri > 0 then output_char oc ',';
120 Printf.fprintf oc "\"%s\":{" (json_escape rep);
121 benches
122 |> List.iteri (fun bi (name, r) ->
123 if bi > 0 then output_char oc ',';
124 Printf.fprintf oc
125 "\"%s\":{\"alpha_us\":%d,\"norm_us\":%d,\"traversals\":%d,\"max_depth\":%d}"
126 (json_escape name) r.alpha_us r.norm_us r.traversals
127 r.max_depth);
128 output_char oc '}');
129 output_string oc "}}")
130
131let bench_rep rep t1 t2 iters =
132 let alpha_ts = Array.make iters 0 in
133 let norm_ts = Array.make iters 0 in
134 let trav = ref 0 in
135 let depth = ref 0 in
136 for i = 0 to iters - 1 do
137 let t0 = now_us () in
138 let (r, c, d) =
139 match rep with
140 | `Named -> Named.alpha_equivalent_counted t1 t2
141 | `Debruijn ->
142 Debruijn.alpha_equivalent_counted
143 (Debruijn.convert_from_named t1)
144 (Debruijn.convert_from_named t2)
145 | `Ln ->
146 Locally_nameless.alpha_equivalent_counted
147 (Locally_nameless.convert_from_named t1)
148 (Locally_nameless.convert_from_named t2)
149 | `Subst ->
150 Explicit_subst.alpha_equivalent_counted
151 (Explicit_subst.convert_from_named t1)
152 (Explicit_subst.convert_from_named t2)
153 in
154 alpha_ts.(i) <- now_us () - t0;
155 ignore r;
156 if c > !trav then trav := c;
157 if d > !depth then depth := d;
158 let t0 = now_us () in
159 let (_, c, d) =
160 let drop (x, c, d) = (ignore x, c, d) in
161 match rep with
162 | `Named -> drop (Named.normalise_counted t1)
163 | `Debruijn ->
164 drop (Debruijn.normalise_counted (Debruijn.convert_from_named t1))
165 | `Ln ->
166 drop
167 (Locally_nameless.normalise_counted
168 (Locally_nameless.convert_from_named t1))
169 | `Subst ->
170 drop
171 (Explicit_subst.normalise_counted
172 (Explicit_subst.convert_from_named t1))
173 in
174 norm_ts.(i) <- now_us () - t0;
175 if c > !trav then trav := c;
176 if d > !depth then depth := d
177 done;
178 {
179 alpha_us = median alpha_ts;
180 norm_us = median norm_ts;
181 traversals = !trav;
182 max_depth = !depth;
183 }
184
185let cmd_bench path iters out_path =
186 let benches = Json_io.load_bench path in
187 let reps = [ `Named; `Debruijn; `Ln; `Subst ] in
188 let pair_for name t =
189 if Filename.check_suffix name "-a" then
190 let base = String.sub name 0 (String.length name - 2) in
191 match List.assoc_opt (base ^ "-b") benches with Some other -> other | None -> t
192 else t
193 in
194 let rep_json =
195 List.map
196 (fun rep ->
197 let bench_json =
198 List.map
199 (fun (name, t) ->
200 let other = pair_for name t in
201 (name, bench_rep rep t other iters))
202 benches
203 in
204 (rep_name rep, bench_json))
205 reps
206 in
207 write_results out_path "ocaml" rep_json;
208 Printf.printf "bench: wrote %s\n" out_path
209
210let () =
211 let argv = Sys.argv in
212 let argc = Array.length argv in
213 if argc < 2 then begin
214 prerr_endline "usage: ego check <t1> <t2> [-r rep] | ego corpus <file> | ego bench <file> [--iters N] [--out file]";
215 exit 2
216 end;
217 match argv.(1) with
218 | "check" ->
219 let rep = ref "named" in
220 let terms = ref [] in
221 let i = ref 2 in
222 while !i < argc do
223 (match argv.(!i) with
224 | "-r" ->
225 incr i;
226 rep := argv.(!i)
227 | s -> terms := s :: !terms);
228 incr i
229 done;
230 (match List.rev !terms with
231 | [ t1; t2 ] -> cmd_check t1 t2 !rep
232 | _ ->
233 prerr_endline "check requires exactly two terms";
234 exit 2)
235 | "corpus" ->
236 if argc < 3 then begin
237 prerr_endline "corpus requires a file";
238 exit 2
239 end;
240 cmd_corpus argv.(2)
241 | "bench" ->
242 let iters = ref 5 in
243 let out = ref "results.json" in
244 let file = ref None in
245 let i = ref 2 in
246 while !i < argc do
247 (match argv.(!i) with
248 | "--iters" ->
249 incr i;
250 iters := int_of_string argv.(!i)
251 | "--out" ->
252 incr i;
253 out := argv.(!i)
254 | s -> file := Some s);
255 incr i
256 done;
257 (match !file with
258 | Some f -> cmd_bench f !iters !out
259 | None ->
260 prerr_endline "bench requires a file";
261 exit 2)
262 | _ ->
263 prerr_endline "unknown command";
264 exit 2