{-# 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr 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) 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) <- forall a. [a] -> [([a], a, [a])]
splits (forall era. [([Name era], [Pred era])] -> [(Name era, [Pred era])]
justOneName [([Name era], [Pred era])]
vs)
  , Env era
env' <- forall era.
Env era
-> [Name era]
-> Name era
-> [Pred era]
-> [(Name era, [Pred era])]
-> [Env era]
shrinkOneVar Env era
env (forall a b. (a -> b) -> [a] -> [b]
map 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) forall a. a -> [a] -> [a]
: [(a
x forall a. a -> [a] -> [a]
: [a]
ys, a
y, [a]
zs) | ([a]
ys, a
y, [a]
zs) <- 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' <- 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 <- forall era. Name era -> Env era -> Maybe (Payload era)
findName Name era
y Env era
originalEnv
          Payload era
p' <- forall era.
Name era -> [Pred era] -> Payload era -> Maybe (Payload era)
fixupVar Name era
y (forall a b. (a -> b) -> [a] -> [b]
map (forall era. Subst era -> Pred era -> Pred era
substPred forall a b. (a -> b) -> a -> b
$ forall era. Env era -> Subst era
envToSubst Env era
env) [Pred era]
ycs) Payload era
p
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era. Name era -> Payload era -> Env era -> Env era
storeName Name era
y Payload era
p' Env era
env
  , Env era
env' <- forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ 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 (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 = forall era. [Name era] -> Env era -> Env era
restrictEnv [Name era]
before Env era
originalEnv
    beforeSubst :: Subst era
beforeSubst = forall era. Env era -> Subst era
envToSubst Env era
beforeEnv
    cs' :: [Pred era]
cs' = forall a b. (a -> b) -> [a] -> [b]
map (forall era. Subst era -> Pred era -> Pred era
substPred Subst era
beforeSubst) [Pred era]
cs
    val :: Payload era
val = case 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 -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"shrinkOneVar: Failed to find: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Name era
x 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' <- forall era. Payload era -> [Payload era]
shrinkPayload Payload era
p, 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) = [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' <- 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 = forall a. [a] -> Maybe a
listToMaybe [Payload era
p' | Payload era
p' <- [Payload era
p | forall era. Name era -> Payload era -> [Pred era] -> Bool
validAssignment Name era
v Payload era
p [Pred era]
cs] forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [a]
reverse (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 = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall era. Env era -> Pred era -> Bool
runPred_ forall a b. (a -> b) -> a -> b
$ forall era. Name era -> Payload era -> Env era -> Env era
storeName Name era
v Payload era
p 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 = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const Bool
False) forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall x. Typed x -> Either [[Char]] x
runTyped forall a b. (a -> b) -> a -> b
$ forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env Pred era
p