Mercurial > urweb

annotate src/sigcheck.sml @ 2244:e4a7e3cd6f11

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Use uniform representation of comparisons for better simplification.
author Ziv Scully <ziv@mit.edu>
date Mon, 20 Jul 2015 23:25:44 -0700
parents 3683d1a8c1c8
children 25874084bf1f
rev   line source
adam@1856 1 (* Copyright (c) 2013, Adam Chlipala
adam@1856 2 * All rights reserved.
adam@1856 3 *
adam@1856 4 * Redistribution and use in source and binary forms, with or without
adam@1856 5 * modification, are permitted provided that the following conditions are met:
adam@1856 6 *
adam@1856 7 * - Redistributions of source code must retain the above copyright notice,
adam@1856 8 * this list of conditions and the following disclaimer.
adam@1856 9 * - Redistributions in binary form must reproduce the above copyright notice,
adam@1856 10 * this list of conditions and the following disclaimer in the documentation
adam@1856 11 * and/or other materials provided with the distribution.
adam@1856 12 * - The names of contributors may not be used to endorse or promote products
adam@1856 13 * derived from this software without specific prior written permission.
adam@1856 14 *
adam@1856 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adam@1856 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adam@1856 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adam@1856 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adam@1856 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adam@1856 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adam@1856 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adam@1856 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adam@1856 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adam@1856 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adam@1856 25 * POSSIBILITY OF SUCH DAMAGE.
adam@1856 26 *)
adam@1856 27
adam@1856 28 structure SigCheck :> SIG_CHECK = struct
adam@1856 29
adam@1856 30 open Mono
adam@1856 31
adam@1856 32 structure IS = IntBinarySet
adam@1856 33 structure E = ErrorMsg
adam@1856 34
adam@1856 35 fun check (ds, sl) =
adam@1856 36 let
adam@1856 37 fun isSiggy siggers =
adam@1856 38 MonoUtil.Decl.exists {typ = fn _ => false,
adam@1856 39 decl = fn _ => false,
adam@1856 40 exp = fn e =>
adam@1856 41 case e of
adam@1856 42 ERel n => IS.member (siggers, n)
adam@1856 43 | EFfiApp ("Basis", "sigString", _) => true
adam@1856 44 | _ => false}
adam@1856 45
adam@1856 46 fun sigify' sigdecs e =
adam@1856 47 case e of
adam@1856 48 ENamed n => if IS.member (sigdecs, n) then
adam@1856 49 (EApp ((e, E.dummySpan),
adam@1856 50 (ERecord [], E.dummySpan)))
adam@1856 51 else
adam@1856 52 e
adam@1856 53 | _ => e
adam@1856 54
adam@1856 55 fun sigify sigdecs =
adam@1856 56 MonoUtil.Decl.map {typ = fn x => x,
adam@1856 57 decl = fn d => d,
adam@1856 58 exp = sigify' sigdecs}
adam@1856 59
adam@1856 60 fun sigifyE sigdecs =
adam@1856 61 MonoUtil.Exp.map {typ = fn x => x,
adam@1856 62 exp = sigify' sigdecs}
adam@1856 63
adam@1856 64 fun isFun (e, _) =
adam@1856 65 case e of
adam@1856 66 EAbs _ => true
adam@1856 67 | _ => false
adam@1856 68
adam@1856 69 fun doDecl (d : decl, (siggers, sigdecs)) =
adam@1856 70 case #1 d of
adam@1856 71 DVal (x, n, t, e, s) =>
adam@1856 72 if isSiggy siggers d then
adam@1856 73 if isFun e then
adam@1856 74 (sigify sigdecs d, (IS.add (siggers, n), sigdecs))
adam@1856 75 else
adam@1856 76 ((DVal (x, n, (TFun ((TRecord [], #2 d), t), #2 d),
adam@1856 77 (EAbs ("_", (TRecord [], #2 d), t, sigifyE sigdecs e), #2 d),
adam@1856 78 s), #2 d),
adam@1856 79 (IS.add (siggers, n),
adam@1856 80 IS.add (sigdecs, n)))
adam@1856 81 else
adam@1856 82 (sigify sigdecs d, (siggers, sigdecs))
adam@1856 83 | DValRec vis =>
adam@1856 84 if isSiggy siggers d then
adam@1856 85 (sigify sigdecs d,
adam@1856 86 (foldl IS.add' siggers (map #2 vis),
adam@1856 87 sigdecs))
adam@1856 88 else
adam@1856 89 (sigify sigdecs d, (siggers, sigdecs))
adam@1856 90 | _ => (sigify sigdecs d, (siggers, sigdecs))
adam@1856 91
adam@1856 92 val (ds, _) = ListUtil.foldlMap doDecl (IS.empty, IS.empty) ds
adam@1856 93 in
adam@1856 94 (ds, sl)
adam@1856 95 end
adam@1856 96
adam@1856 97 end