Mercurial > urweb
changeset 634:6302b10dbe0e
Folder generation for functors
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 24 Feb 2009 15:54:05 -0500 |
| parents | 03ab853c8e4b |
| children | 75c7a69354d6 |
| files | demo/crud1.ur demo/crud2.ur demo/metaform1.ur demo/metaform2.ur src/elaborate.sml |
| diffstat | 5 files changed, 63 insertions(+), 73 deletions(-) [+] |
line wrap: on
line diff
--- a/demo/crud1.ur Tue Feb 24 15:38:01 2009 -0500 +++ b/demo/crud1.ur Tue Feb 24 15:54:05 2009 -0500 @@ -9,10 +9,4 @@ B = Crud.string "B", C = Crud.float "C", D = Crud.bool "D"} - - val fl = Folder.cons [#A] [_] ! - (Folder.cons [#B] [_] ! - (Folder.cons [#C] [_] ! - (Folder.cons [#D] [_] ! - Folder.nil))) end)
--- a/demo/crud2.ur Tue Feb 24 15:38:01 2009 -0500 +++ b/demo/crud2.ur Tue Feb 24 15:54:05 2009 -0500 @@ -31,8 +31,4 @@ Inject = _ } } - - val fl = Folder.cons [#Nam] [_] ! - (Folder.cons [#Ready] [_] ! - Folder.nil) end)
--- a/demo/metaform1.ur Tue Feb 24 15:38:01 2009 -0500 +++ b/demo/metaform1.ur Tue Feb 24 15:54:05 2009 -0500 @@ -1,4 +1,3 @@ open Metaform.Make(struct val names = {A = "Tic", B = "Tac", C = "Toe"} - val fl = Folder.cons [#A] [()] ! (Folder.cons [#B] [()] ! (Folder.cons [#C] [()] ! Folder.nil)) end)
--- a/demo/metaform2.ur Tue Feb 24 15:38:01 2009 -0500 +++ b/demo/metaform2.ur Tue Feb 24 15:54:05 2009 -0500 @@ -1,6 +1,5 @@ structure MM = Metaform.Make(struct val names = {X = "x", Y = "y"} - val fl = Folder.cons [#X] [()] ! (Folder.cons [#Y] [()] ! Folder.nil) end) fun diversion () = return <xml><body>
--- a/src/elaborate.sml Tue Feb 24 15:38:01 2009 -0500 +++ b/src/elaborate.sml Tue Feb 24 15:54:05 2009 -0500 @@ -1057,10 +1057,18 @@ datatype constraint = Disjoint of D.goal | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span - | Folder of E.env * L'.con * L'.exp option ref * ErrorMsg.span val enD = map Disjoint + fun isClassOrFolder env cl = + E.isClass env cl + orelse case hnormCon env cl of + (L'.CKApp (cl, _), _) => + (case hnormCon env cl of + (L'.CModProj (top_n, [], "folder"), _) => top_n = !top_r + | _ => false) + | _ => false + fun elabHead (env, denv) infer (e as (_, loc)) t = let fun unravel (t, e) = @@ -1091,7 +1099,7 @@ val cl = hnormCon env cl in if infer <> L.TypesOnly then - if E.isClass env cl then + if isClassOrFolder env cl then let val r = ref NONE val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc)) @@ -1099,21 +1107,7 @@ (e, t, TypeClass (env, dom, r, loc) :: gs) end else - case hnormCon env cl of - (L'.CKApp (cl, _), _) => - (case hnormCon env cl of - (L'.CModProj (top_n, [], "folder"), _) => - if top_n = !top_r then - let - val r = ref NONE - val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc)) - in - (e, t, Folder (env, x, r, loc) :: gs) - end - else - default () - | _ => default ()) - | _ => default () + default () else default () end @@ -2849,11 +2843,10 @@ in case #1 t of L'.CApp (f, _) => - if E.isClass env' f then + if isClassOrFolder env' f then (neededC, constraints, SS.add (neededV, x)) else default () - | _ => default () end @@ -2863,18 +2856,19 @@ end) (SM.empty, [], SS.empty, env) sgis - val (neededC, neededV) = foldl (fn ((d, _), needed as (neededC, neededV)) => - case d of - L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV) - handle NotFound => - needed) - | L.DClass (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV) - handle NotFound => needed) - | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x)) - handle NotFound => needed) - | L.DOpen _ => (SM.empty, SS.empty) - | _ => needed) - (neededC, neededV) ds + val (neededC, neededV) = + foldl (fn ((d, _), needed as (neededC, neededV)) => + case d of + L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV) + handle NotFound => + needed) + | L.DClass (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV) + handle NotFound => needed) + | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x)) + handle NotFound => needed) + | L.DOpen _ => (SM.empty, SS.empty) + | _ => needed) + (neededC, neededV) ds val ds' = List.mapPartial (fn (env', (c1, c2), loc) => case (decompileCon env' c1, decompileCon env' c2) of @@ -3534,8 +3528,7 @@ case E.resolveClass env c of SOME e => r := SOME e | NONE => expError env (Unresolvable (loc, c)) - end - | Folder _ => raise Fail "Unresolved folder in top.ur") gs + end) gs val () = subSgn env' topSgn' topSgn @@ -3583,38 +3576,47 @@ ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) | TypeClass (env, c, r, loc) => let + fun default () = expError env (Unresolvable (loc, c)) + val c = normClassKey env c in case E.resolveClass env c of SOME e => r := SOME e - | NONE => expError env (Unresolvable (loc, c)) - end - | Folder (env, c, r, loc) => - let - val c = hnormCon env c - in - case #1 c of - L'.CRecord (k, xcs) => - let - val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc) - val e = (L'.EKApp (e, k), loc) - - val (folder, _) = foldr (fn ((x, c), (folder, xcs)) => - let - val e = (L'.EModProj (top_n, ["Folder"], "cons"), loc) - val e = (L'.EKApp (e, k), loc) - val e = (L'.ECApp (e, (L'.CRecord (k, xcs), loc)), loc) - val e = (L'.ECApp (e, x), loc) - val e = (L'.ECApp (e, c), loc) - val e = (L'.EApp (e, folder), loc) - in - (e, (x, c) :: xcs) - end) - (e, []) xcs - in - r := SOME folder - end - | _ => expError env (Unresolvable (loc, c)) + | NONE => + case #1 (hnormCon env c) of + L'.CApp (f, x) => + (case (#1 (hnormCon env f), #1 (hnormCon env x)) of + (L'.CKApp (f, _), L'.CRecord (k, xcs)) => + (case #1 (hnormCon env f) of + L'.CModProj (top_n', [], "folder") => + if top_n' = top_n then + let + val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc) + val e = (L'.EKApp (e, k), loc) + + val (folder, _) = foldr (fn ((x, c), (folder, xcs)) => + let + val e = (L'.EModProj (top_n, ["Folder"], + "cons"), loc) + val e = (L'.EKApp (e, k), loc) + val e = (L'.ECApp (e, + (L'.CRecord (k, xcs), + loc)), loc) + val e = (L'.ECApp (e, x), loc) + val e = (L'.ECApp (e, c), loc) + val e = (L'.EApp (e, folder), loc) + in + (e, (x, c) :: xcs) + end) + (e, []) xcs + in + r := SOME folder + end + else + default () + | _ => default ()) + | _ => default ()) + | _ => default () end) gs; (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)