vm.fail
Alpha equivalence checker for arbitrary lambda terms
1type token =
2 | TBackslash
3 | TDot
4 | TLParen
5 | TRParen
6 | TLBrack
7 | TRBrack
8 | TColonEq
9 | TVar of string
10
11exception Parse_error of string
12
13let is_var_start c = (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z')
14
15let is_var_char c =
16 is_var_start c || (c >= '0' && c <= '9') || c = '_' || c = '\'' || c = '-'
17
18let lex s =
19 let n = String.length s in
20 let rec go i acc =
21 if i >= n then List.rev acc
22 else
23 match s.[i] with
24 | ' ' | '\t' | '\n' | '\r' -> go (i + 1) acc
25 | '\\' -> go (i + 1) (TBackslash :: acc)
26 | '.' -> go (i + 1) (TDot :: acc)
27 | '(' -> go (i + 1) (TLParen :: acc)
28 | ')' -> go (i + 1) (TRParen :: acc)
29 | '[' -> go (i + 1) (TLBrack :: acc)
30 | ']' -> go (i + 1) (TRBrack :: acc)
31 | ':' ->
32 if i + 1 < n && s.[i + 1] = '=' then go (i + 2) (TColonEq :: acc)
33 else raise (Parse_error ("unexpected ':' at position " ^ string_of_int i))
34 | c when is_var_start c ->
35 let j = ref (i + 1) in
36 while !j < n && is_var_char s.[!j] do
37 incr j
38 done;
39 go !j (TVar (String.sub s i (!j - i)) :: acc)
40 | c ->
41 raise
42 (Parse_error
43 (Printf.sprintf "unexpected character %C at position %d" c i))
44 in
45 go 0 []
46
47let parse s =
48 let toks = Array.of_list (lex s) in
49 let n = Array.length toks in
50 let pos = ref 0 in
51 let peek () = if !pos < n then Some toks.(!pos) else None in
52 let next () =
53 let t = peek () in
54 incr pos;
55 t
56 in
57 let expect tok what =
58 match next () with
59 | Some t when t = tok -> ()
60 | _ -> raise (Parse_error ("expected " ^ what))
61 in
62 let starts_atom = function
63 | Some (TVar _) | Some TLParen | Some TBackslash | Some TLBrack -> true
64 | _ -> false
65 in
66 let rec term () =
67 match peek () with
68 | Some TBackslash -> lam ()
69 | Some TLBrack -> subst ()
70 | _ -> app ()
71 and lam () =
72 ignore (next ());
73 match next () with
74 | Some (TVar v) ->
75 expect TDot "'.'";
76 let body = term () in
77 Named.Lam (v, body)
78 | _ -> raise (Parse_error "expected variable after '\\'")
79 and subst () =
80 ignore (next ());
81 match next () with
82 | Some (TVar v) ->
83 expect TColonEq "':='";
84 let s = term () in
85 expect TRBrack "']'";
86 let body = term () in
87 Named.Subst (v, s, body)
88 | _ -> raise (Parse_error "expected variable after '['")
89 and app () =
90 let lhs = atom () in
91 let rec args lhs =
92 if starts_atom (peek ()) then args (Named.App (lhs, atom ())) else lhs
93 in
94 args lhs
95 and atom () =
96 match next () with
97 | Some (TVar v) -> Named.Var v
98 | Some TLParen ->
99 let t = term () in
100 expect TRParen "')'";
101 t
102 | Some TBackslash -> begin
103 match next () with
104 | Some (TVar v) ->
105 expect TDot "'.'";
106 Named.Lam (v, term ())
107 | _ -> raise (Parse_error "expected variable after '\\'")
108 end
109 | Some TLBrack -> begin
110 match next () with
111 | Some (TVar v) ->
112 expect TColonEq "':='";
113 let s = term () in
114 expect TRBrack "']'";
115 Named.Subst (v, s, term ())
116 | _ -> raise (Parse_error "expected variable after '['")
117 end
118 | _ -> raise (Parse_error "expected a term")
119 in
120 let t = term () in
121 if !pos <> n then raise (Parse_error "trailing input");
122 t
123
124let parse_result s =
125 match parse s with t -> Ok t | exception Parse_error m -> Error m