{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Test.Cardano.Ledger.Constrained.Stage where

import Cardano.Ledger.Core (Era (..))
import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import qualified Data.Map.Strict as Map
import Data.Pulse (foldlM')
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Env (Env, Name, emptyEnv)
import Test.Cardano.Ledger.Constrained.Monad (monadTyped)
import Test.Cardano.Ledger.Constrained.Preds.CertState (certStatePreds, pstatePreds, vstatePreds)
import Test.Cardano.Ledger.Constrained.Preds.LedgerState (ledgerStatePreds)
import Test.Cardano.Ledger.Constrained.Preds.PParams (pParamsPreds)
import Test.Cardano.Ledger.Constrained.Preds.Universes (UnivSize (..), universePreds)
import Test.Cardano.Ledger.Constrained.Rewrite (
  DependGraph (..),
  OrderInfo,
  initialOrder,
  mkDependGraph,
  notBefore,
  rewriteGen,
  standardOrderInfo,
 )
import Test.Cardano.Ledger.Constrained.Solver (solveOneVar)
import Test.Cardano.Ledger.Generic.Proof hiding (lift)
import Test.QuickCheck

-- ====================================

-- | Group together some Preds and OrderInfo about how to decide the
--   order in which to solve the variables appearing in the Preds
data Stage era = Stage OrderInfo [Pred era]

type Pipeline era = [Stage era]

-- | A pipeline for specifying the LederState
ledgerPipeline :: Reflect era => UnivSize -> Proof era -> Pipeline era
ledgerPipeline :: forall era. Reflect era => UnivSize -> Proof era -> Pipeline era
ledgerPipeline UnivSize
sizes Proof era
proof =
  [ forall era. OrderInfo -> [Pred era] -> Stage era
Stage OrderInfo
standardOrderInfo (forall era. Reflect era => Proof era -> [Pred era]
pParamsPreds Proof era
proof)
  , forall era. OrderInfo -> [Pred era] -> Stage era
Stage OrderInfo
standardOrderInfo (forall era. Reflect era => UnivSize -> Proof era -> [Pred era]
universePreds UnivSize
sizes Proof era
proof)
  ]
    forall a. [a] -> [a] -> [a]
++ ( case forall era. Proof era -> PParamsWit era
whichPParams Proof era
proof of
          PParamsWit era
PParamsConwayToConway -> [forall era. OrderInfo -> [Pred era] -> Stage era
Stage OrderInfo
standardOrderInfo (forall era. Era era => Proof era -> [Pred era]
vstatePreds Proof era
proof)]
          PParamsWit era
_ -> []
       )
    forall a. [a] -> [a] -> [a]
++ [ forall era. OrderInfo -> [Pred era] -> Stage era
Stage OrderInfo
standardOrderInfo (forall era. Era era => Proof era -> [Pred era]
pstatePreds Proof era
proof)
       , forall era. OrderInfo -> [Pred era] -> Stage era
Stage OrderInfo
standardOrderInfo (forall era. Era era => Proof era -> [Pred era]
certStatePreds Proof era
proof)
       , forall era. OrderInfo -> [Pred era] -> Stage era
Stage OrderInfo
standardOrderInfo (forall era. Reflect era => UnivSize -> Proof era -> [Pred era]
ledgerStatePreds UnivSize
sizes Proof era
proof)
       ]

-- | Translate a Stage into a DependGraph, given the set
--   of variables that have aready been solved for.
stageToGraph :: Era era => Int -> Stage era -> HashSet (Name era) -> Gen (Int, DependGraph era)
stageToGraph :: forall era.
Era era =>
Int
-> Stage era -> HashSet (Name era) -> Gen (Int, DependGraph era)
stageToGraph Int
n0 (Stage OrderInfo
info [Pred era]
ps) HashSet (Name era)
alreadyDefined = do
  (Int
n1, [Pred era]
simple) <- forall era. Era era => (Int, [Pred era]) -> Gen (Int, [Pred era])
rewriteGen (Int
n0, [Pred era]
ps)
  [Name era]
orderedNames <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Era era => OrderInfo -> [Pred era] -> Typed [Name era]
initialOrder OrderInfo
info [Pred era]
simple
  DependGraph era
graph <-
    forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$
      forall era.
Era era =>
Int
-> [([Name era], [Pred era])]
-> HashSet (Name era)
-> [Name era]
-> [Name era]
-> [Pred era]
-> Typed (DependGraph era)
mkDependGraph
        (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name era]
orderedNames)
        []
        HashSet (Name era)
alreadyDefined
        [Name era]
orderedNames
        []
        (forall a. (a -> Bool) -> [a] -> [a]
Prelude.filter forall era. Pred era -> Bool
notBefore [Pred era]
simple)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
n1, DependGraph era
graph)

-- | Merge a Pipeline into an existing DependGraph, given the set of variables
--   that have aready been solved for, to get a larger DependGraph
mergePipeline ::
  Era era =>
  Int ->
  Pipeline era ->
  HashSet (Name era) ->
  DependGraph era ->
  Gen (Int, DependGraph era)
mergePipeline :: forall era.
Era era =>
Int
-> Pipeline era
-> HashSet (Name era)
-> DependGraph era
-> Gen (Int, DependGraph era)
mergePipeline Int
n [] HashSet (Name era)
_ DependGraph era
graph = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
n, DependGraph era
graph)
mergePipeline Int
n0 (Stage era
pipe : [Stage era]
more) HashSet (Name era)
defined (DependGraph [([Name era], [Pred era])]
xs) = do
  (Int
n1, DependGraph [([Name era], [Pred era])]
ys) <- forall era.
Era era =>
Int
-> Stage era -> HashSet (Name era) -> Gen (Int, DependGraph era)
stageToGraph Int
n0 Stage era
pipe HashSet (Name era)
defined
  let names :: [Name era]
names = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [([Name era], [Pred era])]
ys)
  forall era.
Era era =>
Int
-> Pipeline era
-> HashSet (Name era)
-> DependGraph era
-> Gen (Int, DependGraph era)
mergePipeline Int
n1 [Stage era]
more (forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.union (forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.fromList [Name era]
names) HashSet (Name era)
defined) (forall era. [([Name era], [Pred era])] -> DependGraph era
DependGraph ([([Name era], [Pred era])]
xs forall a. [a] -> [a] -> [a]
++ [([Name era], [Pred era])]
ys))

-- | Solve a Pipeline to get a Env, Subst, and a DependGraph
solvePipeline :: Reflect era => Pipeline era -> Gen (Env era, Subst era, DependGraph era)
solvePipeline :: forall era.
Reflect era =>
Pipeline era -> Gen (Env era, Subst era, DependGraph era)
solvePipeline Pipeline era
pipes = do
  (Int
_, gr :: DependGraph era
gr@(DependGraph [([Name era], [Pred era])]
pairs)) <- forall era.
Era era =>
Int
-> Pipeline era
-> HashSet (Name era)
-> DependGraph era
-> Gen (Int, DependGraph era)
mergePipeline Int
0 Pipeline era
pipes forall a. HashSet a
HashSet.empty (forall era. [([Name era], [Pred era])] -> DependGraph era
DependGraph [])
  Subst Map String (SubstElem era)
subst <- forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' forall era.
Era era =>
Subst era -> ([Name era], [Pred era]) -> Gen (Subst era)
solveOneVar forall era. Subst era
emptySubst [([Name era], [Pred era])]
pairs
  let isTempV :: t Char -> Bool
isTempV t Char
k = Bool -> Bool
not (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
'.' t Char
k)
  let sub :: Subst era
sub = forall era. Map String (SubstElem era) -> Subst era
Subst (forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\String
k SubstElem era
_ -> forall {t :: * -> *}. Foldable t => t Char -> Bool
isTempV String
k) Map String (SubstElem era)
subst)
  Env era
env <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
sub forall era. Env era
emptyEnv)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env era
env, Subst era
sub, DependGraph era
gr)