{-# LANGUAGE OverloadedStrings #-}

module Rerefined.Refine
  (
  -- * @Refined@
    type Refined
  , refine
  , unrefine

  -- * @Refined1@
  , type Refined1
  , refine1
  , unrefine1

  -- * Errors
  , 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 @a@ with predicate @p@.
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

-- reifyPredicate is just a weaker version of validate without proxy.
-- Maybe the latter is useful, though...?

-- | Refine @f a@ with functor predicate @p@.
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

{- TODO
* got an extra \n at start oops
* make it look better lol
* make tail-call recursive? need to ferry more indents around though
-}
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)

-- TODO this requires switching inner errors so that last is first lol x)
-- also we only <> right. maybe that's useful for perf
-- to remove newline at start we need to start in a special mode so we know not
-- to add the first newline at bPred. but I cba it will be messier and I want to
-- replace this ASAP when someone comes up with a good pretty error format
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