Mercurial > urweb
changeset 623:588b9d16b00a
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 22 Feb 2009 16:10:25 -0500 |
| parents | d64533157f40 |
| children | 354800878b4d |
| files | lib/ur/top.ur lib/ur/top.urs src/core.sml src/core_print.sml src/core_util.sml src/corify.sml src/elab.sml src/elab_env.sig src/elab_env.sml src/elab_err.sig src/elab_err.sml src/elab_ops.sig src/elab_ops.sml src/elab_print.sig src/elab_print.sml src/elab_util.sig src/elab_util.sml src/elaborate.sml src/expl.sml src/expl_print.sml src/expl_util.sml src/explify.sml src/monoize.sml src/reduce.sml src/reduce_local.sml src/source.sml src/source_print.sml src/termination.sml src/unnest.sml src/urweb.grm src/urweb.lex |
| diffstat | 31 files changed, 737 insertions(+), 492 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/top.ur Sat Feb 21 16:11:56 2009 -0500 +++ b/lib/ur/top.ur Sun Feb 22 16:10:25 2009 -0500 @@ -1,3 +1,12 @@ +(** Row folding *) + +con folder = K ==> fn r :: {K} => + tf :: ({K} -> Type) + -> (nm :: Name -> v :: K -> r :: {K} -> tf r + -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) + -> tf [] -> tf r + + fun not b = if b then False else True con idT (t :: Type) = t @@ -27,23 +36,23 @@ (f : nm :: Name -> rest :: {Unit} -> fn [[nm] ~ rest] => tf -> tr rest -> tr ([nm] ++ rest)) - (i : tr []) = + (i : tr []) (r ::: {Unit}) (fold : folder r)= fold [fn r :: {Unit} => $(mapUT tf r) -> tr r] - (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc - [[nm] ~ rest] r => - f [nm] [rest] r.nm (acc (r -- nm))) - (fn _ => i) + (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc + [[nm] ~ rest] r => + f [nm] [rest] r.nm (acc (r -- nm))) + (fn _ => i) fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type) (f : nm :: Name -> rest :: {Unit} -> fn [[nm] ~ rest] => tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) - (i : tr []) = + (i : tr []) (r ::: {Unit}) (fold : folder r) = fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r] - (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc - [[nm] ~ rest] r1 r2 => - f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) - (fn _ _ => i) + (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc + [[nm] ~ rest] r1 r2 => + f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) + (fn _ _ => i) fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit}) (f : nm :: Name -> rest :: {Unit} @@ -54,134 +63,46 @@ <xml>{f [nm] [rest] v1 v2}{acc}</xml>) <xml/> -fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type) - (f : nm :: Name -> t :: Type -> rest :: {Type} +fun foldR K (tf :: K -> Type) (tr :: {K} -> Type) + (f : nm :: Name -> t :: K -> rest :: {K} -> fn [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {Type} => $(map tf r) -> tr r] - (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest) + (i : tr []) (r ::: {K}) (fold : folder r) = + fold [fn r :: {K} => $(map tf r) -> tr r] + (fn (nm :: Name) (t :: K) (rest :: {K}) (acc : _ -> tr rest) [[nm] ~ rest] r => f [nm] [t] [rest] r.nm (acc (r -- nm))) (fn _ => i) -fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type) - (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {(Type * Type)} => $(map tf r) -> tr r] - (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) - (acc : _ -> tr rest) [[nm] ~ rest] r => - f [nm] [t] [rest] r.nm (acc (r -- nm))) - (fn _ => i) - -fun foldT3R (tf :: (Type * Type * Type) -> Type) (tr :: {(Type * Type * Type)} -> Type) - (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {(Type * Type * Type)} => $(map tf r) -> tr r] - (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) - (acc : _ -> tr rest) [[nm] ~ rest] r => - f [nm] [t] [rest] r.nm (acc (r -- nm))) - (fn _ => i) - -fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type) - (f : nm :: Name -> t :: Type -> rest :: {Type} +fun foldR2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (tr :: {K} -> Type) + (f : nm :: Name -> t :: K -> rest :: {K} -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {Type} => $(map tf1 r) -> $(map tf2 r) -> tr r] - (fn (nm :: Name) (t :: Type) (rest :: {Type}) - (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => - f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) - (fn _ _ => i) + (i : tr []) (r ::: {K}) (fold : folder r) = + fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r] + (fn (nm :: Name) (t :: K) (rest :: {K}) + (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => + f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) + (fn _ _ => i) -fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) - (tr :: {(Type * Type)} -> Type) - (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {(Type * Type)} => $(map tf1 r) -> $(map tf2 r) -> tr r] - (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) - (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => - f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) - (fn _ _ => i) - -fun foldT3R2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type) - (tr :: {(Type * Type * Type)} -> Type) - (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {(Type * Type * Type)} => $(map tf1 r) -> $(map tf2 r) -> tr r] - (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) - (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => - f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) - (fn _ _ => i) - -fun foldTRX (tf :: Type -> Type) (ctx :: {Unit}) - (f : nm :: Name -> t :: Type -> rest :: {Type} +fun foldRX K (tf :: K -> Type) (ctx :: {Unit}) + (f : nm :: Name -> t :: K -> rest :: {K} -> fn [[nm] ~ rest] => tf t -> xml ctx [] []) = - foldTR [tf] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] r acc => - <xml>{f [nm] [t] [rest] r}{acc}</xml>) - <xml/> + foldR [tf] [fn _ => xml ctx [] []] + (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest] r acc => + <xml>{f [nm] [t] [rest] r}{acc}</xml>) + <xml/> -fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit}) - (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> xml ctx [] []) = - foldT2R [tf] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) - [[nm] ~ rest] r acc => - <xml>{f [nm] [t] [rest] r}{acc}</xml>) - <xml/> - -fun foldT3RX (tf :: (Type * Type * Type) -> Type) (ctx :: {Unit}) - (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> xml ctx [] []) = - foldT3R [tf] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) - [[nm] ~ rest] r acc => - <xml>{f [nm] [t] [rest] r}{acc}</xml>) - <xml/> - -fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit}) - (f : nm :: Name -> t :: Type -> rest :: {Type} +fun foldRX2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (ctx :: {Unit}) + (f : nm :: Name -> t :: K -> rest :: {K} -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> xml ctx [] []) = - foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] - r1 r2 acc => - <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) - <xml/> - -fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) - (ctx :: {Unit}) - (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) = - foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) - [[nm] ~ rest] r1 r2 acc => - <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) - <xml/> - -fun foldT3RX2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type) - (ctx :: {Unit}) - (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) = - foldT3R2 [tf1] [tf2] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) - [[nm] ~ rest] r1 r2 acc => - <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) - <xml/> + foldR2 [tf1] [tf2] [fn _ => xml ctx [] []] + (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest] + r1 r2 acc => + <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>) + <xml/> fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) (q : sql_query tables exps) [tables ~ exps]
--- a/lib/ur/top.urs Sat Feb 21 16:11:56 2009 -0500 +++ b/lib/ur/top.urs Sun Feb 22 16:10:25 2009 -0500 @@ -1,3 +1,12 @@ +(** Row folding *) + +con folder = K ==> fn r :: {K} => + tf :: ({K} -> Type) + -> (nm :: Name -> v :: K -> r :: {K} -> tf r + -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) + -> tf [] -> tf r + + val not : bool -> bool con idT = fn t :: Type => t @@ -25,103 +34,46 @@ -> (nm :: Name -> rest :: {Unit} -> fn [[nm] ~ rest] => tf -> tr rest -> tr ([nm] ++ rest)) - -> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r + -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf r) -> tr r val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type) -> (nm :: Name -> rest :: {Unit} -> fn [[nm] ~ rest] => tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) - -> tr [] -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r + -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit} -> (nm :: Name -> rest :: {Unit} -> fn [[nm] ~ rest] => tf1 -> tf2 -> xml ctx [] []) - -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] [] + -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] [] -val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type) - -> (nm :: Name -> t :: Type -> rest :: {Type} +val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type) + -> (nm :: Name -> t :: K -> rest :: {K} -> fn [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {Type} -> $(map tf r) -> tr r + -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r -val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type) - -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} +val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) + -> tr :: ({K} -> Type) + -> (nm :: Name -> t :: K -> rest :: {K} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) + -> tr [] + -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r + +val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: K -> rest :: {K} + -> fn [[nm] ~ rest] => + tf t -> xml ctx [] []) + -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] [] + +val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: K -> rest :: {K} -> fn [[nm] ~ rest] => - tf t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {(Type * Type)} -> $(map tf r) -> tr r - -val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type) - -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {(Type * Type * Type)} -> $(map tf r) -> tr r - -val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) - -> tr :: ({Type} -> Type) - -> (nm :: Name -> t :: Type -> rest :: {Type} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] - -> r :: {Type} -> $(map tf1 r) -> $(map tf2 r) -> tr r - -val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) - -> tr :: ({(Type * Type)} -> Type) - -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {(Type * Type)} - -> $(map tf1 r) -> $(map tf2 r) -> tr r - -val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) - -> tr :: ({(Type * Type * Type)} -> Type) - -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {(Type * Type * Type)} - -> $(map tf1 r) -> $(map tf2 r) -> tr r - -val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: Type -> rest :: {Type} - -> fn [[nm] ~ rest] => - tf t -> xml ctx [] []) - -> r :: {Type} -> $(map tf r) -> xml ctx [] [] - -val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> xml ctx [] []) - -> r :: {(Type * Type)} -> $(map tf r) -> xml ctx [] [] - -val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> xml ctx [] []) - -> r :: {(Type * Type * Type)} -> $(map tf r) -> xml ctx [] [] - -val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: Type -> rest :: {Type} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) - -> r :: {Type} - -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] - -val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) - -> ctx :: {Unit} - -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) - -> r :: {(Type * Type)} - -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] - - -val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) - -> ctx :: {Unit} - -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) - -> r :: {(Type * Type * Type)} - -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] + tf1 t -> tf2 t -> xml ctx [] []) + -> r ::: {K} -> folder r + -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> sql_query tables exps
--- a/src/core.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/core.sml Sun Feb 22 16:10:25 2009 -0500 @@ -96,7 +96,6 @@ | 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 }
--- a/src/core_print.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/core_print.sml Sun Feb 22 16:10:25 2009 -0500 @@ -342,7 +342,6 @@ string "---", space, p_con' true env c]) - | EFold _ => string "fold" | ECase (e, pes, {disc, result}) => parenIf par (box [string "case",
--- a/src/core_util.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/core_util.sml Sun Feb 22 16:10:25 2009 -0500 @@ -454,10 +454,6 @@ | (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 @@ 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,
--- a/src/corify.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/corify.sml Sun Feb 22 16:10:25 2009 -0500 @@ -592,7 +592,6 @@ {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,
--- a/src/elab.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/elab.sml Sun Feb 22 16:10:25 2009 -0500 @@ -40,6 +40,9 @@ | 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 @@ | 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 @@ | 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 }
--- a/src/elab_env.sig Sat Feb 21 16:11:56 2009 -0500 +++ b/src/elab_env.sig Sun Feb 22 16:10:25 2009 -0500 @@ -47,6 +47,10 @@ | 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
--- a/src/elab_env.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/elab_env.sml Sun Feb 22 16:10:25 2009 -0500 @@ -45,8 +45,32 @@ 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 @@ 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 @@ | (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 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 @@ 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 @@ end val empty = { + renameK = SM.empty, + relK = [], + renameC = SM.empty, relC = [], namedC = IM.empty, @@ -261,12 +305,51 @@ | 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 @@ 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 @@ 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 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 @@ 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 @@ 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 @@ | 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 @@ | _ => 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,
--- a/src/elab_err.sig Sat Feb 21 16:11:56 2009 -0500 +++ b/src/elab_err.sig Sun Feb 22 16:10:25 2009 -0500 @@ -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
--- a/src/elab_err.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/elab_err.sml Sun Feb 22 16:10:25 2009 -0500 @@ -36,7 +36,7 @@ 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 @@ ("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 @@ | 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 @@ | 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 @@ 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 @@ ("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 @@ (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 @@ ("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 @@ 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 =>
--- a/src/elab_ops.sig Sat Feb 21 16:11:56 2009 -0500 +++ b/src/elab_ops.sig Sun Feb 22 16:10:25 2009 -0500 @@ -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
--- a/src/elab_ops.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/elab_ops.sml Sun Feb 22 16:10:25 2009 -0500 @@ -32,8 +32,64 @@ 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 @@ 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 @@ | 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 @@ | _ => 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
--- a/src/elab_print.sig Sat Feb 21 16:11:56 2009 -0500 +++ b/src/elab_print.sig Sun Feb 22 16:10:25 2009 -0500 @@ -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
--- a/src/elab_print.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/elab_print.sml Sun Feb 22 16:10:25 2009 -0500 @@ -38,25 +38,36 @@ 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_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 @@ 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 @@ space, string "::", space, - p_kind k, + p_kind env k, space, string "=>", space, @@ -152,7 +165,7 @@ 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 @@ | 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 @@ space, p_explicitness exp, space, - p_kind k, + p_kind env k, space, string "=>", space, @@ -377,8 +406,6 @@ 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 @@ 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 @@ 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 @@ 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 @@ space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space, @@ -719,7 +756,7 @@ space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space,
--- a/src/elab_util.sig Sat Feb 21 16:11:56 2009 -0500 +++ b/src/elab_util.sig Sun Feb 22 16:10:25 2009 -0500 @@ -30,17 +30,24 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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,
--- a/src/elab_util.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/elab_util.sml Sun Feb 22 16:10:25 2009 -0500 @@ -43,44 +43,60 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ | 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 @@ | 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 @@ 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 @@ 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 @@ 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 @@ (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 @@ 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 @@ | 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 @@ | 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 @@ 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 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 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 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 @@ 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 @@ | 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 @@ 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 @@ | 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)),
--- a/src/elaborate.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/elaborate.sml Sun Feb 22 16:10:25 2009 -0500 @@ -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 @@ | 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 @@ (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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ | 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 @@ | 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 @@ | 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 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 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 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 @@ | 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 @@ | 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 @@ | 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 @@ 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 @@ 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 @@ | 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')
--- a/src/expl.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/expl.sml Sun Feb 22 16:10:25 2009 -0500 @@ -93,7 +93,6 @@ | 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 }
--- a/src/expl_print.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/expl_print.sml Sun Feb 22 16:10:25 2009 -0500 @@ -351,7 +351,6 @@ string "---", space, p_con' true env c]) - | EFold _ => string "fold" | EWrite e => box [string "write(", p_exp env e,
--- a/src/expl_util.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/expl_util.sml Sun Feb 22 16:10:25 2009 -0500 @@ -311,10 +311,6 @@ 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,
--- a/src/explify.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/explify.sml Sun Feb 22 16:10:25 2009 -0500 @@ -107,8 +107,6 @@ {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,
--- a/src/monoize.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/monoize.sml Sun Feb 22 16:10:25 2009 -0500 @@ -2183,7 +2183,6 @@ | L.EConcat _ => poly () | L.ECut _ => poly () | L.ECutMulti _ => poly () - | L.EFold _ => poly () | L.ECase (e, pes, {disc, result}) => let
--- a/src/reduce.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/reduce.sml Sun Feb 22 16:10:25 2009 -0500 @@ -214,20 +214,6 @@ 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 @@ | _ => default () end - | EFold _ => all - | ECase (e, pes, {disc, result}) => let fun patBinds (p, _) =
--- a/src/reduce_local.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/reduce_local.sml Sun Feb 22 16:10:25 2009 -0500 @@ -107,8 +107,6 @@ | 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, _) =
--- a/src/source.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/source.sml Sun Feb 22 16:10:25 2009 -0500 @@ -38,6 +38,9 @@ | KTuple of kind list | KWild + | KFun of string * kind + | KVar of string + withtype kind = kind' located datatype explicitness = @@ -56,6 +59,9 @@ | 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 @@ | 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
--- a/src/source_print.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/source_print.sml Sun Feb 22 16:10:25 2009 -0500 @@ -50,6 +50,13 @@ 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 @@ | 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 @@ 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 @@ 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, _) =
--- a/src/termination.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/termination.sml Sun Feb 22 16:10:25 2009 -0500 @@ -190,6 +190,7 @@ in (p, ps, calls) end + | EKApp (e, _) => combiner calls e | _ => let val (p, calls) = exp parent (penv, calls) e @@ -239,6 +240,13 @@ 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 @@ in (Rabble, calls) end - | EFold _ => (Rabble, calls) | ECase (e, pes, _) => let
--- a/src/unnest.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/unnest.sml Sun Feb 22 16:10:25 2009 -0500 @@ -37,7 +37,7 @@ 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 @@ | (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 @@ | ((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 @@ | _ => 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 @@ 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 @@ | _ => 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 @@ 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
--- a/src/urweb.grm Sat Feb 21 16:11:56 2009 -0500 +++ b/src/urweb.grm Sun Feb 22 16:10:25 2009 -0500 @@ -184,10 +184,10 @@ | 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 @@ %name Urweb +%right KARROW +%nonassoc DKARROW %right SEMI %nonassoc LARROW %nonassoc IF THEN ELSE @@ -575,6 +577,8 @@ | 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 @@ 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 @@ ((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 @@ 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 @@ ((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 @@ (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 @@ () 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
--- a/src/urweb.lex Sat Feb 21 16:11:56 2009 -0500 +++ b/src/urweb.lex Sun Feb 22 16:10:25 2009 -0500 @@ -247,7 +247,9 @@ <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 @@ <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));