Mercurial > urweb
changeset 329:eec65c11d3e2
foldTR2
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 13 Sep 2008 10:30:45 -0400 |
| parents | 58f1260f293f |
| children | f307cdd08d81 |
| files | lib/top.ur lib/top.urs src/elab_err.sig src/elab_err.sml src/elab_ops.sml src/elab_util.sig src/elab_util.sml src/elaborate.sml src/sources src/urweb.grm tests/crud.ur tests/crud.urs |
| diffstat | 12 files changed, 593 insertions(+), 328 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/top.ur Thu Sep 11 19:59:31 2008 -0400 +++ b/lib/top.ur Sat Sep 13 10:30:45 2008 -0400 @@ -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 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 []) =
--- a/lib/top.urs Thu Sep 11 19:59:31 2008 -0400 +++ b/lib/top.urs Sat Sep 13 10:30:45 2008 -0400 @@ -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 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/elab_err.sig Sat Sep 13 10:30:45 2008 -0400 @@ -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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/elab_err.sml Sat Sep 13 10:30:45 2008 -0400 @@ -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
--- a/src/elab_ops.sml Thu Sep 11 19:59:31 2008 -0400 +++ b/src/elab_ops.sml Sat Sep 13 10:30:45 2008 -0400 @@ -127,7 +127,47 @@ (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 @@ | ((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
--- a/src/elab_util.sig Thu Sep 11 19:59:31 2008 -0400 +++ b/src/elab_util.sig Sat Sep 13 10:30:45 2008 -0400 @@ -38,7 +38,7 @@ 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 @@ 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 @@ 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 @@ 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
--- a/src/elab_util.sml Thu Sep 11 19:59:31 2008 -0400 +++ b/src/elab_util.sml Sat Sep 13 10:30:45 2008 -0400 @@ -96,7 +96,7 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ | 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))
--- a/src/elaborate.sml Thu Sep 11 19:59:31 2008 -0400 +++ b/src/elaborate.sml Sat Sep 13 10:30:45 2008 -0400 @@ -36,6 +36,7 @@ open Print open ElabPrint +open ElabErr structure IM = IntBinaryMap @@ -58,23 +59,8 @@ 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 @@ 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 @@ 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 @@ | _ => 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 @@ 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 @@ ("|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 @@ 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
--- a/src/sources Thu Sep 11 19:59:31 2008 -0400 +++ b/src/sources Sat Sep 13 10:30:45 2008 -0400 @@ -41,6 +41,9 @@ disjoint.sig disjoint.sml +elab_err.sig +elab_err.sml + elaborate.sig elaborate.sml
--- a/src/urweb.grm Thu Sep 11 19:59:31 2008 -0400 +++ b/src/urweb.grm Sat Sep 13 10:30:45 2008 -0400 @@ -543,6 +543,13 @@ ((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 @@ ((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)
--- a/tests/crud.ur Thu Sep 11 19:59:31 2008 -0400 +++ b/tests/crud.ur Sat Sep 13 10:30:45 2008 -0400 @@ -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 @@ 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>;
--- a/tests/crud.urs Thu Sep 11 19:59:31 2008 -0400 +++ b/tests/crud.urs Sat Sep 13 10:30:45 2008 -0400 @@ -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}