From fd4eb7dd00d813477498ba05431ba1ae89b4ec33 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Wed, 12 Apr 2023 11:59:51 -0400 Subject: [PATCH] Create `Simple` function --- src/Control/Lens/Equality.idr | 2 +- src/Control/Lens/Getter.idr | 2 +- src/Control/Lens/Iso.idr | 2 +- src/Control/Lens/Lens.idr | 2 +- src/Control/Lens/Optic.idr | 5 +++++ src/Control/Lens/Optional.idr | 2 +- src/Control/Lens/OptionalFold.idr | 2 +- src/Control/Lens/Prism.idr | 2 +- src/Control/Lens/Setter.idr | 2 +- src/Control/Lens/Traversal.idr | 2 +- 10 files changed, 14 insertions(+), 9 deletions(-) diff --git a/src/Control/Lens/Equality.idr b/src/Control/Lens/Equality.idr index cead56b..8731f48 100644 --- a/src/Control/Lens/Equality.idr +++ b/src/Control/Lens/Equality.idr @@ -15,7 +15,7 @@ Equality s t a b = forall p. IsEquality p => p a b -> p s t public export 0 Equality' : k -> k -> Type -Equality' s a = Equality s s a a +Equality' = Simple Equality public export diff --git a/src/Control/Lens/Getter.idr b/src/Control/Lens/Getter.idr index 6d200a3..668d08c 100644 --- a/src/Control/Lens/Getter.idr +++ b/src/Control/Lens/Getter.idr @@ -21,7 +21,7 @@ getterToLens @{MkIsGetter _} = MkIsLens %search public export 0 Getter : (s,a : Type) -> Type -Getter s a = Optic IsGetter s s a a +Getter = Simple (Optic IsGetter) public export diff --git a/src/Control/Lens/Iso.idr b/src/Control/Lens/Iso.idr index 493be10..7cc1d42 100644 --- a/src/Control/Lens/Iso.idr +++ b/src/Control/Lens/Iso.idr @@ -23,7 +23,7 @@ Iso = Optic IsIso public export 0 Iso' : (s,a : Type) -> Type -Iso' s a = Iso s s a a +Iso' = Simple Iso public export diff --git a/src/Control/Lens/Lens.idr b/src/Control/Lens/Lens.idr index 3d52d64..c461b7b 100644 --- a/src/Control/Lens/Lens.idr +++ b/src/Control/Lens/Lens.idr @@ -25,7 +25,7 @@ Lens = Optic IsLens public export 0 Lens' : (s,a : Type) -> Type -Lens' s a = Lens s s a a +Lens' = Simple Lens public export diff --git a/src/Control/Lens/Optic.idr b/src/Control/Lens/Optic.idr index 764c4a1..3947389 100644 --- a/src/Control/Lens/Optic.idr +++ b/src/Control/Lens/Optic.idr @@ -5,6 +5,11 @@ import Data.Profunctor %default total +public export +Simple : (k -> k -> k' -> k' -> r) -> k -> k' -> r +Simple f s a = f s s a a + + public export Optic' : (p : Type -> Type -> Type) -> (s,t,a,b : Type) -> Type Optic' p s t a b = p a b -> p s t diff --git a/src/Control/Lens/Optional.idr b/src/Control/Lens/Optional.idr index e1adac3..79db1dd 100644 --- a/src/Control/Lens/Optional.idr +++ b/src/Control/Lens/Optional.idr @@ -27,7 +27,7 @@ Optional = Optic IsOptional public export 0 Optional' : (s,a : Type) -> Type -Optional' s a = Optional s s a a +Optional' = Simple Optional public export diff --git a/src/Control/Lens/OptionalFold.idr b/src/Control/Lens/OptionalFold.idr index b46b6f8..8dcb1a9 100644 --- a/src/Control/Lens/OptionalFold.idr +++ b/src/Control/Lens/OptionalFold.idr @@ -26,7 +26,7 @@ optFoldToGetter @{MkIsOptFold _} = MkIsGetter %search public export 0 OptionalFold : (s,a : Type) -> Type -OptionalFold s a = Optic IsOptFold s s a a +OptionalFold = Simple (Optic IsOptFold) public export diff --git a/src/Control/Lens/Prism.idr b/src/Control/Lens/Prism.idr index ee1559c..dcedc21 100644 --- a/src/Control/Lens/Prism.idr +++ b/src/Control/Lens/Prism.idr @@ -23,7 +23,7 @@ Prism = Optic IsPrism public export 0 Prism' : (s,a : Type) -> Type -Prism' s a = Prism s s a a +Prism' = Simple Prism public export diff --git a/src/Control/Lens/Setter.idr b/src/Control/Lens/Setter.idr index 7800c56..bbb0c42 100644 --- a/src/Control/Lens/Setter.idr +++ b/src/Control/Lens/Setter.idr @@ -28,7 +28,7 @@ Setter = Optic IsSetter public export 0 Setter' : (s,a : Type) -> Type -Setter' s a = Optic IsSetter s s a a +Setter' = Simple Setter public export diff --git a/src/Control/Lens/Traversal.idr b/src/Control/Lens/Traversal.idr index a6eb358..1c2b0dc 100644 --- a/src/Control/Lens/Traversal.idr +++ b/src/Control/Lens/Traversal.idr @@ -27,7 +27,7 @@ Traversal = Optic IsTraversal public export 0 Traversal' : (s,a : Type) -> Type -Traversal' s a = Traversal s s a a +Traversal' = Simple Traversal public export