Mercurial > urweb

comparison src/mono_reduce.sml @ 133:55d8cfa4d024

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
MonoReduce
author Adam Chlipala <adamc@hcoop.net>
date Thu, 17 Jul 2008 12:59:52 -0400
parents
children 25b169416ea8
comparison
equal deleted inserted replaced
132:25b28625d4df 133:55d8cfa4d024
1 (* Copyright (c) 2008, Adam Chlipala
2 * All rights reserved.
3 *
4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met:
6 *
7 * - Redistributions of source code must retain the above copyright notice,
8 * this list of conditions and the following disclaimer.
9 * - Redistributions in binary form must reproduce the above copyright notice,
10 * this list of conditions and the following disclaimer in the documentation
11 * and/or other materials provided with the distribution.
12 * - The names of contributors may not be used to endorse or promote products
13 * derived from this software without specific prior written permission.
14 *
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25 * POSSIBILITY OF SUCH DAMAGE.
26 *)
27
28 (* Simplify a Mono program algebraically *)
29
30 structure MonoReduce :> MONO_REDUCE = struct
31
32 open Mono
33
34 structure E = MonoEnv
35 structure U = MonoUtil
36
37 val liftExpInExp =
38 U.Exp.mapB {typ = fn t => t,
39 exp = fn bound => fn e =>
40 case e of
41 ERel xn =>
42 if xn < bound then
43 e
44 else
45 ERel (xn + 1)
46 | _ => e,
47 bind = fn (bound, U.Exp.RelE _) => bound + 1
48 | (bound, _) => bound}
49
50 val subExpInExp =
51 U.Exp.mapB {typ = fn t => t,
52 exp = fn (xn, rep) => fn e =>
53 case e of
54 ERel xn' =>
55 (case Int.compare (xn', xn) of
56 EQUAL => #1 rep
57 | GREATER=> ERel (xn' - 1)
58 | LESS => e)
59 | _ => e,
60 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
61 | (ctx, _) => ctx}
62
63 fun bind (env, b) =
64 case b of
65 U.Decl.NamedT (x, n, co) => E.pushTNamed env x n co
66 | U.Decl.RelE (x, t) => E.pushERel env x t
67 | U.Decl.NamedE (x, n, t, eo, s) => E.pushENamed env x n t eo s
68
69 fun typ c = c
70
71 fun exp env e =
72 case e of
73 ENamed n =>
74 (case E.lookupENamed env n of
75 (_, _, SOME e', _) => #1 e'
76 | _ => e)
77
78 | EApp ((EAbs (_, _, _, e1), loc), e2) =>
79 #1 (reduceExp env (subExpInExp (0, e2) e1))
80
81 | _ => e
82
83 and reduceExp env = U.Exp.mapB {typ = typ, exp = exp, bind = bind} env
84
85 fun decl env d = d
86
87 val reduce = U.File.mapB {typ = typ, exp = exp, decl = decl, bind = bind} E.empty
88
89 end