diff options
author | 2008-01-26 15:26:12 -0500 | |
---|---|---|
committer | 2008-01-26 15:26:12 -0500 | |
commit | e0a8e775a4c1e12debb2a3fa458007340685dc9d (patch) | |
tree | ed45e466a53dc18a1c772e2bdaad2e5f7ac8025b | |
parent | 485f8c00cc43334ba7bb429a830eb3b651ff92f6 (diff) |
Elaborating cons and decls
-rw-r--r-- | src/elab_print.sig | 37 | ||||
-rw-r--r-- | src/elab_print.sml | 153 | ||||
-rw-r--r-- | src/elab_util.sig | 2 | ||||
-rw-r--r-- | src/elab_util.sml | 6 | ||||
-rw-r--r-- | src/elaborate.sml | 200 | ||||
-rw-r--r-- | src/errormsg.sig | 3 | ||||
-rw-r--r-- | src/errormsg.sml | 6 | ||||
-rw-r--r-- | src/print.sig | 10 | ||||
-rw-r--r-- | src/print.sml | 22 | ||||
-rw-r--r-- | src/sources | 3 |
10 files changed, 427 insertions, 15 deletions
diff --git a/src/elab_print.sig b/src/elab_print.sig new file mode 100644 index 00000000..489b0756 --- /dev/null +++ b/src/elab_print.sig @@ -0,0 +1,37 @@ +(* 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. + *) + +(* Pretty-printing Laconic/Web *) + +signature ELAB_PRINT = sig + val p_kind : Elab.kind Print.printer + val p_explicitness : Elab.explicitness Print.printer + val p_con : ElabEnv.env -> Elab.con Print.printer + val p_decl : ElabEnv.env -> Elab.decl Print.printer + val p_file : ElabEnv.env -> Elab.file Print.printer +end + diff --git a/src/elab_print.sml b/src/elab_print.sml new file mode 100644 index 00000000..18d01695 --- /dev/null +++ b/src/elab_print.sml @@ -0,0 +1,153 @@ +(* 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. + *) + +(* Pretty-printing elaborated Laconic/Web *) + +structure ElabPrint :> ELAB_PRINT = struct + +open Print.PD +open Print + +open Elab + +structure E = ElabEnv + +fun p_kind' par (k, _) = + case k of + KType => string "Type" + | KArrow (k1, k2) => parenIf par (box [p_kind' true k1, + space, + string "->", + space, + p_kind k2]) + | KName => string "Name" + | KRecord k => box [string "{", p_kind k, string "}"] + + | KError => string "<ERROR>" + | KUnif (_, ref (SOME k)) => p_kind' par k + | KUnif (s, _) => string ("<UNIF:" ^ s ^ ">") + +and p_kind k = p_kind' false k + +fun p_explicitness e = + case e of + Explicit => string "::" + | Implicit => string ":::" + +fun p_con' par env (c, _) = + case c of + TFun (t1, t2) => parenIf par (box [p_con' true env t1, + space, + string "->", + space, + p_con env t2]) + | TCFun (e, x, k, c) => parenIf par (box [string x, + space, + p_explicitness e, + space, + p_kind k, + space, + string "->", + space, + p_con (E.pushCRel env x k) c]) + | TRecord (CRecord (_, xcs), _) => box [string "{", + p_list (fn (x, c) => + box [p_con env x, + space, + string ":", + space, + p_con env c]) xcs, + string "}"] + | TRecord c => box [string "$", + p_con' true env c] + + | CRel n => string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n) + | CNamed n => string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n) + + | CApp (c1, c2) => parenIf par (box [p_con env c1, + space, + p_con' true env c2]) + | CAbs (e, x, k, c) => parenIf par (box [string "fn", + space, + string x, + space, + p_explicitness e, + space, + p_kind k, + space, + string "=>", + space, + p_con (E.pushCRel env x k) c]) + + | CName s => box [string "#", string s] + + | CRecord (k, xcs) => parenIf par (box [string "[", + p_list (fn (x, c) => + box [p_con env x, + space, + string "=", + space, + p_con env c]) xcs, + string "]::", + p_kind k]) + | CConcat (c1, c2) => parenIf par (box [p_con' true env c1, + space, + string "++", + space, + p_con env c2]) + + | CError => string "<ERROR>" + | CUnif (_, ref (SOME c)) => p_con' par env c + | CUnif (s, _) => string ("<UNIF:" ^ s ^ ">") + +and p_con env = p_con' false env + +fun p_decl env ((d, _) : decl) = + case d of + DCon (x, k, c) => box [string "con", + space, + string x, + space, + string "::", + space, + p_kind k, + space, + string "=", + space, + p_con env c] + +fun p_file env file = + let + val (_, pds) = foldr (fn (d, (env, pds)) => + (ElabUtil.declBinds env d, + p_decl env d :: pds)) + (env, []) file + in + p_list_sep newline (fn x => x) pds + end + +end diff --git a/src/elab_util.sig b/src/elab_util.sig index 0190b576..da1a02f4 100644 --- a/src/elab_util.sig +++ b/src/elab_util.sig @@ -33,4 +33,6 @@ structure Kind : sig val exists : (Elab.kind' -> bool) -> Elab.kind -> bool end +val declBinds : ElabEnv.env -> Elab.decl -> ElabEnv.env + end diff --git a/src/elab_util.sml b/src/elab_util.sml index 8a0463cf..f5640d15 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -75,4 +75,10 @@ fun exists f k = end +structure E = ElabEnv + +fun declBinds env (d, _) = + case d of + DCon (x, k, _) => #1 (E.pushCNamed env x k) + end diff --git a/src/elaborate.sml b/src/elaborate.sml index ca950de2..e6044e49 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -32,6 +32,9 @@ structure L' = Elab structure E = ElabEnv structure U = ElabUtil +open Print +open ElabPrint + fun elabKind (k, loc) = case k of L.KType => (L'.KType, loc) @@ -48,34 +51,40 @@ fun occursKind r = U.Kind.exists (fn L'.KUnif (_, r') => r = r' | _ => false) -datatype unify_error = +datatype kunify_error = KOccursCheckFailed of L'.kind * L'.kind | KIncompatible of L'.kind * L'.kind -fun unifyError err = +exception KUnify' of kunify_error + +fun kunifyError err = case err of KOccursCheckFailed (k1, k2) => - ErrorMsg.errorAt (#2 k1) "Kind occurs check failed" + eprefaces "Kind occurs check failed" + [("Kind 1", p_kind k1), + ("Kind 2", p_kind k2)] | KIncompatible (k1, k2) => - ErrorMsg.errorAt (#2 k1) "Incompatible kinds" + eprefaces "Incompatible kinds" + [("Kind 1", p_kind k1), + ("Kind 2", p_kind k2)] -fun unifyKinds (k1All as (k1, pos)) (k2All as (k2, _)) = +fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) = let - fun err f = unifyError (f (k1All, k2All)) + fun err f = raise KUnify' (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) + (unifyKinds' d1 d2; + unifyKinds' r1 r2) | (L'.KName, L'.KName) => () - | (L'.KRecord k1, L'.KRecord k2) => unifyKinds k1 k2 + | (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 (_, ref (SOME k1All)), _) => unifyKinds' k1All k2All + | (_, L'.KUnif (_, ref (SOME k2All))) => unifyKinds' k1All k2All | (L'.KUnif (_, r1), L'.KUnif (_, r2)) => if r1 = r2 then @@ -97,6 +106,175 @@ fun unifyKinds (k1All as (k1, pos)) (k2All as (k2, _)) = | _ => err KIncompatible end +exception KUnify of L'.kind * L'.kind * kunify_error + +fun unifyKinds k1 k2 = + unifyKinds' k1 k2 + handle KUnify' err => raise KUnify (k1, k2, err) + +datatype con_error = + UnboundCon of ErrorMsg.span * string + | WrongKind of L'.con * L'.kind * L'.kind * kunify_error + +fun conError err = + case err of + UnboundCon (loc, s) => + ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s) + | WrongKind (c, k1, k2, kerr) => + (ErrorMsg.errorAt (#2 c) "Wrong kind"; + eprefaces' [("Have", p_kind k1), + ("Need", p_kind k2)]; + kunifyError kerr) + +fun checkKind c k1 k2 = + unifyKinds k1 k2 + handle KUnify (k1, k2, err) => + conError (WrongKind (c, k1, k2, err)) + +val dummy = ErrorMsg.dummySpan + +val ktype = (L'.KType, dummy) +val kname = (L'.KName, dummy) + +val cerror = (L'.CError, dummy) +val kerror = (L'.KError, dummy) + +local + val count = ref 0 +in + +fun resetKunif () = count := 0 + +fun kunif () = + let + val n = !count + val s = if n <= 26 then + str (chr (ord #"A" + n)) + else + "U" ^ Int.toString (n - 26) + in + count := n + 1; + (L'.KUnif (s, ref NONE), dummy) + end + +end + +fun elabCon env (c, loc) = + case c of + L.CAnnot (c, k) => + let + val k' = elabKind k + val (c', ck) = elabCon env c + in + checkKind c' ck k'; + (c', k') + end + + | L.TFun (t1, t2) => + let + val (t1', k1) = elabCon env t1 + val (t2', k2) = elabCon env t2 + in + checkKind t1' k1 ktype; + checkKind t2' k2 ktype; + ((L'.TFun (t1', t2'), loc), ktype) + end + | L.TCFun (e, x, k, t) => + let + val e' = elabExplicitness e + val k' = elabKind k + val env' = E.pushCRel env x k' + val (t', tk) = elabCon env' t + in + checkKind t' tk ktype; + ((L'.TCFun (e', x, k', t'), loc), ktype) + end + | L.TRecord c => + let + val (c', ck) = elabCon env c + val k = (L'.KRecord ktype, loc) + in + checkKind c' ck k; + ((L'.TRecord c', loc), ktype) + end + + | L.CVar s => + (case E.lookupC env s of + E.CNotBound => + (conError (UnboundCon (loc, s)); + (cerror, kerror)) + | E.CRel (n, k) => + ((L'.CRel n, loc), k) + | E.CNamed (n, k) => + ((L'.CNamed n, loc), k)) + | L.CApp (c1, c2) => + let + val (c1', k1) = elabCon env c1 + val (c2', k2) = elabCon env c2 + val dom = kunif () + val ran = kunif () + in + checkKind c1' k1 (L'.KArrow (dom, ran), loc); + checkKind c2' k2 dom; + ((L'.CApp (c1', c2'), loc), ran) + end + | L.CAbs (e, x, k, t) => + let + val e' = elabExplicitness e + val k' = elabKind k + val env' = E.pushCRel env x k' + val (t', tk) = elabCon env' t + in + ((L'.CAbs (e', x, k', t'), loc), + (L'.KArrow (k', tk), loc)) + end + + | L.CName s => + ((L'.CName s, loc), kname) + + | L.CRecord xcs => + let + val k = kunif () + + val xcs' = map (fn (x, c) => + let + val (x', xk) = elabCon env x + val (c', ck) = elabCon env c + in + checkKind x' xk kname; + checkKind c' ck k; + (x', c') + end) xcs + in + ((L'.CRecord (k, xcs'), loc), k) + end + | L.CConcat (c1, c2) => + let + val (c1', k1) = elabCon env c1 + val (c2', k2) = elabCon env c2 + val ku = kunif () + val k = (L'.KRecord ku, loc) + in + checkKind c1' k1 k; + checkKind c2' k2 k; + ((L'.CConcat (c1', c2'), loc), k) + end + +fun elabDecl env (d, loc) = + case d of + L.DCon (x, ko, c) => + let + val k' = case ko of + NONE => kunif () + | SOME k => elabKind k + + val (c', ck) = elabCon env c + in + checkKind c' ck k'; + (E.pushCNamed env x k', + L'.DCon (x, k', c')) + end + fun elabFile _ = raise Fail "" end diff --git a/src/errormsg.sig b/src/errormsg.sig index 24bc8205..92425842 100644 --- a/src/errormsg.sig +++ b/src/errormsg.sig @@ -39,6 +39,9 @@ signature ERROR_MSG = sig val posToString : pos -> string val spanToString : span -> string + val dummyPos : pos + val dummySpan : span + val resetPositioning : string -> unit val newline : int -> unit val lastLineStart : unit -> int diff --git a/src/errormsg.sml b/src/errormsg.sml index 0f5b9b61..e816b9a2 100644 --- a/src/errormsg.sml +++ b/src/errormsg.sml @@ -43,6 +43,12 @@ fun posToString {line, char} = fun spanToString {file, first, last} = String.concat [file, ":", posToString first, "-", posToString last] +val dummyPos = {line = 0, + char = 0} +val dummySpan = {file = "", + first = dummyPos, + last = dummyPos} + val file = ref "" val numLines = ref 1 diff --git a/src/print.sig b/src/print.sig index 5bf3fcd8..39daf5d0 100644 --- a/src/print.sig +++ b/src/print.sig @@ -48,7 +48,11 @@ signature PRINT = sig val preface : string * PD.pp_desc -> unit val epreface : string * PD.pp_desc -> unit - val fprefaces : PD.PPS.stream -> (string * PD.pp_desc) list -> unit - val prefaces : (string * PD.pp_desc) list -> unit - val eprefaces : (string * PD.pp_desc) list -> unit + val fprefaces : PD.PPS.stream -> string -> (string * PD.pp_desc) list -> unit + val prefaces : string -> (string * PD.pp_desc) list -> unit + val eprefaces : string -> (string * PD.pp_desc) list -> unit + + val fprefaces' : PD.PPS.stream -> (string * PD.pp_desc) list -> unit + val prefaces' : (string * PD.pp_desc) list -> unit + val eprefaces' : (string * PD.pp_desc) list -> unit end diff --git a/src/print.sml b/src/print.sml index 6d9019d2..22387090 100644 --- a/src/print.sml +++ b/src/print.sml @@ -71,11 +71,13 @@ fun fpreface f (s, d) = val preface = fpreface out val epreface = fpreface err -fun fprefaces f ls = +fun fprefaces f s ls = let val len = foldl (fn ((s, _), best) => Int.max (size s, best)) 0 ls in + fprint f (PD.string s); + fprint f PD.newline; app (fn (s, d) => let val s = CharVector.tabulate (len - size s, @@ -89,4 +91,22 @@ fun fprefaces f ls = val prefaces = fprefaces out val eprefaces = fprefaces err +fun fprefaces' f ls = + let + val len = foldl (fn ((s, _), best) => + Int.max (size s, best)) 0 ls + in + app (fn (s, d) => + let + val s = CharVector.tabulate (len - size s, + fn _ => #" ") + ^ s ^ ": " + in + fpreface f (s, d) + end) ls + end + +val prefaces' = fprefaces' out +val eprefaces' = fprefaces' err + end diff --git a/src/sources b/src/sources index 6270b1ea..e82c0c7e 100644 --- a/src/sources +++ b/src/sources @@ -23,6 +23,9 @@ elab_util.sml elab_env.sig elab_env.sml +elab_print.sig +elab_print.sml + elaborate.sig elaborate.sml |