Add AppendList

Stdlib/Data/AppendList.juvix

@@ -0,0 +1,23 @@
+module Stdlib.Data.AppendList;
+
+import Stdlib.Data.List open public;
+import Stdlib.Data.Nat open public;
+import Stdlib.Data.AppendList.Base open public;
+import Stdlib.Data.Bool.Base open;
+import Stdlib.Data.String.Base open;
+import Stdlib.Function open;
+import Stdlib.Trait open;
+
+instance
+showAppendListI {A} {{Show A}} : Show (AppendList A) :=
+  Show.mk (AppendList.toList >> Show.show);
+
+instance
+eqAppendListI {A} {{Eq A}} : Eq (AppendList A) :=
+  Eq.mk@{
+    isEqual (a b : AppendList A) : Bool :=
+      Eq.isEqual (AppendList.toList a) (AppendList.toList b);
+  };
+
+instance
+functorAppendListI : Functor AppendList := Functor.mk AppendList.map;

Stdlib/Data/AppendList/Base.juvix

@@ -0,0 +1,55 @@
+module Stdlib.Data.AppendList.Base;
+
+import Stdlib.Data.List.Base as List open;
+import Stdlib.Data.Bool.Base open;
+import Stdlib.Function open;
+import Stdlib.Data.Nat.Base open;
+import Stdlib.Trait.Semigroup open public;
+
+--- A list-like structure with 𝒪(1) concatenation
+type AppendList A :=
+  privateMk@{
+    unwrap : List A -> List A;
+  }
+with
+  instance
+  semigroupAppendListI {A} : Semigroup (AppendList A) := Semigroup.mk append;
+
+  --- 𝒪(1)
+  {-# inline: true #-}
+  append {A} : AppendList A -> AppendList A -> AppendList A
+    | (privateMk l1) (privateMk l2) := privateMk (l2 >> l1);
+
+  --- 𝒪(𝓃)
+  {-# inline: true #-}
+  toList {A} : AppendList A -> List A
+    | (privateMk l) := l [];
+
+  --- 𝒪(1)
+  {-# inline: true #-}
+  fromList {A} (l : List A) : AppendList A := privateMk \{l' := l ++ l'};
+
+  {-# inline: true #-}
+  empty {A} : AppendList A := fromList [];
+
+  {-# inline: true #-}
+  singleton {A} (x : A) : AppendList A := privateMk \{l' := x :: l'};
+
+  --- 𝒪(1) Append an element at the start
+  {-# inline: true #-}
+  cons {A} (x : A) : AppendList A -> AppendList A := append (singleton x);
+
+  --- 𝒪(1) Append an element to the end
+  {-# inline: true #-}
+  consEnd {A} (l : AppendList A) (x : A) : AppendList A :=
+    append l (singleton x);
+
+  --- 𝒪(𝓃)
+  {-# inline: true #-}
+  length {A} : AppendList A -> Nat := toList >> List.length;
+
+  --- 𝒪(𝓃)
+  {-# inline: true #-}
+  map {A} {B} (f : A -> B) (l : AppendList A) : AppendList B :=
+    privateMk \{tail := listMap f (toList l) ++ tail};
+end;

Stdlib/Trait/Semigroup.juvix

@@ -21,4 +21,4 @@ with
   end;
 end;
 
-open Semigroup hiding {mk} public;
+open Semigroup using {++} public;