diff options
author | Adam Chlipala <adamc@hcoop.net> | 2008-01-26 14:27:33 -0500 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2008-01-26 14:27:33 -0500 |
commit | 485f8c00cc43334ba7bb429a830eb3b651ff92f6 (patch) | |
tree | 913a8df05a3ab93ceeef1b559904bdfcf8c57dda /src/elaborate.sml | |
parent | 28605345c88491627b7a34cea6e50c9e5b9b8b01 (diff) |
Start of elaboration
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r-- | src/elaborate.sml | 102 |
1 files changed, 102 insertions, 0 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml new file mode 100644 index 00000000..ca950de2 --- /dev/null +++ b/src/elaborate.sml @@ -0,0 +1,102 @@ +(* Copyright (c) 2008, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +structure Elaborate :> ELABORATE = struct + +structure L = Laconic +structure L' = Elab +structure E = ElabEnv +structure U = ElabUtil + +fun elabKind (k, loc) = + case k of + L.KType => (L'.KType, loc) + | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc) + | L.KName => (L'.KName, loc) + | L.KRecord k => (L'.KRecord (elabKind k), loc) + +fun elabExplicitness e = + case e of + L.Explicit => L'.Explicit + | L.Implicit => L'.Implicit + +fun occursKind r = + U.Kind.exists (fn L'.KUnif (_, r') => r = r' + | _ => false) + +datatype unify_error = + KOccursCheckFailed of L'.kind * L'.kind + | KIncompatible of L'.kind * L'.kind + +fun unifyError err = + case err of + KOccursCheckFailed (k1, k2) => + ErrorMsg.errorAt (#2 k1) "Kind occurs check failed" + | KIncompatible (k1, k2) => + ErrorMsg.errorAt (#2 k1) "Incompatible kinds" + +fun unifyKinds (k1All as (k1, pos)) (k2All as (k2, _)) = + let + fun err f = unifyError (f (k1All, k2All)) + in + case (k1, k2) of + (L'.KType, L'.KType) => () + | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) => + (unifyKinds d1 d2; + unifyKinds r1 r2) + | (L'.KName, L'.KName) => () + | (L'.KRecord k1, L'.KRecord k2) => unifyKinds k1 k2 + + | (L'.KError, _) => () + | (_, L'.KError) => () + + | (L'.KUnif (_, ref (SOME k1All)), _) => unifyKinds k1All k2All + | (_, L'.KUnif (_, ref (SOME k2All))) => unifyKinds k1All k2All + + | (L'.KUnif (_, r1), L'.KUnif (_, r2)) => + if r1 = r2 then + () + else + r1 := SOME k2All + + | (L'.KUnif (_, r), _) => + if occursKind r k2All then + err KOccursCheckFailed + else + r := SOME k2All + | (_, L'.KUnif (_, r)) => + if occursKind r k1All then + err KOccursCheckFailed + else + r := SOME k1All + + | _ => err KIncompatible + end + +fun elabFile _ = raise Fail "" + +end |