Mercurial > urweb

comparison src/elaborate.sml @ 634:6302b10dbe0e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Folder generation for functors
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 15:54:05 -0500
parents 03ab853c8e4b
children fb2a0e76dcef
comparison
equal deleted inserted replaced
633:03ab853c8e4b 634:6302b10dbe0e
1055 | P.String _ => !string 1055 | P.String _ => !string
1056 1056
1057 datatype constraint = 1057 datatype constraint =
1058 Disjoint of D.goal 1058 Disjoint of D.goal
1059 | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span 1059 | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span
1060 | Folder of E.env * L'.con * L'.exp option ref * ErrorMsg.span
1061 1060
1062 val enD = map Disjoint 1061 val enD = map Disjoint
1062
1063 fun isClassOrFolder env cl =
1064 E.isClass env cl
1065 orelse case hnormCon env cl of
1066 (L'.CKApp (cl, _), _) =>
1067 (case hnormCon env cl of
1068 (L'.CModProj (top_n, [], "folder"), _) => top_n = !top_r
1069 | _ => false)
1070 | _ => false
1063 1071
1064 fun elabHead (env, denv) infer (e as (_, loc)) t = 1072 fun elabHead (env, denv) infer (e as (_, loc)) t =
1065 let 1073 let
1066 fun unravel (t, e) = 1074 fun unravel (t, e) =
1067 case hnormCon env t of 1075 case hnormCon env t of
1089 L'.CApp (cl, x) => 1097 L'.CApp (cl, x) =>
1090 let 1098 let
1091 val cl = hnormCon env cl 1099 val cl = hnormCon env cl
1092 in 1100 in
1093 if infer <> L.TypesOnly then 1101 if infer <> L.TypesOnly then
1094 if E.isClass env cl then 1102 if isClassOrFolder env cl then
1095 let 1103 let
1096 val r = ref NONE 1104 val r = ref NONE
1097 val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc)) 1105 val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc))
1098 in 1106 in
1099 (e, t, TypeClass (env, dom, r, loc) :: gs) 1107 (e, t, TypeClass (env, dom, r, loc) :: gs)
1100 end 1108 end
1101 else 1109 else
1102 case hnormCon env cl of 1110 default ()
1103 (L'.CKApp (cl, _), _) =>
1104 (case hnormCon env cl of
1105 (L'.CModProj (top_n, [], "folder"), _) =>
1106 if top_n = !top_r then
1107 let
1108 val r = ref NONE
1109 val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc))
1110 in
1111 (e, t, Folder (env, x, r, loc) :: gs)
1112 end
1113 else
1114 default ()
1115 | _ => default ())
1116 | _ => default ()
1117 else 1111 else
1118 default () 1112 default ()
1119 end 1113 end
1120 | _ => default () 1114 | _ => default ()
1121 end 1115 end
2847 2841
2848 val t = normClassConstraint env' t 2842 val t = normClassConstraint env' t
2849 in 2843 in
2850 case #1 t of 2844 case #1 t of
2851 L'.CApp (f, _) => 2845 L'.CApp (f, _) =>
2852 if E.isClass env' f then 2846 if isClassOrFolder env' f then
2853 (neededC, constraints, SS.add (neededV, x)) 2847 (neededC, constraints, SS.add (neededV, x))
2854 else 2848 else
2855 default () 2849 default ()
2856
2857 | _ => default () 2850 | _ => default ()
2858 end 2851 end
2859 2852
2860 | _ => (neededC, constraints, neededV) 2853 | _ => (neededC, constraints, neededV)
2861 in 2854 in
2862 (needed, constraints, neededV, E.sgiBinds env' (sgi, loc)) 2855 (needed, constraints, neededV, E.sgiBinds env' (sgi, loc))
2863 end) 2856 end)
2864 (SM.empty, [], SS.empty, env) sgis 2857 (SM.empty, [], SS.empty, env) sgis
2865 2858
2866 val (neededC, neededV) = foldl (fn ((d, _), needed as (neededC, neededV)) => 2859 val (neededC, neededV) =
2867 case d of 2860 foldl (fn ((d, _), needed as (neededC, neededV)) =>
2868 L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV) 2861 case d of
2869 handle NotFound => 2862 L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
2870 needed) 2863 handle NotFound =>
2871 | L.DClass (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV) 2864 needed)
2872 handle NotFound => needed) 2865 | L.DClass (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
2873 | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x)) 2866 handle NotFound => needed)
2874 handle NotFound => needed) 2867 | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x))
2875 | L.DOpen _ => (SM.empty, SS.empty) 2868 handle NotFound => needed)
2876 | _ => needed) 2869 | L.DOpen _ => (SM.empty, SS.empty)
2877 (neededC, neededV) ds 2870 | _ => needed)
2871 (neededC, neededV) ds
2878 2872
2879 val ds' = List.mapPartial (fn (env', (c1, c2), loc) => 2873 val ds' = List.mapPartial (fn (env', (c1, c2), loc) =>
2880 case (decompileCon env' c1, decompileCon env' c2) of 2874 case (decompileCon env' c1, decompileCon env' c2) of
2881 (SOME c1, SOME c2) => 2875 (SOME c1, SOME c2) =>
2882 SOME (L.DConstraint (c1, c2), loc) 2876 SOME (L.DConstraint (c1, c2), loc)
3532 val c = normClassKey env c 3526 val c = normClassKey env c
3533 in 3527 in
3534 case E.resolveClass env c of 3528 case E.resolveClass env c of
3535 SOME e => r := SOME e 3529 SOME e => r := SOME e
3536 | NONE => expError env (Unresolvable (loc, c)) 3530 | NONE => expError env (Unresolvable (loc, c))
3537 end 3531 end) gs
3538 | Folder _ => raise Fail "Unresolved folder in top.ur") gs
3539 3532
3540 val () = subSgn env' topSgn' topSgn 3533 val () = subSgn env' topSgn' topSgn
3541 3534
3542 val (env', top_n) = E.pushStrNamed env' "Top" topSgn 3535 val (env', top_n) = E.pushStrNamed env' "Top" topSgn
3543 val () = top_r := top_n 3536 val () = top_r := top_n
3581 ("Con 2", p_con env c2), 3574 ("Con 2", p_con env c2),
3582 ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)), 3575 ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
3583 ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) 3576 ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))]))
3584 | TypeClass (env, c, r, loc) => 3577 | TypeClass (env, c, r, loc) =>
3585 let 3578 let
3579 fun default () = expError env (Unresolvable (loc, c))
3580
3586 val c = normClassKey env c 3581 val c = normClassKey env c
3587 in 3582 in
3588 case E.resolveClass env c of 3583 case E.resolveClass env c of
3589 SOME e => r := SOME e 3584 SOME e => r := SOME e
3590 | NONE => expError env (Unresolvable (loc, c)) 3585 | NONE =>
3591 end 3586 case #1 (hnormCon env c) of
3592 | Folder (env, c, r, loc) => 3587 L'.CApp (f, x) =>
3593 let 3588 (case (#1 (hnormCon env f), #1 (hnormCon env x)) of
3594 val c = hnormCon env c 3589 (L'.CKApp (f, _), L'.CRecord (k, xcs)) =>
3595 in 3590 (case #1 (hnormCon env f) of
3596 case #1 c of 3591 L'.CModProj (top_n', [], "folder") =>
3597 L'.CRecord (k, xcs) => 3592 if top_n' = top_n then
3598 let 3593 let
3599 val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc) 3594 val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc)
3600 val e = (L'.EKApp (e, k), loc) 3595 val e = (L'.EKApp (e, k), loc)
3601 3596
3602 val (folder, _) = foldr (fn ((x, c), (folder, xcs)) => 3597 val (folder, _) = foldr (fn ((x, c), (folder, xcs)) =>
3603 let 3598 let
3604 val e = (L'.EModProj (top_n, ["Folder"], "cons"), loc) 3599 val e = (L'.EModProj (top_n, ["Folder"],
3605 val e = (L'.EKApp (e, k), loc) 3600 "cons"), loc)
3606 val e = (L'.ECApp (e, (L'.CRecord (k, xcs), loc)), loc) 3601 val e = (L'.EKApp (e, k), loc)
3607 val e = (L'.ECApp (e, x), loc) 3602 val e = (L'.ECApp (e,
3608 val e = (L'.ECApp (e, c), loc) 3603 (L'.CRecord (k, xcs),
3609 val e = (L'.EApp (e, folder), loc) 3604 loc)), loc)
3610 in 3605 val e = (L'.ECApp (e, x), loc)
3611 (e, (x, c) :: xcs) 3606 val e = (L'.ECApp (e, c), loc)
3612 end) 3607 val e = (L'.EApp (e, folder), loc)
3613 (e, []) xcs 3608 in
3614 in 3609 (e, (x, c) :: xcs)
3615 r := SOME folder 3610 end)
3616 end 3611 (e, []) xcs
3617 | _ => expError env (Unresolvable (loc, c)) 3612 in
3613 r := SOME folder
3614 end
3615 else
3616 default ()
3617 | _ => default ())
3618 | _ => default ())
3619 | _ => default ()
3618 end) gs; 3620 end) gs;
3619 3621
3620 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) 3622 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
3621 :: ds 3623 :: ds
3622 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) 3624 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan)