comparison src/elab_env.sml @ 825:7f871c03e3a1

Destructing local let, to the point where demo compiles
author Adam Chlipala <adamc@hcoop.net>
date Thu, 28 May 2009 12:07:05 -0400
parents e2780d2f4afc
children e571fb150a9f
comparison
equal deleted inserted replaced
824:be0988e46336 825:7f871c03e3a1
1452 case #1 (hnormSgn env sgn) of 1452 case #1 (hnormSgn env sgn) of
1453 SgnConst sgis => SOME (sgnSeekConstraints (str, sgis)) 1453 SgnConst sgis => SOME (sgnSeekConstraints (str, sgis))
1454 | SgnError => SOME [] 1454 | SgnError => SOME []
1455 | _ => NONE 1455 | _ => NONE
1456 1456
1457 fun patBinds env (p, loc) =
1458 case p of
1459 PWild => env
1460 | PVar (x, t) => pushERel env x t
1461 | PPrim _ => env
1462 | PCon (_, _, _, NONE) => env
1463 | PCon (_, _, _, SOME p) => patBinds env p
1464 | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
1465
1457 fun edeclBinds env (d, loc) = 1466 fun edeclBinds env (d, loc) =
1458 case d of 1467 case d of
1459 EDVal (x, t, _) => pushERel env x t 1468 EDVal (p, _, _) => patBinds env p
1460 | EDValRec vis => foldl (fn ((x, t, _), env) => pushERel env x t) env vis 1469 | EDValRec vis => foldl (fn ((x, t, _), env) => pushERel env x t) env vis
1461 1470
1462 fun declBinds env (d, loc) = 1471 fun declBinds env (d, loc) =
1463 case d of 1472 case d of
1464 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) 1473 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
1563 val t = (CModProj (tn, [], "css_class"), loc) 1572 val t = (CModProj (tn, [], "css_class"), loc)
1564 in 1573 in
1565 pushENamedAs env x n t 1574 pushENamedAs env x n t
1566 end 1575 end
1567 1576
1568 fun patBinds env (p, loc) =
1569 case p of
1570 PWild => env
1571 | PVar (x, t) => pushERel env x t
1572 | PPrim _ => env
1573 | PCon (_, _, _, NONE) => env
1574 | PCon (_, _, _, SOME p) => patBinds env p
1575 | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
1576
1577 end 1577 end