diff --git a/assets/syntax.txt b/assets/syntax.txt index 16f3f15f..328c336b 100644 --- a/assets/syntax.txt +++ b/assets/syntax.txt @@ -20,7 +20,11 @@ _seps: "(){}[],.:;=<>*·+-/%^?~|&∧∨!¬∑∃∀\n\"\\" } ?w block:"block" ?.l([?w ty:"ty" ?w])] [.."("!:"name" ?w "(" ?w args ?w ")" ?w ?currents ?w "=" ?w expr:"expr"] } -4 ty = ["(" ?w .s?.(, type:"ty_arg") ?w ")" .w? "->" ?w type:"ty_ret"] +4 ty = { + ty_var + ["(" ?w .s?.(, type:"ty_arg") ?w ")" .w? "->" ?w type:"ty_ret"] +} +5 ty_var = ["all" ?w .s?.(, .._seps!:"ty_var") ?w "{" ?w ty ?w "}"] 4 args = .s?.(, arg:"arg") 5 arg = [?"mut":"mut" ?w .._seps!:"name" ?[?w ":" ?w ?["'" ?w .._seps!:"lifetime"] ?w ?type:"type"]] diff --git a/source/typechk/refine_quantifier_fail_1.dyon b/source/typechk/refine_quantifier_fail_1.dyon new file mode 100644 index 00000000..4dcb3eac --- /dev/null +++ b/source/typechk/refine_quantifier_fail_1.dyon @@ -0,0 +1,10 @@ +fn foo(a: any, b: any) -> any {return a + b} + all T { (T f64, T f64) -> T f64 } + +fn km(a: f64) -> km f64 {return clone(a)} + +fn check_km(a: km f64) {} + +fn main() { + check_km(foo(km(2), 3)) +} diff --git a/source/typechk/refine_quantifier_fail_2.dyon b/source/typechk/refine_quantifier_fail_2.dyon new file mode 100644 index 00000000..df0e6c5e --- /dev/null +++ b/source/typechk/refine_quantifier_fail_2.dyon @@ -0,0 +1,11 @@ +fn foo(a: any, b: any) -> any {return a + b} + all T { (T f64, T f64) -> T f64 } + +fn km(a: f64) -> km f64 {return clone(a)} +fn m(a: f64) -> m f64 {return clone(a)} + +fn check_km(a: km f64) {} + +fn main() { + check_km(foo(m(2), km(3))) +} diff --git a/source/typechk/refine_quantifier_pass_1.dyon b/source/typechk/refine_quantifier_pass_1.dyon new file mode 100644 index 00000000..5333af29 --- /dev/null +++ b/source/typechk/refine_quantifier_pass_1.dyon @@ -0,0 +1,10 @@ +fn foo(a: any, b: any) -> any {return a + b} + all T { (T f64, T f64) -> T f64 } + +fn km(a: f64) -> km f64 {return clone(a)} + +fn check_km(a: km f64) {} + +fn main() { + check_km(foo(km(2), km(3))) +} diff --git a/source/typechk/refine_quantifier_pass_2.dyon b/source/typechk/refine_quantifier_pass_2.dyon new file mode 100644 index 00000000..08414ed9 --- /dev/null +++ b/source/typechk/refine_quantifier_pass_2.dyon @@ -0,0 +1,8 @@ +fn foo(a: any, b: any) -> any {return a + b} + all T { (T f64, T f64) -> T f64 } + +fn check_f64(a: f64) {} + +fn main() { + check_f64(foo(2, 3)) +} diff --git a/source/typechk/refine_quantifier_pass_3.dyon b/source/typechk/refine_quantifier_pass_3.dyon new file mode 100644 index 00000000..f452ab3e --- /dev/null +++ b/source/typechk/refine_quantifier_pass_3.dyon @@ -0,0 +1,11 @@ +fn foo(a: any, b: any) -> any {return a + b} + all T { (T f64, T f64) -> T f64 } + +fn km(a: f64) -> km f64 {return clone(a)} + +fn check_km(a: km f64) {} + +fn main() { + // Allow no ad-hoc type before the first one. + check_km(foo(2, km(3))) +} diff --git a/source/typechk/refine_quantifier_pass_4.dyon b/source/typechk/refine_quantifier_pass_4.dyon new file mode 100644 index 00000000..cea2618a --- /dev/null +++ b/source/typechk/refine_quantifier_pass_4.dyon @@ -0,0 +1,15 @@ +fn km(a: any) -> km any {return clone(a)} + (vec4) -> km vec4 + (f64) -> km f64 +fn m(a: any) -> m any {return clone(a)} + (vec4) -> m vec4 + (f64) -> m f64 +fn foo(a: any, b: any) -> any {return a + b} + all T { (T vec4, T vec4) -> T vec4 } + all T { (T vec4, T f64) -> T vec4 } + +fn check_m(a: m vec4) {} + +fn main() { + check_m(foo(m((2, 0)), m(2))) +} diff --git a/source/typechk/refine_quantifier_pass_5.dyon b/source/typechk/refine_quantifier_pass_5.dyon new file mode 100644 index 00000000..8d7912a4 --- /dev/null +++ b/source/typechk/refine_quantifier_pass_5.dyon @@ -0,0 +1,12 @@ +fn m(a: any) -> m any {return clone(a)} + (vec4) -> m vec4 + (f64) -> m f64 +fn foo(a: any, b: any) -> any {return a + b} + all T { (T vec4, T vec4) -> T vec4 } + all T { (T vec4, f64) -> T vec4 } + +fn check_m(a: m vec4) {} + +fn main() { + check_m(foo(m((2, 0)), 2)) +} diff --git a/source/typechk/refine_quantifier_pass_6.dyon b/source/typechk/refine_quantifier_pass_6.dyon new file mode 100644 index 00000000..1df14d0e --- /dev/null +++ b/source/typechk/refine_quantifier_pass_6.dyon @@ -0,0 +1,18 @@ +fn km(a: any) -> km any {return clone(a)} + (vec4) -> km vec4 + (f64) -> km f64 +fn m(a: any) -> m any {return clone(a)} + (vec4) -> m vec4 + (f64) -> m f64 + +fn foo(a: any, b: any) -> any {return a + b} + all T { (T f64, T f64) -> T f64 } + all T { (T vec4, T vec4) -> T vec4 } + all T { (T vec4, T f64) -> T vec4 } + (f64, vec4) -> vec4 + +fn check_m(a: m vec4) {} + +fn main() { + check_m(foo(m(2), km((1, 0)))) +} diff --git a/src/lib.dyon b/src/lib.dyon index 6a514980..f45b82ad 100644 --- a/src/lib.dyon +++ b/src/lib.dyon @@ -231,16 +231,16 @@ fn max(array: [f64]) -> f64 { ... } /// Addition. fn add(a: any, b: any) -> any { ... } - (f64, f64) -> f64 - (vec4, vec4) -> vec4 - (vec4, f64) -> vec4 - (f64, vec4) -> vec4 - (mat4, mat4) -> mat4 - (f64, mat4) -> mat4 - (mat4, f64) -> mat4 - (bool, bool) -> bool - (str, str) -> str - (link, link) -> link + all T { (T f64, T f64) -> T f64 } + all T { (T vec4, T vec4) -> T vec4 } + all T { (T vec4, T f64) -> T vec4 } + all T { (T f64, T vec4) -> T vec4 } + all T { (T mat4, T mat4) -> T mat4 } + all T { (T f64, T mat4) -> T mat4 } + all T { (T mat4, T f64) -> T mat4 } + all T { (T bool, T bool) -> T bool } + all T { (T str, T str) -> T str } + all T { (T link, T link) -> T link } /// Returns the length of 4D vector. fn norm(v: vec4) -> f64 { ... } diff --git a/src/lib.rs b/src/lib.rs index ee103bcc..4d456349 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -61,6 +61,7 @@ lazy_static!{ pub(crate) static ref NOT: Arc = Arc::new("not".into()); pub(crate) static ref NEG: Arc = Arc::new("neg".into()); pub(crate) static ref NORM: Arc = Arc::new("norm".into()); + pub(crate) static ref T: Arc = Arc::new("T".into()); } /// Type alias for Dyon arrays. @@ -377,25 +378,25 @@ impl Module { tys: vec![Any; 2], ret: Any, ext: vec![ - (vec![F64, F64], F64), - (vec![Vec4, Vec4], Vec4), - (vec![Vec4, F64], Vec4), - (vec![F64, Vec4], Vec4), - (vec![Mat4, Mat4], Mat4), - (vec![F64, Mat4], Mat4), - (vec![Mat4, F64], Mat4), - (vec![Bool, Bool], Bool), - (vec![Str, Str], Str), - (vec![Link, Link], Link), + Type::all_ext(vec![F64, F64], F64), + Type::all_ext(vec![Vec4, Vec4], Vec4), + Type::all_ext(vec![Vec4, F64], Vec4), + Type::all_ext(vec![F64, Vec4], Vec4), + Type::all_ext(vec![Mat4, Mat4], Mat4), + Type::all_ext(vec![F64, Mat4], Mat4), + Type::all_ext(vec![Mat4, F64], Mat4), + Type::all_ext(vec![Bool, Bool], Bool), + Type::all_ext(vec![Str, Str], Str), + Type::all_ext(vec![Link, Link], Link), ] }); m.add_str("not", not, Dfn::nl(vec![Bool], Bool)); m.add_str("neg", neg, Dfn{ lts: vec![Lt::Default], tys: vec![Any], ret: Any, ext: vec![ - (vec![F64], F64), - (vec![Vec4], Vec4), - (vec![Mat4], Mat4), + (vec![], vec![F64], F64), + (vec![], vec![Vec4], Vec4), + (vec![], vec![Mat4], Mat4), ] }); m.add_str("dot", dot, Dfn { @@ -403,9 +404,9 @@ impl Module { tys: vec![Any; 2], ret: F64, ext: vec![ - (vec![Vec4, Vec4], F64), - (vec![Vec4, F64], F64), - (vec![F64, Vec4], F64), + (vec![], vec![Vec4, Vec4], F64), + (vec![], vec![Vec4, F64], F64), + (vec![], vec![F64, Vec4], F64), ] }); m.add_str("cross", cross, Dfn::nl(vec![Vec4, Vec4], Vec4)); diff --git a/src/lifetime/node.rs b/src/lifetime/node.rs index 3b7e58af..1f594f1e 100644 --- a/src/lifetime/node.rs +++ b/src/lifetime/node.rs @@ -473,6 +473,11 @@ pub fn convert_meta_data( let i = *parents.last().unwrap(); nodes[i].ty = Some(Type::Vec4); } + "ty_var" => { + // Use names as a way of storing type variables. + let i = *parents.last().unwrap(); + nodes[i].names.push(val.clone()); + } _ => {} } } diff --git a/src/lifetime/typecheck/refine.rs b/src/lifetime/typecheck/refine.rs index 3f57101a..fdf0911a 100644 --- a/src/lifetime/typecheck/refine.rs +++ b/src/lifetime/typecheck/refine.rs @@ -1,6 +1,8 @@ use super::*; use prelude::Dfn; +use std::sync::Arc; + fn report( i: usize, found: bool, @@ -52,6 +54,7 @@ pub(crate) fn declaration( { count += 1; let mut all = true; + let mut ty_vars: Vec>> = vec![None; nodes[ty].names.len()]; for (arg_expr, &ty_arg) in nodes[i].children.iter() .filter(|&&arg| nodes[arg].kind == Kind::CallArg && !nodes[arg].children.is_empty()) @@ -65,6 +68,8 @@ pub(crate) fn declaration( } let found_arg = if let (&Some(ref a), &Some(ref b)) = (&nodes[arg_expr].ty, &nodes[ty_arg].ty) { + let b = b.bind_ty_vars(a, &nodes[ty].names, &mut ty_vars) + .map_err(|err| nodes[arg_expr].source.wrap(err))?; if b.goes_with(a) { if b.ambiguous(a) { ambiguous = true; @@ -83,7 +88,18 @@ pub(crate) fn declaration( if let Some(&ind) = nodes[ty].children.iter() .filter(|&&ty| nodes[ty].kind == Kind::TyRet) .next() { - *this_ty = nodes[ind].ty.clone(); + + let mut new_ty = nodes[ind].ty.clone(); + if let Some(ref mut new_ty) = new_ty { + for i in 0..nodes[ty].names.len() { + if let Some(ref val) = ty_vars[i] { + new_ty.insert_var(&nodes[ty].names[i], val); + } else { + new_ty.insert_none_var(&nodes[ty].names[i]); + } + } + } + *this_ty = new_ty; found = true; break; } @@ -106,17 +122,20 @@ pub(crate) fn prelude( let mut ambiguous = false; 'outer: for ty in &f.ext { let mut all = true; + let mut ty_vars: Vec>> = vec![None; ty.0.len()]; for (arg_expr, ty_arg) in nodes[i].children.iter() .filter(|&&arg| nodes[arg].kind == Kind::CallArg && !nodes[arg].children.is_empty()) .map(|&arg| nodes[arg].children[0]) - .zip(ty.0.iter()) + .zip(ty.1.iter()) { if nodes[arg_expr].ty.is_none() { ambiguous = true; break 'outer; } let found_arg = if let Some(ref a) = nodes[arg_expr].ty { + let ty_arg = ty_arg.bind_ty_vars(a, &ty.0, &mut ty_vars) + .map_err(|err| nodes[arg_expr].source.wrap(err))?; if ty_arg.goes_with(a) { if ty_arg.ambiguous(a) { ambiguous = true; @@ -132,7 +151,16 @@ pub(crate) fn prelude( } } if all { - *this_ty = Some(ty.1.clone()); + let mut new_ty = ty.2.clone(); + for i in 0..ty.0.len() { + if let Some(ref val) = ty_vars[i] { + new_ty.insert_var(&ty.0[i], val); + } else { + new_ty.insert_none_var(&ty.0[i]); + } + } + + *this_ty = Some(new_ty); found = true; break; } diff --git a/src/prelude.rs b/src/prelude.rs index 62aed20b..2c2bc289 100644 --- a/src/prelude.rs +++ b/src/prelude.rs @@ -33,7 +33,9 @@ pub struct Dfn { /// Return type of function. pub ret: Type, /// Extra type information. - pub ext: Vec<(Vec, Type)>, + /// + /// Stores type variables, argument types, return type. + pub ext: Vec<(Vec>, Vec, Type)>, } impl Dfn { diff --git a/src/ty.rs b/src/ty.rs index 3df2e85a..e848debf 100644 --- a/src/ty.rs +++ b/src/ty.rs @@ -47,6 +47,17 @@ pub enum Type { } impl Type { + /// Returns an extension quantified over ad-hoc types. + /// + /// For example, `(vec4, vec4) -> vec4` becomes `all T { (T vec4, T vec4) -> T vec4 }`. + pub fn all_ext(args: Vec, ret: Type) -> (Vec>, Vec, Type) { + use crate::T; + use Type::AdHoc; + + (vec![T.clone()], args.into_iter().map(|arg| AdHoc(T.clone(), Box::new(arg))).collect(), + AdHoc(T.clone(), Box::new(ret))) + } + /// Returns description of the type. pub fn description(&self) -> String { use Type::*; @@ -156,6 +167,85 @@ impl Type { /// Returns an in-type with an `any` as inner type. pub fn in_ty() -> Type {Type::In(Box::new(Type::Any))} + /// Binds refinement type variables. + /// + /// Returns the type argument to compare to. + pub fn bind_ty_vars( + &self, + refine: &Type, + names: &[Arc], + ty_vars: &mut Vec>> + ) -> Result { + if names.len() == 0 {return Ok(self.clone())}; + match (self, refine) { + (&Type::AdHoc(ref a_name, ref a_inner_ty), + &Type::AdHoc(ref b_name, ref b_inner_ty)) => { + for i in 0..names.len() { + if a_name == &names[i] { + let new_inner = a_inner_ty.bind_ty_vars(b_inner_ty, names, ty_vars)?; + if let Some(ref existing_name) = ty_vars[i] { + if existing_name != b_name && + new_inner.goes_with(b_inner_ty) && + !new_inner.ambiguous(b_inner_ty) + { + return Err(format!("Type mismatch (#1500): Expected `{}`, found `{}`", + existing_name, b_name)) + } else { + return Ok(Type::AdHoc(existing_name.clone(), + Box::new(new_inner))) + } + } else { + ty_vars[i] = Some(b_name.clone()); + return Ok(Type::AdHoc(b_name.clone(), + Box::new(a_inner_ty.bind_ty_vars(b_inner_ty, names, ty_vars)?))) + } + } + } + Ok(Type::AdHoc(a_name.clone(), + Box::new(a_inner_ty.bind_ty_vars(b_inner_ty, names, ty_vars)?))) + } + (&Type::AdHoc(ref a_name, ref a_inner_ty), ref b) => { + for i in 0..names.len() { + if a_name == &names[i] { + let new_inner = a_inner_ty.bind_ty_vars(refine, names, ty_vars)?; + if let Some(ref n) = ty_vars[i] { + if new_inner.goes_with(b) && !new_inner.ambiguous(b) { + return Err(format!( + "Type mismatch (#1600): Expected `{}`, found no ad-hoc type", n)) + } + } else {break} + } + } + a_inner_ty.bind_ty_vars(refine, names, ty_vars) + } + _ => Ok(self.clone()) + } + } + + /// Inserts variable name, replacing ad-hoc type name. + pub fn insert_var(&mut self, name: &Arc, val: &Arc) { + match *self { + Type::AdHoc(ref mut n, ref mut inner_ty) => { + if n == name { + *n = val.clone(); + } + inner_ty.insert_var(name, val) + } + _ => {} + } + } + + /// Inserts a none ad-hoc variable. + pub fn insert_none_var(&mut self, name: &Arc) { + match *self { + Type::AdHoc(_, ref mut inner_ty) => { + inner_ty.insert_none_var(name); + *self = (**inner_ty).clone(); + } + _ => {} + } + } + /// Returns `true` if a type to be refined is ambiguous relative to this type (directional check). /// /// For example, the type ad-hoc type `Foo str` is ambiguous with type `str`. diff --git a/tests/lib.rs b/tests/lib.rs index 38724a2e..dfe2adcc 100644 --- a/tests/lib.rs +++ b/tests/lib.rs @@ -257,6 +257,13 @@ fn test_typechk() { test_fail_src("source/typechk/refine_closed_fail_1.dyon"); test_fail_src("source/typechk/refine_closed_fail_2.dyon"); test_src("source/typechk/refine_closed_pass_1.dyon"); + test_src("source/typechk/refine_quantifier_pass_1.dyon"); + test_src("source/typechk/refine_quantifier_pass_2.dyon"); + test_src("source/typechk/refine_quantifier_pass_3.dyon"); + test_src("source/typechk/refine_quantifier_pass_4.dyon"); + test_src("source/typechk/refine_quantifier_pass_5.dyon"); + test_fail_src("source/typechk/refine_quantifier_fail_1.dyon"); + test_fail_src("source/typechk/refine_quantifier_fail_2.dyon"); } #[test]