From d995ded9b2ced9e4341562a0f3f771012bb3f330 Mon Sep 17 00:00:00 2001 From: Myriad-Dreamin <35292584+Myriad-Dreamin@users.noreply.github.com> Date: Wed, 15 May 2024 18:42:06 +0800 Subject: [PATCH] =?UTF-8?q?feat:=20implement=20naive=20substitution=20(?= =?UTF-8?q?=CE=B2-reduction)=20(#292)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * feat: implement naive substitution (β-reduction) * fix: order * dev: harder tests --- .../tinymist-query/src/analysis/signature.rs | 2 +- .../tinymist-query/src/analysis/ty/apply.rs | 6 +- .../tinymist-query/src/analysis/ty/syntax.rs | 4 +- .../type_check/snaps/test@with.typ.snap | 10 +- .../src/fixtures/type_check/with.typ | 3 +- crates/tinymist-query/src/ty/builtin.rs | 21 ++ crates/tinymist-query/src/ty/def.rs | 144 ++++++++---- crates/tinymist-query/src/ty/mod.rs | 18 +- crates/tinymist-query/src/ty/mutate.rs | 207 ++++++++++++++++++ crates/tinymist-query/src/ty/subst.rs | 108 ++++++++- 10 files changed, 455 insertions(+), 68 deletions(-) create mode 100644 crates/tinymist-query/src/ty/mutate.rs diff --git a/crates/tinymist-query/src/analysis/signature.rs b/crates/tinymist-query/src/analysis/signature.rs index d2dba032..0719a9b2 100644 --- a/crates/tinymist-query/src/analysis/signature.rs +++ b/crates/tinymist-query/src/analysis/signature.rs @@ -389,7 +389,7 @@ fn analyze_dyn_signature_inner(func: Func) -> Arc { let sig_ty = SigTy::new( pos.iter().map(|e| e.base_type.clone().unwrap_or(Ty::Any)), - named_vec.into_iter(), + named_vec, rest.as_ref() .map(|e| e.base_type.clone().unwrap_or(Ty::Any)), ret_ty.clone(), diff --git a/crates/tinymist-query/src/analysis/ty/apply.rs b/crates/tinymist-query/src/analysis/ty/apply.rs index 1caad0dc..8d076c75 100644 --- a/crates/tinymist-query/src/analysis/ty/apply.rs +++ b/crates/tinymist-query/src/analysis/ty/apply.rs @@ -37,8 +37,10 @@ impl<'a, 'b, 'w> ApplyChecker for ApplyTypeChecker<'a, 'b, 'w> { sig => (sig, false), }; - if let Some(ty) = sig.call(args, pol, Some(self.base.ctx)) { - self.resultant.push(ty); + if !is_partialize { + if let Some(ty) = sig.call(args, pol, Some(self.base.ctx)) { + self.resultant.push(ty); + } } // todo: remove this after we implemented dependent types diff --git a/crates/tinymist-query/src/analysis/ty/syntax.rs b/crates/tinymist-query/src/analysis/ty/syntax.rs index 0a11e4a3..713416c0 100644 --- a/crates/tinymist-query/src/analysis/ty/syntax.rs +++ b/crates/tinymist-query/src/analysis/ty/syntax.rs @@ -353,7 +353,7 @@ impl<'a, 'w> TypeChecker<'a, 'w> { } } - let args = ArgsTy::new(args_res.into_iter(), named.into_iter(), None, None); + let args = ArgsTy::new(args_res, named, None, None); Some(Ty::Args(args.into())) } @@ -408,7 +408,7 @@ impl<'a, 'w> TypeChecker<'a, 'w> { self.weaken(rest); } - let sig = SigTy::new(pos.into_iter(), named.into_iter(), rest, Some(body)); + let sig = SigTy::new(pos, named, rest, Some(body)); Some(Ty::Func(sig.into())) } diff --git a/crates/tinymist-query/src/fixtures/type_check/snaps/test@with.typ.snap b/crates/tinymist-query/src/fixtures/type_check/snaps/test@with.typ.snap index 0213a9ae..ac9d8b6f 100644 --- a/crates/tinymist-query/src/fixtures/type_check/snaps/test@with.typ.snap +++ b/crates/tinymist-query/src/fixtures/type_check/snaps/test@with.typ.snap @@ -4,8 +4,9 @@ expression: result input_file: crates/tinymist-query/src/fixtures/type_check/with.typ --- "f" = (Any) => Any -"g" = (Any | ((Any) => Any).with(..(1) => any)) -"x" = ( ⪰ Any | Type(integer)) +"g" = ((Any) => Any).with(..(1) => any) +"x" = ( ⪰ Any | Type(integer) | Type(integer)) +"x" = 1 --- 5..6 -> @f 7..8 -> @x @@ -13,4 +14,7 @@ input_file: crates/tinymist-query/src/fixtures/type_check/with.typ 20..21 -> @g 24..25 -> @f 24..30 -> (@x) => @x -24..33 -> (@x | ((@x) => @x).with(..(1) => any)) +24..33 -> ((@x) => @x).with(..(1) => any) +40..41 -> @x +44..45 -> (@g | Any) +44..47 -> 1 diff --git a/crates/tinymist-query/src/fixtures/type_check/with.typ b/crates/tinymist-query/src/fixtures/type_check/with.typ index 7b054489..2d6f7f97 100644 --- a/crates/tinymist-query/src/fixtures/type_check/with.typ +++ b/crates/tinymist-query/src/fixtures/type_check/with.typ @@ -1,2 +1,3 @@ #let f(x) = x; -#let g = f.with(1); \ No newline at end of file +#let g = f.with(1); +#let x = g() \ No newline at end of file diff --git a/crates/tinymist-query/src/ty/builtin.rs b/crates/tinymist-query/src/ty/builtin.rs index 01bc5af9..63dd7db2 100644 --- a/crates/tinymist-query/src/ty/builtin.rs +++ b/crates/tinymist-query/src/ty/builtin.rs @@ -506,3 +506,24 @@ pub static FLOW_RADIUS_DICT: Lazy> = Lazy::new(|| { // todo: csv.row-type can be an array or a dictionary // ISO 639 + +#[cfg(test)] +mod tests { + use reflexo::vector::ir::DefId; + + use super::*; + + // todo: map function + // Technical Note for implementing a map function: + // `u`, `v` is in level 2 + // instantiate a `v` as the return type of the map function. + #[test] + fn test_map() { + let u = Ty::Var(TypeVar::new("u".into(), DefId(0))); + let v = Ty::Var(TypeVar::new("v".into(), DefId(1))); + let mapper_fn = Ty::Func(SigTy::new([u], None, None, Some(v.clone())).into()); + let map_fn = Ty::Func(SigTy::new([mapper_fn], None, None, Some(v)).into()); + let _ = map_fn; + // println!("{map_fn:?}"); + } +} diff --git a/crates/tinymist-query/src/ty/def.rs b/crates/tinymist-query/src/ty/def.rs index e54127fa..40c419a3 100644 --- a/crates/tinymist-query/src/ty/def.rs +++ b/crates/tinymist-query/src/ty/def.rs @@ -111,6 +111,23 @@ impl TypeSource { pub trait TypeInterace { fn bone(&self) -> &Interned; fn interface(&self) -> impl Iterator, &Ty)>; + fn field_by_bone_offset(&self, i: usize) -> Option<&Ty>; + + fn common_iface_fields<'a>( + &'a self, + rhs: &'a Self, + ) -> impl Iterator, &'a Ty, &'a Ty)> { + let lhs_names = self.bone(); + let rhs_names = rhs.bone(); + + lhs_names + .intersect_keys_enumerate(rhs_names) + .filter_map(move |(i, j)| { + let lhs = self.field_by_bone_offset(i)?; + let rhs = rhs.field_by_bone_offset(j)?; + Some((&lhs_names.names[i], lhs, rhs)) + }) + } } struct RefDebug<'a>(&'a Ty); @@ -404,6 +421,10 @@ impl TypeInterace for RecordTy { &self.names } + fn field_by_bone_offset(&self, i: usize) -> Option<&Ty> { + self.types.get(i) + } + fn interface(&self) -> impl Iterator, &Ty)> { self.names.names.iter().zip(self.types.iter()) } @@ -496,19 +517,20 @@ impl SigTy { } pub(crate) fn new( - pos: impl Iterator, - named: impl Iterator, Ty)>, + pos: impl IntoIterator, + named: impl IntoIterator, Ty)>, rest: Option, ret_ty: Option, ) -> Self { let named = named + .into_iter() .map(|(name, ty)| (name, ty, Span::detached())) .collect::>(); let (names, types) = RecordTy::shape_fields(named); let spread_right = rest.is_some(); let name_started = if spread_right { 1 } else { 0 } + types.len(); - let types = pos.chain(types).chain(rest).collect::>(); + let types = pos.into_iter().chain(types).chain(rest).collect::>(); let name_started = (types.len() - name_started) as u32; @@ -541,6 +563,22 @@ impl Default for SigTy { } } +impl TypeInterace for SigTy { + fn bone(&self) -> &Interned { + &self.names + } + + fn interface(&self) -> impl Iterator, &Ty)> { + let names = self.names.names.iter(); + let types = self.types.iter().skip(self.name_started as usize); + names.zip(types) + } + + fn field_by_bone_offset(&self, i: usize) -> Option<&Ty> { + self.types.get(i + self.name_started as usize) + } +} + impl SigTy { pub fn positional_params(&self) -> impl ExactSizeIterator { self.types.iter().take(self.name_started as usize) @@ -575,37 +613,42 @@ impl SigTy { pub(crate) fn matches<'a>( &'a self, args: &'a SigTy, - withs: Option<&Vec>>, + withs: Option<&'a Vec>>, ) -> impl Iterator + 'a { let with_len = withs .map(|w| w.iter().map(|w| w.positional_params().len()).sum::()) .unwrap_or(0); - let sig_pos = self.positional_params().skip(with_len); + let sig_pos = self.positional_params(); let arg_pos = args.positional_params(); let sig_rest = self.rest_param(); let arg_rest = args.rest_param(); - let max_len = sig_pos.len().max(arg_pos.len()) + let max_len = sig_pos.len().max(with_len + arg_pos.len()) + if sig_rest.is_some() && arg_rest.is_some() { 1 } else { 0 }; + let arg_pos = withs + .into_iter() + .flat_map(|w| w.iter().rev().map(|w| w.positional_params())) + .flatten() + .chain(arg_pos); + let sig_stream = sig_pos.chain(sig_rest.into_iter().cycle()).take(max_len); let arg_stream = arg_pos.chain(arg_rest.into_iter().cycle()).take(max_len); let mut pos = sig_stream.zip(arg_stream); - let mut named = - self.names - .intersect_keys_enumerate(&args.names) - .filter_map(move |(i, j)| { - let lhs = self.types.get(i + self.name_started as usize)?; - let rhs = args.types.get(j + args.name_started as usize)?; - Some((lhs, rhs)) - }); + let common_ifaces = withs + .map(|e| e.iter().rev()) + .into_iter() + .flatten() + .flat_map(|w| self.common_iface_fields(w)) + .chain(self.common_iface_fields(args)); + let mut named = common_ifaces.map(|(n, l, r)| (l, r)); pos.chain(named) } @@ -890,45 +933,60 @@ mod tests { format!("{res:?}") } - assert_snapshot!(matches(literal_sig!(p1), literal_sig!(q1), None), @r###"[("p1", "q1")]"###); - assert_snapshot!(matches(literal_sig!(p1, p2), literal_sig!(q1), None), @r###"[("p1", "q1")]"###); - assert_snapshot!(matches(literal_sig!(p1, p2), literal_sig!(q1, q2), None), @r###"[("p1", "q1"), ("p2", "q2")]"###); - assert_snapshot!(matches(literal_sig!(p1), literal_sig!(q1, q2), None), @r###"[("p1", "q1")]"###); + assert_snapshot!(matches(literal_sig!(p1), literal_sig!(q1), None), @"[(@p1, @q1)]"); + assert_snapshot!(matches(literal_sig!(p1, p2), literal_sig!(q1), None), @"[(@p1, @q1)]"); + assert_snapshot!(matches(literal_sig!(p1, p2), literal_sig!(q1, q2), None), @"[(@p1, @q1), (@p2, @q2)]"); + assert_snapshot!(matches(literal_sig!(p1), literal_sig!(q1, q2), None), @"[(@p1, @q1)]"); - assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q1), None), @r###"[("p1", "q1")]"###); - assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q1, q2), None), @r###"[("p1", "q1"), ("r1", "q2")]"###); - assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q1, q2, q3), None), @r###"[("p1", "q1"), ("r1", "q2"), ("r1", "q3")]"###); - assert_snapshot!(matches(literal_sig!(...r1), literal_sig!(q1, q2), None), @r###"[("r1", "q1"), ("r1", "q2")]"###); + assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q1), None), @"[(@p1, @q1)]"); + assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q1, q2), None), @"[(@p1, @q1), (@r1, @q2)]"); + assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q1, q2, q3), None), @"[(@p1, @q1), (@r1, @q2), (@r1, @q3)]"); + assert_snapshot!(matches(literal_sig!(...r1), literal_sig!(q1, q2), None), @"[(@r1, @q1), (@r1, @q2)]"); - assert_snapshot!(matches(literal_sig!(p1), literal_sig!(q1, ...s2), None), @r###"[("p1", "q1")]"###); - assert_snapshot!(matches(literal_sig!(p1, p2), literal_sig!(q1, ...s2), None), @r###"[("p1", "q1"), ("p2", "s2")]"###); - assert_snapshot!(matches(literal_sig!(p1, p2, p3), literal_sig!(q1, ...s2), None), @r###"[("p1", "q1"), ("p2", "s2"), ("p3", "s2")]"###); - assert_snapshot!(matches(literal_sig!(p1, p2), literal_sig!(...s2), None), @r###"[("p1", "s2"), ("p2", "s2")]"###); + assert_snapshot!(matches(literal_sig!(p1), literal_sig!(q1, ...s2), None), @"[(@p1, @q1)]"); + assert_snapshot!(matches(literal_sig!(p1, p2), literal_sig!(q1, ...s2), None), @"[(@p1, @q1), (@p2, @s2)]"); + assert_snapshot!(matches(literal_sig!(p1, p2, p3), literal_sig!(q1, ...s2), None), @"[(@p1, @q1), (@p2, @s2), (@p3, @s2)]"); + assert_snapshot!(matches(literal_sig!(p1, p2), literal_sig!(...s2), None), @"[(@p1, @s2), (@p2, @s2)]"); - assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q1, ...s2), None), @r###"[("p1", "q1"), ("r1", "s2")]"###); - assert_snapshot!(matches(literal_sig!(...r1), literal_sig!(q1, ...s2), None), @r###"[("r1", "q1"), ("r1", "s2")]"###); - assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(...s2), None), @r###"[("p1", "s2"), ("r1", "s2")]"###); - assert_snapshot!(matches(literal_sig!(...r1), literal_sig!(...s2), None), @r###"[("r1", "s2")]"###); + assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q1, ...s2), None), @"[(@p1, @q1), (@r1, @s2)]"); + assert_snapshot!(matches(literal_sig!(...r1), literal_sig!(q1, ...s2), None), @"[(@r1, @q1), (@r1, @s2)]"); + assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(...s2), None), @"[(@p1, @s2), (@r1, @s2)]"); + assert_snapshot!(matches(literal_sig!(...r1), literal_sig!(...s2), None), @"[(@r1, @s2)]"); - assert_snapshot!(matches(literal_sig!(p0, p1, ...r1), literal_sig!(q1, ...s2), None), @r###"[("p0", "q1"), ("p1", "s2"), ("r1", "s2")]"###); - assert_snapshot!(matches(literal_sig!(p0, p1, ...r1), literal_sig!(...s2), None), @r###"[("p0", "s2"), ("p1", "s2"), ("r1", "s2")]"###); + assert_snapshot!(matches(literal_sig!(p0, p1, ...r1), literal_sig!(q1, ...s2), None), @"[(@p0, @q1), (@p1, @s2), (@r1, @s2)]"); + assert_snapshot!(matches(literal_sig!(p0, p1, ...r1), literal_sig!(...s2), None), @"[(@p0, @s2), (@p1, @s2), (@r1, @s2)]"); - assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q0, q1, ...s2), None), @r###"[("p1", "q0"), ("r1", "q1"), ("r1", "s2")]"###); - assert_snapshot!(matches(literal_sig!(...r1), literal_sig!(q0, q1, ...s2), None), @r###"[("r1", "q0"), ("r1", "q1"), ("r1", "s2")]"###); + assert_snapshot!(matches(literal_sig!(p1, ...r1), literal_sig!(q0, q1, ...s2), None), @"[(@p1, @q0), (@r1, @q1), (@r1, @s2)]"); + assert_snapshot!(matches(literal_sig!(...r1), literal_sig!(q0, q1, ...s2), None), @"[(@r1, @q0), (@r1, @q1), (@r1, @s2)]"); - assert_snapshot!(matches(literal_sig!(p1 !u1: w1), literal_sig!(q1 !u1: w2), None), @r###"[("p1", "q1"), ("w1", "w2")]"###); - assert_snapshot!(matches(literal_sig!(p1 !u1: w1, ...r1), literal_sig!(q1 !u1: w2), None), @r###"[("p1", "q1"), ("w1", "w2")]"###); - assert_snapshot!(matches(literal_sig!(p1 !u1: w1), literal_sig!(q1 !u1: w2, ...s2), None), @r###"[("p1", "q1"), ("w1", "w2")]"###); - assert_snapshot!(matches(literal_sig!(p1 !u1: w1, ...r1), literal_sig!(q1 !u1: w2, ...s2), None), @r###"[("p1", "q1"), ("r1", "s2"), ("w1", "w2")]"###); + assert_snapshot!(matches(literal_sig!(p1 !u1: w1), literal_sig!(q1 !u1: w2), None), @"[(@p1, @q1), (@w1, @w2)]"); + assert_snapshot!(matches(literal_sig!(p1 !u1: w1, ...r1), literal_sig!(q1 !u1: w2), None), @"[(@p1, @q1), (@w1, @w2)]"); + assert_snapshot!(matches(literal_sig!(p1 !u1: w1), literal_sig!(q1 !u1: w2, ...s2), None), @"[(@p1, @q1), (@w1, @w2)]"); + assert_snapshot!(matches(literal_sig!(p1 !u1: w1, ...r1), literal_sig!(q1 !u1: w2, ...s2), None), @"[(@p1, @q1), (@r1, @s2), (@w1, @w2)]"); assert_snapshot!(matches(literal_sig!(), literal_sig!(!u1: w2), None), @"[]"); assert_snapshot!(matches(literal_sig!(!u1: w1), literal_sig!(), None), @"[]"); - assert_snapshot!(matches(literal_sig!(!u1: w1), literal_sig!(!u1: w2), None), @r###"[("w1", "w2")]"###); + assert_snapshot!(matches(literal_sig!(!u1: w1), literal_sig!(!u1: w2), None), @"[(@w1, @w2)]"); assert_snapshot!(matches(literal_sig!(!u1: w1), literal_sig!(!u2: w2), None), @"[]"); assert_snapshot!(matches(literal_sig!(!u2: w1), literal_sig!(!u1: w2), None), @"[]"); - assert_snapshot!(matches(literal_sig!(!u1: w1, !u2: w3), literal_sig!(!u1: w2, !u2: w4), None), @r###"[("w1", "w2"), ("w3", "w4")]"###); - assert_snapshot!(matches(literal_sig!(!u1: w1, !u2: w3), literal_sig!(!u2: w2, !u1: w4), None), @r###"[("w1", "w4"), ("w3", "w2")]"###); - assert_snapshot!(matches(literal_sig!(!u2: w1), literal_sig!(!u1: w2, !u2: w4), None), @r###"[("w1", "w4")]"###); - assert_snapshot!(matches(literal_sig!(!u1: w1, !u2: w2), literal_sig!(!u2: w4), None), @r###"[("w2", "w4")]"###); + assert_snapshot!(matches(literal_sig!(!u1: w1, !u2: w3), literal_sig!(!u1: w2, !u2: w4), None), @"[(@w1, @w2), (@w3, @w4)]"); + assert_snapshot!(matches(literal_sig!(!u1: w1, !u2: w3), literal_sig!(!u2: w2, !u1: w4), None), @"[(@w1, @w4), (@w3, @w2)]"); + assert_snapshot!(matches(literal_sig!(!u2: w1), literal_sig!(!u1: w2, !u2: w4), None), @"[(@w1, @w4)]"); + assert_snapshot!(matches(literal_sig!(!u1: w1, !u2: w2), literal_sig!(!u2: w4), None), @"[(@w2, @w4)]"); + + assert_snapshot!(matches(literal_sig!(p1 !u1: w1, !u2: w2), literal_sig!(q1), Some(vec![ + literal_sig!(!u2: w6), + ])), @"[(@p1, @q1), (@w2, @w6)]"); + assert_snapshot!(matches(literal_sig!(p1 !u1: w1, !u2: w2), literal_sig!(q1 !u2: w4), Some(vec![ + literal_sig!(!u2: w5), + ])), @"[(@p1, @q1), (@w2, @w5), (@w2, @w4)]"); + assert_snapshot!(matches(literal_sig!(p1 !u1: w1, !u2: w2), literal_sig!(q1 ), Some(vec![ + literal_sig!(!u2: w7), + literal_sig!(!u2: w8), + ])), @"[(@p1, @q1), (@w2, @w8), (@w2, @w7)]"); + assert_snapshot!(matches(literal_sig!(p1, p2, p3), literal_sig!(q1), Some(vec![ + literal_sig!(q2), + literal_sig!(q3), + ])), @"[(@p1, @q3), (@p2, @q2), (@p3, @q1)]"); } } diff --git a/crates/tinymist-query/src/ty/mod.rs b/crates/tinymist-query/src/ty/mod.rs index f20d49e0..4193ff45 100644 --- a/crates/tinymist-query/src/ty/mod.rs +++ b/crates/tinymist-query/src/ty/mod.rs @@ -5,6 +5,7 @@ mod bound; mod builtin; mod def; mod describe; +mod mutate; mod sig; mod simplify; mod subst; @@ -13,16 +14,18 @@ pub(crate) use apply::*; pub(crate) use bound::*; pub(crate) use builtin::*; pub(crate) use def::*; +pub(crate) use mutate::*; pub(crate) use sig::*; #[cfg(test)] mod tests { use super::*; use crate::adt::interner::Interned; - use typst::foundations::Value; + use fxhash::hash64; + use reflexo::vector::ir::DefId; - pub fn str_ins(s: &str) -> Ty { - Ty::Value(InsTy::new(Value::Str(s.into()))) + pub fn var_ins(s: &str) -> Ty { + Ty::Var(TypeVar::new(s.into(), DefId(hash64(s)))) } pub fn str_sig( @@ -31,10 +34,10 @@ mod tests { rest: Option<&str>, ret: Option<&str>, ) -> Interned { - let pos = pos.iter().map(|s| str_ins(s)); - let named = named.iter().map(|(n, t)| ((*n).into(), str_ins(t))); - let rest = rest.map(str_ins); - let ret = ret.map(str_ins); + let pos = pos.iter().map(|s| var_ins(s)); + let named = named.iter().map(|(n, t)| ((*n).into(), var_ins(t))); + let rest = rest.map(var_ins); + let ret = ret.map(var_ins); SigTy::new(pos, named, rest, ret).into() } @@ -55,4 +58,5 @@ mod tests { } pub(crate) use literal_sig; + pub(crate) use literal_sig as literal_args; } diff --git a/crates/tinymist-query/src/ty/mutate.rs b/crates/tinymist-query/src/ty/mutate.rs new file mode 100644 index 00000000..8c1263e1 --- /dev/null +++ b/crates/tinymist-query/src/ty/mutate.rs @@ -0,0 +1,207 @@ +use crate::{adt::interner::Interned, ty::def::*}; + +pub trait MutateDriver { + fn mutate(&mut self, ty: &Ty, pol: bool) -> Option; + + fn mutate_vec(&mut self, ty: &[Ty], pol: bool) -> Option>> { + let mut mutated = false; + + let mut types = Vec::with_capacity(ty.len()); + for ty in ty.iter() { + match self.mutate(ty, pol) { + Some(ty) => { + types.push(ty); + mutated = true; + } + None => types.push(ty.clone()), + } + } + + if mutated { + Some(types.into()) + } else { + None + } + } + + fn mutate_option(&mut self, ty: Option<&Ty>, pol: bool) -> Option> { + match ty { + Some(ty) => self.mutate(ty, pol).map(Some), + None => None, + } + } + + fn mutate_func(&mut self, ty: &Interned, pol: bool) -> Option { + let types = self.mutate_vec(&ty.types, pol); + let ret = self.mutate_option(ty.ret.as_ref(), pol); + + if types.is_none() && ret.is_none() { + return None; + } + + let sig = ty.as_ref().clone(); + let types = types.unwrap_or_else(|| ty.types.clone()); + let ret = ret.unwrap_or_else(|| ty.ret.clone()); + Some(SigTy { types, ret, ..sig }) + } + + fn mutate_record(&mut self, ty: &Interned, pol: bool) -> Option { + let types = self.mutate_vec(&ty.types, pol)?; + + let rec = ty.as_ref().clone(); + Some(RecordTy { types, ..rec }) + } + + fn mutate_with_sig(&mut self, ty: &Interned, pol: bool) -> Option { + let sig = self.mutate(ty.sig.as_ref(), pol); + let with = self.mutate_func(&ty.with, pol); + + if sig.is_none() && with.is_none() { + return None; + } + + let sig = sig.map(Interned::new).unwrap_or_else(|| ty.sig.clone()); + let with = with.map(Interned::new).unwrap_or_else(|| ty.with.clone()); + + Some(SigWithTy { sig, with }) + } + + fn mutate_unary(&mut self, ty: &Interned, pol: bool) -> Option { + let lhs = self.mutate(ty.lhs.as_ref(), pol)?.into(); + + Some(TypeUnary { lhs, op: ty.op }) + } + + fn mutate_binary(&mut self, ty: &Interned, pol: bool) -> Option { + let (lhs, rhs) = &ty.operands; + + let x = self.mutate(lhs, pol); + let y = self.mutate(rhs, pol); + + if x.is_none() && y.is_none() { + return None; + } + + let lhs = x.map(Interned::new).unwrap_or_else(|| lhs.clone()); + let rhs = y.map(Interned::new).unwrap_or_else(|| rhs.clone()); + + Some(TypeBinary { + operands: (lhs, rhs), + op: ty.op, + }) + } + + fn mutate_if(&mut self, ty: &Interned, pol: bool) -> Option { + let cond = self.mutate(ty.cond.as_ref(), pol); + let then = self.mutate(ty.then.as_ref(), pol); + let else_ = self.mutate(ty.else_.as_ref(), pol); + + if cond.is_none() && then.is_none() && else_.is_none() { + return None; + } + + let cond = cond.map(Interned::new).unwrap_or_else(|| ty.cond.clone()); + let then = then.map(Interned::new).unwrap_or_else(|| ty.then.clone()); + let else_ = else_.map(Interned::new).unwrap_or_else(|| ty.else_.clone()); + + Some(IfTy { cond, then, else_ }) + } + + fn mutate_select(&mut self, ty: &Interned, pol: bool) -> Option { + let target = self.mutate(ty.ty.as_ref(), pol)?.into(); + + Some(SelectTy { + ty: target, + select: ty.select.clone(), + }) + } +} + +impl MutateDriver for T +where + T: FnMut(&Ty, bool) -> Option, +{ + fn mutate(&mut self, ty: &Ty, pol: bool) -> Option { + self(ty, pol) + } +} + +impl Ty { + pub fn mutate(&self, pol: bool, checker: &mut impl MutateDriver) -> Option { + let mut worker = Mutator; + worker.ty(self, pol, checker) + } +} + +struct Mutator; + +impl Mutator { + fn ty(&mut self, ty: &Ty, pol: bool, mutator: &mut impl MutateDriver) -> Option { + match ty { + Ty::Func(f) => { + let f = mutator.mutate_func(f, pol)?; + Some(Ty::Func(f.into())) + } + Ty::Dict(r) => { + let r = mutator.mutate_record(r, pol)?; + Some(Ty::Dict(r.into())) + } + Ty::Tuple(e) => { + let e = mutator.mutate_vec(e, pol)?; + Some(Ty::Tuple(e)) + } + Ty::Array(e) => { + let ty = mutator.mutate(e, pol)?; + Some(Ty::Array(ty.into())) + } + Ty::With(w) => { + let w = mutator.mutate_with_sig(w, pol)?; + Some(Ty::With(w.into())) + } + Ty::Args(args) => { + let args = mutator.mutate_func(args, pol)?; + Some(Ty::Args(args.into())) + } + Ty::Unary(u) => { + let u = mutator.mutate_unary(u, pol)?; + Some(Ty::Unary(u.into())) + } + Ty::Binary(b) => { + let b = mutator.mutate_binary(b, pol)?; + Some(Ty::Binary(b.into())) + } + Ty::If(i) => { + let i = mutator.mutate_if(i, pol)?; + Some(Ty::If(i.into())) + } + Ty::Union(v) => { + let v = mutator.mutate_vec(v, pol)?; + Some(Ty::Union(v)) + } + Ty::Field(f) => { + let field = f.field.mutate(pol, mutator)?; + let mut f = f.as_ref().clone(); + f.field = field; + Some(Ty::Field(f.into())) + } + Ty::Select(s) => { + let s = mutator.mutate_select(s, pol)?; + Some(Ty::Select(s.into())) + } + Ty::Var(..) + | Ty::Let(..) + | Ty::Value(..) + | Ty::Clause + | Ty::Undef + | Ty::Content + | Ty::Any + | Ty::None + | Ty::Infer + | Ty::FlowNone + | Ty::Space + | Ty::Auto + | Ty::Boolean(..) + | Ty::Builtin(..) => mutator.mutate(ty, pol), + } + } +} diff --git a/crates/tinymist-query/src/ty/subst.rs b/crates/tinymist-query/src/ty/subst.rs index d25801b6..3ba7fb81 100644 --- a/crates/tinymist-query/src/ty/subst.rs +++ b/crates/tinymist-query/src/ty/subst.rs @@ -15,8 +15,11 @@ impl<'a> Sig<'a> { return body; } + let body = body?; + + // Substitute the bound variables in the body or just body let mut checker = SubstituteChecker { bound_variables }; - checker.ty(&body?, pol) + Some(checker.ty(&body, pol).unwrap_or(body)) } pub fn check_bind( @@ -26,11 +29,13 @@ impl<'a> Sig<'a> { ) -> Option<(HashMap, Option)> { let SigShape { sig, withs } = self.shape(ctx)?; - let has_free_vars = sig.has_free_variables; + // todo: check if the signature has free variables + // let has_free_vars = sig.has_free_variables; + let has_free_vars = true; let mut arguments = HashMap::new(); - for (arg_recv, arg_ins) in sig.matches(args, withs) { - if has_free_vars { + if has_free_vars { + for (arg_recv, arg_ins) in sig.matches(args, withs) { if let Ty::Var(arg_recv) = arg_recv { arguments.insert(arg_recv.def, arg_ins.clone()); } @@ -41,15 +46,100 @@ impl<'a> Sig<'a> { } } -// todo struct SubstituteChecker { bound_variables: HashMap, } + impl SubstituteChecker { fn ty(&mut self, body: &Ty, pol: bool) -> Option { - let _ = self.bound_variables; - let _ = pol; - - Some(body.clone()) + body.mutate(pol, self) + } +} + +impl MutateDriver for SubstituteChecker { + fn mutate(&mut self, ty: &Ty, pol: bool) -> Option { + // todo: extrude the type into a polarized type + let _ = pol; + + Some(match ty { + // todo: substitute the bound in the type + Ty::Let(..) => return None, + Ty::Var(v) => { + if let Some(ty) = self.bound_variables.get(&v.def) { + ty.clone() + } else { + return None; + } + } + Ty::Value(..) + | Ty::Clause + | Ty::Undef + | Ty::Content + | Ty::Any + | Ty::None + | Ty::Infer + | Ty::FlowNone + | Ty::Space + | Ty::Auto + | Ty::Boolean(..) + | Ty::Builtin(..) => return None, + _ => return None, + }) + } +} + +#[cfg(test)] +mod tests { + use insta::{assert_debug_snapshot, assert_snapshot}; + + use crate::ty::tests::*; + + use super::{ApplyChecker, Ty}; + #[test] + fn test_ty() { + use super::*; + let ty = Ty::Clause; + let ty_ref = TyRef::new(ty.clone()); + assert_debug_snapshot!(ty_ref, @"Clause"); + } + + #[derive(Default)] + struct CallCollector(Vec); + + impl ApplyChecker for CallCollector { + fn call( + &mut self, + sig: super::Sig, + arguments: &crate::adt::interner::Interned, + pol: bool, + ) { + let ty = sig.call(arguments, pol, None); + if let Some(ty) = ty { + self.0.push(ty); + } + } + } + + #[test] + fn test_sig_call() { + use super::*; + + fn call(sig: Interned, args: Interned) -> String { + let sig_ty = Ty::Func(sig); + let mut collector = CallCollector::default(); + sig_ty.call(&args, false, &mut collector); + + collector.0.iter().fold(String::new(), |mut acc, ty| { + if !acc.is_empty() { + acc.push_str(", "); + } + + acc.push_str(&format!("{ty:?}")); + acc + }) + } + + assert_snapshot!(call(literal_sig!(p1 -> p1), literal_args!(q1)), @"@q1"); + assert_snapshot!(call(literal_sig!(!u1: w1 -> w1), literal_args!(!u1: w2)), @"@w2"); } }