Every GenericCtx stores binders (#458)

* Every GenericCtx stores binders

* Add names to environment

* Rename Binder::typ to Binder::content

lang/ast/src/ctx/def.rs

@@ -4,10 +4,12 @@ use derivative::Derivative;
 
 use crate::{Idx, Lvl, Var};
 
+use super::values::Binder;
+
 #[derive(Debug, Clone, Default, Derivative)]
 #[derivative(Eq, PartialEq, Hash)]
 pub struct GenericCtx<T> {
-    pub bound: Vec<Vec<T>>,
+    pub bound: Vec<Vec<Binder<T>>>,
 }
 
 impl<T> GenericCtx<T> {
@@ -23,7 +25,7 @@ impl<T> GenericCtx<T> {
         Self { bound: vec![] }
     }
 
-    pub fn iter(&self) -> impl Iterator<Item = &[T]> {
+    pub fn iter(&self) -> impl Iterator<Item = &[Binder<T>]> {
         self.bound.iter().map(|inner| &inner[..])
     }
 
@@ -53,8 +55,8 @@ impl<T> GenericCtx<T> {
     }
 }
 
-impl<T> From<Vec<Vec<T>>> for GenericCtx<T> {
-    fn from(value: Vec<Vec<T>>) -> Self {
+impl<T> From<Vec<Vec<Binder<T>>>> for GenericCtx<T> {
+    fn from(value: Vec<Vec<Binder<T>>>) -> Self {
         GenericCtx { bound: value }
     }
 }

lang/ast/src/ctx/levels.rs

@@ -15,7 +15,7 @@ fn separated<I: IntoIterator<Item = String>>(s: &str, iter: I) -> String {
     vec.join(s)
 }
 
-pub type LevelCtx = GenericCtx<VarBind>;
+pub type LevelCtx = GenericCtx<()>;
 
 impl LevelCtx {
     pub fn append(&self, other: &LevelCtx) -> Self {
@@ -38,13 +38,16 @@ impl LevelCtx {
 
 impl From<Vec<Vec<Param>>> for LevelCtx {
     fn from(value: Vec<Vec<Param>>) -> Self {
-        let bound = value.into_iter().map(|v| v.into_iter().map(|p| p.name).collect()).collect();
+        let bound = value
+            .into_iter()
+            .map(|v| v.into_iter().map(|p| Binder { name: p.name, content: () }).collect())
+            .collect();
         Self { bound }
     }
 }
 
 impl Context for LevelCtx {
-    type Elem = VarBind;
+    type Elem = Binder<()>;
 
     fn push_telescope(&mut self) {
         self.bound.push(Vec::new());
@@ -73,36 +76,54 @@ impl Context for LevelCtx {
     }
 }
 
+impl From<Vec<Vec<VarBind>>> for LevelCtx {
+    fn from(value: Vec<Vec<VarBind>>) -> Self {
+        let bound = value
+            .into_iter()
+            .map(|v| v.into_iter().map(|b| Binder { name: b.clone(), content: () }).collect())
+            .collect();
+        Self { bound }
+    }
+}
+
 impl ContextElem<LevelCtx> for VarBind {
     fn as_element(&self) -> <LevelCtx as Context>::Elem {
-        self.clone()
+        Binder { name: self.clone(), content: () }
     }
 }
 
-impl ContextElem<LevelCtx> for &Binder {
+impl ContextElem<LevelCtx> for &Binder<()> {
     fn as_element(&self) -> <LevelCtx as Context>::Elem {
-        self.name.clone()
+        Binder { name: self.name.clone(), content: () }
     }
 }
 
 impl ContextElem<LevelCtx> for &Param {
     fn as_element(&self) -> <LevelCtx as Context>::Elem {
-        self.name.clone()
+        Binder { name: self.name.clone(), content: () }
     }
 }
 
 impl ContextElem<LevelCtx> for &ParamInst {
     fn as_element(&self) -> <LevelCtx as Context>::Elem {
-        self.name.clone()
+        Binder { name: self.name.clone(), content: () }
     }
 }
 
 impl ContextElem<LevelCtx> for &Option<Motive> {
     fn as_element(&self) -> <LevelCtx as Context>::Elem {
-        match self {
+        let name = match self {
             Some(m) => m.param.name.clone(),
             None => VarBind::Wildcard { span: None },
-        }
+        };
+        Binder { name, content: () }
+    }
+}
+
+impl ContextElem<LevelCtx> for &SelfParam {
+    fn as_element(&self) -> <LevelCtx as Context>::Elem {
+        let name = self.name.clone().unwrap_or(VarBind::Wildcard { span: None });
+        Binder { name, content: () }
     }
 }
 

lang/ast/src/ctx/values.rs

@@ -11,14 +11,16 @@ use crate::*;
 
 use super::{Context, ContextElem, GenericCtx, LevelCtx};
 
-pub type TypeCtx = GenericCtx<Binder>;
+pub type TypeCtx = GenericCtx<Box<Exp>>;
 
 impl TypeCtx {
     pub fn levels(&self) -> LevelCtx {
         let bound: Vec<Vec<_>> = self
             .bound
             .iter()
-            .map(|inner| inner.iter().map(|b| b.name.to_owned()).collect())
+            .map(|inner| {
+                inner.iter().map(|b| Binder { name: b.name.to_owned(), content: () }).collect()
+            })
             .collect();
         LevelCtx::from(bound)
     }
@@ -43,7 +45,10 @@ impl TypeCtx {
             .bound
             .iter()
             .map(|stack| {
-                stack.iter().map(|b| Ok(Binder { name: b.name.clone(), typ: f(&b.typ)? })).collect()
+                stack
+                    .iter()
+                    .map(|b| Ok(Binder { name: b.name.clone(), content: f(&b.content)? }))
+                    .collect()
             })
             .collect();
 
@@ -52,7 +57,7 @@ impl TypeCtx {
 }
 
 impl Context for TypeCtx {
-    type Elem = Binder;
+    type Elem = Binder<Box<Exp>>;
 
     fn lookup<V: Into<Var>>(&self, idx: V) -> Self::Elem {
         let lvl = self.var_to_lvl(idx.into());
@@ -85,7 +90,7 @@ impl Context for TypeCtx {
     }
 }
 
-impl ContextElem<TypeCtx> for &Binder {
+impl ContextElem<TypeCtx> for &Binder<Box<Exp>> {
     fn as_element(&self) -> <TypeCtx as Context>::Elem {
         (*self).clone()
     }
@@ -95,21 +100,21 @@ impl Print for TypeCtx {
     fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
         let iter = self.iter().map(|ctx| {
             alloc
-                .intersperse(ctx.iter().map(|b| b.typ.print(cfg, alloc)), alloc.text(COMMA))
+                .intersperse(ctx.iter().map(|b| b.content.print(cfg, alloc)), alloc.text(COMMA))
                 .brackets()
         });
         alloc.intersperse(iter, alloc.text(COMMA)).brackets()
     }
 }
 
-#[derive(Debug, Clone)]
-pub struct Binder {
+#[derive(Debug, Clone, Hash, PartialEq, Eq)]
+pub struct Binder<T> {
     pub name: VarBind,
-    pub typ: Box<Exp>,
+    pub content: T,
 }
 
-impl Shift for Binder {
+impl<T: Shift> Shift for Binder<T> {
     fn shift_in_range<R: ShiftRange>(&mut self, range: &R, by: (isize, isize)) {
-        self.typ.shift_in_range(range, by);
+        self.content.shift_in_range(range, by);
     }
 }

lang/driver/src/info/data.rs

@@ -21,14 +21,14 @@ impl From<TypeCtx> for Ctx {
     }
 }
 
-impl From<TypeCtxBinder> for Binder {
-    fn from(binder: TypeCtxBinder) -> Self {
+impl From<TypeCtxBinder<Box<ast::Exp>>> for Binder {
+    fn from(binder: TypeCtxBinder<Box<ast::Exp>>) -> Self {
         match binder.name {
             ast::VarBind::Var { id, .. } => {
-                Binder::Var { name: id, typ: binder.typ.print_to_string(None) }
+                Binder::Var { name: id, typ: binder.content.print_to_string(None) }
             }
             ast::VarBind::Wildcard { .. } => {
-                Binder::Wildcard { typ: binder.typ.print_to_string(None) }
+                Binder::Wildcard { typ: binder.content.print_to_string(None) }
             }
         }
     }

lang/elaborator/src/conversion_checking/mod.rs

@@ -125,11 +125,11 @@ mod test {
         let ctx = vec![vec![
             Binder {
                 name: VarBind::Var { span: None, id: "a".to_string() },
-                typ: Box::new(TypeUniv { span: None }.into()),
+                content: Box::new(TypeUniv { span: None }.into()),
             },
             Binder {
                 name: VarBind::Var { span: None, id: "v".to_string() },
-                typ: Box::new(
+                content: Box::new(
                     Variable {
                         span: None,
                         idx: Idx { fst: 0, snd: 1 },
@@ -163,11 +163,11 @@ mod test {
         let ctx = vec![vec![
             Binder {
                 name: VarBind::Var { span: None, id: "a".to_string() },
-                typ: Box::new(TypeUniv { span: None }.into()),
+                content: Box::new(TypeUniv { span: None }.into()),
             },
             Binder {
                 name: VarBind::Var { span: None, id: "v'".to_string() },
-                typ: Box::new(
+                content: Box::new(
                     Variable {
                         span: None,
                         idx: Idx { fst: 0, snd: 2 },
@@ -179,7 +179,7 @@ mod test {
             },
             Binder {
                 name: VarBind::Var { span: None, id: "v".to_string() },
-                typ: Box::new(
+                content: Box::new(
                     Variable {
                         span: None,
                         idx: Idx { fst: 0, snd: 2 },

lang/elaborator/src/normalizer/env.rs

@@ -1,7 +1,7 @@
 use ast::{Shift, ShiftRange, VarBound};
 use pretty::DocAllocator;
 
-use ast::ctx::values::TypeCtx;
+use ast::ctx::values::{Binder, TypeCtx};
 use ast::ctx::{map_idx::*, GenericCtx};
 use ast::ctx::{Context, ContextElem, LevelCtx};
 use ast::{Idx, Var};
@@ -17,7 +17,7 @@ pub struct Env {
 }
 
 impl Context for Env {
-    type Elem = Box<Val>;
+    type Elem = Binder<Box<Val>>;
 
     fn lookup<V: Into<Var>>(&self, idx: V) -> Self::Elem {
         let lvl = self.bound_vars.var_to_lvl(idx.into());
@@ -51,7 +51,7 @@ impl Context for Env {
     }
 }
 
-impl ContextElem<Env> for &Box<Val> {
+impl ContextElem<Env> for Binder<Box<Val>> {
     fn as_element(&self) -> <Env as Context>::Elem {
         (*self).clone()
     }
@@ -63,6 +63,15 @@ impl Env {
     }
 
     pub fn from_vec(bound: Vec<Vec<Box<Val>>>) -> Self {
+        let bound: Vec<Vec<_>> = bound
+            .into_iter()
+            .map(|inner| {
+                inner
+                    .into_iter()
+                    .map(|v| Binder { name: ast::VarBind::Wildcard { span: None }, content: v })
+                    .collect()
+            })
+            .collect();
         Self { bound_vars: GenericCtx::from(bound) }
     }
 
@@ -72,7 +81,7 @@ impl Env {
     {
         for outer in self.bound_vars.bound.iter_mut() {
             for inner in outer {
-                f(inner)
+                f(&mut inner.content)
             }
         }
     }
@@ -139,7 +148,7 @@ impl Print for Env {
     ) -> printer::Builder<'a> {
         let iter = self.bound_vars.iter().map(|ctx| {
             alloc
-                .intersperse(ctx.iter().map(|typ| typ.print(cfg, alloc)), alloc.text(COMMA))
+                .intersperse(ctx.iter().map(|v| v.content.print(cfg, alloc)), alloc.text(COMMA))
                 .brackets()
         });
         alloc.intersperse(iter, alloc.text(COMMA)).brackets()