{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Test.Cardano.Ledger.Constrained.Rewrite (
  rewrite,
  rewriteGen,
  rewritePred,
  compile,
  compileGenWithSubst,
  removeSameVar,
  removeEqual,
  DependGraph (..),
  accumdep,
  OrderInfo (..),
  standardOrderInfo,
  initialOrder,
  showGraph,
  listEq,
  mkDependGraph,
  notBefore,
  cpeq,
  cteq,
  mkNewVar,
  addP,
  addPred,
  partitionE,
  rename,
) where

import Cardano.Ledger.Core (Era)
import qualified Data.Array as A
import Data.Foldable (toList)
import Data.Graph (Graph, SCC (AcyclicSCC, CyclicSCC), Vertex, graphFromEdges, stronglyConnComp)
import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import qualified Data.List as List
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Combinators (setSized)
import Test.Cardano.Ledger.Constrained.Env (
  Access (..),
  AnyF (..),
  Env (..),
  Field (..),
  Name (..),
  V (..),
  sameName,
 )
import Test.Cardano.Ledger.Constrained.Monad (HasConstraint (With), Typed (..), failT, monadTyped)
import Test.Cardano.Ledger.Constrained.Size (Size (SzExact), genFromSize)
import Test.Cardano.Ledger.Constrained.TypeRep
import Test.QuickCheck
import Type.Reflection (typeRep)

-- ============================================================
-- Conservative (approximate) Equality

-- | Test if two terms (of possibly different types) are equal
typedEq :: Era era => Term era a -> Term era b -> Bool
typedEq :: forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era a
x Term era b
y = case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql (forall era t. Era era => Term era t -> Rep era t
termRep Term era a
x) (forall era t. Era era => Term era t -> Rep era t
termRep Term era b
y) of
  Just a :~: b
Refl -> forall era t. Era era => Term era t -> Term era t -> Bool
cteq Term era a
x Term era b
y
  Maybe (a :~: b)
Nothing -> Bool
False

cEq :: (Eq c, Era era) => Term era c -> Term era a -> c -> a -> Bool
cEq :: forall c era a.
(Eq c, Era era) =>
Term era c -> Term era a -> c -> a -> Bool
cEq Term era c
t1 Term era a
t2 c
c1 a
c2 = case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql (forall era t. Era era => Term era t -> Rep era t
termRep Term era c
t1) (forall era t. Era era => Term era t -> Rep era t
termRep Term era a
t2) of
  Just c :~: a
Refl -> c
c1 forall a. Eq a => a -> a -> Bool
== a
c2
  Maybe (c :~: a)
Nothing -> Bool
False

listEq :: (a -> b -> Bool) -> [a] -> [b] -> Bool
listEq :: forall a b. (a -> b -> Bool) -> [a] -> [b] -> Bool
listEq a -> b -> Bool
_ [] [] = Bool
True
listEq a -> b -> Bool
eqf (a
x : [a]
xs) (b
y : [b]
ys) = a -> b -> Bool
eqf a
x b
y Bool -> Bool -> Bool
&& forall a b. (a -> b -> Bool) -> [a] -> [b] -> Bool
listEq a -> b -> Bool
eqf [a]
xs [b]
ys
listEq a -> b -> Bool
_ [a]
_ [b]
_ = Bool
False

-- | Conservative Sum equality
csumeq :: Era era => Sum era t -> Sum era t -> Bool
csumeq :: forall era t. Era era => Sum era t -> Sum era t -> Bool
csumeq (One Term era t
x) (One Term era t
y) = forall era t. Era era => Term era t -> Term era t -> Bool
cteq Term era t
x Term era t
y
csumeq (SumMap Term era (Map a t)
x) (SumMap Term era (Map a t)
y) =
  case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql (forall era t. Era era => Term era t -> Rep era t
termRep Term era (Map a t)
x) (forall era t. Era era => Term era t -> Rep era t
termRep Term era (Map a t)
y) of
    Just Map a t :~: Map a t
Refl -> forall era t. Era era => Term era t -> Term era t -> Bool
cteq Term era (Map a t)
x Term era (Map a t)
y
    Maybe (Map a t :~: Map a t)
Nothing -> Bool
False
csumeq (SumList Term era [t]
x) (SumList Term era [t]
y) = forall era t. Era era => Term era t -> Term era t -> Bool
cteq Term era [t]
x Term era [t]
y
csumeq Sum era t
_ Sum era t
_ = Bool
False

-- | Conservative (and unsound for Constr and Invert) Target equality
_ctareq :: Era era => RootTarget era r t -> RootTarget era r t -> Bool
_ctareq :: forall era r t.
Era era =>
RootTarget era r t -> RootTarget era r t -> Bool
_ctareq (Constr String
x a -> b
_) (Constr String
y a -> b
_) = String
x forall a. Eq a => a -> a -> Bool
== String
y
_ctareq (Invert String
x TypeRep r
_ a -> b
_) (Invert String
y TypeRep r
_ a -> b
_) = String
x forall a. Eq a => a -> a -> Bool
== String
y
_ctareq (Simple Term era t
x) (Simple Term era t
y) = forall era t. Era era => Term era t -> Term era t -> Bool
cteq Term era t
x Term era t
y
_ctareq (RootTarget era r (a -> t)
x :$ (Simple Term era a
xs)) (RootTarget era r (a -> t)
y :$ (Simple Term era a
ys)) =
  case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql (forall era t. Era era => Term era t -> Rep era t
termRep Term era a
xs) (forall era t. Era era => Term era t -> Rep era t
termRep Term era a
ys) of
    Just a :~: a
Refl -> forall era r t.
Era era =>
RootTarget era r t -> RootTarget era r t -> Bool
_ctareq RootTarget era r (a -> t)
x RootTarget era r (a -> t)
y Bool -> Bool -> Bool
&& forall era t. Era era => Term era t -> Term era t -> Bool
cteq Term era a
xs Term era a
ys
    Maybe (a :~: a)
Nothing -> Bool
False
_ctareq RootTarget era r t
_ RootTarget era r t
_ = Bool
False

-- | Conservative Term equality
cteq :: Era era => Term era t -> Term era t -> Bool
cteq :: forall era t. Era era => Term era t -> Term era t -> Bool
cteq (Lit Rep era t
t1 t
x) (Lit Rep era t
t2 t
y) = case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql Rep era t
t1 Rep era t
t2 of
  Just t :~: t
Refl ->
    case forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Eq (s t))
hasEq Rep era t
t1 Rep era t
t1 of
      Typed (Right (With s t1
_)) -> t
x forall a. Eq a => a -> a -> Bool
== t
y
      Typed (HasConstraint Eq (Rep era t))
_ -> Bool
False
  Maybe (t :~: t)
Nothing -> Bool
False
cteq (Var V era t
x) (Var V era t
y) = forall era t. V era t -> Name era
Name V era t
x forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
y
cteq (Dom Term era (Map a b)
x) (Dom Term era (Map a b)
y) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era (Map a b)
x Term era (Map a b)
y
cteq (Rng Term era (Map a b)
x) (Rng Term era (Map a b)
y) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era (Map a b)
x Term era (Map a b)
y
cteq (Elems Term era (Map a b)
x) (Elems Term era (Map a b)
y) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era (Map a b)
x Term era (Map a b)
y
cteq (Delta Term era Coin
x) (Delta Term era Coin
y) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era Coin
x Term era Coin
y
cteq (Negate Term era DeltaCoin
x) (Negate Term era DeltaCoin
y) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era DeltaCoin
x Term era DeltaCoin
y
cteq (HashD Term era (Data era)
x) (HashD Term era (Data era)
y) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era (Data era)
x Term era (Data era)
y
cteq (HashS Term era (ScriptF era)
x) (HashS Term era (ScriptF era)
y) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era (ScriptF era)
x Term era (ScriptF era)
y
cteq (Pair Term era a
x Term era b
a) (Pair Term era a
y Term era b
b) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era a
x Term era a
y Bool -> Bool -> Bool
&& forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era b
a Term era b
b
cteq Term era t
_ Term era t
_ = Bool
False

-- | Conservative Pred equality
cpeq :: Era era => Pred era -> Pred era -> Bool
cpeq :: forall era. Era era => Pred era -> Pred era -> Bool
cpeq (Sized Term era Size
x Term era t
a) (Sized Term era Size
y Term era t
b) = forall era t. Era era => Term era t -> Term era t -> Bool
cteq Term era Size
x Term era Size
y Bool -> Bool -> Bool
&& forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era t
a Term era t
b
cpeq (Term era a
x :=: Term era a
a) (Term era a
y :=: Term era a
b) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era a
x Term era a
y Bool -> Bool -> Bool
&& forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era a
a Term era a
b
cpeq (Term era (Set a)
x :⊆: Term era (Set a)
a) (Term era (Set a)
y :⊆: Term era (Set a)
b) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era (Set a)
x Term era (Set a)
y Bool -> Bool -> Bool
&& forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era (Set a)
a Term era (Set a)
b
cpeq (Disjoint Term era (Set a)
x Term era (Set a)
a) (Disjoint Term era (Set a)
y Term era (Set a)
b) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era (Set a)
x Term era (Set a)
y Bool -> Bool -> Bool
&& forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era (Set a)
a Term era (Set a)
b
cpeq (Random Term era t
x) (Random Term era t
y) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era t
x Term era t
y
cpeq (CanFollow Term era n
x Term era n
a) (CanFollow Term era n
y Term era n
b) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era n
x Term era n
y Bool -> Bool -> Bool
&& forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era n
a Term era n
b
cpeq (SumsTo (Right c
i) Term era c
x OrdCond
c [Sum era c]
xs) (SumsTo (Right c
j) Term era c
y OrdCond
d [Sum era c]
ys) = forall c era a.
(Eq c, Era era) =>
Term era c -> Term era a -> c -> a -> Bool
cEq Term era c
x Term era c
y c
i c
j Bool -> Bool -> Bool
&& forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era c
x Term era c
y Bool -> Bool -> Bool
&& forall a b. (a -> b -> Bool) -> [a] -> [b] -> Bool
listEq forall era c d. Era era => Sum era c -> Sum era d -> Bool
cseq [Sum era c]
xs [Sum era c]
ys Bool -> Bool -> Bool
&& OrdCond
c forall a. Eq a => a -> a -> Bool
== OrdCond
d
cpeq (SumsTo (Left c
i) Term era c
x OrdCond
c [Sum era c]
xs) (SumsTo (Left c
j) Term era c
y OrdCond
d [Sum era c]
ys) = forall c era a.
(Eq c, Era era) =>
Term era c -> Term era a -> c -> a -> Bool
cEq Term era c
x Term era c
y c
i c
j Bool -> Bool -> Bool
&& forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era c
x Term era c
y Bool -> Bool -> Bool
&& forall a b. (a -> b -> Bool) -> [a] -> [b] -> Bool
listEq forall era c d. Era era => Sum era c -> Sum era d -> Bool
cseq [Sum era c]
xs [Sum era c]
ys Bool -> Bool -> Bool
&& OrdCond
c forall a. Eq a => a -> a -> Bool
== OrdCond
d
cpeq (SumSplit c
i Term era c
x OrdCond
c [Sum era c]
xs) (SumSplit c
j Term era c
y OrdCond
d [Sum era c]
ys) = forall c era a.
(Eq c, Era era) =>
Term era c -> Term era a -> c -> a -> Bool
cEq Term era c
x Term era c
y c
i c
j Bool -> Bool -> Bool
&& forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era c
x Term era c
y Bool -> Bool -> Bool
&& forall a b. (a -> b -> Bool) -> [a] -> [b] -> Bool
listEq forall era c d. Era era => Sum era c -> Sum era d -> Bool
cseq [Sum era c]
xs [Sum era c]
ys Bool -> Bool -> Bool
&& OrdCond
c forall a. Eq a => a -> a -> Bool
== OrdCond
d
cpeq (Component (Left Term era t
x) [AnyF era t]
xs) (Component (Left Term era t
y) [AnyF era t]
ys) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era t
x Term era t
y Bool -> Bool -> Bool
&& forall a b. (a -> b -> Bool) -> [a] -> [b] -> Bool
listEq forall era t s. Era era => AnyF era t -> AnyF era s -> Bool
anyWeq [AnyF era t]
xs [AnyF era t]
ys
cpeq (Component (Right Term era t
x) [AnyF era t]
xs) (Component (Right Term era t
y) [AnyF era t]
ys) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era t
x Term era t
y Bool -> Bool -> Bool
&& forall a b. (a -> b -> Bool) -> [a] -> [b] -> Bool
listEq forall era t s. Era era => AnyF era t -> AnyF era s -> Bool
anyWeq [AnyF era t]
xs [AnyF era t]
ys
cpeq (Member (Right Term era a
x) Term era (Set a)
xs) (Member (Right Term era a
y) Term era (Set a)
ys) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era a
x Term era a
y Bool -> Bool -> Bool
&& forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era (Set a)
xs Term era (Set a)
ys
cpeq (Member (Left Term era a
x) Term era (Set a)
xs) (Member (Left Term era a
y) Term era (Set a)
ys) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era a
x Term era a
y Bool -> Bool -> Bool
&& forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era (Set a)
xs Term era (Set a)
ys
cpeq (SubMap Term era (Map k v)
x Term era (Map k v)
xs) (SubMap Term era (Map k v)
y Term era (Map k v)
ys) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era (Map k v)
x Term era (Map k v)
y Bool -> Bool -> Bool
&& forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era (Map k v)
xs Term era (Map k v)
ys
cpeq (NotMember Term era a
x Term era (Set a)
xs) (NotMember Term era a
y Term era (Set a)
ys) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era a
x Term era a
y Bool -> Bool -> Bool
&& forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era (Set a)
xs Term era (Set a)
ys
{- TODO FIX ME
cpeq (x :<-: xs) (y :<-: ys) = case testEql (termRep x) (termRep y) of
  Just Refl -> typedEq x y && _ctareq xs ys
  Nothing -> False
-}
cpeq Pred era
x Pred era
y = forall era. Era era => Pred era -> Pred era -> Bool
sumsEq Pred era
x Pred era
y

-- |  Conservative SumsTo equality
sumsEq :: Era era => Pred era -> Pred era -> Bool
sumsEq :: forall era. Era era => Pred era -> Pred era -> Bool
sumsEq (SumsTo (Left c
s1) Term era c
x1 OrdCond
c1 [Sum era c]
ss1) (SumsTo (Left c
s2) Term era c
x2 OrdCond
c2 [Sum era c]
ss2) =
  case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql (forall era t. Era era => Term era t -> Rep era t
termRep Term era c
x1) (forall era t. Era era => Term era t -> Rep era t
termRep Term era c
x2) of
    Just c :~: c
Refl -> c
s1 forall a. Eq a => a -> a -> Bool
== c
s2 Bool -> Bool -> Bool
&& forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era c
x1 Term era c
x2 Bool -> Bool -> Bool
&& OrdCond
c1 forall a. Eq a => a -> a -> Bool
== OrdCond
c2 Bool -> Bool -> Bool
&& forall a b. (a -> b -> Bool) -> [a] -> [b] -> Bool
listEq forall era t. Era era => Sum era t -> Sum era t -> Bool
csumeq [Sum era c]
ss1 [Sum era c]
ss2
    Maybe (c :~: c)
Nothing -> Bool
False
sumsEq (SumsTo (Right c
s1) Term era c
x1 OrdCond
c1 [Sum era c]
ss1) (SumsTo (Right c
s2) Term era c
x2 OrdCond
c2 [Sum era c]
ss2) =
  case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql (forall era t. Era era => Term era t -> Rep era t
termRep Term era c
x1) (forall era t. Era era => Term era t -> Rep era t
termRep Term era c
x2) of
    Just c :~: c
Refl -> c
s1 forall a. Eq a => a -> a -> Bool
== c
s2 Bool -> Bool -> Bool
&& forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era c
x1 Term era c
x2 Bool -> Bool -> Bool
&& OrdCond
c1 forall a. Eq a => a -> a -> Bool
== OrdCond
c2 Bool -> Bool -> Bool
&& forall a b. (a -> b -> Bool) -> [a] -> [b] -> Bool
listEq forall era t. Era era => Sum era t -> Sum era t -> Bool
csumeq [Sum era c]
ss1 [Sum era c]
ss2
    Maybe (c :~: c)
Nothing -> Bool
False
sumsEq Pred era
_ Pred era
_ = Bool
False

-- | Conservative Sum equality
cseq :: Era era => Sum era c -> Sum era d -> Bool
cseq :: forall era c d. Era era => Sum era c -> Sum era d -> Bool
cseq (One Term era c
x) (One Term era d
y) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era c
x Term era d
y
cseq (SumMap Term era (Map a c)
x) (SumMap Term era (Map a d)
y) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era (Map a c)
x Term era (Map a d)
y
cseq (SumList Term era [c]
x) (SumList Term era [d]
y) = forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era [c]
x Term era [d]
y
cseq (ProjMap Rep era c
r1 Lens' x c
_ Term era (Map a x)
x) (ProjMap Rep era d
r2 Lens' x d
_ Term era (Map a x)
y) = case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql Rep era c
r1 Rep era d
r2 of
  Just c :~: d
Refl -> forall era a b. Era era => Term era a -> Term era b -> Bool
typedEq Term era (Map a x)
x Term era (Map a x)
y
  Maybe (c :~: d)
Nothing -> Bool
False
cseq Sum era c
_ Sum era d
_ = Bool
False

anyWeq :: Era era => AnyF era t -> AnyF era s -> Bool
anyWeq :: forall era t s. Era era => AnyF era t -> AnyF era s -> Bool
anyWeq (AnyF (Field String
x Rep era t
y Rep era t
z Lens' t t
l)) (AnyF (Field String
a Rep era t
b Rep era s
c Lens' s t
m)) = forall era t. V era t -> Name era
Name (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
x Rep era t
y (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era t
z Lens' t t
l)) forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
a Rep era t
b (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era s
c Lens' s t
m))
anyWeq AnyF era t
_ AnyF era s
_ = Bool
False

-- ==================================================================================
-- Rewriting by replacing (Dom x) by a new varariabl xDom, and adding additional
-- [Pred], that relate xDom with other terms

mkNewVar :: forall era d r. Term era (Map d r) -> Term era (Set d)
mkNewVar :: forall era d r. Term era (Map d r) -> Term era (Set d)
mkNewVar (Var (V String
nm (MapR Rep era a
d Rep era b
_) Access era s (Map d r)
_)) = Term era (Set a)
newVar
  where
    newstring :: String
newstring = String
nm forall a. [a] -> [a] -> [a]
++ String
"Dom"
    newV :: V era (Set a)
newV = forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
newstring (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era a
d) forall era s t. Access era s t
No
    newVar :: Term era (Set a)
newVar = forall era t. V era t -> Term era t
Var V era (Set a)
newV
mkNewVar Term era (Map d r)
other = forall a. HasCallStack => String -> a
error (String
"mkNewVar should only be applied to variables: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term era (Map d r)
other)

addP :: Era era => Pred era -> [Pred era] -> [Pred era]
addP :: forall era. Era era => Pred era -> [Pred era] -> [Pred era]
addP Pred era
p [Pred era]
ps = forall a. (a -> a -> Bool) -> [a] -> [a]
List.nubBy forall era. Era era => Pred era -> Pred era -> Bool
cpeq (Pred era
p forall a. a -> [a] -> [a]
: [Pred era]
ps)

addPred ::
  Era era => HashSet (Name era) -> Pred era -> [Name era] -> [Pred era] -> [Pred era] -> [Pred era]
addPred :: forall era.
Era era =>
HashSet (Name era)
-> Pred era -> [Name era] -> [Pred era] -> [Pred era] -> [Pred era]
addPred HashSet (Name era)
bad Pred era
orig [Name era]
names [Pred era]
ans [Pred era]
newps =
  if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Name era
x -> forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member Name era
x HashSet (Name era)
bad) [Name era]
names
    then forall era. Era era => Pred era -> [Pred era] -> [Pred era]
addP Pred era
orig [Pred era]
ans
    else forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall era. Era era => Pred era -> [Pred era] -> [Pred era]
addP [Pred era]
ans [Pred era]
newps

removeSameVar :: Era era => [Pred era] -> [Pred era] -> [Pred era]
removeSameVar :: forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeSameVar [] [Pred era]
ans = forall a. [a] -> [a]
reverse [Pred era]
ans
removeSameVar ((Var V era a
v :=: Var V era a
u) : [Pred era]
more) [Pred era]
ans | forall era t. V era t -> Name era
Name V era a
v forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era a
u = forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeSameVar [Pred era]
more [Pred era]
ans
removeSameVar ((Var V era (Set a)
v :⊆: Var V era (Set a)
u) : [Pred era]
more) [Pred era]
ans | forall era t. V era t -> Name era
Name V era (Set a)
v forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Set a)
u = forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeSameVar [Pred era]
more [Pred era]
ans
removeSameVar (Disjoint (Var v :: V era (Set a)
v@(V String
_ Rep era (Set a)
rep Access era s (Set a)
_)) (Var V era (Set a)
u) : [Pred era]
more) [Pred era]
ans | forall era t. V era t -> Name era
Name V era (Set a)
v forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Set a)
u = forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeSameVar [Pred era]
more ((forall era t. Rep era t -> t -> Term era t
Lit Rep era (Set a)
rep forall a. Monoid a => a
mempty forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era t. V era t -> Term era t
Var V era (Set a)
v) forall a. a -> [a] -> [a]
: [Pred era]
ans)
removeSameVar (Pred era
m : [Pred era]
more) [Pred era]
ans = forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeSameVar [Pred era]
more (Pred era
m forall a. a -> [a] -> [a]
: [Pred era]
ans)

removeEqual :: Era era => [Pred era] -> [Pred era] -> [Pred era]
removeEqual :: forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeEqual [] [Pred era]
ans = forall a. [a] -> [a]
reverse [Pred era]
ans
removeEqual ((Var V era a
v :=: Var V era a
u) : [Pred era]
more) [Pred era]
ans | forall era t. V era t -> Name era
Name V era a
v forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era a
u = forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeEqual [Pred era]
more [Pred era]
ans
removeEqual ((Var V era a
v :=: expr :: Term era a
expr@Lit {}) : [Pred era]
more) [Pred era]
ans = forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeEqual (forall a b. (a -> b) -> [a] -> [b]
map Pred era -> Pred era
sub [Pred era]
more) ((forall era t. V era t -> Term era t
Var V era a
v forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era a
expr) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Pred era -> Pred era
sub [Pred era]
ans)
  where
    sub :: Pred era -> Pred era
sub = forall era. Subst era -> Pred era -> Pred era
substPred (forall era t. V era t -> Term era t -> Subst era
singleSubst V era a
v Term era a
expr)
removeEqual ((expr :: Term era a
expr@Lit {} :=: Var V era a
v) : [Pred era]
more) [Pred era]
ans = forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeEqual (forall a b. (a -> b) -> [a] -> [b]
map Pred era -> Pred era
sub [Pred era]
more) ((Term era a
expr forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era t. V era t -> Term era t
Var V era a
v) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Pred era -> Pred era
sub [Pred era]
ans)
  where
    sub :: Pred era -> Pred era
sub = forall era. Subst era -> Pred era -> Pred era
substPred (forall era t. V era t -> Term era t -> Subst era
singleSubst V era a
v Term era a
expr)
removeEqual (Pred era
m : [Pred era]
more) [Pred era]
ans = forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeEqual [Pred era]
more (Pred era
m forall a. a -> [a] -> [a]
: [Pred era]
ans)

removeTrivial :: Era era => [Pred era] -> [Pred era]
removeTrivial :: forall era. Era era => [Pred era] -> [Pred era]
removeTrivial = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {era}. Era era => Pred era -> Bool
trivial)
  where
    trivial :: Pred era -> Bool
trivial Pred era
p | forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred forall a. Monoid a => a
mempty Pred era
p) =
      case forall x. Typed x -> Either [String] x
runTyped forall a b. (a -> b) -> a -> b
$ forall era. Env era -> Pred era -> Typed Bool
runPred (forall era. Map String (Payload era) -> Env era
Env forall a. Monoid a => a
mempty) Pred era
p of
        Left {} -> Bool
False
        Right Bool
validx -> Bool
validx
    trivial (Term era a
e1 :=: Term era a
e2) = forall era t. Era era => Term era t -> Term era t -> Bool
cteq Term era a
e1 Term era a
e2
    trivial Pred era
_ = Bool
False

rewrite :: Era era => [Pred era] -> [Pred era]
rewrite :: forall era. Era era => [Pred era] -> [Pred era]
rewrite [Pred era]
cs = forall era. Era era => [Pred era] -> [Pred era]
removeTrivial forall a b. (a -> b) -> a -> b
$ forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeSameVar (forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeEqual [Pred era]
cs []) []

-- =========================================================
-- Expanding (Choose _ _ _) into several simpler [Pred era]

type SubItems era = [SubItem era]

fresh :: (Int, SubItems era) -> RootTarget era r t -> (Int, SubItems era)
fresh :: forall era r t.
(Vertex, SubItems era)
-> RootTarget era r t -> (Vertex, SubItems era)
fresh (Vertex
n, SubItems era
sub) (Constr String
_ a -> b
_) = (Vertex
n, SubItems era
sub)
fresh (Vertex
n, SubItems era
sub) (Invert String
_ TypeRep r
_ a -> b
_) = (Vertex
n, SubItems era
sub)
fresh (Vertex
n, SubItems era
sub) (Shift RootTarget era root2 t
x Lens' r root2
_) = forall era r t.
(Vertex, SubItems era)
-> RootTarget era r t -> (Vertex, SubItems era)
fresh (Vertex
n, SubItems era
sub) RootTarget era root2 t
x
fresh (Vertex
n, SubItems era
sub) (Mask RootTarget era r t
x) = forall era r t.
(Vertex, SubItems era)
-> RootTarget era r t -> (Vertex, SubItems era)
fresh (Vertex
n, SubItems era
sub) RootTarget era r t
x
fresh (Vertex
n, SubItems era
sub) (Simple (Var v :: V era t
v@(V String
nm Rep era t
rep Access era s t
acc))) = (Vertex
n forall a. Num a => a -> a -> a
+ Vertex
1, forall era t. V era t -> Term era t -> SubItem era
SubItem V era t
v (forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V (String -> Vertex -> String
index String
nm Vertex
n) Rep era t
rep Access era s t
acc)) forall a. a -> [a] -> [a]
: SubItems era
sub)
fresh (Vertex
n, SubItems era
sub) (Simple Term era t
expr) = Vertex -> [Name era] -> (Vertex, SubItems era)
mksub Vertex
n (forall a. HashSet a -> [a]
HashSet.toList (forall era t. Term era t -> HashSet (Name era)
vars Term era t
expr))
  where
    mksub :: Vertex -> [Name era] -> (Vertex, SubItems era)
mksub Vertex
m [Name era]
names = (Vertex
n forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [Name era]
names, SubItems era
sub2 forall a. [a] -> [a] -> [a]
++ SubItems era
sub)
      where
        sub2 :: SubItems era
sub2 = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Name v :: V era t
v@(V String
nm Rep era t
r Access era s t
_)) Vertex
m1 -> forall era t. V era t -> Term era t -> SubItem era
SubItem V era t
v (forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V (String -> Vertex -> String
index String
nm Vertex
m1) Rep era t
r forall era s t. Access era s t
No))) [Name era]
names [Vertex
m ..]
fresh (Vertex
n, SubItems era
sub) (Lensed (Var v :: V era t
v@(V String
nm Rep era t
rep Access era s t
acc)) SimpleGetter r t
_) = (Vertex
n forall a. Num a => a -> a -> a
+ Vertex
1, forall era t. V era t -> Term era t -> SubItem era
SubItem V era t
v (forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V (String -> Vertex -> String
index String
nm Vertex
n) Rep era t
rep Access era s t
acc)) forall a. a -> [a] -> [a]
: SubItems era
sub)
fresh (Vertex
n, SubItems era
sub) (Lensed Term era t
expr SimpleGetter r t
_) = Vertex -> [Name era] -> (Vertex, SubItems era)
mksub Vertex
n (forall a. HashSet a -> [a]
HashSet.toList (forall era t. Term era t -> HashSet (Name era)
vars Term era t
expr))
  where
    mksub :: Vertex -> [Name era] -> (Vertex, SubItems era)
mksub Vertex
m [Name era]
names = (Vertex
n forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [Name era]
names, SubItems era
sub2 forall a. [a] -> [a] -> [a]
++ SubItems era
sub)
      where
        sub2 :: SubItems era
sub2 = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Name v :: V era t
v@(V String
nm Rep era t
r Access era s t
_)) Vertex
m1 -> forall era t. V era t -> Term era t -> SubItem era
SubItem V era t
v (forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V (String -> Vertex -> String
index String
nm Vertex
m1) Rep era t
r forall era s t. Access era s t
No))) [Name era]
names [Vertex
m ..]
fresh (Vertex
n, SubItems era
sub) (Partial (Var v :: V era t
v@(V String
nm Rep era t
rep Access era s t
acc)) r -> Maybe t
_) = (Vertex
n forall a. Num a => a -> a -> a
+ Vertex
1, forall era t. V era t -> Term era t -> SubItem era
SubItem V era t
v (forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V (String -> Vertex -> String
index String
nm Vertex
n) Rep era t
rep Access era s t
acc)) forall a. a -> [a] -> [a]
: SubItems era
sub)
fresh (Vertex
n, SubItems era
sub) (Partial Term era t
expr r -> Maybe t
_) = Vertex -> [Name era] -> (Vertex, SubItems era)
mksub Vertex
n (forall a. HashSet a -> [a]
HashSet.toList (forall era t. Term era t -> HashSet (Name era)
vars Term era t
expr))
  where
    mksub :: Vertex -> [Name era] -> (Vertex, SubItems era)
mksub Vertex
m [Name era]
names = (Vertex
n forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [Name era]
names, SubItems era
sub2 forall a. [a] -> [a] -> [a]
++ SubItems era
sub)
      where
        sub2 :: SubItems era
sub2 = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Name v :: V era t
v@(V String
nm Rep era t
r Access era s t
_)) Vertex
m1 -> forall era t. V era t -> Term era t -> SubItem era
SubItem V era t
v (forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V (String -> Vertex -> String
index String
nm Vertex
m1) Rep era t
r forall era s t. Access era s t
No))) [Name era]
names [Vertex
m ..]
fresh (Vertex
n, SubItems era
sub) (RootTarget era r (a -> t)
f :$ RootTarget era r a
x) = forall era r t.
(Vertex, SubItems era)
-> RootTarget era r t -> (Vertex, SubItems era)
fresh (forall era r t.
(Vertex, SubItems era)
-> RootTarget era r t -> (Vertex, SubItems era)
fresh (Vertex
n, SubItems era
sub) RootTarget era r (a -> t)
f) RootTarget era r a
x
fresh (Vertex
n, SubItems era
sub) (Virtual Term era t
x PDoc
_ Lens' r t
_) = forall era r t.
(Vertex, SubItems era)
-> RootTarget era r t -> (Vertex, SubItems era)
fresh (Vertex
n, SubItems era
sub) (forall era t. Term era t -> RootTarget era Void t
Simple Term era t
x)

freshP :: (Int, SubItems era) -> Pat era t -> (Int, SubItems era)
freshP :: forall era t.
(Vertex, SubItems era) -> Pat era t -> (Vertex, SubItems era)
freshP (Vertex
n, SubItems era
sub) (Pat Rep era t
_ [Arg era t]
as) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era t.
(Vertex, SubItems era) -> Arg era t -> (Vertex, SubItems era)
freshA (Vertex
n, SubItems era
sub) [Arg era t]
as

freshA :: (Int, SubItems era) -> Arg era t -> (Int, SubItems era)
freshA :: forall era t.
(Vertex, SubItems era) -> Arg era t -> (Vertex, SubItems era)
freshA (Vertex
n, SubItems era
sub) (Arg (Field String
nm Rep era s
r Rep era t
a Lens' t s
l)) = (Vertex
n forall a. Num a => a -> a -> a
+ Vertex
1, forall era t. V era t -> Term era t -> SubItem era
SubItem (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
nm Rep era s
r (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era t
a Lens' t s
l)) (forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V (String -> Vertex -> String
index String
nm Vertex
n) Rep era s
r (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era t
a Lens' t s
l))) forall a. a -> [a] -> [a]
: SubItems era
sub)
freshA (Vertex, SubItems era)
pair (Arg (FConst Rep era s
_ s
_ Rep era t
_ Lens' t s
_)) = (Vertex, SubItems era)
pair
freshA (Vertex
n, SubItems era
sub) (ArgPs (Field String
nm Rep era s
r Rep era t
a Lens' t s
l) [Pat era s]
ps) =
  forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era t.
(Vertex, SubItems era) -> Pat era t -> (Vertex, SubItems era)
freshP (Vertex
n forall a. Num a => a -> a -> a
+ Vertex
1, forall era t. V era t -> Term era t -> SubItem era
SubItem (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
nm Rep era s
r (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era t
a Lens' t s
l)) (forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V (String -> Vertex -> String
index String
nm Vertex
n) Rep era s
r (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era t
a Lens' t s
l))) forall a. a -> [a] -> [a]
: SubItems era
sub) [Pat era s]
ps
freshA (Vertex, SubItems era)
pair (ArgPs (FConst Rep era s
_ s
_ Rep era t
_ Lens' t s
_) [Pat era s]
ps) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era t.
(Vertex, SubItems era) -> Pat era t -> (Vertex, SubItems era)
freshP (Vertex, SubItems era)
pair [Pat era s]
ps

freshVars :: Int -> Int -> V era [t] -> ([Term era t], Int)
freshVars :: forall era t.
Vertex -> Vertex -> V era [t] -> ([Term era t], Vertex)
freshVars Vertex
m Vertex
count (V String
nm (ListR Rep era a
rep) Access era s [t]
_) = ([forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V (String -> Vertex -> String
index String
nm Vertex
c) Rep era a
rep forall era s t. Access era s t
No) | Vertex
c <- [Vertex
m .. Vertex
m forall a. Num a => a -> a -> a
+ (Vertex
count forall a. Num a => a -> a -> a
- Vertex
1)]], Vertex
m forall a. Num a => a -> a -> a
+ Vertex
count)

index :: String -> Int -> String
index :: String -> Vertex -> String
index String
nm Vertex
c = String
nm forall a. [a] -> [a] -> [a]
++ String
"." forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Vertex
c

-- When we expect the variable to have a (FromList t a) constraint
freshVars2 :: FromList fs t => Int -> Int -> V era fs -> ([Term era t], Int)
freshVars2 :: forall fs t era.
FromList fs t =>
Vertex -> Vertex -> V era fs -> ([Term era t], Vertex)
freshVars2 Vertex
m Vertex
count (V String
nm Rep era fs
lrep Access era s fs
_) =
  let arep :: Rep era t
arep = forall ts a era. FromList ts a => Rep era ts -> Rep era a
tsRep Rep era fs
lrep
   in ([forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V (String -> Vertex -> String
index String
nm Vertex
c) Rep era t
arep forall era s t. Access era s t
No) | Vertex
c <- [Vertex
m .. Vertex
m forall a. Num a => a -> a -> a
+ (Vertex
count forall a. Num a => a -> a -> a
- Vertex
1)]], Vertex
m forall a. Num a => a -> a -> a
+ Vertex
count)

freshPairs ::
  ((Int, SubItems era), [(RootTarget era r t, [Pred era])]) ->
  (RootTarget era r t, [Pred era]) ->
  ((Int, SubItems era), [(RootTarget era r t, [Pred era])])
freshPairs :: forall era r t.
((Vertex, SubItems era), [(RootTarget era r t, [Pred era])])
-> (RootTarget era r t, [Pred era])
-> ((Vertex, SubItems era), [(RootTarget era r t, [Pred era])])
freshPairs ((Vertex, SubItems era)
xx, [(RootTarget era r t, [Pred era])]
ans) (RootTarget era r t
tar, [Pred era]
ps) = ((Vertex, SubItems era)
yy, (RootTarget era r t
target2, [Pred era]
ps2) forall a. a -> [a] -> [a]
: [(RootTarget era r t, [Pred era])]
ans)
  where
    yy :: (Vertex, SubItems era)
yy@(Vertex
_, SubItems era
subitems) = forall era r t.
(Vertex, SubItems era)
-> RootTarget era r t -> (Vertex, SubItems era)
fresh (Vertex, SubItems era)
xx RootTarget era r t
tar
    subst :: Subst era
subst = forall era. [SubItem era] -> Subst era
itemsToSubst SubItems era
subitems
    target2 :: RootTarget era r t
target2 = forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
subst RootTarget era r t
tar
    ps2 :: [Pred era]
ps2 = forall a b. (a -> b) -> [a] -> [b]
map (forall era. Subst era -> Pred era -> Pred era
substPred Subst era
subst) [Pred era]
ps

freshPair ::
  Int ->
  (RootTarget era r t, [Pred era]) ->
  (Int, SubItems era, RootTarget era r t, [Pred era])
freshPair :: forall era r t.
Vertex
-> (RootTarget era r t, [Pred era])
-> (Vertex, SubItems era, RootTarget era r t, [Pred era])
freshPair Vertex
m0 (RootTarget era r t
tar, [Pred era]
ps) = (Vertex
m1, SubItems era
subitems, RootTarget era r t
target2, [Pred era]
ps2)
  where
    (Vertex
m1, SubItems era
subitems) = forall era r t.
(Vertex, SubItems era)
-> RootTarget era r t -> (Vertex, SubItems era)
fresh (Vertex
m0, []) RootTarget era r t
tar
    subst :: Subst era
subst = forall era. [SubItem era] -> Subst era
itemsToSubst SubItems era
subitems
    target2 :: RootTarget era r t
target2 = forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
subst RootTarget era r t
tar
    ps2 :: [Pred era]
ps2 = forall a b. (a -> b) -> [a] -> [b]
map (forall era. Subst era -> Pred era -> Pred era
substPred Subst era
subst) [Pred era]
ps

-- | Used to rename targets and preds, where they are embeded in a Triple, where the first component is the frequency
_freshTriples ::
  ((Int, SubItems era), [(Int, RootTarget era r t, [Pred era])]) ->
  (Int, RootTarget era r t, [Pred era]) ->
  ((Int, SubItems era), [(Int, RootTarget era r t, [Pred era])])
_freshTriples :: forall era r t.
((Vertex, SubItems era),
 [(Vertex, RootTarget era r t, [Pred era])])
-> (Vertex, RootTarget era r t, [Pred era])
-> ((Vertex, SubItems era),
    [(Vertex, RootTarget era r t, [Pred era])])
_freshTriples ((Vertex, SubItems era)
xx, [(Vertex, RootTarget era r t, [Pred era])]
ans) (Vertex
i, RootTarget era r t
tar, [Pred era]
ps) = ((Vertex, SubItems era)
yy, (Vertex
i, RootTarget era r t
target2, [Pred era]
ps2) forall a. a -> [a] -> [a]
: [(Vertex, RootTarget era r t, [Pred era])]
ans)
  where
    yy :: (Vertex, SubItems era)
yy@(Vertex
_, SubItems era
subitems) = forall era r t.
(Vertex, SubItems era)
-> RootTarget era r t -> (Vertex, SubItems era)
fresh (Vertex, SubItems era)
xx RootTarget era r t
tar
    subst :: Subst era
subst = forall era. [SubItem era] -> Subst era
itemsToSubst SubItems era
subitems
    target2 :: RootTarget era r t
target2 = forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
subst RootTarget era r t
tar
    ps2 :: [Pred era]
ps2 = forall a b. (a -> b) -> [a] -> [b]
map (forall era. Subst era -> Pred era -> Pred era
substPred Subst era
subst) [Pred era]
ps

freshPats ::
  ((Int, SubItems era), [(Pat era t, [Pred era])]) ->
  (Pat era t, [Pred era]) ->
  ((Int, SubItems era), [(Pat era t, [Pred era])])
freshPats :: forall era t.
((Vertex, SubItems era), [(Pat era t, [Pred era])])
-> (Pat era t, [Pred era])
-> ((Vertex, SubItems era), [(Pat era t, [Pred era])])
freshPats ((Vertex, SubItems era)
xx, [(Pat era t, [Pred era])]
ans) (Pat era t
pat, [Pred era]
ps) = ((Vertex, SubItems era)
yy, (Pat era t
pat2, [Pred era]
ps2) forall a. a -> [a] -> [a]
: [(Pat era t, [Pred era])]
ans)
  where
    yy :: (Vertex, SubItems era)
yy@(Vertex
_, SubItems era
sub) = forall era t.
(Vertex, SubItems era) -> Pat era t -> (Vertex, SubItems era)
freshP (Vertex, SubItems era)
xx Pat era t
pat
    subst :: Subst era
subst = forall era. [SubItem era] -> Subst era
itemsToSubst SubItems era
sub
    pat2 :: Pat era t
pat2 = forall era t. Subst era -> Pat era t -> Pat era t
substPat Subst era
subst Pat era t
pat
    ps2 :: [Pred era]
ps2 = forall a b. (a -> b) -> [a] -> [b]
map (forall era. Subst era -> Pred era -> Pred era
substPred Subst era
subst) [Pred era]
ps

-- | We have something like (SumsTo x total EQL [One x]) and we want
--   something like: (SumsTo x total EQL [One x.1, One x.2, One x.3])
-- | Or something like (SumSplit x total EQL [One x]) which expands to
--   something like: (SumSplitx total EQL [One x.1, One x.2, One x.3])
--   So we find all the bindings for 'x' in the SubItems, and cons them together.
extendSum :: SubItems era -> Sum era c -> [Sum era c]
extendSum :: forall era c. SubItems era -> Sum era c -> [Sum era c]
extendSum SubItems era
sub (ProjOne Lens' x c
l Rep era c
r (Var V era x
v2)) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SubItem era -> [Sum era c] -> [Sum era c]
accum [] SubItems era
sub
  where
    accum :: SubItem era -> [Sum era c] -> [Sum era c]
accum (SubItem V era t
v1 Term era t
term) [Sum era c]
ans | Just t :~: x
Refl <- forall era t s. V era t -> V era s -> Maybe (t :~: s)
sameName V era t
v1 V era x
v2 = forall x c era. Lens' x c -> Rep era c -> Term era x -> Sum era c
ProjOne Lens' x c
l Rep era c
r Term era t
term forall a. a -> [a] -> [a]
: [Sum era c]
ans
    accum SubItem era
_ [Sum era c]
ans = [Sum era c]
ans
extendSum SubItems era
sub (One (Var V era c
v2)) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SubItem era -> [Sum era c] -> [Sum era c]
accum [] SubItems era
sub
  where
    accum :: SubItem era -> [Sum era c] -> [Sum era c]
accum (SubItem V era t
v1 Term era t
term) [Sum era c]
ans | Just t :~: c
Refl <- forall era t s. V era t -> V era s -> Maybe (t :~: s)
sameName V era t
v1 V era c
v2 = forall era c. Term era c -> Sum era c
One Term era t
term forall a. a -> [a] -> [a]
: [Sum era c]
ans
    accum SubItem era
_ [Sum era c]
ans = [Sum era c]
ans
extendSum SubItems era
_sub Sum era c
other = forall a. HasCallStack => String -> a
error (String
"None One or ProjOne in Sum list: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Sum era c
other)

extendSums :: Era era => SubItems era -> [Pred era] -> [Pred era]
extendSums :: forall era. Era era => SubItems era -> [Pred era] -> [Pred era]
extendSums SubItems era
_ [] = []
extendSums SubItems era
sub (SumsTo Direct c
c Term era c
t OrdCond
cond [Sum era c
s] : [Pred era]
more) = forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo Direct c
c Term era c
t OrdCond
cond (forall era c. SubItems era -> Sum era c -> [Sum era c]
extendSum SubItems era
sub Sum era c
s) forall a. a -> [a] -> [a]
: forall era. Era era => SubItems era -> [Pred era] -> [Pred era]
extendSums SubItems era
sub [Pred era]
more
extendSums SubItems era
sub (SumSplit c
c Term era c
t OrdCond
cond [Sum era c
s] : [Pred era]
more) = forall era c.
(Era era, Adds c) =>
c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumSplit c
c Term era c
t OrdCond
cond (forall era c. SubItems era -> Sum era c -> [Sum era c]
extendSum SubItems era
sub Sum era c
s) forall a. a -> [a] -> [a]
: forall era. Era era => SubItems era -> [Pred era] -> [Pred era]
extendSums SubItems era
sub [Pred era]
more
extendSums SubItems era
_ (Pred era
m : [Pred era]
_more) = forall a. HasCallStack => String -> a
error (String
"Non extendableSumsTo in extendSums: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred era
m)

rename :: Name era -> [Int] -> [Name era]
rename :: forall era. Name era -> [Vertex] -> [Name era]
rename name :: Name era
name@(Name (V String
nm Rep era t
r Access era s t
a)) [Vertex]
ns = case forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall a. Eq a => a -> a -> Bool
/= Char
'.') String
nm of
  (Char
_ : String
_) -> forall a b. (a -> b) -> [a] -> [b]
map (\Vertex
n -> forall era t. V era t -> Name era
Name (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V (String -> Vertex -> String
index String
nm Vertex
n) Rep era t
r Access era s t
a)) [Vertex]
ns
  String
_ -> [Name era
name]

nUniqueFromM :: Int -> Int -> Gen [Int]
nUniqueFromM :: Vertex -> Vertex -> Gen [Vertex]
nUniqueFromM Vertex
n Vertex
m
  | Vertex
n forall a. Eq a => a -> a -> Bool
== Vertex
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure []
  | Vertex
n forall a. Ord a => a -> a -> Bool
> Vertex
m = forall (f :: * -> *) a. Applicative f => a -> f a
pure [Vertex
0 .. Vertex
m]
  | Bool
otherwise =
      forall a. Set a -> [a]
Set.toList
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Ord a => [String] -> Vertex -> Gen a -> Gen (Set a)
setSized [String
"from Choose", String
"nUniqueFromM " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Vertex
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Vertex
m] Vertex
n (forall a. Random a => (a, a) -> Gen a
choose (Vertex
0, Vertex
m))

_pickNunique :: Int -> [a] -> Gen [a]
_pickNunique :: forall a. Vertex -> [a] -> Gen [a]
_pickNunique Vertex
n [a]
xs = do
  [Vertex]
indexes <- Vertex -> Vertex -> Gen [Vertex]
nUniqueFromM Vertex
n (forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [a]
xs forall a. Num a => a -> a -> a
- Vertex
1)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure [[a]
xs forall a. [a] -> Vertex -> a
!! Vertex
i | Vertex
i <- [Vertex]
indexes]

-- | Make a GenFrom frequency Pred, from the input and output terms
freq :: forall era t. Term era t -> Term era [(Int, t)] -> Pred era
freq :: forall era t. Term era t -> Term era [(Vertex, t)] -> Pred era
freq Term era t
outVar Term era [(Vertex, t)]
inVar = forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom Term era t
outVar (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"frequency" (forall a. HasCallStack => [(Vertex, Gen a)] -> Gen a
frequency forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {f :: * -> *} {a} {a}. Applicative f => (a, a) -> (a, f a)
h) forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ (forall era t. Term era t -> RootTarget era Void t
Simple Term era [(Vertex, t)]
inVar))
  where
    h :: (a, a) -> (a, f a)
h (a
i, a
x) = (a
i, forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x)

-- | Where is an abstraction for ( term :<-: target : preds )
type Where era t = (Term era t, RootTarget era t t, [Pred era])

-- | Unfold (Where x tar ps) into (x :<-: tar' : ps'), renaming tar to tar' and ps to ps'
unfoldWhere :: forall era t. ([Where era t], Int) -> ([Pred era], Int)
unfoldWhere :: forall era t. ([Where era t], Vertex) -> ([Pred era], Vertex)
unfoldWhere ([Where era t]
ps0, Vertex
m0) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' ([Pred era], Vertex) -> Where era t -> ([Pred era], Vertex)
accum ([], Vertex
m0) [Where era t]
ps0
  where
    accum :: ([Pred era], Int) -> Where era t -> ([Pred era], Int)
    accum :: ([Pred era], Vertex) -> Where era t -> ([Pred era], Vertex)
accum ([Pred era]
ans, Vertex
mx) (Term era t
t, RootTarget era t t
tar, [Pred era]
ps) = ((Term era t
t forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: RootTarget era t t
tar2) forall a. a -> [a] -> [a]
: [Pred era]
ps2 forall a. [a] -> [a] -> [a]
++ [Pred era]
ans, Vertex
mx1)
      where
        (Vertex
mx1, SubItems era
_, RootTarget era t t
tar2, [Pred era]
ps2) = forall era r t.
Vertex
-> (RootTarget era r t, [Pred era])
-> (Vertex, SubItems era, RootTarget era r t, [Pred era])
freshPair Vertex
mx (RootTarget era t t
tar, [Pred era]
ps)

rewritePred :: Era era => Int -> Pred era -> Gen ([Pred era], Int)
{-
OneOf x [(i,t1,p1),(j,t2,p2)] rewrites to
[ Where x.1 t1 p1, Where x.2 t2 p2, List xlist.3 [(i,x.1),(j,x.2)], GenFrom x frequency xlist.3]
where each (Where xi ti pi) is unfolded by renaming 'ti' and 'pi'
-}
rewritePred :: forall era.
Era era =>
Vertex -> Pred era -> Gen ([Pred era], Vertex)
rewritePred Vertex
m0 (Oneof term :: Term era t
term@(Var (V String
nm Rep era t
rep Access era s t
_)) [(Vertex, RootTarget era t t, [Pred era])]
ps0) = do
  let count :: Vertex
count = forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [(Vertex, RootTarget era t t, [Pred era])]
ps0
      ([Term era t]
vs, Vertex
m1) = forall era t.
Vertex -> Vertex -> V era [t] -> ([Term era t], Vertex)
freshVars Vertex
m0 Vertex
count (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
nm (forall era a. Rep era a -> Rep era [a]
ListR Rep era t
rep) forall era s t. Access era s t
No)
      (Term era [(Vertex, t)]
vlist, Vertex
m2) = (forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V (String -> Vertex -> String
index (String
nm forall a. [a] -> [a] -> [a]
++ String
"Pairs") Vertex
m1) (forall era a. Rep era a -> Rep era [a]
ListR (forall era a b. Rep era a -> Rep era b -> Rep era (a, b)
PairR forall era. Rep era Vertex
IntR Rep era t
rep)) forall era s t. Access era s t
No), Vertex
m1 forall a. Num a => a -> a -> a
+ Vertex
1)
      params :: [Term era (Vertex, t)]
params = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Term era t
param (Vertex
i, RootTarget era t t
_, [Pred era]
_) -> forall era a b. Term era a -> Term era b -> Term era (a, b)
Pair (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Vertex
IntR Vertex
i) Term era t
param) [Term era t]
vs [(Vertex, RootTarget era t t, [Pred era])]
ps0
      wheres :: [(Term era t, RootTarget era t t, [Pred era])]
wheres = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Term era t
v (Vertex
_, RootTarget era t t
tar, [Pred era]
ps) -> (Term era t
v, RootTarget era t t
tar, [Pred era]
ps)) [Term era t]
vs [(Vertex, RootTarget era t t, [Pred era])]
ps0
      ([Pred era]
unfolded, Vertex
m3) = forall era t. ([Where era t], Vertex) -> ([Pred era], Vertex)
unfoldWhere ([(Term era t, RootTarget era t t, [Pred era])]
wheres, Vertex
m2)
  ([Pred era]
expandedPred, Vertex
m4) <- forall era.
Era era =>
([Pred era], Vertex) -> [Pred era] -> Gen ([Pred era], Vertex)
removeExpandablePred ([], Vertex
m3) [Pred era]
unfolded
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Pred era]
expandedPred forall a. [a] -> [a] -> [a]
++ [forall fs t era.
FromList fs t =>
Term era fs -> [Term era t] -> Pred era
List Term era [(Vertex, t)]
vlist [Term era (Vertex, t)]
params, forall era t. Term era t -> Term era [(Vertex, t)] -> Pred era
freq Term era t
term Term era [(Vertex, t)]
vlist], Vertex
m4)
rewritePred Vertex
m0 (Choose (Lit Rep era Size
SizeR Size
sz) (Var V era [t]
v) [(Vertex, Target era t, [Pred era])]
ps0) = do
  let ps1 :: [(Vertex, Target era t, [Pred era])]
ps1 = forall a. (a -> Bool) -> [a] -> [a]
filter (\(Vertex
i, Target era t
_, [Pred era]
_) -> Vertex
i forall a. Ord a => a -> a -> Bool
> Vertex
0) [(Vertex, Target era t, [Pred era])]
ps0
  Vertex
count <- Size -> Gen Vertex
genFromSize Size
sz
  [(Target era t, [Pred era])]
ps2 <-
    if Vertex
count forall a. Ord a => a -> a -> Bool
<= forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [(Vertex, Target era t, [Pred era])]
ps1
      then forall a. Vertex -> [a] -> [a]
take Vertex
count forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [a] -> Gen [a]
shuffle (forall a b. (a -> b) -> [a] -> [b]
map (\(Vertex
_, Target era t
t, [Pred era]
p) -> (Target era t
t, [Pred era]
p)) [(Vertex, Target era t, [Pred era])]
ps1)
      else forall a. Vertex -> Gen a -> Gen [a]
vectorOf Vertex
count (forall a. HasCallStack => [(Vertex, Gen a)] -> Gen a
frequency (forall a b. (a -> b) -> [a] -> [b]
map (\(Vertex
i, Target era t
t, [Pred era]
p) -> (Vertex
i, forall (f :: * -> *) a. Applicative f => a -> f a
pure (Target era t
t, [Pred era]
p))) [(Vertex, Target era t, [Pred era])]
ps1))
  let ((Vertex
m1, SubItems era
_), [(Target era t, [Pred era])]
ps3) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era r t.
((Vertex, SubItems era), [(RootTarget era r t, [Pred era])])
-> (RootTarget era r t, [Pred era])
-> ((Vertex, SubItems era), [(RootTarget era r t, [Pred era])])
freshPairs ((Vertex
m0, []), []) [(Target era t, [Pred era])]
ps2
      ([Term era t]
xs, Vertex
m2) = forall era t.
Vertex -> Vertex -> V era [t] -> ([Term era t], Vertex)
freshVars Vertex
m1 Vertex
count V era [t]
v
      renamedPred :: [[Pred era]]
renamedPred = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Target era t, [Pred era])]
ps3
  ([Pred era]
expandedPred, Vertex
m3) <- forall era.
Era era =>
([Pred era], Vertex) -> [Pred era] -> Gen ([Pred era], Vertex)
removeExpandablePred ([], Vertex
m2) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Pred era]]
renamedPred)
  let newps :: [Pred era]
newps = [Pred era]
expandedPred forall a. [a] -> [a] -> [a]
++ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall era t r. Term era t -> RootTarget era r t -> Pred era
(:<-:) [Term era t]
xs (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Target era t, [Pred era])]
ps3) forall a. [a] -> [a] -> [a]
++ [forall fs t era.
FromList fs t =>
Term era fs -> [Term era t] -> Pred era
List (forall era t. V era t -> Term era t
Var V era [t]
v) [Term era t]
xs]
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Pred era]
newps, Vertex
m3)

{- ListWhere (Range 2 2) w target{a,b} [Member a x, Member b y] rewrites to
[ Member a1 x
, Member b1 y
, Member a2 x
, Member b2 y
, w1 :<-: target{a1,b1} a1 b1
, w2 :<-: target{a2,b2} a2 b2
List w [w1,w2]
] -}
rewritePred Vertex
m0 (ListWhere (Lit Rep era Size
SizeR Size
sz) (Var V era [t]
v) RootTarget era t t
tar [Pred era]
ps) = do
  Vertex
count <- Size -> Gen Vertex
genFromSize Size
sz
  ([Pred era]
ps1, Vertex
m1) <- forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Pred era]
ps, Vertex
m0) -- removeExpandablePred ([], m0) ps
  let ((Vertex
m2, SubItems era
_subb), [(RootTarget era t t, [Pred era])]
ps3) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era r t.
((Vertex, SubItems era), [(RootTarget era r t, [Pred era])])
-> (RootTarget era r t, [Pred era])
-> ((Vertex, SubItems era), [(RootTarget era r t, [Pred era])])
freshPairs ((Vertex
m1, []), []) (forall a. Vertex -> [a] -> [a]
take Vertex
count (forall a. a -> [a]
repeat (RootTarget era t t
tar, [Pred era]
ps1)))
      ([Term era t]
vs, Vertex
m3) = forall fs t era.
FromList fs t =>
Vertex -> Vertex -> V era fs -> ([Term era t], Vertex)
freshVars2 Vertex
m2 Vertex
count V era [t]
v -- [v.1, v.2, v.3 ...]
      renamedPred :: [[Pred era]]
renamedPred = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(RootTarget era t t, [Pred era])]
ps3
      renamedTargets :: [RootTarget era t t]
renamedTargets = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(RootTarget era t t, [Pred era])]
ps3
  ([Pred era]
expandedPred, Vertex
m4) <- forall era.
Era era =>
([Pred era], Vertex) -> [Pred era] -> Gen ([Pred era], Vertex)
removeExpandablePred ([], Vertex
m3) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Pred era]]
renamedPred)
  let newps :: [Pred era]
newps = [Pred era]
expandedPred forall a. [a] -> [a] -> [a]
++ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall era t r. Term era t -> RootTarget era r t -> Pred era
(:<-:) [Term era t]
vs [RootTarget era t t]
renamedTargets forall a. [a] -> [a] -> [a]
++ [forall fs t era.
FromList fs t =>
Term era fs -> [Term era t] -> Pred era
List (forall era t. V era t -> Term era t
Var V era [t]
v) [Term era t]
vs]
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Pred era]
newps, Vertex
m4)
rewritePred Vertex
m0 (ForEach (Lit Rep era Size
SizeR Size
sz) (Var V era fs
v) Pat era t
tar [Pred era]
ps) = do
  let ([Pred era]
sumstoPred, [Pred era]
otherPred) = forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (forall era t. Pat era t -> Pred era -> Bool
extendableSumsTo Pat era t
tar) [Pred era]
ps
  Vertex
count <- Size -> Gen Vertex
genFromSize Size
sz
  let ((Vertex
m1, SubItems era
subb), [(Pat era t, [Pred era])]
ps3) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era t.
((Vertex, SubItems era), [(Pat era t, [Pred era])])
-> (Pat era t, [Pred era])
-> ((Vertex, SubItems era), [(Pat era t, [Pred era])])
freshPats ((Vertex
m0, []), []) (forall a. Vertex -> [a] -> [a]
take Vertex
count (forall a. a -> [a]
repeat (Pat era t
tar, [Pred era]
otherPred)))
      ([Term era t]
xs, Vertex
m2) = forall fs t era.
FromList fs t =>
Vertex -> Vertex -> V era fs -> ([Term era t], Vertex)
freshVars2 Vertex
m1 Vertex
count V era fs
v
      renamedPred :: [[Pred era]]
renamedPred = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Pat era t, [Pred era])]
ps3
  ([Pred era]
expandedPred, Vertex
m3) <- forall era.
Era era =>
([Pred era], Vertex) -> [Pred era] -> Gen ([Pred era], Vertex)
removeExpandablePred ([], Vertex
m2) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Pred era]]
renamedPred)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    ( [Pred era]
expandedPred
        forall a. [a] -> [a] -> [a]
++ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component (forall a b. (a -> b) -> [a] -> [b]
map forall a b. b -> Either a b
Right [Term era t]
xs) (forall a b. (a -> b) -> [a] -> [b]
map (forall era t. Pat era t -> [AnyF era t]
patToAnyF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Pat era t, [Pred era])]
ps3)
        forall a. [a] -> [a] -> [a]
++ [forall fs t era.
FromList fs t =>
Term era fs -> [Term era t] -> Pred era
List (forall era t. V era t -> Term era t
Var V era fs
v) [Term era t]
xs]
        forall a. [a] -> [a] -> [a]
++ forall era. Era era => SubItems era -> [Pred era] -> [Pred era]
extendSums SubItems era
subb [Pred era]
sumstoPred
    , Vertex
m3
    )
rewritePred Vertex
_ (ForEach Term era Size
sz Term era fs
t Pat era t
tar [Pred era]
ps) =
  forall a. HasCallStack => String -> a
error (String
"Not a valid ForEach predicate " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era fs t.
(Era era, FromList fs t, Eq t) =>
Term era Size -> Term era fs -> Pat era t -> [Pred era] -> Pred era
ForEach Term era Size
sz Term era fs
t Pat era t
tar [Pred era]
ps))
rewritePred Vertex
m0 (Maybe (Var V era (Maybe t)
v) (RootTarget era r t
target :: (RootTarget era r t)) [Pred era]
preds) = do
  Vertex
count <- (Vertex, Vertex) -> Gen Vertex
chooseInt (Vertex
0, Vertex
1) -- 0 is Nothing, 1 is Just
  if Vertex
count forall a. Eq a => a -> a -> Bool
== Vertex
0
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure ([forall era t. V era t -> Term era t
Var V era (Maybe t)
v forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"(const Nothing)" (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era ()
UnitR ()))], Vertex
m0)
    else do
      let (Vertex
m1, SubItems era
subs) = forall era r t.
(Vertex, SubItems era)
-> RootTarget era r t -> (Vertex, SubItems era)
fresh (Vertex
m0, []) RootTarget era r t
target
          subst :: Subst era
subst = forall era. [SubItem era] -> Subst era
itemsToSubst SubItems era
subs
          target2 :: RootTarget era r t
target2 = forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
subst RootTarget era r t
target
          renamedPred :: [Pred era]
renamedPred = forall a b. (a -> b) -> [a] -> [b]
map (forall era. Subst era -> Pred era -> Pred era
substPred Subst era
subst) [Pred era]
preds
      ([Pred era]
expandedPred, Vertex
m2) <- forall era.
Era era =>
([Pred era], Vertex) -> [Pred era] -> Gen ([Pred era], Vertex)
removeExpandablePred ([], Vertex
m1) [Pred era]
renamedPred
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Pred era]
expandedPred forall a. [a] -> [a] -> [a]
++ [forall era t. V era t -> Term era t
Var V era (Maybe t)
v forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall root a b era.
String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert String
"Just" (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @r) forall a. a -> Maybe a
Just forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ RootTarget era r t
target2)], Vertex
m2)
rewritePred Vertex
m0 Pred era
p = forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Pred era
p], Vertex
m0)

removeExpandablePred :: Era era => ([Pred era], Int) -> [Pred era] -> Gen ([Pred era], Int)
removeExpandablePred :: forall era.
Era era =>
([Pred era], Vertex) -> [Pred era] -> Gen ([Pred era], Vertex)
removeExpandablePred ([Pred era]
ps, Vertex
m) [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. (a -> a -> Bool) -> [a] -> [a]
List.nubBy forall era. Era era => Pred era -> Pred era -> Bool
cpeq (forall a. [a] -> [a]
reverse [Pred era]
ps), Vertex
m)
removeExpandablePred ([Pred era]
ps, Vertex
m) (Pred era
p : [Pred era]
more) = do
  ([Pred era]
ps2, Vertex
m1) <- forall era.
Era era =>
Vertex -> Pred era -> Gen ([Pred era], Vertex)
rewritePred Vertex
m Pred era
p
  forall era.
Era era =>
([Pred era], Vertex) -> [Pred era] -> Gen ([Pred era], Vertex)
removeExpandablePred ([Pred era]
ps2 forall a. [a] -> [a] -> [a]
++ [Pred era]
ps, Vertex
m1) [Pred era]
more

removeMetaSize :: Era era => [Pred era] -> [Pred era] -> Gen [Pred era]
removeMetaSize :: forall era. Era era => [Pred era] -> [Pred era] -> Gen [Pred era]
removeMetaSize [] [Pred era]
ans = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [Pred era]
ans
removeMetaSize ((MetaSize Size
sz t :: Term era Size
t@(Var V era Size
v)) : [Pred era]
more) [Pred era]
ans = do
  Vertex
n <- Size -> Gen Vertex
genFromSize Size
sz
  let sub :: Pred era -> Pred era
sub = forall era. Subst era -> Pred era -> Pred era
substPred (forall era t. V era t -> Term era t -> Subst era
singleSubst V era Size
v (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Size
SizeR (Vertex -> Size
SzExact Vertex
n)))
  forall era. Era era => [Pred era] -> [Pred era] -> Gen [Pred era]
removeMetaSize (forall a b. (a -> b) -> [a] -> [b]
map Pred era -> Pred era
sub [Pred era]
more) ((Term era Size
t forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era t. Term era t -> RootTarget era Void t
Simple (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Size
SizeR (Vertex -> Size
SzExact Vertex
n))) forall a. a -> [a] -> [a]
: (forall a b. (a -> b) -> [a] -> [b]
map Pred era -> Pred era
sub [Pred era]
ans))
removeMetaSize (Pred era
m : [Pred era]
more) [Pred era]
ans = forall era. Era era => [Pred era] -> [Pred era] -> Gen [Pred era]
removeMetaSize [Pred era]
more (Pred era
m forall a. a -> [a] -> [a]
: [Pred era]
ans)

rewriteGen :: Era era => (Int, [Pred era]) -> Gen (Int, [Pred era])
rewriteGen :: forall era.
Era era =>
(Vertex, [Pred era]) -> Gen (Vertex, [Pred era])
rewriteGen (Vertex
m, [Pred era]
cs0) = do
  [Pred era]
cs1 <- forall era. Era era => [Pred era] -> [Pred era] -> Gen [Pred era]
removeMetaSize [Pred era]
cs0 []
  ([Pred era]
cs2, Vertex
m1) <- forall era.
Era era =>
([Pred era], Vertex) -> [Pred era] -> Gen ([Pred era], Vertex)
removeExpandablePred ([], Vertex
m) [Pred era]
cs1
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Vertex
m1, forall era. Era era => [Pred era] -> [Pred era]
removeTrivial forall a b. (a -> b) -> a -> b
$ forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeSameVar (forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeEqual [Pred era]
cs2 []) [])

notBefore :: Pred era -> Bool
notBefore :: forall era. Pred era -> Bool
notBefore (Before Term era a
_ Term era b
_) = Bool
False
notBefore Pred era
_ = Bool
True

-- | Construct the DependGraph
compileGenWithSubst :: Era era => OrderInfo -> Subst era -> [Pred era] -> Gen (Int, DependGraph era)
compileGenWithSubst :: forall era.
Era era =>
OrderInfo
-> Subst era -> [Pred era] -> Gen (Vertex, DependGraph era)
compileGenWithSubst OrderInfo
info Subst era
subst0 [Pred era]
cs = do
  (Vertex
m, [Pred era]
simple) <- forall era.
Era era =>
(Vertex, [Pred era]) -> Gen (Vertex, [Pred era])
rewriteGen (Vertex
0, [Pred era]
cs)
  let instanSimple :: [Pred era]
instanSimple = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall era. Subst era -> Pred era -> Pred era
substPredWithVarTest Subst era
subst0) [Pred era]
simple
  DependGraph era
graph <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ do
    [Name era]
orderedNames <- forall era. Era era => OrderInfo -> [Pred era] -> Typed [Name era]
initialOrder OrderInfo
info [Pred era]
instanSimple
    forall era.
Era era =>
Vertex
-> [([Name era], [Pred era])]
-> HashSet (Name era)
-> [Name era]
-> [Name era]
-> [Pred era]
-> Typed (DependGraph era)
mkDependGraph (forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [Name era]
orderedNames) [] forall a. HashSet a
HashSet.empty [Name era]
orderedNames [] (forall a. (a -> Bool) -> [a] -> [a]
filter forall era. Pred era -> Bool
notBefore [Pred era]
instanSimple)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Vertex
m, DependGraph era
graph)

-- ==============================================================
-- Build a Dependency Graph that extracts an ordering on the
-- variables in the [Pred] we are trying to solve. The idea is that
-- solving for for a [Pred] will be easier if it contains only
-- one variable, and all other Terms are constants (Fixed (Lit rep x))

-- | An Ordering
newtype DependGraph era = DependGraph [([Name era], [Pred era])]

instance Era era => Show (DependGraph era) where
  show :: DependGraph era -> String
show (DependGraph [([Name era], [Pred era])]
xs) = [String] -> String
unlines (forall a b. (a -> b) -> [a] -> [b]
map ([Name era], [Pred era]) -> String
f [([Name era], [Pred era])]
xs)
    where
      f :: ([Name era], [Pred era]) -> String
f ([Name era]
nm, [Pred era]
cs) = Vertex -> ShowS
pad Vertex
n (forall t. (t -> String) -> String -> [t] -> String
showL Name era -> String
shName String
" " [Name era]
nm) forall a. [a] -> [a] -> [a]
++ String
" | " forall a. [a] -> [a] -> [a]
++ forall t. (t -> String) -> String -> [t] -> String
showL forall a. Show a => a -> String
show String
", " [Pred era]
cs
      n :: Vertex
n = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (forall a b. (a -> b) -> [a] -> [b]
map (forall (t :: * -> *) a. Foldable t => t a -> Vertex
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall t. (t -> String) -> String -> [t] -> String
showL Name era -> String
shName String
" ") forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [([Name era], [Pred era])]
xs) forall a. Num a => a -> a -> a
+ Vertex
2
      shName :: Name era -> String
      shName :: Name era -> String
shName (Name (V String
v Rep era t
_ Access era s t
_)) = String
v

-- =========================================================
-- Sketch of algorithm for creating a DependGraph
--
-- for every pair (name,[cond]) the variables of [cond] only contain name, and names
-- defined in previous pairs in the DependGraph. Can we find such an order?
-- To compute this from a [Pred era] we implement this algorithm
-- try prev choices constraints =
--   (c,more) <- pick choices
--   possible <- filter (only mentions (c:prev)) constraints
--   if null possible
--      then try prev (more ++ [(c,possible)]) constraints
--      else possible ++ try (c:prev) more (constraints - possible)
--
-- ===================================================================
-- Find an order to solve the variables in

-- | Three possible cases
-- 1) Many predicates that define the same Name
-- 2) One predicate that defines many Names
-- 3) Some other bad combination
splitMultiName ::
  Era era =>
  Name era ->
  [([Name era], Pred era)] ->
  ([Pred era], Maybe ([Name era], Pred era), [String]) ->
  ([Pred era], Maybe ([Name era], Pred era), [String])
splitMultiName :: forall era.
Era era =>
Name era
-> [([Name era], Pred era)]
-> ([Pred era], Maybe ([Name era], Pred era), [String])
-> ([Pred era], Maybe ([Name era], Pred era), [String])
splitMultiName Name era
_ [] ([Pred era]
unary, Maybe ([Name era], Pred era)
nary, [String]
bad) = ([Pred era]
unary, Maybe ([Name era], Pred era)
nary, [String]
bad)
splitMultiName n :: Name era
n@(Name V era t
vn) (([m :: Name era
m@(Name V era t
vm)], Pred era
p) : [([Name era], Pred era)]
more) ([Pred era]
unary, Maybe ([Name era], Pred era)
nary, [String]
bad) =
  if Name era
n forall a. Eq a => a -> a -> Bool
== Name era
m
    then forall era.
Era era =>
Name era
-> [([Name era], Pred era)]
-> ([Pred era], Maybe ([Name era], Pred era), [String])
-> ([Pred era], Maybe ([Name era], Pred era), [String])
splitMultiName Name era
n [([Name era], Pred era)]
more (Pred era
p forall a. a -> [a] -> [a]
: [Pred era]
unary, Maybe ([Name era], Pred era)
nary, [String]
bad)
    else
      forall era.
Era era =>
Name era
-> [([Name era], Pred era)]
-> ([Pred era], Maybe ([Name era], Pred era), [String])
-> ([Pred era], Maybe ([Name era], Pred era), [String])
splitMultiName
        Name era
n
        [([Name era], Pred era)]
more
        ( [Pred era]
unary
        , Maybe ([Name era], Pred era)
nary
        , ( String
"A unary MultiName "
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show V era t
vm
              forall a. [a] -> [a] -> [a]
++ String
" does not match the search name "
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show V era t
vn
              forall a. [a] -> [a] -> [a]
++ String
" "
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred era
p
          )
            forall a. a -> [a] -> [a]
: [String]
bad
        )
splitMultiName Name era
n (([Name era]
ms, Pred era
p) : [([Name era], Pred era)]
more) ([Pred era]
unary, Maybe ([Name era], Pred era)
Nothing, [String]
bad) =
  if forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Name era
n [Name era]
ms
    then forall era.
Era era =>
Name era
-> [([Name era], Pred era)]
-> ([Pred era], Maybe ([Name era], Pred era), [String])
-> ([Pred era], Maybe ([Name era], Pred era), [String])
splitMultiName Name era
n [([Name era], Pred era)]
more ([Pred era]
unary, forall a. a -> Maybe a
Just ([Name era]
ms, Pred era
p), [String]
bad)
    else
      forall era.
Era era =>
Name era
-> [([Name era], Pred era)]
-> ([Pred era], Maybe ([Name era], Pred era), [String])
-> ([Pred era], Maybe ([Name era], Pred era), [String])
splitMultiName
        Name era
n
        [([Name era], Pred era)]
more
        ( [Pred era]
unary
        , forall a. Maybe a
Nothing
        , (String
"A set of nary Multinames " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name era]
ms forall a. [a] -> [a] -> [a]
++ String
" does not contain the search name " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name era
n) forall a. a -> [a] -> [a]
: [String]
bad
        )
splitMultiName Name era
n (([Name era]
ms, Pred era
p) : [([Name era], Pred era)]
more) ([Pred era]
unary, Just ([Name era], Pred era)
first, [String]
bad) =
  forall era.
Era era =>
Name era
-> [([Name era], Pred era)]
-> ([Pred era], Maybe ([Name era], Pred era), [String])
-> ([Pred era], Maybe ([Name era], Pred era), [String])
splitMultiName
    Name era
n
    [([Name era], Pred era)]
more
    ([Pred era]
unary, forall a. a -> Maybe a
Just ([Name era], Pred era)
first, (String
"More than one Multiname: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ([Name era], Pred era)
first forall a. [a] -> [a] -> [a]
++ String
" and " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ([Name era]
ms, Pred era
p)) forall a. a -> [a] -> [a]
: [String]
bad)

mkDependGraph ::
  forall era.
  Era era =>
  Int ->
  [([Name era], [Pred era])] ->
  HashSet (Name era) ->
  [Name era] ->
  [Name era] ->
  [Pred era] ->
  Typed (DependGraph era)
mkDependGraph :: forall era.
Era era =>
Vertex
-> [([Name era], [Pred era])]
-> HashSet (Name era)
-> [Name era]
-> [Name era]
-> [Pred era]
-> Typed (DependGraph era)
mkDependGraph Vertex
_ [([Name era], [Pred era])]
prev HashSet (Name era)
_ [Name era]
_ [Name era]
_ [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era. [([Name era], [Pred era])] -> DependGraph era
DependGraph (forall a. [a] -> [a]
reverse [([Name era], [Pred era])]
prev))
mkDependGraph Vertex
count [([Name era], [Pred era])]
prev HashSet (Name era)
_ [Name era]
choices [Name era]
badchoices [Pred era]
specs
  | Vertex
count forall a. Ord a => a -> a -> Bool
<= Vertex
0 =
      forall a. [String] -> Typed a
failT
        [ String
"\nFailed to find an Ordering of variables to solve for.\nHandled Constraints\n"
        , forall a. Show a => a -> String
show (forall era. [([Name era], [Pred era])] -> DependGraph era
DependGraph (forall a. [a] -> [a]
reverse [([Name era], [Pred era])]
prev))
        , String
"\n  vars to be processed"
        , forall a. Show a => a -> String
show [Name era]
choices
        , String
"\n  vars bad "
        , forall a. Show a => a -> String
show [Name era]
badchoices
        , String
"\n  Still to be processed\n"
        , [String] -> String
unlines (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Pred era]
specs)
        ]
mkDependGraph Vertex
count [([Name era], [Pred era])]
prev HashSet (Name era)
prevNames [] [Name era]
badchoices [Pred era]
cs = forall era.
Era era =>
Vertex
-> [([Name era], [Pred era])]
-> HashSet (Name era)
-> [Name era]
-> [Name era]
-> [Pred era]
-> Typed (DependGraph era)
mkDependGraph (Vertex
count forall a. Num a => a -> a -> a
- Vertex
1) [([Name era], [Pred era])]
prev HashSet (Name era)
prevNames (forall a. [a] -> [a]
reverse [Name era]
badchoices) [] [Pred era]
cs
mkDependGraph Vertex
count [([Name era], [Pred era])]
prev HashSet (Name era)
prevNames (Name era
n : [Name era]
more) [Name era]
badchoices [Pred era]
cs =
  case forall a b. (a -> Either b a) -> [a] -> ([b], [a])
partitionE Pred era -> Either ([Name era], Pred era) (Pred era)
okE [Pred era]
cs of
    ([], [Pred era]
_) -> forall era.
Era era =>
Vertex
-> [([Name era], [Pred era])]
-> HashSet (Name era)
-> [Name era]
-> [Name era]
-> [Pred era]
-> Typed (DependGraph era)
mkDependGraph Vertex
count [([Name era], [Pred era])]
prev HashSet (Name era)
prevNames [Name era]
more (Name era
n forall a. a -> [a] -> [a]
: [Name era]
badchoices) [Pred era]
cs
    ([([Name era], Pred era)]
possible, [Pred era]
notPossible) -> case forall era.
Era era =>
Name era
-> [([Name era], Pred era)]
-> ([Pred era], Maybe ([Name era], Pred era), [String])
-> ([Pred era], Maybe ([Name era], Pred era), [String])
splitMultiName Name era
n [([Name era], Pred era)]
possible ([], forall a. Maybe a
Nothing, []) of
      ([Pred era]
ps, Maybe ([Name era], Pred era)
Nothing, []) ->
        forall era.
Era era =>
Vertex
-> [([Name era], [Pred era])]
-> HashSet (Name era)
-> [Name era]
-> [Name era]
-> [Pred era]
-> Typed (DependGraph era)
mkDependGraph
          Vertex
count
          (([Name era
n], [Pred era]
ps) forall a. a -> [a] -> [a]
: [([Name era], [Pred era])]
prev)
          (forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert Name era
n HashSet (Name era)
prevNames)
          (forall a. [a] -> [a]
reverse [Name era]
badchoices forall a. [a] -> [a] -> [a]
++ [Name era]
more)
          []
          [Pred era]
notPossible
      ([], Just ([Name era]
ns, Pred era
p), []) ->
        forall era.
Era era =>
Vertex
-> [([Name era], [Pred era])]
-> HashSet (Name era)
-> [Name era]
-> [Name era]
-> [Pred era]
-> Typed (DependGraph era)
mkDependGraph
          Vertex
count
          (([Name era]
ns, [Pred era
p]) forall a. a -> [a] -> [a]
: [([Name era], [Pred era])]
prev)
          (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]
ns) HashSet (Name era)
prevNames)
          (forall a. [a] -> [a]
reverse [Name era]
badchoices forall a. [a] -> [a] -> [a]
++ [Name era]
more)
          []
          [Pred era]
notPossible
      ([Pred era]
unary, Maybe ([Name era], Pred era)
binary, [String]
bad) ->
        forall a. HasCallStack => String -> a
error
          ( String
"SOMETHING IS WRONG in partionE \nunary = "
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Pred era]
unary
              forall a. [a] -> [a] -> [a]
++ String
"\nbinary = "
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Maybe ([Name era], Pred era)
binary
              forall a. [a] -> [a] -> [a]
++ String
"\nbad = "
              forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines [String]
bad
          )
  where
    !defined :: HashSet (Name era)
defined = forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert Name era
n HashSet (Name era)
prevNames
    okE :: Pred era -> Either ([Name era], Pred era) (Pred era)
    okE :: Pred era -> Either ([Name era], Pred era) (Pred era)
okE p :: Pred era
p@(SumSplit c
_ Term era c
t OrdCond
_ [Sum era c]
ns) =
      let rhsNames :: HashSet (Name era)
rhsNames = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era r. HashSet (Name era) -> Sum era r -> HashSet (Name era)
varsOfSum forall a. HashSet a
HashSet.empty [Sum era c]
ns
       in if forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> Bool
HashSet.isSubsetOf (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm forall a. HashSet a
HashSet.empty Term era c
t) HashSet (Name era)
prevNames
            Bool -> Bool -> Bool
&& forall a. Hashable a => HashSet a -> HashSet a -> Bool
hashSetDisjoint HashSet (Name era)
prevNames HashSet (Name era)
rhsNames
            Bool -> Bool -> Bool
&& forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member Name era
n HashSet (Name era)
rhsNames
            then forall a b. a -> Either a b
Left (forall a. HashSet a -> [a]
HashSet.toList HashSet (Name era)
rhsNames, Pred era
p)
            else forall a b. b -> Either a b
Right Pred era
p
    okE Pred era
constraint =
      if forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> Bool
HashSet.isSubsetOf (forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred forall a. HashSet a
HashSet.empty Pred era
constraint) HashSet (Name era)
defined
        then forall a b. a -> Either a b
Left ([Name era
n], Pred era
constraint)
        else forall a b. b -> Either a b
Right Pred era
constraint

partitionE :: (a -> Either b a) -> [a] -> ([b], [a])
partitionE :: forall a b. (a -> Either b a) -> [a] -> ([b], [a])
partitionE a -> Either b a
_ [] = ([], [])
partitionE a -> Either b a
f (a
x : [a]
xs) = case (a -> Either b a
f a
x, forall a b. (a -> Either b a) -> [a] -> ([b], [a])
partitionE a -> Either b a
f [a]
xs) of
  (Left b
b, ([b]
bs, [a]
as)) -> (b
b forall a. a -> [a] -> [a]
: [b]
bs, [a]
as)
  (Right a
a, ([b]
bs, [a]
as)) -> ([b]
bs, a
a forall a. a -> [a] -> [a]
: [a]
as)

_firstE :: (a -> Either b a) -> [a] -> (Maybe b, [a])
_firstE :: forall a b. (a -> Either b a) -> [a] -> (Maybe b, [a])
_firstE a -> Either b a
_ [] = (forall a. Maybe a
Nothing, [])
_firstE a -> Either b a
f (a
x : [a]
xs) = case a -> Either b a
f a
x of
  Left b
b -> (forall a. a -> Maybe a
Just b
b, [a]
xs)
  Right a
a -> case forall a b. (a -> Either b a) -> [a] -> (Maybe b, [a])
_firstE a -> Either b a
f [a]
xs of
    (Maybe b
Nothing, [a]
as) -> (forall a. Maybe a
Nothing, a
a forall a. a -> [a] -> [a]
: [a]
as)
    (Just b
b, [a]
as) -> (forall a. a -> Maybe a
Just b
b, a
a forall a. a -> [a] -> [a]
: [a]
as)

-- ============================================================
-- Create a Graph from which we can extract a DependGraph

-- | Add to the dependency map 'answer' constraints such that every Name in 'before'
--   preceeds every Name in 'after' in the order in which Names are solved for.
mkDeps ::
  HashSet (Name era) ->
  HashSet (Name era) ->
  Map (Name era) (HashSet (Name era)) ->
  Map (Name era) (HashSet (Name era))
mkDeps :: forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps HashSet (Name era)
before HashSet (Name era)
after Map (Name era) (HashSet (Name era))
answer = forall a b. (a -> b -> a) -> a -> HashSet b -> a
HashSet.foldl' Map (Name era) (HashSet (Name era))
-> Name era -> Map (Name era) (HashSet (Name era))
accum Map (Name era) (HashSet (Name era))
answer HashSet (Name era)
after
  where
    accum :: Map (Name era) (HashSet (Name era))
-> Name era -> Map (Name era) (HashSet (Name era))
accum Map (Name era) (HashSet (Name era))
ans Name era
left = forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.union) Name era
left HashSet (Name era)
before Map (Name era) (HashSet (Name era))
ans

data OrderInfo = OrderInfo
  { OrderInfo -> Bool
sumBeforeParts :: Bool
  , OrderInfo -> Bool
sizeBeforeArg :: Bool
  , OrderInfo -> Bool
setBeforeSubset :: Bool
  }
  deriving (Vertex -> OrderInfo -> ShowS
[OrderInfo] -> ShowS
OrderInfo -> String
forall a.
(Vertex -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OrderInfo] -> ShowS
$cshowList :: [OrderInfo] -> ShowS
show :: OrderInfo -> String
$cshow :: OrderInfo -> String
showsPrec :: Vertex -> OrderInfo -> ShowS
$cshowsPrec :: Vertex -> OrderInfo -> ShowS
Show, OrderInfo -> OrderInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OrderInfo -> OrderInfo -> Bool
$c/= :: OrderInfo -> OrderInfo -> Bool
== :: OrderInfo -> OrderInfo -> Bool
$c== :: OrderInfo -> OrderInfo -> Bool
Eq)

standardOrderInfo :: OrderInfo
standardOrderInfo :: OrderInfo
standardOrderInfo =
  OrderInfo
    { sumBeforeParts :: Bool
sumBeforeParts = Bool
False
    , sizeBeforeArg :: Bool
sizeBeforeArg = Bool
True
    , setBeforeSubset :: Bool
setBeforeSubset = Bool
True
    }

accumdep ::
  Era era =>
  OrderInfo ->
  Map (Name era) (HashSet (Name era)) ->
  Pred era ->
  Map (Name era) (HashSet (Name era))
accumdep :: forall era.
Era era =>
OrderInfo
-> Map (Name era) (HashSet (Name era))
-> Pred era
-> Map (Name era) (HashSet (Name era))
accumdep OrderInfo
info Map (Name era) (HashSet (Name era))
answer Pred era
c = case Pred era
c of
  Term era (Set a)
sub :⊆: Term era (Set a)
set ->
    if OrderInfo -> Bool
setBeforeSubset OrderInfo
info
      then forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era (Set a)
set) (forall era t. Term era t -> HashSet (Name era)
vars Term era (Set a)
sub) Map (Name era) (HashSet (Name era))
answer
      else forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era (Set a)
sub) (forall era t. Term era t -> HashSet (Name era)
vars Term era (Set a)
set) Map (Name era) (HashSet (Name era))
answer
  Term era a
lhs :=: Term era a
rhs -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era a
lhs) (forall era t. Term era t -> HashSet (Name era)
vars Term era a
rhs) Map (Name era) (HashSet (Name era))
answer
  Disjoint Term era (Set a)
left Term era (Set a)
right -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era (Set a)
left) (forall era t. Term era t -> HashSet (Name era)
vars Term era (Set a)
right) Map (Name era) (HashSet (Name era))
answer
  Sized Term era Size
size Term era t
argx ->
    if OrderInfo -> Bool
sizeBeforeArg OrderInfo
info
      then forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era Size
size) (forall era t. Term era t -> HashSet (Name era)
vars Term era t
argx) Map (Name era) (HashSet (Name era))
answer
      else forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era t
argx) (forall era t. Term era t -> HashSet (Name era)
vars Term era Size
size) Map (Name era) (HashSet (Name era))
answer
  SumsTo (Left c
_) Term era c
sm OrdCond
_ [Sum era c]
parts -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era c
sm) (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era r. HashSet (Name era) -> Sum era r -> HashSet (Name era)
varsOfSum forall a. HashSet a
HashSet.empty [Sum era c]
parts) Map (Name era) (HashSet (Name era))
answer
  SumsTo (Right c
_) Term era c
sm OrdCond
_ [Sum era c]
parts -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era r. HashSet (Name era) -> Sum era r -> HashSet (Name era)
varsOfSum forall a. HashSet a
HashSet.empty [Sum era c]
parts) (forall era t. Term era t -> HashSet (Name era)
vars Term era c
sm) Map (Name era) (HashSet (Name era))
answer
  SumSplit c
_ Term era c
sm OrdCond
_ [Sum era c]
parts -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era c
sm) (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era r. HashSet (Name era) -> Sum era r -> HashSet (Name era)
varsOfSum forall a. HashSet a
HashSet.empty [Sum era c]
parts) Map (Name era) (HashSet (Name era))
answer
  Component (Right Term era t
t) [AnyF era t]
cs -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era s. [AnyF era s] -> HashSet (Name era)
componentVars [AnyF era t]
cs) (forall era t. Term era t -> HashSet (Name era)
vars Term era t
t) Map (Name era) (HashSet (Name era))
answer
  Component (Left Term era t
t) [AnyF era t]
cs -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era t
t) (forall era s. [AnyF era s] -> HashSet (Name era)
componentVars [AnyF era t]
cs) Map (Name era) (HashSet (Name era))
answer
  Member (Left Term era a
t) Term era (Set a)
cs -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era a
t) (forall era t. Term era t -> HashSet (Name era)
vars Term era (Set a)
cs) Map (Name era) (HashSet (Name era))
answer
  Member (Right Term era a
t) Term era (Set a)
cs -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era (Set a)
cs) (forall era t. Term era t -> HashSet (Name era)
vars Term era a
t) Map (Name era) (HashSet (Name era))
answer
  NotMember Term era a
t Term era (Set a)
cs -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era a
t) (forall era t. Term era t -> HashSet (Name era)
vars Term era (Set a)
cs) Map (Name era) (HashSet (Name era))
answer
  MapMember Term era k
k Term era v
v (Left Term era (Map k v)
m) -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era v
v) (forall era t. Term era t -> HashSet (Name era)
vars Term era k
k) (forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era k
k) (forall era t. Term era t -> HashSet (Name era)
vars Term era (Map k v)
m) Map (Name era) (HashSet (Name era))
answer)
  MapMember Term era k
k Term era v
v (Right Term era (Map k v)
m) -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era (Map k v)
m) (forall era t. Term era t -> HashSet (Name era)
vars Term era k
k) (forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era k
k) (forall era t. Term era t -> HashSet (Name era)
vars Term era v
v) Map (Name era) (HashSet (Name era))
answer)
  Term era t
t :<-: RootTarget era r t
ts -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget forall a. HashSet a
HashSet.empty RootTarget era r t
ts) (forall era t. Term era t -> HashSet (Name era)
vars Term era t
t) Map (Name era) (HashSet (Name era))
answer
  GenFrom Term era t
t RootTarget era r (Gen t)
ts -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget forall a. HashSet a
HashSet.empty RootTarget era r (Gen t)
ts) (forall era t. Term era t -> HashSet (Name era)
vars Term era t
t) Map (Name era) (HashSet (Name era))
answer
  List Term era fs
t [Term era t]
cs -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm forall a. HashSet a
HashSet.empty [Term era t]
cs) (forall era t. Term era t -> HashSet (Name era)
vars Term era fs
t) Map (Name era) (HashSet (Name era))
answer
  Maybe Term era (Maybe t)
t RootTarget era r t
target [Pred era]
ps -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era (Maybe t)
t) (forall era r t2.
Era era =>
HashSet (Name era)
-> [(RootTarget era r t2, [Pred era])] -> HashSet (Name era)
varsOfPairs forall a. HashSet a
HashSet.empty [(RootTarget era r t
target, [Pred era]
ps)]) Map (Name era) (HashSet (Name era))
answer
  ForEach Term era Size
sz Term era fs
x Pat era t
pat [Pred era]
ps ->
    forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps
      (forall era t. Term era t -> HashSet (Name era)
vars Term era Size
sz)
      (forall era t. Term era t -> HashSet (Name era)
vars Term era fs
x)
      (forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era fs
x) (forall era t2.
Era era =>
HashSet (Name era)
-> [(Pat era t2, [Pred era])] -> HashSet (Name era)
varsOfPats forall a. HashSet a
HashSet.empty [(Pat era t
pat, [Pred era]
ps)]) Map (Name era) (HashSet (Name era))
answer)
  ListWhere Term era Size
sz Term era [t]
x RootTarget era t t
tar [Pred era]
ps ->
    forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps
      (forall era t. Term era t -> HashSet (Name era)
vars Term era Size
sz)
      (forall era t. Term era t -> HashSet (Name era)
vars Term era [t]
x)
      (forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era [t]
x) (forall era r t2.
Era era =>
HashSet (Name era)
-> [(RootTarget era r t2, [Pred era])] -> HashSet (Name era)
varsOfPairs forall a. HashSet a
HashSet.empty [(RootTarget era t t
tar, [Pred era]
ps)]) Map (Name era) (HashSet (Name era))
answer)
  Choose Term era Size
sz Term era [t]
x [(Vertex, Target era t, [Pred era])]
xs ->
    forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era Size
sz) (forall era t. Term era t -> HashSet (Name era)
vars Term era [t]
x) (forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era [t]
x) (forall era r t2.
Era era =>
HashSet (Name era)
-> [(Vertex, RootTarget era r t2, [Pred era])]
-> HashSet (Name era)
varsOfTrips forall a. HashSet a
HashSet.empty [(Vertex, Target era t, [Pred era])]
xs) Map (Name era) (HashSet (Name era))
answer)
  SubMap Term era (Map k v)
left Term era (Map k v)
right -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era (Map k v)
left) (forall era t. Term era t -> HashSet (Name era)
vars Term era (Map k v)
right) Map (Name era) (HashSet (Name era))
answer
  If RootTarget era r Bool
t Pred era
x Pred era
y ->
    ( forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps
        (forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget forall a. HashSet a
HashSet.empty RootTarget era r Bool
t)
        (forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred forall a. HashSet a
HashSet.empty Pred era
x)
        (forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget forall a. HashSet a
HashSet.empty RootTarget era r Bool
t) (forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred forall a. HashSet a
HashSet.empty Pred era
y) Map (Name era) (HashSet (Name era))
answer)
    )
  Before Term era a
x Term era b
y -> forall era.
HashSet (Name era)
-> HashSet (Name era)
-> Map (Name era) (HashSet (Name era))
-> Map (Name era) (HashSet (Name era))
mkDeps (forall era t. Term era t -> HashSet (Name era)
vars Term era a
x) (forall era t. Term era t -> HashSet (Name era)
vars Term era b
y) Map (Name era) (HashSet (Name era))
answer
  Pred era
other -> forall a b. (a -> b -> a) -> a -> HashSet b -> a
HashSet.foldl' forall {k} {a}.
(Ord k, Eq a) =>
Map k (HashSet a) -> k -> Map k (HashSet a)
accum Map (Name era) (HashSet (Name era))
answer (forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred forall a. HashSet a
HashSet.empty Pred era
other)
    where
      accum :: Map k (HashSet a) -> k -> Map k (HashSet a)
accum Map k (HashSet a)
ans k
v = forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.union) k
v forall a. HashSet a
HashSet.empty Map k (HashSet a)
ans

componentVars :: [AnyF era s] -> HashSet (Name era)
componentVars :: forall era s. [AnyF era s] -> HashSet (Name era)
componentVars [] = forall a. HashSet a
HashSet.empty
componentVars (AnyF (Field String
n Rep era t
r Rep era s
a Lens' s t
l) : [AnyF era s]
cs) = forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert (forall era t. V era t -> Name era
Name forall a b. (a -> b) -> a -> b
$ forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
n Rep era t
r (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era s
a Lens' s t
l)) forall a b. (a -> b) -> a -> b
$ forall era s. [AnyF era s] -> HashSet (Name era)
componentVars [AnyF era s]
cs
componentVars (AnyF (FConst Rep era t
_ t
_ Rep era s
_ Lens' s t
_) : [AnyF era s]
cs) = forall era s. [AnyF era s] -> HashSet (Name era)
componentVars [AnyF era s]
cs

-- =========================================================================
-- Create an initial Ordering. Build a Graph, then extract the Ordering

initialOrder :: forall era. Era era => OrderInfo -> [Pred era] -> Typed [Name era]
initialOrder :: forall era. Era era => OrderInfo -> [Pred era] -> Typed [Name era]
initialOrder OrderInfo
info [Pred era]
cs0 = do
  [Vertex]
mmm <- [SCC Vertex] -> Typed [Vertex]
flatOrError (forall key node. Ord key => [(node, key, [key])] -> [SCC node]
stronglyConnComp [(Vertex, Name era, [Name era])]
listDep)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Vertex -> Name era
getname [Vertex]
mmm
  where
    allvs :: HashSet (Name era)
allvs = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred forall a. HashSet a
HashSet.empty [Pred era]
cs0
    noDepMap :: Map (Name era) (HashSet (Name era))
noDepMap = forall a b. (a -> b -> a) -> a -> HashSet b -> a
HashSet.foldl' (\Map (Name era) (HashSet (Name era))
ans Name era
n -> forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name era
n forall a. HashSet a
HashSet.empty Map (Name era) (HashSet (Name era))
ans) forall k a. Map k a
Map.empty HashSet (Name era)
allvs
    mapDep :: Map (Name era) (HashSet (Name era))
mapDep = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (forall era.
Era era =>
OrderInfo
-> Map (Name era) (HashSet (Name era))
-> Pred era
-> Map (Name era) (HashSet (Name era))
accumdep OrderInfo
info) Map (Name era) (HashSet (Name era))
noDepMap [Pred era]
cs0
    listDep :: [(Vertex, Name era, [Name era])]
listDep = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Name era
x, HashSet (Name era)
m) Vertex
n -> (Vertex
n, Name era
x, forall a. HashSet a -> [a]
HashSet.toList HashSet (Name era)
m)) (forall k a. Map k a -> [(k, a)]
Map.toList Map (Name era) (HashSet (Name era))
mapDep) [Vertex
0 ..]
    (Graph
_graph1, Vertex -> (Vertex, Name era, [Name era])
nodeFun, Name era -> Maybe Vertex
_keyf) = forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Vertex -> (node, key, [key]), key -> Maybe Vertex)
graphFromEdges [(Vertex, Name era, [Name era])]
listDep
    getname :: Vertex -> Name era
    getname :: Vertex -> Name era
getname Vertex
x = Name era
n where (Vertex
_node, Name era
n, [Name era]
_children) = Vertex -> (Vertex, Name era, [Name era])
nodeFun Vertex
x
    flatOrError :: [SCC Vertex] -> Typed [Vertex]
flatOrError [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    flatOrError (AcyclicSCC Vertex
x : [SCC Vertex]
more) = (Vertex
x forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SCC Vertex] -> Typed [Vertex]
flatOrError [SCC Vertex]
more
    flatOrError (CyclicSCC [Vertex]
xs : [SCC Vertex]
_) = forall a. [String] -> Typed a
failT [String
message, forall a. Show a => a -> String
show OrderInfo
info, [String] -> String
unlines (forall a b. (a -> b) -> [a] -> [b]
map ((String
"  " forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) [Pred era]
usesNames)]
      where
        names :: [Name era]
names = forall a b. (a -> b) -> [a] -> [b]
map Vertex -> Name era
getname [Vertex]
xs
        namesSet :: Set (Name era)
namesSet = forall a. Ord a => [a] -> Set a
Set.fromList [Name era]
names
        usesNames :: [Pred era]
usesNames =
          [Pred era
pr | Pred era
pr <- [Pred era]
cs0, forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Name era)
namesSet) (forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred forall a. HashSet a
HashSet.empty Pred era
pr)]
        theCycle :: [String]
theCycle = case [Name era]
names of
          [] -> forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Name era]
names
          (Name era
x : [Name era]
_) -> forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show ([Name era]
names forall a. [a] -> [a] -> [a]
++ [Name era
x])
        message :: String
message = String
"Cycle in dependencies: " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
List.intercalate String
" <= " [String]
theCycle

-- | Construct the DependGraph
compile :: Era era => OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile :: forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile OrderInfo
info [Pred era]
cs = do
  let simple :: [Pred era]
simple = forall era. Era era => [Pred era] -> [Pred era]
rewrite [Pred era]
cs
  [Name era]
orderedNames <- forall era. Era era => OrderInfo -> [Pred era] -> Typed [Name era]
initialOrder OrderInfo
info [Pred era]
simple
  forall era.
Era era =>
Vertex
-> [([Name era], [Pred era])]
-> HashSet (Name era)
-> [Name era]
-> [Name era]
-> [Pred era]
-> Typed (DependGraph era)
mkDependGraph (forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [Name era]
orderedNames) [] forall a. HashSet a
HashSet.empty [Name era]
orderedNames [] (forall a. (a -> Bool) -> [a] -> [a]
filter forall era. Pred era -> Bool
notBefore [Pred era]
simple)

showGraph :: (Vertex -> String) -> Graph -> String
showGraph :: (Vertex -> String) -> Graph -> String
showGraph Vertex -> String
nameof Graph
g = [String] -> String
unlines (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show (forall a b. [a] -> [b] -> [(a, b)]
zip [String]
names (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Array Vertex [String]
zs)))
  where
    (Vertex
lo, Vertex
hi) = forall i e. Array i e -> (i, i)
A.bounds Graph
g
    names :: [String]
names = forall a b. (a -> b) -> [a] -> [b]
map Vertex -> String
nameof [Vertex
lo .. Vertex
hi]
    zs :: Array Vertex [String]
zs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a -> b) -> [a] -> [b]
map Vertex -> String
nameof) Graph
g