Added support for ad-hoc variables in refinement types

See PistonDevelopers#645

Use the semantics that none ad-hoc type is quantified over by `all`.

- Added `Type::all_ext`
- Added `Type::bind_ty_vars`
- Added `Type::insert_var`
- Added `Type::insert_none_var`
- Added `T` lazy static string
- Added some refine quantifier tests
- Updated `add` in “lib.dyon”
- Updated `add` extra type information
- Added support for type quantifier in syntax
- Push type variable names to “ty” node

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"]]

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))
+}

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)))
+}

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)))
+}

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))
+}

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)))
+}

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)))
+}

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))
+}

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))))
+}

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 { ... }

src/lib.rs

@@ -61,6 +61,7 @@ lazy_static!{
     pub(crate) static ref NOT: Arc<String> = Arc::new("not".into());
     pub(crate) static ref NEG: Arc<String> = Arc::new("neg".into());
     pub(crate) static ref NORM: Arc<String> = Arc::new("norm".into());
+    pub(crate) static ref T: Arc<String> = Arc::new("T".into());
 }
 
 /// Type alias for Dyon arrays.
@@ -377,35 +378,35 @@ 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 {
             lts: vec![Lt::Default; 2],
             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));

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());
+                    }
                     _ => {}
                 }
             }

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<Option<Arc<String>>> = 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<Option<Arc<String>>> = 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;
         }

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>, Type)>,
+    ///
+    /// Stores type variables, argument types, return type.
+    pub ext: Vec<(Vec<Arc<String>>, Vec<Type>, Type)>,
 }
 
 impl Dfn {