[ bind as ] Move logic to util function

src/check/rules/clause/mod.rs

@@ -13,11 +13,17 @@ mod lhs;
 mod state;
 
 /// Bind as patterns
-pub fn bind_as_pats<T>(mut tcs: TCS, asb: Vec<AsBind>, f: impl FnOnce(TCS) -> T) -> T {
+pub fn bind_as_pats<T>(mut tcs: TCS, asb: Vec<AsBind>, f: impl FnOnce(TCS) -> TCMS<T>) -> TCMS<T> {
+    let to_pop = asb.len();
     for bind in asb {
         tcs.gamma.push(bind.into());
     }
-    f(tcs)
+    let (thing, mut tcs) = f(tcs)?;
+    for _ in 0..=to_pop {
+        let len = tcs.gamma.len();
+        tcs.gamma.remove(len - 1);
+    }
+    Ok((thing, tcs))
 }
 
 /// Checking an abstract clause.
@@ -31,7 +37,6 @@ pub fn clause(tcs: TCS, cls: AbsClause, against: Term) -> TCMS<Clause> {
     let ty = lhs.ty;
     let patterns = lhs.pats;
     let has_absurd = lhs.has_absurd;
-    let to_pop = lhs.as_binds.len();
     bind_as_pats(tcs, lhs.as_binds, |mut tcs| {
         let body = if has_absurd {
             None
@@ -41,10 +46,6 @@ pub fn clause(tcs: TCS, cls: AbsClause, against: Term) -> TCMS<Clause> {
             tcs = new_tcs;
             Some(term.ast)
         };
-        for _ in 0..=to_pop {
-            let len = tcs.gamma.len();
-            tcs.gamma.remove(len - 1);
-        }
         let clause = Clause {
             pat_tele,
             patterns,