Skip to content

Commit

Permalink
cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
@LighghtEeloo
LighghtEeloo committed Jul 3, 2024
1 parent 788efd6 commit 6349201
Show file tree
Hide file tree
Showing 3 changed files with 43 additions and 40 deletions.
30 changes: 15 additions & 15 deletions lang/statics/src/lift.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ impl SEnv<KindId> {
/// generate the type of algebra (signature) for a kind by algebra passing style for higher order contravariant kinds
/// for value type `A`, return `Top`
/// for computation type `B`, return `Algebra M B`
/// for arrow `fn Y -> S`, return `Sig`
/// for arrow `fn Y -> S Y`, return `U (Sig(Y)) -> Sig(S Y)`
pub fn signature(&self, tycker: &mut Tycker, mo_ty: TypeId, ty: TypeId) -> ResultKont<TypeId> {
let ctype = tycker.ctype(&self.env);
let res = match tycker.statics.kinds[&self.inner].to_owned() {
Expand All @@ -95,7 +95,7 @@ impl SEnv<KindId> {
assert!(Lub::lub(a_kd, _kd, tycker).is_ok(), "input kind mismatch");
let ty_a = Alloc::alloc(tycker, tvar_a, a_kd);
let alg_a = self.mk(a_kd).signature(tycker, mo_ty, ty_a)?;
let thunk_alg_a = tycker.thunk_app(&self.env, alg_a);
let thunk_alg_a = tycker.thunk_arg(&self.env, alg_a);
let alg_b = self.mk(b_kd).signature(tycker, mo_ty, body)?;
Alloc::alloc(tycker, Arrow(thunk_alg_a, alg_b), ctype)
}
Expand Down Expand Up @@ -270,7 +270,7 @@ impl SEnv<TypeId> {
// m
let m_ty = {
let ty_mo_x = Alloc::alloc(tycker, App(mo_ty, ty_x), ctype);
tycker.thunk_app(&self.env, ty_mo_x)
tycker.thunk_arg(&self.env, ty_mo_x)
};
let var_m = Alloc::alloc(tycker, VarName("m".to_string()), m_ty.into());
let vpat_m: VPatId = Alloc::alloc(tycker, var_m, m_ty);
Expand All @@ -279,7 +279,7 @@ impl SEnv<TypeId> {
// f
let f_ty = {
let arrs = Alloc::alloc(tycker, Arrow(ty_x, mo_a_ty), ctype);
tycker.thunk_app(&self.env, arrs)
tycker.thunk_arg(&self.env, arrs)
};
let var_f = Alloc::alloc(tycker, VarName("f".to_string()), f_ty.into());
let vpat_f: VPatId = Alloc::alloc(tycker, var_f, f_ty);
Expand Down Expand Up @@ -309,7 +309,7 @@ impl SEnv<TypeId> {
let force_mo_bind_x_a_m_ty = {
// Thunk (X -> M A) -> M A
let x_arr_mo_a = Alloc::alloc(tycker, Arrow(ty_x, mo_a_ty), ctype);
let thunk_x_arr_mo_a = tycker.thunk_app(&self.env, x_arr_mo_a);
let thunk_x_arr_mo_a = tycker.thunk_arg(&self.env, x_arr_mo_a);
Alloc::alloc(tycker, Arrow(thunk_x_arr_mo_a, mo_a_ty), ctype)
};
let force_mo_bind_x_a_m = Alloc::alloc(
Expand Down Expand Up @@ -421,7 +421,7 @@ impl SEnv<TypeId> {
let ty_x_arr_b = Alloc::alloc(tycker, Arrow(ty_x, b_ty), ctype);
let function = Alloc::alloc(tycker, Abs(vpat_x, force_f_x_a), ty_x_arr_b);

let ann = tycker.thunk_app(&self.env, ty_x_arr_b);
let ann = tycker.thunk_arg(&self.env, ty_x_arr_b);
Alloc::alloc(tycker, Thunk(function), ann)
};

Expand Down Expand Up @@ -492,7 +492,7 @@ impl SEnv<TypeId> {
let function =
Alloc::alloc(tycker, Abs(vpat_x, force_f_x_dtor), ty_x_arr_b);

let ann = tycker.thunk_app(&self.env, ty_x_arr_b);
let ann = tycker.thunk_arg(&self.env, ty_x_arr_b);
Alloc::alloc(tycker, Thunk(function), ann)
};

Expand Down Expand Up @@ -701,7 +701,7 @@ impl SEnv<CompuId> {
let (thunked_function_ty, thunked_function) = {
let function_ty = Alloc::alloc(tycker, Arrow(binder_ty, tail_ty), ctype);
let function = Alloc::alloc(tycker, Abs(binder_, tail_), function_ty);
let thunked_function_ty = tycker.thunk_app(&self.env, function_ty);
let thunked_function_ty = tycker.thunk_arg(&self.env, function_ty);
let thunked_function =
Alloc::alloc(tycker, Thunk(function), thunked_function_ty);
(thunked_function_ty, thunked_function)
Expand All @@ -717,7 +717,7 @@ impl SEnv<CompuId> {
let binda_v = Alloc::alloc(tycker, App(binda, binder_ty), binda_v_ty);
let bindee_ = self.mk(bindee).lift(tycker, (mo, mo_ty), algs)?;
let bindee_ty = tycker.statics.annotations_compu[&bindee];
let thunked_bindee_ty = tycker.thunk_app(&self.env, bindee_ty);
let thunked_bindee_ty = tycker.thunk_arg(&self.env, bindee_ty);
let thunked_bindee = Alloc::alloc(tycker, Thunk(bindee_), thunked_bindee_ty);
let binda_v_thunked_bindee_ty =
Alloc::alloc(tycker, Arrow(thunked_function_ty, tail_ty), ctype);
Expand Down Expand Up @@ -815,10 +815,10 @@ fn gen_mo_bind_body(
// where M is the monad type `mo_ty`
let ctype = tycker.ctype(env);
let m_a = Alloc::alloc(tycker, App(mo_ty, a_ty), ctype);
let thunk_m_a = tycker.thunk_app(env, m_a);
let thunk_m_a = tycker.thunk_arg(env, m_a);
let m_a_prime = Alloc::alloc(tycker, App(mo_ty, a_prime_ty), ctype);
let a_arr_m_a_prime = Alloc::alloc(tycker, Arrow(a_ty, m_a_prime), ctype);
let thunk_a_arr_m_a_prime = tycker.thunk_app(env, a_arr_m_a_prime);
let thunk_a_arr_m_a_prime = tycker.thunk_arg(env, a_arr_m_a_prime);
let latter_arr = Alloc::alloc(tycker, Arrow(thunk_a_arr_m_a_prime, m_a_prime), ctype);
Alloc::alloc(tycker, Arrow(thunk_m_a, latter_arr), ctype)
}
Expand Down Expand Up @@ -855,7 +855,7 @@ fn gen_alg_thunk_a_r_r(
// Thunk (A -> R) -> R
let ctype = tycker.ctype(env);
let a_arr_carrier = Alloc::alloc(tycker, Arrow(a_ty, carrier_ty), ctype);
let thunk_a_arr_carrier = tycker.thunk_app(env, a_arr_carrier);
let thunk_a_arr_carrier = tycker.thunk_arg(env, a_arr_carrier);
Alloc::alloc(tycker, Arrow(thunk_a_arr_carrier, carrier_ty), ctype)
}
/// `Thunk (M A) -> Thunk (A -> R) -> R`
Expand All @@ -866,7 +866,7 @@ fn gen_alg_binda_body(
// where M is the monad type `mo_ty` and R is the carrier of the algebra `b`
let ctype = tycker.ctype(env);
let m_a = Alloc::alloc(tycker, App(mo_ty, a_ty), ctype);
let thunk_m_a = tycker.thunk_app(env, m_a);
let thunk_m_a = tycker.thunk_arg(env, m_a);
let latter_arr = gen_alg_thunk_a_r_r(env, tycker, a_ty, carrier_ty);
Alloc::alloc(tycker, Arrow(thunk_m_a, latter_arr), ctype)
}
Expand Down Expand Up @@ -911,7 +911,7 @@ fn gen_algebra_template(
// M X
let m_x_ty = Alloc::alloc(tycker, App(mo_ty, ty_x), ctype);
// Thunk (M X)
let m_ty = tycker.thunk_app(env, m_x_ty);
let m_ty = tycker.thunk_arg(env, m_x_ty);

// m
let var_m = Alloc::alloc(tycker, VarName("m".to_string()), m_ty.into());
Expand All @@ -920,7 +920,7 @@ fn gen_algebra_template(

// Thunk (X -> R) -> R
let x_arr_r_r_ty = gen_alg_thunk_a_r_r(env, tycker, ty_x, carrier_ty);
let f_ty = tycker.thunk_app(env, x_arr_r_r_ty);
let f_ty = tycker.thunk_arg(env, x_arr_r_r_ty);

// f
let var_f = Alloc::alloc(tycker, VarName("f".to_string()), f_ty.into());
Expand Down
29 changes: 18 additions & 11 deletions lang/statics/src/prims.rs
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
use crate::{syntax::*, *};
use zydeco_utils::arena::ArenaAccess;

/* ---------------------------------- Kind ---------------------------------- */
impl Tycker {
pub fn vtype(&mut self, env: &Env<AnnId>) -> KindId {
let AnnId::Kind(kd) = env[self.prim.vtype.get()] else { unreachable!() };
Expand All @@ -10,36 +11,42 @@ impl Tycker {
let AnnId::Kind(kd) = env[self.prim.ctype.get()] else { unreachable!() };
kd
}
}

/* ---------------------------------- Type ---------------------------------- */
impl Tycker {
pub fn thunk(&mut self, env: &Env<AnnId>) -> TypeId {
let AnnId::Type(ty) = env[self.prim.thunk.get()] else { unreachable!() };
ty
}
pub fn thunk_app(&mut self, env: &Env<AnnId>, arg: TypeId) -> TypeId {
/// generates `Thunk B`
pub fn thunk_arg(&mut self, env: &Env<AnnId>, arg: TypeId) -> TypeId {
let thunk = self.thunk(env);
let vtype = self.vtype(env);
Alloc::alloc(self, App(thunk, arg), vtype)
}
pub fn thunk_app_hole(&mut self, env: &Env<AnnId>, site: su::TermId) -> TypeId {
let AnnId::Type(ty) = env[self.prim.thunk.get()] else { unreachable!() };
/// generates `Thunk _`
pub fn thunk_hole(&mut self, env: &Env<AnnId>, site: su::TermId) -> TypeId {
let fill = self.statics.fills.alloc(site);
let ctype = self.ctype(env);
let hole = Alloc::alloc(self, fill, ctype);
let vtype = self.vtype(env);
let app = Alloc::alloc(self, App(ty, hole), vtype);
app
self.thunk_arg(env, hole)
}
pub fn ret(&mut self, env: &Env<AnnId>) -> TypeId {
let AnnId::Type(ty) = env[self.prim.ret.get()] else { unreachable!() };
ty
}
pub fn ret_app_hole(&mut self, env: &Env<AnnId>, site: su::TermId) -> TypeId {
let AnnId::Type(ty) = env[self.prim.ret.get()] else { unreachable!() };
/// generates `Ret A`
pub fn ret_arg(&mut self, env: &Env<AnnId>, arg: TypeId) -> TypeId {
let ret = self.ret(env);
let ctype = self.ctype(env);
Alloc::alloc(self, App(ret, arg), ctype)
}
pub fn ret_hole(&mut self, env: &Env<AnnId>, site: su::TermId) -> TypeId {
let fill = self.statics.fills.alloc(site);
let vtype = self.vtype(env);
let hole = Alloc::alloc(self, fill, vtype);
let ctype = self.ctype(env);
let app = Alloc::alloc(self, App(ty, hole), ctype);
app
self.ret_arg(env, hole)
}
pub fn unit(&mut self, env: &Env<AnnId>) -> TypeId {
let AnnId::Type(ty) = env[self.prim.unit.get()] else { unreachable!() };
Expand Down
24 changes: 10 additions & 14 deletions lang/statics/src/tyck.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1200,7 +1200,7 @@ impl Tyck for SEnv<su::TermId> {
let switch = {
match switch {
| Switch::Ana(AnnId::Type(ty)) => {
let thunk_app_ty = tycker.thunk_app(&self.env, ty);
let thunk_app_ty = tycker.thunk_arg(&self.env, ty);
Switch::Ana(thunk_app_ty.into())
}
| _ => switch,
Expand Down Expand Up @@ -1477,13 +1477,13 @@ impl Tyck for SEnv<su::TermId> {
| Tm::Thunk(term) => {
let su::Thunk(body) = term;
let ana = match switch {
| Switch::Syn => tycker.thunk_app_hole(&self.env, self.inner).into(),
| Switch::Syn => tycker.thunk_hole(&self.env, self.inner).into(),
| Switch::Ana(ana) => ana,
};
let AnnId::Type(ana_ty) = ana else {
tycker.err_k(TyckError::SortMismatch, std::panic::Location::caller())?
};
let thunk_app_hole = tycker.thunk_app_hole(&self.env, body);
let thunk_app_hole = tycker.thunk_hole(&self.env, body);
let ty = Lub::lub_k(ana_ty, thunk_app_hole, tycker)?;
let ss::Type::App(thunk_app_body_ty) = tycker.statics.types[&ty].to_owned() else {
unreachable!()
Expand All @@ -1495,7 +1495,7 @@ impl Tyck for SEnv<su::TermId> {
TyckError::SortMismatch,
std::panic::Location::caller(),
)?;
let thunk_app_body_ty = tycker.thunk_app(&self.env, body_ty);
let thunk_app_body_ty = tycker.thunk_arg(&self.env, body_ty);
let thunk = Alloc::alloc(tycker, ss::Thunk(body_out), thunk_app_body_ty);
TermAnnId::Value(thunk, thunk_app_body_ty)
}
Expand All @@ -1505,7 +1505,7 @@ impl Tyck for SEnv<su::TermId> {
match switch {
| Switch::Syn => {
// if syn, then ana the body with thunk_app_hole
let thunk_app_hole = tycker.thunk_app_hole(&self.env, body);
let thunk_app_hole = tycker.thunk_hole(&self.env, body);
thunk_app_hole
}
| Switch::Ana(ana) => {
Expand All @@ -1521,7 +1521,7 @@ impl Tyck for SEnv<su::TermId> {
let ana_ty_kd = tycker.statics.annotations_type[&ana_ty].to_owned();
Lub::lub_k(ctype, ana_ty_kd, tycker)?;
// if ana, then ana the body with thunked body_ty
tycker.thunk_app(&self.env, ana_ty)
tycker.thunk_arg(&self.env, ana_ty)
}
}
};
Expand Down Expand Up @@ -1549,13 +1549,13 @@ impl Tyck for SEnv<su::TermId> {
| Tm::Ret(term) => {
let su::Ret(body) = term;
let ana = match switch {
| Switch::Syn => tycker.ret_app_hole(&self.env, self.inner).into(),
| Switch::Syn => tycker.ret_hole(&self.env, self.inner).into(),
| Switch::Ana(ana) => ana,
};
let AnnId::Type(ana_ty) = ana else {
tycker.err_k(TyckError::SortMismatch, std::panic::Location::caller())?
};
let ret_app_hole = tycker.ret_app_hole(&self.env, self.inner);
let ret_app_hole = tycker.ret_hole(&self.env, self.inner);
let ty = Lub::lub_k(ana_ty, ret_app_hole, tycker)?;
let ss::Type::App(ret_app_body_ty) = tycker.statics.types[&ty].to_owned() else {
unreachable!()
Expand All @@ -1567,19 +1567,15 @@ impl Tyck for SEnv<su::TermId> {
TyckError::SortMismatch,
std::panic::Location::caller(),
)?;
let ret_app_body_ty = {
let ret_ty = tycker.ret(&self.env);
let ctype = tycker.ctype(&self.env);
Alloc::alloc(tycker, ss::App(ret_ty, body_ty), ctype)
};
let ret_app_body_ty = tycker.ret_arg(&self.env, body_ty);
let ret = Alloc::alloc(tycker, ss::Ret(body_out), ret_app_body_ty);
TermAnnId::Compu(ret, ret_app_body_ty)
}
| Tm::Do(term) => {
let su::Bind { binder, bindee, tail } = term;
// first, ana bindee with ret_app_hole, and we get a compu that should be ret_app_body_ty
let (bindee_out, bindee_ty) = {
let ret_app_hole = tycker.ret_app_hole(&self.env, bindee);
let ret_app_hole = tycker.ret_hole(&self.env, bindee);
let bindee_out_ann =
self.mk(bindee).tyck(tycker, Action::ana(ret_app_hole.into()))?;
bindee_out_ann.try_as_compu(
Expand Down

0 comments on commit 6349201

Please sign in to comment.