diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-02-24 15:38:01 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-02-24 15:38:01 -0500 |
| commit | 4f172cc3cd29894ec3989f5a43b40efca1da781b (patch) | |
| tree | 8bec27c38f3de514ebe12b02407a0eb7c935f82d | |
| parent | a609e91b959d905fc10554e97df153c09769ec90 (diff) | |
Folder generation for functions
| -rw-r--r-- | demo/sum.ur | 6 | ||||
| -rw-r--r-- | demo/tcSum.ur | 4 | ||||
| -rw-r--r-- | src/elaborate.sml | 73 |
3 files changed, 69 insertions, 14 deletions
diff --git a/demo/sum.ur b/demo/sum.ur index 62954e20..d2c03004 100644 --- a/demo/sum.ur +++ b/demo/sum.ur @@ -4,7 +4,7 @@ fun sum (fs ::: {Unit}) (fl : folder fs) (x : $(mapUT int fs)) = 0 [fs] fl x fun main () = return <xml><body> - {[sum Folder.nil {}]}<br/> - {[sum (Folder.cons [#A] [()] ! (Folder.cons [#B] [()] ! Folder.nil)) {A = 0, B = 1}]}<br/> - {[sum (Folder.cons [#D] [()] ! (Folder.cons [#C] [()] ! (Folder.cons [#E] [()] ! Folder.nil))) {C = 2, D = 3, E = 4}]} + {[sum {}]}<br/> + {[sum {A = 0, B = 1}]}<br/> + {[sum {C = 2, D = 3, E = 4}]} </body></xml> diff --git a/demo/tcSum.ur b/demo/tcSum.ur index e3340021..080de173 100644 --- a/demo/tcSum.ur +++ b/demo/tcSum.ur @@ -4,6 +4,6 @@ fun sum (t ::: Type) (_ : num t) (fs ::: {Unit}) (fl : folder fs) (x : $(mapUT t zero [fs] fl x fun main () = return <xml><body> - {[sum (Folder.cons [#A] [()] ! (Folder.cons [#B] [()] ! Folder.nil)) {A = 0, B = 1}]}<br/> - {[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}]}<br/> + {[sum {C = 2.1, D = 3.2, E = 4.3}]} </body></xml> diff --git a/src/elaborate.sml b/src/elaborate.sml index c88edd44..5d4d9843 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -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 @@ fun elabFile basis topStr topSgn env file = 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 @@ fun elabFile basis topStr topSgn env file = 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) |