|
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@133
|
66 | U.Decl.RelE (x, t) => E.pushERel env x t
|
|
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@133
|
71 fun exp env e =
|
|
adamc@133
|
72 case e of
|
|
adamc@133
|
73 ENamed n =>
|
|
adamc@133
|
74 (case E.lookupENamed env n of
|
|
adamc@133
|
75 (_, _, SOME e', _) => #1 e'
|
|
adamc@133
|
76 | _ => e)
|
|
adamc@133
|
77
|
|
adamc@133
|
78 | EApp ((EAbs (_, _, _, e1), loc), e2) =>
|
|
adamc@133
|
79 #1 (reduceExp env (subExpInExp (0, e2) e1))
|
|
adamc@133
|
80
|
|
adamc@133
|
81 | _ => e
|
|
adamc@133
|
82
|
|
adamc@133
|
83 and reduceExp env = U.Exp.mapB {typ = typ, exp = exp, bind = bind} env
|
|
adamc@133
|
84
|
|
adamc@133
|
85 fun decl env d = d
|
|
adamc@133
|
86
|
|
adamc@133
|
87 val reduce = U.File.mapB {typ = typ, exp = exp, decl = decl, bind = bind} E.empty
|
|
adamc@133
|
88
|
|
adamc@133
|
89 end
|
