Partial trait (#85)

* Closes #78

---------

Co-authored-by: Paul Cadman <[email protected]>

Stdlib/Data/Int.juvix

@@ -4,6 +4,7 @@ import Stdlib.Data.Int.Base open public;
 
 import Stdlib.Data.Nat as Nat;
 open Nat using {Nat; suc; zero; sub};
+
 import Stdlib.Data.String open;
 import Stdlib.Data.Bool open;
 

Stdlib/Data/Int/Base.juvix

@@ -4,6 +4,7 @@ import Stdlib.Data.Fixity open;
 
 import Stdlib.Data.Nat.Base as Nat;
 open Nat using {Nat; zero; suc; sub};
+
 import Stdlib.Data.Bool.Base open;
 
 --- Inductive integers. I.e. whole numbers that can be positive, zero, or negative.

Stdlib/Data/List.juvix

@@ -3,14 +3,14 @@ module Stdlib.Data.List;
 import Stdlib.Data.List.Base open public;
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.String.Base open;
-import Stdlib.Debug.Fail open;
 
 import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
+import Stdlib.Trait.Partial open;
 
 --- 𝒪(1). Partial function that returns the first element of a ;List;.
-head {A} : List A -> A
+phead {A} {{Partial}} : List A -> A
   | (x :: _) := x
   | nil := fail "head: empty list";
 

Stdlib/Data/List/Base.juvix

@@ -147,6 +147,10 @@ tail {A} : List A → List A
   | (_ :: xs) := xs
   | nil := nil;
 
+head {A} (a : A) : List A -> A
+  | (x :: _) := x
+  | nil := a;
+
 syntax iterator any {init := 0; range := 1};
 
 --- 𝒪(𝓃). Returns ;true; if at least one element of the ;List; satisfies the predicate.

Stdlib/Debug/Fail.juvix

@@ -4,4 +4,4 @@ import Stdlib.Data.String.Base open;
 
 --- Primitive that exits the program with an error message.
 builtin fail
-axiom fail : {A : Type} → String → A;
+axiom failwith : {A : Type} → String → A;

Stdlib/Trait.juvix

@@ -3,3 +3,4 @@ module Stdlib.Trait;
 import Stdlib.Trait.Eq as Eq open using {Eq; module Eq} public;
 import Stdlib.Trait.Show as Show open using {Show; module Show} public;
 import Stdlib.Trait.Ord as Ord open using {Ord; module Ord} public;
+import Stdlib.Trait.Partial open public;

Stdlib/Trait/Partial.juvix

@@ -0,0 +1,13 @@
+module Stdlib.Trait.Partial;
+
+import Stdlib.Data.String.Base open;
+import Stdlib.Debug.Fail as Debug;
+
+trait
+type Partial :=
+  mkPartial {fail : {A : Type} -> String -> A};
+
+open Partial public;
+
+runPartial {A} (f : {{Partial}} -> A) : A :=
+  f {{mkPartial Debug.failwith}};

test/Test.juvix

@@ -140,124 +140,85 @@ sortTest : String -> (List Int -> List Int) -> QC.Test
   | sortName sort :=
     QC.mkTest
       ("sort properties: " ++str sortName)
-      (QC.mkFun (prop-sort sort));
+      (prop-sort sort);
 
-dropTest : QC.Test :=
-  QC.mkTest
-    "drop properties"
-    (QC.mkFun \ {a := QC.mkFun \ {b := prop-drop a b}});
+dropTest : QC.Test := QC.mkTest "drop properties" prop-drop;
 
-snocTest : QC.Test :=
-  QC.mkTest
-    "snoc properties"
-    (QC.mkFun \ {a := QC.mkFun \ {b := prop-snoc a b}});
+snocTest : QC.Test := QC.mkTest "snoc properties" prop-snoc;
 
-zipTest : QC.Test :=
-  QC.mkTest
-    "zip properties"
-    (QC.mkFun \ {a := QC.mkFun \ {b := prop-zip a b}});
+zipTest : QC.Test := QC.mkTest "zip properties" prop-zip;
 
 zipWithTest : QC.Test :=
-  QC.mkTest
-    "zipWith properties"
-    (QC.mkFun
-      \ {a :=
-        QC.mkFun
-          \ {b :=
-            QC.mkFun
-              \ {c :=
-                prop-zipWith \ {x := QC.Fun.fun (QC.Fun.fun a x)} b c}}});
+  QC.mkTest "zipWith properties" prop-zipWith;
 
 equalCompareToEqTest : QC.Test :=
   QC.mkTest
     "equal Nats compare to EQ"
-    (QC.mkFun prop-equal-compare-to-eq);
+    prop-equal-compare-to-eq;
 
 gcdNoCoprimeTest : QC.Test :=
-  QC.mkTest
-    "no integers are coprime"
-    (QC.mkFun \ {a := QC.mkFun \ {b := prop-gcd-bad a b}});
+  QC.mkTest "no integers are coprime" prop-gcd-bad;
 
 partitionTest : QC.Test :=
   QC.mkTest
     "partition: recombination of the output equals the input"
-    (QC.mkFun
-      \ {a := QC.mkFun \ {b := prop-partition a (QC.Fun.fun b)}});
+    prop-partition;
 
 testDistributive : QC.Test :=
   QC.mkTest
     "all functions are distributive over +"
-    (QC.mkFun
-      \ {a :=
-        QC.mkFun
-          \ {b :=
-            QC.mkFun \ {c := prop-distributive a b (QC.Fun.fun c)}}});
+    prop-distributive;
 
 reverseLengthTest : QC.Test :=
   QC.mkTest
     "reverse preserves length"
-    (QC.mkFun prop-reverseDoesNotChangeLength);
+    prop-reverseDoesNotChangeLength;
 
 reverseReverseIdTest : QC.Test :=
   QC.mkTest
     "reverse of reverse is identity"
-    (QC.mkFun prop-reverseReverseIsIdentity);
+    prop-reverseReverseIsIdentity;
 
 splitAtRecombineTest : QC.Test :=
   QC.mkTest
     "splitAt: recombination of the output is equal to the input list"
-    (QC.mkFun
-      \ {a := QC.mkFun \ {b := prop-splitAtRecombine a b}});
+    prop-splitAtRecombine;
 
 splitAtLengthTest : QC.Test :=
   QC.mkTest
     "splitAt: Check lengths of output if the input Nat is greater than the length of the input list"
-    (QC.mkFun
-      \ {a := QC.mkFun \ {b := prop-splitAtLength a b}});
+    prop-splitAtLength;
 
 mergeSumLengthsTest : QC.Test :=
   QC.mkTest
     "merge: sum of the lengths of input lists is equal to the length of output list"
-    (QC.mkFun
-      \ {a := QC.mkFun \ {b := prop-mergeSumLengths a b}});
+    prop-mergeSumLengths;
 
 tailLengthOneLessTest : QC.Test :=
   QC.mkTest
     "tail: length of output is one less than input unless empty"
-    (QC.mkFun prop-tailLengthOneLess);
+    prop-tailLengthOneLess;
 
 transposeMatrixIdTest : QC.Test :=
   QC.mkTest
     {{QC.testableFunction {{showListI}} {{QC.arbitraryMatrix}}}}
     "transpose: recrangular matrix has property transpose . transpose = id"
-    (QC.mkFun prop-transposeMatrixId);
+    prop-transposeMatrixId;
 
 transposeMatrixDimentionsTest : QC.Test :=
   QC.mkTest
     {{QC.testableFunction {{showListI}} {{QC.arbitraryMatrix}}}}
     "transpose: transpose swaps dimensions"
-    (QC.mkFun prop-transposeMatrixDimensions);
+    prop-transposeMatrixDimensions;
 
 main : IO :=
   readLn
     \ {seed :=
       QC.runTestsIO
         100
         (stringToNat seed)
-        (partitionTest
-          :: reverseLengthTest
-          :: reverseReverseIdTest
-          :: splitAtRecombineTest
-          :: splitAtLengthTest
-          :: mergeSumLengthsTest
-          :: tailLengthOneLessTest
-          :: equalCompareToEqTest
-          :: zipTest
-          :: zipWithTest
-          :: snocTest
-          :: dropTest
-          :: sortTest "mergeSort" mergeSort
-          :: sortTest "quickSort" quickSort
-          :: transposeMatrixIdTest
-          :: transposeMatrixDimentionsTest
-          :: nil)};
+        [partitionTest; reverseLengthTest; reverseReverseIdTest; splitAtRecombineTest; splitAtLengthTest; mergeSumLengthsTest; tailLengthOneLessTest; equalCompareToEqTest; zipTest; zipWithTest; snocTest; dropTest; sortTest
+          "mergeSort"
+          mergeSort; sortTest
+          "quickSort"
+          quickSort; transposeMatrixIdTest; transposeMatrixDimentionsTest]};

test/juvix.lock.yaml

@@ -0,0 +1,16 @@
+# This file was autogenerated by Juvix version 0.5.2.
+# Do not edit this file manually.
+
+dependencies:
+- path: ../
+  dependencies: []
+- git:
+    name: quickcheck
+    ref: 760e80205ffa5b5c363a2aa56c583bdfd31fe252
+    url: https://github.com/anoma/juvix-quickcheck.git
+  dependencies:
+  - git:
+      name: stdlib
+      ref: 86f9e82c34395f3e0447c58566bc92347603ebd3
+      url: https://github.com/anoma/juvix-stdlib
+    dependencies: []

test/juvix.yaml

@@ -2,7 +2,7 @@ dependencies:
 - ../
 - git:
     url: https://github.com/anoma/juvix-quickcheck.git
-    ref: v0.7.1
+    ref: v0.8.0
     name: quickcheck
 name: stdlib-test
 version: 0.0.0