syntax.ml
1:
2:
3:
4: type name = string
5:
6:
7:
8: type ltype =
9: | VInt
10: | VBool
11: | VForget of ctype
12: | CFree of vtype
13: | CArrow of vtype * ctype
14:
15: and vtype = ltype
16:
17: and ctype = ltype
18:
19:
20:
21:
22:
23: type value = expr
24:
25: and expr =
26: | Var of name
27: | Int of int
28: | Bool of bool
29: | Times of value * value
30: | Plus of value * value
31: | Minus of value * value
32: | Equal of value * value
33: | Less of value * value
34: | Thunk of expr
35: | Force of value
36: | Return of value
37: | To of expr * name * expr
38: | Let of name * value * expr
39: | If of value * expr * expr
40: | Fun of name * ltype * expr
41: | Apply of expr * value
42: | Rec of name * ltype * expr
43:
44:
45: type toplevel_cmd =
46: | Expr of expr
47: | Def of name * expr
48: | Use of string
49: | Quit
50:
51:
52: let string_of_type ty =
53: let rec to_str n ty =
54: let (m, str) =
55: match ty with
56: | VInt -> (3, "int")
57: | VBool -> (3, "bool")
58: | VForget ty -> (2, "U " ^ to_str 1 ty)
59: | CFree ty -> (2, "F " ^ to_str 1 ty)
60: | CArrow (ty1, ty2) -> (1, (to_str 1 ty1) ^ " -> " ^ (to_str 0 ty2))
61: in
62: if m > n then str else "(" ^ str ^ ")"
63: in
64: to_str (-1) ty
65:
66:
67: let string_of_expr e =
68: let rec to_str n e =
69: let (m, str) =
70: match e with
71: | Int n -> (10, string_of_int n)
72: | Bool b -> (10, string_of_bool b)
73: | Var x -> (10, x)
74: | Return e -> ( 9, "return " ^ (to_str 9 e))
75: | Force e -> ( 9, "force " ^ (to_str 9 e))
76: | Thunk e -> ( 9, "thunk " ^ (to_str 9 e))
77: | Apply (e1, e2) -> ( 9, (to_str 8 e1) ^ " " ^ (to_str 9 e2))
78: | Times (e1, e2) -> ( 8, (to_str 7 e1) ^ " * " ^ (to_str 8 e2))
79: | Plus (e1, e2) -> ( 7, (to_str 6 e1) ^ " + " ^ (to_str 7 e2))
80: | Minus (e1, e2) -> ( 7, (to_str 6 e1) ^ " - " ^ (to_str 7 e2))
81: | Equal (e1, e2) -> ( 5, (to_str 5 e1) ^ " = " ^ (to_str 5 e2))
82: | Less (e1, e2) -> ( 5, (to_str 5 e1) ^ " < " ^ (to_str 5 e2))
83: | If (e1, e2, e3) -> ( 4, "if " ^ (to_str 4 e1) ^ " then " ^ (to_str 4 e2) ^ " else " ^ (to_str 4 e3))
84: | Fun (x, ty, e) -> ( 2, "fun " ^ x ^ " : " ^ (string_of_type ty) ^ " -> " ^ (to_str 0 e))
85: | Rec (x, ty, e) -> ( 2, "rec " ^ x ^ " : " ^ (string_of_type ty) ^ " is " ^ (to_str 0 e))
86: | Let (x, e1, e2) ->( 1, "let " ^ x ^ " = " ^ to_str 1 e1 ^ " in " ^ to_str 0 e2)
87: | To (e1, x, e2) -> ( 1, to_str 1 e1 ^ " to " ^ x ^ " . " ^ to_str 0 e2)
88: in
89: if m > n then str else "(" ^ str ^ ")"
90: in
91: to_str (-1) e
92:
93:
94:
95: let rec subst s = function
96: | (Var x) as e -> (try List.assoc x s with Not_found -> e)
97: | (Int _ | Bool _) as e -> e
98: | Times (e1, e2) -> Times (subst s e1, subst s e2)
99: | Plus (e1, e2) -> Plus (subst s e1, subst s e2)
100: | Minus (e1, e2) -> Minus (subst s e1, subst s e2)
101: | Equal (e1, e2) -> Equal (subst s e1, subst s e2)
102: | Less (e1, e2) -> Less (subst s e1, subst s e2)
103: | If (e1, e2, e3) -> If (subst s e1, subst s e2, subst s e3)
104: | Fun (x, ty, e) -> let s' = List.remove_assoc x s in Fun (x, ty, subst s' e)
105: | Let (x, e1, e2) -> Let (x, subst s e1, subst (List.remove_assoc x s) e2)
106: | To (e1, x, e2) -> To (subst s e1, x, subst (List.remove_assoc x s) e2)
107: | Return e -> Return (subst s e)
108: | Force e -> Force (subst s e)
109: | Thunk e -> Thunk (subst s e)
110: | Apply (e1, e2) -> Apply (subst s e1, subst s e2)
111: | Rec (x, ty, e) -> let s' = List.remove_assoc x s in Rec (x, ty, subst s' e)
type_check.ml
1:
2:
3: open Syntax
4:
5:
6: exception Type_error of string
7:
8:
9: let type_error msg = raise (Type_error ("Type error: " ^ msg))
10:
11: let rec is_ctype = function
12: | (VInt | VBool | VForget _) -> false
13: | CFree ty -> is_vtype ty
14: | CArrow (ty1, ty2) -> is_vtype ty1 && is_ctype ty2
15:
16: and is_vtype = function
17: | VInt | VBool -> true
18: | VForget ty -> is_ctype ty
19: | (CFree _ | CArrow _) -> false
20:
21: let check_ctype ty =
22: if not (is_ctype ty) then type_error (string_of_type ty ^ " is not a computation type")
23:
24: let check_vtype ty =
25: if not (is_vtype ty) then type_error (string_of_type ty ^ " is not a value type")
26:
27:
28:
29:
30: let rec check ctx ty e =
31: let ty' = type_of ctx e in
32: if ty' <> ty then
33: type_error
34: (string_of_expr e ^ " has type " ^ string_of_type ty' ^
35: " but is used as if it had type " ^ string_of_type ty)
36:
37:
38:
39: and type_of ctx = function
40: | Var x ->
41: (try
42: List.assoc x ctx
43: with
44: Not_found -> type_error ("unknown identifier " ^ x))
45: | Int _ -> VInt
46: | Bool _ -> VBool
47: | Times (e1, e2) -> check ctx VInt e1 ; check ctx VInt e2 ; VInt
48: | Plus (e1, e2) -> check ctx VInt e1 ; check ctx VInt e2 ; VInt
49: | Minus (e1, e2) -> check ctx VInt e1 ; check ctx VInt e2 ; VInt
50: | Equal (e1, e2) -> check ctx VInt e1 ; check ctx VInt e2 ; VBool
51: | Less (e1, e2) -> check ctx VInt e1 ; check ctx VInt e2 ; VBool
52: | If (e1, e2, e3) ->
53: check ctx VBool e1 ;
54: let ty = type_of ctx e2 in
55: check_ctype ty ; check ctx ty e3 ; ty
56: | Fun (x, ty, e) ->
57: check_vtype ty ;
58: let ty2 = type_of ((x,ty)::ctx) e in
59: check_ctype ty2 ; CArrow (ty, ty2)
60: | Apply (e1, e2) ->
61: (match type_of ctx e1 with
62: | CArrow (ty1, ty2) -> check ctx ty1 e2 ; ty2
63: | ty ->
64: type_error (string_of_expr e1 ^
65: " is used as a function but its type is " ^
66: string_of_type ty))
67: | To (e1, x, e2) ->
68: (match type_of ctx e1 with
69: | CFree ty1 ->
70: check_vtype ty1 ;
71: let ty2 = type_of ((x,ty1)::ctx) e2 in
72: check_ctype ty2 ; ty2
73: | ty -> type_error (string_of_expr e1 ^
74: " is used in sequencing but its type is " ^
75: string_of_type ty))
76: | Let (x, e1, e2) ->
77: let ty1 = type_of ctx e1 in
78: check_vtype ty1;
79: let ty2 = type_of ((x,ty1)::ctx) e2 in
80: check_ctype ty2 ; ty2
81: | Return e ->
82: let ty = type_of ctx e in
83: check_vtype ty ; CFree ty
84: | Force e ->
85: (match type_of ctx e with
86: | VForget ty -> check_ctype ty ; ty
87: | ty -> type_error (string_of_expr e ^ " is forced but its type is " ^ string_of_type ty))
88: | Thunk e ->
89: let ty = type_of ctx e in
90: check_ctype ty ; VForget ty
91: | Rec (x, ty, e) ->
92: check_ctype ty ;
93: check ((x, VForget ty)::ctx) ty e ;
94: ty
interpret.ml
1:
2:
3: open Syntax
4:
5: type environment = (name * runtime) list
6:
7: and runtime =
8: | VInt of int
9: | VBool of bool
10: | VThunk of environment * expr
11: | VFun of environment * name * expr
12: | VReturn of runtime
13:
14: exception Runtime_error of string
15:
16: let runtime_error msg = raise (Runtime_error ("Runtime error: " ^ msg))
17:
18:
19: let rec string_of_runtime = function
20: | VInt k -> string_of_int k
21: | VBool b -> string_of_bool b
22: | VThunk _ -> "<thunk>"
23: | VFun _ -> "<fun>"
24: | VReturn v -> "return " ^ string_of_runtime v
25:
26: let rec interp env = function
27: | Var x ->
28: (try
29: List.assoc x env
30: with
31: Not_found -> runtime_error ("Unknown variable " ^ x))
32: | Int k -> VInt k
33: | Bool b -> VBool b
34: | Thunk e -> VThunk (env, e)
35: | Fun (x, _, e) -> VFun (env, x, e)
36: | Times (e1, e2) ->
37: (match (interp env e1), (interp env e2) with
38: | VInt k1, VInt k2 -> VInt (k1 * k2)
39: | _ -> runtime_error "Integers expected in multiplication")
40: | Plus (e1, e2) ->
41: (match (interp env e1), (interp env e2) with
42: | VInt k1, VInt k2 -> VInt (k1 + k2)
43: | _ -> runtime_error "Integers expected in addition")
44: | Minus (e1, e2) ->
45: (match (interp env e1), (interp env e2) with
46: | VInt k1, VInt k2 -> VInt (k1 - k2)
47: | _ -> runtime_error "Integers expected in subtraction")
48: | Equal (e1, e2) ->
49: (match (interp env e1), (interp env e2) with
50: | VInt k1, VInt k2 -> VBool (k1 = k2)
51: | _ -> runtime_error "Integers expected in =")
52: | Less (e1, e2) ->
53: (match (interp env e1), (interp env e2) with
54: | VInt k1, VInt k2 -> VBool (k1 < k2)
55: | _ -> runtime_error "Integers expected in <")
56: | If (e1, e2, e3) ->
57: (match interp env e1 with
58: | VBool true -> interp env e2
59: | VBool false -> interp env e3
60: | _ -> runtime_error "Boolean expected in if")
61: | Apply (e1, e2) ->
62: (match interp env e1, interp env e2 with
63: | VFun (env, x, e), v2 -> interp ((x,v2)::env) e
64: | _, _ -> runtime_error "Function expected in application")
65: | Let (x, e1, e2) ->
66: let v = interp env e1 in interp ((x,v)::env) e2
67: | To (e1, x, e2) ->
68: (match interp env e1 with
69: | VReturn v -> interp ((x,v)::env) e2
70: | _ -> runtime_error "Return expected in sequencing")
71: | Return e -> VReturn (interp env e)
72: | Force e ->
73: (match interp env e with
74: | VThunk (env, e) -> interp env e
75: | _ -> runtime_error "Thunk expected in force")
76: | Rec (x, _, e') as e -> interp ((x, VThunk (env, e)) :: env) e'
lexer.mll
1: {
2: open Parser
3: open Lexing
4:
5: let incr_linenum lexbuf =
6: let pos = lexbuf.lex_curr_p in
7: lexbuf.lex_curr_p <- { pos with
8: pos_lnum = pos.pos_lnum + 1;
9: pos_bol = pos.pos_cnum;
10: }
11: }
12:
13: let var = ['_' 'a'-'z' 'A'-'Z'] ['_' 'a'-'z' 'A'-'Z' '0'-'9']*
14:
15: rule token = parse
16: | '#' [^'\n']* ('\n' | eof) { incr_linenum lexbuf; token lexbuf }
17: | '\n' { incr_linenum lexbuf; token lexbuf }
18: | [' ' '\t'] { token lexbuf }
19: | ['0'-'9']+ { INT (int_of_string(lexeme lexbuf)) }
20:
21: | 'U' { TFORGET }
22: | 'F' { TFREE }
23: | "->" { ARROW }
24: | "bool" { TBOOL }
25: | "int" { TINT }
26:
27: | "else" { ELSE }
28: | "false" { FALSE }
29: | "force" { FORCE }
30: | "fun" { FUN }
31: | "if" { IF }
32: | "in" { IN }
33: | "is" { IS }
34: | "let" { LET }
35: | "rec" { REC }
36: | "return" { RETURN }
37: | "then" { THEN }
38: | "thunk" { THUNK }
39: | "to" { TO }
40: | "true" { TRUE }
41:
42: | "$use" { USE }
43: | "$quit" { QUIT }
44: | ";;" { SEMICOLON2 }
45: | '\"' [^'\"']* '\"' { let str = lexeme lexbuf in
46: STRING (String.sub str 1 (String.length str - 2)) }
47:
48: | '(' { LPAREN }
49: | ')' { RPAREN }
50: | '*' { TIMES }
51: | '+' { PLUS }
52: | '-' { MINUS }
53: | ':' { COLON }
54: | '<' { LESS }
55: | '=' { EQUAL }
56:
57: | var { VAR (lexeme lexbuf) }
58: | eof { EOF }
59:
60: {
61: }
parser.mly
1: %{
2: open Syntax
3: %}
4:
5: %token TINT
6: %token TBOOL
7: %token TFORGET
8: %token TFREE
9: %token TARROW
10: %token <Syntax.name> VAR
11: %token <int> INT
12: %token TRUE FALSE
13: %token PLUS
14: %token MINUS
15: %token TIMES
16: %token EQUAL LESS
17: %token IF THEN ELSE
18: %token FUN ARROW
19: %token REC IS
20: %token COLON
21: %token LPAREN RPAREN
22: %token LET IN
23: %token TO
24: %token SEMICOLON2
25: %token RETURN THUNK FORCE
26: %token QUIT
27: %token USE
28: %token <string>STRING
29: %token EOF
30:
31: %start toplevel
32: %type <Syntax.toplevel_cmd list> toplevel
33:
34: %nonassoc TO PERIOD
35: %nonassoc LET IN
36: %nonassoc FUN ARROW REC IS
37: %nonassoc IF THEN ELSE
38: %nonassoc EQUAL LESS
39: %left PLUS MINUS
40: %left TIMES
41: %right TARROW
42:
43: %%
44:
45: toplevel:
46: | EOF { [] }
47: | lettop { $1 }
48: | exprtop { $1 }
49: | cmdtop { $1 }
50:
51: lettop:
52: | def EOF { [$1] }
53: | def lettop { $1 :: $2 }
54: | def SEMICOLON2 toplevel { $1 :: $3 }
55:
56: exprtop:
57: | expr EOF { [Expr $1] }
58: | expr SEMICOLON2 toplevel { Expr $1 :: $3 }
59:
60: cmdtop:
61: | cmd EOF { [$1] }
62: | cmd SEMICOLON2 toplevel { $1 :: $3 }
63:
64: cmd:
65: | USE STRING { Use $2 }
66: | QUIT { Quit }
67:
68: def: LET VAR EQUAL expr { Def ($2, $4) }
69:
70: expr:
71: | app { $1 }
72: | arith { $1 }
73: | boolean { $1 }
74: | LET VAR EQUAL expr IN expr { Let ($2, $4, $6) }
75: | expr TO VAR IN expr { To ($1, $3, $5) }
76: | IF expr THEN expr ELSE expr { If ($2, $4, $6) }
77: | FUN VAR COLON ty ARROW expr { Fun ($2, $4, $6) }
78: | REC VAR COLON ty IS expr { Rec ($2, $4, $6) }
79:
80: app:
81: | non_app { $1 }
82: | FORCE non_app { Force $2 }
83: | RETURN non_app { Return $2 }
84: | THUNK non_app { Thunk $2 }
85: | app non_app { Apply ($1, $2) }
86:
87: non_app:
88: | VAR { Var $1 }
89: | TRUE { Bool true }
90: | FALSE { Bool false }
91: | INT { Int $1 }
92: | LPAREN expr RPAREN { $2 }
93:
94: arith:
95: | MINUS INT { Int (-$2) }
96: | expr PLUS expr { Plus ($1, $3) }
97: | expr MINUS expr { Minus ($1, $3) }
98: | expr TIMES expr { Times ($1, $3) }
99:
100: boolean:
101: | expr EQUAL expr { Equal ($1, $3) }
102: | expr LESS expr { Less ($1, $3) }
103:
104: ty:
105: | TINT { VInt }
106: | TBOOL { VBool }
107: | ty ARROW ty { CArrow ($1, $3) }
108: | TFORGET ty { VForget $2 }
109: | TFREE ty { CFree $2 }
110: | LPAREN ty RPAREN { $2 }
111:
112: %%
levy.ml
1:
2:
3: open Message
4: open Syntax
5:
6:
7:
8:
9:
10:
11:
12:
13:
14:
15:
16:
17:
18:
19:
20:
21: exception Fatal_error of string
22:
23: let fatal_error msg = raise (Fatal_error msg)
24:
25:
26:
27:
28:
29: let rec exec_cmd n (ctx, env) = function
30: | Expr e ->
31:
32: let ty = Type_check.type_of ctx e in
33: let v = Interpret.interp env e in
34: print_endline ((if Type_check.is_ctype ty then "comp " else "val ") ^
35: string_of_type ty ^ " = " ^ Interpret.string_of_runtime v) ;
36: (ctx, env)
37: | Def (x, e) ->
38:
39: let ty = Type_check.type_of ctx e in
40: Type_check.check_vtype ty ;
41: let v = Interpret.interp env e in
42: print_endline ("val " ^ x ^ " : " ^ string_of_type ty ^ " = " ^ Interpret.string_of_runtime v) ;
43: ((x,ty)::ctx, (x,v)::env)
44: | Quit -> raise End_of_file
45: | Use fn -> exec_file n (ctx, env) fn
46:
47:
48:
49:
50:
51:
52: and exec_file n ce fn =
53: let fh = open_in fn in
54: let lex = Message.lexer_from_channel fn fh in
55: try
56: let cmds = Parser.toplevel Lexer.token lex in
57: close_in fh ;
58: exec_cmds n ce cmds
59: with
60: Type_check.Type_error msg -> fatal_error (fn ^ ":\n" ^ msg)
61: | Interpret.Runtime_error msg -> fatal_error msg
62: | Sys.Break -> fatal_error "Interrupted."
63: | Parsing.Parse_error | Failure("lexing: empty token") ->
64: fatal_error (Message.syntax_error lex)
65:
66:
67:
68:
69:
70: and exec_cmds n ce cmds =
71: List.fold_left (exec_cmd n) ce cmds
72: ;;
73:
74:
75:
76: let shell n ctx env =
77: print_string ("Levy. Press ") ;
78: print_string (match Sys.os_type with
79: "Unix" | "Cygwin" -> "Ctrl-D"
80: | "Win32" -> "Ctrl-Z"
81: | _ -> "EOF") ;
82: print_endline " to exit." ;
83: let global_ctx = ref ctx in
84: let global_env = ref env in
85: try
86: while true do
87: try
88:
89: print_string "Levy> ";
90: let str = read_line () in
91: let lex = Message.lexer_from_string str in
92: let cmds =
93: try
94: Parser.toplevel Lexer.token lex
95: with
96: | Failure("lexing: empty token")
97: | Parsing.Parse_error -> fatal_error (Message.syntax_error lex)
98: in
99: let (ctx, env) = exec_cmds n (!global_ctx, !global_env) cmds in
100:
101: global_ctx := ctx ;
102: global_env := env
103: with
104: Fatal_error msg -> Message.report msg
105: | Interpret.Runtime_error msg -> Message.report msg
106: | Type_check.Type_error msg -> Message.report msg
107: | Sys.Break -> Message.report ("Interrupted.")
108: done
109: with
110: End_of_file -> print_endline "\nGood bye."
111:
112:
113: let main =
114: Sys.catch_break true ;
115: let print_depth = ref 100 in
116: let noninteractive = ref false in
117: let files = ref [] in
118: Arg.parse
119: [("-n", Arg.Set noninteractive, "do not run the interactive shell");
120: ("-p", Arg.Int (fun n -> print_depth := n), "set print depth")]
121: (fun f -> files := f :: !files)
122: "Usage: levy [-p <int>] [-n] [file] ..." ;
123: files := List.rev !files ;
124: let ctx, env =
125: try
126: List.fold_left (exec_file !print_depth) ([],[]) !files
127: with
128: Fatal_error msg -> Message.report msg ; exit 1
129: in
130: if not !noninteractive then shell !print_depth ctx env