summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/elab_print.sig37
-rw-r--r--src/elab_print.sml153
-rw-r--r--src/elab_util.sig2
-rw-r--r--src/elab_util.sml6
-rw-r--r--src/elaborate.sml200
-rw-r--r--src/errormsg.sig3
-rw-r--r--src/errormsg.sml6
-rw-r--r--src/print.sig10
-rw-r--r--src/print.sml22
-rw-r--r--src/sources3
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-11 00:10:11 +0000