Skip to content

Commit

Permalink
Remove TypAppInfo
Browse files Browse the repository at this point in the history
  • Loading branch information
@BinderDavid
BinderDavid committed Apr 28, 2024
1 parent 392dc3b commit 1b1c6ab
Show file tree
Hide file tree
Showing 14 changed files with 96 additions and 141 deletions.
2 changes: 1 addition & 1 deletion lang/elaborator/src/normalizer/eval.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,7 @@ impl Eval for ust::LocalComatch {
type Val = Rc<Val>;

fn eval(&self, prg: &ust::Prg, env: &mut Env) -> Result<Self::Val, TypeError> {
let ust::LocalComatch { span, info: (), ctx: _, name, is_lambda_sugar, body } = self;
let ust::LocalComatch { span, name, is_lambda_sugar, body, .. } = self;
Ok(Rc::new(Val::Comatch {
span: *span,
name: name.clone(),
Expand Down
4 changes: 2 additions & 2 deletions lang/elaborator/src/normalizer/read_back.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,11 +38,11 @@ impl ReadBack for val::Val {
val::Val::Comatch { span, name, is_lambda_sugar, body } => {
ust::Exp::LocalComatch(ust::LocalComatch {
span: *span,
info: (),
ctx: None,
name: name.clone(),
is_lambda_sugar: *is_lambda_sugar,
body: body.read_back(prg)?,
inferred_type: None,
})
}
val::Val::Neu { exp } => exp.read_back(prg)?,
Expand Down Expand Up @@ -71,13 +71,13 @@ impl ReadBack for val::Neu {
}),
val::Neu::Match { span, name, on_exp, body } => ust::Exp::LocalMatch(ust::LocalMatch {
span: *span,
info: (),
ctx: None,
motive: None,
ret_typ: None,
name: name.clone(),
on_exp: on_exp.read_back(prg)?,
body: body.read_back(prg)?,
inferred_type: None,
}),
val::Neu::Hole { span } => {
ust::Exp::Hole(Hole { span: *span, inferred_type: None, inferred_ctx: None })
Expand Down
9 changes: 4 additions & 5 deletions lang/elaborator/src/typechecker/typecheck.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -729,8 +729,7 @@ impl Check for ust::LocalMatch {
ctx: &mut Ctx,
t: Rc<ust::Exp>,
) -> Result<Self::Target, TypeError> {
let ust::LocalMatch { span, info: (), ctx: _, name, on_exp, motive, ret_typ: _, body } =
self;
let ust::LocalMatch { span, name, on_exp, motive, body, .. } = self;
let on_exp_out = on_exp.infer(prg, ctx)?;
let typ_app_nf = on_exp_out
.typ()
Expand Down Expand Up @@ -790,13 +789,13 @@ impl Check for ust::LocalMatch {

Ok(tst::LocalMatch {
span: *span,
info: tst::TypeAppInfo { typ: typ_app },
ctx: Some(ctx.vars.clone()),
name: name.clone(),
on_exp: on_exp_out,
motive: motive_out,
ret_typ: ret_typ_out.into(),
body: body_out,
inferred_type: Some(typ_app),
})
}
}
Expand All @@ -810,7 +809,7 @@ impl Check for ust::LocalComatch {
ctx: &mut Ctx,
t: Rc<ust::Exp>,
) -> Result<Self::Target, TypeError> {
let ust::LocalComatch { span, info: (), ctx: _, name, is_lambda_sugar, body } = self;
let ust::LocalComatch { span, name, is_lambda_sugar, body, .. } = self;
let typ_app_nf = t.expect_typ_app()?;
let typ_app = typ_app_nf.infer(prg, ctx)?;

Expand All @@ -833,11 +832,11 @@ impl Check for ust::LocalComatch {

Ok(tst::LocalComatch {
span: *span,
info: tst::TypeAppInfo { typ: typ_app },
ctx: Some(ctx.vars.clone()),
name: name.clone(),
is_lambda_sugar: *is_lambda_sugar,
body: body_out,
inferred_type: Some(typ_app),
})
}
}
Expand Down
20 changes: 2 additions & 18 deletions lang/lifting/src/fv.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,14 +35,7 @@ impl FV for ust::Exp {
typ.visit_fv(v)
}
ust::Exp::Variable(e) => e.visit_fv(v),
ust::Exp::LocalComatch(ust::LocalComatch {
span: _,
info: _,
ctx: _,
name: _,
is_lambda_sugar: _,
body,
}) => body.visit_fv(v),
ust::Exp::LocalComatch(ust::LocalComatch { body, .. }) => body.visit_fv(v),
ust::Exp::Call(ust::Call { args, .. }) => args.visit_fv(v),
ust::Exp::DotCall(ust::DotCall { exp, args, .. }) => {
exp.visit_fv(v);
Expand All @@ -51,16 +44,7 @@ impl FV for ust::Exp {
ust::Exp::TypCtor(e) => e.visit_fv(v),
ust::Exp::Hole(Hole { .. }) => {}
ust::Exp::TypeUniv(TypeUniv { span: _ }) => {}
ust::Exp::LocalMatch(ust::LocalMatch {
span: _,
info: _,
ctx: _,
name: _,
on_exp,
motive,
ret_typ: _,
body,
}) => {
ust::Exp::LocalMatch(ust::LocalMatch { on_exp, motive, body, .. }) => {
on_exp.visit_fv(v);
motive.visit_fv(v);
body.visit_fv(v)
Expand Down
55 changes: 40 additions & 15 deletions lang/lifting/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -417,18 +417,43 @@ impl Lift for tst::LocalMatch {
type Target = ust::Exp;

fn lift(&self, ctx: &mut Ctx) -> Self::Target {
let tst::LocalMatch { span, info, ctx: type_ctx, name, on_exp, motive, ret_typ, body } =
self;
ctx.lift_match(span, info, &type_ctx.clone().unwrap(), name, on_exp, motive, ret_typ, body)
let tst::LocalMatch {
span,
ctx: type_ctx,
name,
on_exp,
motive,
ret_typ,
body,
inferred_type,
} = self;
ctx.lift_match(
span,
&inferred_type.clone().unwrap(),
&type_ctx.clone().unwrap(),
name,
on_exp,
motive,
ret_typ,
body,
)
}
}

impl Lift for tst::LocalComatch {
type Target = ust::Exp;

fn lift(&self, ctx: &mut Ctx) -> Self::Target {
let tst::LocalComatch { span, info, ctx: type_ctx, name, is_lambda_sugar, body } = self;
ctx.lift_comatch(span, info, &type_ctx.clone().unwrap(), name, *is_lambda_sugar, body)
let tst::LocalComatch { span, ctx: type_ctx, name, is_lambda_sugar, body, inferred_type } =
self;
ctx.lift_comatch(
span,
&inferred_type.clone().unwrap(),
&type_ctx.clone().unwrap(),
name,
*is_lambda_sugar,
body,
)
}
}
impl Lift for tst::Motive {
Expand Down Expand Up @@ -538,7 +563,7 @@ impl Ctx {
fn lift_match(
&mut self,
span: &Option<Span>,
info: &tst::TypeAppInfo,
inferred_type: &tst::TypCtor,
type_ctx: &TypeCtx,
name: &tst::Label,
on_exp: &Rc<tst::Exp>,
Expand All @@ -547,10 +572,10 @@ impl Ctx {
body: &tst::Match,
) -> ust::Exp {
// Only lift local matches for the specified type
if info.typ.name != self.name {
if inferred_type.name != self.name {
return ust::Exp::LocalMatch(ust::LocalMatch {
span: *span,
info: info.forget_tst(),
inferred_type: None,
ctx: None,
name: name.clone(),
on_exp: on_exp.lift(self),
Expand All @@ -571,7 +596,7 @@ impl Ctx {
.unwrap_or_else(|| free_vars(&ret_typ.forget_tst(), type_ctx));

let body = body.lift(self);
let self_typ = info.typ.lift(self);
let self_typ = inferred_type.lift(self);

let FreeVarsResult { telescope, subst, args } = free_vars(&body, type_ctx)
.union(free_vars(&self_typ, type_ctx))
Expand All @@ -592,7 +617,7 @@ impl Ctx {
};

// Build the new top-level definition
let name = self.unique_def_name(name, &info.typ.name);
let name = self.unique_def_name(name, &inferred_type.name);

let def = ust::Def {
span: None,
Expand Down Expand Up @@ -624,28 +649,28 @@ impl Ctx {
fn lift_comatch(
&mut self,
span: &Option<Span>,
info: &tst::TypeAppInfo,
inferred_type: &tst::TypCtor,
type_ctx: &TypeCtx,
name: &tst::Label,
is_lambda_sugar: bool,
body: &tst::Match,
) -> ust::Exp {
// Only lift local matches for the specified type
if info.typ.name != self.name {
if inferred_type.name != self.name {
return ust::Exp::LocalComatch(ust::LocalComatch {
span: *span,
info: info.forget_tst(),
ctx: None,
name: name.clone(),
is_lambda_sugar,
body: body.lift(self),
inferred_type: None,
});
}

self.mark_modified();

let body = body.lift(self);
let typ = info.typ.lift(self);
let typ = inferred_type.lift(self);

// Collect the free variables in the comatch and the return type
// Build a telescope of the types of the lifted variables
Expand All @@ -657,7 +682,7 @@ impl Ctx {
let typ = typ.subst(&mut self.ctx, &subst.in_body());

// Build the new top-level definition
let name = self.unique_codef_name(name, &info.typ.name);
let name = self.unique_codef_name(name, &inferred_type.name);

let codef = ust::Codef {
span: None,
Expand Down
4 changes: 2 additions & 2 deletions lang/lowering/src/lower/exp.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -174,13 +174,13 @@ impl Lower for cst::exp::LocalMatch {
let cst::exp::LocalMatch { span, name, on_exp, motive, body } = self;
Ok(ust::Exp::LocalMatch(ust::LocalMatch {
span: Some(*span),
info: (),
ctx: None,
name: ctx.unique_label(name.to_owned(), span)?,
on_exp: on_exp.lower(ctx)?,
motive: motive.lower(ctx)?,
ret_typ: None,
body: body.lower(ctx)?,
inferred_type: None,
}))
}
}
Expand All @@ -192,11 +192,11 @@ impl Lower for cst::exp::LocalComatch {
let cst::exp::LocalComatch { span, name, is_lambda_sugar, body } = self;
Ok(ust::Exp::LocalComatch(ust::LocalComatch {
span: Some(*span),
info: (),
ctx: None,
name: ctx.unique_label(name.to_owned(), span)?,
is_lambda_sugar: *is_lambda_sugar,
body: body.lower(ctx)?,
inferred_type: None,
}))
}
}
Expand Down
4 changes: 2 additions & 2 deletions lang/printer/src/generic.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -590,7 +590,7 @@ impl<'a, P: Phase> Print<'a> for LocalMatch<P> {
alloc: &'a Alloc<'a>,
_prec: Precedence,
) -> Builder<'a> {
let LocalMatch { span: _, info: _, ctx: _, name, on_exp, motive, ret_typ: _, body } = self;
let LocalMatch { name, on_exp, motive, body, .. } = self;
on_exp
.print(cfg, alloc)
.append(DOT)
Expand All @@ -612,7 +612,7 @@ impl<'a, P: Phase> Print<'a> for LocalComatch<P> {
alloc: &'a Alloc<'a>,
_prec: Precedence,
) -> Builder<'a> {
let LocalComatch { span: _, info: _, ctx: _, name, is_lambda_sugar, body } = self;
let LocalComatch { name, is_lambda_sugar, body, .. } = self;
if *is_lambda_sugar && cfg.print_lambda_sugar {
print_lambda_sugar(body, cfg, alloc)
} else {
Expand Down
Loading

0 comments on commit 1b1c6ab

Please sign in to comment.