Skip to content

Commit

Permalink
Add erased fields to ast (#429)
Browse files Browse the repository at this point in the history
  • Loading branch information
@timsueberkrueb
timsueberkrueb authored Jan 4, 2025
1 parent bdf4821 commit 52d2591
Show file tree
Hide file tree
Showing 22 changed files with 323 additions and 235 deletions.
229 changes: 106 additions & 123 deletions Cargo.lock
View file

Large diffs are not rendered by default.

29 changes: 22 additions & 7 deletions lang/ast/src/decls.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -873,6 +873,7 @@ impl SelfParam {
implicit: false,
name: self.name.clone().unwrap_or_else(|| VarBind::from_string("")),
typ: Box::new(self.typ.to_exp()),
erased: false,
}],
}
}
Expand Down Expand Up @@ -946,11 +947,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 +980,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 +1065,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 +1083,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 +1101,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 +1119,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 +1137,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 +1148,7 @@ mod print_telescope_tests {
name: VarBound::from_string("a"),
inferred_type: None,
})),
erased: false,
};
let param3 = Param {
implicit: false,
Expand All @@ -1147,6 +1159,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 +1177,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;
if *implicit {
alloc
.text(IMPLICIT)
Expand All @@ -1193,14 +1208,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
93 changes: 58 additions & 35 deletions lang/ast/src/exp/args.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,61 +23,69 @@ use super::{Exp, Hole, Lvl, MetaVar, VarBound};
#[derive(Debug, Clone, Derivative)]
#[derivative(Eq, PartialEq, Hash)]
pub enum Arg {
UnnamedArg(Box<Exp>),
NamedArg(VarBound, Box<Exp>),
InsertedImplicitArg(Hole),
UnnamedArg { arg: Box<Exp>, erased: bool },
NamedArg { name: VarBound, arg: Box<Exp>, erased: bool },
InsertedImplicitArg { hole: Hole, erased: bool },
}

impl Arg {
pub fn is_inserted_implicit(&self) -> bool {
matches!(self, Arg::InsertedImplicitArg(_))
matches!(self, Arg::InsertedImplicitArg { .. })
}

pub fn exp(&self) -> Box<Exp> {
match self {
Arg::UnnamedArg(e) => e.clone(),
Arg::NamedArg(_, e) => e.clone(),
Arg::InsertedImplicitArg(hole) => Box::new(hole.clone().into()),
Arg::UnnamedArg { arg, .. } => arg.clone(),
Arg::NamedArg { arg, .. } => arg.clone(),
Arg::InsertedImplicitArg { hole, .. } => Box::new(hole.clone().into()),
}
}

pub fn erased(&self) -> bool {
match self {
Arg::UnnamedArg { erased, .. } => *erased,
Arg::NamedArg { erased, .. } => *erased,
Arg::InsertedImplicitArg { erased, .. } => *erased,
}
}
}

impl HasSpan for Arg {
fn span(&self) -> Option<Span> {
match self {
Arg::UnnamedArg(e) => e.span(),
Arg::NamedArg(_, e) => e.span(),
Arg::InsertedImplicitArg(hole) => hole.span(),
Arg::UnnamedArg { arg, .. } => arg.span(),
Arg::NamedArg { arg, .. } => arg.span(),
Arg::InsertedImplicitArg { hole, .. } => hole.span(),
}
}
}

impl Shift for Arg {
fn shift_in_range<R: ShiftRange>(&mut self, range: &R, by: (isize, isize)) {
match self {
Arg::UnnamedArg(e) => e.shift_in_range(range, by),
Arg::NamedArg(_, e) => e.shift_in_range(range, by),
Arg::InsertedImplicitArg(hole) => hole.shift_in_range(range, by),
Arg::UnnamedArg { arg, .. } => arg.shift_in_range(range, by),
Arg::NamedArg { arg, .. } => arg.shift_in_range(range, by),
Arg::InsertedImplicitArg { hole, .. } => hole.shift_in_range(range, by),
}
}
}

impl Occurs for Arg {
fn occurs(&self, ctx: &mut LevelCtx, lvl: Lvl) -> bool {
match self {
Arg::UnnamedArg(e) => e.occurs(ctx, lvl),
Arg::NamedArg(_, e) => e.occurs(ctx, lvl),
Arg::InsertedImplicitArg(hole) => hole.occurs(ctx, lvl),
Arg::UnnamedArg { arg, .. } => arg.occurs(ctx, lvl),
Arg::NamedArg { arg, .. } => arg.occurs(ctx, lvl),
Arg::InsertedImplicitArg { hole, .. } => hole.occurs(ctx, lvl),
}
}
}

impl HasType for Arg {
fn typ(&self) -> Option<Box<Exp>> {
match self {
Arg::UnnamedArg(e) => e.typ(),
Arg::NamedArg(_, e) => e.typ(),
Arg::InsertedImplicitArg(hole) => hole.typ(),
Arg::UnnamedArg { arg, .. } => arg.typ(),
Arg::NamedArg { arg, .. } => arg.typ(),
Arg::InsertedImplicitArg { hole, .. } => hole.typ(),
}
}
}
Expand All @@ -86,19 +94,27 @@ impl Substitutable for Arg {
type Result = Arg;
fn subst<S: Substitution>(&self, ctx: &mut LevelCtx, by: &S) -> Self::Result {
match self {
Arg::UnnamedArg(e) => Arg::UnnamedArg(e.subst(ctx, by)),
Arg::NamedArg(i, e) => Arg::NamedArg(i.clone(), e.subst(ctx, by)),
Arg::InsertedImplicitArg(hole) => Arg::InsertedImplicitArg(hole.subst(ctx, by)),
Arg::UnnamedArg { arg, erased } => {
Arg::UnnamedArg { arg: arg.subst(ctx, by), erased: *erased }
}
Arg::NamedArg { name: var, arg, erased } => {
Arg::NamedArg { name: var.clone(), arg: arg.subst(ctx, by), erased: *erased }
}
Arg::InsertedImplicitArg { hole, erased } => {
Arg::InsertedImplicitArg { hole: hole.subst(ctx, by), erased: *erased }
}
}
}
}

impl Print for Arg {
fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
match self {
Arg::UnnamedArg(e) => e.print(cfg, alloc),
Arg::NamedArg(i, e) => alloc.text(&i.id).append(COLONEQ).append(e.print(cfg, alloc)),
Arg::InsertedImplicitArg(_) => {
Arg::UnnamedArg { arg, .. } => arg.print(cfg, alloc),
Arg::NamedArg { name: var, arg, .. } => {
alloc.text(&var.id).append(COLONEQ).append(arg.print(cfg, alloc))
}
Arg::InsertedImplicitArg { .. } => {
panic!("Inserted implicit arguments should not be printed")
}
}
Expand All @@ -111,19 +127,19 @@ impl Zonk for Arg {
meta_vars: &crate::HashMap<MetaVar, crate::MetaVarState>,
) -> Result<(), ZonkError> {
match self {
Arg::UnnamedArg(e) => e.zonk(meta_vars),
Arg::NamedArg(_, e) => e.zonk(meta_vars),
Arg::InsertedImplicitArg(hole) => hole.zonk(meta_vars),
Arg::UnnamedArg { arg, .. } => arg.zonk(meta_vars),
Arg::NamedArg { arg, .. } => arg.zonk(meta_vars),
Arg::InsertedImplicitArg { hole, .. } => hole.zonk(meta_vars),
}
}
}

impl ContainsMetaVars for Arg {
fn contains_metavars(&self) -> bool {
match self {
Arg::UnnamedArg(e) => e.contains_metavars(),
Arg::NamedArg(_, e) => e.contains_metavars(),
Arg::InsertedImplicitArg(hole) => hole.contains_metavars(),
Arg::UnnamedArg { arg, .. } => arg.contains_metavars(),
Arg::NamedArg { arg, .. } => arg.contains_metavars(),
Arg::InsertedImplicitArg { hole, .. } => hole.contains_metavars(),
}
}
}
Expand Down Expand Up @@ -249,13 +265,19 @@ mod args_tests {
);

assert_eq!(
Args { args: vec![Arg::UnnamedArg(ctor.clone())] }.print_to_string(Default::default()),
Args { args: vec![Arg::UnnamedArg { arg: ctor.clone(), erased: false }] }
.print_to_string(Default::default()),
"(T)".to_string()
);

assert_eq!(
Args { args: vec![Arg::UnnamedArg(ctor.clone()), Arg::UnnamedArg(ctor)] }
.print_to_string(Default::default()),
Args {
args: vec![
Arg::UnnamedArg { arg: ctor.clone(), erased: false },
Arg::UnnamedArg { arg: ctor, erased: false }
]
}
.print_to_string(Default::default()),
"(T, T)".to_string()
)
}
Expand All @@ -273,7 +295,8 @@ mod args_tests {
};

assert_eq!(
Args { args: vec![Arg::InsertedImplicitArg(hole)] }.print_to_string(Default::default()),
Args { args: vec![Arg::InsertedImplicitArg { hole, erased: false }] }
.print_to_string(Default::default()),
"".to_string()
)
}
Expand Down
8 changes: 5 additions & 3 deletions lang/ast/src/exp/telescope_inst.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,11 +75,13 @@ pub struct ParamInst {
pub name: VarBind,
#[derivative(PartialEq = "ignore", Hash = "ignore")]
pub typ: Option<Box<Exp>>,
/// Whether the parameter is erased during compilation.
pub erased: bool,
}

impl Print for ParamInst {
fn print<'a>(&'a self, _cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
let ParamInst { span: _, info: _, name, typ: _ } = self;
let ParamInst { span: _, info: _, name, typ: _, erased: _ } = self;
alloc.text(&name.id)
}
}
Expand All @@ -89,7 +91,7 @@ impl Zonk for ParamInst {
&mut self,
meta_vars: &crate::HashMap<MetaVar, crate::MetaVarState>,
) -> Result<(), ZonkError> {
let ParamInst { span: _, info, name: _, typ } = self;
let ParamInst { span: _, info, name: _, typ, erased: _ } = self;

info.zonk(meta_vars)?;
typ.zonk(meta_vars)?;
Expand All @@ -99,7 +101,7 @@ impl Zonk for ParamInst {

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

info.contains_metavars() || typ.contains_metavars()
}
Expand Down
3 changes: 3 additions & 0 deletions lang/backend/Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,9 @@ categories.workspace = true
[dependencies]
# ir structures
url = { workspace = true }
# error handling
miette = { workspace = true }
thiserror = { workspace = true }
# workspace dependencies
ast = { path = "../ast" }
printer = { path = "../printer" }
3 changes: 0 additions & 3 deletions lang/backend/src/ir/decls.rs
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,3 @@
//! High-level intermediate respresentation of the AST after erasure.
//! This representation is shared between any compiler backends and hence can only make few assumptions about the compilation target.
use url::Url;

use ast::UseDecl;
Expand Down
2 changes: 2 additions & 0 deletions lang/backend/src/ir/exprs.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -205,6 +205,8 @@ impl Print for Case {
pub struct Pattern {
pub is_copattern: bool,
pub name: String,
/// The URI of the module where `name` is defined.
pub module_uri: Url,
pub params: Vec<String>,
}

Expand Down
Loading

0 comments on commit 52d2591

Please sign in to comment.