Skip to content

Commit

Permalink
Split Ident
Browse files Browse the repository at this point in the history
  • Loading branch information
@timsueberkrueb
timsueberkrueb committed Nov 6, 2024
1 parent 314f8c1 commit ee16b2a
Show file tree
Hide file tree
Showing 40 changed files with 2,225 additions and 274 deletions.
2 changes: 1 addition & 1 deletion lang/ast/src/ctx/values.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ impl Print for TypeCtx {

#[derive(Debug, Clone)]
pub struct Binder {
pub name: Ident,
pub name: VarBind,
pub typ: Box<Exp>,
}

Expand Down
72 changes: 33 additions & 39 deletions lang/ast/src/decls.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ use printer::PrintCfg;
use url::Url;

use crate::ctx::LevelCtx;
use crate::named::Named;
use crate::identifiable::GloballyIdentifiable;
use crate::shift_and_clone;
use crate::ContainsMetaVars;
use crate::Zonk;
Expand Down Expand Up @@ -184,7 +184,7 @@ pub struct Module {
}

impl Module {
pub fn xdefs_for_type(&self, type_name: &str) -> Vec<Ident> {
pub fn xdefs_for_type(&self, type_name: &str) -> Vec<IdBind> {
let mut out = vec![];

for decl in &self.decls {
Expand All @@ -206,7 +206,7 @@ impl Module {
out
}

pub fn xtors_for_type(&self, type_name: &str) -> Vec<Ident> {
pub fn xtors_for_type(&self, type_name: &str) -> Vec<IdBind> {
let mut out = vec![];

for decl in &self.decls {
Expand All @@ -232,25 +232,25 @@ impl Module {
out
}

pub fn lookup_decl(&self, name: &Ident) -> Option<&Decl> {
self.decls.iter().find(|decl| decl.name() == name)
pub fn lookup_decl(&self, name: &IdBind) -> Option<&Decl> {
self.decls.iter().find(|decl| decl.ident() == name)
}

pub fn lookup_let(&self, name: &Ident) -> Option<&Let> {
pub fn lookup_let(&self, name: &IdBind) -> Option<&Let> {
self.decls.iter().find_map(|decl| match decl {
Decl::Let(tl_let) if tl_let.name == *name => Some(tl_let),
_ => None,
})
}

pub fn lookup_def(&self, name: &Ident) -> Option<&Def> {
pub fn lookup_def(&self, name: &IdBind) -> Option<&Def> {
self.decls.iter().find_map(|decl| match decl {
Decl::Def(def) if def.name == *name => Some(def),
_ => None,
})
}

pub fn lookup_codef(&self, name: &Ident) -> Option<&Codef> {
pub fn lookup_codef(&self, name: &IdBind) -> Option<&Codef> {
self.decls.iter().find_map(|decl| match decl {
Decl::Codef(codef) if codef.name == *name => Some(codef),
_ => None,
Expand Down Expand Up @@ -367,8 +367,8 @@ impl Decl {
}
}

impl Named for Decl {
fn name(&self) -> &Ident {
impl GloballyIdentifiable for Decl {
fn ident(&self) -> &IdBind {
match self {
Decl::Data(Data { name, .. }) => name,
Decl::Codata(Codata { name, .. }) => name,
Expand Down Expand Up @@ -435,7 +435,7 @@ impl ContainsMetaVars for Decl {
pub struct Data {
pub span: Option<Span>,
pub doc: Option<DocComment>,
pub name: Ident,
pub name: IdBind,
pub attr: Attributes,
pub typ: Box<Telescope>,
pub ctors: Vec<Ctor>,
Expand Down Expand Up @@ -503,7 +503,7 @@ impl ContainsMetaVars for Data {
pub struct Codata {
pub span: Option<Span>,
pub doc: Option<DocComment>,
pub name: Ident,
pub name: IdBind,
pub attr: Attributes,
pub typ: Box<Telescope>,
pub dtors: Vec<Dtor>,
Expand Down Expand Up @@ -571,7 +571,7 @@ impl ContainsMetaVars for Codata {
pub struct Ctor {
pub span: Option<Span>,
pub doc: Option<DocComment>,
pub name: Ident,
pub name: IdBind,
pub params: Telescope,
pub typ: TypCtor,
}
Expand Down Expand Up @@ -619,7 +619,7 @@ impl ContainsMetaVars for Ctor {
pub struct Dtor {
pub span: Option<Span>,
pub doc: Option<DocComment>,
pub name: Ident,
pub name: IdBind,
pub params: Telescope,
pub self_param: SelfParam,
pub ret_typ: Box<Exp>,
Expand Down Expand Up @@ -670,7 +670,7 @@ impl ContainsMetaVars for Dtor {
pub struct Def {
pub span: Option<Span>,
pub doc: Option<DocComment>,
pub name: Ident,
pub name: IdBind,
pub attr: Attributes,
pub params: Telescope,
pub self_param: SelfParam,
Expand Down Expand Up @@ -748,7 +748,7 @@ impl ContainsMetaVars for Def {
pub struct Codef {
pub span: Option<Span>,
pub doc: Option<DocComment>,
pub name: Ident,
pub name: IdBind,
pub attr: Attributes,
pub params: Telescope,
pub typ: TypCtor,
Expand Down Expand Up @@ -822,7 +822,7 @@ impl ContainsMetaVars for Codef {
pub struct Let {
pub span: Option<Span>,
pub doc: Option<DocComment>,
pub name: Ident,
pub name: IdBind,
pub attr: Attributes,
pub params: Telescope,
pub typ: Box<Exp>,
Expand Down Expand Up @@ -884,7 +884,7 @@ impl ContainsMetaVars for Let {
#[derive(Debug, Clone)]
pub struct SelfParam {
pub info: Option<Span>,
pub name: Option<Ident>,
pub name: Option<VarBind>,
pub typ: TypCtor,
}

Expand All @@ -893,7 +893,7 @@ impl SelfParam {
Telescope {
params: vec![Param {
implicit: false,
name: self.name.clone().unwrap_or_else(|| Ident::from_string("")),
name: self.name.clone().unwrap_or_else(|| VarBind::from_string("")),
typ: Box::new(self.typ.to_exp()),
}],
}
Expand Down Expand Up @@ -1083,12 +1083,12 @@ mod print_telescope_tests {
fn print_simple_chunk() {
let param1 = Param {
implicit: false,
name: Ident::from_string("x"),
name: VarBind::from_string("x"),
typ: Box::new(TypeUniv::new().into()),
};
let param2 = Param {
implicit: false,
name: Ident::from_string("y"),
name: VarBind::from_string("y"),
typ: Box::new(TypeUniv::new().into()),
};
let tele = Telescope { params: vec![param1, param2] };
Expand All @@ -1099,12 +1099,12 @@ mod print_telescope_tests {
fn print_simple_implicit_chunk() {
let param1 = Param {
implicit: true,
name: Ident::from_string("x"),
name: VarBind::from_string("x"),
typ: Box::new(TypeUniv::new().into()),
};
let param2 = Param {
implicit: true,
name: Ident::from_string("y"),
name: VarBind::from_string("y"),
typ: Box::new(TypeUniv::new().into()),
};
let tele = Telescope { params: vec![param1, param2] };
Expand All @@ -1115,12 +1115,12 @@ mod print_telescope_tests {
fn print_mixed_implicit_chunk_1() {
let param1 = Param {
implicit: true,
name: Ident::from_string("x"),
name: VarBind::from_string("x"),
typ: Box::new(TypeUniv::new().into()),
};
let param2 = Param {
implicit: false,
name: Ident::from_string("y"),
name: VarBind::from_string("y"),
typ: Box::new(TypeUniv::new().into()),
};
let tele = Telescope { params: vec![param1, param2] };
Expand All @@ -1131,12 +1131,12 @@ mod print_telescope_tests {
fn print_mixed_implicit_chunk_2() {
let param1 = Param {
implicit: false,
name: Ident::from_string("x"),
name: VarBind::from_string("x"),
typ: Box::new(TypeUniv::new().into()),
};
let param2 = Param {
implicit: true,
name: Ident::from_string("y"),
name: VarBind::from_string("y"),
typ: Box::new(TypeUniv::new().into()),
};
let tele = Telescope { params: vec![param1, param2] };
Expand All @@ -1147,26 +1147,26 @@ mod print_telescope_tests {
fn print_shifting_example() {
let param1 = Param {
implicit: false,
name: Ident::from_string("a"),
name: VarBind::from_string("a"),
typ: Box::new(TypeUniv::new().into()),
};
let param2 = Param {
implicit: false,
name: Ident::from_string("x"),
name: VarBind::from_string("x"),
typ: Box::new(Exp::Variable(Variable {
span: None,
idx: Idx { fst: 0, snd: 0 },
name: Ident::from_string("a"),
name: VarBound::from_string("a"),
inferred_type: None,
})),
};
let param3 = Param {
implicit: false,
name: Ident::from_string("y"),
name: VarBind::from_string("y"),
typ: Box::new(Exp::Variable(Variable {
span: None,
idx: Idx { fst: 0, snd: 1 },
name: Ident::from_string("a"),
name: VarBound::from_string("a"),
inferred_type: None,
})),
};
Expand All @@ -1184,16 +1184,10 @@ mod print_telescope_tests {
pub struct Param {
pub implicit: bool,
#[derivative(PartialEq = "ignore", Hash = "ignore")]
pub name: Ident,
pub name: VarBind,
pub typ: Box<Exp>,
}

impl Named for Param {
fn name(&self) -> &Ident {
&self.name
}
}

impl Substitutable for Param {
type Result = Param;
fn subst<S: Substitution>(&self, ctx: &mut LevelCtx, by: &S) -> Self {
Expand Down
Loading

0 comments on commit ee16b2a

Please sign in to comment.