Mercurial > urweb
changeset 326:950320f33232
Crud list works
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 11 Sep 2008 18:32:41 -0400 |
| parents | e457d8972ff1 |
| children | 3a57f3b3a3f8 |
| files | lib/basis.urs src/disjoint.sml src/elab_ops.sml src/elaborate.sml tests/crud.ur tests/crud.urs |
| diffstat | 6 files changed, 85 insertions(+), 44 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/basis.urs Thu Sep 11 17:41:52 2008 -0400 +++ b/lib/basis.urs Thu Sep 11 18:32:41 2008 -0400 @@ -251,6 +251,7 @@ con xhtml = xml [Html] con page = xhtml [] [] con xbody = xml [Body] [] [] +con xtr = xml [Body, Tr] [] [] (*** HTML details *)
--- a/src/disjoint.sml Thu Sep 11 17:41:52 2008 -0400 +++ b/src/disjoint.sml Thu Sep 11 18:32:41 2008 -0400 @@ -199,6 +199,8 @@ | _ => (Unknown cAll :: acc, gs) end in + (*Print.prefaces "decomposeRow'" [("c", ElabPrint.p_con env c), + ("c'", ElabPrint.p_con env (#1 (hnormCon (env, denv) c)))];*) case #1 (#1 (hnormCon (env, denv) c)) of CApp ( (CApp (
--- a/src/elab_ops.sml Thu Sep 11 17:41:52 2008 -0400 +++ b/src/elab_ops.sml Thu Sep 11 18:32:41 2008 -0400 @@ -98,36 +98,40 @@ ("sc", p_con env sc)];*) sc end - | CApp (c', i) => - (case #1 (hnormCon env c') of - CApp (c', f) => - (case #1 (hnormCon env c') of - CFold ks => - (case #1 (hnormCon env c2) of - CRecord (_, []) => hnormCon env i - | CRecord (k, (x, c) :: rest) => - hnormCon env - (CApp ((CApp ((CApp (f, x), loc), c), loc), + | c1' as CApp (c', i) => + let + fun default () = (CApp ((c1', loc), hnormCon env c2), loc) + in + case #1 (hnormCon env c') of + CApp (c', f) => + (case #1 (hnormCon env c') of + CFold ks => + (case #1 (hnormCon env c2) of + CRecord (_, []) => hnormCon env i + | CRecord (k, (x, c) :: rest) => + hnormCon env + (CApp ((CApp ((CApp (f, x), loc), c), loc), (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), - (CRecord (k, rest), loc)), loc)), loc) - | CConcat ((CRecord (k, (x, c) :: rest), _), rest') => - let - val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc) + (CRecord (k, rest), loc)), loc)), loc) + | CConcat ((CRecord (k, (x, c) :: rest), _), rest') => + let + val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc) - (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc), + (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc), + (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), + rest''), loc)), loc)*) + in + (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*) + hnormCon env + (CApp ((CApp ((CApp (f, x), loc), c), loc), (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), - rest''), loc)), loc)*) - in - (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*) - hnormCon env - (CApp ((CApp ((CApp (f, x), loc), c), loc), - (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), - rest''), loc)), loc) - end - | _ => cAll) - | _ => cAll) - | _ => cAll) - | _ => cAll) + rest''), loc)), loc) + end + | _ => default ()) + | _ => default ()) + | _ => default () + end + | c1' => (CApp ((c1', loc), hnormCon env c2), loc)) | CConcat (c1, c2) => (case (hnormCon env c1, hnormCon env c2) of
--- a/src/elaborate.sml Thu Sep 11 17:41:52 2008 -0400 +++ b/src/elaborate.sml Thu Sep 11 18:32:41 2008 -0400 @@ -896,17 +896,28 @@ end and unifyCons' (env, denv) c1 c2 = - let - val (c1, gs1) = hnormCon (env, denv) c1 - val (c2, gs2) = hnormCon (env, denv) c2 - in + case (#1 c1, #1 c2) of + (L'.TDisjoint (x1, y1, t1), L'.TDisjoint (x2, y2, t2)) => let - val gs3 = unifyCons'' (env, denv) c1 c2 + val gs1 = unifyCons' (env, denv) x1 x2 + val gs2 = unifyCons' (env, denv) y1 y2 + val (denv', gs3) = D.assert env denv (x1, y1) + val gs4 = unifyCons' (env, denv') t1 t2 in - gs1 @ gs2 @ gs3 + gs1 @ gs2 @ gs3 @ gs4 end - handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex) - end + | _ => + let + val (c1, gs1) = hnormCon (env, denv) c1 + val (c2, gs2) = hnormCon (env, denv) c2 + in + let + val gs3 = unifyCons'' (env, denv) c1 c2 + in + gs1 @ gs2 @ gs3 + end + handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex) + end and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) = let @@ -1116,12 +1127,18 @@ (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'.CApp ((L'.CRel 3, loc), - recCons (dom, - (L'.CRel 2, loc), - (L'.CRel 1, loc), - (L'.CRel 0, loc), - loc)), loc)), loc)), + (L'.TDisjoint ((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),
--- a/tests/crud.ur Thu Sep 11 17:41:52 2008 -0400 +++ b/tests/crud.ur Thu Sep 11 18:32:41 2008 -0400 @@ -1,3 +1,5 @@ +con colMeta = fn cols :: {Type} => $(Top.mapTT (fn t => {Show : t -> xbody}) cols) + functor Make(M : sig con cols :: {Type} constraint [Id] ~ cols @@ -5,7 +7,7 @@ val title : string - val cols : $(mapTT (fn t => {Show : t -> xbody}) cols) + val cols : $(Top.mapTT (fn t => {Show : t -> xbody}) cols) end) = struct open constraints M @@ -14,7 +16,20 @@ fun list () = rows <- query (SELECT * FROM tab AS T) (fn fs acc => return <body> - {acc} <tr> <td>{txt _ fs.T.Id}</td> </tr> + {acc} + <tr> + <td>{txt _ fs.T.Id}</td> + {fold [fn cols :: {Type} => $cols -> colMeta cols -> xtr] + (fn (nm :: Name) (t :: Type) (rest :: {Type}) acc => + [[nm] ~ rest] => + fn (r : $([nm = t] ++ rest)) cols => + <tr> + <td>{cols.nm.Show r.nm}</td> + {acc (r -- nm) (cols -- nm)} + </tr>) + (fn _ _ => <tr></tr>) + [M.cols] (fs.T -- #Id) M.cols} + </tr> </body>) <body></body>; return <html><head> <title>List</title>
--- a/tests/crud.urs Thu Sep 11 17:41:52 2008 -0400 +++ b/tests/crud.urs Thu Sep 11 18:32:41 2008 -0400 @@ -1,3 +1,5 @@ +con colMeta = fn cols :: {Type} => $(mapTT (fn t => {Show : t -> xbody}) cols) + functor Make(M : sig con cols :: {Type} constraint [Id] ~ cols @@ -5,7 +7,7 @@ val title : string - val cols : $(mapTT (fn t => {Show : t -> xbody}) cols) + val cols : colMeta cols end) : sig val main : unit -> transaction page end