adamc@482
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@482
|
2 * All rights reserved.
|
adamc@482
|
3 *
|
adamc@482
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@482
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@482
|
6 *
|
adamc@482
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@482
|
8 * this list of conditions and the following disclaimer.
|
adamc@482
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@482
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@482
|
11 * and/or other materials provided with the distribution.
|
adamc@482
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@482
|
13 * derived from this software without specific prior written permission.
|
adamc@482
|
14 *
|
adamc@482
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@482
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@482
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@482
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@482
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@482
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@482
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@482
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@482
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@482
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@482
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@482
|
26 *)
|
adamc@482
|
27
|
adamc@482
|
28 (* Simplify a Core program algebraically, without unfolding definitions *)
|
adamc@482
|
29
|
adamc@482
|
30 structure ReduceLocal :> REDUCE_LOCAL = struct
|
adamc@482
|
31
|
adamc@482
|
32 open Core
|
adamc@482
|
33
|
adamc@512
|
34 structure IM = IntBinaryMap
|
adamc@482
|
35
|
adamc@512
|
36 datatype env_item =
|
adamc@512
|
37 Unknown
|
adamc@512
|
38 | Known of exp
|
adamc@482
|
39
|
adamc@512
|
40 | Lift of int
|
adamc@482
|
41
|
adamc@512
|
42 type env = env_item list
|
adamc@512
|
43
|
adamc@512
|
44 val deKnown = List.filter (fn Known _ => false
|
adamc@512
|
45 | _ => true)
|
adamc@512
|
46
|
adamc@512
|
47 fun exp env (all as (e, loc)) =
|
adamc@512
|
48 case e of
|
adamc@512
|
49 EPrim _ => all
|
adamc@512
|
50 | ERel n =>
|
adamc@512
|
51 let
|
adamc@512
|
52 fun find (n', env, nudge, lift) =
|
adamc@512
|
53 case env of
|
adamc@642
|
54 [] => (ERel (n + nudge), loc)
|
adamc@512
|
55 | Lift lift' :: rest => find (n', rest, nudge + lift', lift + lift')
|
adamc@512
|
56 | Unknown :: rest =>
|
adamc@512
|
57 if n' = 0 then
|
adamc@512
|
58 (ERel (n + nudge), loc)
|
adamc@512
|
59 else
|
adamc@512
|
60 find (n' - 1, rest, nudge, lift + 1)
|
adamc@512
|
61 | Known e :: rest =>
|
adamc@512
|
62 if n' = 0 then
|
adamc@512
|
63 ((*print "SUBSTITUTING\n";*)
|
adamc@512
|
64 exp (Lift lift :: rest) e)
|
adamc@512
|
65 else
|
adamc@512
|
66 find (n' - 1, rest, nudge - 1, lift)
|
adamc@512
|
67 in
|
adamc@512
|
68 find (n, env, 0, 0)
|
adamc@512
|
69 end
|
adamc@512
|
70 | ENamed _ => all
|
adamc@512
|
71 | ECon (dk, pc, cs, eo) => (ECon (dk, pc, cs, Option.map (exp env) eo), loc)
|
adamc@512
|
72 | EFfi _ => all
|
adamc@512
|
73 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
|
adamc@512
|
74
|
adamc@721
|
75 | EApp ((ECApp ((ECAbs (_, _, (EAbs (_, (CRel 0, _), _,
|
adamc@721
|
76 (ECon (dk, pc, [(CRel 0, loc)], SOME (ERel 0, _)), _)), _)), _),
|
adamc@721
|
77 t), _), e) =>
|
adamc@721
|
78 (ECon (dk, pc, [t], SOME (exp env e)), loc)
|
adamc@721
|
79
|
adamc@512
|
80 | EApp (e1, e2) =>
|
adamc@512
|
81 let
|
adamc@512
|
82 val e1 = exp env e1
|
adamc@512
|
83 val e2 = exp env e2
|
adamc@512
|
84 in
|
adamc@512
|
85 case #1 e1 of
|
adamc@512
|
86 EAbs (_, _, _, b) => exp (Known e2 :: deKnown env) b
|
adamc@512
|
87 | _ => (EApp (e1, e2), loc)
|
adamc@512
|
88 end
|
adamc@512
|
89
|
adamc@512
|
90 | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc)
|
adamc@512
|
91
|
adamc@721
|
92 | ECApp ((ECAbs (_, _, (ECon (dk, pc, [(CRel 0, loc)], NONE), _)), _), t) =>
|
adamc@721
|
93 (ECon (dk, pc, [t], NONE), loc)
|
adamc@721
|
94
|
adamc@512
|
95 | ECApp (e, c) => (ECApp (exp env e, c), loc)
|
adamc@626
|
96 | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc)
|
adamc@512
|
97
|
adamc@626
|
98 | EKApp (e, k) => (EKApp (exp env e, k), loc)
|
adamc@626
|
99 | EKAbs (x, e) => (EKAbs (x, exp env e), loc)
|
adamc@512
|
100
|
adamc@512
|
101 | ERecord xcs => (ERecord (map (fn (x, e, t) => (x, exp env e, t)) xcs), loc)
|
adamc@512
|
102 | EField (e, c, others) =>
|
adamc@512
|
103 let
|
adamc@512
|
104 val e = exp env e
|
adamc@512
|
105
|
adamc@512
|
106 fun default () = (EField (e, c, others), loc)
|
adamc@512
|
107 in
|
adamc@512
|
108 case (#1 e, #1 c) of
|
adamc@512
|
109 (ERecord xcs, CName x) =>
|
adamc@512
|
110 (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of
|
adamc@512
|
111 NONE => default ()
|
adamc@512
|
112 | SOME (_, e, _) => e)
|
adamc@512
|
113 | _ => default ()
|
adamc@512
|
114 end
|
adamc@512
|
115
|
adamc@512
|
116 | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, c1, exp env e2, c2), loc)
|
adamc@512
|
117 | ECut (e, c, others) => (ECut (exp env e, c, others), loc)
|
adamc@512
|
118 | ECutMulti (e, c, others) => (ECutMulti (exp env e, c, others), loc)
|
adamc@512
|
119
|
adamc@512
|
120 | ECase (e, pes, others) =>
|
adamc@512
|
121 let
|
adamc@512
|
122 fun patBinds (p, _) =
|
adamc@512
|
123 case p of
|
adamc@512
|
124 PWild => 0
|
adamc@512
|
125 | PVar _ => 1
|
adamc@512
|
126 | PPrim _ => 0
|
adamc@512
|
127 | PCon (_, _, _, NONE) => 0
|
adamc@512
|
128 | PCon (_, _, _, SOME p) => patBinds p
|
adamc@512
|
129 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
|
adamc@512
|
130 in
|
adamc@512
|
131 (ECase (exp env e,
|
adamc@512
|
132 map (fn (p, e) => (p,
|
adamc@512
|
133 exp (List.tabulate (patBinds p, fn _ => Unknown) @ env) e))
|
adamc@512
|
134 pes, others), loc)
|
adamc@512
|
135 end
|
adamc@512
|
136
|
adamc@512
|
137 | EWrite e => (EWrite (exp env e), loc)
|
adamc@512
|
138 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
|
adamc@512
|
139
|
adamc@512
|
140 | ELet (x, t, e1, e2) => (ELet (x, t, exp env e1, exp (Unknown :: env) e2), loc)
|
adamc@512
|
141
|
adamc@1020
|
142 | EServerCall (n, es, t) => (EServerCall (n, map (exp env) es, t), loc)
|
adamc@607
|
143
|
adamc@512
|
144 fun reduce file =
|
adamc@482
|
145 let
|
adamc@512
|
146 fun doDecl (d as (_, loc)) =
|
adamc@512
|
147 case #1 d of
|
adamc@512
|
148 DCon _ => d
|
adamc@512
|
149 | DDatatype _ => d
|
adamc@512
|
150 | DVal (x, n, t, e, s) =>
|
adamc@512
|
151 let
|
adamc@512
|
152 val e = exp [] e
|
adamc@512
|
153 in
|
adamc@512
|
154 (DVal (x, n, t, e, s), loc)
|
adamc@512
|
155 end
|
adamc@512
|
156 | DValRec vis =>
|
adamc@512
|
157 (DValRec (map (fn (x, n, t, e, s) => (x, n, t, exp [] e, s)) vis), loc)
|
adamc@512
|
158 | DExport _ => d
|
adamc@512
|
159 | DTable _ => d
|
adamc@512
|
160 | DSequence _ => d
|
adamc@754
|
161 | DView _ => d
|
adamc@512
|
162 | DDatabase _ => d
|
adamc@512
|
163 | DCookie _ => d
|
adamc@718
|
164 | DStyle _ => d
|
adamc@482
|
165 in
|
adamc@512
|
166 map doDecl file
|
adamc@482
|
167 end
|
adamc@482
|
168
|
adamc@642
|
169 val reduceExp = exp []
|
adamc@642
|
170
|
adamc@482
|
171 end
|