annotate lab2/check.ml @ 1:b5139af1a420 tip basis

Fixed permissions on compile scripts
author Mike Spivey <mike@cs.ox.ac.uk>
date Fri, 13 Oct 2017 17:27:58 +0100
parents bfdcc3820b32
children
rev   line source
mike@0 1 (* lab2/check.ml *)
mike@0 2 (* Copyright (c) 2017 J. M. Spivey *)
mike@0 3
mike@0 4 open Print
mike@0 5 open Keiko
mike@0 6 open Tree
mike@0 7 open Dict
mike@0 8
mike@0 9 (* |err_line| -- line number for error messages *)
mike@0 10 let err_line = ref 1
mike@0 11
mike@0 12 (* |Semantic_error| -- exception raised if error detected *)
mike@0 13 exception Semantic_error of string * Print.arg list * int
mike@0 14
mike@0 15 (* |sem_error| -- issue error message by raising exception *)
mike@0 16 let sem_error fmt args =
mike@0 17 raise (Semantic_error (fmt, args, !err_line))
mike@0 18
mike@0 19 (* |accum| -- fold_left with arguments swapped *)
mike@0 20 let rec accum f xs a =
mike@0 21 match xs with
mike@0 22 [] -> a
mike@0 23 | y::ys -> accum f ys (f y a)
mike@0 24
mike@0 25 (* |lookup_def| -- find definition of a name, give error is none *)
mike@0 26 let lookup_def x env =
mike@0 27 err_line := x.x_line;
mike@0 28 try let d = lookup x.x_name env in x.x_def <- Some d; d.d_type with
mike@0 29 Not_found -> sem_error "$ is not declared" [fStr x.x_name]
mike@0 30
mike@0 31 (* |add_def| -- add definition to env, give error if already declared *)
mike@0 32 let add_def d env =
mike@0 33 try define d env with
mike@0 34 Exit -> sem_error "$ is already declared" [fStr d.d_tag]
mike@0 35
mike@0 36 (* |type_error| -- report a type error. The message could be better. *)
mike@0 37 let type_error () = sem_error "type mismatch in expression" []
mike@0 38
mike@0 39 (* |check_monop| -- check a unary operator and return its type *)
mike@0 40 let check_monop w t =
mike@0 41 match w with
mike@0 42 Uminus ->
mike@0 43 if t <> Integer then type_error ();
mike@0 44 Integer
mike@0 45 | Not ->
mike@0 46 if t <> Boolean then type_error ();
mike@0 47 Boolean
mike@0 48 | _ -> failwith "bad monop"
mike@0 49
mike@0 50 (* |check_binop| -- check a binary operator and return its type *)
mike@0 51 let check_binop w ta tb =
mike@0 52 match w with
mike@0 53 Plus | Minus | Times | Div | Mod ->
mike@0 54 if ta <> Integer || tb <> Integer then type_error ();
mike@0 55 Integer
mike@0 56 | Eq | Lt | Gt | Leq | Geq | Neq ->
mike@0 57 if ta <> tb then type_error ();
mike@0 58 Boolean
mike@0 59 | And | Or ->
mike@0 60 if ta <> Boolean || tb <> Boolean then type_error ();
mike@0 61 Boolean
mike@0 62 | _ -> failwith "bad binop"
mike@0 63
mike@0 64 (* |check_expr| -- check and annotate an expression *)
mike@0 65 let rec check_expr e env =
mike@0 66 let t = expr_type e env in
mike@0 67 (e.e_type <- t; t)
mike@0 68
mike@0 69 (* |expr_type| -- check an expression and return its type *)
mike@0 70 and expr_type e env =
mike@0 71 match e.e_guts with
mike@0 72 Variable x ->
mike@0 73 lookup_def x env
mike@0 74 | Sub (v, e) ->
mike@0 75 failwith "subscripts not implemented"
mike@0 76 | Constant (n, t) -> t
mike@0 77 | Monop (w, e1) ->
mike@0 78 let t = check_expr e1 env in
mike@0 79 check_monop w t
mike@0 80 | Binop (w, e1, e2) ->
mike@0 81 let ta = check_expr e1 env
mike@0 82 and tb = check_expr e2 env in
mike@0 83 check_binop w ta tb
mike@0 84
mike@0 85 (* |check_stmt| -- check and annotate a statement *)
mike@0 86 let rec check_stmt s env =
mike@0 87 match s with
mike@0 88 Skip -> ()
mike@0 89 | Seq ss ->
mike@0 90 List.iter (fun s1 -> check_stmt s1 env) ss
mike@0 91 | Assign (lhs, rhs) ->
mike@0 92 let ta = check_expr lhs env
mike@0 93 and tb = check_expr rhs env in
mike@0 94 if ta <> tb then sem_error "type mismatch in assignment" []
mike@0 95 | Print e ->
mike@0 96 let t = check_expr e env in
mike@0 97 if t <> Integer then sem_error "print needs an integer" []
mike@0 98 | Newline ->
mike@0 99 ()
mike@0 100 | IfStmt (cond, thenpt, elsept) ->
mike@0 101 let t = check_expr cond env in
mike@0 102 if t <> Boolean then
mike@0 103 sem_error "boolean needed in if statement" [];
mike@0 104 check_stmt thenpt env;
mike@0 105 check_stmt elsept env
mike@0 106 | WhileStmt (cond, body) ->
mike@0 107 let t = check_expr cond env in
mike@0 108 if t <> Boolean then
mike@0 109 sem_error "need boolean after while" [];
mike@0 110 check_stmt body env
mike@0 111
mike@0 112 (* |make_def| -- construct definition of variable *)
mike@0 113 let make_def x t a = { d_tag = x; d_type = t; d_lab = a }
mike@0 114
mike@0 115 (* |check_decl| -- check declaration and return extended environment *)
mike@0 116 let check_decl (Decl (vs, t)) env0 =
mike@0 117 let declare x env =
mike@0 118 let lab = sprintf "_$" [fStr x.x_name] in
mike@0 119 let d = make_def x.x_name t lab in
mike@0 120 x.x_def <- Some d; add_def d env in
mike@0 121 accum declare vs env0
mike@0 122
mike@0 123 (* |check_decls| -- check a sequence of declarations *)
mike@0 124 let check_decls ds env0 =
mike@0 125 accum check_decl ds env0
mike@0 126
mike@0 127 (* |annotate| -- check and annotate a program *)
mike@0 128 let annotate (Program (ds, ss)) =
mike@0 129 let env = check_decls ds init_env in
mike@0 130 check_stmt ss env
mike@0 131
mike@0 132