Mercurial > urweb

annotate src/marshalcheck.sml @ 713:baaae037e7f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Retry failed record summary unifications at the end, in hopes that more has been learned
author Adam Chlipala <adamc@hcoop.net>
date Thu, 09 Apr 2009 14:59:29 -0400
parents 09df0c85f306
children d049d31a1966
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 val clientToServer = [("Basis", "int"),
adamc@680 57 ("Basis", "float"),
adamc@680 58 ("Basis", "string"),
adamc@680 59 ("Basis", "time"),
adamc@680 60 ("Basis", "unit"),
adamc@692 61 ("Basis", "option"),
adamc@692 62 ("Basis", "bool")]
adamc@680 63
adamc@680 64 val clientToServer = PS.addList (PS.empty, clientToServer)
adamc@680 65
adamc@680 66 fun check file =
adamc@680 67 let
adamc@680 68 fun kind (_, st) = st
adamc@680 69
adamc@680 70 fun con cmap (c, st) =
adamc@680 71 case c of
adamc@680 72 CFfi mx =>
adamc@680 73 if PS.member (clientToServer, mx) then
adamc@680 74 st
adamc@680 75 else
adamc@680 76 PS.add (st, mx)
adamc@680 77 | CNamed n =>
adamc@680 78 (case IM.find (cmap, n) of
adamc@680 79 NONE => st
adamc@680 80 | SOME st' => PS.union (st, st'))
adamc@680 81 | _ => st
adamc@680 82
adamc@680 83 fun sins cmap = U.Con.fold {kind = kind, con = con cmap} PS.empty
adamc@680 84 in
adamc@680 85 ignore (foldl (fn ((d, _), (cmap, emap)) =>
adamc@680 86 case d of
adamc@680 87 DCon (_, n, _, c) => (IM.insert (cmap, n, sins cmap c), emap)
adamc@680 88 | DDatatype (_, n, _, xncs) =>
adamc@680 89 (IM.insert (cmap, n, foldl (fn ((_, _, co), s) =>
adamc@680 90 case co of
adamc@680 91 NONE => s
adamc@680 92 | SOME c => PS.union (s, sins cmap c))
adamc@680 93 PS.empty xncs),
adamc@680 94 emap)
adamc@680 95
adamc@680 96 | DVal (_, n, t, _, tag) => (cmap, IM.insert (emap, n, (t, tag)))
adamc@680 97 | DValRec vis => (cmap,
adamc@680 98 foldl (fn ((_, n, t, _, tag), emap) => IM.insert (emap, n, (t, tag)))
adamc@680 99 emap vis)
adamc@680 100
adamc@680 101 | DExport (_, n) =>
adamc@680 102 (case IM.find (emap, n) of
adamc@680 103 NONE => raise Fail "MarshalCheck: Unknown export"
adamc@680 104 | SOME (t, tag) =>
adamc@680 105 let
adamc@680 106 fun makeS (t, _) =
adamc@680 107 case t of
adamc@680 108 TFun (dom, ran) => PS.union (sins cmap dom, makeS ran)
adamc@680 109 | _ => PS.empty
adamc@680 110 val s = makeS t
adamc@680 111 in
adamc@680 112 if PS.isEmpty s then
adamc@680 113 ()
adamc@680 114 else
adamc@680 115 E.error ("Input to exported function '"
adamc@680 116 ^ tag ^ "' involves one or more disallowed types: "
adamc@680 117 ^ PS.toString s);
adamc@680 118 (cmap, emap)
adamc@680 119 end)
adamc@680 120
adamc@680 121 | DCookie (_, _, t, tag) =>
adamc@680 122 let
adamc@680 123 val s = sins cmap t
adamc@680 124 in
adamc@680 125 if PS.isEmpty s then
adamc@680 126 ()
adamc@680 127 else
adamc@680 128 E.error ("Cookie '" ^ tag ^ "' includes one or more disallowed types: "
adamc@680 129 ^ PS.toString s);
adamc@680 130 (cmap, emap)
adamc@680 131 end
adamc@680 132
adamc@680 133 | _ => (cmap, emap))
adamc@680 134 (IM.empty, IM.empty) file)
adamc@680 135 end
adamc@680 136
adamc@680 137 end