Skip to content

Commit

Permalink
Add erased fields to ast
Browse files Browse the repository at this point in the history
  • Loading branch information
@timsueberkrueb
timsueberkrueb committed Jan 4, 2025
1 parent bdf4821 commit d06e928
Show file tree
Hide file tree
Showing 31 changed files with 389 additions and 255 deletions.
229 changes: 106 additions & 123 deletions Cargo.lock
View file

Large diffs are not rendered by default.

74 changes: 58 additions & 16 deletions lang/ast/src/decls.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -601,11 +601,13 @@ pub struct Dtor {
pub params: Telescope,
pub self_param: SelfParam,
pub ret_typ: Box<Exp>,
/// Whether the destructor is erased during compilation.
pub erased: bool,
}

impl Print for Dtor {
fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
let Dtor { span: _, doc, name, params, self_param, ret_typ } = self;
let Dtor { span: _, doc, name, params, self_param, ret_typ, erased: _ } = self;

let doc = doc.print(cfg, alloc);
let head = if self_param.is_simple() {
Expand All @@ -624,7 +626,7 @@ impl Print for Dtor {

impl Zonk for Dtor {
fn zonk(&mut self, meta_vars: &HashMap<MetaVar, MetaVarState>) -> Result<(), crate::ZonkError> {
let Dtor { span: _, doc: _, name: _, params, self_param, ret_typ } = self;
let Dtor { span: _, doc: _, name: _, params, self_param, ret_typ, erased: _ } = self;
params.zonk(meta_vars)?;
self_param.zonk(meta_vars)?;
ret_typ.zonk(meta_vars)?;
Expand All @@ -634,7 +636,7 @@ impl Zonk for Dtor {

impl ContainsMetaVars for Dtor {
fn contains_metavars(&self) -> bool {
let Dtor { span: _, doc: _, name: _, params, self_param, ret_typ } = self;
let Dtor { span: _, doc: _, name: _, params, self_param, ret_typ, erased: _ } = self;

params.contains_metavars() || self_param.contains_metavars() || ret_typ.contains_metavars()
}
Expand All @@ -654,6 +656,8 @@ pub struct Def {
pub self_param: SelfParam,
pub ret_typ: Box<Exp>,
pub cases: Vec<Case>,
/// Whether the definition is erased during compilation.
pub erased: bool,
}

impl Def {
Expand All @@ -665,13 +669,14 @@ impl Def {
params: self.params.clone(),
self_param: self.self_param.clone(),
ret_typ: self.ret_typ.clone(),
erased: self.erased,
}
}
}

impl Print for Def {
fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
let Def { span: _, doc, name, attr, params, self_param, ret_typ, cases } = self;
let Def { span: _, doc, name, attr, params, self_param, ret_typ, cases, erased: _ } = self;
if !attr.is_visible() {
return alloc.nil();
}
Expand All @@ -696,7 +701,17 @@ impl Print for Def {

impl Zonk for Def {
fn zonk(&mut self, meta_vars: &HashMap<MetaVar, MetaVarState>) -> Result<(), crate::ZonkError> {
let Def { span: _, doc: _, name: _, attr: _, params, self_param, ret_typ, cases } = self;
let Def {
span: _,
doc: _,
name: _,
attr: _,
params,
self_param,
ret_typ,
cases,
erased: _,
} = self;
params.zonk(meta_vars)?;
self_param.zonk(meta_vars)?;
ret_typ.zonk(meta_vars)?;
Expand All @@ -709,7 +724,17 @@ impl Zonk for Def {

impl ContainsMetaVars for Def {
fn contains_metavars(&self) -> bool {
let Def { span: _, doc: _, name: _, attr: _, params, self_param, ret_typ, cases } = self;
let Def {
span: _,
doc: _,
name: _,
attr: _,
params,
self_param,
ret_typ,
cases,
erased: _,
} = self;

params.contains_metavars()
|| self_param.contains_metavars()
Expand Down Expand Up @@ -805,6 +830,8 @@ pub struct Let {
pub params: Telescope,
pub typ: Box<Exp>,
pub body: Box<Exp>,
/// Whether the let binding is erased during compilation.
pub erased: bool,
}

impl Let {
Expand All @@ -816,7 +843,7 @@ impl Let {

impl Print for Let {
fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
let Let { span: _, doc, name, attr, params, typ, body } = self;
let Let { span: _, doc, name, attr, params, typ, body, erased: _ } = self;
if !attr.is_visible() {
return alloc.nil();
}
Expand All @@ -839,7 +866,7 @@ impl Print for Let {

impl Zonk for Let {
fn zonk(&mut self, meta_vars: &HashMap<MetaVar, MetaVarState>) -> Result<(), crate::ZonkError> {
let Let { span: _, doc: _, name: _, attr: _, params, typ, body } = self;
let Let { span: _, doc: _, name: _, attr: _, params, typ, body, erased: _ } = self;
params.zonk(meta_vars)?;
typ.zonk(meta_vars)?;
body.zonk(meta_vars)?;
Expand All @@ -849,7 +876,7 @@ impl Zonk for Let {

impl ContainsMetaVars for Let {
fn contains_metavars(&self) -> bool {
let Let { span: _, doc: _, name: _, attr: _, params, typ, body } = self;
let Let { span: _, doc: _, name: _, attr: _, params, typ, body, erased: _ } = self;

params.contains_metavars() || typ.contains_metavars() || body.contains_metavars()
}
Expand All @@ -873,6 +900,7 @@ impl SelfParam {
implicit: false,
name: self.name.clone().unwrap_or_else(|| VarBind::from_string("")),
typ: Box::new(self.typ.to_exp()),
erased: false,

Check warning on line 903 in lang/ast/src/decls.rs

View check run for this annotation

Codecov / codecov/patch

lang/ast/src/decls.rs#L903 

Added line #L903 was not covered by tests
}],
}
}
Expand Down Expand Up @@ -946,11 +974,12 @@ impl Telescope {
let params = self
.params
.iter()
.map(|Param { name, .. }| ParamInst {
.map(|Param { name, erased, .. }| ParamInst {
span: None,
name: name.clone(),
info: None,
typ: None,
erased: *erased,
})
.collect();
TelescopeInst { params }
Expand Down Expand Up @@ -978,7 +1007,7 @@ impl Print for Telescope {
};
// Running stands for the type and implicitness of the current "chunk" we are building.
let mut running: Option<(&Exp, bool)> = None;
for Param { implicit, name, typ } in params {
for Param { implicit, name, typ, erased: _ } in params {
match running {
// We need to shift before comparing to ensure we compare the correct De-Bruijn indices
Some((rtype, rimplicit))
Expand Down Expand Up @@ -1063,11 +1092,13 @@ mod print_telescope_tests {
implicit: false,
name: VarBind::from_string("x"),
typ: Box::new(TypeUniv::new().into()),
erased: false,
};
let param2 = Param {
implicit: false,
name: VarBind::from_string("y"),
typ: Box::new(TypeUniv::new().into()),
erased: false,
};
let tele = Telescope { params: vec![param1, param2] };
assert_eq!(tele.print_to_string(Default::default()), "(x y: Type)")
Expand All @@ -1079,11 +1110,13 @@ mod print_telescope_tests {
implicit: true,
name: VarBind::from_string("x"),
typ: Box::new(TypeUniv::new().into()),
erased: false,
};
let param2 = Param {
implicit: true,
name: VarBind::from_string("y"),
typ: Box::new(TypeUniv::new().into()),
erased: false,
};
let tele = Telescope { params: vec![param1, param2] };
assert_eq!(tele.print_to_string(Default::default()), "(implicit x y: Type)")
Expand All @@ -1095,11 +1128,13 @@ mod print_telescope_tests {
implicit: true,
name: VarBind::from_string("x"),
typ: Box::new(TypeUniv::new().into()),
erased: false,
};
let param2 = Param {
implicit: false,
name: VarBind::from_string("y"),
typ: Box::new(TypeUniv::new().into()),
erased: false,
};
let tele = Telescope { params: vec![param1, param2] };
assert_eq!(tele.print_to_string(Default::default()), "(implicit x: Type, y: Type)")
Expand All @@ -1111,11 +1146,13 @@ mod print_telescope_tests {
implicit: false,
name: VarBind::from_string("x"),
typ: Box::new(TypeUniv::new().into()),
erased: false,
};
let param2 = Param {
implicit: true,
name: VarBind::from_string("y"),
typ: Box::new(TypeUniv::new().into()),
erased: false,
};
let tele = Telescope { params: vec![param1, param2] };
assert_eq!(tele.print_to_string(Default::default()), "(x: Type, implicit y: Type)")
Expand All @@ -1127,6 +1164,7 @@ mod print_telescope_tests {
implicit: false,
name: VarBind::from_string("a"),
typ: Box::new(TypeUniv::new().into()),
erased: false,
};
let param2 = Param {
implicit: false,
Expand All @@ -1137,6 +1175,7 @@ mod print_telescope_tests {
name: VarBound::from_string("a"),
inferred_type: None,
})),
erased: false,
};
let param3 = Param {
implicit: false,
Expand All @@ -1147,6 +1186,7 @@ mod print_telescope_tests {
name: VarBound::from_string("a"),
inferred_type: None,
})),
erased: false,
};
let tele = Telescope { params: vec![param1, param2, param3] };
assert_eq!(tele.print_to_string(Default::default()), "(a: Type, x y: a)")
Expand All @@ -1164,19 +1204,21 @@ pub struct Param {
#[derivative(PartialEq = "ignore", Hash = "ignore")]
pub name: VarBind,
pub typ: Box<Exp>,
/// Whether the parameter is erased during compilation.
pub erased: bool,
}

impl Substitutable for Param {
type Result = Param;
fn subst<S: Substitution>(&self, ctx: &mut LevelCtx, by: &S) -> Self {
let Param { implicit, name, typ } = self;
Param { implicit: *implicit, name: name.clone(), typ: typ.subst(ctx, by) }
let Param { implicit, name, typ, erased } = self;
Param { implicit: *implicit, name: name.clone(), typ: typ.subst(ctx, by), erased: *erased }
}
}

impl Print for Param {
fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
let Param { implicit, name, typ } = self;
let Param { implicit, name, typ, erased: _ } = self;

Check warning on line 1221 in lang/ast/src/decls.rs

View check run for this annotation

Codecov / codecov/patch

lang/ast/src/decls.rs#L1221 

Added line #L1221 was not covered by tests
if *implicit {
alloc
.text(IMPLICIT)
Expand All @@ -1193,14 +1235,14 @@ impl Print for Param {

impl Zonk for Param {
fn zonk(&mut self, meta_vars: &HashMap<MetaVar, MetaVarState>) -> Result<(), crate::ZonkError> {
let Param { implicit: _, name: _, typ } = self;
let Param { implicit: _, name: _, typ, erased: _ } = self;
typ.zonk(meta_vars)
}
}

impl ContainsMetaVars for Param {
fn contains_metavars(&self) -> bool {
let Param { implicit: _, name: _, typ } = self;
let Param { implicit: _, name: _, typ, erased: _ } = self;

typ.contains_metavars()
}
Expand Down
Loading

0 comments on commit d06e928

Please sign in to comment.