diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/core.sml | 1 | ||||
| -rw-r--r-- | src/core_print.sml | 1 | ||||
| -rw-r--r-- | src/core_util.sml | 8 | ||||
| -rw-r--r-- | src/corify.sml | 1 | ||||
| -rw-r--r-- | src/elab.sml | 11 | ||||
| -rw-r--r-- | src/elab_env.sig | 4 | ||||
| -rw-r--r-- | src/elab_env.sml | 130 | ||||
| -rw-r--r-- | src/elab_err.sig | 7 | ||||
| -rw-r--r-- | src/elab_err.sml | 61 | ||||
| -rw-r--r-- | src/elab_ops.sig | 6 | ||||
| -rw-r--r-- | src/elab_ops.sml | 69 | ||||
| -rw-r--r-- | src/elab_print.sig | 2 | ||||
| -rw-r--r-- | src/elab_print.sml | 95 | ||||
| -rw-r--r-- | src/elab_util.sig | 38 | ||||
| -rw-r--r-- | src/elab_util.sml | 154 | ||||
| -rw-r--r-- | src/elaborate.sml | 241 | ||||
| -rw-r--r-- | src/expl.sml | 1 | ||||
| -rw-r--r-- | src/expl_print.sml | 1 | ||||
| -rw-r--r-- | src/expl_util.sml | 4 | ||||
| -rw-r--r-- | src/explify.sml | 2 | ||||
| -rw-r--r-- | src/monoize.sml | 1 | ||||
| -rw-r--r-- | src/reduce.sml | 16 | ||||
| -rw-r--r-- | src/reduce_local.sml | 2 | ||||
| -rw-r--r-- | src/source.sml | 9 | ||||
| -rw-r--r-- | src/source_print.sml | 26 | ||||
| -rw-r--r-- | src/termination.sml | 9 | ||||
| -rw-r--r-- | src/unnest.sml | 18 | ||||
| -rw-r--r-- | src/urweb.grm | 23 | ||||
| -rw-r--r-- | src/urweb.lex | 3 |
29 files changed, 658 insertions, 286 deletions
diff --git a/src/core.sml b/src/core.sml index d7a57493..a28d93dd 100644 --- a/src/core.sml +++ b/src/core.sml @@ -96,7 +96,6 @@ datatype exp' = | EConcat of exp * con * exp * con | ECut of exp * con * { field : con, rest : con } | ECutMulti of exp * con * { rest : con } - | EFold of kind | ECase of exp * (pat * exp) list * { disc : con, result : con } diff --git a/src/core_print.sml b/src/core_print.sml index db8c3907..504773ab 100644 --- a/src/core_print.sml +++ b/src/core_print.sml @@ -342,7 +342,6 @@ fun p_exp' par env (e, _) = string "---", space, p_con' true env c]) - | EFold _ => string "fold" | ECase (e, pes, {disc, result}) => parenIf par (box [string "case", diff --git a/src/core_util.sml b/src/core_util.sml index e76da387..d5f8dd05 100644 --- a/src/core_util.sml +++ b/src/core_util.sml @@ -454,10 +454,6 @@ fun compare ((e1, _), (e2, _)) = | (ECutMulti _, _) => LESS | (_, ECutMulti _) => GREATER - | (EFold _, EFold _) => EQUAL - | (EFold _, _) => LESS - | (_, EFold _) => GREATER - | (ECase (e1, pes1, _), ECase (e2, pes2, _)) => join (compare (e1, e2), fn () => joinL (fn ((p1, e1), (p2, e2)) => @@ -609,10 +605,6 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = S.map2 (mfc ctx rest, fn rest' => (ECutMulti (e', c', {rest = rest'}), loc)))) - | EFold k => - S.map2 (mfk k, - fn k' => - (EFold k', loc)) | ECase (e, pes, {disc, result}) => S.bind2 (mfe ctx e, diff --git a/src/corify.sml b/src/corify.sml index c464e5a5..802baf66 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -592,7 +592,6 @@ fun corifyExp st (e, loc) = {field = corifyCon st field, rest = corifyCon st rest}), loc) | L.ECutMulti (e1, c, {rest}) => (L'.ECutMulti (corifyExp st e1, corifyCon st c, {rest = corifyCon st rest}), loc) - | L.EFold k => (L'.EFold (corifyKind k), loc) | L.ECase (e, pes, {disc, result}) => (L'.ECase (corifyExp st e, diff --git a/src/elab.sml b/src/elab.sml index ec8a910a..9ec3793e 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -40,6 +40,9 @@ datatype kind' = | KError | KUnif of ErrorMsg.span * string * kind option ref + | KRel of int + | KFun of string * kind + withtype kind = kind' located datatype explicitness = @@ -62,6 +65,10 @@ datatype con' = | CAbs of string * kind * con | CDisjoint of auto_instantiate * con * con * con + | CKAbs of string * con + | CKApp of con * kind + | TKFun of string * con + | CName of string | CRecord of kind * (con * con) list @@ -106,12 +113,14 @@ datatype exp' = | ECApp of exp * con | ECAbs of explicitness * string * kind * exp + | EKAbs of string * exp + | EKApp of exp * kind + | ERecord of (con * exp * con) list | EField of exp * con * { field : con, rest : con } | EConcat of exp * con * exp * con | ECut of exp * con * { field : con, rest : con } | ECutMulti of exp * con * { rest : con } - | EFold of kind | ECase of exp * (pat * exp) list * { disc : con, result : con } diff --git a/src/elab_env.sig b/src/elab_env.sig index 0b436106..10d11e3b 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -47,6 +47,10 @@ signature ELAB_ENV = sig | Rel of int * 'a | Named of int * 'a + val pushKRel : env -> string -> env + val lookupKRel : env -> int -> string + val lookupK : env -> string -> int option + val pushCRel : env -> string -> Elab.kind -> env val lookupCRel : env -> int -> string * Elab.kind diff --git a/src/elab_env.sml b/src/elab_env.sml index 53c934dd..083e7d55 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -45,8 +45,32 @@ exception UnboundNamed of int exception SynUnif +val liftKindInKind = + U.Kind.mapB {kind = fn bound => fn k => + case k of + KRel xn => + if xn < bound then + k + else + KRel (xn + 1) + | _ => k, + bind = fn (bound, _) => bound + 1} + +val liftKindInCon = + U.Con.mapB {kind = fn bound => fn k => + case k of + KRel xn => + if xn < bound then + k + else + KRel (xn + 1) + | _ => k, + con = fn _ => fn c => c, + bind = fn (bound, U.Con.RelK _) => bound + 1 + | (bound, _) => bound} + val liftConInCon = - U.Con.mapB {kind = fn k => k, + U.Con.mapB {kind = fn _ => fn k => k, con = fn bound => fn c => case c of CRel xn => @@ -56,13 +80,27 @@ val liftConInCon = CRel (xn + 1) (*| CUnif _ => raise SynUnif*) | _ => c, - bind = fn (bound, U.Con.Rel _) => bound + 1 + bind = fn (bound, U.Con.RelC _) => bound + 1 | (bound, _) => bound} val lift = liftConInCon 0 +val liftKindInExp = + U.Exp.mapB {kind = fn bound => fn k => + case k of + KRel xn => + if xn < bound then + k + else + KRel (xn + 1) + | _ => k, + con = fn _ => fn c => c, + exp = fn _ => fn e => e, + bind = fn (bound, U.Exp.RelK _) => bound + 1 + | (bound, _) => bound} + val liftConInExp = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn bound => fn c => case c of CRel xn => @@ -76,7 +114,7 @@ val liftConInExp = | (bound, _) => bound} val liftExpInExp = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn _ => fn c => c, exp = fn bound => fn e => case e of @@ -93,7 +131,7 @@ val liftExpInExp = val liftExp = liftExpInExp 0 val subExpInExp = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn _ => fn c => c, exp = fn (xn, rep) => fn e => case e of @@ -203,6 +241,9 @@ fun printClasses cs = (print "Classes:\n"; print "\n")) cs) type env = { + renameK : int SM.map, + relK : string list, + renameC : kind var' SM.map, relC : (string * kind) list, namedC : (string * kind * con option) IM.map, @@ -234,6 +275,9 @@ fun newNamed () = end val empty = { + renameK = SM.empty, + relK = [], + renameC = SM.empty, relC = [], namedC = IM.empty, @@ -261,12 +305,51 @@ fun liftClassKey ck = | CkProj _ => ck | CkApp (ck1, ck2) => CkApp (liftClassKey ck1, liftClassKey ck2) +fun pushKRel (env : env) x = + let + val renameK = SM.map (fn n => n+1) (#renameK env) + in + {renameK = SM.insert (renameK, x, 0), + relK = x :: #relK env, + + renameC = SM.map (fn Rel' (n, k) => Rel' (n, liftKindInKind 0 k) + | x => x) (#renameC env), + relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env), + namedC = #namedC env, + + datatypes = #datatypes env, + constructors = #constructors env, + + classes = #classes env, + + renameE = SM.map (fn Rel' (n, c) => Rel' (n, liftKindInCon 0 c) + | Named' (n, c) => Named' (n, c)) (#renameE env), + relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env), + namedE = #namedE env, + + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = #renameStr env, + str = #str env + } + end + +fun lookupKRel (env : env) n = + (List.nth (#relK env, n)) + handle Subscript => raise UnboundRel n + +fun lookupK (env : env) x = SM.find (#renameK env, x) + fun pushCRel (env : env) x k = let val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k) | x => x) (#renameC env) in - {renameC = SM.insert (renameC, x, Rel' (0, k)), + {renameK = #renameK env, + relK = #relK env, + + renameC = SM.insert (renameC, x, Rel' (0, k)), relC = (x, k) :: #relC env, namedC = #namedC env, @@ -298,7 +381,10 @@ fun lookupCRel (env : env) n = handle Subscript => raise UnboundRel n fun pushCNamedAs (env : env) x n k co = - {renameC = SM.insert (#renameC env, x, Named' (n, k)), + {renameK = #renameK env, + relK = #relK env, + + renameC = SM.insert (#renameC env, x, Named' (n, k)), relC = #relC env, namedC = IM.insert (#namedC env, n, (x, k, co)), @@ -340,7 +426,10 @@ fun pushDatatype (env : env) n xs xncs = let val dk = U.classifyDatatype xncs in - {renameC = #renameC env, + {renameK = #renameK env, + relK = #relK env, + + renameC = #renameC env, relC = #relC env, namedC = #namedC env, @@ -380,7 +469,10 @@ fun datatypeArgs (xs, _) = xs fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt fun pushClass (env : env) n = - {renameC = #renameC env, + {renameK = #renameK env, + relK = #relK env, + + renameC = #renameC env, relC = #relC env, namedC = #namedC env, @@ -468,7 +560,10 @@ fun pushERel (env : env) x t = CM.insert (classes, f, class) end in - {renameC = #renameC env, + {renameK = #renameK env, + relK = #relK env, + + renameC = #renameC env, relC = #relC env, namedC = #namedC env, @@ -509,7 +604,10 @@ fun pushENamedAs (env : env) x n t = CM.insert (classes, f, class) end in - {renameC = #renameC env, + {renameK = #renameK env, + relK = #relK env, + + renameC = #renameC env, relC = #relC env, namedC = #namedC env, @@ -552,7 +650,10 @@ fun lookupE (env : env) x = | SOME (Named' x) => Named x fun pushSgnNamedAs (env : env) x n sgis = - {renameC = #renameC env, + {renameK = #renameK env, + relK = #relK env, + + renameC = #renameC env, relC = #relC env, namedC = #namedC env, @@ -868,7 +969,10 @@ fun enrichClasses env classes (m1, ms) sgn = | _ => classes fun pushStrNamedAs (env : env) x n sgn = - {renameC = #renameC env, + {renameK = #renameK env, + relK = #relK env, + + renameC = #renameC env, relC = #relC env, namedC = #namedC env, diff --git a/src/elab_err.sig b/src/elab_err.sig index d757572f..3b14406b 100644 --- a/src/elab_err.sig +++ b/src/elab_err.sig @@ -27,11 +27,16 @@ signature ELAB_ERR = sig + datatype kind_error = + UnboundKind of ErrorMsg.span * string + + val kindError : ElabEnv.env -> kind_error -> unit + datatype kunify_error = KOccursCheckFailed of Elab.kind * Elab.kind | KIncompatible of Elab.kind * Elab.kind - val kunifyError : kunify_error -> unit + val kunifyError : ElabEnv.env -> kunify_error -> unit datatype con_error = UnboundCon of ErrorMsg.span * string diff --git a/src/elab_err.sml b/src/elab_err.sml index e8d7ff68..8892674c 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -36,7 +36,7 @@ structure U = ElabUtil open Print structure P = ElabPrint -val simplCon = U.Con.mapB {kind = fn k => k, +val simplCon = U.Con.mapB {kind = fn _ => fn k => k, con = fn env => fn c => let val c = (c, ErrorMsg.dummySpan) @@ -46,25 +46,34 @@ val simplCon = U.Con.mapB {kind = fn k => k, ("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} + bind = fn (env, U.Con.RelC (x, k)) => E.pushCRel env x k + | (env, U.Con.NamedC (x, n, k)) => E.pushCNamedAs env x n k NONE + | (env, _) => env} val p_kind = P.p_kind + +datatype kind_error = + UnboundKind of ErrorMsg.span * string + +fun kindError env err = + case err of + UnboundKind (loc, s) => + ErrorMsg.errorAt loc ("Unbound kind variable " ^ s) datatype kunify_error = KOccursCheckFailed of kind * kind | KIncompatible of kind * kind -fun kunifyError err = +fun kunifyError env err = case err of KOccursCheckFailed (k1, k2) => eprefaces "Kind occurs check failed" - [("Kind 1", p_kind k1), - ("Kind 2", p_kind k2)] + [("Kind 1", p_kind env k1), + ("Kind 2", p_kind env k2)] | KIncompatible (k1, k2) => eprefaces "Incompatible kinds" - [("Kind 1", p_kind k1), - ("Kind 2", p_kind k2)] + [("Kind 1", p_kind env k1), + ("Kind 2", p_kind env k2)] fun p_con env c = P.p_con env (simplCon env c) @@ -89,9 +98,9 @@ fun conError env err = | 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) + ("Have kind", p_kind env k1), + ("Need kind", p_kind env k2)]; + kunifyError env kerr) | DuplicateField (loc, s) => ErrorMsg.errorAt loc ("Duplicate record field " ^ s) | ProjBounds (c, n) => @@ -101,7 +110,7 @@ fun conError env err = | ProjMismatch (c, k) => (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor"; eprefaces' [("Constructor", p_con env c), - ("Kind", p_kind k)]) + ("Kind", p_kind env k)]) datatype cunify_error = @@ -116,9 +125,9 @@ 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) + [("Kind 1", p_kind env k1), + ("Kind 2", p_kind env k2)]; + kunifyError env kerr) | COccursCheckFailed (c1, c2) => eprefaces "Constructor occurs check failed" [("Con 1", p_con env c1), @@ -133,7 +142,7 @@ fun cunifyError env err = ("Con 2", p_con env c2)] | CKindof (k, c, expected) => eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")") - [("Kind", p_kind k), + [("Kind", p_kind env k), ("Con", p_con env c)] | CRecordFailure (c1, c2) => eprefaces "Can't unify record constructors" @@ -267,9 +276,9 @@ fun sgnError env err = (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) + ("Kind 1", p_kind env k1), + ("Kind 2", p_kind env k2)]; + kunifyError env kerr) | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) => (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:"; eprefaces' [("Have", p_sgn_item env sgi1), @@ -296,9 +305,9 @@ fun sgnError env err = ("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) + eprefaces' [("Have", p_kind env k1), + ("Need", p_kind env k2)]; + kunifyError env kerr) | NotIncludable sgn => (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'"; eprefaces' [("Signature", p_sgn env sgn)]) @@ -337,10 +346,10 @@ fun strError env err = 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) + eprefaces' [("Kind", p_kind env k), + ("Subkind 1", p_kind env k1), + ("Subkind 2", p_kind env k2)]; + kunifyError env ue) | DuplicateConstructor (x, loc) => ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x) | NotDatatype loc => diff --git a/src/elab_ops.sig b/src/elab_ops.sig index 62af9638..7088bf06 100644 --- a/src/elab_ops.sig +++ b/src/elab_ops.sig @@ -27,6 +27,12 @@ signature ELAB_OPS = sig + val liftKindInKind : int -> Elab.kind -> Elab.kind + val subKindInKind : int * Elab.kind -> Elab.kind -> Elab.kind + + val liftKindInCon : int -> Elab.con -> Elab.con + val subKindInCon : int * Elab.kind -> Elab.con -> Elab.con + val liftConInCon : int -> Elab.con -> Elab.con val subConInCon : int * Elab.con -> Elab.con -> Elab.con val subStrInSgn : int * int -> Elab.sgn -> Elab.sgn diff --git a/src/elab_ops.sml b/src/elab_ops.sml index c3e9274c..60a7639d 100644 --- a/src/elab_ops.sml +++ b/src/elab_ops.sml @@ -32,8 +32,64 @@ open Elab structure E = ElabEnv structure U = ElabUtil +fun liftKindInKind' by = + U.Kind.mapB {kind = fn bound => fn k => + case k of + KRel xn => + if xn < bound then + k + else + KRel (xn + by) + | _ => k, + bind = fn (bound, _) => bound + 1} + +fun subKindInKind' rep = + U.Kind.mapB {kind = fn (by, xn) => fn k => + case k of + KRel xn' => + (case Int.compare (xn', xn) of + EQUAL => #1 (liftKindInKind' by 0 rep) + | GREATER => KRel (xn' - 1) + | LESS => k) + | _ => k, + bind = fn ((by, xn), _) => (by+1, xn+1)} + +val liftKindInKind = liftKindInKind' 1 + +fun subKindInKind (xn, rep) = subKindInKind' rep (0, xn) + +fun liftKindInCon by = + U.Con.mapB {kind = fn bound => fn k => + case k of + KRel xn => + if xn < bound then + k + else + KRel (xn + by) + | _ => k, + con = fn _ => fn c => c, + bind = fn (bound, U.Con.RelK _) => bound + 1 + | (bound, _) => bound} + +fun subKindInCon' rep = + U.Con.mapB {kind = fn (by, xn) => fn k => + case k of + KRel xn' => + (case Int.compare (xn', xn) of + EQUAL => #1 (liftKindInKind' by 0 rep) + | GREATER => KRel (xn' - 1) + | LESS => k) + | _ => k, + con = fn _ => fn c => c, + bind = fn ((by, xn), U.Con.RelK _) => (by+1, xn+1) + | (st, _) => st} + +val liftKindInCon = liftKindInCon 1 + +fun subKindInCon (xn, rep) = subKindInCon' rep (0, xn) + fun liftConInCon by = - U.Con.mapB {kind = fn k => k, + U.Con.mapB {kind = fn _ => fn k => k, con = fn bound => fn c => case c of CRel xn => @@ -43,11 +99,11 @@ fun liftConInCon by = CRel (xn + by) (*| CUnif _ => raise SynUnif*) | _ => c, - bind = fn (bound, U.Con.Rel _) => bound + 1 + bind = fn (bound, U.Con.RelC _) => bound + 1 | (bound, _) => bound} fun subConInCon' rep = - U.Con.mapB {kind = fn k => k, + U.Con.mapB {kind = fn _ => fn k => k, con = fn (by, xn) => fn c => case c of CRel xn' => @@ -57,7 +113,7 @@ fun subConInCon' rep = | LESS => c) (*| CUnif _ => raise SynUnif*) | _ => c, - bind = fn ((by, xn), U.Con.Rel _) => (by+1, xn+1) + bind = fn ((by, xn), U.Con.RelC _) => (by+1, xn+1) | (ctx, _) => ctx} val liftConInCon = liftConInCon 1 @@ -205,6 +261,11 @@ fun hnormCon env (cAll as (c, loc)) = | _ => default () end | c1' => (CApp ((c1', loc), hnormCon env c2), loc)) + + | CKApp (c1, k) => + (case hnormCon env c1 of + (CKAbs (_, body), _) => hnormCon env (subKindInCon (0, k) body) + | _ => cAll) | CConcat (c1, c2) => (case (hnormCon env c1, hnormCon env c2) of diff --git a/src/elab_print.sig b/src/elab_print.sig index 3d078576..41d72ca7 100644 --- a/src/elab_print.sig +++ b/src/elab_print.sig @@ -28,7 +28,7 @@ (* Pretty-printing Ur/Web *) signature ELAB_PRINT = sig - val p_kind : Elab.kind Print.printer + val p_kind : ElabEnv.env -> Elab.kind Print.printer val p_explicitness : Elab.explicitness Print.printer val p_con : ElabEnv.env -> Elab.con Print.printer val p_pat : ElabEnv.env -> Elab.pat Print.printer diff --git a/src/elab_print.sml b/src/elab_print.sml index 098c9259..a0e1a54a 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -38,25 +38,36 @@ structure E = ElabEnv val debug = ref false -fun p_kind' par (k, _) = +fun p_kind' par env (k, _) = case k of KType => string "Type" - | KArrow (k1, k2) => parenIf par (box [p_kind' true k1, + | KArrow (k1, k2) => parenIf par (box [p_kind' true env k1, space, string "->", space, - p_kind k2]) + p_kind env k2]) | KName => string "Name" - | KRecord k => box [string "{", p_kind k, string "}"] + | KRecord k => box [string "{", p_kind env k, string "}"] | KUnit => string "Unit" | KTuple ks => box [string "(", - p_list_sep (box [space, string "*", space]) p_kind ks, + p_list_sep (box [space, string "*", space]) (p_kind env) ks, string ")"] | KError => string "<ERROR>" - | KUnif (_, _, ref (SOME k)) => p_kind' par k + | KUnif (_, _, ref (SOME k)) => p_kind' par env k | KUnif (_, s, _) => string ("<UNIF:" ^ s ^ ">") + | KRel n => ((if !debug then + string (E.lookupKRel env n ^ "_" ^ Int.toString n) + else + string (E.lookupKRel env n)) + handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n)) + | KFun (x, k) => box [string x, + space, + string "-->", + space, + p_kind (E.pushKRel env x) k] + and p_kind k = p_kind' false k fun p_explicitness e = @@ -66,7 +77,7 @@ fun p_explicitness e = fun p_con' par env (c, _) = case c of - TFun (t1, t2) => parenIf par (box [p_con' true env t1, + TFun (t1, t2) => parenIf true (box [p_con' true env t1, space, string "->", space, @@ -75,20 +86,22 @@ fun p_con' par env (c, _) = space, p_explicitness e, space, - p_kind k, + p_kind env k, space, string "->", space, p_con (E.pushCRel env x k) c]) - | CDisjoint (_, c1, c2, c3) => parenIf par (box [p_con env c1, - space, - string "~", - space, - p_con env c2, - space, - string "=>", - space, - p_con env c3]) + | CDisjoint (ai, c1, c2, c3) => parenIf par (box [p_con env c1, + space, + string (case ai of + Instantiate => "~" + | LeaveAlone => "~~"), + space, + p_con env c2, + space, + string "=>", + space, + p_con env c3]) | TRecord (CRecord (_, xcs), _) => box [string "{", p_list (fn (x, c) => box [p_name env x, @@ -134,7 +147,7 @@ fun p_con' par env (c, _) = space, string "::", space, - p_kind k, + p_kind env k, space, string "=>", space, @@ -152,7 +165,7 @@ fun p_con' par env (c, _) = space, p_con env c]) xcs, string "]::", - p_kind k]) + p_kind env k]) else parenIf par (box [string "[", p_list (fn (x, c) => @@ -181,8 +194,24 @@ fun p_con' par env (c, _) = | CError => string "<ERROR>" | CUnif (_, _, _, ref (SOME c)) => p_con' par env c | CUnif (_, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"), - p_kind k, + p_kind env k, string ">"] + + | CKAbs (x, c) => box [string x, + space, + string "==>", + space, + p_con (E.pushKRel env x) c] + | CKApp (c, k) => box [p_con env c, + string "[[", + p_kind env k, + string "]]"] + | TKFun (x, c) => box [string x, + space, + string "-->", + space, + p_con (E.pushKRel env x) c] + and p_con env = p_con' false env @@ -286,7 +315,7 @@ fun p_exp' par env (e, _) = space, p_explicitness exp, space, - p_kind k, + p_kind env k, space, string "=>", space, @@ -377,8 +406,6 @@ fun p_exp' par env (e, _) = space, p_con' true env c]) - | EFold _ => string "fold" - | ECase (e, pes, _) => parenIf par (box [string "case", space, p_exp env e, @@ -415,6 +442,16 @@ fun p_exp' par env (e, _) = string "end"] end + | EKAbs (x, e) => box [string x, + space, + string "==>", + space, + p_exp (E.pushKRel env x) e] + | EKApp (e, k) => box [p_exp env e, + string "[[", + p_kind env k, + string "]]"] + and p_exp env = p_exp' false env and p_edecl env (dAll as (d, _)) = @@ -478,14 +515,14 @@ fun p_sgn_item env (sgi, _) = space, string "::", space, - p_kind k] + p_kind env k] | SgiCon (x, n, k, c) => box [string "con", space, p_named x n, space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space, @@ -540,14 +577,14 @@ fun p_sgn_item env (sgi, _) = space, string "::", space, - p_kind k] + p_kind env k] | SgiClass (x, n, k, c) => box [string "class", space, p_named x n, space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space, @@ -627,7 +664,7 @@ fun p_decl env (dAll as (d, _) : decl) = space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space, @@ -719,7 +756,7 @@ fun p_decl env (dAll as (d, _) : decl) = space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space, diff --git a/src/elab_util.sig b/src/elab_util.sig index f9988981..817f885f 100644 --- a/src/elab_util.sig +++ b/src/elab_util.sig @@ -30,17 +30,24 @@ signature ELAB_UTIL = sig val classifyDatatype : (string * int * 'a option) list -> Elab.datatype_kind structure Kind : sig + val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, + bind : 'context * string -> 'context} + -> ('context, Elab.kind, 'state, 'abort) Search.mapfolderB val mapfold : (Elab.kind', 'state, 'abort) Search.mapfolder -> (Elab.kind, 'state, 'abort) Search.mapfolder val exists : (Elab.kind' -> bool) -> Elab.kind -> bool + val mapB : {kind : 'context -> Elab.kind' -> Elab.kind', + bind : 'context * string -> 'context} + -> 'context -> (Elab.kind -> Elab.kind) end structure Con : sig datatype binder = - Rel of string * Elab.kind - | Named of string * int * Elab.kind + RelK of string + | RelC of string * Elab.kind + | NamedC of string * int * Elab.kind - val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, + val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, bind : 'context * binder -> 'context} -> ('context, Elab.con, 'state, 'abort) Search.mapfolderB @@ -48,7 +55,7 @@ structure Con : sig con : (Elab.con', 'state, 'abort) Search.mapfolder} -> (Elab.con, 'state, 'abort) Search.mapfolder - val mapB : {kind : Elab.kind' -> Elab.kind', + val mapB : {kind : 'context -> Elab.kind' -> Elab.kind', con : 'context -> Elab.con' -> Elab.con', bind : 'context * binder -> 'context} -> 'context -> (Elab.con -> Elab.con) @@ -58,7 +65,7 @@ structure Con : sig val exists : {kind : Elab.kind' -> bool, con : Elab.con' -> bool} -> Elab.con -> bool - val foldB : {kind : Elab.kind' * 'state -> 'state, + val foldB : {kind : 'context * Elab.kind' * 'state -> 'state, con : 'context * Elab.con' * 'state -> 'state, bind : 'context * binder -> 'context} -> 'context -> 'state -> Elab.con -> 'state @@ -66,12 +73,13 @@ end structure Exp : sig datatype binder = - RelC of string * Elab.kind + RelK of string + | RelC of string * Elab.kind | NamedC of string * int * Elab.kind | RelE of string * Elab.con | NamedE of string * Elab.con - val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, + val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB, bind : 'context * binder -> 'context} @@ -80,7 +88,7 @@ structure Exp : sig con : (Elab.con', 'state, 'abort) Search.mapfolder, exp : (Elab.exp', 'state, 'abort) Search.mapfolder} -> (Elab.exp, 'state, 'abort) Search.mapfolder - val mapB : {kind : Elab.kind' -> Elab.kind', + val mapB : {kind : 'context -> Elab.kind' -> Elab.kind', con : 'context -> Elab.con' -> Elab.con', exp : 'context -> Elab.exp' -> Elab.exp', bind : 'context * binder -> 'context} @@ -89,7 +97,7 @@ structure Exp : sig con : Elab.con' -> bool, exp : Elab.exp' -> bool} -> Elab.exp -> bool - val foldB : {kind : Elab.kind' * 'state -> 'state, + val foldB : {kind : 'context * Elab.kind' * 'state -> 'state, con : 'context * Elab.con' * 'state -> 'state, exp : 'context * Elab.exp' * 'state -> 'state, bind : 'context * binder -> 'context} @@ -98,12 +106,13 @@ end structure Sgn : sig datatype binder = - RelC of string * Elab.kind + RelK of string + | RelC of string * Elab.kind | NamedC of string * int * Elab.kind | Str of string * Elab.sgn | Sgn of string * Elab.sgn - val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, + val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB, sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB, @@ -127,14 +136,15 @@ end structure Decl : sig datatype binder = - RelC of string * Elab.kind + RelK of string + | RelC 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 | Sgn of string * Elab.sgn - val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, + val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB, sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB, @@ -168,7 +178,7 @@ structure Decl : sig decl : Elab.decl' -> 'a option} -> Elab.decl -> 'a option - val foldMapB : {kind : Elab.kind' * 'state -> Elab.kind' * 'state, + val foldMapB : {kind : 'context * Elab.kind' * 'state -> Elab.kind' * 'state, con : 'context * Elab.con' * 'state -> Elab.con' * 'state, exp : 'context * Elab.exp' * 'state -> Elab.exp' * 'state, sgn_item : 'context * Elab.sgn_item' * 'state -> Elab.sgn_item' * 'state, diff --git a/src/elab_util.sml b/src/elab_util.sml index f052a06d..be1c9459 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -43,44 +43,60 @@ structure S = Search structure Kind = struct -fun mapfold f = +fun mapfoldB {kind, bind} = let - fun mfk k acc = - S.bindP (mfk' k acc, f) + fun mfk ctx k acc = + S.bindP (mfk' ctx k acc, kind ctx) - and mfk' (kAll as (k, loc)) = + and mfk' ctx (kAll as (k, loc)) = case k of KType => S.return2 kAll | KArrow (k1, k2) => - S.bind2 (mfk k1, + S.bind2 (mfk ctx k1, fn k1' => - S.map2 (mfk k2, + S.map2 (mfk ctx k2, fn k2' => (KArrow (k1', k2'), loc))) | KName => S.return2 kAll | KRecord k => - S.map2 (mfk k, + S.map2 (mfk ctx k, fn k' => (KRecord k', loc)) | KUnit => S.return2 kAll | KTuple ks => - S.map2 (ListUtil.mapfold mfk ks, + S.map2 (ListUtil.mapfold (mfk ctx) ks, fn ks' => (KTuple ks', loc)) | KError => S.return2 kAll - | KUnif (_, _, ref (SOME k)) => mfk' k + | KUnif (_, _, ref (SOME k)) => mfk' ctx k | KUnif _ => S.return2 kAll + + | KRel _ => S.return2 kAll + | KFun (x, k) => + S.map2 (mfk (bind (ctx, x)) k, + fn k' => + (KFun (x, k'), loc)) in mfk end +fun mapfold fk = + mapfoldB {kind = fn () => fk, + bind = fn ((), _) => ()} () + +fun mapB {kind, bind} ctx k = + case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()), + bind = bind} ctx k () of + S.Continue (k, ()) => k + | S.Return _ => raise Fail "ElabUtil.Kind.mapB: Impossible" + fun exists f k = case mapfold (fn k => fn () => if f k then @@ -95,12 +111,13 @@ end structure Con = struct datatype binder = - Rel of string * Elab.kind - | Named of string * int * Elab.kind + RelK of string + | RelC of string * Elab.kind + | NamedC of string * int * Elab.kind fun mapfoldB {kind = fk, con = fc, bind} = let - val mfk = Kind.mapfold fk + val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, s) => bind (ctx, RelK s)} fun mfc ctx c acc = S.bindP (mfc' ctx c acc, fc ctx) @@ -114,9 +131,9 @@ fun mapfoldB {kind = fk, con = fc, bind} = fn c2' => (TFun (c1', c2'), loc))) | TCFun (e, x, k, c) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => - S.map2 (mfc (bind (ctx, Rel (x, k))) c, + S.map2 (mfc (bind (ctx, RelC (x, k))) c, fn c' => (TCFun (e, x, k', c'), loc))) | CDisjoint (ai, c1, c2, c3) => @@ -142,16 +159,16 @@ fun mapfoldB {kind = fk, con = fc, bind} = fn c2' => (CApp (c1', c2'), loc))) | CAbs (x, k, c) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => - S.map2 (mfc (bind (ctx, Rel (x, k))) c, + S.map2 (mfc (bind (ctx, RelC (x, k))) c, fn c' => (CAbs (x, k', c'), loc))) | CName _ => S.return2 cAll | CRecord (k, xcs) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => S.map2 (ListUtil.mapfold (fn (x, c) => S.bind2 (mfc ctx x, @@ -169,9 +186,9 @@ fun mapfoldB {kind = fk, con = fc, bind} = fn c2' => (CConcat (c1', c2'), loc))) | CMap (k1, k2) => - S.bind2 (mfk k1, + S.bind2 (mfk ctx k1, fn k1' => - S.map2 (mfk k2, + S.map2 (mfk ctx k2, fn k2' => (CMap (k1', k2'), loc))) @@ -190,17 +207,32 @@ fun mapfoldB {kind = fk, con = fc, bind} = | CError => S.return2 cAll | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c | CUnif _ => S.return2 cAll + + | CKAbs (x, c) => + S.map2 (mfc (bind (ctx, RelK x)) c, + fn c' => + (CKAbs (x, c'), loc)) + | CKApp (c, k) => + S.bind2 (mfc ctx c, + fn c' => + S.map2 (mfk ctx k, + fn k' => + (CKApp (c', k'), loc))) + | TKFun (x, c) => + S.map2 (mfc (bind (ctx, RelK x)) c, + fn c' => + (TKFun (x, c'), loc)) in mfc end fun mapfold {kind = fk, con = fc} = - mapfoldB {kind = fk, + mapfoldB {kind = fn () => fk, con = fn () => fc, bind = fn ((), _) => ()} () fun mapB {kind, con, bind} ctx c = - case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), + case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()), con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), bind = bind} ctx c () of S.Continue (c, ()) => c @@ -227,7 +259,7 @@ fun exists {kind, con} k = | S.Continue _ => false fun foldB {kind, con, bind} ctx st c = - case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)), + case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)), con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)), bind = bind} ctx c st of S.Continue (_, st) => st @@ -238,20 +270,22 @@ end structure Exp = struct datatype binder = - RelC of string * Elab.kind + RelK of string + | RelC of string * Elab.kind | NamedC of string * int * Elab.kind | RelE of string * Elab.con | NamedE of string * Elab.con fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = let - val mfk = Kind.mapfold fk + val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)} fun bind' (ctx, b) = let val b' = case b of - Con.Rel x => RelC x - | Con.Named x => NamedC x + Con.RelK x => RelK x + | Con.RelC x => RelC x + | Con.NamedC x => NamedC x in bind (ctx, b') end @@ -288,7 +322,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = fn c' => (ECApp (e', c'), loc))) | ECAbs (expl, x, k, e) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => S.map2 (mfe (bind (ctx, RelC (x, k))) e, fn e' => @@ -347,11 +381,6 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = fn rest' => (ECutMulti (e', c', {rest = rest'}), loc)))) - | EFold k => - S.map2 (mfk k, - fn k' => - (EFold k', loc)) - | ECase (e, pes, {disc, result}) => S.bind2 (mfe ctx e, fn e' => @@ -406,6 +435,17 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = (ELet (des', e'), loc))) end + | EKAbs (x, e) => + S.map2 (mfe (bind (ctx, RelK x)) e, + fn e' => + (EKAbs (x, e'), loc)) + | EKApp (e, k) => + S.bind2 (mfe ctx e, + fn e' => + S.map2 (mfk ctx k, + fn k' => + (EKApp (e', k'), loc))) + and mfed ctx (dAll as (d, loc)) = case d of EDVal vi => @@ -432,7 +472,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = end fun mapfold {kind = fk, con = fc, exp = fe} = - mapfoldB {kind = fk, + mapfoldB {kind = fn () => fk, con = fn () => fc, exp = fn () => fe, bind = fn ((), _) => ()} () @@ -457,7 +497,7 @@ fun exists {kind, con, exp} k = | S.Continue _ => false fun mapB {kind, con, exp, bind} ctx e = - case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), + case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()), con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()), bind = bind} ctx e () of @@ -465,7 +505,7 @@ fun mapB {kind, con, exp, bind} ctx e = | S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible" fun foldB {kind, con, exp, bind} ctx st e = - case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)), + case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)), con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)), exp = fn ctx => fn e => fn st => S.Continue (e, exp (ctx, e, st)), bind = bind} ctx e st of @@ -477,7 +517,8 @@ end structure Sgn = struct datatype binder = - RelC of string * Elab.kind + RelK of string + | RelC of string * Elab.kind | NamedC of string * int * Elab.kind | Str of string * Elab.sgn | Sgn of string * Elab.sgn @@ -487,14 +528,15 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = fun bind' (ctx, b) = let val b' = case b of - Con.Rel x => RelC x - | Con.Named x => NamedC x + Con.RelK x => RelK x + | Con.RelC x => RelC x + | Con.NamedC x => NamedC x in bind (ctx, b') end val con = Con.mapfoldB {kind = kind, con = con, bind = bind'} - val kind = Kind.mapfold kind + val kind = Kind.mapfoldB {kind = kind, bind = fn (ctx, x) => bind (ctx, RelK x)} fun sgi ctx si acc = S.bindP (sgi' ctx si acc, sgn_item ctx) @@ -502,11 +544,11 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = and sgi' ctx (siAll as (si, loc)) = case si of SgiConAbs (x, n, k) => - S.map2 (kind k, + S.map2 (kind ctx k, fn k' => (SgiConAbs (x, n, k'), loc)) | SgiCon (x, n, k, c) => - S.bind2 (kind k, + S.bind2 (kind ctx k, fn k' => S.map2 (con ctx c, fn c' => @@ -548,11 +590,11 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = fn c2' => (SgiConstraint (c1', c2'), loc))) | SgiClassAbs (x, n, k) => - S.map2 (kind k, + S.map2 (kind ctx k, fn k' => (SgiClassAbs (x, n, k'), loc)) | SgiClass (x, n, k, c) => - S.bind2 (kind k, + S.bind2 (kind ctx k, fn k' => S.map2 (con ctx c, fn c' => @@ -608,7 +650,7 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = end fun mapfold {kind, con, sgn_item, sgn} = - mapfoldB {kind = kind, + mapfoldB {kind = fn () => kind, con = fn () => con, sgn_item = fn () => sgn_item, sgn = fn () => sgn, @@ -627,7 +669,8 @@ end structure Decl = struct datatype binder = - RelC of string * Elab.kind + RelK of string + | RelC of string * Elab.kind | NamedC of string * int * Elab.kind | RelE of string * Elab.con | NamedE of string * Elab.con @@ -636,13 +679,14 @@ datatype binder = fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} = let - val mfk = Kind.mapfold fk + val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)} fun bind' (ctx, b) = let val b' = case b of - Con.Rel x => RelC x - | Con.Named x => NamedC x + Con.RelK x => RelK x + | Con.RelC x => RelC x + | Con.NamedC x => NamedC x in bind (ctx, b') end @@ -651,7 +695,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f fun bind' (ctx, b) = let val b' = case b of - Exp.RelC x => RelC x + Exp.RelK x => RelK x + | Exp.RelC x => RelC x | Exp.NamedC x => NamedC x | Exp.RelE x => RelE x | Exp.NamedE x => NamedE x @@ -663,7 +708,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f fun bind' (ctx, b) = let val b' = case b of - Sgn.RelC x => RelC x + Sgn.RelK x => RelK x + | Sgn.RelC x => RelC x | Sgn.NamedC x => NamedC x | Sgn.Sgn x => Sgn x | Sgn.Str x => Str x @@ -760,7 +806,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f and mfd' ctx (dAll as (d, loc)) = case d of DCon (x, n, k, c) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => S.map2 (mfc ctx c, fn c' => @@ -825,7 +871,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f | DSequence _ => S.return2 dAll | DClass (x, n, k, c) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => S.map2 (mfc ctx c, fn c' => @@ -849,7 +895,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f end fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} = - mapfoldB {kind = kind, + mapfoldB {kind = fn () => kind, con = fn () => con, exp = fn () => exp, sgn_item = fn () => sgn_item, @@ -938,7 +984,7 @@ fun search {kind, con, exp, sgn_item, sgn, str, decl} k = | S.Continue _ => NONE fun foldMapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx st d = - case mapfoldB {kind = fn x => fn st => S.Continue (kind (x, st)), + case mapfoldB {kind = fn ctx => fn x => fn st => S.Continue (kind (ctx, x, st)), con = fn ctx => fn x => fn st => S.Continue (con (ctx, x, st)), exp = fn ctx => fn x => fn st => S.Continue (exp (ctx, x, st)), sgn_item = fn ctx => fn x => fn st => S.Continue (sgn_item (ctx, x, st)), diff --git a/src/elaborate.sml b/src/elaborate.sml index 0c335603..54543ae9 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -61,7 +61,7 @@ exception KUnify' of kunify_error - fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) = + fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) = let fun err f = raise KUnify' (f (k1All, k2All)) in @@ -70,19 +70,27 @@ | (L'.KUnit, L'.KUnit) => () | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) => - (unifyKinds' d1 d2; - unifyKinds' r1 r2) + (unifyKinds' env d1 d2; + unifyKinds' env r1 r2) | (L'.KName, L'.KName) => () - | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2 + | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' env k1 k2 | (L'.KTuple ks1, L'.KTuple ks2) => - ((ListPair.appEq (fn (k1, k2) => unifyKinds' k1 k2) (ks1, ks2)) + ((ListPair.appEq (fn (k1, k2) => unifyKinds' env k1 k2) (ks1, ks2)) handle ListPair.UnequalLengths => err KIncompatible) + | (L'.KRel n1, L'.KRel n2) => + if n1 = n2 then + () + else + err KIncompatible + | (L'.KFun (x, k1), L'.KFun (_, k2)) => + unifyKinds' (E.pushKRel env x) 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' env k1All k2All + | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' env k1All k2All | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) => if r1 = r2 then @@ -106,12 +114,12 @@ exception KUnify of L'.kind * L'.kind * kunify_error - fun unifyKinds k1 k2 = - unifyKinds' k1 k2 + fun unifyKinds env k1 k2 = + unifyKinds' env k1 k2 handle KUnify' err => raise KUnify (k1, k2, err) fun checkKind env c k1 k2 = - unifyKinds k1 k2 + unifyKinds env k1 k2 handle KUnify (k1, k2, err) => conError env (WrongKind (c, k1, k2, err)) @@ -172,16 +180,23 @@ end - fun elabKind (k, loc) = + fun elabKind env (k, loc) = case k of L.KType => (L'.KType, loc) - | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc) + | L.KArrow (k1, k2) => (L'.KArrow (elabKind env k1, elabKind env k2), loc) | L.KName => (L'.KName, loc) - | L.KRecord k => (L'.KRecord (elabKind k), loc) + | L.KRecord k => (L'.KRecord (elabKind env k), loc) | L.KUnit => (L'.KUnit, loc) - | L.KTuple ks => (L'.KTuple (map elabKind ks), loc) + | L.KTuple ks => (L'.KTuple (map (elabKind env) ks), loc) | L.KWild => kunif loc + | L.KVar s => (case E.lookupK env s of + NONE => + (kindError env (UnboundKind (loc, s)); + kerror) + | SOME n => (L'.KRel n, loc)) + | L.KFun (x, k) => (L'.KFun (x, elabKind (E.pushKRel env x) k), loc) + fun mapKind (dom, ran, loc)= (L'.KArrow ((L'.KArrow (dom, ran), loc), (L'.KArrow ((L'.KRecord dom, loc), @@ -192,11 +207,31 @@ L'.KUnif (_, _, ref (SOME k)) => hnormKind k | _ => kAll + open ElabOps + val hnormCon = D.hnormCon + + fun elabConHead (c as (_, loc)) k = + let + fun unravel (k, c) = + case hnormKind k of + (L'.KFun (x, k'), _) => + let + val u = kunif loc + + val k'' = subKindInKind (0, u) k' + in + unravel (k'', (L'.CKApp (c, u), loc)) + end + | _ => (c, k) + in + unravel (k, c) + end + fun elabCon (env, denv) (c, loc) = case c of L.CAnnot (c, k) => let - val k' = elabKind k + val k' = elabKind env k val (c', ck, gs) = elabCon (env, denv) c in checkKind env c' ck k'; @@ -215,13 +250,21 @@ | L.TCFun (e, x, k, t) => let val e' = elabExplicitness e - val k' = elabKind k + val k' = elabKind env k val env' = E.pushCRel env x k' val (t', tk, gs) = elabCon (env', D.enter denv) t in checkKind env t' tk ktype; ((L'.TCFun (e', x, k', t'), loc), ktype, gs) end + | L.TKFun (x, t) => + let + val env' = E.pushKRel env x + val (t', tk, gs) = elabCon (env', denv) t + in + checkKind env t' tk ktype; + ((L'.TKFun (x, t'), loc), ktype, gs) + end | L.CDisjoint (c1, c2, c) => let val (c1', k1, gs1) = elabCon (env, denv) c1 @@ -253,9 +296,17 @@ (conError env (UnboundCon (loc, s)); (cerror, kerror, [])) | E.Rel (n, k) => - ((L'.CRel n, loc), k, []) + let + val (c, k) = elabConHead (L'.CRel n, loc) k + in + (c, k, []) + end | E.Named (n, k) => - ((L'.CNamed n, loc), k, [])) + let + val (c, k) = elabConHead (L'.CNamed n, loc) k + in + (c, k, []) + end) | L.CVar (m1 :: ms, s) => (case E.lookupStr env m1 of NONE => (conError env (UnboundStrInCon (loc, m1)); @@ -292,7 +343,7 @@ let val k' = case ko of NONE => kunif loc - | SOME k => elabKind k + | SOME k => elabKind env k val env' = E.pushCRel env x k' val (t', tk, gs) = elabCon (env', D.enter denv) t in @@ -300,6 +351,15 @@ (L'.KArrow (k', tk), loc), gs) end + | L.CKAbs (x, t) => + let + val env' = E.pushKRel env x + val (t', tk, gs) = elabCon (env', denv) t + in + ((L'.CKAbs (x, t'), loc), + (L'.KFun (x, tk), loc), + gs) + end | L.CName s => ((L'.CName s, loc), kname, []) @@ -392,7 +452,7 @@ | L.CWild k => let - val k' = elabKind k + val k' = elabKind env k in (cunif (loc, k'), k', []) end @@ -431,8 +491,6 @@ exception SynUnif = E.SynUnif - open ElabOps - type record_summary = { fields : (L'.con * L'.con) list, unifs : (L'.con * L'.con option ref) list, @@ -499,7 +557,12 @@ | L'.CError => kerror | L'.CUnif (_, k, _, _) => k - val hnormCon = D.hnormCon + | L'.CKAbs (x, c) => (L'.KFun (x, kindof (E.pushKRel env x) c), loc) + | L'.CKApp (c, k) => + (case hnormKind (kindof env c) of + (L'.KFun (_, k'), _) => subKindInKind (0, k) k' + | k => raise CUnify' (CKindof (k, c, "kapp"))) + | L'.TKFun _ => ktype fun deConstraintCon (env, denv) c = let @@ -564,6 +627,10 @@ | L'.CError => false | L'.CUnif (_, k, _, _) => #1 k = L'.KUnit + | L'.CKAbs _ => false + | L'.CKApp _ => false + | L'.TKFun _ => false + fun unifyRecordCons (env, denv) (c1, c2) = let fun rkindof c = @@ -578,7 +645,7 @@ val (r1, gs1) = recordSummary (env, denv) c1 val (r2, gs2) = recordSummary (env, denv) c2 in - unifyKinds k1 k2; + unifyKinds env k1 k2; unifySummaries (env, denv) (k1, r1, r2); gs1 @ gs2 end @@ -848,12 +915,13 @@ val (c2, gs2) = hnormCon (env, denv) c2 in let + (*val () = prefaces "unifyCons'" [("old1", p_con env old1), + ("old2", p_con env old2), + ("c1", p_con env c1), + ("c2", p_con env c2)]*) + val gs3 = unifyCons'' (env, denv) c1 c2 in - (*prefaces "unifyCons'" [("c1", p_con env old1), - ("c2", p_con env old2), - ("t", PD.string (LargeReal.toString (Time.toReal - (Time.- (Time.now (), befor)))))];*) gs1 @ gs2 @ gs3 end handle ex => guessMap (env, denv) (c1, c2, gs1 @ gs2, ex) @@ -878,7 +946,7 @@ if expl1 <> expl2 then err CExplicitness else - (unifyKinds d1 d2; + (unifyKinds env d1 d2; let val denv' = D.enter denv (*val befor = Time.now ()*) @@ -906,7 +974,7 @@ (unifyCons' (env, denv) d1 d2; unifyCons' (env, denv) r1 r2) | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) => - (unifyKinds k1 k2; + (unifyKinds env k1 k2; unifyCons' (E.pushCRel env x1 k1, D.enter denv) c1 c2) | (L'.CName n1, L'.CName n2) => @@ -954,6 +1022,19 @@ else err CIncompatible + | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) => + (unifyKinds env dom1 dom2; + unifyKinds env ran1 ran2; + []) + + | (L'.CKAbs (x, c1), L'.CKAbs (_, c2)) => + unifyCons' (E.pushKRel env x, denv) c1 c2 + | (L'.CKApp (c1, k1), L'.CKApp (c2, k2)) => + (unifyKinds env k1 k2; + unifyCons' (env, denv) c1 c2) + | (L'.TKFun (x, c1), L'.TKFun (_, c2)) => + unifyCons' (E.pushKRel env x, denv) c1 c2 + | (L'.CError, _) => [] | (_, L'.CError) => [] @@ -966,7 +1047,7 @@ if r1 = r2 then [] else - (unifyKinds k1 k2; + (unifyKinds env k1 k2; r1 := SOME c2All; []) @@ -983,11 +1064,6 @@ (r := SOME c1All; []) - | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) => - (unifyKinds dom1 dom2; - unifyKinds ran1 ran2; - []) - | _ => err CIncompatible end @@ -1013,36 +1089,7 @@ P.Int _ => !int | P.Float _ => !float | P.String _ => !string - - fun recCons (k, nm, v, rest, loc) = - (L'.CConcat ((L'.CRecord (k, [(nm, v)]), loc), - rest), loc) - - fun foldType (dom, loc) = - (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc), - (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc), - (L'.TCFun (L'.Explicit, "v", dom, - (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc), - (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc), - (L'.CDisjoint (L'.Instantiate, - (L'.CRecord - ((L'.KUnit, loc), - [((L'.CRel 2, loc), - (L'.CUnit, loc))]), loc), - (L'.CRel 0, loc), - (L'.CApp ((L'.CRel 3, loc), - recCons (dom, - (L'.CRel 2, loc), - (L'.CRel 1, loc), - (L'.CRel 0, loc), - loc)), loc)), - loc)), loc)), - loc)), loc)), loc), - (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc), - (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc), - (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)), - loc)), loc)), loc) - + datatype constraint = Disjoint of D.goal | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span @@ -1056,7 +1103,16 @@ val (t, gs) = hnormCon (env, denv) t in case t of - (L'.TCFun (L'.Implicit, x, k, t'), _) => + (L'.TKFun (x, t'), _) => + let + val u = kunif loc + + val t'' = subKindInCon (0, u) t' + val (e, t, gs') = unravel (t'', (L'.EKApp (e, u), loc)) + in + (e, t, enD gs @ gs') + end + | (L'.TCFun (L'.Implicit, x, k, t'), _) => let val u = cunif (loc, k) @@ -1575,7 +1631,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) = | L.ECAbs (expl, x, k, e) => let val expl' = elabExplicitness expl - val k' = elabKind k + val k' = elabKind env k val env' = E.pushCRel env x k' val (e', et, gs) = elabExp (env', D.enter denv) e @@ -1584,6 +1640,15 @@ fun elabExp (env, denv) (eAll as (e, loc)) = (L'.TCFun (expl', x, k', et), loc), gs) end + | L.EKAbs (x, e) => + let + val env' = E.pushKRel env x + val (e', et, gs) = elabExp (env', denv) e + in + ((L'.EKAbs (x, e'), loc), + (L'.TKFun (x, et), loc), + gs) + end | L.EDisjoint (c1, c2, e) => let @@ -1710,13 +1775,6 @@ fun elabExp (env, denv) (eAll as (e, loc)) = gs1 @ enD gs2 @ enD gs3 @ enD gs4) end - | L.EFold => - let - val dom = kunif loc - in - ((L'.EFold dom, loc), foldType (dom, loc), []) - end - | L.ECase (e, pes) => let val (e', et, gs1) = elabExp (env, denv) e @@ -1781,6 +1839,7 @@ and elabEdecl denv (dAll as (d, loc), (env, gs : constraint list)) = case e of L.EAbs _ => true | L.ECAbs (_, _, _, e) => allowable e + | L.EKAbs (_, e) => allowable e | L.EDisjoint (_, _, e) => allowable e | _ => false @@ -1859,7 +1918,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = case sgi of L.SgiConAbs (x, k) => let - val k' = elabKind k + val k' = elabKind env k val (env', n) = E.pushCNamed env x k' NONE in @@ -1870,7 +1929,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = let val k' = case ko of NONE => kunif loc - | SOME k => elabKind k + | SOME k => elabKind env k val (c', ck, gs') = elabCon (env, denv) c val (env', n) = E.pushCNamed env x k' (SOME c') @@ -1979,7 +2038,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = val (env', n) = E.pushENamed env x c' val c' = normClassConstraint env c' in - (unifyKinds ck ktype + (unifyKinds env ck ktype handle KUnify ue => strError env (NotType (ck, ue))); ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) @@ -2027,7 +2086,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = | L.SgiClassAbs (x, k) => let - val k = elabKind k + val k = elabKind env k val k' = (L'.KArrow (k, (L'.KType, loc)), loc) val (env, n) = E.pushCNamed env x k' NONE val env = E.pushClass env n @@ -2037,7 +2096,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = | L.SgiClass (x, k, c) => let - val k = elabKind k + val k = elabKind env k val k' = (L'.KArrow (k, (L'.KType, loc)), loc) val (c', ck, gs) = elabCon (env, denv) c val (env, n) = E.pushCNamed env x k' (SOME c') @@ -2149,7 +2208,7 @@ and elabSgn (env, denv) (sgn, loc) = | L'.SgnConst sgis => if List.exists (fn (L'.SgiConAbs (x', _, k), _) => x' = x andalso - (unifyKinds k ck + (unifyKinds env k ck handle KUnify x => sgnError env (WhereWrongKind x); true) | _ => false) sgis then @@ -2355,7 +2414,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = fun found (x', n1, k1, co1) = if x = x' then let - val () = unifyKinds k1 k2 + val () = unifyKinds env k1 k2 handle KUnify (k1, k2, err) => sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) val env = E.pushCNamedAs env x n1 k1 co1 @@ -2606,7 +2665,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = fun found (x', n1, k1, co) = if x = x' then let - val () = unifyKinds k1 k2 + val () = unifyKinds env k1 k2 handle KUnify (k1, k2, err) => sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) @@ -2635,7 +2694,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = fun found (x', n1, k1, c1) = if x = x' then let - val () = unifyKinds k1 k2 + val () = unifyKinds env k1 k2 handle KUnify (k1, k2, err) => sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) @@ -2702,6 +2761,9 @@ fun positive self = | CAbs _ => false | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 + | CKAbs _ => false + | TKFun _ => false + | CName _ => true | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs @@ -2728,6 +2790,9 @@ fun positive self = | CAbs _ => false | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 + | CKAbs _ => false + | TKFun _ => false + | CName _ => true | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs @@ -2777,6 +2842,9 @@ fun wildifyStr env (str, sgn) = | L'.KUnif (_, _, ref (SOME k)) => decompileKind k | L'.KUnif _ => NONE + | L'.KRel _ => NONE + | L'.KFun _ => NONE + fun decompileCon env (c, loc) = case c of L'.CRel i => @@ -2914,7 +2982,7 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = let val k' = case ko of NONE => kunif loc - | SOME k => elabKind k + | SOME k => elabKind env k val (c', ck, gs') = elabCon (env, denv) c val (env', n) = E.pushCNamed env x k' (SOME c') @@ -3047,6 +3115,7 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = case e of L.EAbs _ => true | L.ECAbs (_, _, _, e) => allowable e + | L.EKAbs (_, e) => allowable e | L.EDisjoint (_, _, e) => allowable e | _ => false @@ -3264,7 +3333,7 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = | L.DClass (x, k, c) => let - val k = elabKind k + val k = elabKind env k val k' = (L'.KArrow (k, (L'.KType, loc)), loc) val (c', ck, gs') = elabCon (env, denv) c val (env, n) = E.pushCNamed env x k' (SOME c') diff --git a/src/expl.sml b/src/expl.sml index c0d291b5..0101dd1f 100644 --- a/src/expl.sml +++ b/src/expl.sml @@ -93,7 +93,6 @@ datatype exp' = | EConcat of exp * con * exp * con | ECut of exp * con * { field : con, rest : con } | ECutMulti of exp * con * { rest : con } - | EFold of kind | ECase of exp * (pat * exp) list * { disc : con, result : con } diff --git a/src/expl_print.sml b/src/expl_print.sml index 7044bfa2..313fef5c 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -351,7 +351,6 @@ fun p_exp' par env (e, loc) = string "---", space, p_con' true env c]) - | EFold _ => string "fold" | EWrite e => box [string "write(", p_exp env e, diff --git a/src/expl_util.sml b/src/expl_util.sml index a2b5f2f6..febf3586 100644 --- a/src/expl_util.sml +++ b/src/expl_util.sml @@ -311,10 +311,6 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = S.map2 (mfc ctx rest, fn rest' => (ECutMulti (e', c', {rest = rest'}), loc)))) - | EFold k => - S.map2 (mfk k, - fn k' => - (EFold k', loc)) | EWrite e => S.map2 (mfe ctx e, diff --git a/src/explify.sml b/src/explify.sml index a4eab0ba..5bce9268 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -107,8 +107,6 @@ fun explifyExp (e, loc) = {field = explifyCon field, rest = explifyCon rest}), loc) | L.ECutMulti (e1, c, {rest}) => (L'.ECutMulti (explifyExp e1, explifyCon c, {rest = explifyCon rest}), loc) - | L.EFold k => (L'.EFold (explifyKind k), loc) - | L.ECase (e, pes, {disc, result}) => (L'.ECase (explifyExp e, map (fn (p, e) => (explifyPat p, explifyExp e)) pes, diff --git a/src/monoize.sml b/src/monoize.sml index 898d3e61..96ef2c6a 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -2183,7 +2183,6 @@ fun monoExp (env, st, fm) (all as (e, loc)) = | L.EConcat _ => poly () | L.ECut _ => poly () | L.ECutMulti _ => poly () - | L.EFold _ => poly () | L.ECase (e, pes, {disc, result}) => let diff --git a/src/reduce.sml b/src/reduce.sml index 949b2a6d..77718b66 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -214,20 +214,6 @@ fun conAndExp (namedC, namedE) = in case #1 e of ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b - - | EApp ((EApp ((ECApp ((EFold _, _), _), _), f), _), i) => - (case #1 c of - CRecord (_, []) => i - | CRecord (k, (nm, v) :: rest) => - let - val rest = (CRecord (k, rest), loc) - in - exp (deKnown env) - (EApp ((ECApp ((ECApp ((ECApp (f, nm), loc), v), loc), rest), loc), - (ECApp (e, rest), loc)), loc) - end - | _ => (ECApp (e, c), loc)) - | _ => (ECApp (e, c), loc) end @@ -334,8 +320,6 @@ fun conAndExp (namedC, namedE) = | _ => default () end - | EFold _ => all - | ECase (e, pes, {disc, result}) => let fun patBinds (p, _) = diff --git a/src/reduce_local.sml b/src/reduce_local.sml index 7de7d799..25b1023a 100644 --- a/src/reduce_local.sml +++ b/src/reduce_local.sml @@ -107,8 +107,6 @@ fun exp env (all as (e, loc)) = | ECut (e, c, others) => (ECut (exp env e, c, others), loc) | ECutMulti (e, c, others) => (ECutMulti (exp env e, c, others), loc) - | EFold _ => all - | ECase (e, pes, others) => let fun patBinds (p, _) = diff --git a/src/source.sml b/src/source.sml index d70d0f5d..e9531245 100644 --- a/src/source.sml +++ b/src/source.sml @@ -38,6 +38,9 @@ datatype kind' = | KTuple of kind list | KWild + | KFun of string * kind + | KVar of string + withtype kind = kind' located datatype explicitness = @@ -56,6 +59,9 @@ datatype con' = | CAbs of string * kind option * con | CDisjoint of con * con * con + | CKAbs of string * con + | TKFun of string * con + | CName of string | CRecord of (con * con) list @@ -119,12 +125,13 @@ datatype exp' = | ECAbs of explicitness * string * kind * exp | EDisjoint of con * con * exp + | EKAbs of string * exp + | ERecord of (con * exp) list | EField of exp * con | EConcat of exp * exp | ECut of exp * con | ECutMulti of exp * con - | EFold | EWild diff --git a/src/source_print.sml b/src/source_print.sml index 148157c2..f2420947 100644 --- a/src/source_print.sml +++ b/src/source_print.sml @@ -50,6 +50,13 @@ fun p_kind' par (k, _) = p_list_sep (box [space, string "*", space]) p_kind ks, string ")"] + | KVar x => string x + | KFun (x, k) => box [string x, + space, + string "-->", + space, + p_kind k] + and p_kind k = p_kind' false k fun p_explicitness e = @@ -156,6 +163,17 @@ fun p_con' par (c, _) = | CProj (c, n) => box [p_con c, string ".", string (Int.toString n)] + + | CKAbs (x, c) => box [string x, + space, + string "==>", + space, + p_con c] + | TKFun (x, c) => box [string x, + space, + string "-->", + space, + p_con c] and p_con c = p_con' false c @@ -273,8 +291,6 @@ fun p_exp' par (e, _) = string "---", space, p_con' true c]) - | EFold => string "fold" - | ECase (e, pes) => parenIf par (box [string "case", space, p_exp e, @@ -300,6 +316,12 @@ fun p_exp' par (e, _) = newline, string "end"] + | EKAbs (x, e) => box [string x, + space, + string "-->", + space, + p_exp e] + and p_exp e = p_exp' false e and p_edecl (d, _) = diff --git a/src/termination.sml b/src/termination.sml index e89f329e..5dd95f46 100644 --- a/src/termination.sml +++ b/src/termination.sml @@ -190,6 +190,7 @@ fun declOk' env (d, loc) = in (p, ps, calls) end + | EKApp (e, _) => combiner calls e | _ => let val (p, calls) = exp parent (penv, calls) e @@ -239,6 +240,13 @@ fun declOk' env (d, loc) = in (Rabble, calls) end + | EKApp _ => apps () + | EKAbs (_, e) => + let + val (_, calls) = exp parent (penv, calls) e + in + (Rabble, calls) + end | ERecord xets => let @@ -278,7 +286,6 @@ fun declOk' env (d, loc) = in (Rabble, calls) end - | EFold _ => (Rabble, calls) | ECase (e, pes, _) => let diff --git a/src/unnest.sml b/src/unnest.sml index 8e363301..1d0c2388 100644 --- a/src/unnest.sml +++ b/src/unnest.sml @@ -37,7 +37,7 @@ structure U = ElabUtil structure IS = IntBinarySet fun liftExpInExp by = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn _ => fn c => c, exp = fn bound => fn e => case e of @@ -51,7 +51,7 @@ fun liftExpInExp by = | (bound, _) => bound} val subExpInExp = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn _ => fn c => c, exp = fn (xn, rep) => fn e => case e of @@ -65,7 +65,7 @@ val subExpInExp = | ((xn, rep), U.Exp.RelC _) => (xn, E.liftConInExp 0 rep) | (ctx, _) => ctx} -val fvsCon = U.Con.foldB {kind = fn (_, st) => st, +val fvsCon = U.Con.foldB {kind = fn (_, _, st) => st, con = fn (cb, c, cvs) => case c of CRel n => @@ -76,11 +76,11 @@ val fvsCon = U.Con.foldB {kind = fn (_, st) => st, | _ => cvs, bind = fn (cb, b) => case b of - U.Con.Rel _ => cb + 1 + U.Con.RelC _ => cb + 1 | _ => cb} 0 IS.empty -fun fvsExp nr = U.Exp.foldB {kind = fn (_, st) => st, +fun fvsExp nr = U.Exp.foldB {kind = fn (_, _, st) => st, con = fn ((cb, eb), c, st as (cvs, evs)) => case c of CRel n => @@ -124,7 +124,7 @@ fun positionOf (x : int) ls = end fun squishCon cfv = - U.Con.mapB {kind = fn k => k, + U.Con.mapB {kind = fn _ => fn k => k, con = fn cb => fn c => case c of CRel n => @@ -135,12 +135,12 @@ fun squishCon cfv = | _ => c, bind = fn (cb, b) => case b of - U.Con.Rel _ => cb + 1 + U.Con.RelC _ => cb + 1 | _ => cb} 0 fun squishExp (nr, cfv, efv) = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn (cb, eb) => fn c => case c of CRel n => @@ -169,7 +169,7 @@ type state = { decls : (string * int * con * exp) list } -fun kind (k, st) = (k, st) +fun kind (_, k, st) = (k, st) fun exp ((ks, ts), e as old, st : state) = case e of diff --git a/src/urweb.grm b/src/urweb.grm index d425caec..b6e4ce72 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -184,10 +184,10 @@ fun tagIn bt = | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR | PLUS | MINUS | DIVIDE | DOTDOTDOT | MOD | AT - | CON | LTYPE | VAL | REC | AND | FUN | MAP | FOLD | UNIT | KUNIT | CLASS + | CON | LTYPE | VAL | REC | AND | FUN | MAP | UNIT | KUNIT | CLASS | DATATYPE | OF | TYPE | NAME - | ARROW | LARROW | DARROW | STAR | SEMI + | ARROW | LARROW | DARROW | STAR | SEMI | KARROW | DKARROW | FN | PLUSPLUS | MINUSMINUS | MINUSMINUSMINUS | DOLLAR | TWIDDLE | LET | IN | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | SQL @@ -327,6 +327,8 @@ fun tagIn bt = %name Urweb +%right KARROW +%nonassoc DKARROW %right SEMI %nonassoc LARROW %nonassoc IF THEN ELSE @@ -575,6 +577,8 @@ kind : TYPE (KType, s (TYPEleft, TYPEright)) | KUNIT (KUnit, s (KUNITleft, KUNITright)) | UNDERUNDER (KWild, s (UNDERUNDERleft, UNDERUNDERright)) | LPAREN ktuple RPAREN (KTuple ktuple, s (LPARENleft, RPARENright)) + | CSYMBOL (KVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) + | CSYMBOL KARROW kind (KFun (CSYMBOL, kind), s (CSYMBOLleft, kindright)) ktuple : kind STAR kind ([kind1, kind2]) | kind STAR ktuple (kind :: ktuple) @@ -585,10 +589,12 @@ capps : cterm (cterm) cexp : capps (capps) | cexp ARROW cexp (TFun (cexp1, cexp2), s (cexp1left, cexp2right)) | SYMBOL kcolon kind ARROW cexp (TCFun (kcolon, SYMBOL, kind, cexp), s (SYMBOLleft, cexpright)) + | CSYMBOL KARROW cexp (TKFun (CSYMBOL, cexp), s (CSYMBOLleft, cexpright)) | cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right)) | FN cargs DARROW cexp (#1 (cargs (cexp, (KWild, s (FNleft, cexpright))))) + | CSYMBOL DKARROW cexp (CKAbs (CSYMBOL, cexp), s (CSYMBOLleft, cexpright)) | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright)) @@ -651,7 +657,7 @@ cargp : SYMBOL (fn (c, k) => ((CAbs (SYMBOL, SOME kind, c), loc), (KArrow (kind, k), loc)) end) - | LBRACK cexp TWIDDLE cexp RBRACK (fn (c, k) => + | LBRACK cexp TWIDDLE cexp RBRACK (fn (c, k) => let val loc = s (LBRACKleft, RBRACKright) in @@ -716,6 +722,7 @@ eexp : eapps (eapps) in #1 (eargs (eexp, (CWild (KType, loc), loc))) end) + | CSYMBOL DKARROW eexp (EKAbs (CSYMBOL, eexp), s (CSYMBOLleft, eexpright)) | eexp COLON cexp (EAnnot (eexp, cexp), s (eexpleft, cexpright)) | eexp MINUSMINUS cexp (ECut (eexp, cexp), s (eexpleft, cexpright)) | eexp MINUSMINUSMINUS cexp (ECutMulti (eexp, cexp), s (eexpleft, cexpright)) @@ -851,6 +858,13 @@ eargp : SYMBOL (fn (e, t) => ((EDisjoint (cexp1, cexp2, e), loc), (CDisjoint (cexp1, cexp2, t), loc)) end) + | CSYMBOL (fn (e, t) => + let + val loc = s (CSYMBOLleft, CSYMBOLright) + in + ((EKAbs (CSYMBOL, e), loc), + (TKFun (CSYMBOL, t), loc)) + end) eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright)) | LPAREN etuple RPAREN (let @@ -895,7 +909,6 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright)) (EField (e, ident), loc)) (EVar (#1 path, #2 path, DontInfer), s (pathleft, pathright)) idents end) - | FOLD (EFold, s (FOLDleft, FOLDright)) | XML_BEGIN xml XML_END (let val loc = s (XML_BEGINleft, XML_ENDright) @@ -1070,7 +1083,7 @@ xmlOne : NOTAGS (EApp ((EVar (["Basis"], "cdata", Infer) () else ErrorMsg.errorAt pos "Begin and end tags don't match."; - (EFold, pos)) + (EWild, pos)) end) | LBRACE eexp RBRACE (eexp) | LBRACE LBRACK eexp RBRACK RBRACE (let diff --git a/src/urweb.lex b/src/urweb.lex index 29e07194..bb57f03d 100644 --- a/src/urweb.lex +++ b/src/urweb.lex @@ -247,7 +247,9 @@ notags = [^<{\n]+; <INITIAL> "}" => (exitBrace (); Tokens.RBRACE (pos yypos, pos yypos + size yytext)); +<INITIAL> "-->" => (Tokens.KARROW (pos yypos, pos yypos + size yytext)); <INITIAL> "->" => (Tokens.ARROW (pos yypos, pos yypos + size yytext)); +<INITIAL> "==>" => (Tokens.DKARROW (pos yypos, pos yypos + size yytext)); <INITIAL> "=>" => (Tokens.DARROW (pos yypos, pos yypos + size yytext)); <INITIAL> "++" => (Tokens.PLUSPLUS (pos yypos, pos yypos + size yytext)); <INITIAL> "--" => (Tokens.MINUSMINUS (pos yypos, pos yypos + size yytext)); @@ -291,7 +293,6 @@ notags = [^<{\n]+; <INITIAL> "fun" => (Tokens.FUN (pos yypos, pos yypos + size yytext)); <INITIAL> "fn" => (Tokens.FN (pos yypos, pos yypos + size yytext)); <INITIAL> "map" => (Tokens.MAP (pos yypos, pos yypos + size yytext)); -<INITIAL> "fold" => (Tokens.FOLD (pos yypos, pos yypos + size yytext)); <INITIAL> "case" => (Tokens.CASE (pos yypos, pos yypos + size yytext)); <INITIAL> "if" => (Tokens.IF (pos yypos, pos yypos + size yytext)); <INITIAL> "then" => (Tokens.THEN (pos yypos, pos yypos + size yytext)); |