let () = Printexc.record_backtrace true
exception Parse_error
let must_kwd s k = match Stream.next s with Genlex.Kwd k' when k' = k -> () | _ -> raise Parse_error
let peek_kwd s k = match Stream.peek s with Some (Genlex.Kwd k') when k' = k -> let _ = Stream.next s in true | _ -> false
let stream_is_empty s = try Stream.empty s; true with Stream.Failure -> false
let ident s = match Stream.next s with Genlex.Ident x -> x | _ -> raise Parse_error
let lexer = Genlex.make_lexer ["("; ")"; "=>"; "/\\"; "\\/"; "fun"; "->"; ","; ":"; "fst"; "snd"; "T"; "left"; "right"; "not"; "case"; "of"; "|"; "absurd"; "_"]
let ty_of_tk s =
let rec ty () = arr ()
and arr () =
let a = prod () in
if peek_kwd s "=>" then Imp (a, arr ()) else a
and prod () =
let a = sum () in
if peek_kwd s "/\\" then And (a, prod ()) else a
and sum () =
let a = base () in
if peek_kwd s "\\/" then Or (a, sum ()) else a
and base () =
match Stream.next s with
| Genlex.Ident x -> TVar x
| Genlex.Kwd "(" ->
let a = ty () in
must_kwd s ")";
a
| Genlex.Kwd "T" -> True
| Genlex.Kwd "_" -> False
| Genlex.Kwd "not" ->
let a = base () in
Imp (a, False)
| _ -> raise Parse_error
in
ty ()
let tm_of_tk s =
let noapp = List.map (fun k -> Some (Genlex.Kwd k)) [")"; ","; "case"; "fun"; "of"; "->"; "|"] in
let ty () = ty_of_tk s in
let rec tm () = app ()
and app () =
let t = ref (abs ()) in
while not (stream_is_empty s) && not (List.mem (Stream.peek s) noapp) do
t := App (!t, abs ())
done;
!t
and abs () =
if peek_kwd s "fun" then
(
must_kwd s "(";
let x = ident s in
must_kwd s ":";
let a = ty () in
must_kwd s ")";
must_kwd s "->";
let t = tm () in
Abs (x, a, t)
)
else if peek_kwd s "case" then
(
let t = tm () in
must_kwd s "of";
let x = ident s in
must_kwd s "->";
let u = tm () in
must_kwd s "|";
let y = ident s in
must_kwd s "->";
let v = tm () in
Case (t, x, u, y, v)
)
else
base ()
and base () =
match Stream.next s with
| Genlex.Ident x -> Var x
| Genlex.Kwd "(" ->
if peek_kwd s ")" then
Unit
else
let t = tm () in
if peek_kwd s "," then
let u = tm () in
must_kwd s ")";
Pair (t, u)
else
(
must_kwd s ")";
t
)
| Genlex.Kwd "fst" ->
must_kwd s "(";
let t = tm () in
must_kwd s ")";
Fst t
| Genlex.Kwd "snd" ->
must_kwd s "(";
let t = tm () in
must_kwd s ")";
Snd t
| Genlex.Kwd "left" ->
must_kwd s "(";
let t = tm () in
must_kwd s ",";
let b = ty () in
must_kwd s ")";
Left (t, b)
| Genlex.Kwd "right" ->
must_kwd s "(";
let a = ty () in
must_kwd s ",";
let t = tm () in
must_kwd s ")";
Right (a, t)
| Genlex.Kwd "absurd" ->
must_kwd s "(";
let t = tm () in
must_kwd s ",";
let a = ty () in
must_kwd s ")";
Absurd (t, a)
| _ -> raise Parse_error
in
tm ()
let ty_of_string a = ty_of_tk (lexer (Stream.of_string a))
let tm_of_string t = tm_of_tk (lexer (Stream.of_string t))