Remove Context trait (#462)

* Remove Context trait

* ContextElem -> AsBinder

* Improve docs for BindContext

* Remove Context trait for good

lang/ast/src/ctx/def.rs

@@ -14,6 +14,17 @@ pub struct GenericCtx<T> {
     pub bound: Vec<Vec<Binder<T>>>,
 }
 
+impl<T: Clone> GenericCtx<T> {
+    pub fn lookup<V: Into<Var>>(&self, idx: V) -> Binder<T> {
+        let lvl = self.var_to_lvl(idx.into());
+        self.bound
+            .get(lvl.fst)
+            .and_then(|ctx| ctx.get(lvl.snd))
+            .unwrap_or_else(|| panic!("Unbound variable {lvl}"))
+            .clone()
+    }
+}
+
 impl<T> GenericCtx<T> {
     pub fn len(&self) -> usize {
         self.bound.len()
@@ -58,6 +69,27 @@ impl<T> GenericCtx<T> {
 }
 
 impl<T: Shift> GenericCtx<T> {
+    fn push_telescope(&mut self) {
+        self.shift(&(0..), (1, 0));
+        self.bound.push(vec![]);
+    }
+
+    fn pop_telescope(&mut self) {
+        self.bound.pop().unwrap();
+        self.shift(&(0..), (-1, 0));
+    }
+
+    fn push_binder(&mut self, elem: Binder<T>) {
+        self.bound.last_mut().expect("Cannot push without calling level_inc_fst first").push(elem);
+        self.shift_at_lvl(&(0..1), self.bound.len() - 1, (0, 1));
+    }
+
+    fn pop_binder(&mut self, _elem: Binder<T>) {
+        let err = "Cannot pop from empty context";
+        self.bound.last_mut().expect(err).pop().expect(err);
+        self.shift_at_lvl(&(0..1), self.bound.len() - 1, (0, -1));
+    }
+
     pub fn shift<R: ShiftRange>(&mut self, range: &R, by: (isize, isize)) {
         for lvl in 0..self.bound.len() {
             self.shift_at_lvl(range, lvl, by)
@@ -98,84 +130,27 @@ impl<T: Print> Print for GenericCtx<T> {
     }
 }
 
-impl<T: Shift + Clone> Context for GenericCtx<T> {
-    type Elem = Binder<T>;
-
-    fn lookup<V: Into<Var>>(&self, idx: V) -> Self::Elem {
-        let lvl = self.var_to_lvl(idx.into());
-        self.bound
-            .get(lvl.fst)
-            .and_then(|ctx| ctx.get(lvl.snd))
-            .unwrap_or_else(|| panic!("Unbound variable {lvl}"))
-            .clone()
-    }
-
-    fn push_telescope(&mut self) {
-        self.shift(&(0..), (1, 0));
-        self.bound.push(vec![]);
-    }
-
-    fn pop_telescope(&mut self) {
-        self.bound.pop().unwrap();
-        self.shift(&(0..), (-1, 0));
-    }
-
-    fn push_binder(&mut self, elem: Self::Elem) {
-        self.bound.last_mut().expect("Cannot push without calling level_inc_fst first").push(elem);
-        self.shift_at_lvl(&(0..1), self.bound.len() - 1, (0, 1));
-    }
-
-    fn pop_binder(&mut self, _elem: Self::Elem) {
-        let err = "Cannot pop from empty context";
-        self.bound.last_mut().expect(err).pop().expect(err);
-        self.shift_at_lvl(&(0..1), self.bound.len() - 1, (0, -1));
-    }
-}
-
-/// Defines the interface of a variable context
-pub trait Context: Sized {
-    /// The type of elements that are stored in the context
-    type Elem: Clone;
-
-    /// Get the element bound at `var`
-    fn lookup<V: Into<Var> + std::fmt::Debug>(&self, var: V) -> Self::Elem;
-
-    /// Add a new telescope to the context
-    /// This function is run if a new list of binders should be pushed to the context
-    fn push_telescope(&mut self);
-
-    /// Remove a telescope from the context
-    /// Function that is run if the most-recently pushed list of binders should be unbound from the context
-    fn pop_telescope(&mut self);
-
-    /// Push a binder into the most-recently pushed telescope
-    fn push_binder(&mut self, elem: Self::Elem);
-
-    /// Pop a binder from the most-recently pushed telescope
-    fn pop_binder(&mut self, elem: Self::Elem);
-}
-
-/// Interface to bind variables to anything that has a `Context`
+/// Interface to bind variables to anything that has a `GenericCtx`.
 ///
 /// There are two ways to use this trait.
 ///
-/// Case 1: You have a type that implements `Context`.
-/// Then, a blanket impl ensures that this type also implements `BindContext`.
+/// Case 1: It is implemented for `GenericCtx`.
 ///
-/// Case 2: You have a type that has a field which implements `Context`.
+/// Case 2: You have a type that has a field of type `GenericCtx`.
 /// Then, only implement the `ctx_mut` method for `BindContext` and return the field that implements `Context`.
 /// Do not override the default implementations for the `bind_*` methods.
 ///
 /// In both cases, `BindContext` will provide a safe interface to bind variables and telescopes.
 pub trait BindContext: Sized {
-    type Ctx: Context;
+    type Content: Shift + Clone;
 
-    fn ctx_mut(&mut self) -> &mut Self::Ctx;
+    /// Get a mutable reference to the context
+    fn ctx_mut(&mut self) -> &mut GenericCtx<Self::Content>;
 
-    /// Bind a single element
+    /// Bind a single binder as a one-element telescope
     fn bind_single<T, O, F>(&mut self, elem: T, f: F) -> O
     where
-        T: ContextElem<Self::Ctx>,
+        T: AsBinder<Self::Content>,
         F: FnOnce(&mut Self) -> O,
     {
         self.bind_iter([elem].into_iter(), f)
@@ -184,13 +159,22 @@ pub trait BindContext: Sized {
     /// Bind an iterator `iter` of binders
     fn bind_iter<T, I, O, F>(&mut self, iter: I, f: F) -> O
     where
-        T: ContextElem<Self::Ctx>,
+        T: AsBinder<Self::Content>,
         I: Iterator<Item = T>,
         F: FnOnce(&mut Self) -> O,
     {
-        self.bind_fold(iter, (), |_ctx, (), x| x.as_element(), |ctx, ()| f(ctx))
+        self.bind_fold(iter, (), |_ctx, (), x| x.as_binder(), |ctx, ()| f(ctx))
     }
 
+    /// Bind a telescope, binder by binder and simultaneously fold over the binders
+    ///
+    /// Parameters:
+    /// * `iter`: An iterator of elements to bind
+    /// * `acc`: Initial fold accumulator
+    /// * `f_acc`: Function called on each element in `iter`
+    ///            The return value is the binder to bind.
+    ///            The function can mutate the accumulator.
+    /// * `f_inner`: Function called on a context where all binders have been bound
     fn bind_fold<T, I: Iterator<Item = T>, O1, O2, F1, F2>(
         &mut self,
         iter: I,
@@ -199,7 +183,7 @@ pub trait BindContext: Sized {
         f_inner: F2,
     ) -> O2
     where
-        F1: Fn(&mut Self, &mut O1, T) -> <Self::Ctx as Context>::Elem,
+        F1: Fn(&mut Self, &mut O1, T) -> Binder<Self::Content>,
         F2: FnOnce(&mut Self, O1) -> O2,
     {
         self.bind_fold_failable(
@@ -211,6 +195,7 @@ pub trait BindContext: Sized {
         .unwrap()
     }
 
+    /// Like `bind_fold`, but allows the accumulator function `f_acc` to fail
     fn bind_fold_failable<T, I: Iterator<Item = T>, O1, O2, F1, F2, E>(
         &mut self,
         iter: I,
@@ -219,7 +204,7 @@ pub trait BindContext: Sized {
         f_inner: F2,
     ) -> Result<O2, E>
     where
-        F1: Fn(&mut Self, &mut O1, T) -> Result<<Self::Ctx as Context>::Elem, E>,
+        F1: Fn(&mut Self, &mut O1, T) -> Result<Binder<Self::Content>, E>,
         F2: FnOnce(&mut Self, O1) -> O2,
     {
         fn bind_inner<This: BindContext, T, I: Iterator<Item = T>, O1, O2, F1, F2, E>(
@@ -230,11 +215,7 @@ pub trait BindContext: Sized {
             f_inner: F2,
         ) -> Result<O2, E>
         where
-            F1: Fn(
-                &mut This,
-                &mut O1,
-                T,
-            ) -> Result<<<This as BindContext>::Ctx as Context>::Elem, E>,
+            F1: Fn(&mut This, &mut O1, T) -> Result<Binder<<This as BindContext>::Content>, E>,
             F2: FnOnce(&mut This, O1) -> O2,
         {
             match iter.next() {
@@ -256,20 +237,20 @@ pub trait BindContext: Sized {
     }
 }
 
-pub trait ContextElem<C: Context> {
-    fn as_element(&self) -> C::Elem;
+pub trait AsBinder<T> {
+    fn as_binder(&self) -> Binder<T>;
 }
 
-impl<C: Context> BindContext for C {
-    type Ctx = Self;
+impl<T: Shift + Clone> BindContext for GenericCtx<T> {
+    type Content = T;
 
-    fn ctx_mut(&mut self) -> &mut Self::Ctx {
+    fn ctx_mut(&mut self) -> &mut GenericCtx<Self::Content> {
         self
     }
 }
 
-impl<C: Context> ContextElem<C> for C::Elem {
-    fn as_element(&self) -> C::Elem {
+impl<T: Clone> AsBinder<T> for Binder<T> {
+    fn as_binder(&self) -> Binder<T> {
         self.clone()
     }
 }

lang/ast/src/ctx/levels.rs

@@ -56,32 +56,32 @@ impl From<Vec<Vec<VarBind>>> for LevelCtx {
     }
 }
 
-impl ContextElem<LevelCtx> for VarBind {
-    fn as_element(&self) -> <LevelCtx as Context>::Elem {
+impl AsBinder<()> for VarBind {
+    fn as_binder(&self) -> Binder<()> {
         Binder { name: self.clone(), content: () }
     }
 }
 
-impl ContextElem<LevelCtx> for &Binder<()> {
-    fn as_element(&self) -> <LevelCtx as Context>::Elem {
+impl AsBinder<()> for &Binder<()> {
+    fn as_binder(&self) -> Binder<()> {
         Binder { name: self.name.clone(), content: () }
     }
 }
 
-impl ContextElem<LevelCtx> for &Param {
-    fn as_element(&self) -> <LevelCtx as Context>::Elem {
+impl AsBinder<()> for &Param {
+    fn as_binder(&self) -> Binder<()> {
         Binder { name: self.name.clone(), content: () }
     }
 }
 
-impl ContextElem<LevelCtx> for &ParamInst {
-    fn as_element(&self) -> <LevelCtx as Context>::Elem {
+impl AsBinder<()> for &ParamInst {
+    fn as_binder(&self) -> Binder<()> {
         Binder { name: self.name.clone(), content: () }
     }
 }
 
-impl ContextElem<LevelCtx> for &Option<Motive> {
-    fn as_element(&self) -> <LevelCtx as Context>::Elem {
+impl AsBinder<()> for &Option<Motive> {
+    fn as_binder(&self) -> Binder<()> {
         let name = match self {
             Some(m) => m.param.name.clone(),
             None => VarBind::Wildcard { span: None },
@@ -90,8 +90,8 @@ impl ContextElem<LevelCtx> for &Option<Motive> {
     }
 }
 
-impl ContextElem<LevelCtx> for &SelfParam {
-    fn as_element(&self) -> <LevelCtx as Context>::Elem {
+impl AsBinder<()> for &SelfParam {
+    fn as_binder(&self) -> Binder<()> {
         let name = self.name.clone().unwrap_or(VarBind::Wildcard { span: None });
         Binder { name, content: () }
     }

lang/ast/src/ctx/values.rs

@@ -5,7 +5,7 @@
 use crate::traits::Shift;
 use crate::*;
 
-use super::{Context, ContextElem, GenericCtx, LevelCtx};
+use super::{GenericCtx, LevelCtx};
 
 pub type TypeCtx = GenericCtx<Box<Exp>>;
 
@@ -40,12 +40,6 @@ impl TypeCtx {
     }
 }
 
-impl ContextElem<TypeCtx> for &Binder<Box<Exp>> {
-    fn as_element(&self) -> <TypeCtx as Context>::Elem {
-        (*self).clone()
-    }
-}
-
 #[derive(Debug, Clone, Hash, PartialEq, Eq)]
 pub struct Binder<T> {
     pub name: VarBind,

lang/elaborator/src/typechecker/ctx.rs

@@ -7,7 +7,7 @@ use std::rc::Rc;
 use crate::normalizer::env::{Env, ToEnv};
 use crate::normalizer::normalize::Normalize;
 use ast::ctx::values::TypeCtx;
-use ast::ctx::{BindContext, Context, LevelCtx};
+use ast::ctx::{BindContext, LevelCtx};
 use ast::*;
 use printer::Print;
 
@@ -58,9 +58,9 @@ impl ContextSubstExt for Ctx {
 }
 
 impl BindContext for Ctx {
-    type Ctx = TypeCtx;
+    type Content = Box<Exp>;
 
-    fn ctx_mut(&mut self) -> &mut Self::Ctx {
+    fn ctx_mut(&mut self) -> &mut TypeCtx {
         &mut self.vars
     }
 }

lang/elaborator/src/typechecker/exprs/local_match.rs

@@ -51,7 +51,7 @@ impl CheckInfer for LocalMatch {
                 let self_binder = Binder { name: param.name.clone(), content: self_t_nf.clone() };
 
                 // Typecheck the motive
-                let ret_typ_out = ctx.bind_single(&self_binder, |ctx| {
+                let ret_typ_out = ctx.bind_single(self_binder.clone(), |ctx| {
                     ret_typ.check(ctx, &Box::new(TypeUniv::new().into()))
                 })?;
 
@@ -71,7 +71,7 @@ impl CheckInfer for LocalMatch {
                 let motive_t_nf = motive_t.normalize(&ctx.type_info_table, &mut ctx.env())?;
                 convert(ctx.vars.clone(), &mut ctx.meta_vars, motive_t_nf, t, span)?;
 
-                body_t = ctx.bind_single(&self_binder, |ctx| {
+                body_t = ctx.bind_single(self_binder.clone(), |ctx| {
                     ret_typ.normalize(&ctx.type_info_table, &mut ctx.env())
                 })?;
                 motive_out = Some(Motive {

lang/lowering/src/ctx.rs

@@ -144,9 +144,9 @@ impl Ctx {
 }
 
 impl BindContext for Ctx {
-    type Ctx = LevelCtx;
+    type Content = ();
 
-    fn ctx_mut(&mut self) -> &mut Self::Ctx {
+    fn ctx_mut(&mut self) -> &mut LevelCtx {
         &mut self.binders
     }
 }

lang/transformations/src/lifting/fv.rs

@@ -330,9 +330,9 @@ impl USTVisitor<'_> {
 }
 
 impl BindContext for USTVisitor<'_> {
-    type Ctx = LevelCtx;
+    type Content = ();
 
-    fn ctx_mut(&mut self) -> &mut Self::Ctx {
+    fn ctx_mut(&mut self) -> &mut LevelCtx {
         &mut self.lvl_ctx
     }
 }

lang/transformations/src/lifting/mod.rs

@@ -61,9 +61,9 @@ struct Ctx {
 }
 
 impl BindContext for Ctx {
-    type Ctx = LevelCtx;
+    type Content = ();
 
-    fn ctx_mut(&mut self) -> &mut Self::Ctx {
+    fn ctx_mut(&mut self) -> &mut LevelCtx {
         &mut self.ctx
     }
 }

lang/transformations/src/renaming/ctx.rs

@@ -15,9 +15,9 @@ impl From<GenericCtx<()>> for Ctx {
 }
 
 impl BindContext for Ctx {
-    type Ctx = LevelCtx;
+    type Content = ();
 
-    fn ctx_mut(&mut self) -> &mut Self::Ctx {
+    fn ctx_mut(&mut self) -> &mut LevelCtx {
         &mut self.binders
     }
 }