Simple refinement types

Cargo.toml

@@ -18,6 +18,7 @@ read_color = "1.0.0"
 read_token = "1.0.0"
 lazy_static = "1.0.0"
 vecmath = "1.0.0"
+advancedresearch-tree_mem_sort = "0.2.0"
 
 [dependencies.reqwest]
 version = "0.4.0"

assets/syntax.txt

@@ -17,12 +17,21 @@ _seps: "(){}[],.:;=<>*·+-/%^?~|&∧∨!¬∑∃∀\n\"\\"
     ["fn" .w! .."("!:"name" ?w "(" ?w args ?w ")" ?w ?currents ?w {
             ["->":"returns" ?w ?type:"ret_type"]
             !"->":!"returns"
-        } ?w block:"block"]
+        } ?w block:"block" ?.l([?w ty:"ty" ?w])]
     [.."("!:"name" ?w "(" ?w args ?w ")" ?w ?currents ?w "=" ?w expr:"expr"]
 }
+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"]]
+         ?["'" ?w .._seps!:"lifetime"] ?w ?type:"type"]
+         ?[?w "=>" ?w .s!.([?w "|" ?w] {
+            "ok(_)":"ok(_)" "err(_)":"err(_)" "some(_)":"some(_)" lazy:"grab"})]]
+// Fake grab expression to reuse code for lazy invariants.
+5 lazy = expr:"expr"
 6 imm_arg = [!"mut " .._seps!:"name" ?[?w ":" ?w !"'" ?type:"type"]]
 7 closure = ["\\(" ?w .s?.(, imm_arg:"arg") ?w ")" ?w ?currents
              ?w "=" ?w expr:"expr"]
@@ -97,8 +106,8 @@ _seps: "(){}[],.:;=<>*·+-/%^?~|&∧∨!¬∑∃∀\n\"\\"
                ?[, arg_expr:"z" ?[, arg_expr:"w"]] ?,]
 26 text = .t?:"text"
 27 bool = [{"true":"bool" "false":!"bool"} !.._seps!]
-28 unop_not = [{"!":"!" "¬":"!"} ?w lexpr:"expr"]
-29 unop_neg = ["-":"-" ?w mul_expr:"expr"]
+28 unop_not = [{"!" "¬"} ?w lexpr:"expr"]
+29 unop_neg = ["-" ?w mul_expr:"expr"]
 30 norm = ["|" ?w expr:"expr" ?w "|"]
 31 item = [?"~":"current" ?w .._seps!:"name" ?[wn "?":"try_item"]
     ?item_extra:"item_extra"]
@@ -137,7 +146,7 @@ _seps: "(){}[],.:;=<>*·+-/%^?~|&∧∨!¬∑∃∀\n\"\\"
 49 assign_op = {
   ":=":":=" "=":"=" "+=":"+=" "-=":"-=" "*=":"*=" "/=":"/=" "%=":"%=" "^=":"^="
 }
-50 compare = [lexpr:"left" wn compare_op ?w expr:"right"]
+50 compare = [lexpr:"expr" wn compare_op ?w expr:"expr"]
 51 compare_op = {"==":"==" "!=":"!=" "¬=":"!=" "<=":"<=" "<":"<" ">=":">=" ">":">"}
 52 grab = ["grab" ?[w "'" .$:"grab_level"] w expr:"expr"]
 53 try_expr = ["try" w expr:"expr"]
@@ -154,7 +163,7 @@ _seps: "(){}[],.:;=<>*·+-/%^?~|&∧∨!¬∑∃∀\n\"\\"
 64 , = [?w "," ?w]
 65 arr = {array:"array" array_fill:"array_fill"}
 66 items = {mat4:"mat4" vec4:"vec4" link:"link" grab:"grab" try_expr:"try_expr"
-            ["(" ?w expr ?w ")"] unop_not:"unop" norm:"norm"
+            ["(" ?w expr ?w ")"] unop_not:"not" norm:"norm"
             text go:"go"
             call_closure:"call_closure" named_call_closure:"named_call_closure"
             call:"call" named_call:"named_call"
@@ -213,7 +222,7 @@ _seps: "(){}[],.:;=<>*·+-/%^?~|&∧∨!¬∑∃∀\n\"\\"
     ["in" ?w "[" ?w type:"in" ?w "]"]
     "in":"in_any"
     closure_type:"closure_type"
-    [.._seps!:"ad_hoc" ?[?w type:"ad_hoc_ty"]]
+    [!"sec" .._seps!:"ad_hoc" ?[?w type:"ad_hoc_ty"]]
 }
 101 closure_type = ["\\(" ?w .s?.(, type:"cl_arg") ?w ")"
     ?w "->" ?w type:"cl_ret"]
@@ -229,8 +238,8 @@ _seps: "(){}[],.:;=<>*·+-/%^?~|&∧∨!¬∑∃∀\n\"\\"
 } ?w]
 203 / = [wn "/":"/" !"/" ?w]
 204 % = [wn "%":"%" ?w]
-205 pow = [lexpr:"base" wn {"^" "⊻" ["xor" w]} ?w lexpr:"exp"]
-206 mul = .s!({* / %} {unop_neg:"unop" pow:"pow" lexpr:"val"})
+205 pow = [lexpr:"expr" wn {"^":"^" "⊻":"^" ["xor":"^" w]} ?w lexpr:"expr"]
+206 mul = .s!({* / %} {unop_neg:"neg" pow:"pow" lexpr:"expr"})
 207 mul_expr = {mul:"mul"}
 208 add = .s!({+ -} mul_expr:"expr")
 

examples/call.rs

@@ -2,22 +2,14 @@
 extern crate dyon;
 
 use std::sync::Arc;
-use dyon::{load_str, error, Call, Module, Dfn, Lt, Type, Runtime, RustObject};
+use dyon::{load_str, error, Call, Module, Dfn, Type, Runtime, RustObject};
 
 fn main() {
     let mut module = Module::new();
 
     // Add functions to read `a` and `b` from `RustArgs`.
-    module.add(Arc::new("a_of".into()), a_of, Dfn {
-        lts: vec![Lt::Default],
-        tys: vec![Type::Any],
-        ret: Type::F64
-    });
-    module.add(Arc::new("b_of".into()), b_of, Dfn {
-        lts: vec![Lt::Default],
-        tys: vec![Type::Any],
-        ret: Type::F64
-    });
+    module.add(Arc::new("a_of".into()), a_of, Dfn::nl(vec![Type::Any], Type::F64));
+    module.add(Arc::new("b_of".into()), b_of, Dfn::nl(vec![Type::Any], Type::F64));
 
     error(load_str("main.dyon", Arc::new(r#"
         fn add_args(a: f64, b: f64) {

source/syntax/lazy_pass_1.dyon

@@ -0,0 +1,8 @@
+fn foo(a: bool => false, b: bool) -> bool {return a && b}
+
+fn main() {
+    println(foo(false, {
+        println("this is a test")
+        false
+    }))
+}

source/syntax/lazy_pass_2.dyon

@@ -0,0 +1,8 @@
+fn foo(a: f64 => 0, b: f64) -> f64 {return a * b}
+
+fn main() {
+    println(foo(0, {
+        println("this is a test")
+        2
+    }))
+}

source/syntax/lazy_pass_3.dyon

@@ -0,0 +1,8 @@
+fn foo(a: [f64] => [], b: [f64]) -> [f64] {return clone(a)}
+
+fn main() {
+    println(foo([], {
+        println("this is a test")
+        [1, 2]
+    }))
+}

source/syntax/lazy_pass_4.dyon

@@ -0,0 +1,8 @@
+fn foo(a: str => "hi", b: str) -> str {return clone(a)}
+
+fn main() {
+    println(foo("hi", {
+        println("this is a test")
+        "hello"
+    }))
+}

source/syntax/lazy_pass_5.dyon

@@ -0,0 +1,8 @@
+fn foo(a: res[str] => ok(_), b: str) -> str {return unwrap_or(a, b)}
+
+fn main() {
+    println(foo(ok("hi"), {
+        println("this is a test")
+        "hello"
+    }))
+}

source/syntax/lazy_pass_6.dyon

@@ -0,0 +1,9 @@
+fn foo(a: res[str] => ok(_), b: str) -> str {return unwrap_or(a, b)}
+
+fn main() {
+    a := ok("hi")
+    println(foo(a, {
+        println("this is a test")
+        "hello"
+    }))
+}

source/syntax/lazy_pass_7.dyon

@@ -0,0 +1,12 @@
+fn foo(a: res[str] => err(_), b: str) -> any {
+    return if is_err(a) {unwrap_err(a)}
+           else {clone(b)}
+}
+
+fn main() {
+    a := err("hi")
+    println(foo(a, {
+        println("this is a test")
+        "hello"
+    }))
+}

source/syntax/lazy_pass_8.dyon

@@ -0,0 +1,11 @@
+fn foo(a: any => ok(_) | some(_), b: str) -> str {
+    return unwrap_or(a, b)
+}
+
+fn main() {
+    a := ok("hi")
+    println(foo(a, {
+        println("this is a test")
+        "hello"
+    }))
+}

source/syntax/secret_fail.dyon

@@ -0,0 +1,6 @@
+// Must use `sec[bool]` or `sec[f64]`.
+fn check(_: sec) {}
+
+fn main() {
+    check(explain_where(2, ""))
+}

source/test.dyon

@@ -1,6 +1,12 @@
-norm(x: f64) = x+1
+// Use `any` implicitly.
+fn foo(x) -> {return x + 1}
+// Add simple refinement types to catch more errors.
+(f64) -> f64
+(any) -> vec4
+
+bar(x: f64) = x + 1
 
 fn main() {
-    a := \(x: f64) = |x|
-    println(\a(2))
+    x := bar(foo((1, 2)))
+    println(x)
 }

source/typechk/args_refinement.dyon

@@ -0,0 +1,5 @@
+fn foo(a: bool) -> {return clone(a)}
+(bool, bool) -> bool
+
+fn main() {
+}

source/typechk/arr_fail_2.dyon

@@ -0,0 +1,3 @@
+fn main() {
+    println([0; false])
+}

source/typechk/closure_ad_hoc.dyon

@@ -0,0 +1,5 @@
+fn foo() -> Foo \() -> bool {return \() = true}
+fn main() {
+    a := foo()
+    println(\a())
+}

source/typechk/refine_closed_fail_1.dyon

@@ -0,0 +1,7 @@
+fn foo(a) -> {return clone(a)}
+(bool) -> bool
+(f64) -> f64
+
+fn main() {
+    println(foo("hi"))
+}

source/typechk/refine_closed_fail_2.dyon

@@ -0,0 +1,7 @@
+fn foo(a, b) -> {return clone(a)}
+(bool, bool) -> bool
+(f64, bool) -> f64
+
+fn main() {
+    println(foo(1, 2))
+}

source/typechk/refine_closed_pass_1.dyon

@@ -0,0 +1,7 @@
+fn foo(a) -> {return clone(a)}
+(bool) -> bool
+(any) -> f64
+
+fn main() {
+    println(foo(1))
+}

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

source/typechk/refine_type_fail.dyon

@@ -0,0 +1,5 @@
+fn foo(a: bool) -> {return clone(a)}
+(str) -> bool
+
+fn main() {
+}

source/typechk/refine_type_fail_2.dyon

@@ -0,0 +1,5 @@
+fn foo(a: bool) -> bool {return clone(a)}
+(bool) -> str
+
+fn main() {
+}

source/typechk/refinement.dyon

@@ -0,0 +1,12 @@
+// Use `any` implicitly.
+fn foo(x) -> {return x + 1}
+// Add simple refinement types to catch more errors.
+(f64) -> f64
+(vec4) -> vec4
+
+bar(x: f64) = x + 1
+
+fn main() {
+    x := bar(foo((1, 2)))
+    println(x)
+}

source/typechk/refinement_10.dyon

@@ -0,0 +1,7 @@
+fn check_bool(_: bool) {}
+fn foo(a) -> {return clone(a)}
+([]) -> [bool]
+
+fn main() {
+    check_bool(foo([true, true, false]))
+}

source/typechk/refinement_11.dyon

@@ -0,0 +1,11 @@
+fn check_bool(_: bool) {}
+fn foo(a) -> {return clone(a)}
+([bool]) -> [bool]
+fn bar(a: [bool]) -> [] {return clone(a)}
+
+fn main() {
+    // `bar` returns an ambiguous array type `[]`,
+    // so `foo` should not refine type type,
+    // which should make `check_bool` not detect a type error.
+    check_bool(foo(bar([true, true, false])))
+}