adam@1856: (* Copyright (c) 2013, Adam Chlipala
adam@1856:  * All rights reserved.
adam@1856:  *
adam@1856:  * Redistribution and use in source and binary forms, with or without
adam@1856:  * modification, are permitted provided that the following conditions are met:
adam@1856:  *
adam@1856:  * - Redistributions of source code must retain the above copyright notice,
adam@1856:  *   this list of conditions and the following disclaimer.
adam@1856:  * - Redistributions in binary form must reproduce the above copyright notice,
adam@1856:  *   this list of conditions and the following disclaimer in the documentation
adam@1856:  *   and/or other materials provided with the distribution.
adam@1856:  * - The names of contributors may not be used to endorse or promote products
adam@1856:  *   derived from this software without specific prior written permission.
adam@1856:  *
adam@1856:  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adam@1856:  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adam@1856:  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adam@1856:  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
ziv@2252:  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
adam@1856:  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adam@1856:  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adam@1856:  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adam@1856:  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adam@1856:  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adam@1856:  * POSSIBILITY OF SUCH DAMAGE.
adam@1856:  *)
adam@1856: 
adam@1856: structure SigCheck :> SIG_CHECK = struct
adam@1856: 
adam@1856: open Mono
adam@1856: 
adam@1856: structure IS = IntBinarySet
adam@1856: structure E = ErrorMsg
adam@1856: 
ziv@2252: fun check (ds, sl) =
adam@1856:     let
adam@1856:         fun isSiggy siggers =
adam@1856:             MonoUtil.Decl.exists {typ = fn _ => false,
adam@1856:                                   decl = fn _ => false,
adam@1856:                                   exp = fn e =>
adam@1856:                                         case e of
adam@1856:                                             ERel n => IS.member (siggers, n)
adam@1856:                                           | EFfiApp ("Basis", "sigString", _) => true
adam@1856:                                           | _ => false}
adam@1856: 
adam@1856:         fun sigify' sigdecs e =
adam@1856:             case e of
adam@1856:                 ENamed n => if IS.member (sigdecs, n) then
adam@1856:                                 (EApp ((e, E.dummySpan),
adam@1856:                                        (ERecord [], E.dummySpan)))
adam@1856:                             else
adam@1856:                                 e
adam@1856:               | _ => e
adam@1856: 
adam@1856:         fun sigify sigdecs =
adam@1856:             MonoUtil.Decl.map {typ = fn x => x,
adam@1856:                                decl = fn d => d,
adam@1856:                                exp = sigify' sigdecs}
adam@1856: 
adam@1856:         fun sigifyE sigdecs =
adam@1856:             MonoUtil.Exp.map {typ = fn x => x,
adam@1856:                               exp = sigify' sigdecs}
adam@1856: 
adam@1856:         fun isFun (e, _) =
adam@1856:             case e of
adam@1856:                 EAbs _ => true
adam@1856:               | _ => false
adam@1856: 
adam@1856:         fun doDecl (d : decl, (siggers, sigdecs)) =
adam@1856:             case #1 d of
adam@1856:                 DVal (x, n, t, e, s) =>
adam@1856:                 if isSiggy siggers d then
adam@1856:                     if isFun e then
adam@1856:                         (sigify sigdecs d, (IS.add (siggers, n), sigdecs))
adam@1856:                     else
adam@1856:                         ((DVal (x, n, (TFun ((TRecord [], #2 d), t), #2 d),
adam@1856:                                 (EAbs ("_", (TRecord [], #2 d), t, sigifyE sigdecs e), #2 d),
adam@1856:                                 s), #2 d),
adam@1856:                          (IS.add (siggers, n),
adam@1856:                           IS.add (sigdecs, n)))
adam@1856:                 else
adam@1856:                     (sigify sigdecs d, (siggers, sigdecs))
adam@1856:               | DValRec vis =>
adam@1856:                 if isSiggy siggers d then
adam@1856:                     (sigify sigdecs d,
adam@1856:                      (foldl IS.add' siggers (map #2 vis),
adam@1856:                       sigdecs))
adam@1856:                 else
adam@1856:                     (sigify sigdecs d, (siggers, sigdecs))
adam@1856:               | _ => (sigify sigdecs d, (siggers, sigdecs))
adam@1856: 
ziv@2252:         val (ds, _) = ListUtil.foldlMap doDecl (IS.empty, IS.empty) ds
adam@1856:     in
ziv@2252:         (ds, sl)
adam@1856:     end
adam@1856: 
adam@1856: end