# HG changeset patch # User Adam Chlipala # Date 1235507881 18000 # Node ID 03ab853c8e4bffc61daa11e189ffca7c317b7ee5 # Parent 6c4643880df5d7bd9b92bb2954251749c14b42b2 Folder generation for functions diff -r 6c4643880df5 -r 03ab853c8e4b demo/sum.ur --- a/demo/sum.ur Tue Feb 24 15:12:13 2009 -0500 +++ b/demo/sum.ur Tue Feb 24 15:38:01 2009 -0500 @@ -4,7 +4,7 @@ 0 [fs] fl x fun main () = return - {[sum Folder.nil {}]}
- {[sum (Folder.cons [#A] [()] ! (Folder.cons [#B] [()] ! Folder.nil)) {A = 0, B = 1}]}
- {[sum (Folder.cons [#D] [()] ! (Folder.cons [#C] [()] ! (Folder.cons [#E] [()] ! Folder.nil))) {C = 2, D = 3, E = 4}]} + {[sum {}]}
+ {[sum {A = 0, B = 1}]}
+ {[sum {C = 2, D = 3, E = 4}]} diff -r 6c4643880df5 -r 03ab853c8e4b demo/tcSum.ur --- a/demo/tcSum.ur Tue Feb 24 15:12:13 2009 -0500 +++ b/demo/tcSum.ur Tue Feb 24 15:38:01 2009 -0500 @@ -4,6 +4,6 @@ zero [fs] fl x fun main () = return - {[sum (Folder.cons [#A] [()] ! (Folder.cons [#B] [()] ! Folder.nil)) {A = 0, B = 1}]}
- {[sum (Folder.cons [#D] [()] ! (Folder.cons [#C] [()] ! (Folder.cons [#E] [()] ! Folder.nil))) {C = 2.1, D = 3.2, E = 4.3}]} + {[sum {A = 0, B = 1}]}
+ {[sum {C = 2.1, D = 3.2, E = 4.3}]} diff -r 6c4643880df5 -r 03ab853c8e4b src/elaborate.sml --- a/src/elaborate.sml Tue Feb 24 15:12:13 2009 -0500 +++ b/src/elaborate.sml Tue Feb 24 15:38:01 2009 -0500 @@ -49,6 +49,7 @@ structure SM = BinaryMapFn(SK) val basis_r = ref 0 + val top_r = ref 0 fun elabExplicitness e = case e of @@ -1056,6 +1057,7 @@ 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 @@ -1079,19 +1081,43 @@ in unravel (t'', (L'.ECApp (e, u), loc)) end - | (L'.TFun (dom as (L'.CApp (cl, _), _), ran), _) => + | (L'.TFun (dom, ran), _) => let - val cl = hnormCon env cl + fun default () = (e, t, []) in - if infer <> L.TypesOnly andalso E.isClass env cl then + case #1 (hnormCon env dom) of + L'.CApp (cl, x) => let - val r = ref NONE - val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc)) + val cl = hnormCon env cl in - (e, t, TypeClass (env, dom, r, loc) :: gs) + if infer <> L.TypesOnly then + if E.isClass env cl then + let + val r = ref NONE + val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc)) + in + (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 () + else + default () end - else - (e, t, []) + | _ => default () end | (L'.TDisjoint (r1, r2, t'), loc) => if infer <> L.TypesOnly then @@ -3508,11 +3534,13 @@ case E.resolveClass env c of SOME e => r := SOME e | NONE => expError env (Unresolvable (loc, c)) - end) gs + end + | Folder _ => raise Fail "Unresolved folder in top.ur") gs val () = subSgn env' topSgn' topSgn val (env', top_n) = E.pushStrNamed env' "Top" topSgn + val () = top_r := top_n val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} @@ -3560,6 +3588,33 @@ 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)) end) gs; (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)