diff lab2/check.ml @ 0:bfdcc3820b32

Basis
author Mike Spivey <mike@cs.ox.ac.uk>
date Thu, 05 Oct 2017 08:04:15 +0100
parents
children
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lab2/check.ml	Thu Oct 05 08:04:15 2017 +0100
@@ -0,0 +1,132 @@
+(* lab2/check.ml *)
+(* Copyright (c) 2017 J. M. Spivey *)
+
+open Print 
+open Keiko
+open Tree 
+open Dict 
+
+(* |err_line| -- line number for error messages *)
+let err_line = ref 1
+
+(* |Semantic_error| -- exception raised if error detected *)
+exception Semantic_error of string * Print.arg list * int
+
+(* |sem_error| -- issue error message by raising exception *)
+let sem_error fmt args = 
+  raise (Semantic_error (fmt, args, !err_line))
+
+(* |accum| -- fold_left with arguments swapped *)
+let rec accum f xs a =
+  match xs with
+      [] -> a
+    | y::ys -> accum f ys (f y a)
+
+(* |lookup_def| -- find definition of a name, give error is none *)
+let lookup_def x env =
+  err_line := x.x_line;
+  try let d = lookup x.x_name env in x.x_def <- Some d; d.d_type with 
+    Not_found -> sem_error "$ is not declared" [fStr x.x_name]
+
+(* |add_def| -- add definition to env, give error if already declared *)
+let add_def d env =
+  try define d env with 
+    Exit -> sem_error "$ is already declared" [fStr d.d_tag]
+
+(* |type_error| -- report a type error.  The message could be better. *)
+let type_error () = sem_error "type mismatch in expression" []
+
+(* |check_monop| -- check a unary operator and return its type *)
+let check_monop w t =
+  match w with
+      Uminus ->
+        if t <> Integer then type_error ();
+        Integer
+    | Not ->
+        if t <> Boolean then type_error ();
+        Boolean
+    | _ -> failwith "bad monop"
+
+(* |check_binop| -- check a binary operator and return its type *)
+let check_binop w ta tb =
+  match w with
+      Plus | Minus | Times | Div | Mod ->
+        if ta <> Integer || tb <> Integer then type_error ();
+        Integer
+    | Eq | Lt | Gt | Leq | Geq | Neq ->
+        if ta <> tb then type_error ();
+        Boolean
+    | And | Or ->
+        if ta <> Boolean || tb <> Boolean then type_error ();
+        Boolean
+    | _ -> failwith "bad binop"
+
+(* |check_expr| -- check and annotate an expression *)
+let rec check_expr e env =
+  let t = expr_type e env in
+  (e.e_type <- t; t)
+
+(* |expr_type| -- check an expression and return its type *)
+and expr_type e env = 
+  match e.e_guts with
+      Variable x -> 
+        lookup_def x env
+    | Sub (v, e) ->
+        failwith "subscripts not implemented"
+    | Constant (n, t) -> t
+    | Monop (w, e1) -> 
+        let t = check_expr e1 env in
+        check_monop w t
+    | Binop (w, e1, e2) -> 
+        let ta = check_expr e1 env
+        and tb = check_expr e2 env in
+        check_binop w ta tb
+
+(* |check_stmt| -- check and annotate a statement *)
+let rec check_stmt s env =
+  match s with
+      Skip -> ()
+    | Seq ss ->
+        List.iter (fun s1 -> check_stmt s1 env) ss
+    | Assign (lhs, rhs) ->
+        let ta = check_expr lhs env
+        and tb = check_expr rhs env in
+        if ta <> tb then sem_error "type mismatch in assignment" []
+    | Print e ->
+        let t = check_expr e env in
+        if t <> Integer then sem_error "print needs an integer" []
+    | Newline ->
+        ()
+    | IfStmt (cond, thenpt, elsept) ->
+        let t = check_expr cond env in
+        if t <> Boolean then
+          sem_error "boolean needed in if statement" [];
+        check_stmt thenpt env; 
+        check_stmt elsept env
+    | WhileStmt (cond, body) ->
+        let t = check_expr cond env in
+        if t <> Boolean then
+          sem_error "need boolean after while" [];
+        check_stmt body env
+
+(* |make_def| -- construct definition of variable *)
+let make_def x t a = { d_tag = x; d_type = t; d_lab = a }
+
+(* |check_decl| -- check declaration and return extended environment *)
+let check_decl (Decl (vs, t)) env0 =
+  let declare x env = 
+    let lab = sprintf "_$" [fStr x.x_name] in
+    let d = make_def x.x_name t lab in
+    x.x_def <- Some d; add_def d env in
+  accum declare vs env0
+
+(* |check_decls| -- check a sequence of declarations *)
+let check_decls ds env0 =
+  accum check_decl ds env0
+
+(* |annotate| -- check and annotate a program *)
+let annotate (Program (ds, ss)) =
+  let env = check_decls ds init_env in
+  check_stmt ss env
+
+