From 11809629254afd8ea304b98b840bd9a1aea29f6c Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 24 Feb 2009 15:54:05 -0500 Subject: Folder generation for functors --- src/elaborate.sml | 124 +++++++++++++++++++++++++++--------------------------- 1 file changed, 63 insertions(+), 61 deletions(-) (limited to 'src/elaborate.sml') diff --git a/src/elaborate.sml b/src/elaborate.sml index 5d4d9843..c55593b4 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -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 @@ fun wildifyStr env (str, sgn) = 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 @@ fun wildifyStr env (str, sgn) = 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 @@ 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 _ => raise Fail "Unresolved folder in top.ur") gs + end) gs val () = subSgn env' topSgn' topSgn @@ -3583,38 +3576,47 @@ fun elabFile basis topStr topSgn env file = ("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) -- cgit v1.2.3