Mercurial > urweb

comparison src/elaborate.sml @ 1662:edf86cef0dba

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Make wildification a bit smarter about ordering of new wildcard declarations
author Adam Chlipala <adam@chlipala.net>
date Sat, 07 Jan 2012 11:01:21 -0500
parents b46c93ce7be2
children 64c1e65c2365
comparison
equal deleted inserted replaced
1661:28b9b3d9414f 1662:edf86cef0dba
3643 | _ => nd) 3643 | _ => nd)
3644 nd ds 3644 nd ds
3645 3645
3646 val nd = removeUsed (nd, ds) 3646 val nd = removeUsed (nd, ds)
3647 3647
3648 (* Among the declarations present explicitly in the program, find the last constructor or constraint declaration.
3649 * The new constructor/constraint declarations that we add may safely be put after that point. *)
3650 fun findLast (ds, acc) =
3651 case ds of
3652 [] => ([], acc)
3653 | (d : L.decl) :: ds' =>
3654 let
3655 val isCony = case #1 d of
3656 L.DCon _ => true
3657 | L.DDatatype _ => true
3658 | L.DDatatypeImp _ => true
3659 | L.DStr _ => true
3660 | L.DConstraint _ => true
3661 | L.DClass _ => true
3662 | _ => false
3663 in
3664 if isCony then
3665 (ds, acc)
3666 else
3667 findLast (ds', d :: acc)
3668 end
3669
3670 val (dPrefix, dSuffix) = findLast (rev ds, [])
3671
3648 fun extend (env, nd, ds) = 3672 fun extend (env, nd, ds) =
3649 let 3673 let
3650 val ds' = List.mapPartial (fn (env', (c1, c2), loc) => 3674 val ds' = List.mapPartial (fn (env', (c1, c2), loc) =>
3651 case (decompileCon env' c1, decompileCon env' c2) of 3675 case (decompileCon env' c1, decompileCon env' c2) of
3652 (SOME c1, SOME c2) => 3676 (SOME c1, SOME c2) =>
3688 | SOME (env, nd') => 3712 | SOME (env, nd') =>
3689 (L.DStr (x, s, (L.StrConst (extend (env, nd', ds')), loc')), loc)) 3713 (L.DStr (x, s, (L.StrConst (extend (env, nd', ds')), loc')), loc))
3690 | d => d) ds 3714 | d => d) ds
3691 end 3715 end
3692 in 3716 in
3693 (L.StrConst (extend (env, nd, ds)), #2 str) 3717 (L.StrConst (extend (env, nd, rev dPrefix) @ dSuffix), #2 str)
3694 end 3718 end
3695 | _ => str) 3719 | _ => str)
3696 | _ => str 3720 | _ => str
3697 3721
3698 and elabDecl (dAll as (d, loc), (env, denv, gs)) = 3722 and elabDecl (dAll as (d, loc), (env, denv, gs)) =