Mercurial > urweb
changeset 629:e68de2a5506b
Top.Fold.concat elaborates
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 24 Feb 2009 13:46:08 -0500 |
| parents | 12b73f3c108e |
| children | 6a6eb9882d57 |
| files | lib/ur/basis.urs lib/ur/top.ur lib/ur/top.urs src/elaborate.sml src/source.sml src/source_print.sml src/urweb.grm src/urweb.lex |
| diffstat | 8 files changed, 129 insertions(+), 92 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/basis.urs Tue Feb 24 12:01:24 2009 -0500 +++ b/lib/ur/basis.urs Tue Feb 24 13:46:08 2009 -0500 @@ -277,7 +277,7 @@ (*** Executing queries *) val query : tables ::: {{Type}} -> exps ::: {Type} - -> fn [tables ~ exps] => + -> [tables ~ exps] => state ::: Type -> sql_query tables exps -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) @@ -298,7 +298,7 @@ -> dml val update : unchanged ::: {Type} -> changed :: {Type} -> - fn [changed ~ unchanged] => + [changed ~ unchanged] => $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed) -> sql_table (changed ++ unchanged) -> sql_exp [T = changed ++ unchanged] [] [] bool @@ -326,23 +326,23 @@ -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit} -> useOuter ::: {Type} -> useInner ::: {Type} -> bindOuter ::: {Type} -> bindInner ::: {Type} - -> fn [attrsGiven ~ attrsAbsent] - [useOuter ~ useInner] - [bindOuter ~ bindInner] => - $attrsGiven - -> tag (attrsGiven ++ attrsAbsent) - ctxOuter ctxInner useOuter bindOuter - -> xml ctxInner useInner bindInner - -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner) + -> [attrsGiven ~ attrsAbsent] => + [useOuter ~ useInner] => + [bindOuter ~ bindInner] => + $attrsGiven + -> tag (attrsGiven ++ attrsAbsent) + ctxOuter ctxInner useOuter bindOuter + -> xml ctxInner useInner bindInner + -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner) val join : ctx ::: {Unit} -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type} - -> fn [use1 ~ bind1] [bind1 ~ bind2] => + -> [use1 ~ bind1] => [bind1 ~ bind2] => xml ctx use1 bind1 -> xml ctx (use1 ++ bind1) bind2 -> xml ctx use1 (bind1 ++ bind2) val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type} -> bind ::: {Type} - -> fn [use1 ~ use2] => + -> [use1 ~ use2] => xml ctx use1 bind -> xml ctx (use1 ++ use2) bind @@ -370,11 +370,11 @@ val body : unit -> tag [] html body [] [] con bodyTag = fn (attrs :: {Type}) => ctx ::: {Unit} -> - fn [[Body] ~ ctx] => + [[Body] ~ ctx] => unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] [] con bodyTagStandalone = fn (attrs :: {Type}) => ctx ::: {Unit} - -> fn [[Body] ~ ctx] => + -> [[Body] ~ ctx] => unit -> tag attrs ([Body] ++ ctx) [] [] [] val br : bodyTagStandalone [] @@ -399,12 +399,12 @@ val a : bodyTag [Link = transaction page, Onclick = transaction unit] val form : ctx ::: {Unit} -> bind ::: {Type} - -> fn [[Body] ~ ctx] => + -> [[Body] ~ ctx] => xml form [] bind -> xml ([Body] ++ ctx) [] [] con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) => ctx ::: {Unit} - -> fn [[Form] ~ ctx] => + -> [[Form] ~ ctx] => nm :: Name -> unit -> tag attrs ([Form] ++ ctx) inner [] [nm = ty] val textbox : formTag string [] [Value = string, Size = int, Source = source string] @@ -422,7 +422,7 @@ val option : unit -> tag [Value = string, Selected = bool] select [] [] [] val submit : ctx ::: {Unit} -> use ::: {Type} - -> fn [[Form] ~ ctx] => + -> [[Form] ~ ctx] => unit -> tag [Value = string, Action = $use -> transaction page] ([Form] ++ ctx) ([Form] ++ ctx) use [] @@ -431,7 +431,7 @@ con cformTag = fn (attrs :: {Type}) => ctx ::: {Unit} - -> fn [[Body] ~ ctx] => + -> [[Body] ~ ctx] => unit -> tag attrs ([Body] ++ ctx) [] [] [] val ctextbox : cformTag [Value = string, Size = int, Source = source string] @@ -439,13 +439,13 @@ (*** Tables *) -val tabl : other ::: {Unit} -> fn [other ~ [Body, Table]] => +val tabl : other ::: {Unit} -> [other ~ [Body, Table]] => unit -> tag [Border = int] ([Body] ++ other) ([Body, Table] ++ other) [] [] -val tr : other ::: {Unit} -> fn [other ~ [Body, Table, Tr]] => +val tr : other ::: {Unit} -> [other ~ [Body, Table, Tr]] => unit -> tag [] ([Body, Table] ++ other) ([Body, Tr] ++ other) [] [] -val th : other ::: {Unit} -> fn [other ~ [Body, Tr]] => +val th : other ::: {Unit} -> [other ~ [Body, Tr]] => unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] [] -val td : other ::: {Unit} -> fn [other ~ [Body, Tr]] => +val td : other ::: {Unit} -> [other ~ [Body, Tr]] => unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] []
--- a/lib/ur/top.ur Tue Feb 24 12:01:24 2009 -0500 +++ b/lib/ur/top.ur Tue Feb 24 13:46:08 2009 -0500 @@ -3,32 +3,32 @@ con folder = K ==> fn r :: {K} => tf :: ({K} -> Type) -> (nm :: Name -> v :: K -> r :: {K} -> tf r - -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) + -> [[nm] ~ r] => tf ([nm = v] ++ r)) -> tf [] -> tf r structure Folder = struct fun nil K (tf :: {K} -> Type) (f : nm :: Name -> v :: K -> r :: {K} -> tf r - -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) + -> [[nm] ~ r] => tf ([nm = v] ++ r)) (i : tf []) = i fun cons K (r ::: {K}) (nm :: Name) (v :: K) [[nm] ~ r] (fold : folder r) (tf :: {K} -> Type) (f : nm :: Name -> v :: K -> r :: {K} -> tf r - -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) - (i : tf []) = f [nm] [v] [r] (fold [tf] f i) + -> [[nm] ~ r] => tf ([nm = v] ++ r)) + (i : tf []) = f [nm] [v] [r] (fold [tf] f i) ! fun concat K (r1 ::: {K}) (r2 ::: {K}) [r1 ~ r2] (f1 : folder r1) (f2 : folder r2) (tf :: {K} -> Type) (f : nm :: Name -> v :: K -> r :: {K} -> tf r - -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) + -> [[nm] ~ r] => tf ([nm = v] ++ r)) (i : tf []) = - f1 [fn r1' [r1' ~ r2] => tf (r1' ++ r2)] 0 - (*(fn (nm :: Name) (v :: K) (r1' :: {K}) (acc : fn [r1' ~ r2] => tf (r1' ++ r2)) + f1 [fn r1' => [r1' ~ r2] => tf (r1' ++ r2)] + (fn (nm :: Name) (v :: K) (r1' :: {K}) (acc : [r1' ~ r2] => tf (r1' ++ r2)) [[nm] ~ r1'] [[nm = v] ++ r1' ~ r2] => - f [nm] [v] [r1' ++ r2] acc) - (f2 [tf] f i)*) + f [nm] [v] [r1' ++ r2] acc !) + (fn [[] ~ r2] => f2 [tf] f i) ! end @@ -59,74 +59,74 @@ fun foldUR (tf :: Type) (tr :: {Unit} -> Type) (f : nm :: Name -> rest :: {Unit} - -> fn [[nm] ~ rest] => + -> [[nm] ~ rest] => tf -> tr rest -> tr ([nm] ++ rest)) (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))) + 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] => + -> [[nm] ~ rest] => tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) (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))) + 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} - -> fn [[nm] ~ rest] => + -> [[nm] ~ rest] => tf1 -> tf2 -> xml ctx [] []) = foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []] (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] v1 v2 acc => - <xml>{f [nm] [rest] v1 v2}{acc}</xml>) + <xml>{f [nm] [rest] ! v1 v2}{acc}</xml>) <xml/> fun foldR K (tf :: K -> Type) (tr :: {K} -> Type) (f : nm :: Name -> t :: K -> rest :: {K} - -> fn [[nm] ~ rest] => + -> [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ 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))) + f [nm] [t] [rest] ! r.nm (acc (r -- nm))) (fn _ => i) fun foldR2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (tr :: {K} -> Type) (f : nm :: Name -> t :: K -> rest :: {K} - -> fn [[nm] ~ rest] => + -> [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) (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))) + f [nm] [t] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) (fn _ _ => i) fun foldRX K (tf :: K -> Type) (ctx :: {Unit}) (f : nm :: Name -> t :: K -> rest :: {K} - -> fn [[nm] ~ rest] => + -> [[nm] ~ rest] => tf t -> xml ctx [] []) = 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>{f [nm] [t] [rest] ! r}{acc}</xml>) <xml/> fun foldRX2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (ctx :: {Unit}) (f : nm :: Name -> t :: K -> rest :: {K} - -> fn [[nm] ~ rest] => + -> [[nm] ~ rest] => tf1 t -> tf2 t -> xml ctx [] []) = 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>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>) <xml/> fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) @@ -148,13 +148,14 @@ <xml/> fun oneOrNoRows (tables ::: {{Type}}) (exps ::: {Type}) - (q : sql_query tables exps) [tables ~ exps] = + [tables ~ exps] + (q : sql_query tables exps) = query q (fn fs _ => return (Some fs)) None fun oneRow (tables ::: {{Type}}) (exps ::: {Type}) - (q : sql_query tables exps) [tables ~ exps] = + [tables ~ exps] (q : sql_query tables exps) = o <- oneOrNoRows q; return (case o of None => error <xml>Query returned no rows</xml>
--- a/lib/ur/top.urs Tue Feb 24 12:01:24 2009 -0500 +++ b/lib/ur/top.urs Tue Feb 24 13:46:08 2009 -0500 @@ -3,15 +3,15 @@ con folder = K ==> fn r :: {K} => tf :: ({K} -> Type) -> (nm :: Name -> v :: K -> r :: {K} -> tf r - -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) + -> [[nm] ~ r] => tf ([nm = v] ++ r)) -> tf [] -> tf r structure Folder : sig val nil : K --> folder (([]) :: {K}) val cons : K --> r ::: {K} -> nm :: Name -> v :: K - -> fn [[nm] ~ r] => folder r -> folder ([nm = v] ++ r) + -> [[nm] ~ r] => folder r -> folder ([nm = v] ++ r) val concat : K --> r1 ::: {K} -> r2 ::: {K} - -> fn [r1 ~ r2] => folder r1 -> folder r2 -> folder (r1 ++ r2) + -> [r1 ~ r2] => folder r1 -> folder r2 -> folder (r1 ++ r2) end @@ -40,78 +40,78 @@ val foldUR : tf :: Type -> tr :: ({Unit} -> Type) -> (nm :: Name -> rest :: {Unit} - -> fn [[nm] ~ rest] => + -> [[nm] ~ rest] => tf -> tr rest -> tr ([nm] ++ rest)) -> 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] => + -> [[nm] ~ rest] => tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) -> 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] => + -> [[nm] ~ rest] => tf1 -> tf2 -> xml ctx [] []) -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] [] val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type) -> (nm :: Name -> t :: K -> rest :: {K} - -> fn [[nm] ~ rest] => + -> [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tr :: ({K} -> Type) -> (nm :: Name -> t :: K -> rest :: {K} - -> fn [[nm] ~ rest] => + -> [[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] => + -> [[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] => + -> [[nm] ~ rest] => 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 - -> fn [tables ~ exps] => + -> [tables ~ exps] => ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> xml ctx [] []) -> transaction (xml ctx [] []) val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> sql_query tables exps - -> fn [tables ~ exps] => + -> [tables ~ exps] => ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (xml ctx [] [])) -> transaction (xml ctx [] []) val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type} - -> sql_query tables exps - -> fn [tables ~ exps] => - transaction - (option - $(exps - ++ map (fn fields :: {Type} => $fields) tables)) + -> [tables ~ exps] => + sql_query tables exps + -> transaction + (option + $(exps + ++ map (fn fields :: {Type} => $fields) tables)) val oneRow : tables ::: {{Type}} -> exps ::: {Type} - -> sql_query tables exps - -> fn [tables ~ exps] => - transaction - $(exps - ++ map (fn fields :: {Type} => $fields) tables) - + -> [tables ~ exps] => + sql_query tables exps + -> transaction + $(exps + ++ map (fn fields :: {Type} => $fields) tables) + val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type -> sql_injectable (option t) -> sql_exp tables agg exps (option t)
--- a/src/elaborate.sml Tue Feb 24 12:01:24 2009 -0500 +++ b/src/elaborate.sml Tue Feb 24 13:46:08 2009 -0500 @@ -1025,7 +1025,7 @@ val enD = map Disjoint - fun elabHead env infer (e as (_, loc)) t = + fun elabHead (env, denv) infer (e as (_, loc)) t = let fun unravel (t, e) = case hnormCon env t of @@ -1059,6 +1059,16 @@ else (e, t, []) end + | (L'.TDisjoint (r1, r2, t'), loc) => + if infer <> L.TypesOnly then + let + val gs = D.prove env denv (r1, r2, loc) + val (e, t, gs') = unravel (t', e) + in + (e, t, enD gs @ gs') + end + else + (e, t, []) | t => (e, t, []) in case infer of @@ -1185,7 +1195,7 @@ | Datatype _ => "Datatype" | Record _ => "Record" -fun exhaustive (env, t, ps) = +fun exhaustive (env, t, ps, loc) = let fun depth (p, _) = case p of @@ -1364,7 +1374,8 @@ end | L'.CError => true | c => - (prefaces "Not a datatype" [("c", p_con env (c, ErrorMsg.dummySpan))]; + (prefaces "Not a datatype" [("loc", PD.string (ErrorMsg.spanToString loc)), + ("c", p_con env (c, ErrorMsg.dummySpan))]; raise Fail "isTotal: Not a datatype") end | Record _ => List.all (fn c2 => coverageImp (c, c2)) (enumerateCases depth t) @@ -1437,8 +1448,8 @@ E.NotBound => (expError env (UnboundExp (loc, s)); (eerror, cerror, [])) - | E.Rel (n, t) => elabHead env infer (L'.ERel n, loc) t - | E.Named (n, t) => elabHead env infer (L'.ENamed n, loc) t) + | E.Rel (n, t) => elabHead (env, denv) infer (L'.ERel n, loc) t + | E.Named (n, t) => elabHead (env, denv) infer (L'.ENamed n, loc) t) | L.EVar (m1 :: ms, s, infer) => (case E.lookupStr env m1 of NONE => (expError env (UnboundStrInExp (loc, m1)); @@ -1457,7 +1468,7 @@ cerror) | SOME t => t in - elabHead env infer (L'.EModProj (n, ms, s), loc) t + elabHead (env, denv) infer (L'.EModProj (n, ms, s), loc) t end) | L.EWild => @@ -1566,6 +1577,20 @@ (e', (L'.TDisjoint (c1', c2', t), loc), enD gs1 @ enD gs2 @ gs3) end + | L.EDisjointApp e => + let + val (e', t, gs1) = elabExp (env, denv) e + + val k1 = kunif loc + val c1 = cunif (loc, (L'.KRecord k1, loc)) + val k2 = kunif loc + val c2 = cunif (loc, (L'.KRecord k2, loc)) + val t' = cunif (loc, ktype) + val () = checkCon env e' t (L'.TDisjoint (c1, c2, t'), loc) + val gs2 = D.prove env denv (c1, c2, loc) + in + (e', t', enD gs2 @ gs1) + end | L.ERecord xes => let @@ -1617,11 +1642,10 @@ val ft = cunif (loc, ktype) val rest = cunif (loc, ktype_record) val first = (L'.CRecord (ktype, [(c', ft)]), loc) - + val () = checkCon env e' et + (L'.TRecord (L'.CConcat (first, rest), loc), loc); val gs3 = D.prove env denv (first, rest, loc) in - checkCon env e' et - (L'.TRecord (L'.CConcat (first, rest), loc), loc); ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3) end @@ -1633,10 +1657,11 @@ val r1 = cunif (loc, ktype_record) val r2 = cunif (loc, ktype_record) + val () = checkCon env e1' e1t (L'.TRecord r1, loc) + val () = checkCon env e2' e2t (L'.TRecord r2, loc) + val gs3 = D.prove env denv (r1, r2, loc) in - checkCon env e1' e1t (L'.TRecord r1, loc); - checkCon env e2' e2t (L'.TRecord r2, loc); ((L'.EConcat (e1', r1, e2', r2), loc), (L'.TRecord ((L'.CConcat (r1, r2), loc)), loc), gs1 @ gs2 @ enD gs3) @@ -1649,11 +1674,12 @@ val ft = cunif (loc, ktype) val rest = cunif (loc, ktype_record) val first = (L'.CRecord (ktype, [(c', ft)]), loc) + + val () = checkCon env e' et + (L'.TRecord (L'.CConcat (first, rest), loc), loc) val gs3 = D.prove env denv (first, rest, loc) in - checkCon env e' et - (L'.TRecord (L'.CConcat (first, rest), loc), loc); ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc), gs1 @ enD gs2 @ enD gs3) end @@ -1663,11 +1689,12 @@ val (c', ck, gs2) = elabCon (env, denv) c val rest = cunif (loc, ktype_record) + + val () = checkCon env e' et + (L'.TRecord (L'.CConcat (c', rest), loc), loc) val gs3 = D.prove env denv (c', rest, loc) in - checkCon env e' et - (L'.TRecord (L'.CConcat (c', rest), loc), loc); ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc), gs1 @ enD gs2 @ enD gs3) end @@ -1681,15 +1708,15 @@ let val ((p', pt), (env, _)) = elabPat (p, (env, SS.empty)) - val (e', et, gs1) = elabExp (env, denv) e + val (e', et', gs1) = elabExp (env, denv) e in checkPatCon env p' pt et; - checkCon env e' et result; + checkCon env e' et' result; ((p', e'), gs1 @ gs) end) gs1 pes in - if exhaustive (env, et, map #1 pes') then + if exhaustive (env, et, map #1 pes', loc) then () else expError env (Inexhaustive loc); @@ -1722,10 +1749,11 @@ val (e', et, gs2) = elabExp (env, denv) e + val () = checkCon env e' et c' + val c' = normClassConstraint env c' val env' = E.pushERel env x c' in - checkCon env e' et c'; ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ gs)) end | L.EDValRec vis => @@ -2958,10 +2986,12 @@ | SOME c => elabCon (env, denv) c val (e', et, gs2) = elabExp (env, denv) e + + val () = checkCon env e' et c' + val c = normClassConstraint env c' val (env', n) = E.pushENamed env x c' in - checkCon env e' et c'; (*prefaces "DVal" [("x", Print.PD.string x), ("c'", p_con env c')];*) ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ gs))
--- a/src/source.sml Tue Feb 24 12:01:24 2009 -0500 +++ b/src/source.sml Tue Feb 24 13:46:08 2009 -0500 @@ -124,6 +124,7 @@ | ECApp of exp * con | ECAbs of explicitness * string * kind * exp | EDisjoint of con * con * exp + | EDisjointApp of exp | EKAbs of string * exp
--- a/src/source_print.sml Tue Feb 24 12:01:24 2009 -0500 +++ b/src/source_print.sml Tue Feb 24 13:46:08 2009 -0500 @@ -267,6 +267,9 @@ string "=>", space, p_exp e]) + | EDisjointApp e => parenIf par (box [p_exp e, + space, + string "!"]) | ERecord xes => box [string "{", p_list (fn (x, e) =>
--- a/src/urweb.grm Tue Feb 24 12:01:24 2009 -0500 +++ b/src/urweb.grm Tue Feb 24 13:46:08 2009 -0500 @@ -187,7 +187,7 @@ | CON | LTYPE | VAL | REC | AND | FUN | MAP | UNIT | KUNIT | CLASS | DATATYPE | OF | TYPE | NAME - | ARROW | LARROW | DARROW | STAR | SEMI | KARROW | DKARROW + | ARROW | LARROW | DARROW | STAR | SEMI | KARROW | DKARROW | BANG | FN | PLUSPLUS | MINUSMINUS | MINUSMINUSMINUS | DOLLAR | TWIDDLE | LET | IN | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | SQL @@ -710,6 +710,7 @@ eapps : eterm (eterm) | eapps eterm (EApp (eapps, eterm), s (eappsleft, etermright)) | eapps LBRACK cexp RBRACK (ECApp (eapps, cexp), s (eappsleft, RBRACKright)) + | eapps BANG (EDisjointApp eapps, s (eappsleft, BANGright)) eexp : eapps (eapps) | FN eargs DARROW eexp (let
--- a/src/urweb.lex Tue Feb 24 12:01:24 2009 -0500 +++ b/src/urweb.lex Tue Feb 24 13:46:08 2009 -0500 @@ -276,6 +276,7 @@ <INITIAL> "*" => (Tokens.STAR (pos yypos, pos yypos + size yytext)); <INITIAL> "<-" => (Tokens.LARROW (pos yypos, pos yypos + size yytext)); <INITIAL> ";" => (Tokens.SEMI (pos yypos, pos yypos + size yytext)); +<INITIAL> "!" => (Tokens.BANG (pos yypos, pos yypos + size yytext)); <INITIAL> "+" => (Tokens.PLUS (pos yypos, pos yypos + size yytext)); <INITIAL> "-" => (Tokens.MINUS (pos yypos, pos yypos + size yytext));