{-# LANGUAGE OverloadedStrings #-}
module Rerefined.Refine
(
type Refined
, refine
, unrefine
, type Refined1
, refine1
, unrefine1
, type RefineFailure
, prettyRefineFailure
, prettyRefineFailure'
) where
import Rerefined.Refined
import Rerefined.Predicate
import GHC.Exts ( proxy# )
import Data.Text ( Text )
import Data.Text.Builder.Linear qualified as TBL
refine
:: forall p a. Refine p a
=> a -> Either RefineFailure (Refined p a)
refine :: forall {k} (p :: k) a.
Refine p a =>
a -> Either RefineFailure (Refined p a)
refine a
a =
case Proxy# p -> a -> Maybe RefineFailure
forall {k} (p :: k) a.
Refine p a =>
Proxy# p -> a -> Maybe RefineFailure
validate (forall (a :: k). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @p) a
a of
Maybe RefineFailure
Nothing -> Refined p a -> Either RefineFailure (Refined p a)
forall a b. b -> Either a b
Right (a -> Refined p a
forall {k} (p :: k) a. a -> Refined p a
Refined a
a)
Just RefineFailure
e -> RefineFailure -> Either RefineFailure (Refined p a)
forall a b. a -> Either a b
Left RefineFailure
e
refine1
:: forall p f a. Refine1 p f
=> f a -> Either RefineFailure (Refined1 p f a)
refine1 :: forall {k} {k1} (p :: k) (f :: k1 -> Type) (a :: k1).
Refine1 p f =>
f a -> Either RefineFailure (Refined1 p f a)
refine1 f a
fa =
case Proxy# p -> f a -> Maybe RefineFailure
forall (a :: k1). Proxy# p -> f a -> Maybe RefineFailure
forall {k} {k1} (p :: k) (f :: k1 -> Type) (a :: k1).
Refine1 p f =>
Proxy# p -> f a -> Maybe RefineFailure
validate1 (forall (a :: k). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @p) f a
fa of
Maybe RefineFailure
Nothing -> Refined1 p f a -> Either RefineFailure (Refined1 p f a)
forall a b. b -> Either a b
Right (f a -> Refined1 p f a
forall {k} {k1} (p :: k) (f :: k1 -> Type) (a :: k1).
f a -> Refined1 p f a
Refined1 f a
fa)
Just RefineFailure
e -> RefineFailure -> Either RefineFailure (Refined1 p f a)
forall a b. a -> Either a b
Left RefineFailure
e
prettyRefineFailure :: RefineFailure -> Text
prettyRefineFailure :: RefineFailure -> Text
prettyRefineFailure = Builder -> Text
Builder -> Text
TBL.runBuilder (Builder -> Text)
-> (RefineFailure -> Builder) -> RefineFailure -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [RefineFailure] -> Builder
go (Int
0 :: Int) ([RefineFailure] -> Builder)
-> (RefineFailure -> [RefineFailure]) -> RefineFailure -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\RefineFailure
e -> [RefineFailure
e])
where
go :: Int -> [RefineFailure] -> Builder
go Int
n = \case
[] -> Builder
forall a. Monoid a => a
mempty
(RefineFailure
e:[RefineFailure]
es) ->
let bPred :: Builder
bPred = Char -> Builder
TBL.fromChar Char
'\n' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
indent Int
n Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> RefineFailure -> Builder
refineFailurePredicate RefineFailure
e
bDetail :: Builder
bDetail = Char -> Builder
TBL.fromChar Char
'\n' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
indent (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> RefineFailure -> Builder
refineFailureDetail RefineFailure
e
in Builder
bPred Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
bDetail Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> [RefineFailure] -> Builder
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) (RefineFailure -> [RefineFailure]
refineFailureInner RefineFailure
e) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> [RefineFailure] -> Builder
go Int
n [RefineFailure]
es
indent :: Int -> Builder
indent = \case
Int
0 -> Builder
forall a. Monoid a => a
mempty
Int
n -> Char -> Builder
TBL.fromChar Char
' ' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
indent (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
prettyRefineFailure' :: RefineFailure -> Text
prettyRefineFailure' :: RefineFailure -> Text
prettyRefineFailure' = \RefineFailure
e -> Builder -> Text
Builder -> Text
TBL.runBuilder (Builder -> Text) -> Builder -> Text
forall a b. (a -> b) -> a -> b
$ Builder -> [(Int, RefineFailure)] -> Builder
go Builder
forall a. Monoid a => a
mempty [(Int
0 :: Int, RefineFailure
e)]
where
go :: Builder -> [(Int, RefineFailure)] -> Builder
go Builder
b = \case
[] -> Builder
b
((Int
n, RefineFailure
e) : [(Int, RefineFailure)]
es) ->
let bPred :: Builder
bPred = Char -> Builder
TBL.fromChar Char
'\n' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
indent Int
n Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> RefineFailure -> Builder
refineFailurePredicate RefineFailure
e
bDetail :: Builder
bDetail = Char -> Builder
TBL.fromChar Char
'\n' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
indent (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> RefineFailure -> Builder
refineFailureDetail RefineFailure
e
b' :: Builder
b' = Builder
b Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
bPred Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
bDetail
in Builder -> [(Int, RefineFailure)] -> Builder
go Builder
b' (Int
-> [(Int, RefineFailure)]
-> [RefineFailure]
-> [(Int, RefineFailure)]
forall {a} {b}. a -> [(a, b)] -> [b] -> [(a, b)]
idk (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) [(Int, RefineFailure)]
es (RefineFailure -> [RefineFailure]
refineFailureInner RefineFailure
e))
indent :: Int -> Builder
indent = \case
Int
0 -> Builder
forall a. Monoid a => a
mempty
Int
n -> Char -> Builder
TBL.fromChar Char
' ' Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
indent (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
idk :: a -> [(a, b)] -> [b] -> [(a, b)]
idk a
n [(a, b)]
rs = \case
[] -> [(a, b)]
rs
b
l:[b]
ls -> a -> [(a, b)] -> [b] -> [(a, b)]
idk a
n ((a
n, b
l)(a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:[(a, b)]
rs) [b]
ls