adamc@133
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@133
|
2 * All rights reserved.
|
adamc@133
|
3 *
|
adamc@133
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@133
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@133
|
6 *
|
adamc@133
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@133
|
8 * this list of conditions and the following disclaimer.
|
adamc@133
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@133
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@133
|
11 * and/or other materials provided with the distribution.
|
adamc@133
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@133
|
13 * derived from this software without specific prior written permission.
|
adamc@133
|
14 *
|
adamc@133
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@133
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@133
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@133
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@133
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@133
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@133
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@133
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@133
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@133
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@133
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@133
|
26 *)
|
adamc@133
|
27
|
adamc@133
|
28 (* Simplify a Mono program algebraically *)
|
adamc@133
|
29
|
adamc@133
|
30 structure MonoReduce :> MONO_REDUCE = struct
|
adamc@133
|
31
|
adamc@133
|
32 open Mono
|
adamc@133
|
33
|
adamc@133
|
34 structure E = MonoEnv
|
adamc@133
|
35 structure U = MonoUtil
|
adamc@133
|
36
|
adamc@133
|
37 val liftExpInExp =
|
adamc@133
|
38 U.Exp.mapB {typ = fn t => t,
|
adamc@133
|
39 exp = fn bound => fn e =>
|
adamc@133
|
40 case e of
|
adamc@133
|
41 ERel xn =>
|
adamc@133
|
42 if xn < bound then
|
adamc@133
|
43 e
|
adamc@133
|
44 else
|
adamc@133
|
45 ERel (xn + 1)
|
adamc@133
|
46 | _ => e,
|
adamc@133
|
47 bind = fn (bound, U.Exp.RelE _) => bound + 1
|
adamc@133
|
48 | (bound, _) => bound}
|
adamc@133
|
49
|
adamc@133
|
50 val subExpInExp =
|
adamc@133
|
51 U.Exp.mapB {typ = fn t => t,
|
adamc@133
|
52 exp = fn (xn, rep) => fn e =>
|
adamc@133
|
53 case e of
|
adamc@133
|
54 ERel xn' =>
|
adamc@133
|
55 (case Int.compare (xn', xn) of
|
adamc@133
|
56 EQUAL => #1 rep
|
adamc@133
|
57 | GREATER=> ERel (xn' - 1)
|
adamc@133
|
58 | LESS => e)
|
adamc@133
|
59 | _ => e,
|
adamc@133
|
60 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
|
adamc@133
|
61 | (ctx, _) => ctx}
|
adamc@133
|
62
|
adamc@133
|
63 fun bind (env, b) =
|
adamc@133
|
64 case b of
|
adamc@168
|
65 U.Decl.Datatype (x, n, xncs) => E.pushDatatype env x n xncs
|
adamc@183
|
66 | U.Decl.RelE (x, t) => E.pushERel env x t NONE
|
adamc@133
|
67 | U.Decl.NamedE (x, n, t, eo, s) => E.pushENamed env x n t eo s
|
adamc@133
|
68
|
adamc@133
|
69 fun typ c = c
|
adamc@133
|
70
|
adamc@183
|
71 fun match (env, p : pat, e : exp) =
|
adamc@183
|
72 case (#1 p, #1 e) of
|
adamc@183
|
73 (PWild, _) => SOME env
|
adamc@183
|
74 | (PVar (x, t), _) => SOME (E.pushERel env x t (SOME e))
|
adamc@183
|
75
|
adamc@183
|
76 | (PPrim p, EPrim p') =>
|
adamc@183
|
77 if Prim.equal (p, p') then
|
adamc@183
|
78 SOME env
|
adamc@183
|
79 else
|
adamc@183
|
80 NONE
|
adamc@183
|
81
|
adamc@185
|
82 | (PCon (PConVar n1, NONE), ECon (PConVar n2, NONE)) =>
|
adamc@183
|
83 if n1 = n2 then
|
adamc@183
|
84 SOME env
|
adamc@183
|
85 else
|
adamc@183
|
86 NONE
|
adamc@183
|
87
|
adamc@185
|
88 | (PCon (PConVar n1, SOME p), ECon (PConVar n2, SOME e)) =>
|
adamc@183
|
89 if n1 = n2 then
|
adamc@183
|
90 match (env, p, e)
|
adamc@183
|
91 else
|
adamc@183
|
92 NONE
|
adamc@183
|
93
|
adamc@185
|
94 | (PCon (PConFfi {mod = m1, con = con1, ...}, NONE), ECon (PConFfi {mod = m2, con = con2, ...}, NONE)) =>
|
adamc@185
|
95 if m1 = m2 andalso con1 = con2 then
|
adamc@185
|
96 SOME env
|
adamc@185
|
97 else
|
adamc@185
|
98 NONE
|
adamc@185
|
99
|
adamc@185
|
100 | (PCon (PConFfi {mod = m1, con = con1, ...}, SOME ep), ECon (PConFfi {mod = m2, con = con2, ...}, SOME e)) =>
|
adamc@185
|
101 if m1 = m2 andalso con1 = con2 then
|
adamc@185
|
102 match (env, p, e)
|
adamc@185
|
103 else
|
adamc@185
|
104 NONE
|
adamc@185
|
105
|
adamc@183
|
106 | (PRecord xps, ERecord xes) =>
|
adamc@183
|
107 let
|
adamc@183
|
108 fun consider (xps, env) =
|
adamc@183
|
109 case xps of
|
adamc@183
|
110 [] => SOME env
|
adamc@183
|
111 | (x, p, _) :: rest =>
|
adamc@183
|
112 case List.find (fn (x', _, _) => x' = x) xes of
|
adamc@183
|
113 NONE => NONE
|
adamc@183
|
114 | SOME (_, e, _) =>
|
adamc@183
|
115 case match (env, p, e) of
|
adamc@183
|
116 NONE => NONE
|
adamc@183
|
117 | SOME env => consider (rest, env)
|
adamc@183
|
118 in
|
adamc@183
|
119 consider (xps, env)
|
adamc@183
|
120 end
|
adamc@183
|
121
|
adamc@183
|
122 | _ => NONE
|
adamc@183
|
123
|
adamc@133
|
124 fun exp env e =
|
adamc@133
|
125 case e of
|
adamc@183
|
126 ERel n =>
|
adamc@183
|
127 (case E.lookupERel env n of
|
adamc@183
|
128 (_, _, SOME e') => #1 e'
|
adamc@183
|
129 | _ => e)
|
adamc@183
|
130 | ENamed n =>
|
adamc@133
|
131 (case E.lookupENamed env n of
|
adamc@133
|
132 (_, _, SOME e', _) => #1 e'
|
adamc@133
|
133 | _ => e)
|
adamc@133
|
134
|
adamc@133
|
135 | EApp ((EAbs (_, _, _, e1), loc), e2) =>
|
adamc@133
|
136 #1 (reduceExp env (subExpInExp (0, e2) e1))
|
adamc@133
|
137
|
adamc@184
|
138 | ECase (disc, pes, _) =>
|
adamc@183
|
139 (case ListUtil.search (fn (p, body) =>
|
adamc@183
|
140 case match (env, p, disc) of
|
adamc@183
|
141 NONE => NONE
|
adamc@183
|
142 | SOME env => SOME (#1 (reduceExp env body))) pes of
|
adamc@183
|
143 NONE => e
|
adamc@183
|
144 | SOME e' => e')
|
adamc@183
|
145
|
adamc@133
|
146 | _ => e
|
adamc@133
|
147
|
adamc@133
|
148 and reduceExp env = U.Exp.mapB {typ = typ, exp = exp, bind = bind} env
|
adamc@133
|
149
|
adamc@133
|
150 fun decl env d = d
|
adamc@133
|
151
|
adamc@133
|
152 val reduce = U.File.mapB {typ = typ, exp = exp, decl = decl, bind = bind} E.empty
|
adamc@133
|
153
|
adamc@133
|
154 end
|