annotate lab4/simp.ml @ 0:bfdcc3820b32

Basis
author Mike Spivey <mike@cs.ox.ac.uk>
date Thu, 05 Oct 2017 08:04:15 +0100
parents
children
rev   line source
0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1 (* lab4/simp.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 Optree
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
5
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
6 (* |exact_log2| -- return log2 of argument, or raise Not_found *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
7 let exact_log2 x =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
8 let rec loop y i =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
9 if y = 1 then i
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
10 else if y mod 2 <> 0 then raise Not_found
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
11 else loop (y/2) (i+1) in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
12 if x <= 0 then raise Not_found;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
13 loop x 0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
14
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
15 (* |swap| -- find reverse operation or raise Not_found *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
16 let swap =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
17 function Plus -> Plus | Times -> Times | Eq -> Eq | Lt -> Gt
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
18 | Gt -> Lt | Leq -> Geq | Geq -> Leq | Neq -> Neq
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
19 | And -> And | Or -> Or
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
20 | _ -> raise Not_found
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
21
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
22 (* |is_const| -- test if expression is a constant *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
23 let is_const = function <CONST a> -> true | _ -> false
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
24
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
25 (* |simp| -- simplify an expression tree at the root *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
26 let rec simp t =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
27 match t with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
28 (* Constant folding *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
29 <BINOP w, <CONST a>, <CONST b>> ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
30 <CONST (do_binop w a b)>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
31 | <MONOP w, <CONST a>> ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
32 <CONST (do_monop w a)>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
33
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
34 (* Static bound checks *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
35 | <BOUND, <CONST k>, <CONST b>> ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
36 if 0 <= k && k < b then <CONST k> else t
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
37
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
38 (* Simplifications -- mainly directed at addressing calculations *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
39 | <BINOP Plus, t1, <CONST a>> when a < 0 ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
40 <BINOP Minus, t1, <CONST (-a)>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
41 | <BINOP Minus, t1, <CONST a>> when a < 0 ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
42 <BINOP Plus, t1, <CONST (-a)>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
43
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
44 | <OFFSET, <LOCAL a>, <CONST b>> ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
45 <LOCAL (a+b)>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
46 | <OFFSET, <OFFSET, t1, <CONST a>>, <CONST b>> ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
47 simp <OFFSET, t1, <CONST (a+b)>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
48 | <OFFSET, t1, <CONST 0>> ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
49 t1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
50 | <BINOP Times, <BINOP Times, t1, <CONST a>>, <CONST b>> ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
51 simp <BINOP Times, t1, <CONST (a * b)>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
52 | <BINOP Times, <BINOP Plus, t1, <CONST a>>, <CONST b>> ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
53 simp <BINOP Plus,
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
54 simp <BINOP Times, t1, <CONST b>>,
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
55 <CONST (a*b)>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
56 | <BINOP Times, <BINOP Minus, t1, <CONST a>>, <CONST b>> ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
57 simp <BINOP Minus,
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
58 simp <BINOP Times, t1, <CONST b>>,
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
59 <CONST (a*b)>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
60 | <OFFSET, t1, <BINOP Plus, t2, t3>> ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
61 simp <OFFSET, simp <OFFSET, t1, t2>, t3>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
62 | <OFFSET, t1, <BINOP Minus, t2, <CONST n>>> ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
63 simp <OFFSET, simp <OFFSET, t1, t2>, <CONST (-n)>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
64 | <BINOP Times, t1, <CONST 1>> -> t1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
65 | <BINOP Times, t1, <CONST n>> when n > 0 ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
66 (try
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
67 let k = exact_log2 n in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
68 <BINOP Lsl, t1, <CONST k>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
69 with Not_found -> t)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
70 | <BINOP Plus, t1, <CONST 0>> -> t1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
71 | <BINOP Minus, t1, <CONST 0>> -> t1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
72
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
73 (* Swap operands to put constant on right *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
74 | <BINOP w, <CONST a>, t2> ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
75 if is_const t2 || not (Util.can swap w) then t else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
76 simp <BINOP (swap w), t2, <CONST a>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
77 | <JUMPC (w, lab), <CONST a>, t2> ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
78 if is_const t2 then t else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
79 simp <JUMPC (swap w, lab), t2, <CONST a>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
80
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
81 | _ -> t
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
82
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
83 (* |simplify| -- recursively simplify an expression *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
84 let rec simplify <x, @ts> = simp <x, @(List.map simplify ts)>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
85
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
86 (* |optimise| -- simplify a procedure body *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
87 let optimise prog =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
88 List.map simplify prog
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
89