vm.fail
Alpha equivalence checker for arbitrary lambda terms
1exception Json_error of string
2
3type json =
4 | JObject of (string * json) list
5 | JArray of json list
6 | JString of string
7 | JBool of bool
8 | JNull
9
10let read_file path =
11 let ic = open_in_bin path in
12 Fun.protect
13 ~finally:(fun () -> close_in_noerr ic)
14 (fun () ->
15 let n = in_channel_length ic in
16 really_input_string ic n)
17
18let parse_json s =
19 let n = String.length s in
20 let i = ref 0 in
21 let error m = raise (Json_error (m ^ " at byte " ^ string_of_int !i)) in
22 let ws () =
23 while !i < n && match s.[!i] with ' ' | '\n' | '\r' | '\t' -> true | _ -> false do
24 incr i
25 done
26 in
27 let expect c =
28 ws ();
29 if !i >= n || s.[!i] <> c then error ("expected " ^ String.make 1 c);
30 incr i
31 in
32 let parse_lit lit v =
33 let len = String.length lit in
34 if !i + len <= n && String.sub s !i len = lit then (i := !i + len; v)
35 else error ("expected " ^ lit)
36 in
37 let parse_string () =
38 expect '"';
39 let b = Buffer.create 16 in
40 let rec loop () =
41 if !i >= n then error "unterminated string";
42 match s.[!i] with
43 | '"' -> incr i; JString (Buffer.contents b)
44 | '\\' ->
45 incr i;
46 if !i >= n then error "unterminated escape";
47 let c =
48 match s.[!i] with
49 | '"' -> '"'
50 | '\\' -> '\\'
51 | '/' -> '/'
52 | 'b' -> '\b'
53 | 'f' -> '\012'
54 | 'n' -> '\n'
55 | 'r' -> '\r'
56 | 't' -> '\t'
57 | _ -> error "unsupported string escape"
58 in
59 Buffer.add_char b c;
60 incr i;
61 loop ()
62 | c ->
63 Buffer.add_char b c;
64 incr i;
65 loop ()
66 in
67 loop ()
68 in
69 let rec value () =
70 ws ();
71 if !i >= n then error "expected value";
72 match s.[!i] with
73 | '{' -> obj ()
74 | '[' -> arr ()
75 | '"' -> parse_string ()
76 | 't' -> parse_lit "true" (JBool true)
77 | 'f' -> parse_lit "false" (JBool false)
78 | 'n' -> parse_lit "null" JNull
79 | _ -> error "unexpected value"
80 and obj () =
81 expect '{';
82 ws ();
83 if !i < n && s.[!i] = '}' then (incr i; JObject [])
84 else
85 let rec fields acc =
86 let key =
87 match parse_string () with JString k -> k | _ -> assert false
88 in
89 expect ':';
90 let v = value () in
91 ws ();
92 if !i < n && s.[!i] = ',' then (incr i; fields ((key, v) :: acc))
93 else if !i < n && s.[!i] = '}' then (incr i; JObject (List.rev ((key, v) :: acc)))
94 else error "expected ',' or '}'"
95 in
96 fields []
97 and arr () =
98 expect '[';
99 ws ();
100 if !i < n && s.[!i] = ']' then (incr i; JArray [])
101 else
102 let rec elems acc =
103 let v = value () in
104 ws ();
105 if !i < n && s.[!i] = ',' then (incr i; elems (v :: acc))
106 else if !i < n && s.[!i] = ']' then (incr i; JArray (List.rev (v :: acc)))
107 else error "expected ',' or ']'"
108 in
109 elems []
110 in
111 let v = value () in
112 ws ();
113 if !i <> n then error "trailing input";
114 v
115
116let member k = function
117 | JObject xs -> begin
118 match List.assoc_opt k xs with
119 | Some v -> v
120 | None -> raise (Json_error ("missing field: " ^ k))
121 end
122 | _ -> raise (Json_error "expected object")
123
124let to_string = function
125 | JString s -> s
126 | _ -> raise (Json_error "expected string")
127
128let to_list = function
129 | JArray xs -> xs
130 | _ -> raise (Json_error "expected array")
131
132let to_assoc = function
133 | JObject xs -> xs
134 | _ -> raise (Json_error "expected object")
135
136let rec named_of_json j =
137 match member "tag" j |> to_string with
138 | "Var" -> Named.Var (member "name" j |> to_string)
139 | "Lam" ->
140 Named.Lam (member "param" j |> to_string, named_of_json (member "body" j))
141 | "App" ->
142 Named.App (named_of_json (member "fun" j), named_of_json (member "arg" j))
143 | "Subst" ->
144 Named.Subst
145 ( member "var" j |> to_string,
146 named_of_json (member "repl" j),
147 named_of_json (member "body" j) )
148 | t -> raise (Json_error ("unknown tag: " ^ t))
149
150let rec json_of_named = function
151 | Named.Var x -> JObject [ ("tag", JString "Var"); ("name", JString x) ]
152 | Named.Lam (x, b) ->
153 JObject [ ("tag", JString "Lam"); ("param", JString x); ("body", json_of_named b) ]
154 | Named.App (f, a) ->
155 JObject [ ("tag", JString "App"); ("fun", json_of_named f); ("arg", json_of_named a) ]
156 | Named.Subst (x, s, b) ->
157 JObject
158 [ ("tag", JString "Subst");
159 ("var", JString x);
160 ("repl", json_of_named s);
161 ("body", json_of_named b) ]
162
163type corpus_entry = {
164 name : string;
165 t1 : Named.t;
166 t2 : Named.t;
167 expected : bool option;
168}
169
170let load_corpus path =
171 parse_json (read_file path) |> to_list
172 |> List.map (fun e ->
173 {
174 name = member "name" e |> to_string;
175 t1 = named_of_json (member "t1" e);
176 t2 = named_of_json (member "t2" e);
177 expected =
178 (match member "expected" e with
179 | JNull -> None
180 | JBool b -> Some b
181 | _ -> raise (Json_error "expected must be bool or null"));
182 })
183
184let load_bench path =
185 parse_json (read_file path) |> to_assoc
186 |> List.map (fun (k, v) -> (k, named_of_json v))