{-# LANGUAGE OverloadedStrings, AllowAmbiguousTypes #-}

module Rerefined.Refine where

import Rerefined.Refined
import Rerefined.Refined1
import Rerefined.Predicate
import GHC.Exts ( proxy#, IsString )

-- | Refine @a@ with predicate @p@.
refine
    :: forall p a. Refine p a
    => a -> Either (RefineFailure String) (Refined p a)
refine :: forall {k} (p :: k) a.
Refine p a =>
a -> Either (RefineFailure String) (Refined p a)
refine a
a =
    case Proxy# p -> a -> Maybe (RefineFailure String)
forall {k} (p :: k) a.
Refine p a =>
Proxy# p -> a -> Maybe (RefineFailure String)
validate (forall (a :: k). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @p) a
a of
      Maybe (RefineFailure String)
Nothing -> Refined p a -> Either (RefineFailure String) (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 String
e  -> RefineFailure String -> Either (RefineFailure String) (Refined p a)
forall a b. a -> Either a b
Left RefineFailure String
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 String) (Refined1 p f a)
refine1 :: forall {k} {k1} (p :: k) (f :: k1 -> Type) (a :: k1).
Refine1 p f =>
f a -> Either (RefineFailure String) (Refined1 p f a)
refine1 f a
fa =
    case Proxy# p -> f a -> Maybe (RefineFailure String)
forall (a :: k1). Proxy# p -> f a -> Maybe (RefineFailure String)
forall {k} {k1} (p :: k) (f :: k1 -> Type) (a :: k1).
Refine1 p f =>
Proxy# p -> f a -> Maybe (RefineFailure String)
validate1 (forall (a :: k). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @p) f a
fa of
      Maybe (RefineFailure String)
Nothing -> Refined1 p f a -> Either (RefineFailure String) (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 String
e  -> RefineFailure String
-> Either (RefineFailure String) (Refined1 p f a)
forall a b. a -> Either a b
Left RefineFailure String
e

-- TODO needs work. boring & idk how to format nicely. and extra \n at start
prettyRefineFailure :: (Semigroup a, IsString a) => RefineFailure a -> a
prettyRefineFailure :: forall a. (Semigroup a, IsString a) => RefineFailure a -> a
prettyRefineFailure = Int -> [RefineFailure a] -> a
go (Int
0 :: Int) ([RefineFailure a] -> a)
-> (RefineFailure a -> [RefineFailure a]) -> RefineFailure a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\RefineFailure a
e -> [RefineFailure a
e])
  where
    go :: Int -> [RefineFailure a] -> a
go Int
n = \case
      []     -> a
""
      (RefineFailure a
e:[RefineFailure a]
es) ->
           a
"\n" a -> a -> a
forall a. Semigroup a => a -> a -> a
<> Int -> a
indent Int
n     a -> a -> a
forall a. Semigroup a => a -> a -> a
<> RefineFailure a -> a
forall a. RefineFailure a -> a
refineFailurePredicate RefineFailure a
e
        a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
"\n" a -> a -> a
forall a. Semigroup a => a -> a -> a
<> Int -> a
indent (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) a -> a -> a
forall a. Semigroup a => a -> a -> a
<> RefineFailure a -> a
forall a. RefineFailure a -> a
refineFailureDetail    RefineFailure a
e
        a -> a -> a
forall a. Semigroup a => a -> a -> a
<> Int -> [RefineFailure a] -> a
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) (RefineFailure a -> [RefineFailure a]
forall a. RefineFailure a -> [RefineFailure a]
refineFailureInner RefineFailure a
e)
        a -> a -> a
forall a. Semigroup a => a -> a -> a
<> Int -> [RefineFailure a] -> a
go Int
n [RefineFailure a]
es
    indent :: Int -> a
indent = \case
      Int
0 -> a
""
      Int
n -> a
" " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> Int -> a
indent (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)