Mercurial > urweb

annotate src/reduce_local.sml @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hooks for measuring how much interesting proving is going on in elaboration
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Nov 2009 12:44:14 -0500
parents dfe34fad749d
children 3bc726a822fb
rev   line source
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