Mercurial > urweb

comparison src/reduce.sml @ 20:1ab48e37d0ef

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Some con reducing
author Adam Chlipala <adamc@hcoop.net>
date Sun, 08 Jun 2008 15:47:44 -0400
parents
children 067029c748e9
comparison
equal deleted inserted replaced
19:e634ae817a8e 20:1ab48e37d0ef
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 Core program algebraically *)
29
30 structure Reduce :> REDUCE = struct
31
32 open Core
33
34 structure E = CoreEnv
35 structure U = CoreUtil
36
37 val liftConInCon = E.liftConInCon
38
39 val subConInCon =
40 U.Con.mapB {kind = fn k => k,
41 con = fn (xn, rep) => fn c =>
42 case c of
43 CRel xn' =>
44 if xn = xn' then
45 #1 rep
46 else
47 c
48 | _ => c,
49 bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
50 | (ctx, _) => ctx}
51
52 fun bindC (env, b) =
53 case b of
54 U.Con.Rel (x, k) => E.pushCRel env x k
55 | U.Con.Named (x, n, k, co) => E.pushCNamed env x n k co
56
57 fun bind (env, b) =
58 case b of
59 U.Decl.RelC (x, k) => E.pushCRel env x k
60 | U.Decl.NamedC (x, n, k, co) => E.pushCNamed env x n k co
61 | U.Decl.RelE (x, t) => E.pushERel env x t
62 | U.Decl.NamedE (x, n, t, eo) => E.pushENamed env x n t eo
63
64 fun kind k = k
65
66 fun con env c =
67 case c of
68 CApp ((CAbs (_, _, c1), loc), c2) =>
69 #1 (reduceCon env (subConInCon (0, c2) c1))
70 | CNamed n =>
71 (case E.lookupCNamed env n of
72 (_, _, SOME c') => #1 c'
73 | _ => c)
74 | CConcat ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => CRecord (k, xcs1 @ xcs2)
75 | _ => c
76
77 and reduceCon env = U.Con.mapB {kind = kind, con = con, bind = bindC} env
78
79 fun exp env e = e
80
81 fun decl env d = d
82
83 val reduce = U.File.mapB {kind = kind, con = con, exp = exp, decl = decl, bind = bind} CoreEnv.basis
84
85 end