Mercurial > urweb

comparison src/elaborate.sml @ 633:03ab853c8e4b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Folder generation for functions
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 15:38:01 -0500
parents 6c4643880df5
children 6302b10dbe0e
comparison
equal deleted inserted replaced
632:6c4643880df5 633:03ab853c8e4b
47 47
48 structure SS = BinarySetFn(SK) 48 structure SS = BinarySetFn(SK)
49 structure SM = BinaryMapFn(SK) 49 structure SM = BinaryMapFn(SK)
50 50
51 val basis_r = ref 0 51 val basis_r = ref 0
52 val top_r = ref 0
52 53
53 fun elabExplicitness e = 54 fun elabExplicitness e =
54 case e of 55 case e of
55 L.Explicit => L'.Explicit 56 L.Explicit => L'.Explicit
56 | L.Implicit => L'.Implicit 57 | L.Implicit => L'.Implicit
1054 | P.String _ => !string 1055 | P.String _ => !string
1055 1056
1056 datatype constraint = 1057 datatype constraint =
1057 Disjoint of D.goal 1058 Disjoint of D.goal
1058 | 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
1059 1061
1060 val enD = map Disjoint 1062 val enD = map Disjoint
1061 1063
1062 fun elabHead (env, denv) infer (e as (_, loc)) t = 1064 fun elabHead (env, denv) infer (e as (_, loc)) t =
1063 let 1065 let
1077 1079
1078 val t'' = subConInCon (0, u) t' 1080 val t'' = subConInCon (0, u) t'
1079 in 1081 in
1080 unravel (t'', (L'.ECApp (e, u), loc)) 1082 unravel (t'', (L'.ECApp (e, u), loc))
1081 end 1083 end
1082 | (L'.TFun (dom as (L'.CApp (cl, _), _), ran), _) => 1084 | (L'.TFun (dom, ran), _) =>
1083 let 1085 let
1084 val cl = hnormCon env cl 1086 fun default () = (e, t, [])
1085 in 1087 in
1086 if infer <> L.TypesOnly andalso E.isClass env cl then 1088 case #1 (hnormCon env dom) of
1089 L'.CApp (cl, x) =>
1087 let 1090 let
1088 val r = ref NONE 1091 val cl = hnormCon env cl
1089 val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc))
1090 in 1092 in
1091 (e, t, TypeClass (env, dom, r, loc) :: gs) 1093 if infer <> L.TypesOnly then
1094 if E.isClass env cl then
1095 let
1096 val r = ref NONE
1097 val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc))
1098 in
1099 (e, t, TypeClass (env, dom, r, loc) :: gs)
1100 end
1101 else
1102 case hnormCon env cl of
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
1118 default ()
1092 end 1119 end
1093 else 1120 | _ => default ()
1094 (e, t, [])
1095 end 1121 end
1096 | (L'.TDisjoint (r1, r2, t'), loc) => 1122 | (L'.TDisjoint (r1, r2, t'), loc) =>
1097 if infer <> L.TypesOnly then 1123 if infer <> L.TypesOnly then
1098 let 1124 let
1099 val gs = D.prove env denv (r1, r2, loc) 1125 val gs = D.prove env denv (r1, r2, loc)
3506 val c = normClassKey env c 3532 val c = normClassKey env c
3507 in 3533 in
3508 case E.resolveClass env c of 3534 case E.resolveClass env c of
3509 SOME e => r := SOME e 3535 SOME e => r := SOME e
3510 | NONE => expError env (Unresolvable (loc, c)) 3536 | NONE => expError env (Unresolvable (loc, c))
3511 end) gs 3537 end
3538 | Folder _ => raise Fail "Unresolved folder in top.ur") gs
3512 3539
3513 val () = subSgn env' topSgn' topSgn 3540 val () = subSgn env' topSgn' topSgn
3514 3541
3515 val (env', top_n) = E.pushStrNamed env' "Top" topSgn 3542 val (env', top_n) = E.pushStrNamed env' "Top" topSgn
3543 val () = top_r := top_n
3516 3544
3517 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} 3545 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn}
3518 3546
3519 fun elabDecl' (d, (env, gs)) = 3547 fun elabDecl' (d, (env, gs)) =
3520 let 3548 let
3558 val c = normClassKey env c 3586 val c = normClassKey env c
3559 in 3587 in
3560 case E.resolveClass env c of 3588 case E.resolveClass env c of
3561 SOME e => r := SOME e 3589 SOME e => r := SOME e
3562 | NONE => expError env (Unresolvable (loc, c)) 3590 | NONE => expError env (Unresolvable (loc, c))
3591 end
3592 | Folder (env, c, r, loc) =>
3593 let
3594 val c = hnormCon env c
3595 in
3596 case #1 c of
3597 L'.CRecord (k, xcs) =>
3598 let
3599 val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc)
3600 val e = (L'.EKApp (e, k), loc)
3601
3602 val (folder, _) = foldr (fn ((x, c), (folder, xcs)) =>
3603 let
3604 val e = (L'.EModProj (top_n, ["Folder"], "cons"), loc)
3605 val e = (L'.EKApp (e, k), loc)
3606 val e = (L'.ECApp (e, (L'.CRecord (k, xcs), loc)), loc)
3607 val e = (L'.ECApp (e, x), loc)
3608 val e = (L'.ECApp (e, c), loc)
3609 val e = (L'.EApp (e, folder), loc)
3610 in
3611 (e, (x, c) :: xcs)
3612 end)
3613 (e, []) xcs
3614 in
3615 r := SOME folder
3616 end
3617 | _ => expError env (Unresolvable (loc, c))
3563 end) gs; 3618 end) gs;
3564 3619
3565 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) 3620 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
3566 :: ds 3621 :: ds
3567 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) 3622 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan)