summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml73
1 files changed, 64 insertions, 9 deletions
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)