CI: set bundled stdlib to the PR branch commit

.github/workflows/ci.yml

@@ -28,7 +28,14 @@ jobs:
         with:
           repository: anoma/juvix
           path: juvix
-          submodules: true
+          submodules: false
+
+      - name: Set bundled stdlib to PR branch commit
+        run: |
+          cd juvix
+          git submodule update --init --recursive
+          cd juvix-stdlib
+          git checkout $GITHUB_SHA || git checkout ${{ github.event.pull_request.head.sha }}
 
       - name: install LLVM
         run: |
@@ -46,7 +53,7 @@ jobs:
           working-directory: juvix
           test: false
           fast: false
-      
+
       - name: Install Juvix
         run: |
           cd juvix
@@ -55,7 +62,7 @@ jobs:
 
       - name: Checkout Std Library
         uses: actions/checkout@v3
- 
+
       - name : Typecheck library code
         run : make check
 

Stdlib/Data/List.juvix

@@ -105,11 +105,7 @@ traversableListI : Traversable List :=
   mkTraversable@{
     terminating
     sequenceA
-      {F : Type -> Type}
-      {{Applicative F}}
-      {A}
-      (xs : List (F A))
-      : F (List A) :=
+      {F : Type -> Type} {{Applicative F}} {A} (xs : List (F A)) : F (List A) :=
       case xs of
         | nil := pure nil
         | x :: xs := liftA2 (::) x (sequenceA xs);

Stdlib/Data/Set.juvix

@@ -138,12 +138,7 @@ open Internal;
 --- Ord A, Ord K and fun must be compatible. i.e cmp_k (fun a1) (fun a2) == cmp_a a1 a2
 {-# specialize: [1, 2] #-}
 lookupWith
-  {A K}
-  {{order : Ord K}}
-  (fun : A -> K)
-  (elem : K)
-  (set : Set A)
-  : Maybe A :=
+  {A K} {{order : Ord K}} (fun : A -> K) (elem : K) (set : Set A) : Maybe A :=
   let
     {-# specialize-by: [order, fun] #-}
     go : Set A -> Maybe A
@@ -172,12 +167,7 @@ isMember {A} {{Ord A}} (elem : A) (set : Set A) : Bool :=
 --- where == comes from Ord a.
 {-# specialize: [1, 2] #-}
 insertWith
-  {A}
-  {{order : Ord A}}
-  (fun : A -> A -> A)
-  (elem : A)
-  (set : Set A)
-  : Set A :=
+  {A} {{order : Ord A}} (fun : A -> A -> A) (elem : A) (set : Set A) : Set A :=
   let
     {-# specialize-by: [order, fun] #-}
     go : Set A -> Set A
@@ -235,8 +225,7 @@ deleteWith
 
 --- 𝒪(log 𝓃). Removes `elem` from `set`.
 {-# specialize: [1] #-}
-delete {A} {{Ord A}} (elem : A) (set : Set A) : Set A :=
-  deleteWith id elem set;
+delete {A} {{Ord A}} (elem : A) (set : Set A) : Set A := deleteWith id elem set;
 
 --- 𝒪(log 𝓃). Returns the minimum element of `set`.
 lookupMin {A} : (set : Set A) -> Maybe A
@@ -309,8 +298,7 @@ instance
 polymorphicFoldableSetI : Polymorphic.Foldable Set :=
   Polymorphic.mkFoldable@{
     {-# inline: true #-}
-    for {A B} (f : B -> A -> B) (acc : B) (set : Set A) : B :=
-      foldl f acc set;
+    for {A B} (f : B -> A -> B) (acc : B) (set : Set A) : B := foldl f acc set;
     {-# inline: true #-}
     rfor {A B} (f : B -> A -> B) (acc : B) (set : Set A) : B :=
       foldr (flip f) acc set;
@@ -423,11 +411,7 @@ filter {A} {{Ord A}} (predicate : A -> Bool) (set : Set A) : Set A :=
 
 syntax iterator partition {init := 0; range := 1};
 partition
-  {A}
-  {{Ord A}}
-  (predicate : A -> Bool)
-  (set : Set A)
-  : Pair (Set A) (Set A) :=
+  {A} {{Ord A}} (predicate : A -> Bool) (set : Set A) : Pair (Set A) (Set A) :=
   for (trueSet, falseSet := empty, empty) (x in set) {
     if
       | predicate x := insert x trueSet, falseSet