Strengthen Cons and Snoc interfaces

This commit is contained in:
Kiana Sheibani 2023-04-25 12:39:52 -04:00
parent e1da48721e
commit e980b3602d
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
3 changed files with 57 additions and 9 deletions

View file

@ -4,6 +4,7 @@ import Data.Profunctor
import Control.Lens.Optic
import Control.Lens.Iso
import Control.Lens.Prism
import Control.Lens.Review
import Control.Lens.Optional
%default total
@ -13,9 +14,15 @@ import Control.Lens.Optional
||| left side of a sequence.
public export
interface Cons s t a b | s where
||| This is a prism that can attach or detach a value from the left side of a
||| An isomorphism that can inspact the left side of a sequence.
consIso : Iso s t (Maybe (a, s)) (Maybe (b, t))
||| A prism that can attach or detach a value from the left side of a
||| sequence.
cons_ : Prism s t (a, s) (b, t)
cons_ = consIso . prism Just (\case
Nothing => Left Nothing
Just x => Right x)
||| Access the head (left-most element) of a sequence, if it is non-empty.
public export
@ -28,14 +35,25 @@ public export
tail_ : Cons s s a a => Optional' s s
tail_ @{_} @{MkIsOptional _} = cons_ . second
||| Use a `Cons` implementation to construct an empty sequence.
public export
nil : Cons s s a a => s
nil = review consIso Nothing
||| An interface that provides a way to detach and inspect elements from the
||| right side of a sequence.
public export
interface Snoc s t a b | s where
||| An isomorphism that can inspact the right side of a sequence.
snocIso : Iso s t (Maybe (s, a)) (Maybe (t, b))
||| This is a prism that can attach or detach a value from the right side of a
||| sequence.
snoc_ : Prism s t (s, a) (t, b)
snoc_ = snocIso . prism Just (\case
Nothing => Left Nothing
Just x => Right x)
||| Access all but the right-most element of a sequence, if it is non-empty.
public export
@ -46,3 +64,8 @@ init_ @{_} @{MkIsOptional _} = snoc_ . first
public export
last_ : Snoc s s a a => Optional' s a
last_ @{_} @{MkIsOptional _} = snoc_ . second
||| Use a `Snoc` implementation to construct an empty sequence.
public export
nil' : Snoc s s a a => s
nil' = review snocIso Nothing

View file

@ -48,22 +48,30 @@ reversed = iso reverse reverse
public export
Ixed Nat a (List a) where
ix n = optional' (getAt n) (\xs,x => case inBounds n xs of
Yes _ => replaceAt n x xs
No _ => xs)
ix = element
public export
Cons (List a) (List b) a b where
consIso = iso (\case
[] => Nothing
x :: xs => Just (x,xs))
(maybe [] $ uncurry (::))
cons_ = prism (uncurry (::)) (\case
[] => Left []
x :: xs => Right (x, xs))
unsnoc : a -> List a -> (List a, a)
unsnoc x [] = ([], x)
unsnoc x (y :: xs) = mapFst (x ::) $ unsnoc y xs
public export
Snoc (List a) (List b) a b where
snocIso = iso (\case
[] => Nothing
x :: xs => Just $ unsnoc x xs)
(maybe [] $ uncurry snoc)
snoc_ = prism (uncurry snoc) (\case
[] => Left []
x :: xs => Right $ unsnoc x xs)
where
unsnoc : a -> List a -> (List a, a)
unsnoc x [] = ([], x)
unsnoc x (y :: xs) = mapFst (x ::) $ unsnoc y xs

View file

@ -26,6 +26,11 @@ public export
packed : Iso' (List Char) String
packed = iso pack unpack
||| An isomorphism between a string and its reverse.
public export
reversed : Iso' String String
reversed = involuted reverse
public export
Ixed Nat Char String where
@ -33,8 +38,20 @@ Ixed Nat Char String where
public export
Cons String String Char Char where
consIso = iso strUncons (maybe "" $ uncurry strCons)
cons_ = prism' (uncurry strCons) strUncons
snoc : String -> Char -> String
snoc s c = s ++ singleton c
unsnoc : String -> Maybe (String, Char)
unsnoc s =
case length s of
Z => Nothing
(S n) => Just (substr Z n s,
assert_total $ strIndex s (cast n))
public export
Snoc String String Char Char where
snoc_ = unpacked . snoc_ . mappingFst packed
snocIso = iso unsnoc (maybe "" $ uncurry snoc)
snoc_ = prism' (uncurry snoc) unsnoc