Fixed bug in not

Use simple refinement types to handle secrets. - Added “typechk/secret_11.dyon”
PistonDevelopers · Oct 23, 2019 · d4f1e7c · d4f1e7c
1 parent 78d2acc
commit d4f1e7c
Show file tree

Hide file tree

Showing 4 changed files with 23 additions and 4 deletions.
diff --git a/source/typechk/secret_11.dyon b/source/typechk/secret_11.dyon
@@ -0,0 +1,7 @@
+fn main() {
+    list := [1, 2, 3]
+    check := all i {list[i] < 2}
+    if !check {
+        why := why(!check)
+    }
+}
diff --git a/src/lib.dyon b/src/lib.dyon
@@ -354,7 +354,9 @@ fn pow(a: any, b: any) -> any { ... }
 fn norm(v: vec4) -> f64 { ... }
 
 /// Logical NOT.
-fn not(b: bool) -> bool { ... }
+fn not(b: any) -> any { ... }
+    (sec[bool]) -> sec[bool]
+    (bool) -> bool
 
 /// Negation.
 fn neg(v: any) -> any { ... }

diff --git a/src/module.rs b/src/module.rs
@@ -130,7 +130,7 @@ impl Module {
             ],
             lazy: LAZY_NO
         });
-        m.add_str("and_also", and_also, Dfn {
+        m.add(crate::AND_ALSO.clone(), and_also, Dfn {
             lts: vec![Lt::Default; 2],
             tys: vec![Bool, Bool],
             ret: Any,
@@ -140,7 +140,7 @@ impl Module {
             ],
             lazy: LAZY_AND
         });
-        m.add_str("or_else", or_else, Dfn {
+        m.add(crate::OR_ELSE.clone(), or_else, Dfn {
             lts: vec![Lt::Default; 2],
             tys: vec![Bool, Bool],
             ret: Any,
@@ -238,7 +238,16 @@ impl Module {
             ],
             lazy: LAZY_NO
         });
-        m.add_unop(crate::NOT.clone(), not, Dfn::nl(vec![Bool], Bool));
+        m.add_unop(crate::NOT.clone(), not, Dfn {
+            lts: vec![Lt::Default],
+            tys: vec![Any],
+            ret: Any,
+            ext: vec![
+                (vec![], vec![Type::Secret(Box::new(Bool))], Type::Secret(Box::new(Bool))),
+                (vec![], vec![Bool], Bool),
+            ],
+            lazy: LAZY_NO
+        });
         m.add_unop(crate::NEG.clone(), neg, Dfn{
             lts: vec![Lt::Default], tys: vec![Any], ret: Any,
             ext: vec![

diff --git a/tests/lib.rs b/tests/lib.rs
@@ -223,6 +223,7 @@ fn test_typechk() {
     test_src("source/typechk/secret_8.dyon");
     test_src("source/typechk/secret_9.dyon");
     test_fail_src("source/typechk/secret_10.dyon");
+    test_src("source/typechk/secret_11.dyon");
     test_src("source/typechk/dot.dyon");
     test_src("source/typechk/in.dyon");
     test_fail_src("source/typechk/in_2.dyon");