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