From d59c628052443940e5c2ba770c3f44bdc5508e78 Mon Sep 17 00:00:00 2001 From: mariari Date: Fri, 8 Nov 2024 13:40:31 +0800 Subject: [PATCH 1/2] Losen the Constraints on the Partial Trait Partial trait relied upon import Stdlib.Data.String.Base open; which indirectly relies upon list, we loosen the restriction to just rely on the String type itself. This lets us move some functions around to the base module --- Stdlib/Debug/Fail.juvix | 2 +- Stdlib/Trait/Partial.juvix | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Stdlib/Debug/Fail.juvix b/Stdlib/Debug/Fail.juvix index 45a106e6..bfc03523 100644 --- a/Stdlib/Debug/Fail.juvix +++ b/Stdlib/Debug/Fail.juvix @@ -1,6 +1,6 @@ module Stdlib.Debug.Fail; -import Stdlib.Data.String.Base open; +import Juvix.Builtin.V1.String open; --- Exit the program with an error message. builtin fail diff --git a/Stdlib/Trait/Partial.juvix b/Stdlib/Trait/Partial.juvix index 1670c417..9b2e3449 100644 --- a/Stdlib/Trait/Partial.juvix +++ b/Stdlib/Trait/Partial.juvix @@ -1,6 +1,6 @@ module Stdlib.Trait.Partial; -import Stdlib.Data.String.Base open; +import Juvix.Builtin.V1.String open; import Stdlib.Debug.Fail as Debug; trait From 8483879fadb0a0d0e4213e614c7ecd3d9ec3a001 Mon Sep 17 00:00:00 2001 From: mariari Date: Fri, 8 Nov 2024 13:40:36 +0800 Subject: [PATCH 2/2] Move Phead to List Base --- Stdlib/Data/List.juvix | 5 ----- Stdlib/Data/List/Base.juvix | 6 ++++++ 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix index f62aa06d..0091378d 100644 --- a/Stdlib/Data/List.juvix +++ b/Stdlib/Data/List.juvix @@ -16,11 +16,6 @@ import Stdlib.Trait.Foldable open using { fromPolymorphicFoldable; }; ---- 𝒪(1). Partial function that returns the first element of a ;List;. -phead {A} {{Partial}} : List A -> A - | (x :: _) := x - | nil := fail "head: empty list"; - instance eqListI {A} {{Eq A}} : Eq (List A) := let diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index bc8d0900..425a850b 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/Stdlib/Data/List/Base.juvix @@ -7,6 +7,7 @@ import Stdlib.Function open; import Stdlib.Data.Nat.Base open; import Stdlib.Data.Maybe.Base open; import Stdlib.Trait.Ord open; +import Stdlib.Trait.Partial open; import Stdlib.Data.Pair.Base open; --- 𝒪(𝓃). Returns ;true; if the given object elem is in the ;List;. @@ -165,6 +166,11 @@ head {A} (defaultValue : A) (list : List A) : A := | x :: _ := x | nil := defaultValue; +--- 𝒪(1). Partial function that returns the first element of a ;List;. +phead {A} {{Partial}} : List A -> A + | (x :: _) := x + | nil := fail "head: empty list"; + syntax iterator any {init := 0; range := 1}; --- 𝒪(𝓃). Returns ;true; if at least one element of the ;List; satisfies the predicate.