71 lines
1.6 KiB
OCaml
71 lines
1.6 KiB
OCaml
open Lexer
|
|
open Lexing
|
|
open Parser
|
|
open Types
|
|
|
|
exception EvaluationComplete
|
|
|
|
let rec string_of_term (t:term) =
|
|
match t with
|
|
| TmAbs(x, t1) ->
|
|
"(\\" ^ x ^ "." ^ (string_of_term t1) ^ ")"
|
|
| TmApp(t1, t2) ->
|
|
"(" ^ (string_of_term t1) ^ " " ^ (string_of_term t2) ^ ")"
|
|
| TmVar(x) -> x
|
|
|
|
(*
|
|
let termshift d t =
|
|
let rec walk c t =
|
|
match t with
|
|
| TmVar(x) -> if
|
|
|
|
let termsubsttop (s:term) (t:term) =
|
|
termshift (-1) (termsubst 0 (termshift 1 s) t)
|
|
|
|
let rec isval ctx t =
|
|
match t with
|
|
| TmAbs(_, _, _) -> true
|
|
| _ -> false
|
|
|
|
let rec helper ctx t =
|
|
match t with
|
|
| TmApp(TmAbs(x, t1), v2) when isval ctx v2 -> termsubsttop v2 t1
|
|
| _ -> EvaluationComplete
|
|
*)
|
|
|
|
let assign ctx (name, t) : context =
|
|
(name, t)::ctx
|
|
|
|
let rec lookup ctx name : term =
|
|
match ctx with
|
|
| [] -> raise (Failure ("unbound variable " ^ name))
|
|
| (n, t)::tail ->
|
|
if n = name then t else lookup tail name
|
|
|
|
let rec eval (ctx, t) =
|
|
let rec helper (ctx, t) =
|
|
raise EvaluationComplete
|
|
in try
|
|
let (ctx', t') = helper (ctx, t) in
|
|
eval (ctx', t')
|
|
with EvaluationComplete -> (ctx, t)
|
|
|
|
let _ =
|
|
try
|
|
let rec loop ctx =
|
|
print_string "> "; flush stdout;
|
|
let lexbuf = Lexing.from_channel stdin in
|
|
let x = Parser.main Lexer.token lexbuf in
|
|
match x with
|
|
| Types.Term t ->
|
|
let (ctx', r) = eval (ctx, t) in
|
|
print_endline (string_of_term r); flush stdout;
|
|
loop ctx'
|
|
| Types.Assign (n, t) ->
|
|
let (ctx', r) = eval (ctx, t) in
|
|
(* bind the name *)
|
|
loop ctx'
|
|
in loop []
|
|
with Lexer.Eof ->
|
|
print_endline "^D";
|
|
exit 0
|