module Data.OpenApi.Compare.Formula
  ( FormulaF,
    VarRef,
    variable,
    eitherOf,
    anError,
    errors,
    calculate,
    maxFixpoint,
    mapErrors,
  )
where

import Data.Kind
import qualified Data.List.NonEmpty as NE
import Data.Monoid
import Data.OpenApi.Compare.Paths
import qualified Data.OpenApi.Compare.PathsPrefixTree as P

type VarRef = Int

-- | The type @FormulaF f r ()@ describes (modulo contents of errors) boolean
-- formulas involving variables, conjunctions, and disjunctions. These
-- operations (and the generated algebra) are monotonous. This ensures that
-- fixpoints always exist, i.e. that @x = f x@ has at least one solution.
data FormulaF (q :: k -> k -> Type) (f :: k -> Type) (r :: k) (a :: Type) where
  Result :: a -> FormulaF q f r a
  Errors ::
    !(P.PathsPrefixTree q f r) ->
    -- | invariant: never empty
    FormulaF q f r a
  Apply ::
    FormulaF q f r (b -> c) ->
    FormulaF q f r b ->
    (c -> a) ->
    -- | invariant: at least one of LHS and RHS is not 'Errors', and they are
    -- both not 'Result'
    FormulaF q f r a
  SelectFirst ::
    NE.NonEmpty (SomeFormulaF b) ->
    !(P.PathsPrefixTree q f r) ->
    (b -> a) ->
    -- | invariant: the list doesn't contain any 'Result's, 'Errors' or
    -- 'SelectFirst'
    FormulaF q f r a
  Variable :: !VarRef -> a -> FormulaF q f r a

mkApply :: FormulaF q f r (b -> c) -> FormulaF q f r b -> (c -> a) -> FormulaF q f r a
mkApply :: FormulaF q f r (b -> c)
-> FormulaF q f r b -> (c -> a) -> FormulaF q f r a
mkApply (Result b -> c
f) FormulaF q f r b
x c -> a
h = c -> a
h (c -> a) -> (b -> c) -> b -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> c
f (b -> a) -> FormulaF q f r b -> FormulaF q f r a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FormulaF q f r b
x
mkApply FormulaF q f r (b -> c)
f (Result b
x) c -> a
h = c -> a
h (c -> a) -> ((b -> c) -> c) -> (b -> c) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b -> c) -> b -> c
forall a b. (a -> b) -> a -> b
$ b
x) ((b -> c) -> a) -> FormulaF q f r (b -> c) -> FormulaF q f r a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FormulaF q f r (b -> c)
f
mkApply (Errors PathsPrefixTree q f r
e1) (Errors PathsPrefixTree q f r
e2) c -> a
_ = PathsPrefixTree q f r -> FormulaF q f r a
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
PathsPrefixTree q f r -> FormulaF q f r a
Errors (PathsPrefixTree q f r
e1 PathsPrefixTree q f r
-> PathsPrefixTree q f r -> PathsPrefixTree q f r
forall a. Semigroup a => a -> a -> a
<> PathsPrefixTree q f r
e2)
mkApply FormulaF q f r (b -> c)
f FormulaF q f r b
x c -> a
h = FormulaF q f r (b -> c)
-> FormulaF q f r b -> (c -> a) -> FormulaF q f r a
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) b c a.
FormulaF q f r (b -> c)
-> FormulaF q f r b -> (c -> a) -> FormulaF q f r a
Apply FormulaF q f r (b -> c)
f FormulaF q f r b
x c -> a
h

mkSelectFirst :: [SomeFormulaF b] -> P.PathsPrefixTree q f r -> (b -> a) -> FormulaF q f r a
mkSelectFirst :: [SomeFormulaF b]
-> PathsPrefixTree q f r -> (b -> a) -> FormulaF q f r a
mkSelectFirst [SomeFormulaF b]
fs PathsPrefixTree q f r
allE b -> a
h = case (SomeFormulaF b -> (First b, [SomeFormulaF b]))
-> [SomeFormulaF b] -> (First b, [SomeFormulaF b])
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap SomeFormulaF b -> (First b, [SomeFormulaF b])
forall a. SomeFormulaF a -> (First a, [SomeFormulaF a])
check [SomeFormulaF b]
fs of
  (First (Just b
x), [SomeFormulaF b]
_) -> a -> FormulaF q f r a
forall k a (q :: k -> k -> *) (f :: k -> *) (r :: k).
a -> FormulaF q f r a
Result (b -> a
h b
x)
  (First Maybe b
Nothing, SomeFormulaF b
x : [SomeFormulaF b]
xs) -> NonEmpty (SomeFormulaF b)
-> PathsPrefixTree q f r -> (b -> a) -> FormulaF q f r a
forall k b (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
NonEmpty (SomeFormulaF b)
-> PathsPrefixTree q f r -> (b -> a) -> FormulaF q f r a
SelectFirst (SomeFormulaF b
x SomeFormulaF b -> [SomeFormulaF b] -> NonEmpty (SomeFormulaF b)
forall a. a -> [a] -> NonEmpty a
NE.:| [SomeFormulaF b]
xs) PathsPrefixTree q f r
allE b -> a
h
  (First Maybe b
Nothing, []) -> PathsPrefixTree q f r -> FormulaF q f r a
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
PathsPrefixTree q f r -> FormulaF q f r a
Errors PathsPrefixTree q f r
allE
  where
    check :: SomeFormulaF a -> (First a, [SomeFormulaF a])
check (SomeFormulaF (Result a
x)) = (Maybe a -> First a
forall a. Maybe a -> First a
First (a -> Maybe a
forall a. a -> Maybe a
Just a
x), [SomeFormulaF a]
forall a. Monoid a => a
mempty)
    check (SomeFormulaF (Errors PathsPrefixTree q f r
_)) = (First a
forall a. Monoid a => a
mempty, [SomeFormulaF a]
forall a. Monoid a => a
mempty)
    check (SomeFormulaF (SelectFirst NonEmpty (SomeFormulaF b)
xs PathsPrefixTree q f r
_ b -> a
h')) =
      (First a
forall a. Monoid a => a
mempty, NonEmpty (SomeFormulaF a) -> [SomeFormulaF a]
forall a. NonEmpty a -> [a]
NE.toList ((SomeFormulaF b -> SomeFormulaF a)
-> NonEmpty (SomeFormulaF b) -> NonEmpty (SomeFormulaF a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> a) -> SomeFormulaF b -> SomeFormulaF a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> a
h') NonEmpty (SomeFormulaF b)
xs))
    check SomeFormulaF a
x = (First a
forall a. Monoid a => a
mempty, [SomeFormulaF a
x])

data SomeFormulaF (a :: Type) where
  SomeFormulaF :: FormulaF q f r a -> SomeFormulaF a

anError :: AnItem q f r -> FormulaF q f r a
anError :: AnItem q f r -> FormulaF q f r a
anError AnItem q f r
e = PathsPrefixTree q f r -> FormulaF q f r a
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
PathsPrefixTree q f r -> FormulaF q f r a
Errors (PathsPrefixTree q f r -> FormulaF q f r a)
-> PathsPrefixTree q f r -> FormulaF q f r a
forall a b. (a -> b) -> a -> b
$ AnItem q f r -> PathsPrefixTree q f r
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k).
AnItem q f r -> PathsPrefixTree q f r
P.singleton AnItem q f r
e

errors :: P.PathsPrefixTree q f r -> FormulaF q f r ()
errors :: PathsPrefixTree q f r -> FormulaF q f r ()
errors PathsPrefixTree q f r
t
  | PathsPrefixTree q f r -> Bool
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k).
PathsPrefixTree q f r -> Bool
P.null PathsPrefixTree q f r
t = () -> FormulaF q f r ()
forall k a (q :: k -> k -> *) (f :: k -> *) (r :: k).
a -> FormulaF q f r a
Result ()
  | Bool
otherwise = PathsPrefixTree q f r -> FormulaF q f r ()
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
PathsPrefixTree q f r -> FormulaF q f r a
Errors PathsPrefixTree q f r
t

variable :: VarRef -> FormulaF q f r ()
variable :: VarRef -> FormulaF q f r ()
variable VarRef
v = VarRef -> () -> FormulaF q f r ()
forall k a (q :: k -> k -> *) (f :: k -> *) (r :: k).
VarRef -> a -> FormulaF q f r a
Variable VarRef
v ()

instance Functor (FormulaF q f r) where
  fmap :: (a -> b) -> FormulaF q f r a -> FormulaF q f r b
fmap a -> b
f (Result a
x) = b -> FormulaF q f r b
forall k a (q :: k -> k -> *) (f :: k -> *) (r :: k).
a -> FormulaF q f r a
Result (a -> b
f a
x)
  fmap a -> b
_ (Errors PathsPrefixTree q f r
e) = PathsPrefixTree q f r -> FormulaF q f r b
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
PathsPrefixTree q f r -> FormulaF q f r a
Errors PathsPrefixTree q f r
e
  fmap a -> b
f (Apply FormulaF q f r (b -> c)
g FormulaF q f r b
x c -> a
h) = FormulaF q f r (b -> c)
-> FormulaF q f r b -> (c -> b) -> FormulaF q f r b
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) b c a.
FormulaF q f r (b -> c)
-> FormulaF q f r b -> (c -> a) -> FormulaF q f r a
Apply FormulaF q f r (b -> c)
g FormulaF q f r b
x (a -> b
f (a -> b) -> (c -> a) -> c -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> a
h)
  fmap a -> b
f (SelectFirst NonEmpty (SomeFormulaF b)
xs PathsPrefixTree q f r
e b -> a
h) = NonEmpty (SomeFormulaF b)
-> PathsPrefixTree q f r -> (b -> b) -> FormulaF q f r b
forall k b (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
NonEmpty (SomeFormulaF b)
-> PathsPrefixTree q f r -> (b -> a) -> FormulaF q f r a
SelectFirst NonEmpty (SomeFormulaF b)
xs PathsPrefixTree q f r
e (a -> b
f (a -> b) -> (b -> a) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
h)
  fmap a -> b
f (Variable VarRef
r a
x) = VarRef -> b -> FormulaF q f r b
forall k a (q :: k -> k -> *) (f :: k -> *) (r :: k).
VarRef -> a -> FormulaF q f r a
Variable VarRef
r (a -> b
f a
x)

instance Functor SomeFormulaF where
  fmap :: (a -> b) -> SomeFormulaF a -> SomeFormulaF b
fmap a -> b
f (SomeFormulaF FormulaF q f r a
x) = FormulaF q f r b -> SomeFormulaF b
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
FormulaF q f r a -> SomeFormulaF a
SomeFormulaF ((a -> b) -> FormulaF q f r a -> FormulaF q f r b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f FormulaF q f r a
x)

instance Applicative (FormulaF q f r) where
  pure :: a -> FormulaF q f r a
pure = a -> FormulaF q f r a
forall k a (q :: k -> k -> *) (f :: k -> *) (r :: k).
a -> FormulaF q f r a
Result
  FormulaF q f r (a -> b)
f <*> :: FormulaF q f r (a -> b) -> FormulaF q f r a -> FormulaF q f r b
<*> FormulaF q f r a
x = FormulaF q f r (a -> b)
-> FormulaF q f r a -> (b -> b) -> FormulaF q f r b
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) b c a.
FormulaF q f r (b -> c)
-> FormulaF q f r b -> (c -> a) -> FormulaF q f r a
mkApply FormulaF q f r (a -> b)
f FormulaF q f r a
x b -> b
forall a. a -> a
id

eitherOf :: [FormulaF q' f' r' a] -> AnItem q f r -> FormulaF q f r a
eitherOf :: [FormulaF q' f' r' a] -> AnItem q f r -> FormulaF q f r a
eitherOf [FormulaF q' f' r' a]
fs AnItem q f r
allE = [SomeFormulaF a]
-> PathsPrefixTree q f r -> (a -> a) -> FormulaF q f r a
forall k b (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
[SomeFormulaF b]
-> PathsPrefixTree q f r -> (b -> a) -> FormulaF q f r a
mkSelectFirst ((FormulaF q' f' r' a -> SomeFormulaF a)
-> [FormulaF q' f' r' a] -> [SomeFormulaF a]
forall a b. (a -> b) -> [a] -> [b]
map FormulaF q' f' r' a -> SomeFormulaF a
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
FormulaF q f r a -> SomeFormulaF a
SomeFormulaF [FormulaF q' f' r' a]
fs) (AnItem q f r -> PathsPrefixTree q f r
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k).
AnItem q f r -> PathsPrefixTree q f r
P.singleton AnItem q f r
allE) a -> a
forall a. a -> a
id

calculate :: FormulaF q f r a -> Either (P.PathsPrefixTree q f r) a
calculate :: FormulaF q f r a -> Either (PathsPrefixTree q f r) a
calculate (Result a
x) = a -> Either (PathsPrefixTree q f r) a
forall a b. b -> Either a b
Right a
x
calculate (Errors PathsPrefixTree q f r
e) = PathsPrefixTree q f r -> Either (PathsPrefixTree q f r) a
forall a b. a -> Either a b
Left PathsPrefixTree q f r
e
calculate (Apply FormulaF q f r (b -> c)
f FormulaF q f r b
x c -> a
h) = case FormulaF q f r (b -> c) -> Either (PathsPrefixTree q f r) (b -> c)
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
FormulaF q f r a -> Either (PathsPrefixTree q f r) a
calculate FormulaF q f r (b -> c)
f of
  Left PathsPrefixTree q f r
e1 -> case FormulaF q f r b -> Either (PathsPrefixTree q f r) b
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
FormulaF q f r a -> Either (PathsPrefixTree q f r) a
calculate FormulaF q f r b
x of
    Left PathsPrefixTree q f r
e2 -> PathsPrefixTree q f r -> Either (PathsPrefixTree q f r) a
forall a b. a -> Either a b
Left (PathsPrefixTree q f r
e1 PathsPrefixTree q f r
-> PathsPrefixTree q f r -> PathsPrefixTree q f r
forall a. Semigroup a => a -> a -> a
<> PathsPrefixTree q f r
e2)
    Right b
_ -> PathsPrefixTree q f r -> Either (PathsPrefixTree q f r) a
forall a b. a -> Either a b
Left PathsPrefixTree q f r
e1
  Right b -> c
f' -> case FormulaF q f r b -> Either (PathsPrefixTree q f r) b
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
FormulaF q f r a -> Either (PathsPrefixTree q f r) a
calculate FormulaF q f r b
x of
    Left PathsPrefixTree q f r
e2 -> PathsPrefixTree q f r -> Either (PathsPrefixTree q f r) a
forall a b. a -> Either a b
Left PathsPrefixTree q f r
e2
    Right b
x' -> a -> Either (PathsPrefixTree q f r) a
forall a b. b -> Either a b
Right (c -> a
h (b -> c
f' b
x'))
calculate (SelectFirst NonEmpty (SomeFormulaF b)
xs PathsPrefixTree q f r
e b -> a
h) = [SomeFormulaF b] -> Either (PathsPrefixTree q f r) a
go (NonEmpty (SomeFormulaF b) -> [SomeFormulaF b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (SomeFormulaF b)
xs)
  where
    go :: [SomeFormulaF b] -> Either (PathsPrefixTree q f r) a
go (SomeFormulaF FormulaF q f r b
r : [SomeFormulaF b]
rs) = case FormulaF q f r b -> Either (PathsPrefixTree q f r) b
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
FormulaF q f r a -> Either (PathsPrefixTree q f r) a
calculate FormulaF q f r b
r of
      Left PathsPrefixTree q f r
_ -> [SomeFormulaF b] -> Either (PathsPrefixTree q f r) a
go [SomeFormulaF b]
rs
      Right b
x -> a -> Either (PathsPrefixTree q f r) a
forall a b. b -> Either a b
Right (b -> a
h b
x)
    go [] = PathsPrefixTree q f r -> Either (PathsPrefixTree q f r) a
forall a b. a -> Either a b
Left PathsPrefixTree q f r
e
calculate (Variable VarRef
i a
_) = [Char] -> Either (PathsPrefixTree q f r) a
forall a. HasCallStack => [Char] -> a
error ([Char] -> Either (PathsPrefixTree q f r) a)
-> [Char] -> Either (PathsPrefixTree q f r) a
forall a b. (a -> b) -> a -> b
$ [Char]
"Unknown variable " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> VarRef -> [Char]
forall a. Show a => a -> [Char]
show VarRef
i

-- Approximate for now. Answers yes/no correctly, but the error lists aren't
-- super accurate. TODO: improve
maxFixpoint :: VarRef -> FormulaF q f r () -> FormulaF q f r ()
maxFixpoint :: VarRef -> FormulaF q f r () -> FormulaF q f r ()
maxFixpoint VarRef
i = FormulaF q f r () -> FormulaF q f r ()
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
FormulaF q f r a -> FormulaF q f r a
go
  where
    go :: FormulaF q f r a -> FormulaF q f r a
    go :: FormulaF q f r a -> FormulaF q f r a
go (Result a
x) = a -> FormulaF q f r a
forall k a (q :: k -> k -> *) (f :: k -> *) (r :: k).
a -> FormulaF q f r a
Result a
x
    go (Errors PathsPrefixTree q f r
e) = PathsPrefixTree q f r -> FormulaF q f r a
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
PathsPrefixTree q f r -> FormulaF q f r a
Errors PathsPrefixTree q f r
e
    go (Apply FormulaF q f r (b -> c)
f FormulaF q f r b
x c -> a
h) = FormulaF q f r (b -> c)
-> FormulaF q f r b -> (c -> a) -> FormulaF q f r a
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) b c a.
FormulaF q f r (b -> c)
-> FormulaF q f r b -> (c -> a) -> FormulaF q f r a
mkApply (FormulaF q f r (b -> c) -> FormulaF q f r (b -> c)
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
FormulaF q f r a -> FormulaF q f r a
go FormulaF q f r (b -> c)
f) (FormulaF q f r b -> FormulaF q f r b
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
FormulaF q f r a -> FormulaF q f r a
go FormulaF q f r b
x) c -> a
h
    go (SelectFirst NonEmpty (SomeFormulaF b)
fs PathsPrefixTree q f r
e b -> a
h) = [SomeFormulaF b]
-> PathsPrefixTree q f r -> (b -> a) -> FormulaF q f r a
forall k b (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
[SomeFormulaF b]
-> PathsPrefixTree q f r -> (b -> a) -> FormulaF q f r a
mkSelectFirst (NonEmpty (SomeFormulaF b) -> [SomeFormulaF b]
forall a. NonEmpty a -> [a]
NE.toList ((SomeFormulaF b -> SomeFormulaF b)
-> NonEmpty (SomeFormulaF b) -> NonEmpty (SomeFormulaF b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SomeFormulaF b -> SomeFormulaF b
forall a. SomeFormulaF a -> SomeFormulaF a
goSF NonEmpty (SomeFormulaF b)
fs)) PathsPrefixTree q f r
e b -> a
h
    go (Variable VarRef
j a
x) | VarRef
i VarRef -> VarRef -> Bool
forall a. Eq a => a -> a -> Bool
== VarRef
j = a -> FormulaF q f r a
forall k a (q :: k -> k -> *) (f :: k -> *) (r :: k).
a -> FormulaF q f r a
Result a
x
    go v :: FormulaF q f r a
v@(Variable VarRef
_ a
_) = FormulaF q f r a
v
    goSF :: SomeFormulaF a -> SomeFormulaF a
    goSF :: SomeFormulaF a -> SomeFormulaF a
goSF (SomeFormulaF FormulaF q f r a
x) = FormulaF q f r a -> SomeFormulaF a
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
FormulaF q f r a -> SomeFormulaF a
SomeFormulaF (FormulaF q f r a -> FormulaF q f r a
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
FormulaF q f r a -> FormulaF q f r a
go FormulaF q f r a
x)

mapErrors :: (P.PathsPrefixTree q f r -> P.PathsPrefixTree q' f' r') -> FormulaF q f r a -> FormulaF q' f' r' a
mapErrors :: (PathsPrefixTree q f r -> PathsPrefixTree q' f' r')
-> FormulaF q f r a -> FormulaF q' f' r' a
mapErrors PathsPrefixTree q f r -> PathsPrefixTree q' f' r'
_ (Result a
x) = a -> FormulaF q' f' r' a
forall k a (q :: k -> k -> *) (f :: k -> *) (r :: k).
a -> FormulaF q f r a
Result a
x
mapErrors PathsPrefixTree q f r -> PathsPrefixTree q' f' r'
m (Errors PathsPrefixTree q f r
e) = PathsPrefixTree q' f' r' -> FormulaF q' f' r' a
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
PathsPrefixTree q f r -> FormulaF q f r a
Errors (PathsPrefixTree q' f' r' -> FormulaF q' f' r' a)
-> PathsPrefixTree q' f' r' -> FormulaF q' f' r' a
forall a b. (a -> b) -> a -> b
$ PathsPrefixTree q f r -> PathsPrefixTree q' f' r'
m PathsPrefixTree q f r
e
mapErrors PathsPrefixTree q f r -> PathsPrefixTree q' f' r'
m (Apply FormulaF q f r (b -> c)
f FormulaF q f r b
x c -> a
h) = FormulaF q' f' r' (b -> c)
-> FormulaF q' f' r' b -> (c -> a) -> FormulaF q' f' r' a
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) b c a.
FormulaF q f r (b -> c)
-> FormulaF q f r b -> (c -> a) -> FormulaF q f r a
mkApply ((PathsPrefixTree q f r -> PathsPrefixTree q' f' r')
-> FormulaF q f r (b -> c) -> FormulaF q' f' r' (b -> c)
forall k k (q :: k -> k -> *) (f :: k -> *) (r :: k)
       (q' :: k -> k -> *) (f' :: k -> *) (r' :: k) a.
(PathsPrefixTree q f r -> PathsPrefixTree q' f' r')
-> FormulaF q f r a -> FormulaF q' f' r' a
mapErrors PathsPrefixTree q f r -> PathsPrefixTree q' f' r'
m FormulaF q f r (b -> c)
f) ((PathsPrefixTree q f r -> PathsPrefixTree q' f' r')
-> FormulaF q f r b -> FormulaF q' f' r' b
forall k k (q :: k -> k -> *) (f :: k -> *) (r :: k)
       (q' :: k -> k -> *) (f' :: k -> *) (r' :: k) a.
(PathsPrefixTree q f r -> PathsPrefixTree q' f' r')
-> FormulaF q f r a -> FormulaF q' f' r' a
mapErrors PathsPrefixTree q f r -> PathsPrefixTree q' f' r'
m FormulaF q f r b
x) c -> a
h
mapErrors PathsPrefixTree q f r -> PathsPrefixTree q' f' r'
m (SelectFirst NonEmpty (SomeFormulaF b)
fs PathsPrefixTree q f r
e b -> a
h) = [SomeFormulaF b]
-> PathsPrefixTree q' f' r' -> (b -> a) -> FormulaF q' f' r' a
forall k b (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
[SomeFormulaF b]
-> PathsPrefixTree q f r -> (b -> a) -> FormulaF q f r a
mkSelectFirst (NonEmpty (SomeFormulaF b) -> [SomeFormulaF b]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (SomeFormulaF b)
fs) (PathsPrefixTree q f r -> PathsPrefixTree q' f' r'
m PathsPrefixTree q f r
e) b -> a
h
mapErrors PathsPrefixTree q f r -> PathsPrefixTree q' f' r'
_ (Variable VarRef
i a
x) = VarRef -> a -> FormulaF q' f' r' a
forall k a (q :: k -> k -> *) (f :: k -> *) (r :: k).
VarRef -> a -> FormulaF q f r a
Variable VarRef
i a
x