Skip to content

Commit

Permalink
Adapt typechecker
Browse files Browse the repository at this point in the history
  • Loading branch information
BinderDavid committed Feb 20, 2024
1 parent 7533fd3 commit 8e99700
Show file tree
Hide file tree
Showing 15 changed files with 10 additions and 29 deletions.
1 change: 0 additions & 1 deletion lang/lifting/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -261,7 +261,6 @@ impl Lift for tst::Match {
}
}


impl Lift for tst::Case {
type Target = ust::Case;

Expand Down
2 changes: 0 additions & 2 deletions lang/lowering/src/imp.rs
Original file line number Diff line number Diff line change
Expand Up @@ -355,7 +355,6 @@ impl Lower for cst::Match {
}
}


impl Lower for cst::Case {
type Target = ust::Case;

Expand All @@ -368,7 +367,6 @@ impl Lower for cst::Case {
}
}


impl Lower for cst::TypApp {
type Target = ust::TypApp;

Expand Down
1 change: 0 additions & 1 deletion lang/normalizer/src/eval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,6 @@ impl Eval for ust::Case {
}
}


impl Eval for ust::TypApp {
type Val = val::TypApp;

Expand Down
3 changes: 0 additions & 3 deletions lang/normalizer/src/val.rs
Original file line number Diff line number Diff line change
Expand Up @@ -172,7 +172,6 @@ impl ShiftInRange for Match {
}
}


impl ShiftInRange for Case {
fn shift_in_range<R: ShiftRange>(&self, range: R, by: (isize, isize)) -> Self {
let Case { info, name, args, body } = self;
Expand All @@ -186,7 +185,6 @@ impl ShiftInRange for Case {
}
}


impl ShiftInRange for Closure {
fn shift_in_range<R: ShiftRange>(&self, range: R, by: (isize, isize)) -> Self {
let Closure { env, n_args, body } = self;
Expand Down Expand Up @@ -279,7 +277,6 @@ impl<'a> Print<'a> for Case {
}
}


impl<'a> Print<'a> for Closure {
fn print(&'a self, _cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
alloc.text("...")
Expand Down
1 change: 0 additions & 1 deletion lang/parser/src/cst.rs
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,6 @@ pub struct Match {
pub omit_absurd: bool,
}


#[derive(Debug, Clone)]
pub struct Case {
pub span: Span,
Expand Down
1 change: 0 additions & 1 deletion lang/printer/src/ust.rs
Original file line number Diff line number Diff line change
Expand Up @@ -318,7 +318,6 @@ impl<'a> Print<'a> for Case {
}
}


impl<'a> Print<'a> for Telescope {
fn print(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
let Telescope { params } = self;
Expand Down
2 changes: 1 addition & 1 deletion lang/query/src/info.rs
Original file line number Diff line number Diff line change
Expand Up @@ -145,7 +145,7 @@ impl Visitor<tst::TST> for InfoCollector {
_hidden: bool,
_params: &tst::Telescope,
typ: &tst::TypApp,
_body: &tst::Comatch,
_body: &tst::Match,
) {
self.add_item_span(
Item::Codef { name: name.clone(), type_name: typ.name.clone() },
Expand Down
1 change: 0 additions & 1 deletion lang/syntax/src/trees/forget/tst.rs
Original file line number Diff line number Diff line change
Expand Up @@ -168,7 +168,6 @@ impl Forget for tst::Match {
}
}


impl Forget for tst::Case {
type Target = ust::Case;

Expand Down
1 change: 0 additions & 1 deletion lang/syntax/src/trees/generic/def.rs
Original file line number Diff line number Diff line change
Expand Up @@ -459,7 +459,6 @@ impl<P: Phase> HasPhase for Match<P> {
type Phase = P;
}


impl<P: Phase> HasPhase for Case<P> {
type Phase = P;
}
Expand Down
2 changes: 0 additions & 2 deletions lang/syntax/src/trees/generic/fold.rs
Original file line number Diff line number Diff line change
Expand Up @@ -430,7 +430,6 @@ impl<P: Phase, O: Out> Fold<P, O> for Match<P> {
}
}


impl<P: Phase, O: Out> Fold<P, O> for Case<P> {
type Out = O::Case;

Expand All @@ -446,7 +445,6 @@ impl<P: Phase, O: Out> Fold<P, O> for Case<P> {
}
}


impl<P: Phase, O: Out> Fold<P, O> for TypApp<P> {
type Out = O::TypApp;

Expand Down
1 change: 0 additions & 1 deletion lang/syntax/src/trees/nf/def.rs
Original file line number Diff line number Diff line change
Expand Up @@ -133,7 +133,6 @@ impl HasSpan for Case {
}
}


#[derive(Debug, Clone)]
pub struct TypApp {
pub info: Option<Span>,
Expand Down
2 changes: 0 additions & 2 deletions lang/syntax/src/trees/nf/forget.rs
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,6 @@ impl Forget for Match {
}
}


impl Forget for Case {
type Target = ust::Case;

Expand All @@ -80,7 +79,6 @@ impl Forget for Case {
}
}


impl Forget for TypApp {
type Target = ust::TypApp;

Expand Down
1 change: 0 additions & 1 deletion lang/syntax/src/trees/nf/shift.rs
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,6 @@ impl ShiftInRange for Match {
}
}


impl ShiftInRange for Case {
fn shift_in_range<R: ShiftRange>(&self, range: R, by: (isize, isize)) -> Self {
let Case { info, name, args, body } = self;
Expand Down
1 change: 0 additions & 1 deletion lang/syntax/src/trees/ust/occurs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,6 @@ impl Occurs for Match {
}
}


impl Occurs for Case {
fn occurs(&self, ctx: &mut LevelCtx, lvl: Lvl) -> bool {
let Case { args, body, .. } = self;
Expand Down
19 changes: 9 additions & 10 deletions lang/typechecker/src/typecheck.rs
Original file line number Diff line number Diff line change
Expand Up @@ -386,7 +386,7 @@ impl<'a> Check for WithScrutinee<'a> {
}

struct WithDestructee<'a> {
inner: &'a ust::Comatch,
inner: &'a ust::Match,
/// Name of the global codefinition that gets substituted for the destructor's self parameters
label: Option<Ident>,
n_label_args: usize,
Expand All @@ -395,10 +395,10 @@ struct WithDestructee<'a> {

/// Infer a copattern match
impl<'a> Infer for WithDestructee<'a> {
type Target = tst::Comatch;
type Target = tst::Match;

fn infer(&self, prg: &ust::Prg, ctx: &mut Ctx) -> Result<Self::Target, TypeError> {
let ust::Comatch { info, cases, omit_absurd } = &self.inner;
let ust::Match { info, cases, omit_absurd } = &self.inner;

// Check that this comatch is on a codata type
let codata = prg.decls.codata(&self.destructee.name, *info)?;
Expand Down Expand Up @@ -437,8 +437,7 @@ impl<'a> Infer for WithDestructee<'a> {
for name in dtors_missing.cloned() {
let ust::Dtor { params, .. } = prg.decls.dtor(&name, *info)?;

let case =
ust::Cocase { info: *info, name, params: params.instantiate(), body: None };
let case = ust::Case { info: *info, name, args: params.instantiate(), body: None };
cases.push((case, true));
}
}
Expand Down Expand Up @@ -503,7 +502,7 @@ impl<'a> Infer for WithDestructee<'a> {
}
}

Ok(tst::Comatch { info: *info, cases: cases_out, omit_absurd: *omit_absurd })
Ok(tst::Match { info: *info, cases: cases_out, omit_absurd: *omit_absurd })
}
}

Expand Down Expand Up @@ -601,12 +600,12 @@ fn check_case(
#[trace("{:P} |- {:P} <= {:P}", ctx, cocase, t)]
fn check_cocase(
eqns: Vec<Eqn>,
cocase: &ust::Cocase,
cocase: &ust::Case,
prg: &ust::Prg,
ctx: &mut Ctx,
t: Rc<nf::Nf>,
) -> Result<tst::Cocase, TypeError> {
let ust::Cocase { info, name, params: params_inst, body } = cocase;
) -> Result<tst::Case, TypeError> {
let ust::Case { info, name, args: params_inst, body } = cocase;
let ust::Dtor { name, params, .. } = prg.decls.dtor(name, *info)?;

params_inst.check_telescope(
Expand Down Expand Up @@ -650,7 +649,7 @@ fn check_cocase(
}
};

Ok(tst::Cocase { info: *info, name: name.clone(), params: args_out, body: body_out })
Ok(tst::Case { info: *info, name: name.clone(), args: args_out, body: body_out })
},
*info,
)
Expand Down

0 comments on commit 8e99700

Please sign in to comment.