diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index be480c6f..42f1843f 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix index e1e29043..91a188c0 100644 --- a/Stdlib/Data/List.juvix +++ b/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); diff --git a/Stdlib/Data/Set.juvix b/Stdlib/Data/Set.juvix index c6c7b900..ce2350d2 100644 --- a/Stdlib/Data/Set.juvix +++ b/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