diff --git a/README.md b/README.md index 5d414e5..41354d6 100644 --- a/README.md +++ b/README.md @@ -1 +1,4 @@ # λ + +Based on Benjamin Pierce's _Types and Programming Languages_ + diff --git a/lambda.ml b/lambda.ml index e2870d9..3390806 100644 --- a/lambda.ml +++ b/lambda.ml @@ -3,24 +3,72 @@ open Lexing open Parser open Types +exception EvaluationComplete + let rec string_of_term (t:term) = match t with | TmAbs(x, t1) -> - "(\\" ^ (String.make 1 x) ^ "." ^ (string_of_term t1) ^ ")" + "(\\" ^ x ^ "." ^ (string_of_term t1) ^ ")" | TmApp(t1, t2) -> - "(" ^ (string_of_term t1) ^ (string_of_term t2) ^ ")" - | TmVar(x) -> - String.make 1 x + "(" ^ (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) = + match t with + | Assign(name, t') -> + let (ctx', r) = helper(ctx, t') in + (assign ctx (name, r), r) + | TmAbs(name, t') -> + let (ctx', v) = helper (ctx, t') in + (assign ctx (name, v), v) + | TmVar(name) -> + (ctx, lookup ctx name) + | _ -> 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 result = Parser.main Lexer.token lexbuf in - print_endline (string_of_term result); flush stdout; - loop ctx in + let t = Parser.main Lexer.token lexbuf in + let (ctx', r) = eval (ctx, t) in + print_endline (string_of_term r); flush stdout; + loop ctx' in loop [] with Lexer.Eof -> - print_endline "error"; + print_endline "^D"; exit 0 diff --git a/lexer.mll b/lexer.mll index f6ac937..04412b6 100644 --- a/lexer.mll +++ b/lexer.mll @@ -6,7 +6,10 @@ rule token = parse | ' ' | '\t' { token lexbuf } | '\n' { EOL } + | '=' { Equal } | '\\' { Lambda } + | '(' { LParen } + | ')' { RParen } | '.' { Dot } - | ['a'-'z'] as c | ['A'-'Z'] as c { Ident(c) } + | ['a'-'z' 'A'-'Z'] ['a'-'z' 'A'-'Z' '0'-'9' '_']* as s { Ident(s) } | eof { raise Eof } diff --git a/parser.mly b/parser.mly index c2959bd..f6e9def 100644 --- a/parser.mly +++ b/parser.mly @@ -4,7 +4,10 @@ %token EOL %token Dot -%token Ident +%token Equal +%token LParen +%token RParen +%token Ident %token Lambda %start main @@ -12,12 +15,16 @@ %% main: - expr EOL { $1 } + | assign EOL { $1 } + | expr EOL { $1 } +; +assign: + | Ident Equal expr { Types.Assign($1, $3) } ; expr: | var { Types.TmVar($1) } | Lambda var Dot expr { Types.TmAbs($2, $4) } - | expr expr { Types.TmApp ($1, $2) } + | LParen expr expr RParen { Types.TmApp ($2, $3) } ; var: Ident { $1 } diff --git a/types.ml b/types.ml index 83286fa..60ca23d 100644 --- a/types.ml +++ b/types.ml @@ -1,9 +1,10 @@ +type var = string + type term = - | TmVar of char - | TmAbs of char * term + | Assign of string * term + | TmVar of var + | TmAbs of var * term | TmApp of term * term -type binding = NameBind - -type context = (char * binding) list +type context = (string * term) list