Mercurial > urweb

comparison src/elaborate.sml @ 2092:d4eb9b6729f8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Another try at a proper fix for constraint matching in subsignature checking
author Adam Chlipala <adam@chlipala.net>
date Tue, 23 Dec 2014 11:23:27 -0500
parents 834b438d57f3
children 0d898b086bbe
comparison
equal deleted inserted replaced
2091:35c1341b0179 2092:d4eb9b6729f8
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 | _ => false
2047 end
2048 in
2049 ces
2050 end
2051
2017 2052
2018 fun elabExp (env, denv) (eAll as (e, loc)) = 2053 fun elabExp (env, denv) (eAll as (e, loc)) =
2019 let 2054 let
2020 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*) 2055 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*)
2021 (*val befor = Time.now ()*) 2056 (*val befor = Time.now ()*)
3018 (L'.SgnError, _) => () 3053 (L'.SgnError, _) => ()
3019 | (_, L'.SgnError) => () 3054 | (_, L'.SgnError) => ()
3020 3055
3021 | (L'.SgnConst sgis1, L'.SgnConst sgis2) => 3056 | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
3022 let 3057 let
3023 (* This reshuffling was added to avoid some unfortunate unification behavior. 3058 (*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), 3059 ("sgn2", p_sgn env sgn2),
3044 ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)), 3060 ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)),
3045 ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*) 3061 ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*)
3046 3062
3047 fun cpart n = IM.find (!counterparts, n) 3063 fun cpart n = IM.find (!counterparts, n)
3368 3384
3369 | L'.SgiConstraint (c2, d2) => 3385 | L'.SgiConstraint (c2, d2) =>
3370 seek (fn (env, sgi1All as (sgi1, loc)) => 3386 seek (fn (env, sgi1All as (sgi1, loc)) =>
3371 case sgi1 of 3387 case sgi1 of
3372 L'.SgiConstraint (c1, d1) => 3388 L'.SgiConstraint (c1, d1) =>
3373 if consEq env loc (c1, c2) 3389 (* It's important to do only simple equality checking here,
3374 andalso consEq env loc (d1, d2) then 3390 * with no unification, because constraints are unnamed.
3391 * It's too easy to pick the wrong pair to unify! *)
3392 if consEqSimple env (c1, c2)
3393 andalso consEqSimple env (d1, d2) then
3375 SOME env 3394 SOME env
3376 else 3395 else
3377 NONE 3396 NONE
3378 | _ => NONE) 3397 | _ => NONE)
3379 3398