Update to standard library traits

Apps/Sudoku.juvix

@@ -40,9 +40,6 @@ import Data.Map as Map;
 open Map using {Map};
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Int.Ord open;
-
-import Stdlib.Data.Nat.Ord as Nat;
 
 module Reward;
   staticData : ByteString := 0 :: nil;
@@ -60,7 +57,7 @@ end;
 
 --- Definitions related to the Sudoku ;Resource; in the application
 module Sudoku;
-  
+
   type Puzzle :=
     mkPuzzle {
       logicHash : LogicHash;
@@ -87,7 +84,7 @@ end;
     * The only squares that change between the previous and new solutinos
     are changes from zero (i.e unfilled) to non-zero (i.e filled).
  --}
-checkTransition (fromResource : Resource) (toResource : Resource) (reward : Resource)
+checkTransition {{Partial}} (fromResource : Resource) (toResource : Resource) (reward : Resource)
   : Bool :=
   let
     fromSolution : ByteString :=
@@ -99,17 +96,17 @@ checkTransition (fromResource : Resource) (toResource : Resource) (reward : Reso
     -- compared index-wise
     diff : List (Nat × Nat) :=
       filter (x, y in zip fromSolution toSolution)
-        x Nat./= y;
+        x /= y;
 
     -- Check that any solved squares in the toSolution are unsolved in the
     -- fromSolution
     checkSolvedFromUnsolved : Bool :=
       all (consumedSquare, _ in diff)
         not (Sudoku.entryFilled? consumedSquare);
 
-  in length toSolution Nat.== length fromSolution
+  in length toSolution == length fromSolution
     && Sudoku.filledSquares toSolution
-      Nat.>= Sudoku.filledSquares fromSolution
+      >= Sudoku.filledSquares fromSolution
     && Sudoku.validGrid? (Sudoku.decode toSolution)
     && checkSolvedFromUnsolved
     && ofNat (length diff) == rewardQuantity;
@@ -131,7 +128,7 @@ vacuously valid.
 
 If the logic function part of a ;Resource; that is created by the partial
 transaction then it is valid. --}
-logicFunction : Sudoku.Puzzle -> LogicFunction
+logicFunction {{Partial}} : Sudoku.Puzzle -> LogicFunction
   | data kind tx :=
     let
       puzzleDenom : Denomination := Sudoku.denomination data;
@@ -156,16 +153,16 @@ logicFunction : Sudoku.Puzzle -> LogicFunction
 -- Definitions relating to the Dealer participant in the application
 module Dealer;
   {-- The logic function for the Sudoku dealer parital transaction.
-  
+
    Performs the following check:
-  
+
    If there is exactly one consumed ;Resource; representing a Sudoku puzzle then:
-  
+
    1. The solution matches the Dealer's solution.
-  
+
    If the partial transaction does not consume a Sudoku puzzle then it is
    vacuously valid.
-  
+
    If the logic function part of a ;Resource; that is created by the partial
    transaction then it is valid.
    --}
@@ -195,7 +192,7 @@ module Dealer;
   denomination (d : Sudoku.Puzzle) : Denomination
    := logicHash d :: staticData d;
 
-  mkResource (d : Sudoku.Puzzle) (n : Int) : Resource 
+  mkResource (d : Sudoku.Puzzle) (n : Int) : Resource
     := mkResource' (
     logicHash := logicHash d;
     staticData := staticData d;
@@ -213,7 +210,7 @@ dealer (puzzle : Sudoku.Puzzle)
         , Sudoku.mkResource puzzle initialBoard 1
     );
 
-logicFunctions (puzzle : Sudoku.Puzzle)
+logicFunctions {{Partial}} (puzzle : Sudoku.Puzzle)
  : Map LogicHash LogicFunction :=
   mkLogicFunctionMap
     ((Sudoku.Puzzle.logicHash puzzle

Apps/Sudoku/Extra.juvix

@@ -2,8 +2,6 @@ module Apps.Sudoku.Extra;
 
 import Stdlib.Prelude open;
 
-import Stdlib.Data.Nat.Ord open;
-
 import Data.Set as Set;
 open Set using {Set};
 

Apps/Sudoku/Serializer.juvix

@@ -7,9 +7,6 @@ import Data.ByteString open;
 
 import Stdlib.Prelude open;
 
-import Stdlib.Data.Nat.Ord open;
-import Stdlib.Debug.Fail open;
-
 import Stdlib.Data.Nat.Ord as Nat;
 
 --- Encode a Sudoku ;Grid; to a ;ByteString;
@@ -29,7 +26,7 @@ floorSquareRoot : Nat -> Nat
 
 --- Partial function that computes a square root. If the input ;Nat; is not a
 --- square number then fail.
-checkSquareRoot (n : Nat) : Nat
+checkSquareRoot {{Partial}} (n : Nat) : Nat
 :=  let
     root : Nat := floorSquareRoot n;
   in if
@@ -38,24 +35,24 @@ checkSquareRoot (n : Nat) : Nat
     (fail "checkSquareRoot: not a square number");
 
 --- Decode a Sudoku ;Grid; from a ;ByteString;
-decode (bs : ByteString ) : Grid
+decode {{Partial}} (bs : ByteString ) : Grid
 :=  let
     gridWidth : Nat := checkSquareRoot (length bs);
-    
+
     subGridWidth : Nat := checkSquareRoot gridWidth;
 
     rows : List (List Nat) := chunksOf gridWidth bs;
-    
+
     split {A : Type} : List A -> List (List A) := chunksOf subGridWidth;
-    
+
     pack : List (List Nat) -> List (List (List (List Nat)))
       := split ∘ map split;
-    
-    unpack : List (List (List (List Nat))) -> List (List Nat) 
+
+    unpack : List (List (List (List Nat))) -> List (List Nat)
       := map flatten ∘ flatten;
     subGrids : List (List Nat) -> List (List Nat) := unpack ∘ map transpose ∘ pack;
 
-    decodeSubGrid : List Nat -> SubGrid 
+    decodeSubGrid : List Nat -> SubGrid
       := subGrid ∘ chunksOf subGridWidth;
   in grid
     (chunksOf subGridWidth (map decodeSubGrid (subGrids rows)));

Apps/Sudoku/Validator.juvix

@@ -3,8 +3,6 @@ module Apps.Sudoku.Validator;
 import Stdlib.Prelude open;
 import Data.ByteString open;
 
-import Stdlib.Data.Nat.Ord open;
-
 import Apps.Sudoku.Grid open public;
 import Apps.Sudoku.Extra open;
 

Apps/TwoPartyExchange.juvix

@@ -82,11 +82,10 @@ import Data.Map as Map;
 open Map using {Map};
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Int.Ord open;
 
 --- Definitions related to Alice's intent
 module AliceIntent;
-  
+
   logicFunction : LogicFunction
     | kind tx :=
       let
@@ -96,10 +95,10 @@ module AliceIntent;
         createdHashes : List LogicHash :=
           map Resource.logicHash createdRs;
       in isCreated kind
-        || (quantityOfDenom Dolphin.denomination createdRs == 1
-          && quantityOfDenom A.denomination createdRs == 1)
-        || quantityOfDenom Dolphin.denomination createdRs == 1
-        && quantityOfDenom B.denomination createdRs == 2;
+        || (quantityOfDenom Dolphin.denomination createdRs == ofNat 1
+          && quantityOfDenom A.denomination createdRs == ofNat 1)
+        || quantityOfDenom Dolphin.denomination createdRs == ofNat 1
+        && quantityOfDenom B.denomination createdRs == ofNat 2;
 
   --- This will be computed from the logic function
   logicHash : LogicHash := 1;

Simulator.juvix

@@ -7,13 +7,14 @@ import Simulator.PartialTx open public;
 import Simulator.Denomination open public;
 
 import Stdlib.Prelude open;
-import Stdlib.Debug.Fail open;
 import Data.ByteString open public;
 
 import Data.Map as Map;
 open Map using {Map};
 open Resource;
-validPartialTx (m : Map LogicHash LogicFunction) 
+
+validPartialTx {{Partial}}
+  (m : Map LogicHash LogicFunction)
   (ptx : PartialTx) : Bool :=
   let
     getLogicFn (kind : ResourceKind) (res : Resource)
@@ -42,8 +43,8 @@ balanceDelta (tx : PartialTx) : Balance :=
     (sumBalances (map mkBalance (consumedResources tx)))
     (sumBalances (map mkBalance (createdResources tx)));
 
-checkTransaction 
-  (m : Map LogicHash LogicFunction) 
+checkTransaction {{Partial}}
+  (m : Map LogicHash LogicFunction)
   (ptxs : List PartialTx) : Bool :=
   let
     allValid : Bool := all (validPartialTx m) ptxs;

Simulator/Balance.juvix

@@ -6,7 +6,6 @@ import Simulator.Resource open;
 import Simulator.Denomination open;
 
 import Data.Map as Map;
-import Stdlib.Data.Int as Int;
 import Stdlib.Data.Int.Ord as Int;
 
 type Balance :=
@@ -17,7 +16,7 @@ emptyBalance : Balance := balance nil;
 addBalance : Balance -> Balance -> Balance
   | (balance xs) (balance ys) :=
     balance
-      (Map.toList (Map.fromListWith (Int.+) (xs ++ ys)));
+      (Map.toList (Map.fromListWith (+) (xs ++ ys)));
 
 negateBalance : Balance -> Balance
   | (balance bs) := balance (map (b in bs) second neg b);

Simulator/Resource.juvix

@@ -4,8 +4,6 @@ import Stdlib.Prelude open;
 import Data.ByteString open;
 import Simulator.Denomination open;
 
-import Stdlib.Data.Int as Int;
-
 --- A ;Resource; is an immutable object that represents part of an application's
 --- state.
 type Resource :=
@@ -34,8 +32,8 @@ resourcesForDenom (d : Denomination) (rs : List Resource)
 --- Aggregate the quantities associated with a denomination
 quantityOfDenom (d : Denomination) (rs : List Resource)
   : Int :=
-  for (acc := Int.ofNat 0) (r in resourcesForDenom d rs)
-    quantity r Int.+ acc;
+  for (acc := ofNat 0) (r in resourcesForDenom d rs)
+    quantity r + acc;
 
 --- Return true if the list is empty or the list has exactly 1 element and the predicate is satisfied
 zeroOrOneCheck : (Resource -> Bool) -> List Resource -> Bool

Test/AppsTest.juvix

@@ -16,7 +16,7 @@ open Sudoku hiding {logicFunctions};
 
 import Test.JuvixUnit open;
 
-twoPartyExchange : Test :=
+twoPartyExchange {{Partial}} : Test :=
   let
     txs : List PartialTx :=
       Alice.partialTransaction
@@ -29,8 +29,7 @@ twoPartyExchange : Test :=
       "expected two-party exchange transactions to validate"
       (checkTransaction TwoPartyExchange.logicFunctions txs));
 
-
-sudoku : Test :=
+sudoku {{Partial}} : Test :=
   let
     solution : ByteString :=
       1
@@ -51,12 +50,12 @@ sudoku : Test :=
         :: 3
         :: nil;
 
-    puzzleData : Sudoku.Puzzle := 
+    puzzleData : Sudoku.Puzzle :=
       Sudoku.mkPuzzle (logicHash := 3; solution := solution);
-    
+
     dealerPartialTx : PartialTx := dealer puzzleData (1 :: replicate 15 0);
 
-    alicePartialTx : PartialTx  := 
+    alicePartialTx : PartialTx  :=
       mkPartialTx (
         createdPair := Sudoku.mkResource puzzleData (1 :: 2 :: replicate 14 0) 1
             , Reward.mkResource 1;
@@ -66,10 +65,10 @@ sudoku : Test :=
 
     bobPartialTx : PartialTx :=
       mkPartialTx (
-        createdPair := 
+        createdPair :=
           Sudoku.mkResource puzzleData solution 0
             , Reward.mkResource 14;
-        consumedPair := 
+        consumedPair :=
           Sudoku.mkResource puzzleData (1 :: 2 :: replicate 14 0) 1
             , Dealer.mkResource puzzleData 1
           );
@@ -82,7 +81,7 @@ sudoku : Test :=
       "expected Sudoku solutions to validate"
       (checkTransaction (Sudoku.logicFunctions puzzleData) txs));
 
-emptyTest : Test :=
+emptyTest {{Partial}} : Test :=
   let
     emptyFunctions : Map LogicHash LogicFunction := Map.empty;
   in testCase
@@ -91,9 +90,10 @@ emptyTest : Test :=
       "expected transactions to validate"
       (checkTransaction emptyFunctions nil));
 
-tests : List Test := emptyTest :: 
-  twoPartyExchange :: 
-  sudoku :: 
+tests {{Partial}} : List Test := emptyTest ::
+  twoPartyExchange ::
+  sudoku ::
   nil;
 
-main : IO := runTestSuite (testSuite "Taiga simulator" tests);
+main : IO :=
+  runPartial λ {{{_}} := runTestSuite (testSuite "Taiga simulator" tests)};