comparison src/elaborate.sml @ 480:40c737913075

Especialize handles records better
author Adam Chlipala <adamc@hcoop.net>
date Sat, 08 Nov 2008 16:02:59 -0500
parents 6ee1c761818f
children ae03d09043c1
comparison
equal deleted inserted replaced
479:ffa18975e661 480:40c737913075
2613 ignore (foldl folder (env, denv) sgis2) 2613 ignore (foldl folder (env, denv) sgis2)
2614 end 2614 end
2615 2615
2616 | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) => 2616 | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) =>
2617 let 2617 let
2618 val ran1 = 2618 val ran2 =
2619 if n1 = n2 then 2619 if n1 = n2 then
2620 ran1 2620 ran2
2621 else 2621 else
2622 subStrInSgn (n1, n2) ran1 2622 subStrInSgn (n2, n1) ran2
2623 in 2623 in
2624 subSgn (env, denv) dom2 dom1; 2624 subSgn (env, denv) dom2 dom1;
2625 subSgn (E.pushStrNamedAs env m2 n2 dom2, denv) ran1 ran2 2625 subSgn (E.pushStrNamedAs env m1 n1 dom2, denv) ran1 ran2
2626 end 2626 end
2627 2627
2628 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))) 2628 | _ => sgnError env (SgnWrongForm (sgn1, sgn2)))
2629 2629
2630 2630