{-# LANGUAGE GADTs #-}

module Test.Cardano.Ledger.Constrained.Shrink (
  shrinkEnv,
) where

import Control.Monad
import Data.Maybe
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Monad
import Test.Cardano.Ledger.Constrained.Rewrite
import Test.Cardano.Ledger.Constrained.TypeRep

justOneName :: [([Name era], [Pred era])] -> [(Name era, [Pred era])]
justOneName :: forall era. [([Name era], [Pred era])] -> [(Name era, [Pred era])]
justOneName [([Name era], [Pred era])]
xs = (([Name era], [Pred era])
 -> [(Name era, [Pred era])] -> [(Name era, [Pred era])])
-> [(Name era, [Pred era])]
-> [([Name era], [Pred era])]
-> [(Name era, [Pred era])]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([Name era], [Pred era])
-> [(Name era, [Pred era])] -> [(Name era, [Pred era])]
forall {a} {b}. ([a], b) -> [(a, b)] -> [(a, b)]
accum [] [([Name era], [Pred era])]
xs -- FIXME throw away new style DependGraph elements
  where
    accum :: ([a], b) -> [(a, b)] -> [(a, b)]
accum ([a
x], b
cs) [(a, b)]
ans = (a
x, b
cs) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)]
ans
    accum ([a], b)
_ [(a, b)]
ans = [(a, b)]
ans

-- | Shrink an environment subject to the constraints in the given dependency graph.
--   The strategy is
--    * pick a variable
--    * shrink its value to something that still satisfies the defining constraints for the variable
--    * adjust the values for variables depending on the picked variables to fix constraint
--      violations resulting from the changed value
--   Note that the DependGraph tells us the dependency order of the variables: a variable only
--   depends on the variables before it in the graph, so when shrinking the value of a variable we
--   only need to adjust the values of later variables.
shrinkEnv :: DependGraph era -> Env era -> [Env era]
shrinkEnv :: forall era. DependGraph era -> Env era -> [Env era]
shrinkEnv (DependGraph [([Name era], [Pred era])]
vs) Env era
env =
  [ Env era
env'
  | ([(Name era, [Pred era])]
before, (Name era
x, [Pred era]
cs), [(Name era, [Pred era])]
after) <- [(Name era, [Pred era])]
-> [([(Name era, [Pred era])], (Name era, [Pred era]),
     [(Name era, [Pred era])])]
forall a. [a] -> [([a], a, [a])]
splits ([([Name era], [Pred era])] -> [(Name era, [Pred era])]
forall era. [([Name era], [Pred era])] -> [(Name era, [Pred era])]
justOneName [([Name era], [Pred era])]
vs)
  , Env era
env' <- Env era
-> [Name era]
-> Name era
-> [Pred era]
-> [(Name era, [Pred era])]
-> [Env era]
forall era.
Env era
-> [Name era]
-> Name era
-> [Pred era]
-> [(Name era, [Pred era])]
-> [Env era]
shrinkOneVar Env era
env (((Name era, [Pred era]) -> Name era)
-> [(Name era, [Pred era])] -> [Name era]
forall a b. (a -> b) -> [a] -> [b]
map (Name era, [Pred era]) -> Name era
forall a b. (a, b) -> a
fst [(Name era, [Pred era])]
before) Name era
x [Pred era]
cs [(Name era, [Pred era])]
after
  ]
  where
    splits :: [a] -> [([a], a, [a])]
    splits :: forall a. [a] -> [([a], a, [a])]
splits [] = []
    splits (a
x : [a]
xs) = ([], a
x, [a]
xs) ([a], a, [a]) -> [([a], a, [a])] -> [([a], a, [a])]
forall a. a -> [a] -> [a]
: [(a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ys, a
y, [a]
zs) | ([a]
ys, a
y, [a]
zs) <- [a] -> [([a], a, [a])]
forall a. [a] -> [([a], a, [a])]
splits [a]
xs]

shrinkOneVar ::
  Env era -> [Name era] -> Name era -> [Pred era] -> [(Name era, [Pred era])] -> [Env era]
shrinkOneVar :: forall era.
Env era
-> [Name era]
-> Name era
-> [Pred era]
-> [(Name era, [Pred era])]
-> [Env era]
shrinkOneVar Env era
originalEnv [Name era]
before Name era
x [Pred era]
cs [(Name era, [Pred era])]
after =
  [ Env era
env'
  | Payload era
val' <- Name era -> [Pred era] -> Payload era -> [Payload era]
forall era. Name era -> [Pred era] -> Payload era -> [Payload era]
shrinkVar Name era
x [Pred era]
cs' Payload era
val
  , let fixup :: Env era -> (Name era, [Pred era]) -> Maybe (Env era)
fixup Env era
env (Name era
y, [Pred era]
ycs) = do
          Payload era
p <- Name era -> Env era -> Maybe (Payload era)
forall era. Name era -> Env era -> Maybe (Payload era)
findName Name era
y Env era
originalEnv
          Payload era
p' <- Name era -> [Pred era] -> Payload era -> Maybe (Payload era)
forall era.
Name era -> [Pred era] -> Payload era -> Maybe (Payload era)
fixupVar Name era
y ((Pred era -> Pred era) -> [Pred era] -> [Pred era]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era -> Pred era -> Pred era
forall era. Subst era -> Pred era -> Pred era
substPred (Subst era -> Pred era -> Pred era)
-> Subst era -> Pred era -> Pred era
forall a b. (a -> b) -> a -> b
$ Env era -> Subst era
forall era. Env era -> Subst era
envToSubst Env era
env) [Pred era]
ycs) Payload era
p
          Env era -> Maybe (Env era)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env era -> Maybe (Env era)) -> Env era -> Maybe (Env era)
forall a b. (a -> b) -> a -> b
$ Name era -> Payload era -> Env era -> Env era
forall era. Name era -> Payload era -> Env era -> Env era
storeName Name era
y Payload era
p' Env era
env
  , Env era
env' <- Maybe (Env era) -> [Env era]
forall a. Maybe a -> [a]
maybeToList (Maybe (Env era) -> [Env era]) -> Maybe (Env era) -> [Env era]
forall a b. (a -> b) -> a -> b
$ (Env era -> (Name era, [Pred era]) -> Maybe (Env era))
-> Env era -> [(Name era, [Pred era])] -> Maybe (Env era)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Env era -> (Name era, [Pred era]) -> Maybe (Env era)
fixup (Name era -> Payload era -> Env era -> Env era
forall era. Name era -> Payload era -> Env era -> Env era
storeName Name era
x Payload era
val' Env era
beforeEnv) [(Name era, [Pred era])]
after
  ]
  where
    beforeEnv :: Env era
beforeEnv = [Name era] -> Env era -> Env era
forall era. [Name era] -> Env era -> Env era
restrictEnv [Name era]
before Env era
originalEnv
    beforeSubst :: Subst era
beforeSubst = Env era -> Subst era
forall era. Env era -> Subst era
envToSubst Env era
beforeEnv
    cs' :: [Pred era]
cs' = (Pred era -> Pred era) -> [Pred era] -> [Pred era]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era -> Pred era -> Pred era
forall era. Subst era -> Pred era -> Pred era
substPred Subst era
beforeSubst) [Pred era]
cs
    val :: Payload era
val = case Name era -> Env era -> Maybe (Payload era)
forall era. Name era -> Env era -> Maybe (Payload era)
findName Name era
x Env era
originalEnv of
      Just Payload era
v -> Payload era
v
      Maybe (Payload era)
Nothing -> [Char] -> Payload era
forall a. HasCallStack => [Char] -> a
error ([Char] -> Payload era) -> [Char] -> Payload era
forall a b. (a -> b) -> a -> b
$ [Char]
"shrinkOneVar: Failed to find: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name era -> [Char]
forall a. Show a => a -> [Char]
show Name era
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" in env"

shrinkVar :: Name era -> [Pred era] -> Payload era -> [Payload era]
shrinkVar :: forall era. Name era -> [Pred era] -> Payload era -> [Payload era]
shrinkVar Name era
v [Pred era]
cs Payload era
p = [Payload era
p' | Payload era
p' <- Payload era -> [Payload era]
forall era. Payload era -> [Payload era]
shrinkPayload Payload era
p, Name era -> Payload era -> [Pred era] -> Bool
forall era. Name era -> Payload era -> [Pred era] -> Bool
validAssignment Name era
v Payload era
p' [Pred era]
cs]

shrinkPayload :: Payload era -> [Payload era]
shrinkPayload :: forall era. Payload era -> [Payload era]
shrinkPayload (Payload Rep era t
rep t
t Access era s t
acc) = [Rep era t -> t -> Access era s t -> Payload era
forall era t s. Rep era t -> t -> Access era s t -> Payload era
Payload Rep era t
rep t
t' Access era s t
acc | t
t' <- Rep era t -> t -> [t]
forall era t. Rep era t -> t -> [t]
shrinkRep Rep era t
rep t
t]

-- | Compute something satisfying the constraints that's as "close" to the original value as
--   possible. TODO: more cleverness
fixupVar :: Name era -> [Pred era] -> Payload era -> Maybe (Payload era)
fixupVar :: forall era.
Name era -> [Pred era] -> Payload era -> Maybe (Payload era)
fixupVar Name era
v [Pred era]
cs Payload era
p = [Payload era] -> Maybe (Payload era)
forall a. [a] -> Maybe a
listToMaybe [Payload era
p' | Payload era
p' <- [Payload era
p | Name era -> Payload era -> [Pred era] -> Bool
forall era. Name era -> Payload era -> [Pred era] -> Bool
validAssignment Name era
v Payload era
p [Pred era]
cs] [Payload era] -> [Payload era] -> [Payload era]
forall a. [a] -> [a] -> [a]
++ [Payload era] -> [Payload era]
forall a. [a] -> [a]
reverse (Name era -> [Pred era] -> Payload era -> [Payload era]
forall era. Name era -> [Pred era] -> Payload era -> [Payload era]
shrinkVar Name era
v [Pred era]
cs Payload era
p)]

-- | Assumes the variable is the only free variable in the constraints.
validAssignment :: Name era -> Payload era -> [Pred era] -> Bool
validAssignment :: forall era. Name era -> Payload era -> [Pred era] -> Bool
validAssignment Name era
v Payload era
p [Pred era]
cs = (Pred era -> Bool) -> [Pred era] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Env era -> Pred era -> Bool
forall era. Env era -> Pred era -> Bool
runPred_ (Env era -> Pred era -> Bool) -> Env era -> Pred era -> Bool
forall a b. (a -> b) -> a -> b
$ Name era -> Payload era -> Env era -> Env era
forall era. Name era -> Payload era -> Env era -> Env era
storeName Name era
v Payload era
p Env era
forall era. Env era
emptyEnv) [Pred era]
cs

runPred_ :: Env era -> Pred era -> Bool
runPred_ :: forall era. Env era -> Pred era -> Bool
runPred_ Env era
env Pred era
p = ([[Char]] -> Bool)
-> (Bool -> Bool) -> Either [[Char]] Bool -> Bool
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Bool -> [[Char]] -> Bool
forall a b. a -> b -> a
const Bool
False) Bool -> Bool
forall a. a -> a
id (Either [[Char]] Bool -> Bool) -> Either [[Char]] Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Typed Bool -> Either [[Char]] Bool
forall x. Typed x -> Either [[Char]] x
runTyped (Typed Bool -> Either [[Char]] Bool)
-> Typed Bool -> Either [[Char]] Bool
forall a b. (a -> b) -> a -> b
$ Env era -> Pred era -> Typed Bool
forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env Pred era
p