Fix let term semantics

carcara/src/ast/tests.rs

@@ -101,8 +101,8 @@ fn test_polyeq() {
                 "(choice ((a Int)) (forall ((b Int)) (exists ((c Int)) (= a b c))))",
             ),
             (
-                "(let ((x 0) (y (+ x 2)) (z (< x y))) (and z (= x y)))",
-                "(let ((z 0) (x (+ z 2)) (y (< z x))) (and y (= z x)))",
+                "(let ((x 0)) (let ((y (+ x 2))) (let ((z (< x y))) (and z (= x y)))))",
+                "(let ((z 0)) (let ((x (+ z 2))) (let ((y (< z x))) (and y (= z x)))))",
             ),
         ],
         TestType::AlphaEquiv,

carcara/src/elaborator/polyeq.rs

@@ -149,8 +149,6 @@ impl<'a> PolyeqElaborator<'a> {
                     .map(|(name, value)| AnchorArg::Variable((name.clone(), pool.sort(value))))
                     .collect();
 
-                self.open_subproof();
-
                 // The values of the binding lists in the `let` terms may not be syntactically
                 // identical, in which case we need to prove their equality so the `bind_let` step
                 // is valid.
@@ -167,6 +165,7 @@ impl<'a> PolyeqElaborator<'a> {
                     })
                     .collect();
 
+                self.open_subproof();
                 let previous = self.create_bind_subproof(pool, (a_inner.clone(), b_inner.clone()));
                 let last_step = StepNode {
                     id: String::new(), // this will be overwritten later

carcara/src/parser/mod.rs

@@ -1334,21 +1334,29 @@ impl<'a, R: BufRead> Parser<'a, R> {
     /// consumed.
     fn parse_let_term(&mut self) -> CarcaraResult<Rc<Term>> {
         self.expect_token(Token::OpenParen)?;
-        self.state.symbol_table.push_scope();
+
+        // Since the let binding semantics is *simultaneous*, we first parse all bindings, and only
+        // then add them to the symbol table.
         let bindings = self.parse_sequence(
             |p| {
                 p.expect_token(Token::OpenParen)?;
                 let name = p.expect_symbol()?;
                 let value = p.parse_term()?;
-                let sort = p.pool.sort(&value);
-                p.insert_sorted_var((name.clone(), sort));
                 p.expect_token(Token::CloseParen)?;
                 Ok((name, value))
             },
             true,
         )?;
+
+        self.state.symbol_table.push_scope();
+        for (name, value) in &bindings {
+            let sort = self.pool.sort(value);
+            self.insert_sorted_var((name.clone(), sort));
+        }
+
         let inner = self.parse_term()?;
         self.expect_token(Token::CloseParen)?;
+
         self.state.symbol_table.pop_scope();
 
         if self.config.expand_lets {