From 63492015b964b798bbb43f47165e66b2629447a9 Mon Sep 17 00:00:00 2001 From: Yuchen Date: Wed, 3 Jul 2024 14:46:57 -0400 Subject: [PATCH] cleanup --- lang/statics/src/lift.rs | 30 +++++++++++++++--------------- lang/statics/src/prims.rs | 29 ++++++++++++++++++----------- lang/statics/src/tyck.rs | 24 ++++++++++-------------- 3 files changed, 43 insertions(+), 40 deletions(-) diff --git a/lang/statics/src/lift.rs b/lang/statics/src/lift.rs index 2a28f16c..d05ae703 100644 --- a/lang/statics/src/lift.rs +++ b/lang/statics/src/lift.rs @@ -82,7 +82,7 @@ impl SEnv { /// 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 { let ctype = tycker.ctype(&self.env); let res = match tycker.statics.kinds[&self.inner].to_owned() { @@ -95,7 +95,7 @@ impl SEnv { 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) } @@ -270,7 +270,7 @@ impl SEnv { // 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); @@ -279,7 +279,7 @@ impl SEnv { // 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); @@ -309,7 +309,7 @@ impl SEnv { 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( @@ -421,7 +421,7 @@ impl SEnv { 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) }; @@ -492,7 +492,7 @@ impl SEnv { 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) }; @@ -701,7 +701,7 @@ impl SEnv { 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) @@ -717,7 +717,7 @@ impl SEnv { 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); @@ -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) } @@ -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` @@ -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) } @@ -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()); @@ -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()); diff --git a/lang/statics/src/prims.rs b/lang/statics/src/prims.rs index ae9078e4..c787afff 100644 --- a/lang/statics/src/prims.rs +++ b/lang/statics/src/prims.rs @@ -1,6 +1,7 @@ use crate::{syntax::*, *}; use zydeco_utils::arena::ArenaAccess; +/* ---------------------------------- Kind ---------------------------------- */ impl Tycker { pub fn vtype(&mut self, env: &Env) -> KindId { let AnnId::Kind(kd) = env[self.prim.vtype.get()] else { unreachable!() }; @@ -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) -> TypeId { let AnnId::Type(ty) = env[self.prim.thunk.get()] else { unreachable!() }; ty } - pub fn thunk_app(&mut self, env: &Env, arg: TypeId) -> TypeId { + /// generates `Thunk B` + pub fn thunk_arg(&mut self, env: &Env, 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, 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, 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) -> TypeId { let AnnId::Type(ty) = env[self.prim.ret.get()] else { unreachable!() }; ty } - pub fn ret_app_hole(&mut self, env: &Env, 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, 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, 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) -> TypeId { let AnnId::Type(ty) = env[self.prim.unit.get()] else { unreachable!() }; diff --git a/lang/statics/src/tyck.rs b/lang/statics/src/tyck.rs index 850dc816..12819259 100644 --- a/lang/statics/src/tyck.rs +++ b/lang/statics/src/tyck.rs @@ -1200,7 +1200,7 @@ impl Tyck for SEnv { 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, @@ -1477,13 +1477,13 @@ impl Tyck for SEnv { | 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!() @@ -1495,7 +1495,7 @@ impl Tyck for SEnv { 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) } @@ -1505,7 +1505,7 @@ impl Tyck for SEnv { 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) => { @@ -1521,7 +1521,7 @@ impl Tyck for SEnv { 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) } } }; @@ -1549,13 +1549,13 @@ impl Tyck for SEnv { | 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!() @@ -1567,11 +1567,7 @@ impl Tyck for SEnv { 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) } @@ -1579,7 +1575,7 @@ impl Tyck for SEnv { 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(