Mercurial > urweb

annotate src/marshalcheck.sml @ 1327:1cc67fdac4d3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New argument to transactional free functions, to specify whether we are about to retry
author Adam Chlipala <adam@chlipala.net>
date Sat, 04 Dec 2010 11:15:20 -0500
parents 72670131dace
children b106ca8200b1
rev   line source
adamc@680 1 (* Copyright (c) 2009, Adam Chlipala
adamc@680 2 * All rights reserved.
adamc@680 3 *
adamc@680 4 * Redistribution and use in source and binary forms, with or without
adamc@680 5 * modification, are permitted provided that the following conditions are met:
adamc@680 6 *
adamc@680 7 * - Redistributions of source code must retain the above copyright notice,
adamc@680 8 * this list of conditions and the following disclaimer.
adamc@680 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@680 10 * this list of conditions and the following disclaimer in the documentation
adamc@680 11 * and/or other materials provided with the distribution.
adamc@680 12 * - The names of contributors may not be used to endorse or promote products
adamc@680 13 * derived from this software without specific prior written permission.
adamc@680 14 *
adamc@680 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@680 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@680 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@680 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@680 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@680 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@680 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@680 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@680 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@680 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@680 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@680 26 *)
adamc@680 27
adamc@680 28 structure MarshalCheck :> MARSHAL_CHECK = struct
adamc@680 29
adamc@680 30 open Core
adamc@680 31
adamc@680 32 structure U = CoreUtil
adamc@680 33 structure E = ErrorMsg
adamc@680 34
adamc@680 35 structure PK = struct
adamc@680 36 open Order
adamc@680 37 type ord_key = string * string
adamc@680 38 fun compare ((m1, x1), (m2, x2)) =
adamc@680 39 join (String.compare (m1, m2),
adamc@680 40 fn () => String.compare (x1, x2))
adamc@680 41 end
adamc@680 42
adamc@680 43 structure PS = BinarySetFn(PK)
adamc@680 44 structure PS = struct
adamc@680 45 open PS
adamc@680 46 fun toString' (m, x) = m ^ "." ^ x
adamc@680 47 fun toString set =
adamc@680 48 case PS.listItems set of
adamc@680 49 [] => "{}"
adamc@680 50 | [x] => toString' x
adamc@680 51 | x :: xs => List.foldl (fn (x, s) => s ^ ", " ^ toString' x) (toString' x) xs
adamc@680 52 end
adamc@680 53
adamc@680 54 structure IM = IntBinaryMap
adamc@680 55
adamc@680 56 fun check file =
adamc@680 57 let
adamc@680 58 fun kind (_, st) = st
adamc@680 59
adamc@680 60 fun con cmap (c, st) =
adamc@680 61 case c of
adamc@680 62 CFfi mx =>
adamc@765 63 if Settings.mayClientToServer mx then
adamc@680 64 st
adamc@680 65 else
adamc@680 66 PS.add (st, mx)
adamc@680 67 | CNamed n =>
adamc@680 68 (case IM.find (cmap, n) of
adamc@680 69 NONE => st
adamc@680 70 | SOME st' => PS.union (st, st'))
adamc@680 71 | _ => st
adamc@680 72
adamc@680 73 fun sins cmap = U.Con.fold {kind = kind, con = con cmap} PS.empty
adamc@680 74 in
adamc@680 75 ignore (foldl (fn ((d, _), (cmap, emap)) =>
adamc@680 76 case d of
adamc@680 77 DCon (_, n, _, c) => (IM.insert (cmap, n, sins cmap c), emap)
adamc@807 78 | DDatatype dts =>
adamc@807 79 (foldl (fn ((_, n, _, xncs), cmap) =>
adamc@807 80 IM.insert (cmap, n, foldl (fn ((_, _, co), s) =>
adamc@807 81 case co of
adamc@807 82 NONE => s
adamc@807 83 | SOME c => PS.union (s, sins cmap c))
adamc@807 84 PS.empty xncs)) cmap dts,
adamc@680 85 emap)
adamc@680 86
adamc@680 87 | DVal (_, n, t, _, tag) => (cmap, IM.insert (emap, n, (t, tag)))
adamc@680 88 | DValRec vis => (cmap,
adamc@680 89 foldl (fn ((_, n, t, _, tag), emap) => IM.insert (emap, n, (t, tag)))
adamc@680 90 emap vis)
adamc@680 91
adamc@1104 92 | DExport (_, n, _) =>
adamc@680 93 (case IM.find (emap, n) of
adamc@680 94 NONE => raise Fail "MarshalCheck: Unknown export"
adamc@680 95 | SOME (t, tag) =>
adamc@680 96 let
adamc@680 97 fun makeS (t, _) =
adamc@680 98 case t of
adamc@680 99 TFun (dom, ran) => PS.union (sins cmap dom, makeS ran)
adamc@680 100 | _ => PS.empty
adamc@680 101 val s = makeS t
adamc@680 102 in
adamc@680 103 if PS.isEmpty s then
adamc@680 104 ()
adamc@680 105 else
adamc@680 106 E.error ("Input to exported function '"
adamc@680 107 ^ tag ^ "' involves one or more disallowed types: "
adamc@680 108 ^ PS.toString s);
adamc@680 109 (cmap, emap)
adamc@680 110 end)
adamc@680 111
adamc@680 112 | DCookie (_, _, t, tag) =>
adamc@680 113 let
adamc@680 114 val s = sins cmap t
adamc@680 115 in
adamc@680 116 if PS.isEmpty s then
adamc@680 117 ()
adamc@680 118 else
adamc@680 119 E.error ("Cookie '" ^ tag ^ "' includes one or more disallowed types: "
adamc@680 120 ^ PS.toString s);
adamc@680 121 (cmap, emap)
adamc@680 122 end
adamc@680 123
adamc@680 124 | _ => (cmap, emap))
adamc@680 125 (IM.empty, IM.empty) file)
adamc@680 126 end
adamc@680 127
adamc@680 128 end