Mercurial > urweb

comparison src/elaborate.sml @ 2226:e10881cd92da

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge.
author Ziv Scully <ziv@mit.edu>
date Fri, 27 Mar 2015 11:26:06 -0400
parents f42fea631c1d
children 010ce27228f1
comparison
equal deleted inserted replaced
2225:6262dabc08d6 2226:e10881cd92da
2012 2012
2013 fun chaseUnifs c = 2013 fun chaseUnifs c =
2014 case #1 c of 2014 case #1 c of
2015 L'.CUnif (_, _, _, _, ref (L'.Known c)) => chaseUnifs c 2015 L'.CUnif (_, _, _, _, ref (L'.Known c)) => chaseUnifs c
2016 | _ => c 2016 | _ => c
2017
2018 val consEqSimple =
2019 let
2020 fun ces env (c1 : L'.con, c2 : L'.con) =
2021 let
2022 val c1 = hnormCon env c1
2023 val c2 = hnormCon env c2
2024 in
2025 case (#1 c1, #1 c2) of
2026 (L'.CRel n1, L'.CRel n2) => n1 = n2
2027 | (L'.CNamed n1, L'.CNamed n2) =>
2028 n1 = n2 orelse
2029 (case #3 (E.lookupCNamed env n1) of
2030 SOME (L'.CNamed n2', _) => n2' = n1
2031 | _ => false)
2032 | (L'.CModProj n1, L'.CModProj n2) => n1 = n2
2033 | (L'.CApp (f1, x1), L'.CApp (f2, x2)) => ces env (f1, f2) andalso ces env (x1, x2)
2034 | (L'.CAbs (x1, k1, c1), L'.CAbs (_, _, c2)) => ces (E.pushCRel env x1 k1) (c1, c2)
2035 | (L'.CName x1, L'.CName x2) => x1 = x2
2036 | (L'.CRecord (_, xts1), L'.CRecord (_, xts2)) =>
2037 ListPair.all (fn ((x1, t1), (x2, t2)) =>
2038 ces env (x1, x2) andalso ces env (t2, t2)) (xts1, xts2)
2039 | (L'.CConcat (x1, y1), L'.CConcat (x2, y2)) =>
2040 ces env (x1, x2) andalso ces env (y1, y2)
2041 | (L'.CMap _, L'.CMap _) => true
2042 | (L'.CUnit, L'.CUnit) => true
2043 | (L'.CTuple cs1, L'.CTuple cs2) => ListPair.all (ces env) (cs1, cs2)
2044 | (L'.CProj (c1, n1), L'.CProj (c2, n2)) => ces env (c1, c2) andalso n1 = n2
2045 | (L'.CUnif (_, _, _, _, r1), L'.CUnif (_, _, _, _, r2)) => r1 = r2
2046
2047 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => ces env (d1, d2) andalso ces env (r1, r2)
2048 | (L'.TRecord c1, L'.TRecord c2) => ces env (c1, c2)
2049
2050 | _ => false
2051 end
2052 in
2053 ces
2054 end
2055
2017 2056
2018 fun elabExp (env, denv) (eAll as (e, loc)) = 2057 fun elabExp (env, denv) (eAll as (e, loc)) =
2019 let 2058 let
2020 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*) 2059 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*)
2021 (*val befor = Time.now ()*) 2060 (*val befor = Time.now ()*)
3018 (L'.SgnError, _) => () 3057 (L'.SgnError, _) => ()
3019 | (_, L'.SgnError) => () 3058 | (_, L'.SgnError) => ()
3020 3059
3021 | (L'.SgnConst sgis1, L'.SgnConst sgis2) => 3060 | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
3022 let 3061 let
3023 (* This reshuffling was added to avoid some unfortunate unification behavior. 3062 (*val () = prefaces "subSgn" [("sgn1", p_sgn env sgn1),
3024 * In particular, in sub-signature checking, constraints might be unified,
3025 * even when we don't expect them to be unifiable, deciding on bad values
3026 * for unification variables and dooming later unification.
3027 * By putting all the constraints _last_, we allow all the other unifications
3028 * to happen first, hoping that no unification variables survive to confuse
3029 * constraint unification. *)
3030
3031 val sgis2 =
3032 let
3033 val (constraints, others) = List.partition
3034 (fn (L'.SgiConstraint _, _) => true
3035 | _ => false) sgis2
3036 in
3037 case constraints of
3038 [] => sgis2
3039 | _ => others @ constraints
3040 end
3041
3042 (*val () = prefaces "subSgn" [("sgn1", p_sgn env sgn1),
3043 ("sgn2", p_sgn env sgn2), 3063 ("sgn2", p_sgn env sgn2),
3044 ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)), 3064 ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)),
3045 ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*) 3065 ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*)
3046 3066
3047 fun cpart n = IM.find (!counterparts, n) 3067 fun cpart n = IM.find (!counterparts, n)
3327 seek (fn (env, sgi1All as (sgi1, loc)) => 3347 seek (fn (env, sgi1All as (sgi1, loc)) =>
3328 case sgi1 of 3348 case sgi1 of
3329 L'.SgiStr (x', n1, sgn1) => 3349 L'.SgiStr (x', n1, sgn1) =>
3330 if x = x' then 3350 if x = x' then
3331 let 3351 let
3352 (* Don't forget to save & restore the
3353 * counterparts map around recursive calls!
3354 * Otherwise, all sorts of mayhem may result. *)
3355 val saved = !counterparts
3332 val () = subSgn' counterparts env loc sgn1 sgn2 3356 val () = subSgn' counterparts env loc sgn1 sgn2
3357 val () = counterparts := saved
3333 val env = E.pushStrNamedAs env x n1 sgn1 3358 val env = E.pushStrNamedAs env x n1 sgn1
3334 val env = if n1 = n2 then 3359 val env = if n1 = n2 then
3335 env 3360 env
3336 else 3361 else
3337 E.pushStrNamedAs env x n2 3362 E.pushStrNamedAs env x n2
3368 3393
3369 | L'.SgiConstraint (c2, d2) => 3394 | L'.SgiConstraint (c2, d2) =>
3370 seek (fn (env, sgi1All as (sgi1, loc)) => 3395 seek (fn (env, sgi1All as (sgi1, loc)) =>
3371 case sgi1 of 3396 case sgi1 of
3372 L'.SgiConstraint (c1, d1) => 3397 L'.SgiConstraint (c1, d1) =>
3373 if consEq env loc (c1, c2) 3398 (* It's important to do only simple equality checking here,
3374 andalso consEq env loc (d1, d2) then 3399 * with no unification, because constraints are unnamed.
3400 * It's too easy to pick the wrong pair to unify! *)
3401 if consEqSimple env (c1, c2)
3402 andalso consEqSimple env (d1, d2) then
3375 SOME env 3403 SOME env
3376 else 3404 else
3377 NONE 3405 NONE
3378 | _ => NONE) 3406 | _ => NONE)
3379 3407
3667 NONE => NONE 3695 NONE => NONE
3668 | SOME c' => SOME (L.TRecord c', loc)) 3696 | SOME c' => SOME (L.TRecord c', loc))
3669 3697
3670 | c => ((*Print.preface ("WTF?", p_con env (c, loc));*) NONE) 3698 | c => ((*Print.preface ("WTF?", p_con env (c, loc));*) NONE)
3671 3699
3700 fun isClassOrFolder' env (c : L'.con) =
3701 case #1 c of
3702 L'.CAbs (x, k, c) =>
3703 let
3704 val env = E.pushCRel env x k
3705
3706 fun toHead (c : L'.con) =
3707 case #1 c of
3708 L'.CApp (c, _) => toHead c
3709 | _ => isClassOrFolder env c
3710 in
3711 toHead (hnormCon env c)
3712 end
3713 | _ => isClassOrFolder env c
3714
3672 fun buildNeeded env sgis = 3715 fun buildNeeded env sgis =
3673 #1 (foldl (fn ((sgi, loc), (nd, env')) => 3716 #1 (foldl (fn ((sgi, loc), (nd, env')) =>
3674 (case sgi of 3717 (case sgi of
3675 L'.SgiCon (x, _, k, _) => naddCon (nd, x, k) 3718 L'.SgiCon (x, _, k, _) => naddCon (nd, x, k)
3676 | L'.SgiConAbs (x, _, k) => naddCon (nd, x, k) 3719 | L'.SgiConAbs (x, _, k) => naddCon (nd, x, k)
3678 | L'.SgiVal (x, _, t) => 3721 | L'.SgiVal (x, _, t) =>
3679 let 3722 let
3680 fun should t = 3723 fun should t =
3681 let 3724 let
3682 val t = normClassConstraint env' t 3725 val t = normClassConstraint env' t
3726
3727 fun shouldR c =
3728 case hnormCon env' c of
3729 (L'.CApp (f, _), _) =>
3730 (case hnormCon env' f of
3731 (L'.CApp (f, cl), loc) =>
3732 (case hnormCon env' f of
3733 (L'.CMap _, _) => isClassOrFolder' env' cl
3734 | _ => false)
3735 | _ => false)
3736 | (L'.CConcat (c1, c2), _) =>
3737 shouldR c1 orelse shouldR c2
3738 | c => false
3683 in 3739 in
3684 case #1 t of 3740 case #1 t of
3685 L'.CApp (f, _) => isClassOrFolder env' f 3741 L'.CApp (f, _) => isClassOrFolder env' f
3686 | L'.TRecord t => 3742 | L'.TRecord t => shouldR t
3687 (case hnormCon env' t of
3688 (L'.CApp (f, _), _) =>
3689 (case hnormCon env' f of
3690 (L'.CApp (f, cl), loc) =>
3691 (case hnormCon env' f of
3692 (L'.CMap _, _) => isClassOrFolder env' cl
3693 | _ => false)
3694 | _ => false)
3695 | _ => false)
3696 | _ => false 3743 | _ => false
3697 end 3744 end
3698 in 3745 in
3699 if should t then 3746 if should t then
3700 naddVal (nd, x) 3747 naddVal (nd, x)