Mercurial > urweb

annotate src/fuse.sml @ 1215:360f1ed0a969

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Implemented proper congruence closure, to the point where tests/policy works
author Adam Chlipala <adamc@hcoop.net>
date Thu, 08 Apr 2010 12:46:21 -0400
parents 9304474170ed
children c1e3805e604e
rev   line source
adamc@506 1 (* Copyright (c) 2008, Adam Chlipala
adamc@506 2 * All rights reserved.
adamc@506 3 *
adamc@506 4 * Redistribution and use in source and binary forms, with or without
adamc@506 5 * modification, are permitted provided that the following conditions are met:
adamc@506 6 *
adamc@506 7 * - Redistributions of source code must retain the above copyright notice,
adamc@506 8 * this list of conditions and the following disclaimer.
adamc@506 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@506 10 * this list of conditions and the following disclaimer in the documentation
adamc@506 11 * and/or other materials provided with the distribution.
adamc@506 12 * - The names of contributors may not be used to endorse or promote products
adamc@506 13 * derived from this software without specific prior written permission.
adamc@506 14 *
adamc@506 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@506 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@506 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@506 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@506 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@506 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@506 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@506 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@506 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@506 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@506 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@506 26 *)
adamc@506 27
adamc@506 28 structure Fuse :> FUSE = struct
adamc@506 29
adamc@506 30 open Mono
adamc@506 31 structure U = MonoUtil
adamc@506 32
adamc@506 33 structure IM = IntBinaryMap
adamc@506 34
adamc@506 35 fun returnsString (t, loc) =
adamc@506 36 let
adamc@506 37 fun rs (t, loc) =
adamc@506 38 case t of
adamc@506 39 TFfi ("Basis", "string") => SOME ([], (TRecord [], loc))
adamc@506 40 | TFun (dom, ran) =>
adamc@506 41 (case rs ran of
adamc@506 42 NONE => NONE
adamc@506 43 | SOME (args, ran') => SOME (dom :: args, (TFun (dom, ran'), loc)))
adamc@506 44 | _ => NONE
adamc@506 45 in
adamc@506 46 case t of
adamc@506 47 TFun (dom, ran) =>
adamc@506 48 (case rs ran of
adamc@506 49 NONE => NONE
adamc@506 50 | SOME (args, ran') => SOME (dom :: args, (TFun (dom, ran'), loc)))
adamc@506 51 | _ => NONE
adamc@506 52 end
adamc@506 53
adamc@506 54 fun fuse file =
adamc@506 55 let
adamc@506 56 fun doDecl (d as (_, loc), (funcs, maxName)) =
adamc@506 57 let
adamc@1018 58 exception GetBody
adamc@1018 59
adamc@1018 60 fun doVi ((x, n, t, e, s), funcs, maxName) =
adamc@1018 61 case returnsString t of
adamc@1018 62 NONE => (NONE, funcs, maxName)
adamc@1018 63 | SOME (args, t') =>
adamc@1018 64 let
adamc@1018 65 fun getBody (e, args) =
adamc@1018 66 case (#1 e, args) of
adamc@1018 67 (_, []) => (e, [])
adamc@1018 68 | (EAbs (x, t, _, e), _ :: args) =>
adamc@1018 69 let
adamc@1018 70 val (body, args') = getBody (e, args)
adamc@1018 71 in
adamc@1018 72 (body, (x, t) :: args')
adamc@1018 73 end
adamc@1018 74 | _ => raise GetBody
adamc@1018 75
adamc@1018 76 val (body, args) = getBody (e, args)
adamc@1018 77 val body = MonoOpt.optExp (EWrite body, loc)
adamc@1018 78 val (body, _) = foldr (fn ((x, dom), (body, ran)) =>
adamc@1018 79 ((EAbs (x, dom, ran, body), loc),
adamc@1018 80 (TFun (dom, ran), loc)))
adamc@1018 81 (body, (TRecord [], loc)) args
adamc@1018 82 in
adamc@1018 83 (SOME (x, maxName, t', body, s),
adamc@1018 84 IM.insert (funcs, n, maxName),
adamc@1018 85 maxName + 1)
adamc@1018 86 end
adamc@1018 87 handle GetBody => (NONE, funcs, maxName)
adamc@1018 88
adamc@506 89 val (d, funcs, maxName) =
adamc@506 90 case #1 d of
adamc@1018 91 DVal vi =>
adamc@1018 92 let
adamc@1018 93 val (vi', funcs, maxName) = doVi (vi, funcs, maxName)
adamc@1018 94 in
adamc@1018 95 (case vi' of
adamc@1018 96 NONE => d
adamc@1018 97 | SOME vi' => (DValRec [vi, vi'], loc),
adamc@1018 98 funcs, maxName)
adamc@1018 99 end
adamc@1018 100 | DValRec vis =>
adamc@506 101 let
adamc@506 102 val (vis', funcs, maxName) =
adamc@1018 103 foldl (fn (vi, (vis', funcs, maxName)) =>
adamc@1018 104 let
adamc@1018 105 val (vi', funcs, maxName) = doVi (vi, funcs, maxName)
adamc@1018 106 in
adamc@1018 107 (case vi' of
adamc@1018 108 NONE => vis'
adamc@1018 109 | SOME vi' => vi' :: vis',
adamc@1018 110 funcs, maxName)
adamc@1018 111 end)
adamc@506 112 ([], funcs, maxName) vis
adamc@506 113 in
adamc@506 114 ((DValRec (vis @ vis'), loc), funcs, maxName)
adamc@506 115 end
adamc@506 116 | _ => (d, funcs, maxName)
adamc@506 117
adamc@506 118 fun exp e =
adamc@506 119 case e of
adamc@506 120 EWrite e' =>
adamc@506 121 let
adamc@506 122 fun unravel (e, loc) =
adamc@506 123 case e of
adamc@506 124 ENamed n =>
adamc@506 125 (case IM.find (funcs, n) of
adamc@506 126 NONE => NONE
adamc@506 127 | SOME n' => SOME (ENamed n', loc))
adamc@506 128 | EApp (e1, e2) =>
adamc@506 129 (case unravel e1 of
adamc@506 130 NONE => NONE
adamc@506 131 | SOME e1 => SOME (EApp (e1, e2), loc))
adamc@506 132 | _ => NONE
adamc@506 133 in
adamc@506 134 case unravel e' of
adamc@506 135 NONE => e
adamc@506 136 | SOME (e', _) => e'
adamc@506 137 end
adamc@506 138 | _ => e
adamc@506 139 in
adamc@506 140 (U.Decl.map {typ = fn x => x,
adamc@506 141 exp = exp,
adamc@506 142 decl = fn x => x}
adamc@506 143 d,
adamc@506 144 (funcs, maxName))
adamc@506 145 end
adamc@506 146
adamc@506 147 val (file, _) = ListUtil.foldlMap doDecl (IM.empty, U.File.maxName file + 1) file
adamc@506 148 in
adamc@506 149 file
adamc@506 150 end
adamc@506 151
adamc@506 152 end