Mercurial > urweb

comparison src/elaborate.sml @ 1767:1bbad32cb4a8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Implicit records of folders
author Adam Chlipala <adam@chlipala.net>
date Thu, 17 May 2012 16:22:05 -0400
parents 518e0b23c4ef
children bb942416bf1c
comparison
equal deleted inserted replaced
1766:92cfc69419bd 1767:1bbad32cb4a8
1442 1442
1443 fun hasInstance c = 1443 fun hasInstance c =
1444 case hnormCon env c of 1444 case hnormCon env c of
1445 (L'.TRecord c, _) => U.Con.exists {kind = fn _ => false, 1445 (L'.TRecord c, _) => U.Con.exists {kind = fn _ => false,
1446 con = fn c => 1446 con = fn c =>
1447 E.isClass env (hnormCon env (c, loc))} c 1447 isClassOrFolder env (hnormCon env (c, loc))} c
1448 | c => 1448 | c =>
1449 let 1449 let
1450 fun findHead c = 1450 fun findHead c =
1451 case #1 c of 1451 case #1 c of
1452 L'.CApp (f, _) => findHead f 1452 L'.CApp (f, _) => findHead f
4589 4589
4590 if stopHere () then 4590 if stopHere () then
4591 () 4591 ()
4592 else 4592 else
4593 let 4593 let
4594 fun solver gs = 4594 fun solver (gs : constraint list) =
4595 let 4595 let
4596 val (gs, solved) = 4596 val (gs, solved) =
4597 ListUtil.foldlMapPartial 4597 ListUtil.foldlMapPartial
4598 (fn (g, solved) => 4598 (fn (g : constraint, solved) =>
4599 case g of 4599 case g of
4600 Disjoint (loc, env, denv, c1, c2) => 4600 Disjoint (loc, env, denv, c1, c2) =>
4601 (case D.prove env denv (c1, c2, loc) of 4601 (case D.prove env denv (c1, c2, loc) of
4602 [] => (NONE, true) 4602 [] => (NONE, true)
4603 | _ => (SOME g, solved)) 4603 | _ => (SOME g, solved))
4604 | TypeClass (env, c, r, loc) => 4604 | TypeClass (env, c, r, loc) =>
4605 let 4605 let
4606 fun default () = (SOME g, solved) 4606 fun default () = (SOME g, solved)
4607 4607
4608 val c = normClassKey env c 4608 fun resolver r c =
4609 let
4610 val c = normClassKey env c
4611 in
4612 case resolveClass env c of
4613 SOME e => (r := SOME e;
4614 (NONE, true))
4615 | NONE =>
4616 case #1 (hnormCon env c) of
4617 L'.CApp (f, x) =>
4618 (case (#1 (hnormCon env f), #1 (hnormCon env x)) of
4619 (L'.CKApp (f, _), L'.CRecord (k, xcs)) =>
4620 (case #1 (hnormCon env f) of
4621 L'.CModProj (top_n', [], "folder") =>
4622 if top_n' = top_n then
4623 let
4624 val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc)
4625 val e = (L'.EKApp (e, k), loc)
4626
4627 val (folder, _) = foldr (fn ((x, c), (folder, xcs)) =>
4628 let
4629 val e = (L'.EModProj (top_n, ["Folder"],
4630 "cons"), loc)
4631 val e = (L'.EKApp (e, k), loc)
4632 val e = (L'.ECApp (e,
4633 (L'.CRecord (k, xcs),
4634 loc)), loc)
4635 val e = (L'.ECApp (e, x), loc)
4636 val e = (L'.ECApp (e, c), loc)
4637 val e = (L'.EApp (e, folder), loc)
4638 in
4639 (e, (x, c) :: xcs)
4640 end)
4641 (e, []) xcs
4642 in
4643 (r := SOME folder;
4644 (NONE, true))
4645 end
4646 else
4647 default ()
4648 | _ => default ())
4649 | _ => default ())
4650
4651 | L'.TRecord c' =>
4652 (case #1 (hnormCon env c') of
4653 L'.CRecord (_, xts) =>
4654 let
4655 val witnesses = map (fn (x, t) =>
4656 let
4657 val r = ref NONE
4658 val (opt, _) = resolver r t
4659 in
4660 case opt of
4661 SOME _ => NONE
4662 | NONE =>
4663 case !r of
4664 NONE => NONE
4665 | SOME e =>
4666 SOME (x, e, t)
4667 end) xts
4668 in
4669 if List.all Option.isSome witnesses then
4670 (r := SOME (L'.ERecord (map valOf witnesses), loc);
4671 (NONE, true))
4672 else
4673 (SOME g, solved)
4674 end
4675 | _ => (SOME g, solved))
4676
4677 | _ => default ()
4678 end
4609 in 4679 in
4610 case resolveClass env c of 4680 resolver r c
4611 SOME e => (r := SOME e;
4612 (NONE, true))
4613 | NONE =>
4614 case #1 (hnormCon env c) of
4615 L'.CApp (f, x) =>
4616 (case (#1 (hnormCon env f), #1 (hnormCon env x)) of
4617 (L'.CKApp (f, _), L'.CRecord (k, xcs)) =>
4618 (case #1 (hnormCon env f) of
4619 L'.CModProj (top_n', [], "folder") =>
4620 if top_n' = top_n then
4621 let
4622 val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc)
4623 val e = (L'.EKApp (e, k), loc)
4624
4625 val (folder, _) = foldr (fn ((x, c), (folder, xcs)) =>
4626 let
4627 val e = (L'.EModProj (top_n, ["Folder"],
4628 "cons"), loc)
4629 val e = (L'.EKApp (e, k), loc)
4630 val e = (L'.ECApp (e,
4631 (L'.CRecord (k, xcs),
4632 loc)), loc)
4633 val e = (L'.ECApp (e, x), loc)
4634 val e = (L'.ECApp (e, c), loc)
4635 val e = (L'.EApp (e, folder), loc)
4636 in
4637 (e, (x, c) :: xcs)
4638 end)
4639 (e, []) xcs
4640 in
4641 (r := SOME folder;
4642 (NONE, true))
4643 end
4644 else
4645 default ()
4646 | _ => default ())
4647 | _ => default ())
4648 | _ => default ()
4649 end) 4681 end)
4650 false gs 4682 false gs
4651 in 4683 in
4652 case (gs, solved) of 4684 case (gs, solved) of
4653 ([], _) => () 4685 ([], _) => ()
4683 | TypeClass (env, c, r, loc) => 4715 | TypeClass (env, c, r, loc) =>
4684 let 4716 let
4685 val c = normClassKey env c 4717 val c = normClassKey env c
4686 in 4718 in
4687 case resolveClass env c of 4719 case resolveClass env c of
4688 SOME _ => () 4720 SOME e => r := SOME e
4689 | NONE => expError env (Unresolvable (loc, c)) 4721 | NONE => expError env (Unresolvable (loc, c))
4690 end) 4722 end)
4691 gs) 4723 gs)
4692 end 4724 end
4693 in 4725 in