summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/top.ur5
-rw-r--r--lib/top.urs8
-rw-r--r--src/elab_err.sig113
-rw-r--r--src/elab_err.sml349
-rw-r--r--src/elab_ops.sml44
-rw-r--r--src/elab_util.sig8
-rw-r--r--src/elab_util.sml42
-rw-r--r--src/elaborate.sml315
-rw-r--r--src/sources3
-rw-r--r--src/urweb.grm14
-rw-r--r--tests/crud.ur17
-rw-r--r--tests/crud.urs3
12 files changed, 593 insertions, 328 deletions
diff --git a/lib/top.ur b/lib/top.ur
index ec0e58af..4df12ff0 100644
--- a/lib/top.ur
+++ b/lib/top.ur
@@ -1,3 +1,6 @@
+con idT = fn t :: Type => t
+con record = fn t :: {Type} => $t
+
con mapTT (f :: Type -> Type) = fold (fn nm t acc => [nm] ~ acc =>
[nm = f t] ++ acc) []
@@ -5,7 +8,7 @@ fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type) (f1 : t2 -> t3) (f2 : t1 -
fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) = cdata (show sh v)
-fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
+val foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
(f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
-> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
(i : tr []) =
diff --git a/lib/top.urs b/lib/top.urs
index 80344602..c2d2fc8f 100644
--- a/lib/top.urs
+++ b/lib/top.urs
@@ -1,3 +1,6 @@
+con idT = fn t :: Type => t
+con record = fn t :: {Type} => $t
+
con mapTT = fn f :: Type -> Type => fold (fn nm t acc => [nm] ~ acc =>
[nm = f t] ++ acc) []
@@ -6,3 +9,8 @@ val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type
val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
-> xml ctx use []
+
+val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> tr :: ({Type} -> Type)
+ -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
+ -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+ -> tr [] -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r
diff --git a/src/elab_err.sig b/src/elab_err.sig
new file mode 100644
index 00000000..7682cd31
--- /dev/null
+++ b/src/elab_err.sig
@@ -0,0 +1,113 @@
+(* 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.
+ *)
+
+signature ELAB_ERR = sig
+
+ datatype kunify_error =
+ KOccursCheckFailed of Elab.kind * Elab.kind
+ | KIncompatible of Elab.kind * Elab.kind
+
+ val kunifyError : kunify_error -> unit
+
+ datatype con_error =
+ UnboundCon of ErrorMsg.span * string
+ | UnboundDatatype of ErrorMsg.span * string
+ | UnboundStrInCon of ErrorMsg.span * string
+ | WrongKind of Elab.con * Elab.kind * Elab.kind * kunify_error
+ | DuplicateField of ErrorMsg.span * string
+ | ProjBounds of Elab.con * int
+ | ProjMismatch of Elab.con * Elab.kind
+
+ val conError : ElabEnv.env -> con_error -> unit
+
+ datatype cunify_error =
+ CKind of Elab.kind * Elab.kind * kunify_error
+ | COccursCheckFailed of Elab.con * Elab.con
+ | CIncompatible of Elab.con * Elab.con
+ | CExplicitness of Elab.con * Elab.con
+ | CKindof of Elab.kind * Elab.con
+ | CRecordFailure of Elab.con * Elab.con
+
+ val cunifyError : ElabEnv.env -> cunify_error -> unit
+
+ datatype exp_error =
+ UnboundExp of ErrorMsg.span * string
+ | UnboundStrInExp of ErrorMsg.span * string
+ | Unify of Elab.exp * Elab.con * Elab.con * cunify_error
+ | Unif of string * Elab.con
+ | WrongForm of string * Elab.exp * Elab.con
+ | IncompatibleCons of Elab.con * Elab.con
+ | DuplicatePatternVariable of ErrorMsg.span * string
+ | PatUnify of Elab.pat * Elab.con * Elab.con * cunify_error
+ | UnboundConstructor of ErrorMsg.span * string list * string
+ | PatHasArg of ErrorMsg.span
+ | PatHasNoArg of ErrorMsg.span
+ | Inexhaustive of ErrorMsg.span
+ | DuplicatePatField of ErrorMsg.span * string
+ | Unresolvable of ErrorMsg.span * Elab.con
+ | OutOfContext of ErrorMsg.span * (Elab.exp * Elab.con) option
+ | IllegalRec of string * Elab.exp
+
+ val expError : ElabEnv.env -> exp_error -> unit
+
+ datatype decl_error =
+ KunifsRemain of Elab.decl list
+ | CunifsRemain of Elab.decl list
+ | Nonpositive of Elab.decl
+
+ val declError : ElabEnv.env -> decl_error -> unit
+
+ datatype sgn_error =
+ UnboundSgn of ErrorMsg.span * string
+ | UnmatchedSgi of Elab.sgn_item
+ | SgiWrongKind of Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * kunify_error
+ | SgiWrongCon of Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * cunify_error
+ | SgiMismatchedDatatypes of Elab.sgn_item * Elab.sgn_item * (Elab.con * Elab.con * cunify_error) option
+ | SgnWrongForm of Elab.sgn * Elab.sgn
+ | UnWhereable of Elab.sgn * string
+ | WhereWrongKind of Elab.kind * Elab.kind * kunify_error
+ | NotIncludable of Elab.sgn
+ | DuplicateCon of ErrorMsg.span * string
+ | DuplicateVal of ErrorMsg.span * string
+ | DuplicateSgn of ErrorMsg.span * string
+ | DuplicateStr of ErrorMsg.span * string
+ | NotConstraintsable of Elab.sgn
+
+ val sgnError : ElabEnv.env -> sgn_error -> unit
+
+ datatype str_error =
+ UnboundStr of ErrorMsg.span * string
+ | NotFunctor of Elab.sgn
+ | FunctorRebind of ErrorMsg.span
+ | UnOpenable of Elab.sgn
+ | NotType of Elab.kind * (Elab.kind * Elab.kind * kunify_error)
+ | DuplicateConstructor of string * ErrorMsg.span
+ | NotDatatype of ErrorMsg.span
+
+ val strError : ElabEnv.env -> str_error -> unit
+
+end
diff --git a/src/elab_err.sml b/src/elab_err.sml
new file mode 100644
index 00000000..34e26cd1
--- /dev/null
+++ b/src/elab_err.sml
@@ -0,0 +1,349 @@
+(* 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 ElabErr :> ELAB_ERR = struct
+
+structure L = Source
+open Elab
+
+structure E = ElabEnv
+structure U = ElabUtil
+
+open Print
+structure P = ElabPrint
+
+val simplCon = U.Con.mapB {kind = fn k => k,
+ con = fn env => fn c =>
+ let
+ val c = (c, ErrorMsg.dummySpan)
+ val (c', _) = Disjoint.hnormCon (env, Disjoint.empty) c
+ in
+ (*prefaces "simpl" [("c", P.p_con env c),
+ ("c'", P.p_con env c')];*)
+ #1 c'
+ end,
+ bind = fn (env, U.Con.Rel (x, k)) => E.pushCRel env x k
+ | (env, U.Con.Named (x, n, k)) => E.pushCNamedAs env x n k NONE}
+
+val p_kind = P.p_kind
+
+datatype kunify_error =
+ KOccursCheckFailed of kind * kind
+ | KIncompatible of kind * kind
+
+fun kunifyError err =
+ case err of
+ KOccursCheckFailed (k1, k2) =>
+ eprefaces "Kind occurs check failed"
+ [("Kind 1", p_kind k1),
+ ("Kind 2", p_kind k2)]
+ | KIncompatible (k1, k2) =>
+ eprefaces "Incompatible kinds"
+ [("Kind 1", p_kind k1),
+ ("Kind 2", p_kind k2)]
+
+
+fun p_con env c = P.p_con env (simplCon env c)
+
+datatype con_error =
+ UnboundCon of ErrorMsg.span * string
+ | UnboundDatatype of ErrorMsg.span * string
+ | UnboundStrInCon of ErrorMsg.span * string
+ | WrongKind of con * kind * kind * kunify_error
+ | DuplicateField of ErrorMsg.span * string
+ | ProjBounds of con * int
+ | ProjMismatch of con * kind
+
+fun conError env err =
+ case err of
+ UnboundCon (loc, s) =>
+ ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
+ | UnboundDatatype (loc, s) =>
+ ErrorMsg.errorAt loc ("Unbound datatype " ^ s)
+ | UnboundStrInCon (loc, s) =>
+ ErrorMsg.errorAt loc ("Unbound structure " ^ s)
+ | WrongKind (c, k1, k2, kerr) =>
+ (ErrorMsg.errorAt (#2 c) "Wrong kind";
+ eprefaces' [("Constructor", p_con env c),
+ ("Have kind", p_kind k1),
+ ("Need kind", p_kind k2)];
+ kunifyError kerr)
+ | DuplicateField (loc, s) =>
+ ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
+ | ProjBounds (c, n) =>
+ (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection";
+ eprefaces' [("Constructor", p_con env c),
+ ("Index", Print.PD.string (Int.toString n))])
+ | ProjMismatch (c, k) =>
+ (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
+ eprefaces' [("Constructor", p_con env c),
+ ("Kind", p_kind k)])
+
+
+datatype cunify_error =
+ CKind of kind * kind * kunify_error
+ | COccursCheckFailed of con * con
+ | CIncompatible of con * con
+ | CExplicitness of con * con
+ | CKindof of kind * con
+ | CRecordFailure of con * con
+
+fun cunifyError env err =
+ case err of
+ CKind (k1, k2, kerr) =>
+ (eprefaces "Kind unification failure"
+ [("Kind 1", p_kind k1),
+ ("Kind 2", p_kind k2)];
+ kunifyError kerr)
+ | COccursCheckFailed (c1, c2) =>
+ eprefaces "Constructor occurs check failed"
+ [("Con 1", p_con env c1),
+ ("Con 2", p_con env c2)]
+ | CIncompatible (c1, c2) =>
+ eprefaces "Incompatible constructors"
+ [("Con 1", p_con env c1),
+ ("Con 2", p_con env c2)]
+ | CExplicitness (c1, c2) =>
+ eprefaces "Differing constructor function explicitness"
+ [("Con 1", p_con env c1),
+ ("Con 2", p_con env c2)]
+ | CKindof (k, c) =>
+ eprefaces "Unexpected kind for kindof calculation"
+ [("Kind", p_kind k),
+ ("Con", p_con env c)]
+ | CRecordFailure (c1, c2) =>
+ eprefaces "Can't unify record constructors"
+ [("Summary 1", p_con env c1),
+ ("Summary 2", p_con env c2)]
+
+datatype exp_error =
+ UnboundExp of ErrorMsg.span * string
+ | UnboundStrInExp of ErrorMsg.span * string
+ | Unify of exp * con * con * cunify_error
+ | Unif of string * con
+ | WrongForm of string * exp * con
+ | IncompatibleCons of con * con
+ | DuplicatePatternVariable of ErrorMsg.span * string
+ | PatUnify of pat * con * con * cunify_error
+ | UnboundConstructor of ErrorMsg.span * string list * string
+ | PatHasArg of ErrorMsg.span
+ | PatHasNoArg of ErrorMsg.span
+ | Inexhaustive of ErrorMsg.span
+ | DuplicatePatField of ErrorMsg.span * string
+ | Unresolvable of ErrorMsg.span * con
+ | OutOfContext of ErrorMsg.span * (exp * con) option
+ | IllegalRec of string * exp
+
+val p_exp = P.p_exp
+val p_pat = P.p_pat
+
+fun expError env err =
+ case err of
+ UnboundExp (loc, s) =>
+ ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
+ | UnboundStrInExp (loc, s) =>
+ ErrorMsg.errorAt loc ("Unbound structure " ^ s)
+ | Unify (e, c1, c2, uerr) =>
+ (ErrorMsg.errorAt (#2 e) "Unification failure";
+ eprefaces' [("Expression", p_exp env e),
+ ("Have con", p_con env c1),
+ ("Need con", p_con env c2)];
+ cunifyError env uerr)
+ | Unif (action, c) =>
+ (ErrorMsg.errorAt (#2 c) ("Unification variable blocks " ^ action);
+ eprefaces' [("Con", p_con env c)])
+ | WrongForm (variety, e, t) =>
+ (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
+ eprefaces' [("Expression", p_exp env e),
+ ("Type", p_con env t)])
+ | IncompatibleCons (c1, c2) =>
+ (ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
+ eprefaces' [("Con 1", p_con env c1),
+ ("Con 2", p_con env c2)])
+ | DuplicatePatternVariable (loc, s) =>
+ ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
+ | PatUnify (p, c1, c2, uerr) =>
+ (ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
+ eprefaces' [("Pattern", p_pat env p),
+ ("Have con", p_con env c1),
+ ("Need con", p_con env c2)];
+ cunifyError env uerr)
+ | UnboundConstructor (loc, ms, s) =>
+ ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern")
+ | PatHasArg loc =>
+ ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
+ | PatHasNoArg loc =>
+ ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
+ | Inexhaustive loc =>
+ ErrorMsg.errorAt loc "Inexhaustive 'case'"
+ | DuplicatePatField (loc, s) =>
+ ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern")
+ | OutOfContext (loc, co) =>
+ (ErrorMsg.errorAt loc "Type class wildcard occurs out of context";
+ Option.app (fn (e, c) => eprefaces' [("Function", p_exp env e),
+ ("Type", p_con env c)]) co)
+ | Unresolvable (loc, c) =>
+ (ErrorMsg.errorAt loc "Can't resolve type class instance";
+ eprefaces' [("Class constraint", p_con env c)])
+ | IllegalRec (x, e) =>
+ (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
+ eprefaces' [("Variable", PD.string x),
+ ("Expression", p_exp env e)])
+
+
+datatype decl_error =
+ KunifsRemain of decl list
+ | CunifsRemain of decl list
+ | Nonpositive of decl
+
+fun lspan [] = ErrorMsg.dummySpan
+ | lspan ((_, loc) :: _) = loc
+
+val p_decl = P.p_decl
+
+fun declError env err =
+ case err of
+ KunifsRemain ds =>
+ (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration";
+ eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
+ | CunifsRemain ds =>
+ (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration";
+ eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
+ | Nonpositive d =>
+ (ErrorMsg.errorAt (#2 d) "Non-strictly-positive datatype declaration (could allow non-termination)";
+ eprefaces' [("Decl", p_decl env d)])
+
+datatype sgn_error =
+ UnboundSgn of ErrorMsg.span * string
+ | UnmatchedSgi of sgn_item
+ | SgiWrongKind of sgn_item * kind * sgn_item * kind * kunify_error
+ | SgiWrongCon of sgn_item * con * sgn_item * con * cunify_error
+ | SgiMismatchedDatatypes of sgn_item * sgn_item * (con * con * cunify_error) option
+ | SgnWrongForm of sgn * sgn
+ | UnWhereable of sgn * string
+ | WhereWrongKind of kind * kind * kunify_error
+ | NotIncludable of sgn
+ | DuplicateCon of ErrorMsg.span * string
+ | DuplicateVal of ErrorMsg.span * string
+ | DuplicateSgn of ErrorMsg.span * string
+ | DuplicateStr of ErrorMsg.span * string
+ | NotConstraintsable of sgn
+
+val p_sgn_item = P.p_sgn_item
+val p_sgn = P.p_sgn
+
+fun sgnError env err =
+ case err of
+ UnboundSgn (loc, s) =>
+ ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
+ | UnmatchedSgi (sgi as (_, loc)) =>
+ (ErrorMsg.errorAt loc "Unmatched signature item";
+ eprefaces' [("Item", p_sgn_item env sgi)])
+ | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
+ (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
+ eprefaces' [("Have", p_sgn_item env sgi1),
+ ("Need", p_sgn_item env sgi2),
+ ("Kind 1", p_kind k1),
+ ("Kind 2", p_kind k2)];
+ kunifyError kerr)
+ | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
+ (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
+ eprefaces' [("Have", p_sgn_item env sgi1),
+ ("Need", p_sgn_item env sgi2),
+ ("Con 1", p_con env c1),
+ ("Con 2", p_con env c2)];
+ cunifyError env cerr)
+ | SgiMismatchedDatatypes (sgi1, sgi2, cerro) =>
+ (ErrorMsg.errorAt (#2 sgi1) "Mismatched 'datatype' specifications:";
+ eprefaces' [("Have", p_sgn_item env sgi1),
+ ("Need", p_sgn_item env sgi2)];
+ Option.app (fn (c1, c2, ue) =>
+ (eprefaces "Unification error"
+ [("Con 1", p_con env c1),
+ ("Con 2", p_con env c2)];
+ cunifyError env ue)) cerro)
+ | SgnWrongForm (sgn1, sgn2) =>
+ (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
+ eprefaces' [("Sig 1", p_sgn env sgn1),
+ ("Sig 2", p_sgn env sgn2)])
+ | UnWhereable (sgn, x) =>
+ (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
+ eprefaces' [("Signature", p_sgn env sgn),
+ ("Field", PD.string x)])
+ | WhereWrongKind (k1, k2, kerr) =>
+ (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
+ eprefaces' [("Have", p_kind k1),
+ ("Need", p_kind k2)];
+ kunifyError kerr)
+ | NotIncludable sgn =>
+ (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
+ eprefaces' [("Signature", p_sgn env sgn)])
+ | DuplicateCon (loc, s) =>
+ ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
+ | DuplicateVal (loc, s) =>
+ ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature")
+ | DuplicateSgn (loc, s) =>
+ ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
+ | DuplicateStr (loc, s) =>
+ ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
+ | NotConstraintsable sgn =>
+ (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'";
+ eprefaces' [("Signature", p_sgn env sgn)])
+
+datatype str_error =
+ UnboundStr of ErrorMsg.span * string
+ | NotFunctor of sgn
+ | FunctorRebind of ErrorMsg.span
+ | UnOpenable of sgn
+ | NotType of kind * (kind * kind * kunify_error)
+ | DuplicateConstructor of string * ErrorMsg.span
+ | NotDatatype of ErrorMsg.span
+
+fun strError env err =
+ case err of
+ UnboundStr (loc, s) =>
+ ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
+ | NotFunctor sgn =>
+ (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
+ eprefaces' [("Signature", p_sgn env sgn)])
+ | FunctorRebind loc =>
+ ErrorMsg.errorAt loc "Attempt to rebind functor"
+ | UnOpenable sgn =>
+ (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
+ eprefaces' [("Signature", p_sgn env sgn)])
+ | NotType (k, (k1, k2, ue)) =>
+ (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
+ eprefaces' [("Kind", p_kind k),
+ ("Subkind 1", p_kind k1),
+ ("Subkind 2", p_kind k2)];
+ kunifyError ue)
+ | DuplicateConstructor (x, loc) =>
+ ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
+ | NotDatatype loc =>
+ ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
+
+end
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index 3cdc37c1..d73180ff 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -127,7 +127,47 @@ fun hnormCon env (cAll as (c, loc)) =
(CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
rest''), loc)), loc)
end
- | _ => default ())
+ | _ =>
+ let
+ fun cunif () =
+ let
+ val r = ref NONE
+ in
+ (r, (CUnif (loc, (KType, loc), "_", r), loc))
+ end
+
+ val (nmR, nm) = cunif ()
+ val (vR, v) = cunif ()
+ val (rR, r) = cunif ()
+
+ val c = f
+ val c = (CApp (c, nm), loc)
+ val c = (CApp (c, v), loc)
+ val c = (CApp (c, r), loc)
+ fun unconstraint c =
+ case hnormCon env c of
+ (CDisjoint (_, _, c), _) => unconstraint c
+ | c => c
+ val c = unconstraint c
+ in
+ (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*)
+ case (hnormCon env i, unconstraint c) of
+ ((CRecord (_, []), _),
+ (CConcat (c1, c2'), _)) =>
+ (case (hnormCon env c1, hnormCon env c2') of
+ ((CRecord (_, [(nm', v')]), _),
+ (CUnif (_, _, _, rR'), _)) =>
+ (case (hnormCon env nm', hnormCon env v') of
+ ((CUnif (_, _, _, nmR'), _),
+ (CUnif (_, _, _, vR'), _)) =>
+ if nmR' = nmR andalso vR' = vR andalso rR' = rR then
+ hnormCon env c2
+ else
+ default ()
+ | _ => default ())
+ | _ => default ())
+ | _ => default ()
+ end)
| _ => default ())
| _ => default ()
end
@@ -141,7 +181,7 @@ fun hnormCon env (cAll as (c, loc)) =
| ((CConcat (c11, c12), loc), c2') =>
hnormCon env (CConcat (c11, (CConcat (c12, c2'), loc)), loc)
| (c1', (CRecord (_, []), _)) => c1'
- | _ => cAll)
+ | (c1', c2') => (CConcat (c1', c2'), loc))
| CProj (c, n) =>
(case hnormCon env c of
diff --git a/src/elab_util.sig b/src/elab_util.sig
index 57883073..f4edd972 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -38,7 +38,7 @@ end
structure Con : sig
datatype binder =
Rel of string * Elab.kind
- | Named of string * Elab.kind
+ | Named of string * int * Elab.kind
val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
@@ -62,7 +62,7 @@ end
structure Exp : sig
datatype binder =
RelC of string * Elab.kind
- | NamedC of string * Elab.kind
+ | NamedC of string * int * Elab.kind
| RelE of string * Elab.con
| NamedE of string * Elab.con
@@ -88,7 +88,7 @@ end
structure Sgn : sig
datatype binder =
RelC of string * Elab.kind
- | NamedC of string * Elab.kind
+ | NamedC of string * int * Elab.kind
| Str of string * Elab.sgn
| Sgn of string * Elab.sgn
@@ -117,7 +117,7 @@ end
structure Decl : sig
datatype binder =
RelC of string * Elab.kind
- | NamedC of string * Elab.kind
+ | NamedC of string * int * Elab.kind
| RelE of string * Elab.con
| NamedE of string * Elab.con
| Str of string * Elab.sgn
diff --git a/src/elab_util.sml b/src/elab_util.sml
index d0f37a92..6f56d9c9 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -96,7 +96,7 @@ structure Con = struct
datatype binder =
Rel of string * Elab.kind
- | Named of string * Elab.kind
+ | Named of string * int * Elab.kind
fun mapfoldB {kind = fk, con = fc, bind} =
let
@@ -240,7 +240,7 @@ structure Exp = struct
datatype binder =
RelC of string * Elab.kind
- | NamedC of string * Elab.kind
+ | NamedC of string * int * Elab.kind
| RelE of string * Elab.con
| NamedE of string * Elab.con
@@ -392,7 +392,7 @@ structure Sgn = struct
datatype binder =
RelC of string * Elab.kind
- | NamedC of string * Elab.kind
+ | NamedC of string * int * Elab.kind
| Str of string * Elab.sgn
| Sgn of string * Elab.sgn
@@ -479,14 +479,14 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
SgnConst sgis =>
S.map2 (ListUtil.mapfoldB (fn (ctx, si) =>
(case #1 si of
- SgiConAbs (x, _, k) =>
- bind (ctx, NamedC (x, k))
- | SgiCon (x, _, k, _) =>
- bind (ctx, NamedC (x, k))
+ SgiConAbs (x, n, k) =>
+ bind (ctx, NamedC (x, n, k))
+ | SgiCon (x, n, k, _) =>
+ bind (ctx, NamedC (x, n, k))
| SgiDatatype (x, n, _, xncs) =>
- bind (ctx, NamedC (x, (KType, loc)))
- | SgiDatatypeImp (x, _, _, _, _, _, _) =>
- bind (ctx, NamedC (x, (KType, loc)))
+ bind (ctx, NamedC (x, n, (KType, loc)))
+ | SgiDatatypeImp (x, n, _, _, _, _, _) =>
+ bind (ctx, NamedC (x, n, (KType, loc)))
| SgiVal _ => ctx
| SgiStr (x, _, sgn) =>
bind (ctx, Str (x, sgn))
@@ -494,10 +494,10 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
bind (ctx, Sgn (x, sgn))
| SgiConstraint _ => ctx
| SgiTable _ => ctx
- | SgiClassAbs (x, _) =>
- bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc)))
- | SgiClass (x, _, _) =>
- bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))),
+ | SgiClassAbs (x, n) =>
+ bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
+ | SgiClass (x, n, _) =>
+ bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc))),
sgi ctx si)) ctx sgis,
fn sgis' =>
(SgnConst sgis', loc))
@@ -542,7 +542,7 @@ structure Decl = struct
datatype binder =
RelC of string * Elab.kind
- | NamedC of string * Elab.kind
+ | NamedC of string * int * Elab.kind
| RelE of string * Elab.con
| NamedE of string * Elab.con
| Str of string * Elab.sgn
@@ -594,11 +594,11 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
StrConst ds =>
S.map2 (ListUtil.mapfoldB (fn (ctx, d) =>
(case #1 d of
- DCon (x, _, k, _) =>
- bind (ctx, NamedC (x, k))
+ DCon (x, n, k, _) =>
+ bind (ctx, NamedC (x, n, k))
| DDatatype (x, n, xs, xncs) =>
let
- val ctx = bind (ctx, NamedC (x, (KType, loc)))
+ val ctx = bind (ctx, NamedC (x, n, (KType, loc)))
in
foldl (fn ((x, _, co), ctx) =>
let
@@ -621,7 +621,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
ctx xncs
end
| DDatatypeImp (x, n, m, ms, x', _, _) =>
- bind (ctx, NamedC (x, (KType, loc)))
+ bind (ctx, NamedC (x, n, (KType, loc)))
| DVal (x, _, c, _) =>
bind (ctx, NamedE (x, c))
| DValRec vis =>
@@ -637,8 +637,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
| DTable (tn, x, n, c) =>
bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "table"), loc),
c), loc)))
- | DClass (x, _, _) =>
- bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc)))
+ | DClass (x, n, _) =>
+ bind (ctx, NamedC (x, n, (KArrow ((KType, loc), (KType, loc)), loc)))
| DDatabase _ => ctx,
mfd ctx d)) ctx ds,
fn ds' => (StrConst ds', loc))
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 7e4ff670..2b548969 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -36,6 +36,7 @@ structure D = Disjoint
open Print
open ElabPrint
+open ElabErr
structure IM = IntBinaryMap
@@ -58,23 +59,8 @@ fun occursKind r =
U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
| _ => false)
-datatype kunify_error =
- KOccursCheckFailed of L'.kind * L'.kind
- | KIncompatible of L'.kind * L'.kind
-
exception KUnify' of kunify_error
-fun kunifyError err =
- case err of
- KOccursCheckFailed (k1, k2) =>
- eprefaces "Kind occurs check failed"
- [("Kind 1", p_kind k1),
- ("Kind 2", p_kind k2)]
- | KIncompatible (k1, k2) =>
- eprefaces "Incompatible kinds"
- [("Kind 1", p_kind k1),
- ("Kind 2", p_kind k2)]
-
fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) =
let
fun err f = raise KUnify' (f (k1All, k2All))
@@ -124,40 +110,6 @@ fun unifyKinds k1 k2 =
unifyKinds' k1 k2
handle KUnify' err => raise KUnify (k1, k2, err)
-datatype con_error =
- UnboundCon of ErrorMsg.span * string
- | UnboundDatatype of ErrorMsg.span * string
- | UnboundStrInCon of ErrorMsg.span * string
- | WrongKind of L'.con * L'.kind * L'.kind * kunify_error
- | DuplicateField of ErrorMsg.span * string
- | ProjBounds of L'.con * int
- | ProjMismatch of L'.con * L'.kind
-
-fun conError env err =
- case err of
- UnboundCon (loc, s) =>
- ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
- | UnboundDatatype (loc, s) =>
- ErrorMsg.errorAt loc ("Unbound datatype " ^ s)
- | UnboundStrInCon (loc, s) =>
- ErrorMsg.errorAt loc ("Unbound structure " ^ s)
- | WrongKind (c, k1, k2, kerr) =>
- (ErrorMsg.errorAt (#2 c) "Wrong kind";
- eprefaces' [("Constructor", p_con env c),
- ("Have kind", p_kind k1),
- ("Need kind", p_kind k2)];
- kunifyError kerr)
- | DuplicateField (loc, s) =>
- ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
- | ProjBounds (c, n) =>
- (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection";
- eprefaces' [("Constructor", p_con env c),
- ("Index", Print.PD.string (Int.toString n))])
- | ProjMismatch (c, k) =>
- (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
- eprefaces' [("Constructor", p_con env c),
- ("Kind", p_kind k)])
-
fun checkKind env c k1 k2 =
unifyKinds k1 k2
handle KUnify (k1, k2, err) =>
@@ -495,44 +447,8 @@ fun occursCon r =
con = fn L'.CUnif (_, _, _, r') => r = r'
| _ => false}
-datatype cunify_error =
- CKind of L'.kind * L'.kind * kunify_error
- | COccursCheckFailed of L'.con * L'.con
- | CIncompatible of L'.con * L'.con
- | CExplicitness of L'.con * L'.con
- | CKindof of L'.kind * L'.con
- | CRecordFailure of PD.pp_desc * PD.pp_desc
-
exception CUnify' of cunify_error
-fun cunifyError env err =
- case err of
- CKind (k1, k2, kerr) =>
- (eprefaces "Kind unification failure"
- [("Kind 1", p_kind k1),
- ("Kind 2", p_kind k2)];
- kunifyError kerr)
- | COccursCheckFailed (c1, c2) =>
- eprefaces "Constructor occurs check failed"
- [("Con 1", p_con env c1),
- ("Con 2", p_con env c2)]
- | CIncompatible (c1, c2) =>
- eprefaces "Incompatible constructors"
- [("Con 1", p_con env c1),
- ("Con 2", p_con env c2)]
- | CExplicitness (c1, c2) =>
- eprefaces "Differing constructor function explicitness"
- [("Con 1", p_con env c1),
- ("Con 2", p_con env c2)]
- | CKindof (k, c) =>
- eprefaces "Unexpected kind for kindof calculation"
- [("Kind", p_kind k),
- ("Con", p_con env c)]
- | CRecordFailure (s1, s2) =>
- eprefaces "Can't unify record constructors"
- [("Summary 1", s1),
- ("Summary 2", s2)]
-
exception SynUnif = E.SynUnif
open ElabOps
@@ -801,18 +717,29 @@ and unifySummaries (env, denv) (k, s1 : record_summary, s2 : record_summary) =
| _ => false
val empty = (L'.CRecord (k, []), dummy)
+ fun unsummarize {fields, unifs, others} =
+ let
+ val c = (L'.CRecord (k, fields), loc)
+
+ val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc))
+ c unifs
+ in
+ foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc))
+ c others
+ end
+
fun pairOffUnifs (unifs1, unifs2) =
case (unifs1, unifs2) of
([], _) =>
if clear then
List.app (fn (_, r) => r := SOME empty) unifs2
else
- raise CUnify' (CRecordFailure (p_summary env s1, p_summary env s2))
+ raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
| (_, []) =>
if clear then
List.app (fn (_, r) => r := SOME empty) unifs1
else
- raise CUnify' (CRecordFailure (p_summary env s1, p_summary env s2))
+ raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
| ((c1, _) :: rest1, (_, r2) :: rest2) =>
(r2 := SOME c1;
pairOffUnifs (rest1, rest2))
@@ -1027,77 +954,6 @@ and unifyCons (env, denv) c1 c2 =
unifyCons' (env, denv) c1 c2
handle CUnify' err => raise CUnify (c1, c2, err)
| KUnify args => raise CUnify (c1, c2, CKind args)
-
-datatype exp_error =
- UnboundExp of ErrorMsg.span * string
- | UnboundStrInExp of ErrorMsg.span * string
- | Unify of L'.exp * L'.con * L'.con * cunify_error
- | Unif of string * L'.con
- | WrongForm of string * L'.exp * L'.con
- | IncompatibleCons of L'.con * L'.con
- | DuplicatePatternVariable of ErrorMsg.span * string
- | PatUnify of L'.pat * L'.con * L'.con * cunify_error
- | UnboundConstructor of ErrorMsg.span * string list * string
- | PatHasArg of ErrorMsg.span
- | PatHasNoArg of ErrorMsg.span
- | Inexhaustive of ErrorMsg.span
- | DuplicatePatField of ErrorMsg.span * string
- | Unresolvable of ErrorMsg.span * L'.con
- | OutOfContext of ErrorMsg.span * (L'.exp * L'.con) option
- | IllegalRec of string * L'.exp
-
-fun expError env err =
- case err of
- UnboundExp (loc, s) =>
- ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
- | UnboundStrInExp (loc, s) =>
- ErrorMsg.errorAt loc ("Unbound structure " ^ s)
- | Unify (e, c1, c2, uerr) =>
- (ErrorMsg.errorAt (#2 e) "Unification failure";
- eprefaces' [("Expression", p_exp env e),
- ("Have con", p_con env c1),
- ("Need con", p_con env c2)];
- cunifyError env uerr)
- | Unif (action, c) =>
- (ErrorMsg.errorAt (#2 c) ("Unification variable blocks " ^ action);
- eprefaces' [("Con", p_con env c)])
- | WrongForm (variety, e, t) =>
- (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
- eprefaces' [("Expression", p_exp env e),
- ("Type", p_con env t)])
- | IncompatibleCons (c1, c2) =>
- (ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
- eprefaces' [("Con 1", p_con env c1),
- ("Con 2", p_con env c2)])
- | DuplicatePatternVariable (loc, s) =>
- ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
- | PatUnify (p, c1, c2, uerr) =>
- (ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
- eprefaces' [("Pattern", p_pat env p),
- ("Have con", p_con env c1),
- ("Need con", p_con env c2)];
- cunifyError env uerr)
- | UnboundConstructor (loc, ms, s) =>
- ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern")
- | PatHasArg loc =>
- ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
- | PatHasNoArg loc =>
- ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
- | Inexhaustive loc =>
- ErrorMsg.errorAt loc "Inexhaustive 'case'"
- | DuplicatePatField (loc, s) =>
- ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern")
- | OutOfContext (loc, co) =>
- (ErrorMsg.errorAt loc "Type class wildcard occurs out of context";
- Option.app (fn (e, c) => eprefaces' [("Function", p_exp env e),
- ("Type", p_con env c)]) co)
- | Unresolvable (loc, c) =>
- (ErrorMsg.errorAt loc "Can't resolve type class instance";
- eprefaces' [("Class constraint", p_con env c)])
- | IllegalRec (x, e) =>
- (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
- eprefaces' [("Variable", PD.string x),
- ("Expression", p_exp env e)])
fun checkCon (env, denv) e c1 c2 =
unifyCons (env, denv) c1 c2
@@ -1787,133 +1643,6 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
("|tcs|", PD.string (Int.toString (length tcs)))];*)
r
end
-
-
-datatype decl_error =
- KunifsRemain of L'.decl list
- | CunifsRemain of L'.decl list
- | Nonpositive of L'.decl
-
-fun lspan [] = ErrorMsg.dummySpan
- | lspan ((_, loc) :: _) = loc
-
-fun declError env err =
- case err of
- KunifsRemain ds =>
- (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration";
- eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
- | CunifsRemain ds =>
- (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration";
- eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
- | Nonpositive d =>
- (ErrorMsg.errorAt (#2 d) "Non-strictly-positive datatype declaration (could allow non-termination)";
- eprefaces' [("Decl", p_decl env d)])
-
-datatype sgn_error =
- UnboundSgn of ErrorMsg.span * string
- | UnmatchedSgi of L'.sgn_item
- | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
- | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
- | SgiMismatchedDatatypes of L'.sgn_item * L'.sgn_item * (L'.con * L'.con * cunify_error) option
- | SgnWrongForm of L'.sgn * L'.sgn
- | UnWhereable of L'.sgn * string
- | WhereWrongKind of L'.kind * L'.kind * kunify_error
- | NotIncludable of L'.sgn
- | DuplicateCon of ErrorMsg.span * string
- | DuplicateVal of ErrorMsg.span * string
- | DuplicateSgn of ErrorMsg.span * string
- | DuplicateStr of ErrorMsg.span * string
- | NotConstraintsable of L'.sgn
-
-fun sgnError env err =
- case err of
- UnboundSgn (loc, s) =>
- ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
- | UnmatchedSgi (sgi as (_, loc)) =>
- (ErrorMsg.errorAt loc "Unmatched signature item";
- eprefaces' [("Item", p_sgn_item env sgi)])
- | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
- (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
- eprefaces' [("Have", p_sgn_item env sgi1),
- ("Need", p_sgn_item env sgi2),
- ("Kind 1", p_kind k1),
- ("Kind 2", p_kind k2)];
- kunifyError kerr)
- | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
- (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
- eprefaces' [("Have", p_sgn_item env sgi1),
- ("Need", p_sgn_item env sgi2),
- ("Con 1", p_con env c1),
- ("Con 2", p_con env c2)];
- cunifyError env cerr)
- | SgiMismatchedDatatypes (sgi1, sgi2, cerro) =>
- (ErrorMsg.errorAt (#2 sgi1) "Mismatched 'datatype' specifications:";
- eprefaces' [("Have", p_sgn_item env sgi1),
- ("Need", p_sgn_item env sgi2)];
- Option.app (fn (c1, c2, ue) =>
- (eprefaces "Unification error"
- [("Con 1", p_con env c1),
- ("Con 2", p_con env c2)];
- cunifyError env ue)) cerro)
- | SgnWrongForm (sgn1, sgn2) =>
- (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
- eprefaces' [("Sig 1", p_sgn env sgn1),
- ("Sig 2", p_sgn env sgn2)])
- | UnWhereable (sgn, x) =>
- (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
- eprefaces' [("Signature", p_sgn env sgn),
- ("Field", PD.string x)])
- | WhereWrongKind (k1, k2, kerr) =>
- (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
- eprefaces' [("Have", p_kind k1),
- ("Need", p_kind k2)];
- kunifyError kerr)
- | NotIncludable sgn =>
- (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
- eprefaces' [("Signature", p_sgn env sgn)])
- | DuplicateCon (loc, s) =>
- ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
- | DuplicateVal (loc, s) =>
- ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature")
- | DuplicateSgn (loc, s) =>
- ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
- | DuplicateStr (loc, s) =>
- ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
- | NotConstraintsable sgn =>
- (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'";
- eprefaces' [("Signature", p_sgn env sgn)])
-
-datatype str_error =
- UnboundStr of ErrorMsg.span * string
- | NotFunctor of L'.sgn
- | FunctorRebind of ErrorMsg.span
- | UnOpenable of L'.sgn
- | NotType of L'.kind * (L'.kind * L'.kind * kunify_error)
- | DuplicateConstructor of string * ErrorMsg.span
- | NotDatatype of ErrorMsg.span
-
-fun strError env err =
- case err of
- UnboundStr (loc, s) =>
- ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
- | NotFunctor sgn =>
- (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
- eprefaces' [("Signature", p_sgn env sgn)])
- | FunctorRebind loc =>
- ErrorMsg.errorAt loc "Attempt to rebind functor"
- | UnOpenable sgn =>
- (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
- eprefaces' [("Signature", p_sgn env sgn)])
- | NotType (k, (k1, k2, ue)) =>
- (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
- eprefaces' [("Kind", p_kind k),
- ("Subkind 1", p_kind k1),
- ("Subkind 2", p_kind k2)];
- kunifyError ue)
- | DuplicateConstructor (x, loc) =>
- ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
- | NotDatatype loc =>
- ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
val hnormSgn = E.hnormSgn
@@ -3527,12 +3256,16 @@ fun elabFile basis topStr topSgn env file =
val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan)
val () = case gs of
[] => ()
- | _ => (app (fn Disjoint (_, env, _, c1, c2) =>
- prefaces "Unresolved"
- [("c1", p_con env c1),
- ("c2", p_con env c2)]
- | TypeClass _ => TextIO.print "Type class\n") gs;
- raise Fail "Unresolved constraints in top.ur")
+ | _ => app (fn Disjoint (loc, env, denv, c1, c2) =>
+ (case D.prove env denv (c1, c2, loc) of
+ [] => ()
+ | _ =>
+ (prefaces "Unresolved constraint in top.ur"
+ [("loc", PD.string (ErrorMsg.spanToString loc)),
+ ("c1", p_con env c1),
+ ("c2", p_con env c2)];
+ raise Fail "Unresolve constraint in top.ur"))
+ | TypeClass _ => raise Fail "Unresolved type class constraint in top.ur") gs
val () = subSgn (env', D.empty) topSgn' topSgn
val (env', top_n) = E.pushStrNamed env' "Top" topSgn
diff --git a/src/sources b/src/sources
index a30626a8..506f1767 100644
--- a/src/sources
+++ b/src/sources
@@ -41,6 +41,9 @@ elab_ops.sml
disjoint.sig
disjoint.sml
+elab_err.sig
+elab_err.sml
+
elaborate.sig
elaborate.sml
diff --git a/src/urweb.grm b/src/urweb.grm
index c8dd5698..ff53b4b8 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -543,6 +543,13 @@ carg : SYMBOL DCOLON kind (fn (c, k) =>
((CAbs (SYMBOL, SOME kind, c), loc),
(KArrow (kind, k), loc))
end)
+ | UNDER DCOLON kind (fn (c, k) =>
+ let
+ val loc = s (UNDERleft, kindright)
+ in
+ ((CAbs ("_", SOME kind, c), loc),
+ (KArrow (kind, k), loc))
+ end)
| cargp (cargp)
cargp : SYMBOL (fn (c, k) =>
@@ -552,6 +559,13 @@ cargp : SYMBOL (fn (c, k) =>
((CAbs (SYMBOL, NONE, c), loc),
(KArrow ((KWild, loc), k), loc))
end)
+ | UNDER (fn (c, k) =>
+ let
+ val loc = s (UNDERleft, UNDERright)
+ in
+ ((CAbs ("_", NONE, c), loc),
+ (KArrow ((KWild, loc), k), loc))
+ end)
| LPAREN SYMBOL DCOLON kind RPAREN (fn (c, k) =>
let
val loc = s (LPARENleft, RPARENright)
diff --git a/tests/crud.ur b/tests/crud.ur
index c3e76e6a..3837061e 100644
--- a/tests/crud.ur
+++ b/tests/crud.ur
@@ -1,4 +1,5 @@
-con colMeta = fn cols :: {Type} => $(Top.mapTT (fn t => {Show : t -> xbody}) cols)
+con colMeta' = fn t :: Type => {Show : t -> xbody}
+con colMeta = fn cols :: {Type} => $(Top.mapTT colMeta' cols)
functor Make(M : sig
con cols :: {Type}
@@ -15,19 +16,19 @@ val tab = M.tab
fun list () =
rows <- query (SELECT * FROM tab AS T)
- (fn fs acc => return <body>
+ (fn (fs : {T : $([Id = int] ++ M.cols)}) acc => return <body>
{acc}
<tr>
<td>{txt _ fs.T.Id}</td>
- {fold [fn cols :: {Type} => $cols -> colMeta cols -> xtr]
- (fn (nm :: Name) (t :: Type) (rest :: {Type}) acc =>
+ {foldTR2 [idT] [colMeta'] [fn _ => xtr]
+ (fn (nm :: Name) (t :: Type) (rest :: {Type}) =>
[[nm] ~ rest] =>
- fn r cols =>
+ fn v funcs acc =>
<tr>
- <td>{cols.nm.Show r.nm}</td>
- {acc (r -- nm) (cols -- nm)}
+ <td>{funcs.Show v}</td>
+ {acc}
</tr>)
- (fn _ _ => <tr></tr>)
+ <tr></tr>
[M.cols] (fs.T -- #Id) M.cols}
</tr>
</body>) <body></body>;
diff --git a/tests/crud.urs b/tests/crud.urs
index c021bea3..4741af00 100644
--- a/tests/crud.urs
+++ b/tests/crud.urs
@@ -1,4 +1,5 @@
-con colMeta = fn cols :: {Type} => $(mapTT (fn t => {Show : t -> xbody}) cols)
+con colMeta' = fn t :: Type => {Show : t -> xbody}
+con colMeta = fn cols :: {Type} => $(Top.mapTT colMeta' cols)
functor Make(M : sig
con cols :: {Type}
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-04 00:37:41 +0000