type checking

src/exec.ml

@@ -2,42 +2,48 @@ open Types
 
 let update m x v = fun y -> if x=y then v else m y
 
-let rec _builtin_iop: 'a. ('a->exp) -> (int->int->'a) -> value =
-  fun ret f ->
-    let iop1 m v =
-      match m "", v with
-      | VInt a, VInt b -> ret (f a b)
-      | _, _ -> raise (Failure "not int") in
-    VFn (builtin, "", EFnB iop1)
-and builtin_iop x = _builtin_iop (fun x -> EInt x) x
-and builtin_cop a = _builtin_iop (fun x -> EBool x) a
-and builtin_bop f =
+let bot x = raise (Failure "undefined var")
+let _builtin_iop ret c f =
+  let iop1 m v =
+    match m "", v with
+    | VInt a, VInt b -> c (f a b)
+    | _, _ -> raise (Failure "not int") in
+  (TFn (TInt, TFn (TInt, ret)),
+  VFn (bot, "", EFnB (TInt, ret, iop1)))
+let builtin_iop x = _builtin_iop TInt (fun x -> EInt x) x
+let builtin_cop a = _builtin_iop TBool (fun x -> EBool x) a
+let builtin_bop f =
   let bop1 m v =
     match m "", v with
     | VBool a, VBool b -> EBool (f a b)
     | _, _ -> raise (Failure "not bool") in
-  VFn (builtin, "", EFnB bop1)
-and builtin = function
-  | "add" -> builtin_iop (+)
-  | "sub" -> builtin_iop (-)
-  | "mul" -> builtin_iop ( * )
-  | "div" -> builtin_iop (/)
-  | "lt" -> builtin_cop (<)
-  | "gt" -> builtin_cop (>)
-  | "ge" -> builtin_cop (>=)
-  | "le" -> builtin_cop (<=)
-  | "eq" -> builtin_cop (=)
-  | "and" -> builtin_bop (&&)
-  | "or" -> builtin_bop (||)
-  | _ -> raise (Failure "undefined var")
+  (TFn (TBool, TFn (TBool, TBool)),
+  VFn (bot, "", EFnB (TBool, TBool, bop1)))
+let builtins = [
+  ("add", builtin_iop (+));
+  ("sub", builtin_iop (-));
+  ("mul", builtin_iop ( * ));
+  ("div", builtin_iop (/));
+  ("lt", builtin_cop (<));
+  ("gt", builtin_cop (>));
+  ("le", builtin_cop (<=));
+  ("ge", builtin_cop (>=));
+  ("eq", builtin_cop (=));
+  ("and", builtin_bop (&&));
+  ("or", builtin_bop (||));
+]
+let builtin_mem =
+  let l = List.map (function(x,(_,v))->(x,v)) builtins in
+  fun x -> List.assoc x l
+let builtin_typctx = List.map (function(x,(t,_))->(x,(t,true))) builtins
 
 let rec eval (m: mem) (e: exp) : value =
   match e with
   | EInt i -> VInt i
   | EBool b -> VBool b
   | EVar x -> m x
-  | EFn (x, e) -> VFn (m, x, e)
-  | EFnB f -> VFnB (m, f)
+  | EFn (x, _, e) -> VFn (m, x, e)
+  | EFnB (_, _, f) -> VFnB (m, f)
   | EApp (e1, e2) ->
       (match eval m e1, eval m e2 with
       | VFn (m, x, body), v -> eval (update m x v) body
@@ -55,3 +61,4 @@ and exec (m: mem) (s: stmt) =
       let v = eval m e in
       v, update m x v
   | SSeq (s1, s2) -> exec (snd (exec m s1)) s2
+  | SDecl _ -> (VInt 0,m)

src/lexer.mll

@@ -8,6 +8,7 @@ rule token = parse
   | ')' { RPAREN }
   | '{' { LBRACE }
   | '}' { RBRACE }
+  | ':' { COLON }
   | ';' { SEMICOLON }
   | '=' { EQUAL }
   | '+' { PLUS }
@@ -21,11 +22,13 @@ rule token = parse
   | "==" { EQ }
   | "&&" { AND }
   | "||" { OR }
+  | "->" { ARROW }
   | "if" { IF }
   | "then" { THEN }
   | "else" { ELSE }
   | "true" { TRUE }
   | "false" { FALSE }
+  | "let" { LET }
   | "fn" { FN }
   | ['0'-'9']+ { NUM (int_of_string (Lexing.lexeme lexbuf)) }
   | ['A'-'Z' 'a'-'z' '_'] (['A'-'Z' 'a'-'z' '0'-'9' '_'])*

src/main.ml

@@ -1,6 +1,7 @@
 let main () =
   let s = Parser.parse_stmt Lexer.token
     (Lexing.from_channel (open_in Sys.argv.(1))) in
-  print_endline (Types.show_stmt s);
-  print_endline (Types.show_value (fst (Exec.exec Exec.builtin s)));;
+  if Option.is_none (Types.typchk_stmt Exec.builtin_typctx s)
+  then print_endline "type error"
+  else print_endline (Types.show_value (fst (Exec.exec Exec.builtin_mem s)));;
 main ();;

src/parser.mly

@@ -2,15 +2,19 @@
   open Types
   let app2 x a b = EApp (EApp (EVar x, a), b)
 %}
-%token LPAREN RPAREN LBRACE RBRACE SEMICOLON EQUAL OR AND PLUS MINUS TIMES DIVIDE EOF
-%token IF THEN ELSE TRUE FALSE FN LT GT LE GE EQ
+%token LPAREN RPAREN LBRACE RBRACE
+%token SEMICOLON COLON EQUAL ARROW
+%token OR AND PLUS MINUS TIMES DIVIDE LT GT LE GE EQ
+%token IF THEN ELSE TRUE FALSE FN LET EOF
 %token<int> NUM
 %token<string> VAR
 
+%nonassoc SEMICOLON
 %nonassoc EQUAL IF THEN ELSE
 %left OR
 %left AND
 %right NOT
+%nonassoc COLON
 %nonassoc TRUE FALSE
 %left PLUS MINUS
 %left TIMES DIVIDE
@@ -18,12 +22,24 @@
 %nonassoc NUM VAR
 %right LPAREN RPAREN
 %nonassoc EOF
+%right ARROW
 
 %start parse_stmt
 %type<Types.stmt> parse_stmt
 
 %%
 
+parse_typ:
+  | parse_typ ARROW parse_typ { TFn ($1,$3) }
+  | typ { $1 }
+
+typ:
+  | LPAREN parse_typ RPAREN { $2 }
+  | VAR { match $1 with
+      | "int" -> TInt
+      | "bool" -> TBool
+      | _ -> raise (Failure "invalid type") }
+
 parse_stmt:
   | stmt { $1 }
   | stmt SEMICOLON parse_stmt { SSeq ($1,$3) }
@@ -31,6 +47,10 @@ parse_stmt:
 stmt:
   | parse_exp { SExp $1 }
   | VAR EQUAL parse_exp { SAsgn ($1,$3) }
+  | LET VAR COLON parse_typ
+      { SDecl ($2,$4) }
+  | LET VAR COLON parse_typ EQUAL parse_exp
+      { SSeq (SDecl ($2,$4), SAsgn ($2,$6)) }
 
 parse_exp:
   | exp { $1 }
@@ -59,8 +79,8 @@ parse_exp:
       { app2 "ge" $1 $3 }
   | parse_exp EQ parse_exp
       { app2 "eq" $1 $3 }
-  | FN VAR parse_exp
-      { EFn ($2,$3) }
+  | FN LPAREN VAR COLON parse_typ RPAREN parse_exp
+      { EFn ($3,$5,$7) }
   | LBRACE parse_stmt RBRACE { EScope $2 }
 
 exp:

src/types.ml

@@ -1,12 +1,22 @@
 type var = string
 [@@deriving show]
 
+type typ =
+  | TInt
+  | TBool
+  | TFn of (typ * typ)
+[@@deriving show]
+
+type typctx = (var * (typ * bool)) list
+let tc_lookup: _ -> typctx -> _ = List.assoc_opt
+let tc_update x t (tc: typctx) = (x, t)::tc
+
 type exp =
   | EInt of int
   | EBool of bool
   | EVar of var
-  | EFn of (var * exp)
-  | EFnB of fnb
+  | EFn of (var * typ * exp)
+  | EFnB of (typ * typ * fnb)
   | EApp of (exp * exp)
   | EIf of (exp * exp * exp)
   | EScope of stmt
@@ -14,6 +24,7 @@ type exp =
 and stmt =
   | SExp of exp
   | SAsgn of (var * exp)
+  | SDecl of (var * typ)
   | SSeq of (stmt * stmt)
 [@@deriving show]
 and mem = var -> value
@@ -24,3 +35,51 @@ and value =
   | VFn of (mem * var * exp)
   | VFnB of (mem * fnb)
 [@@deriving show]
+
+let rec typchk_exp tc = function
+  | EInt _ -> Some TInt
+  | EBool _ -> Some TBool
+  | EVar x ->
+      (match tc_lookup x tc with
+      | Some (t, true) -> Some t
+      | _ -> None)
+  | EFn (x, t, e) ->
+      let tc' = tc_update x (t, true) tc in
+      let t' = typchk_exp tc' e in
+      Option.map (fun t' -> TFn (t, t')) t'
+  | EFnB (t, t', fnb) -> Some (TFn (t, t'))
+  | EApp (e1, e2) ->
+      (match typchk_exp tc e1 with
+      | Some (TFn (t, t')) ->
+          if Some t=typchk_exp tc e2
+          then Some t'
+          else None
+      | _ -> None)
+  | EIf (b, e1, e2) ->
+      (match typchk_exp tc b with
+      | Some TBool ->
+          let t1 = typchk_exp tc e1 in
+          let t2 = typchk_exp tc e2 in
+          if t1=t2 then t1 else None
+      | _ -> None)
+  | EScope s ->
+      (match typchk_stmt tc s with
+      | Some (t, _) -> Some t
+      | _ -> None)
+and typchk_stmt tc = function
+  | SExp e ->
+      (match typchk_exp tc e with
+      | Some t -> Some (t, tc)
+      | _ -> None)
+  | SAsgn (x, e) ->
+      (match tc_lookup x tc, typchk_exp tc e with
+      | Some (t,_), Some t' ->
+              if t=t'
+              then Some (t, tc_update x (t,true) tc)
+              else None
+      | _ -> None)
+  | SDecl (x, t) -> Some (TInt, tc_update x (t,false) tc)
+  | SSeq (s1, s2) ->
+      (match typchk_stmt tc s1 with
+      | Some (_, tc') -> typchk_stmt tc' s2
+      | _ -> None)