{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Test.Cardano.Ledger.Constrained.Solver where

import Cardano.Ledger.BaseTypes (EpochNo (EpochNo), SlotNo (..))
import Cardano.Ledger.Coin (Coin (..), DeltaCoin (..))
import Cardano.Ledger.Core (Era (..), hashScript)
import Cardano.Ledger.Plutus.Data (hashData)
import qualified Data.List as List
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Pulse (foldlM')
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Debug.Trace as Debug
import GHC.Stack (HasCallStack)
import Lens.Micro (Lens', (^.))
import qualified Lens.Micro as Lens
import Numeric.Natural (Natural)
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Classes (
  Adds (..),
  AddsSpec (..),
  Count (..),
  OrdCond (..),
  ScriptF (..),
  Sizeable (getSize),
  varOnLeft,
  varOnRight,
  varOnRightNeg,
  varOnRightSize,
 )
import Test.Cardano.Ledger.Constrained.Combinators (errorMess, genFromMap, itemFromSet, suchThatErr)
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Monad
import Test.Cardano.Ledger.Constrained.Rewrite (
  DependGraph (..),
  OrderInfo,
  compileGenWithSubst,
  cpeq,
 )
import Test.Cardano.Ledger.Constrained.Size (
  Size (..),
  genFromIntRange,
  genFromSize,
 )
import Test.Cardano.Ledger.Constrained.Spec (
  ElemSpec (..),
  ListSpec (..),
  MapSpec (..),
  PairSide (..),
  PairSpec (PairAny, PairSpec),
  RelSpec (..),
  RngSpec (..),
  SetSpec (..),
  genFromListSpec,
  genFromMapSpec,
  genFromSetSpec,
  mapSpec,
  relDisjoint,
  relEqual,
  relSubset,
  relSuperset,
  setSpec,
 )
import Test.Cardano.Ledger.Constrained.TypeRep (
  Rep (..),
  genRep,
  genSizedRep,
  hasEq,
  hasOrd,
  synopsis,
  testEql,
  (:~:) (Refl),
 )
import Test.Cardano.Ledger.Core.Arbitrary ()
import Test.Cardano.Ledger.Generic.Proof (Proof (..), Reflect (reify))
import Test.Cardano.Ledger.Shelley.Serialisation.EraIndepGenerators ()
import Test.QuickCheck hiding (Fixed, getSize, total)

-- ===================================================================================
-- This is testing file, and sometimes it pays for solver to explain what it is doing
-- especially if it fails on some known input. This way the solver can leave a trace
-- of what it is doing, and why.

ifTrace :: Bool -> String -> a -> a
ifTrace :: forall a. Bool -> String -> a -> a
ifTrace Bool
traceOn String
message a
a = case Bool
traceOn of
  Bool
True -> forall a. String -> a -> a
Debug.trace String
message a
a
  Bool
False -> a
a

-- ==================================================
-- Computing if a type has instances

-- ============ Adds ==============

-- | Is there an Adds instance for 't'
hasAdds :: Rep era t -> (s t) -> Typed (HasConstraint Adds (s t))
hasAdds :: forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Adds (s t))
hasAdds Rep era t
ExUnitsR s t
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (c :: * -> Constraint) t1 (s :: * -> *).
c t1 =>
s t1 -> HasConstraint c (s t1)
With s t
x
hasAdds Rep era t
Word64R s t
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (c :: * -> Constraint) t1 (s :: * -> *).
c t1 =>
s t1 -> HasConstraint c (s t1)
With s t
x
hasAdds Rep era t
IntR s t
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (c :: * -> Constraint) t1 (s :: * -> *).
c t1 =>
s t1 -> HasConstraint c (s t1)
With s t
x
hasAdds Rep era t
NaturalR s t
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (c :: * -> Constraint) t1 (s :: * -> *).
c t1 =>
s t1 -> HasConstraint c (s t1)
With s t
x
hasAdds Rep era t
RationalR s t
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (c :: * -> Constraint) t1 (s :: * -> *).
c t1 =>
s t1 -> HasConstraint c (s t1)
With s t
x
hasAdds Rep era t
CoinR s t
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (c :: * -> Constraint) t1 (s :: * -> *).
c t1 =>
s t1 -> HasConstraint c (s t1)
With s t
x
hasAdds Rep era t
DeltaCoinR s t
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (c :: * -> Constraint) t1 (s :: * -> *).
c t1 =>
s t1 -> HasConstraint c (s t1)
With s t
x
hasAdds Rep era t
r s t
_ = forall a. [String] -> Typed a
failT [forall a. Show a => a -> String
show Rep era t
r forall a. [a] -> [a] -> [a]
++ String
" does not have Adds instance."]

isAddsType :: forall era t. Rep era t -> Bool
isAddsType :: forall era t. Rep era t -> Bool
isAddsType Rep era t
rep = case forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Adds (s t))
hasAdds Rep era t
rep Rep era t
rep of
  (Typed (Right (With s t1
_))) -> Bool
True
  (Typed (Left [String]
_)) -> Bool
False

-- ============= Count ================

-- | Is there an Count instance for 't'
hasCount :: Rep era t -> s t -> Typed (HasConstraint Count (s t))
hasCount :: forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Count (s t))
hasCount Rep era t
IntR s t
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (c :: * -> Constraint) t1 (s :: * -> *).
c t1 =>
s t1 -> HasConstraint c (s t1)
With s t
x
hasCount (ProtVerR Proof era
_) s t
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (c :: * -> Constraint) t1 (s :: * -> *).
c t1 =>
s t1 -> HasConstraint c (s t1)
With s t
x
hasCount Rep era t
EpochR s t
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (c :: * -> Constraint) t1 (s :: * -> *).
c t1 =>
s t1 -> HasConstraint c (s t1)
With s t
x
hasCount Rep era t
SlotNoR s t
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (c :: * -> Constraint) t1 (s :: * -> *).
c t1 =>
s t1 -> HasConstraint c (s t1)
With s t
x
hasCount Rep era t
r s t
_ = forall a. [String] -> Typed a
failT [forall a. Show a => a -> String
show Rep era t
r forall a. [a] -> [a] -> [a]
++ String
" does not have Count instance."]

isCountType :: forall era t. Rep era t -> Bool
isCountType :: forall era t. Rep era t -> Bool
isCountType Rep era t
rep = case forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Count (s t))
hasCount Rep era t
rep Rep era t
rep of
  (Typed (Right (With s t1
_))) -> Bool
True
  (Typed (Left [String]
_)) -> Bool
False

-- ==================================================
-- Extras, simple helper functions

sameRep :: Rep era i -> Rep era j -> Typed (i :~: j)
sameRep :: forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era i
r1 Rep era j
r2 = case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql Rep era i
r1 Rep era j
r2 of
  Just i :~: j
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure i :~: j
x
  Maybe (i :~: j)
Nothing -> forall a. [String] -> Typed a
failT [String
"Type error in sameRep:\n  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era i
r1 forall a. [a] -> [a] -> [a]
++ String
" =/=\n  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era j
r2]

-- | Simplify and return with evidence that 'expr' has type 's'
simplifyAtType :: Era era => Rep era s -> Term era t -> Typed s
simplifyAtType :: forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era s
r1 Term era t
term = do
  t
t <- forall era t. Term era t -> Typed t
simplify Term era t
term
  s :~: t
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era s
r1 (forall era t. Era era => Term era t -> Rep era t
termRep Term era t
term)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure t
t

simplifySet ::
  (Ord rng, Era era) => Rep era rng -> Term era y -> Typed (HasConstraint Ord (Set rng))
simplifySet :: forall rng era y.
(Ord rng, Era era) =>
Rep era rng -> Term era y -> Typed (HasConstraint Ord (Set rng))
simplifySet Rep era rng
r1 Term era y
term = do
  y
x <- forall era t. Term era t -> Typed t
simplify Term era y
term
  Set rng :~: y
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era rng
r1) (forall era t. Era era => Term era t -> Rep era t
termRep Term era y
term)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (c :: * -> Constraint) t1 (s :: * -> *).
c t1 =>
s t1 -> HasConstraint c (s t1)
With y
x)

simplifyList :: Era era => Rep era rng -> Term era y -> Typed (HasConstraint Eq [rng])
simplifyList :: forall era rng y.
Era era =>
Rep era rng -> Term era y -> Typed (HasConstraint Eq [rng])
simplifyList Rep era rng
r1 Term era y
term = do
  y
x <- forall era t. Term era t -> Typed t
simplify Term era y
term
  [rng] :~: y
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep (forall era a. Rep era a -> Rep era [a]
ListR Rep era rng
r1) (forall era t. Era era => Term era t -> Rep era t
termRep Term era y
term)
  forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Eq (s t))
hasEq Rep era rng
r1 y
x

-- | Is the Sum a variable (of a map). Only SumMap and Project store maps.
isMapVar :: Name era -> Sum era c -> Bool
isMapVar :: forall era c. Name era -> Sum era c -> Bool
isMapVar Name era
n1 (SumMap (Var V era (Map a c)
v2)) = Name era
n1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a c)
v2
isMapVar Name era
n1 (ProjMap Rep era c
_ Lens' x c
_ (Var V era (Map a x)
v2)) = Name era
n1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a x)
v2
isMapVar Name era
n1 (SumList (Elems (Var V era (Map a b)
v2))) = Name era
n1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2
isMapVar Name era
_ Sum era c
_ = Bool
False

exactlyOne :: (a -> Bool) -> [a] -> Bool
exactlyOne :: forall a. (a -> Bool) -> [a] -> Bool
exactlyOne a -> Bool
pp [a]
xs = Int
1 forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter a -> Bool
pp [a]
xs)

-- | Make a generator for a Map type when there is a Projection from the domain of the map.
--   This has been superceeded by the RelLens  RelSpec
projOnDom ::
  forall era a dom rng.
  Ord dom =>
  Set a ->
  Lens' dom a ->
  Rep era dom ->
  Rep era rng ->
  Gen (Map dom rng)
projOnDom :: forall era a dom rng.
Ord dom =>
Set a
-> Lens' dom a -> Rep era dom -> Rep era rng -> Gen (Map dom rng)
projOnDom Set a
setA Lens' dom a
lensDomA Rep era dom
repDom Rep era rng
repRng = do
  [dom]
ds <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> Gen dom
genThenOverwriteA (forall a. Set a -> [a]
Set.toList Set a
setA)
  [(dom, rng)]
pairs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\dom
d -> do rng
r <- forall era b. Rep era b -> Gen b
genRep Rep era rng
repRng; forall (f :: * -> *) a. Applicative f => a -> f a
pure (dom
d, rng
r)) [dom]
ds
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(dom, rng)]
pairs)
  where
    genThenOverwriteA :: a -> Gen dom
genThenOverwriteA a
a = forall s t a b. ASetter s t a b -> b -> s -> t
Lens.set Lens' dom a
lensDomA a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era b. Rep era b -> Gen b
genRep Rep era dom
repDom

atLeast :: Adds c => Rep era c -> c -> Gen c
atLeast :: forall c era. Adds c => Rep era c -> c -> Gen c
atLeast Rep era c
rep c
c = forall x. Adds x => x -> x -> x
add c
c forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era b. Rep era b -> Gen b
genRep Rep era c
rep

-- ================================================================
-- Solver for variables of type (Map dom rng)
solveMap ::
  forall dom rng era. Era era => V era (Map dom rng) -> Pred era -> Typed (MapSpec era dom rng)
solveMap :: forall dom rng era.
Era era =>
V era (Map dom rng) -> Pred era -> Typed (MapSpec era dom rng)
solveMap v1 :: V era (Map dom rng)
v1@(V String
_ r :: Rep era (Map dom rng)
r@(MapR Rep era a
dom Rep era b
rng) Access era s (Map dom rng)
_) Pred era
predicate = forall a. String -> Typed a -> Typed a
explain String
msg forall a b. (a -> b) -> a -> b
$ case Pred era
predicate of
  (Before (Lit Rep era a
_ a
_) (Var V era b
v2)) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era b
v2 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
  (Sized (Lit Rep era Size
SizeR Size
sz) (Var V era t
v2))
    | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
sz forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (Sized (Lit Rep era Size
SizeR Size
sz) (Dom (Var V era (Map a b)
v2)))
    | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
sz forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (Var V era a
v2 :=: Term era a
expr) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era a
v2 -> do
    Map dom rng
m1 <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era (Map dom rng)
r Term era a
expr
    With s t1
_ <- forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Eq (s t))
hasEq Rep era b
rng Rep era b
rng
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
SzAny (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
dom (forall k a. Map k a -> Set k
Map.keysSet Map dom rng
m1)) forall era a b. PairSpec era a b
PairAny (forall rng era. Eq rng => Rep era rng -> [rng] -> RngSpec era rng
RngElem Rep era b
rng (forall k a. Map k a -> [a]
Map.elems Map dom rng
m1))
  (Term era a
expr :=: v2 :: Term era a
v2@(Var V era a
_)) -> forall dom rng era.
Era era =>
V era (Map dom rng) -> Pred era -> Typed (MapSpec era dom rng)
solveMap V era (Map dom rng)
v1 (Term era a
v2 forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era a
expr)
  (Elems (Var v2 :: V era (Map a b)
v2@(V String
_ Rep era (Map a b)
r2 Access era s (Map a b)
_)) :=: Term era a
expr) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    Map dom rng :~: Map a b
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era (Map dom rng)
r Rep era (Map a b)
r2
    [b]
l <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType (forall era a. Rep era a -> Rep era [a]
ListR Rep era b
rng) Term era a
expr
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzExact (forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
l)) forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny (forall rng era. Eq rng => Rep era rng -> [rng] -> RngSpec era rng
RngElem Rep era b
rng [b]
l)
  (Term era a
expr :=: Elems Term era (Map a b)
v2) -> forall dom rng era.
Era era =>
V era (Map dom rng) -> Pred era -> Typed (MapSpec era dom rng)
solveMap V era (Map dom rng)
v1 (forall a b era. (Ord a, Eq b) => Term era (Map a b) -> Term era [b]
Elems Term era (Map a b)
v2 forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era a
expr)
  (Term era a
expr1 :=: Restrict Term era (Set a)
expr2 (Var v2 :: V era (Map a b)
v2@(V String
_ (MapR Rep era a
a Rep era b
_) Access era s (Map a b)
_))) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
a Rep era a
dom
    a
val1 <- forall era t. Term era t -> Typed t
simplify Term era a
expr1
    Set a
val2 <- forall era t. Term era t -> Typed t
simplify Term era (Set a)
expr2
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzLeast (forall k a. Map k a -> Int
Map.size a
val1)) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
dom Set a
val2) forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (Restrict Term era (Set a)
expr1 Term era (Map a b)
expr2 :=: Term era a
expr3) -> forall dom rng era.
Era era =>
V era (Map dom rng) -> Pred era -> Typed (MapSpec era dom rng)
solveMap V era (Map dom rng)
v1 (Term era a
expr3 forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict Term era (Set a)
expr1 Term era (Map a b)
expr2)
  (ProjS Lens' b t1
lensbt Rep era t1
trep (Dom (Var v2 :: V era (Map a b)
v2@(V String
_ (MapR Rep era a
brep Rep era b
_) Access era s (Map a b)
_))) :=: Lit (SetR Rep era a
drep) a
x) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
brep
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzExact (forall a. Set a -> Int
Set.size a
x)) (forall b dom era.
Ord b =>
Lens' dom b
-> Rep era dom -> Rep era b -> RelSpec era b -> RelSpec era dom
RelLens Lens' b t1
lensbt Rep era a
dom Rep era t1
trep (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
drep a
x)) forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (ProjS Lens' b t1
lensbt Rep era t1
trep (Dom (Var v2 :: V era (Map a b)
v2@(V String
_ (MapR Rep era a
brep Rep era b
_) Access era s (Map a b)
_))) :=: Dom (Lit (MapR Rep era a
drep Rep era b
_) Map a b
x))
    | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
brep
        forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec
          (Int -> Size
SzExact (forall k a. Map k a -> Int
Map.size Map a b
x))
          (forall b dom era.
Ord b =>
Lens' dom b
-> Rep era dom -> Rep era b -> RelSpec era b -> RelSpec era dom
RelLens Lens' b t1
lensbt Rep era a
dom Rep era t1
trep (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
drep (forall k a. Map k a -> Set k
Map.keysSet Map a b
x)))
          forall era a b. PairSpec era a b
PairAny
          forall era rng. RngSpec era rng
RngAny
  (ProjS Lens' b t1
lensbt Rep era t1
trep (Dom (Var v2 :: V era (Map a b)
v2@(V String
_ (MapR Rep era a
brep Rep era b
_) Access era s (Map a b)
_))) `Subset` Dom (Lit (MapR Rep era a
drep Rep era b
_) Map a b
x))
    | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
brep
        forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec
          (Int -> Size
SzMost (forall k a. Map k a -> Int
Map.size Map a b
x))
          (forall b dom era.
Ord b =>
Lens' dom b
-> Rep era dom -> Rep era b -> RelSpec era b -> RelSpec era dom
RelLens Lens' b t1
lensbt Rep era a
dom Rep era t1
trep (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era a
drep (forall k a. Map k a -> Set k
Map.keysSet Map a b
x)))
          forall era a b. PairSpec era a b
PairAny
          forall era rng. RngSpec era rng
RngAny
  (Lit (SetR Rep era a
drep) a
x) :=: ProjS Lens' b t1
lensbt Rep era t1
trep (Dom (Var v2 :: V era (Map a b)
v2@(V String
_ (MapR Rep era a
brep Rep era b
_) Access era s (Map a b)
_))) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
brep
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzExact (forall a. Set a -> Int
Set.size a
x)) (forall b dom era.
Ord b =>
Lens' dom b
-> Rep era dom -> Rep era b -> RelSpec era b -> RelSpec era dom
RelLens Lens' b t1
lensbt Rep era a
dom Rep era t1
trep (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
drep a
x)) forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (Term era a
expr :=: Rng (Var V era (Map a b)
v2))
    | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        a
s <- forall era t. Term era t -> Typed t
simplify Term era a
expr
        let SetR Rep era b
Rep era a
a = forall era t. Era era => Term era t -> Rep era t
termRep Term era a
expr
        b :~: b
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
rng Rep era b
a
        forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzLeast (forall a. Set a -> Int
Set.size a
s)) forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny (forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era b
rng a
s))
  (Rng (Var V era (Map a b)
v2) :=: Term era a
expr)
    | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        a
s <- forall era t. Term era t -> Typed t
simplify Term era a
expr
        let SetR Rep era b
Rep era a
a = forall era t. Era era => Term era t -> Rep era t
termRep Term era a
expr
        b :~: b
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
rng Rep era b
a
        forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzLeast (forall a. Set a -> Int
Set.size a
s)) forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny (forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era b
rng a
s))
  (Rng (Var V era (Map a b)
v2) `Subset` Term era (Set a)
expr)
    | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        With s t1
_ <- forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Ord (s t))
hasOrd Rep era b
rng Rep era b
rng
        With s t1
n <- forall rng era y.
(Ord rng, Era era) =>
Rep era rng -> Term era y -> Typed (HasConstraint Ord (Set rng))
simplifySet Rep era b
rng Term era (Set a)
expr
        forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
SzAny forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny (forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era b
rng s t1
n))
  (Term era (Set a)
expr `Subset` Rng (Var V era (Map a b)
v2))
    | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        With s t1
_ <- forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Ord (s t))
hasOrd Rep era b
rng Rep era b
rng
        With s t1
n <- forall rng era y.
(Ord rng, Era era) =>
Rep era rng -> Term era y -> Typed (HasConstraint Ord (Set rng))
simplifySet Rep era b
rng Term era (Set a)
expr
        forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
SzAny forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny (forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era b
rng s t1
n))
  (Rng Term era (Map a b)
expr `Subset` (Var V era (Set a)
v2))
    | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
        With s t1
_ <- forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Ord (s t))
hasOrd Rep era b
rng Rep era b
rng
        With s t1
n <- forall rng era y.
(Ord rng, Era era) =>
Rep era rng -> Term era y -> Typed (HasConstraint Ord (Set rng))
simplifySet Rep era b
rng Term era (Map a b)
expr
        forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
SzAny forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny (forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era b
rng s t1
n))
  (Term era a
expr :=: Dom (Var V era (Map a b)
v2))
    | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        let SetR Rep era a
Rep era a
a = forall era t. Era era => Term era t -> Rep era t
termRep Term era a
expr
        a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
a
        a
mm <- forall era t. Term era t -> Typed t
simplify Term era a
expr
        forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzExact (forall a. Set a -> Int
Set.size a
mm)) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era a
dom a
mm) forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (Dom (Var V era (Map a b)
v2) :=: Term era a
expr)
    | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        let SetR Rep era a
Rep era a
a = forall era t. Era era => Term era t -> Rep era t
termRep Term era a
expr
        a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
a
        a
mm <- forall era t. Term era t -> Typed t
simplify Term era a
expr
        forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzExact (forall a. Set a -> Int
Set.size a
mm)) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era a
dom a
mm) forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (Dom (Var V era (Map a b)
v2) `Subset` Term era (Set a)
expr)
    | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        With s t1
_ <- forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Ord (s t))
hasOrd Rep era a
dom Rep era a
dom
        With s t1
n <- forall rng era y.
(Ord rng, Era era) =>
Rep era rng -> Term era y -> Typed (HasConstraint Ord (Set rng))
simplifySet Rep era a
dom Term era (Set a)
expr
        forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzMost (forall a. Set a -> Int
Set.size s t1
n)) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era a
dom s t1
n) forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (Term era (Set a)
expr `Subset` Dom (Var V era (Map a b)
v2))
    | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        With s t1
_ <- forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Ord (s t))
hasOrd Rep era a
dom Rep era a
dom
        With s t1
n <- forall rng era y.
(Ord rng, Era era) =>
Rep era rng -> Term era y -> Typed (HasConstraint Ord (Set rng))
simplifySet Rep era a
dom Term era (Set a)
expr
        forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzLeast (forall a. Set a -> Int
Set.size s t1
n)) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
dom s t1
n) forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (SumsTo Direct c
small Term era c
expr OrdCond
cond [Sum era c]
xs) | forall a. (a -> Bool) -> [a] -> Bool
exactlyOne (forall era c. Name era -> Sum era c -> Bool
isMapVar (forall era t. V era t -> Name era
Name V era (Map dom rng)
v1)) [Sum era c]
xs -> do
    c
t <- forall era t. Term era t -> Typed t
simplify Term era c
expr
    RngSpec era rng
rngspec <- forall era c dom rng.
(Era era, Adds c) =>
c
-> c
-> [String]
-> OrdCond
-> V era (Map dom rng)
-> c
-> [Sum era c]
-> Typed (RngSpec era rng)
solveMapSummands (forall a. Direct a -> a
direct Direct c
small) c
t [String
msg] OrdCond
cond V era (Map dom rng)
v1 forall x. Adds x => x
zero [Sum era c]
xs
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
SzAny forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny RngSpec era rng
rngspec
  (Random (Var V era t
v2)) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
SzAny forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (Sized (Size Size
sz) (Var V era t
v2)) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
sz forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (Disjoint Term era (Set a)
expr (Dom (Var V era (Map a b)
v2))) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    With s t1
set <- forall rng era y.
(Ord rng, Era era) =>
Rep era rng -> Term era y -> Typed (HasConstraint Ord (Set rng))
simplifySet Rep era a
dom Term era (Set a)
expr
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
SzAny (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era a
dom s t1
set) forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (Disjoint (Dom (Var V era (Map a b)
v2)) Term era (Set a)
expr) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    With s t1
set <- forall rng era y.
(Ord rng, Era era) =>
Rep era rng -> Term era y -> Typed (HasConstraint Ord (Set rng))
simplifySet Rep era a
dom Term era (Set a)
expr
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
SzAny (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era a
dom s t1
set) forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (Disjoint Term era (Set a)
expr (Rng (Var V era (Map a b)
v2))) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    With s t1
_ <- forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Ord (s t))
hasOrd Rep era b
rng Rep era b
rng
    With s t1
set <- forall rng era y.
(Ord rng, Era era) =>
Rep era rng -> Term era y -> Typed (HasConstraint Ord (Set rng))
simplifySet Rep era b
rng Term era (Set a)
expr
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
SzAny forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny (forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel forall a b. (a -> b) -> a -> b
$ forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era b
rng s t1
set)
  (Disjoint (Rng (Var V era (Map a b)
v2)) Term era (Set a)
expr) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    With s t1
_ <- forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Ord (s t))
hasOrd Rep era b
rng Rep era b
rng
    With s t1
set <- forall rng era y.
(Ord rng, Era era) =>
Rep era rng -> Term era y -> Typed (HasConstraint Ord (Set rng))
simplifySet Rep era b
rng Term era (Set a)
expr
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
SzAny forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny (forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel forall a b. (a -> b) -> a -> b
$ forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era b
rng s t1
set)
  (Member (Left (HashS Term era (ScriptF era)
expr)) (Dom (Var v2 :: V era (Map a b)
v2@(V String
_ (MapR Rep era a
a Rep era b
_) Access era s (Map a b)
_)))) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
a
    ScriptF Proof era
_ Script era
x <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType (forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR forall era. Reflect era => Proof era
reify) Term era (ScriptF era)
expr
    let hash :: ScriptHash
hash = forall era. EraScript era => Script era -> ScriptHash
hashScript @era Script era
x
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzLeast Int
1) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
dom (forall a. a -> Set a
Set.singleton ScriptHash
hash)) forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (Member (Right (HashS Term era (ScriptF era)
expr)) (Dom (Var v2 :: V era (Map a b)
v2@(V String
_ (MapR Rep era a
a Rep era b
_) Access era s (Map a b)
_)))) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
a
    ScriptF Proof era
_ Script era
x <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType (forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR forall era. Reflect era => Proof era
reify) Term era (ScriptF era)
expr
    let hash :: ScriptHash
hash = forall era. EraScript era => Script era -> ScriptHash
hashScript @era Script era
x
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzLeast Int
1) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
dom (forall a. a -> Set a
Set.singleton ScriptHash
hash)) forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (Member (Left (HashD Term era (Data era)
expr)) (Dom (Var v2 :: V era (Map a b)
v2@(V String
_ (MapR Rep era a
a Rep era b
_) Access era s (Map a b)
_)))) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
a
    Data era
x <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType forall era. Era era => Rep era (Data era)
DataR Term era (Data era)
expr
    let hash :: SafeHash EraIndependentData
hash = forall era. Data era -> SafeHash EraIndependentData
hashData @era Data era
x
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzLeast Int
1) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
dom (forall a. a -> Set a
Set.singleton SafeHash EraIndependentData
hash)) forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (Member (Right (HashD Term era (Data era)
expr)) (Dom (Var v2 :: V era (Map a b)
v2@(V String
_ (MapR Rep era a
a Rep era b
_) Access era s (Map a b)
_)))) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
a
    Data era
x <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType forall era. Era era => Rep era (Data era)
DataR Term era (Data era)
expr
    let hash :: SafeHash EraIndependentData
hash = forall era. Data era -> SafeHash EraIndependentData
hashData @era Data era
x
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzLeast Int
1) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
dom (forall a. a -> Set a
Set.singleton SafeHash EraIndependentData
hash)) forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (Member Direct (Term era a)
expr (Dom (Var v2 :: V era (Map a b)
v2@(V String
_ (MapR Rep era a
a Rep era b
_) Access era s (Map a b)
_)))) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
a
    a
x <- forall era t. Term era t -> Typed t
simplify (forall a. Direct a -> a
direct Direct (Term era a)
expr)
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzLeast Int
1) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
dom (forall a. a -> Set a
Set.singleton a
x)) forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (Member Direct (Term era a)
expr (Rng (Var v2 :: V era (Map a b)
v2@(V String
_ (MapR Rep era a
_ Rep era b
b) Access era s (Map a b)
_)))) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    b :~: b
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
rng Rep era b
b
    a
x <- forall era t. Term era t -> Typed t
simplify (forall a. Direct a -> a
direct Direct (Term era a)
expr)
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzLeast Int
1) forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny (forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era b
rng (forall a. a -> Set a
Set.singleton a
x)))
  (NotMember Term era a
expr (Dom (Var v2 :: V era (Map a b)
v2@(V String
_ (MapR Rep era a
a Rep era b
_) Access era s (Map a b)
_)))) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
a
    a
x <- forall era t. Term era t -> Typed t
simplify Term era a
expr
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
SzAny (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era a
dom (forall a. a -> Set a
Set.singleton a
x)) forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (NotMember Term era a
expr (Rng (Var v2 :: V era (Map a b)
v2@(V String
_ (MapR Rep era a
_ Rep era b
b) Access era s (Map a b)
_)))) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    b :~: b
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
rng Rep era b
b
    a
x <- forall era t. Term era t -> Typed t
simplify Term era a
expr
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
SzAny forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny (forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era b
rng (forall a. a -> Set a
Set.singleton a
x)))
  (MapMember Term era k
exprK Term era v
exprV (Left (Var v2 :: V era (Map k v)
v2@(V String
_ (MapR Rep era a
dom2 Rep era b
rng2) Access era s (Map k v)
_)))) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map k v)
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
dom2
    b :~: b
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
rng Rep era b
rng2
    k
k <- forall era t. Term era t -> Typed t
simplify Term era k
exprK
    v
v <- forall era t. Term era t -> Typed t
simplify Term era v
exprV
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec
      (Int -> Size
SzLeast Int
1)
      (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
dom (forall a. a -> Set a
Set.singleton k
k))
      (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era a
dom Rep era b
rng PairSide
VarOnRight (forall k a. k -> a -> Map k a
Map.singleton k
k v
v))
      (forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era b
rng (forall a. a -> Set a
Set.singleton v
v)))
  (MapMember Term era k
exprK Term era v
exprV (Right (Var v2 :: V era (Map k v)
v2@(V String
_ (MapR Rep era a
dom2 Rep era b
rng2) Access era s (Map k v)
_)))) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map k v)
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
dom2
    b :~: b
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
rng Rep era b
rng2
    k
k <- forall era t. Term era t -> Typed t
simplify Term era k
exprK
    v
v <- forall era t. Term era t -> Typed t
simplify Term era v
exprV
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec
      (Int -> Size
SzLeast Int
1)
      (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
dom (forall a. a -> Set a
Set.singleton k
k))
      (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era a
dom Rep era b
rng PairSide
VarOnRight (forall k a. k -> a -> Map k a
Map.singleton k
k v
v))
      (forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era b
rng (forall a. a -> Set a
Set.singleton v
v)))
  (List (Var v2 :: V era fs
v2@(V String
_ Rep era fs
_ Access era s fs
_)) [Term era t]
xs)
    | Just Map dom rng :~: fs
Refl <- forall era t s. V era t -> V era s -> Maybe (t :~: s)
sameName V era (Map dom rng)
v1 V era fs
v2
    , forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term era t]
xs ->
        forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Int -> Size
SzExact Int
0) forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
  (List (Var v2 :: V era fs
v2@(V String
_ Rep era fs
_ Access era s fs
_)) xs :: [Term era t]
xs@(Term era t
x : [Term era t]
_))
    | Just Map dom rng :~: fs
Refl <- forall era t s. V era t -> V era s -> Maybe (t :~: s)
sameName V era (Map dom rng)
v1 V era fs
v2
    , Right (With s t1
_) <- forall x. Typed x -> Either [String] x
runTyped forall a b. (a -> b) -> a -> b
$ forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Ord (s t))
hasOrd Rep era b
rng Rep era b
rng
    , PairR Rep era a
dl Rep era b
rl <- forall era t. Era era => Term era t -> Rep era t
termRep Term era t
x -> do
        a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
dl
        b :~: b
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
rng Rep era b
rl
        [(a, b)]
ys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType (forall era a b. Rep era a -> Rep era b -> Rep era (a, b)
PairR Rep era a
dl Rep era b
rl)) [Term era t]
xs
        let ([a]
ds, [b]
rs) = forall a b. [(a, b)] -> ([a], [b])
unzip [(a, b)]
ys
        forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec
          (Int -> Size
SzExact (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(a, b)]
ys))
          (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
dl (forall ts a. FromList ts a => [a] -> ts
makeFromList @(Set dom) [a]
ds))
          (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era a
dom Rep era b
rng PairSide
VarOnRight (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(a, b)]
ys))
          (forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era b
rl (forall ts a. FromList ts a => [a] -> ts
makeFromList @(Set rng) [b]
rs)))
  (SubMap Term era (Map k v)
subMapExpr (Var v2 :: V era (Map k v)
v2@(V String
_ (MapR Rep era a
dom2 Rep era b
rng2) Access era s (Map k v)
_))) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map k v)
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
dom2
    b :~: b
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
rng Rep era b
rng2
    Map k v
m <- forall era t. Term era t -> Typed t
simplify Term era (Map k v)
subMapExpr
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec
      (Int -> Size
SzLeast (forall k a. Map k a -> Int
Map.size Map k v
m))
      (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
dom (forall k a. Map k a -> Set k
Map.keysSet Map k v
m))
      (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era a
dom Rep era b
rng PairSide
VarOnRight Map k v
m)
      (forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era b
rng (forall a. Ord a => [a] -> Set a
Set.fromList (forall k a. Map k a -> [a]
Map.elems Map k v
m))))
  (SubMap (Var v2 :: V era (Map k v)
v2@(V String
_ (MapR Rep era a
dom2 Rep era b
rng2) Access era s (Map k v)
_)) Term era (Map k v)
subMapExpr) | forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Map k v)
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
dom2
    b :~: b
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
rng Rep era b
rng2
    Map k v
m <- forall era t. Term era t -> Typed t
simplify Term era (Map k v)
subMapExpr
    forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec
      (Int -> Size
SzMost (forall k a. Map k a -> Int
Map.size Map k v
m))
      (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era a
dom (forall k a. Map k a -> Set k
Map.keysSet Map k v
m))
      (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era a
dom Rep era b
rng PairSide
VarOnLeft Map k v
m)
      (forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era b
rng (forall a. Ord a => [a] -> Set a
Set.fromList (forall k a. Map k a -> [a]
Map.elems Map k v
m))))
  Pred era
other -> forall a. [String] -> Typed a
failT [String
"Cannot solve map condition: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred era
other]
  where
    msg :: String
msg = (String
"Solving for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show V era (Map dom rng)
v1 forall a. [a] -> [a] -> [a]
++ String
"\nPredicate = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred era
predicate)

-- | We are solving for a (V era (Map d r)). This must occurr exactly once in the [Sum era c]
--   That can only happen in a (RngSum cond c) or a (RngProj cond rep c) constructor of 'Sum'
--   Because we don't know if 'c' can have negative values, we do the summation as an Integer
solveMapSummands ::
  (Era era, Adds c) =>
  c -> -- The smallest allowed
  c -> -- the evaluated lhs
  [String] -> -- path to here
  OrdCond -> -- The condtion in the SumsTo
  V era (Map dom rng) -> -- The name of the unique Var on the rhs
  c -> -- The sum of the other expressions on the rhs
  [Sum era c] ->
  Typed (RngSpec era rng)
solveMapSummands :: forall era c dom rng.
(Era era, Adds c) =>
c
-> c
-> [String]
-> OrdCond
-> V era (Map dom rng)
-> c
-> [Sum era c]
-> Typed (RngSpec era rng)
solveMapSummands c
small c
lhsC [String]
msgs OrdCond
cond (V String
_ (MapR Rep era a
_ Rep era b
r) Access era s (Map dom rng)
_) c
c [SumList (Elems (Var (V String
name (MapR Rep era a
_ Rep era b
r1) Access era s (Map a b)
_)))] = do
  b :~: b
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
r Rep era b
r1
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall rng era. Adds rng => rng -> Size -> RngSpec era rng
RngSum c
small (forall a. Adds a => [String] -> a -> OrdCond -> a -> String -> Size
varOnRightSize [String]
msgs c
lhsC OrdCond
cond c
c String
name))
solveMapSummands c
small c
lhsC [String]
msgs OrdCond
cond (V String
_ (MapR Rep era a
_ Rep era b
r) Access era s (Map dom rng)
_) c
c [ProjMap Rep era c
_crep Lens' x c
l (Var (V String
name (MapR Rep era a
_ Rep era b
r1) Access era s (Map a x)
_))] = do
  b :~: b
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
r Rep era b
r1
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall c era rng.
Adds c =>
c -> Rep era rng -> Lens' rng c -> Size -> RngSpec era rng
RngProj c
small Rep era b
r Lens' x c
l (forall a. Adds a => [String] -> a -> OrdCond -> a -> String -> Size
varOnRightSize [String]
msgs c
lhsC OrdCond
cond c
c String
name))
solveMapSummands c
small c
lhsC [String]
msgs OrdCond
cond (V String
_ (MapR Rep era a
_ Rep era b
r) Access era s (Map dom rng)
_) c
c [SumMap (Var (V String
name (MapR Rep era a
_ Rep era b
r1) Access era s (Map a c)
_))] = do
  b :~: b
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
r Rep era b
r1
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall rng era. Adds rng => rng -> Size -> RngSpec era rng
RngSum c
small (forall a. Adds a => [String] -> a -> OrdCond -> a -> String -> Size
varOnRightSize [String]
msgs c
lhsC OrdCond
cond c
c String
name))
solveMapSummands c
small c
lhsC [String]
msg OrdCond
cond V era (Map dom rng)
v c
c (Sum era c
s : [Sum era c]
ss)
  | forall era c. Name era -> Sum era c -> Bool
isMapVar (forall era t. V era t -> Name era
Name V era (Map dom rng)
v) Sum era c
s =
      forall era c dom rng.
(Era era, Adds c) =>
c
-> c
-> [String]
-> OrdCond
-> V era (Map dom rng)
-> c
-> [Sum era c]
-> Typed (RngSpec era rng)
solveMapSummands c
small c
lhsC [String]
msg OrdCond
cond V era (Map dom rng)
v c
c ([Sum era c]
ss forall a. [a] -> [a] -> [a]
++ [Sum era c
s])
solveMapSummands c
small c
lhsC [String]
msg OrdCond
cond V era (Map dom rng)
v c
c (Sum era c
s : [Sum era c]
ss) = do
  Int
d <- forall c era. Adds c => Sum era c -> Typed Int
summandAsInt Sum era c
s
  forall era c dom rng.
(Era era, Adds c) =>
c
-> c
-> [String]
-> OrdCond
-> V era (Map dom rng)
-> c
-> [Sum era c]
-> Typed (RngSpec era rng)
solveMapSummands c
small c
lhsC [String]
msg OrdCond
cond V era (Map dom rng)
v (forall x. Adds x => x -> x -> x
add c
c forall a b. (a -> b) -> a -> b
$ forall x. Adds x => [String] -> Int -> x
fromI [String
"solveMapSummands"] Int
d) [Sum era c]
ss
solveMapSummands c
_ c
_ [String]
msg OrdCond
_ V era (Map dom rng)
v c
_ [] = forall a. [String] -> Typed a
failT ((String
"Does not have exactly one summand with variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era t. V era t -> Name era
Name V era (Map dom rng)
v)) forall a. a -> [a] -> [a]
: [String]
msg)

solveMaps :: (Era era, Ord dom) => V era (Map dom rng) -> [Pred era] -> Typed (MapSpec era dom rng)
solveMaps :: forall era dom rng.
(Era era, Ord dom) =>
V era (Map dom rng) -> [Pred era] -> Typed (MapSpec era dom rng)
solveMaps v :: V era (Map dom rng)
v@(V String
_ (MapR Rep era a
_ Rep era b
_) Access era s (Map dom rng)
_) [Pred era]
cs =
  forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' MapSpec era dom rng -> Pred era -> Typed (MapSpec era dom rng)
accum (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
SzAny forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny) [Pred era]
cs
  where
    accum :: MapSpec era dom rng -> Pred era -> Typed (MapSpec era dom rng)
accum MapSpec era dom rng
spec Pred era
cond = do
      MapSpec era dom rng
condspec <- forall dom rng era.
Era era =>
V era (Map dom rng) -> Pred era -> Typed (MapSpec era dom rng)
solveMap V era (Map dom rng)
v Pred era
cond
      forall x. LiftT x => x -> Typed x
liftT (MapSpec era dom rng
spec forall a. Semigroup a => a -> a -> a
<> MapSpec era dom rng
condspec)

-- ===========================================================
-- Solving for variables with type Set

-- | Given a variable: 'v1', with a Set type, compute a SetSpec
--   which describes the constraints implied by the Pred 'predicate'
solveSet :: forall era a. Era era => V era (Set a) -> Pred era -> Typed (SetSpec era a)
solveSet :: forall era a.
Era era =>
V era (Set a) -> Pred era -> Typed (SetSpec era a)
solveSet v1 :: V era (Set a)
v1@(V String
_ (SetR Rep era a
r) Access era s (Set a)
_) Pred era
predicate = case Pred era
predicate of
  (Sized (Size Size
sz) (Var V era t
v2)) | forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec Size
sz forall era dom. RelSpec era dom
RelAny
  (List (Var v2 :: V era fs
v2@(V String
_ (SetR Rep era a
_) Access era s fs
_)) []) | Just Set a :~: fs
Refl <- forall era t s. V era t -> V era s -> Maybe (t :~: s)
sameName V era (Set a)
v1 V era fs
v2 -> forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzExact Int
0) forall era dom. RelSpec era dom
RelAny
  (List (Var v2 :: V era fs
v2@(V String
_ (SetR Rep era a
r2) Access era s fs
_)) expr :: [Term era t]
expr@(Term era t
x : [Term era t]
_)) | Just Set a :~: fs
Refl <- forall era t s. V era t -> V era s -> Maybe (t :~: s)
sameName V era (Set a)
v1 V era fs
v2 -> do
    t :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep (forall era t. Era era => Term era t -> Rep era t
termRep Term era t
x) Rep era a
r2
    [a]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era a
r2) [Term era t]
expr
    forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzMost (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs)) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
r (forall ts a. FromList ts a => [a] -> ts
makeFromList @(Set a) @a [a]
xs))
  (Var V era a
v2 :=: Term era a
expr) | forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era a
v2 -> do
    With s t1
set <- forall rng era y.
(Ord rng, Era era) =>
Rep era rng -> Term era y -> Typed (HasConstraint Ord (Set rng))
simplifySet Rep era a
r Term era a
expr
    forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzExact (forall a. Set a -> Int
Set.size s t1
set)) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
r s t1
set)
  (Var v2 :: V era t
v2@(V String
_ (SetR Rep era a
r2) Access era s t
_) :<-: RootTarget era r t
target) | (forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2) -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r Rep era a
r2
    Set a
x <- forall era t root. RootTarget era root t -> Typed t
simplifyTarget @era @(Set a) RootTarget era r t
target
    forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzExact (forall a. Set a -> Int
Set.size Set a
x)) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
r Set a
x)
  (Term era a
expr :=: v2 :: Term era a
v2@(Var V era a
_)) -> forall era a.
Era era =>
V era (Set a) -> Pred era -> Typed (SetSpec era a)
solveSet V era (Set a)
v1 (Term era a
v2 forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era a
expr)
  (Term era a
expr1 :=: Restrict (Var v2 :: V era (Set a)
v2@(V String
_ (SetR Rep era a
a) Access era s (Set a)
_)) Term era (Map a b)
expr2) | forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
a Rep era a
r
    a
val1 <- forall era t. Term era t -> Typed t
simplify Term era a
expr1
    Map a b
val2 <- forall era t. Term era t -> Typed t
simplify Term era (Map a b)
expr2
    forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzExact (forall k a. Map k a -> Int
Map.size a
val1)) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
r (forall k a. Map k a -> Set k
Map.keysSet Map a b
val2))
  (Restrict Term era (Set a)
expr1 Term era (Map a b)
expr2 :=: Term era a
expr3) -> forall era a.
Era era =>
V era (Set a) -> Pred era -> Typed (SetSpec era a)
solveSet V era (Set a)
v1 (Term era a
expr3 forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict Term era (Set a)
expr1 Term era (Map a b)
expr2)
  (Var V era (Set a)
v2 `Subset` Term era (Set a)
expr) | forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    With s t1
set <- forall rng era y.
(Ord rng, Era era) =>
Rep era rng -> Term era y -> Typed (HasConstraint Ord (Set rng))
simplifySet Rep era a
r Term era (Set a)
expr
    forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzMost (forall a. Set a -> Int
Set.size s t1
set)) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era a
r s t1
set)
  (Term era (Set a)
expr `Subset` Var V era (Set a)
v2) | forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    With s t1
set <- forall rng era y.
(Ord rng, Era era) =>
Rep era rng -> Term era y -> Typed (HasConstraint Ord (Set rng))
simplifySet Rep era a
r Term era (Set a)
expr
    forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzLeast (forall a. Set a -> Int
Set.size s t1
set)) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
r s t1
set)
  (Disjoint (Var V era (Set a)
v2) Term era (Set a)
expr) | forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    With s t1
set <- forall rng era y.
(Ord rng, Era era) =>
Rep era rng -> Term era y -> Typed (HasConstraint Ord (Set rng))
simplifySet Rep era a
r Term era (Set a)
expr
    forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec Size
SzAny (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era a
r s t1
set)
  (Disjoint Term era (Set a)
expr (Var V era (Set a)
v2)) -> forall era a.
Era era =>
V era (Set a) -> Pred era -> Typed (SetSpec era a)
solveSet V era (Set a)
v1 (forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint (forall era t. V era t -> Term era t
Var V era (Set a)
v2) Term era (Set a)
expr)
  (Member (Left (HashS Term era (ScriptF era)
expr)) (Var v2 :: V era (Set a)
v2@(V String
_ (SetR Rep era a
ScriptHashR) Access era s (Set a)
_))) | forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    a :~: ScriptHash
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r forall era. Era era => Rep era ScriptHash
ScriptHashR
    ScriptF Proof era
_ Script era
x <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType (forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR forall era. Reflect era => Proof era
reify) Term era (ScriptF era)
expr
    let hash :: ScriptHash
hash = forall era. EraScript era => Script era -> ScriptHash
hashScript @era Script era
x
    forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzLeast Int
1) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
r (forall a. a -> Set a
Set.singleton ScriptHash
hash))
  (Member (Right (HashS Term era (ScriptF era)
expr)) (Var v2 :: V era (Set a)
v2@(V String
_ (SetR Rep era a
ScriptHashR) Access era s (Set a)
_))) | forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    a :~: ScriptHash
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r forall era. Era era => Rep era ScriptHash
ScriptHashR
    ScriptF Proof era
_ Script era
x <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType (forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR forall era. Reflect era => Proof era
reify) Term era (ScriptF era)
expr
    let hash :: ScriptHash
hash = forall era. EraScript era => Script era -> ScriptHash
hashScript @era Script era
x
    forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzLeast Int
1) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
r (forall a. a -> Set a
Set.singleton ScriptHash
hash))
  (Member (Left (HashD Term era (Data era)
expr)) (Var v2 :: V era (Set a)
v2@(V String
_ (SetR Rep era a
DataHashR) Access era s (Set a)
_))) | forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    a :~: SafeHash EraIndependentData
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r forall era. Era era => Rep era (SafeHash EraIndependentData)
DataHashR
    Data era
x <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType forall era. Era era => Rep era (Data era)
DataR Term era (Data era)
expr
    let hash :: SafeHash EraIndependentData
hash = forall era. Data era -> SafeHash EraIndependentData
hashData @era Data era
x
    forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzLeast Int
1) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
r (forall a. a -> Set a
Set.singleton SafeHash EraIndependentData
hash))
  (Member (Right (HashD Term era (Data era)
expr)) (Var v2 :: V era (Set a)
v2@(V String
_ (SetR Rep era a
DataHashR) Access era s (Set a)
_))) | forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    a :~: SafeHash EraIndependentData
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r forall era. Era era => Rep era (SafeHash EraIndependentData)
DataHashR
    Data era
x <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType forall era. Era era => Rep era (Data era)
DataR Term era (Data era)
expr
    let hash :: SafeHash EraIndependentData
hash = forall era. Data era -> SafeHash EraIndependentData
hashData @era Data era
x
    forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzLeast Int
1) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
r (forall a. a -> Set a
Set.singleton SafeHash EraIndependentData
hash))
  (Member Direct (Term era a)
expr (Var v2 :: V era (Set a)
v2@(V String
_ (SetR Rep era a
a) Access era s (Set a)
_))) | forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
a Rep era a
r
    a
x <- forall era t. Term era t -> Typed t
simplify (forall a. Direct a -> a
direct Direct (Term era a)
expr)
    forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzLeast Int
1) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
r (forall a. a -> Set a
Set.singleton a
x))
  (NotMember Term era a
expr (Var v2 :: V era (Set a)
v2@(V String
_ (SetR Rep era a
a) Access era s (Set a)
_))) | forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
a Rep era a
r
    a
x <- forall era t. Term era t -> Typed t
simplify Term era a
expr
    forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec Size
SzAny (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era a
r (forall a. a -> Set a
Set.singleton a
x))
  (List (Var v2 :: V era fs
v2@(V String
_ (SetR Rep era a
r2) Access era s fs
_)) [Term era t]
xs) | forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era fs
v2 -> do
    a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r Rep era a
r2
    [t]
ys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall era t. Term era t -> Typed t
simplify [Term era t]
xs
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a era. Ord a => Size -> RelSpec era a -> SetSpec era a
SetSpec (Int -> Size
SzMost (forall (t :: * -> *) a. Foldable t => t a -> Int
length [t]
ys)) (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
r (forall ts a. FromList ts a => [a] -> ts
makeFromList [t]
ys))
  (Random (Var V era t
v2)) | forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec Size
SzAny forall era dom. RelSpec era dom
RelAny
  (ProjS Lens' b t1
lensbt Rep era t1
trep (Var v2 :: V era (Set b)
v2@(V String
_ (SetR Rep era a
brep) Access era s (Set b)
_)) :=: Dom (Lit (MapR Rep era a
drep Rep era b
_) Map a b
x))
    | forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Set b)
v2 -> do
        a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r Rep era a
brep
        forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzExact (forall k a. Map k a -> Int
Map.size Map a b
x)) (forall b dom era.
Ord b =>
Lens' dom b
-> Rep era dom -> Rep era b -> RelSpec era b -> RelSpec era dom
RelLens Lens' b t1
lensbt Rep era a
r Rep era t1
trep (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
drep (forall k a. Map k a -> Set k
Map.keysSet Map a b
x)))
  (ProjS Lens' b t1
lensbt Rep era t1
trep (Var v2 :: V era (Set b)
v2@(V String
_ (SetR Rep era a
brep) Access era s (Set b)
_)) `Subset` Dom (Lit (MapR Rep era a
drep Rep era b
_) Map a b
x))
    | forall era t. V era t -> Name era
Name V era (Set a)
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Set b)
v2 -> do
        a :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r Rep era a
brep
        forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzMost (forall k a. Map k a -> Int
Map.size Map a b
x)) (forall b dom era.
Ord b =>
Lens' dom b
-> Rep era dom -> Rep era b -> RelSpec era b -> RelSpec era dom
RelLens Lens' b t1
lensbt Rep era a
r Rep era t1
trep (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era a
drep (forall k a. Map k a -> Set k
Map.keysSet Map a b
x)))
  Pred era
cond -> forall a. [String] -> Typed a
failT [String
"Can't solveSet " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred era
cond forall a. [a] -> [a] -> [a]
++ String
" for variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show V era (Set a)
v1]

solveSets :: Era era => V era (Set a) -> [Pred era] -> Typed (SetSpec era a)
solveSets :: forall era a.
Era era =>
V era (Set a) -> [Pred era] -> Typed (SetSpec era a)
solveSets v :: V era (Set a)
v@(V String
nm (SetR Rep era a
_) Access era s (Set a)
_) [Pred era]
cs =
  forall a. String -> Typed a -> Typed a
explain (String
"\nSolving for " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
", Set Predicates\n" forall a. [a] -> [a] -> [a]
++ [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]
cs)) forall a b. (a -> b) -> a -> b
$
    forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' SetSpec era a -> Pred era -> Typed (SetSpec era a)
accum forall a. Monoid a => a
mempty [Pred era]
cs
  where
    accum :: SetSpec era a -> Pred era -> Typed (SetSpec era a)
accum SetSpec era a
spec Pred era
cond = do
      SetSpec era a
condspec <- forall era a.
Era era =>
V era (Set a) -> Pred era -> Typed (SetSpec era a)
solveSet V era (Set a)
v Pred era
cond
      forall x. LiftT x => x -> Typed x
liftT (SetSpec era a
spec forall a. Semigroup a => a -> a -> a
<> SetSpec era a
condspec)

-- ========================================================
-- Solving for variables with an Adds instance

solveSum :: forall era t. (Adds t, Era era) => V era t -> Pred era -> Typed (AddsSpec t)
solveSum :: forall era t.
(Adds t, Era era) =>
V era t -> Pred era -> Typed (AddsSpec t)
solveSum v1 :: V era t
v1@(V String
nam Rep era t
r Access era s t
_) Pred era
predx =
  case Pred era
predx of
    (Sized Term era Size
expr (Var v2 :: V era t
v2@(V String
nm Rep era t
_ Access era s t
_))) | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> do
      Size
sz <- forall era t. Term era t -> Typed t
simplify Term era Size
expr
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall c. String -> Size -> AddsSpec c
AddsSpecSize String
nm Size
sz
    (Sized (Var V era Size
v2) Term era t
expr) | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era Size
v2 -> do
      t
n <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era t
r Term era t
expr
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
nam OrdCond
EQL t
n
    (Term era a
expr :=: (Var V era a
v2)) | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era a
v2 -> do
      t
n <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era t
r Term era a
expr
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
nam OrdCond
EQL t
n
    ((Var V era a
v2) :=: Term era a
expr) | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era a
v2 -> do
      t
n <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era t
r Term era a
expr
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
nam OrdCond
EQL t
n
    (Term era a
expr :=: Delta (Var v2 :: V era Coin
v2@(V String
_ Rep era Coin
CoinR Access era s Coin
_))) | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era Coin
v2 -> do
      DeltaCoin Integer
n <- forall era t. Term era t -> Typed t
simplify Term era a
expr
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
nam OrdCond
EQL (Integer -> Coin
Coin Integer
n)
    -- This is an EQL test (x :=: y), so whether the
    -- variable is on the Left or the Right does not matter
    (Delta (Var V era Coin
v2) :=: Term era a
expr) -> forall era t.
(Adds t, Era era) =>
V era t -> Pred era -> Typed (AddsSpec t)
solveSum V era t
v1 (Term era a
expr forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (forall era. Term era Coin -> Term era DeltaCoin
Delta (forall era t. V era t -> Term era t
Var V era Coin
v2)))
    (Term era a
expr :=: Negate (Var V era DeltaCoin
v2)) | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era DeltaCoin
v2 -> do
      t :~: DeltaCoin
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r forall era. Rep era DeltaCoin
DeltaCoinR
      DeltaCoin Integer
n <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType forall era. Rep era DeltaCoin
DeltaCoinR Term era a
expr
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
nam OrdCond
EQL (Integer -> DeltaCoin
DeltaCoin (-Integer
n))
    (Negate (Var V era DeltaCoin
v2) :=: Term era a
expr) | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era DeltaCoin
v2 -> do
      t :~: DeltaCoin
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r forall era. Rep era DeltaCoin
DeltaCoinR
      DeltaCoin Integer
n <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType forall era. Rep era DeltaCoin
DeltaCoinR Term era a
expr
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
nam OrdCond
EQL (Integer -> DeltaCoin
DeltaCoin (-Integer
n))
    (Random (Var V era t
v2)) | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall c. AddsSpec c
AddsSpecAny
    (SumsTo Direct c
x (Delta (Lit Rep era Coin
_ n :: Coin
n@(Coin Integer
i))) OrdCond
cond xs :: [Sum era c]
xs@(Sum era c
_ : [Sum era c]
_)) -> do
      (Int
rhsTotal, Bool
needsNeg) <- forall c era t.
Adds c =>
V era t -> [Sum era c] -> Typed (Int, Bool)
intSumWithUniqueV V era t
v1 [Sum era c]
xs
      case Rep era t
r of
        Rep era t
CoinR ->
          if Bool
needsNeg
            then forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a c. Adds a => a -> OrdCond -> a -> String -> AddsSpec c
varOnRightNeg Coin
n OrdCond
cond (forall x. Adds x => [String] -> Int -> x
fromI [String
"solveSum-SumsTo 1"] Int
rhsTotal) String
nam)
            else
              if Int
rhsTotal forall a. Ord a => a -> a -> Bool
< Int
0
                then
                  forall (f :: * -> *) a. Applicative f => a -> f a
pure
                    (forall a c.
Adds a =>
[String] -> a -> OrdCond -> a -> String -> AddsSpec c
varOnRight [String
"CASE1", forall a. Show a => a -> String
show Pred era
predx] (forall x. Adds x => x -> x -> x
add Coin
n (Integer -> Coin
Coin forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall a. Num a => a -> a
negate Int
rhsTotal)) OrdCond
cond (Integer -> Coin
Coin Integer
0) String
nam)
                else
                  forall (f :: * -> *) a. Applicative f => a -> f a
pure
                    ( forall a c.
Adds a =>
[String] -> a -> OrdCond -> a -> String -> AddsSpec c
varOnRight
                        [String
"CASE2", forall a. Show a => a -> String
show Pred era
predx]
                        Coin
n
                        OrdCond
cond
                        (forall x. Adds x => [String] -> Int -> x
fromI [String
"solveSum-SumsTo 2", forall a. Show a => a -> String
show Coin
n, forall a. Show a => a -> String
show Int
rhsTotal, forall a. Show a => a -> String
show Direct c
x, forall a. Show a => a -> String
show V era t
v1] Int
rhsTotal)
                        String
nam
                    )
        Rep era t
DeltaCoinR ->
          if Bool
needsNeg
            then forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a c. Adds a => a -> OrdCond -> a -> String -> AddsSpec c
varOnRightNeg (Integer -> DeltaCoin
DeltaCoin Integer
i) OrdCond
cond (forall x. Adds x => [String] -> Int -> x
fromI [String
"solveSum-SumsTo 3"] Int
rhsTotal) String
nam)
            else
              forall (f :: * -> *) a. Applicative f => a -> f a
pure
                (forall a c.
Adds a =>
[String] -> a -> OrdCond -> a -> String -> AddsSpec c
varOnRight [String
"CASE3", forall a. Show a => a -> String
show Pred era
predx] (Integer -> DeltaCoin
DeltaCoin Integer
i) OrdCond
cond (forall x. Adds x => [String] -> Int -> x
fromI [String
"solveSum-SumsTo 4"] Int
rhsTotal) String
nam)
        Rep era t
other -> forall a. [String] -> Typed a
failT [forall a. Show a => a -> String
show Pred era
predx, forall a. Show a => a -> String
show Rep era t
other forall a. [a] -> [a] -> [a]
++ String
" should be either Coin or DeltaCoin"]
    (SumsTo Direct c
_ (Lit Rep era c
r2 c
n) OrdCond
cond xs :: [Sum era c]
xs@(Sum era c
_ : [Sum era c]
_)) -> do
      (Int
rhsTotal, Bool
needsNeg) <- forall c era t.
Adds c =>
V era t -> [Sum era c] -> Typed (Int, Bool)
intSumWithUniqueV V era t
v1 [Sum era c]
xs
      t :~: c
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r Rep era c
r2
      if Bool
needsNeg
        then forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a c. Adds a => a -> OrdCond -> a -> String -> AddsSpec c
varOnRightNeg c
n OrdCond
cond (forall x. Adds x => [String] -> Int -> x
fromI [String
"solveSum-SumsTo 5"] Int
rhsTotal) String
nam)
        else forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a c.
Adds a =>
[String] -> a -> OrdCond -> a -> String -> AddsSpec c
varOnRight [String
"CASE4", forall a. Show a => a -> String
show Pred era
predx] c
n OrdCond
cond (forall x. Adds x => [String] -> Int -> x
fromI [String
"solveSum-SumsTo 6"] Int
rhsTotal) String
nam)
    (SumsTo Direct c
_ (Var v2 :: V era c
v2@(V String
_ Rep era c
r2 Access era s c
_)) OrdCond
cond xs :: [Sum era c]
xs@(Sum era c
_ : [Sum era c]
_)) | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era c
v2 -> do
      Int
rhsTotal <- forall c era. (Adds c, Era era) => [Sum era c] -> Typed Int
summandsAsInt [Sum era c]
xs
      t :~: c
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r Rep era c
r2
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
nam OrdCond
cond Int
rhsTotal
    (SumsTo Direct c
_ (Delta (Var V era Coin
v2)) OrdCond
cond xs :: [Sum era c]
xs@(Sum era c
_ : [Sum era c]
_)) | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era Coin
v2 -> do
      Int
rhsTotal <- forall c era. (Adds c, Era era) => [Sum era c] -> Typed Int
summandsAsInt [Sum era c]
xs
      case Rep era t
r of
        Rep era t
CoinR -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
nam OrdCond
cond Int
rhsTotal
        Rep era t
DeltaCoinR -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
nam OrdCond
cond Int
rhsTotal
        Rep era t
other -> forall a. [String] -> Typed a
failT [forall a. Show a => a -> String
show Pred era
predx, forall a. Show a => a -> String
show Rep era t
other forall a. [a] -> [a] -> [a]
++ String
" should be either Coin or DeltaCoin"]
    (Var v2 :: V era t
v2@(V String
nm Rep era t
r2 Access era s t
_) :<-: RootTarget era r t
tar) | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> do
      t :~: t
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r Rep era t
r2
      t
x <- forall era t root. RootTarget era root t -> Typed t
simplifyTarget RootTarget era r t
tar
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall c. String -> Size -> AddsSpec c
AddsSpecSize String
nm (Int -> Size
SzExact (forall x. Adds x => x -> Int
toI t
x)))
    Pred era
other -> forall a. [String] -> Typed a
failT [String
"Can't solveSum " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era t. V era t -> Name era
Name V era t
v1) forall a. [a] -> [a] -> [a]
++ String
" = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred era
other]

solveSums :: (Adds t, Era era) => V era t -> [Pred era] -> Typed (AddsSpec t)
solveSums :: forall t era.
(Adds t, Era era) =>
V era t -> [Pred era] -> Typed (AddsSpec t)
solveSums v :: V era t
v@(V String
nm Rep era t
r Access era s t
_) [Pred era]
cs =
  forall a. String -> Typed a -> Typed a
explain
    ( String
"\nGiven (Add "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era t
r
        forall a. [a] -> [a] -> [a]
++ String
"), Solving for "
        forall a. [a] -> [a] -> [a]
++ String
nm
        forall a. [a] -> [a] -> [a]
++ String
" :: "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era t
r
        forall a. [a] -> [a] -> [a]
++ String
",  with Predicates \n"
        forall a. [a] -> [a] -> [a]
++ [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]
cs)
    )
    forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' AddsSpec t -> Pred era -> Typed (AddsSpec t)
accum forall a. Monoid a => a
mempty [Pred era]
cs
  where
    accum :: AddsSpec t -> Pred era -> Typed (AddsSpec t)
accum AddsSpec t
spec Pred era
cond = do
      AddsSpec t
sumVspec <- forall era t.
(Adds t, Era era) =>
V era t -> Pred era -> Typed (AddsSpec t)
solveSum V era t
v Pred era
cond
      forall a. String -> Typed a -> Typed a
explain
        (String
"Solving Sum constraint (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred era
cond forall a. [a] -> [a] -> [a]
++ String
") for variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
nm)
        (forall x. LiftT x => x -> Typed x
liftT (AddsSpec t
spec forall a. Semigroup a => a -> a -> a
<> AddsSpec t
sumVspec))

summandAsInt :: Adds c => Sum era c -> Typed Int
summandAsInt :: forall c era. Adds c => Sum era c -> Typed Int
summandAsInt (One (Lit Rep era c
_ c
x)) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall x. Adds x => x -> Int
toI c
x)
summandAsInt (One (Delta (Lit Rep era Coin
CoinR (Coin Integer
n)))) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall x. Adds x => x -> Int
toI (Integer -> DeltaCoin
DeltaCoin Integer
n))
summandAsInt (One (Negate (Lit Rep era DeltaCoin
DeltaCoinR (DeltaCoin Integer
n)))) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall x. Adds x => x -> Int
toI ((Integer -> DeltaCoin
DeltaCoin (-Integer
n))))
summandAsInt (ProjOne Lens' x c
l Rep era c
CoinR (Lit Rep era x
_ x
x)) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall x. Adds x => x -> Int
toI (x
x forall s a. s -> Getting a s a -> a
^. Lens' x c
l))
summandAsInt (SumMap (Lit Rep era (Map a c)
_ Map a c
m)) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall x. Adds x => x -> Int
toI (forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' forall x. Adds x => x -> x -> x
add forall x. Adds x => x
zero Map a c
m))
summandAsInt (SumList (Lit Rep era [c]
_ [c]
m)) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall x. Adds x => x -> Int
toI (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall x. Adds x => x -> x -> x
add forall x. Adds x => x
zero [c]
m))
summandAsInt (ProjMap Rep era c
_ Lens' x c
l (Lit Rep era (Map a x)
_ Map a x
m)) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall x. Adds x => x -> Int
toI (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\c
ans x
x -> forall x. Adds x => x -> x -> x
add c
ans (x
x forall s a. s -> Getting a s a -> a
^. Lens' x c
l)) forall x. Adds x => x
zero Map a x
m))
summandAsInt Sum era c
x = forall a. [String] -> Typed a
failT [String
"Can't compute summandAsInt: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Sum era c
x forall a. [a] -> [a] -> [a]
++ String
", to an Int."]

genSum :: Adds x => Sum era x -> Rep era x -> x -> Subst era -> Gen (Subst era)
genSum :: forall x era.
Adds x =>
Sum era x -> Rep era x -> x -> Subst era -> Gen (Subst era)
genSum (One (Var V era x
v)) Rep era x
rep x
x Subst era
sub = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era t. V era t -> Term era t -> Subst era -> Subst era
extend V era x
v (forall era t. Rep era t -> t -> Term era t
Lit Rep era x
rep x
x) Subst era
sub
genSum (One (Delta (Var V era Coin
v))) Rep era x
DeltaCoinR x
d Subst era
sub = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era t. V era t -> Term era t -> Subst era -> Subst era
extend V era Coin
v (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (forall x. Adds x => [String] -> Int -> x
fromI [] (forall x. Adds x => x -> Int
toI x
d))) Subst era
sub
genSum (One (Negate (Var V era DeltaCoin
v))) Rep era x
DeltaCoinR (DeltaCoin Integer
n) Subst era
sub = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era t. V era t -> Term era t -> Subst era -> Subst era
extend V era DeltaCoin
v (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era DeltaCoin
DeltaCoinR (Integer -> DeltaCoin
DeltaCoin (-Integer
n))) Subst era
sub
genSum Sum era x
other Rep era x
rep x
x Subst era
_ = forall a. HasCallStack => String -> [String] -> a
errorMess (String
"Can't genSum " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Sum era x
other) [forall a. Show a => a -> String
show Rep era x
rep, forall a. Show a => a -> String
show x
x]

summandsAsInt :: (Adds c, Era era) => [Sum era c] -> Typed Int
summandsAsInt :: forall c era. (Adds c, Era era) => [Sum era c] -> Typed Int
summandsAsInt [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
0
summandsAsInt (Sum era c
x : [Sum era c]
xs) = do
  Int
n <- forall c era. Adds c => Sum era c -> Typed Int
summandAsInt Sum era c
x
  Int
m <- forall c era. (Adds c, Era era) => [Sum era c] -> Typed Int
summandsAsInt [Sum era c]
xs
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
m forall a. Num a => a -> a -> a
+ Int
n)

sameV :: V era s -> V era t -> Typed (s :~: t)
sameV :: forall era s t. V era s -> V era t -> Typed (s :~: t)
sameV (V String
_ Rep era s
r1 Access era s s
_) (V String
_ Rep era t
r2 Access era s t
_) = forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era s
r1 Rep era t
r2

unique2 ::
  Adds c => V era t -> (Int, Bool, [Name era]) -> Sum era c -> Typed (Int, Bool, [Name era])
unique2 :: forall c era t.
Adds c =>
V era t
-> (Int, Bool, [Name era])
-> Sum era c
-> Typed (Int, Bool, [Name era])
unique2 V era t
v1 (Int
c, Bool
b, [Name era]
ns) (One (Var V era c
v2)) =
  if forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era c
v2
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
c, Bool
b, forall era t. V era t -> Name era
Name V era c
v2 forall a. a -> [a] -> [a]
: [Name era]
ns)
    else forall a. [String] -> Typed a
failT [String
"Unexpected Name in 'unique' " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show V era c
v2]
unique2 V era t
v1 (Int
c, Bool
b, [Name era]
ns) (One (Delta (Var v2 :: V era Coin
v2@(V String
_ Rep era Coin
CoinR Access era s Coin
_)))) =
  if forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era Coin
v2
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
c, Bool
b, forall era t. V era t -> Name era
Name V era t
v1 forall a. a -> [a] -> [a]
: [Name era]
ns)
    else forall a. [String] -> Typed a
failT [String
"Unexpected Name in 'unique' " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show V era Coin
v2]
unique2 V era t
v1 (Int
c, Bool
_, [Name era]
ns) (One (Negate (Var v2 :: V era DeltaCoin
v2@(V String
_nam Rep era DeltaCoin
DeltaCoinR Access era s DeltaCoin
_)))) =
  if forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era DeltaCoin
v2
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
c, Bool
True, forall era t. V era t -> Name era
Name V era DeltaCoin
v2 forall a. a -> [a] -> [a]
: [Name era]
ns)
    else forall a. [String] -> Typed a
failT [String
"Unexpected Name in 'unique' " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show V era DeltaCoin
v2]
unique2 V era t
v1 (Int
c, Bool
b, [Name era]
ns) (ProjOne Lens' x c
_ Rep era c
_ (Var V era x
v2)) =
  if forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era x
v2
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
c, Bool
b, forall era t. V era t -> Name era
Name V era x
v2 forall a. a -> [a] -> [a]
: [Name era]
ns)
    else forall a. [String] -> Typed a
failT [String
"Unexpected Name in 'unique' " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show V era x
v2]
unique2 V era t
_ (Int
c1, Bool
b, [Name era]
ns) Sum era c
sumexpr = do Int
c2 <- forall c era. Adds c => Sum era c -> Typed Int
summandAsInt Sum era c
sumexpr; forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
c1 forall a. Num a => a -> a -> a
+ Int
c2, Bool
b, [Name era]
ns)

-- | Check that there is exactly 1 occurence of 'v',
--   and return the sum of the other terms in 'ss'
--   which should all be constants.
intSumWithUniqueV :: Adds c => V era t -> [Sum era c] -> Typed (Int, Bool)
intSumWithUniqueV :: forall c era t.
Adds c =>
V era t -> [Sum era c] -> Typed (Int, Bool)
intSumWithUniqueV v :: V era t
v@(V String
nam Rep era t
_ Access era s t
_) [Sum era c]
ss = do
  (Int
c, Bool
b, [Name era]
ns) <- forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' (forall c era t.
Adds c =>
V era t
-> (Int, Bool, [Name era])
-> Sum era c
-> Typed (Int, Bool, [Name era])
unique2 V era t
v) (Int
0, Bool
False, []) [Sum era c]
ss
  case [Name era]
ns of
    [Name era
_] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
c, Bool
b)
    [] -> forall a. [String] -> Typed a
failT [String
"Failed to find the unique name: " forall a. [a] -> [a] -> [a]
++ String
nam forall a. [a] -> [a] -> [a]
++ String
" in" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Sum era c]
ss]
    (Name era
_ : Name era
_ : [Name era]
_) -> forall a. [String] -> Typed a
failT [String
"The expected unique name: " forall a. [a] -> [a] -> [a]
++ String
nam forall a. [a] -> [a] -> [a]
++ String
" occurs more than once in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Sum era c]
ss]

-- ===========================================================
-- Solving for variables with type List

-- | Given a variable: 'v1', with a List type, compute a ListSpec
--   which describes the constraints implied by the Pred 'predicate'
solveList :: Era era => V era [a] -> Pred era -> Typed (ListSpec era a)
solveList :: forall era a.
Era era =>
V era [a] -> Pred era -> Typed (ListSpec era a)
solveList v1 :: V era [a]
v1@(V String
_ (ListR Rep era a
r) Access era s [a]
_) Pred era
predicate = case Pred era
predicate of
  (Sized (Size Size
sz) (Var V era t
v2)) | forall era t. V era t -> Name era
Name V era [a]
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era t. Size -> ElemSpec era t -> ListSpec era t
ListSpec Size
sz forall era t. ElemSpec era t
ElemAny
  (Var V era a
v2 :=: Term era a
expr) | forall era t. V era t -> Name era
Name V era [a]
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era a
v2 -> do
    With s t1
xs <- forall era rng y.
Era era =>
Rep era rng -> Term era y -> Typed (HasConstraint Eq [rng])
simplifyList Rep era a
r Term era a
expr
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era t. Size -> ElemSpec era t -> ListSpec era t
ListSpec (Int -> Size
SzExact (forall (t :: * -> *) a. Foldable t => t a -> Int
length s t1
xs)) (forall t era. Eq t => Rep era t -> [t] -> ElemSpec era t
ElemEqual Rep era a
r s t1
xs)
  (Term era a
expr :=: v2 :: Term era a
v2@(Var V era a
_)) -> forall era a.
Era era =>
V era [a] -> Pred era -> Typed (ListSpec era a)
solveList V era [a]
v1 (Term era a
v2 forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era a
expr)
  (Random (Var V era t
v2)) | forall era t. V era t -> Name era
Name V era [a]
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era t. Size -> ElemSpec era t -> ListSpec era t
ListSpec Size
SzAny forall era t. ElemSpec era t
ElemAny
  (List (Var v2 :: V era fs
v2@(V String
_ Rep era fs
r2 Access era s fs
_)) [Term era t]
xs) | forall era t. V era t -> Name era
Name V era [a]
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era fs
v2 -> do
    let r3 :: Rep era t
r3 = forall ts a era. FromList ts a => Rep era ts -> Rep era a
tsRep Rep era fs
r2
    a :~: t
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r Rep era t
r3
    [t]
ys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall era t. Term era t -> Typed t
simplify [Term era t]
xs
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era t. Size -> ElemSpec era t -> ListSpec era t
ListSpec (Int -> Size
SzExact (forall (t :: * -> *) a. Foldable t => t a -> Int
length [t]
ys)) (forall t era. Eq t => Rep era t -> [t] -> ElemSpec era t
ElemEqual Rep era a
r [t]
ys)
  Pred era
cond -> forall a. [String] -> Typed a
failT [String
"Can't solveList " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred era
cond forall a. [a] -> [a] -> [a]
++ String
" for variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show V era [a]
v1]

solveLists :: Era era => V era [a] -> [Pred era] -> Typed (ListSpec era a)
solveLists :: forall era a.
Era era =>
V era [a] -> [Pred era] -> Typed (ListSpec era a)
solveLists v :: V era [a]
v@(V String
nm (ListR Rep era a
_) Access era s [a]
_) [Pred era]
cs =
  forall a. String -> Typed a -> Typed a
explain (String
"\nSolving for " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
", List Predicates\n" forall a. [a] -> [a] -> [a]
++ [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]
cs)) forall a b. (a -> b) -> a -> b
$
    forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' ListSpec era a -> Pred era -> Typed (ListSpec era a)
accum forall a. Monoid a => a
mempty [Pred era]
cs
  where
    accum :: ListSpec era a -> Pred era -> Typed (ListSpec era a)
accum ListSpec era a
spec Pred era
cond = do
      ListSpec era a
condspec <- forall era a.
Era era =>
V era [a] -> Pred era -> Typed (ListSpec era a)
solveList V era [a]
v Pred era
cond
      forall x. LiftT x => x -> Typed x
liftT (ListSpec era a
spec forall a. Semigroup a => a -> a -> a
<> ListSpec era a
condspec)

-- ===================================================
-- Helper functions for use in 'dispatch'

-- | Combine solving an generating for a variable with a 'Counts' instance
genCount :: Count t => V era t -> [Pred era] -> Typed (Gen t)
genCount :: forall t era. Count t => V era t -> [Pred era] -> Typed (Gen t)
genCount v1 :: V era t
v1@(V String
_ Rep era t
rep Access era s t
_) [Random (Var V era t
v2)] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era b. Rep era b -> Gen b
genRep Rep era t
rep)
genCount v1 :: V era t
v1@(V String
_ Rep era t
r1 Access era s t
_) [Var v2 :: V era a
v2@(V String
_ Rep era a
r2 Access era s a
_) :=: Term era a
expr] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era a
v2 = do
  t :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era a
r2
  a
val <- forall era t. Term era t -> Typed t
simplify Term era a
expr
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
val)
genCount v1 :: V era t
v1@(V String
_ Rep era t
r1 Access era s t
_) [Term era a
expr :=: Var v2 :: V era a
v2@(V String
_ Rep era a
r2 Access era s a
_)] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era a
v2 = do
  t :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era a
r2
  a
val <- forall era t. Term era t -> Typed t
simplify Term era a
expr
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
val)
genCount v1 :: V era t
v1@(V String
_ Rep era t
r1 Access era s t
_) [CanFollow Term era n
succExpr (Var v2 :: V era n
v2@(V String
_ Rep era n
r2 Access era s n
_))] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era n
v2 = do
  t :~: n
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era n
r2
  n
succVal <- forall era t. Term era t -> Typed t
simplify Term era n
succExpr
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall t. Count t => t -> Gen t
genPred n
succVal)
genCount v1 :: V era t
v1@(V String
_ Rep era t
r1 Access era s t
_) [CanFollow (Var v2 :: V era n
v2@(V String
_ Rep era n
r2 Access era s n
_)) Term era n
predExpr] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era n
v2 = do
  t :~: n
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era n
r2
  n
predVal <- forall era t. Term era t -> Typed t
simplify Term era n
predExpr
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall t. Count t => t -> Gen t
genSucc n
predVal)
genCount v1 :: V era t
v1@(V String
_ Rep era t
r1 Access era s t
_) [Sized Term era Size
sz (Var v2 :: V era t
v2@(V String
_ Rep era t
EpochR Access era s t
_))] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 = do
  t :~: EpochNo
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 forall era. Rep era EpochNo
EpochR
  Size
size <- forall era t. Term era t -> Typed t
simplify Term era Size
sz
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ do
    Int
n <- Size -> Gen Int
genFromIntRange Size
size
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Word64 -> EpochNo
EpochNo forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n
genCount v1 :: V era t
v1@(V String
_ Rep era t
r1 Access era s t
_) [Sized Term era Size
sz (Var v2 :: V era t
v2@(V String
_ Rep era t
SlotNoR Access era s t
_))] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 = do
  t :~: SlotNo
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 forall era. Rep era SlotNo
SlotNoR
  Size
size <- forall era t. Term era t -> Typed t
simplify Term era Size
sz
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ do
    Int
n <- Size -> Gen Int
genFromIntRange Size
size
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Word64 -> SlotNo
SlotNo forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n
genCount v :: V era t
v@(V String
_ Rep era t
r Access era s t
_) [Pred era]
cs = forall a. [String] -> Typed a
failT [String]
zs
  where
    zs :: [String]
zs = (String
"Cannot solve: genCount " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show V era t
v forall a. [a] -> [a] -> [a]
++ String
" at type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era t
r forall a. [a] -> [a] -> [a]
++ String
" on Predicates") forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Pred era]
cs

-- | Used in solving Projections
data Update t where
  Update :: s -> Lens' t s -> Update t

update :: t -> [Update t] -> t
update :: forall t. t -> [Update t] -> t
update t
t [] = t
t
update t
t (Update s
s Lens' t s
l : [Update t]
more) = forall t. t -> [Update t] -> t
update (forall s t a b. ASetter s t a b -> b -> s -> t
Lens.set Lens' t s
l s
s t
t) [Update t]
more

anyToUpdate :: Rep era t1 -> (AnyF era t2) -> Typed (Update t1)
anyToUpdate :: forall era t1 t2. Rep era t1 -> AnyF era t2 -> Typed (Update t1)
anyToUpdate Rep era t1
rep1 (AnyF (FConst Rep era t
_ t
s Rep era t2
rep2 Lens' t2 t
l)) = do
  t1 :~: t2
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t1
rep1 Rep era t2
rep2
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s t. s -> Lens' t s -> Update t
Update t
s Lens' t2 t
l)
anyToUpdate Rep era t1
_ AnyF era t2
x = forall a. [String] -> Typed a
failT [String
"component is not FConst: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AnyF era t2
x]

intToNatural :: Int -> Natural
intToNatural :: Int -> Natural
intToNatural Int
n = forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n

isIf :: Pred era -> Bool
isIf :: forall era. Pred era -> Bool
isIf (If RootTarget era r Bool
_ Pred era
_ Pred era
_) = Bool
True
isIf Pred era
_ = Bool
False

-- ==================================================================================
-- Given a variable ('v1' :: 't') and [Pred] that constrain it. Produce a (Gen t)

-- | Dispatch on the type of the variable 'v1' being solved.
dispatch :: forall t era. (HasCallStack, Era era) => V era t -> [Pred era] -> Typed (Gen t)
dispatch :: forall t era.
(HasCallStack, Era era) =>
V era t -> [Pred era] -> Typed (Gen t)
dispatch V era t
v1 [Pred era]
preds | Just (If RootTarget era r Bool
tar Pred era
x Pred era
y) <- forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find forall era. Pred era -> Bool
isIf [Pred era]
preds = do
  Bool
b <- forall era t root. RootTarget era root t -> Typed t
simplifyTarget RootTarget era r Bool
tar
  let others :: [Pred era]
others = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Pred era -> Bool
isIf) [Pred era]
preds
  if Bool
b then forall t era.
(HasCallStack, Era era) =>
V era t -> [Pred era] -> Typed (Gen t)
dispatch V era t
v1 (Pred era
x forall a. a -> [a] -> [a]
: [Pred era]
others) else forall t era.
(HasCallStack, Era era) =>
V era t -> [Pred era] -> Typed (Gen t)
dispatch V era t
v1 (Pred era
y forall a. a -> [a] -> [a]
: [Pred era]
others)
dispatch v1 :: V era t
v1@(V String
nam Rep era t
r1 Access era s t
_) [Pred era]
preds = forall a. String -> Typed a -> Typed a
explain (String
"Solving for variable " forall a. [a] -> [a] -> [a]
++ String
nam forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Pred era]
preds)) forall a b. (a -> b) -> a -> b
$ case [Pred era]
preds of
  [Var V era a
v2 :=: Lit Rep era a
r2 a
t] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era a
v2 -> do
    t :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era a
r2
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
t)
  [Lit Rep era a
r2 a
t :=: Var V era a
v2] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era a
v2 -> do
    t :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era a
r2
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
t)
  [Term era a
expr :=: Var V era a
v2] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era a
v2 -> do
    t :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 (forall era t. Era era => Term era t -> Rep era t
termRep Term era a
expr)
    a
t <- forall era t. Term era t -> Typed t
simplify Term era a
expr
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
t)
  [Sized (Var v2 :: V era Size
v2@(V String
_ Rep era Size
r2 Access era s Size
_)) Term era t
term] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era Size
v2 -> do
    t :~: Size
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era Size
r2
    t
x <- forall era t. Term era t -> Typed t
simplify Term era t
term
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Size
SzExact (forall t. Sizeable t => t -> Int
getSize t
x))
  [Sized Term era Size
sizeterm (Var v2 :: V era t
v2@(V String
_ Rep era t
r2 Access era s t
_))] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> do
    t :~: t
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era t
r2
    Size
sz <- forall era t. Term era t -> Typed t
simplify Term era Size
sizeterm
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ do Int
n <- Size -> Gen Int
genFromSize Size
sz; forall era t. Int -> Rep era t -> Gen t
genSizedRep Int
n Rep era t
r2
  -- Here we solve for 'nm' by evaluating term, then use the 'lenz' to select the right component of 'x'
  -- then return that value to bind to 'nm'
  [cc :: Pred era
cc@(Component (Left Term era t
term) [AnyF (Field String
nm Rep era t
t Rep era t
_ Lens' t t
lenz)])] | forall era t. V era t -> Name era
Name V era t
v1 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
nm Rep era t
t forall era s t. Access era s t
No) -> forall a. String -> Typed a -> Typed a
explain (String
"Solving " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred era
cc) forall a b. (a -> b) -> a -> b
$ do
    t :~: t
Refl <- forall era s t. V era s -> V era t -> Typed (s :~: t)
sameV V era t
v1 (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
nm Rep era t
t forall era s t. Access era s t
No)
    t
x <- forall era t. Term era t -> Typed t
simplify Term era t
term
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) a. Applicative f => a -> f a
pure (t
x forall s a. s -> Getting a s a -> a
^. Lens' t t
lenz))
  [cc :: Pred era
cc@(Component (Right (Var V era t
v2)) [AnyF era t]
cs)] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> forall a. String -> Typed a -> Typed a
explain (String
"Solving " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred era
cc) forall a b. (a -> b) -> a -> b
$ do
    [Update t]
pairs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall era t1 t2. Rep era t1 -> AnyF era t2 -> Typed (Update t1)
anyToUpdate Rep era t
r1) [AnyF era t]
cs
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ do t
t <- forall era b. Rep era b -> Gen b
genRep Rep era t
r1; forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall t. t -> [Update t] -> t
update t
t [Update t]
pairs)
  [Component (Right (Var V era t
v2)) [AnyF era t]
cs, Random (Var V era t
v3)] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 Bool -> Bool -> Bool
&& forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v3 -> do
    [Update t]
pairs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall era t1 t2. Rep era t1 -> AnyF era t2 -> Typed (Update t1)
anyToUpdate Rep era t
r1) [AnyF era t]
cs
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ do
      t
t <- forall era b. Rep era b -> Gen b
genRep Rep era t
r1
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall t. t -> [Update t] -> t
update t
t [Update t]
pairs)
  [Random (Var V era t
v3), Component (Right (Var V era t
v2)) [AnyF era t]
cs] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 Bool -> Bool -> Bool
&& forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v3 -> do
    [Update t]
pairs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall era t1 t2. Rep era t1 -> AnyF era t2 -> Typed (Update t1)
anyToUpdate Rep era t
r1) [AnyF era t]
cs
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ do
      t
t <- forall era b. Rep era b -> Gen b
genRep Rep era t
r1
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall t. t -> [Update t] -> t
update t
t [Update t]
pairs)
  [Sized (Var V era Size
v2) (Lit Rep era t
SizeR t
x)] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era Size
v2 -> do
    t :~: Size
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 forall era. Rep era Size
SizeR
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Size
SzExact (forall t. Sizeable t => t -> Int
getSize t
x)))
  [Sized (Lit Rep era Size
SizeR Size
sz) (Var V era t
v2)] | forall era t. Rep era t -> Bool
isAddsType Rep era t
r1 Bool -> Bool -> Bool
&& forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> do
    With s t1
_ <- forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Adds (s t))
hasAdds Rep era t
r1 Rep era t
r1
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall x. Adds x => [String] -> Int -> x
fromI [String
"dispatch " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show V era t
v1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Pred era]
preds] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Size -> Gen Int
genFromIntRange Size
sz
  [GenFrom (Var v2 :: V era t
v2@(V String
_ Rep era t
r2 Access era s t
_)) RootTarget era r (Gen t)
target] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> do
    t :~: t
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era t
r2
    Gen t
x <- forall era t root. RootTarget era root t -> Typed t
simplifyTarget @era @(Gen t) RootTarget era r (Gen t)
target
    forall (f :: * -> *) a. Applicative f => a -> f a
pure Gen t
x
  [Var v2 :: V era t
v2@(V String
_ Rep era t
r2 Access era s t
_) :<-: RootTarget era r t
target] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> do
    t :~: t
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era t
r2
    t
x <- forall era t root. RootTarget era root t -> Typed t
simplifyTarget @era @t RootTarget era r t
target
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) a. Applicative f => a -> f a
pure t
x)
  [pred1 :: Pred era
pred1@(Member (Left (HashS (Var v2 :: V era (ScriptF era)
v2@(V String
_ (ScriptR Proof era
p) Access era s (ScriptF era)
_)))) (Dom Term era (Map a b)
expr))] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (ScriptF era)
v2 -> do
    t :~: ScriptF era
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 (forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR Proof era
p)
    case forall era t. Era era => Term era t -> Rep era t
termRep Term era (Map a b)
expr of
      mt :: Rep era (Map a b)
mt@(MapR Rep era a
ScriptHashR (ScriptR Proof era
_)) -> do
        Map a b
m <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era (Map a b)
mt Term era (Map a b)
expr
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"dispatch " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show V era t
v1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Pred era]
preds] Map a b
m)
      Rep era (Map a b)
other ->
        forall a. [String] -> Typed a
failT
          [String
"The Pred: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred era
pred1, String
"Can only be applied to a map whose range is 'Script'.", forall a. Show a => a -> String
show Rep era (Map a b)
other]
  [pred1 :: Pred era
pred1@(Member (Right (HashS (Var v2 :: V era (ScriptF era)
v2@(V String
_ (ScriptR Proof era
p) Access era s (ScriptF era)
_)))) (Dom Term era (Map a b)
expr))] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (ScriptF era)
v2 -> do
    t :~: ScriptF era
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 (forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR Proof era
p)
    case forall era t. Era era => Term era t -> Rep era t
termRep Term era (Map a b)
expr of
      mt :: Rep era (Map a b)
mt@(MapR Rep era a
ScriptHashR (ScriptR Proof era
_)) -> do
        Map a b
m <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era (Map a b)
mt Term era (Map a b)
expr
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"dispatch " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show V era t
v1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Pred era]
preds] Map a b
m)
      Rep era (Map a b)
other ->
        forall a. [String] -> Typed a
failT
          [String
"The Pred: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred era
pred1, String
"Can only be applied to a map whose range is 'Script'.", forall a. Show a => a -> String
show Rep era (Map a b)
other]
  [pred1 :: Pred era
pred1@(Member (Left (HashD (Var v2 :: V era (Data era)
v2@(V String
_ Rep era (Data era)
DataR Access era s (Data era)
_)))) (Dom Term era (Map a b)
expr))] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Data era)
v2 -> do
    t :~: Data era
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 forall era. Era era => Rep era (Data era)
DataR
    case forall era t. Era era => Term era t -> Rep era t
termRep Term era (Map a b)
expr of
      mt :: Rep era (Map a b)
mt@(MapR Rep era a
DataHashR Rep era b
DataR) -> do
        Map a b
m <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era (Map a b)
mt Term era (Map a b)
expr
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"dispatch " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show V era t
v1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Pred era]
preds] Map a b
m)
      Rep era (Map a b)
other ->
        forall a. [String] -> Typed a
failT
          [String
"The Pred: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred era
pred1, String
"Can only be applied to a map whose range is 'Data'.", forall a. Show a => a -> String
show Rep era (Map a b)
other]
  [pred1 :: Pred era
pred1@(Member (Right (HashD (Var v2 :: V era (Data era)
v2@(V String
_ Rep era (Data era)
DataR Access era s (Data era)
_)))) (Dom Term era (Map a b)
expr))] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era (Data era)
v2 -> do
    t :~: Data era
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 forall era. Era era => Rep era (Data era)
DataR
    case forall era t. Era era => Term era t -> Rep era t
termRep Term era (Map a b)
expr of
      mt :: Rep era (Map a b)
mt@(MapR Rep era a
DataHashR Rep era b
DataR) -> do
        Map a b
m <- forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era (Map a b)
mt Term era (Map a b)
expr
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"dispatch " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show V era t
v1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Pred era]
preds] Map a b
m)
      Rep era (Map a b)
other ->
        forall a. [String] -> Typed a
failT
          [String
"The Pred: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred era
pred1, String
"Can only be applied to a map whose range is 'Data'.", forall a. Show a => a -> String
show Rep era (Map a b)
other]
  [Member (Left (Var v2 :: V era a
v2@(V String
_ Rep era a
r2 Access era s a
_))) Term era (Set a)
expr] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era a
v2 -> do
    t :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era a
r2
    Set a
set <- forall era t. Term era t -> Typed t
simplify Term era (Set a)
expr
    let msgs :: [String]
msgs = (String
"Solving for variable " forall a. [a] -> [a] -> [a]
++ String
nam) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Pred era]
preds
    if forall a. Set a -> Bool
Set.null Set a
set
      then
        forall a. [String] -> Typed a
failT ((String
"The set is empty " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall era t. Era era => Term era t -> Rep era t
termRep Term era (Set a)
expr) Set a
set forall a. [a] -> [a] -> [a]
++ String
", can't find an element.") forall a. a -> [a] -> [a]
: [String]
msgs)
      else forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [String] -> Set a -> Gen (a, Set a)
itemFromSet [String]
msgs Set a
set)
  [Member (Right (Var v2 :: V era a
v2@(V String
_ Rep era a
r2 Access era s a
_))) Term era (Set a)
expr] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era a
v2 -> do
    t :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era a
r2
    Set a
set <- forall era t. Term era t -> Typed t
simplify Term era (Set a)
expr
    let msgs :: [String]
msgs = (String
"Solving for variable " forall a. [a] -> [a] -> [a]
++ String
nam) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Pred era]
preds
    if forall a. Set a -> Bool
Set.null Set a
set
      then
        forall a. [String] -> Typed a
failT ((String
"The set is empty " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall era t. Era era => Term era t -> Rep era t
termRep Term era (Set a)
expr) Set a
set forall a. [a] -> [a] -> [a]
++ String
", can't find an element.") forall a. a -> [a] -> [a]
: [String]
msgs)
      else forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [String] -> Set a -> Gen (a, Set a)
itemFromSet [String]
msgs Set a
set)
  [NotMember (Var v2 :: V era a
v2@(V String
_ Rep era a
r2 Access era s a
_)) Term era (Set a)
expr] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era a
v2 -> do
    t :~: a
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era a
r2
    Set a
set <- forall era t. Term era t -> Typed t
simplify Term era (Set a)
expr
    let msgs :: [String]
msgs = (String
"Solving for variable " forall a. [a] -> [a] -> [a]
++ String
nam) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Pred era]
preds
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. [String] -> Gen a -> (a -> Bool) -> Gen a
suchThatErr [String]
msgs (forall era b. Rep era b -> Gen b
genRep Rep era a
r2) (forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set a
set)
  [MapMember (Var v2 :: V era k
v2@(V String
_ Rep era k
r2 Access era s k
_)) Term era v
exprVal Direct (Term era (Map k v))
exprMap] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era k
v2 -> do
    t :~: k
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era k
r2
    Map k v
m <- forall era t. Term era t -> Typed t
simplify (forall a. Direct a -> a
direct Direct (Term era (Map k v))
exprMap)
    v
v <- forall era t. Term era t -> Typed t
simplify Term era v
exprVal
    let m2 :: Map k v
m2 = forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (forall a. Eq a => a -> a -> Bool
== v
v) Map k v
m
    let msgs :: [String]
msgs = (String
"Solving for variable " forall a. [a] -> [a] -> [a]
++ String
nam) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Pred era]
preds
    if forall k a. Map k a -> Bool
Map.null Map k v
m2
      then
        forall a. [String] -> Typed a
failT ((String
"The value: " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall era t. Era era => Term era t -> Rep era t
termRep Term era v
exprVal) v
v forall a. [a] -> [a] -> [a]
++ String
" is not in the range of the map.") forall a. a -> [a] -> [a]
: [String]
msgs)
      else forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [String] -> Set a -> Gen (a, Set a)
itemFromSet [String]
msgs (forall k a. Map k a -> Set k
Map.keysSet Map k v
m2))
  [MapMember Term era k
exprKey (Var v2 :: V era v
v2@(V String
_ Rep era v
r2 Access era s v
_)) Direct (Term era (Map k v))
exprMap] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era v
v2 -> do
    t :~: v
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era v
r2
    Map k v
m <- forall era t. Term era t -> Typed t
simplify (forall a. Direct a -> a
direct Direct (Term era (Map k v))
exprMap)
    k
k <- forall era t. Term era t -> Typed t
simplify Term era k
exprKey
    let msgs :: [String]
msgs = (String
"Solving for variable " forall a. [a] -> [a] -> [a]
++ String
nam) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Pred era]
preds
    case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k Map k v
m of
      Just v
v -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) a. Applicative f => a -> f a
pure v
v)
      Maybe v
Nothing -> forall a. [String] -> Typed a
failT ((String
"The key: " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall era t. Era era => Term era t -> Rep era t
termRep Term era k
exprKey) k
k forall a. [a] -> [a] -> [a]
++ String
" is not in the map.") forall a. a -> [a] -> [a]
: [String]
msgs)
  [List (Var v2 :: V era fs
v2@(V String
_ (MaybeR Rep era t1
r2) Access era s fs
_)) [Term era t]
expr] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era fs
v2 -> do
    t :~: Maybe t1
Refl <- forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 (forall era t1. Rep era t1 -> Rep era (Maybe t1)
MaybeR Rep era t1
r2)
    [t]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall era t. Term era t -> Typed t
simplify [Term era t]
expr
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall ts a. FromList ts a => [a] -> ts
makeFromList [t]
xs)
  [Random (Var V era t
v2)] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era b. Rep era b -> Gen b
genRep Rep era t
r1
  [p1 :: Pred era
p1@(Member (Left (Var V era a
v2)) Term era (Set a)
y), p2 :: Pred era
p2@(NotMember (Var V era a
v3) Term era (Set a)
z)]
    | Just t :~: a
Refl <- forall era t s. V era t -> V era s -> Maybe (t :~: s)
sameName V era t
v1 V era a
v2
    , Just t :~: a
Refl <- forall era t s. V era t -> V era s -> Maybe (t :~: s)
sameName V era t
v1 V era a
v3 -> do
        Set a
yval <- forall era t. Term era t -> Typed t
simplify Term era (Set a)
y
        Set a
zval <- forall era t. Term era t -> Typed t
simplify Term era (Set a)
z
        forall (f :: * -> *) a. Applicative f => a -> f a
pure
          ( forall a b. (a, b) -> a
fst
              forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [String] -> Set a -> Gen (a, Set a)
itemFromSet
                [String
"Solving (Member & NotMember), for variable " forall a. [a] -> [a] -> [a]
++ String
nam, forall a. Show a => a -> String
show Pred era
p1, forall a. Show a => a -> String
show Pred era
p2]
                (forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set a
yval Set a
zval)
          )
  [nm :: Pred era
nm@(NotMember {}), m :: Pred era
m@(Member {})] -> forall t era.
(HasCallStack, Era era) =>
V era t -> [Pred era] -> Typed (Gen t)
dispatch V era t
v1 [Pred era
m, Pred era
nm]
  [Pred era
x, Random (Var V era t
v2)] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> forall t era.
(HasCallStack, Era era) =>
V era t -> [Pred era] -> Typed (Gen t)
dispatch V era t
v1 [Pred era
x]
  [Random (Var V era t
v2), Pred era
x] | forall era t. V era t -> Name era
Name V era t
v1 forall a. Eq a => a -> a -> Bool
== forall era t. V era t -> Name era
Name V era t
v2 -> forall t era.
(HasCallStack, Era era) =>
V era t -> [Pred era] -> Typed (Gen t)
dispatch V era t
v1 [Pred era
x]
  [Pred era]
cs -> case Rep era t
r1 of
    MapR Rep era a
dom Rep era b
rng -> do
      MapSpec era a b
spec <- forall era dom rng.
(Era era, Ord dom) =>
V era (Map dom rng) -> [Pred era] -> Typed (MapSpec era dom rng)
solveMaps V era t
v1 [Pred era]
cs
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era w dom.
(Era era, Ord dom) =>
String
-> [String]
-> Gen dom
-> Gen w
-> MapSpec era dom w
-> Gen (Map dom w)
genFromMapSpec String
nam (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Pred era]
cs) (forall era b. Rep era b -> Gen b
genRep Rep era a
dom) (forall era b. Rep era b -> Gen b
genRep Rep era b
rng) MapSpec era a b
spec
    SetR Rep era a
r -> do
      SetSpec era a
spec <- forall era a.
Era era =>
V era (Set a) -> [Pred era] -> Typed (SetSpec era a)
solveSets V era t
v1 [Pred era]
cs
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era a.
Era era =>
[String] -> Gen a -> SetSpec era a -> Gen (Set a)
genFromSetSpec [] (forall era b. Rep era b -> Gen b
genRep Rep era a
r) SetSpec era a
spec
    ListR Rep era a
r -> do
      ListSpec era a
spec <- forall era a.
Era era =>
V era [a] -> [Pred era] -> Typed (ListSpec era a)
solveLists V era t
v1 [Pred era]
cs
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era r. [String] -> Gen r -> ListSpec era r -> Gen [r]
genFromListSpec [] (forall era b. Rep era b -> Gen b
genRep Rep era a
r) ListSpec era a
spec
    Rep era t
_other
      | forall era t. Rep era t -> Bool
isAddsType Rep era t
r1 -> do
          With s t1
v2 <- forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Adds (s t))
hasAdds Rep era t
r1 V era t
v1
          AddsSpec t1
sumv <- forall t era.
(Adds t, Era era) =>
V era t -> [Pred era] -> Typed (AddsSpec t)
solveSums s t1
v2 [Pred era]
cs
          let msgs :: [String]
msgs = (String
"Solving for variable " forall a. [a] -> [a] -> [a]
++ String
nam) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Pred era]
preds
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall x. Adds x => [String] -> AddsSpec x -> Gen x
genAdds [String]
msgs AddsSpec t1
sumv
      | forall era t. Rep era t -> Bool
isCountType Rep era t
r1 -> do
          With s t1
v2 <- forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Count (s t))
hasCount Rep era t
r1 V era t
v1
          forall t era. Count t => V era t -> [Pred era] -> Typed (Gen t)
genCount s t1
v2 [Pred era]
cs
      | Bool
otherwise ->
          forall a. [String] -> Typed a
failT
            [ String
"No solution for "
                forall a. [a] -> [a] -> [a]
++ String
nam
                forall a. [a] -> [a] -> [a]
++ String
" at type "
                forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era t
r1
                forall a. [a] -> [a] -> [a]
++ String
" for conditions:\n"
                forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. (a -> a -> Bool) -> [a] -> [a]
List.nubBy forall era. Era era => Pred era -> Pred era -> Bool
cpeq [Pred era]
cs)
            ]

genOrFail ::
  Era era =>
  Bool ->
  Either [String] (Subst era) ->
  ([Name era], [Pred era]) ->
  Gen (Either [String] (Subst era))
genOrFail :: forall era.
Era era =>
Bool
-> Either [String] (Subst era)
-> ([Name era], [Pred era])
-> Gen (Either [String] (Subst era))
genOrFail Bool
loud (Right Subst era
subst) ([Name v :: V era t
v@(V String
_ Rep era t
rep Access era s t
_)], [Pred era]
conds) =
  case forall x. Typed x -> Either [String] x
runTyped forall a b. (a -> b) -> a -> b
$
    forall a. Bool -> String -> a -> a
ifTrace
      Bool
loud
      (Int -> String -> String
pad Int
20 (forall a. Show a => a -> String
show (forall era t. V era t -> Name era
Name V era t
v)) 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
"," (forall a b. (a -> b) -> [a] -> [b]
map (forall era. Subst era -> Pred era -> Pred era
substPred Subst era
subst) [Pred era]
conds))
      (forall t era.
(HasCallStack, Era era) =>
V era t -> [Pred era] -> Typed (Gen t)
dispatch V era t
v (forall a b. (a -> b) -> [a] -> [b]
map (forall era. Subst era -> Pred era -> Pred era
substPred Subst era
subst) [Pred era]
conds)) of
    Right Gen t
gen -> do
      t
t <- Gen t
gen
      forall a. Bool -> String -> a -> a
ifTrace
        Bool
loud
        (String
"   " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era t
rep t
t)
        (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right (forall era t. V era t -> Term era t -> Subst era -> Subst era
extend V era t
v (forall era t. Rep era t -> t -> Term era t
Lit Rep era t
rep t
t) Subst era
subst)))
    Left [String]
msgs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left [String]
msgs)
genOrFail Bool
_ (Right Subst era
_) ([Name era]
names, [Pred era]
_) = forall a. HasCallStack => String -> a
error (String
"Multiple names not handed yet " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name era]
names)
genOrFail Bool
_ (Left [String]
msgs) ([Name era], [Pred era])
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> Either a b
Left [String]
msgs)

genOrFailList ::
  Era era =>
  Bool ->
  Either [String] (Subst era) ->
  [([Name era], [Pred era])] ->
  Gen (Either [String] (Subst era))
genOrFailList :: forall era.
Era era =>
Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
genOrFailList Bool
loud = forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' (forall era.
Era era =>
Bool
-> Either [String] (Subst era)
-> ([Name era], [Pred era])
-> Gen (Either [String] (Subst era))
genOrFail Bool
loud)

genDependGraph :: Bool -> Proof era -> DependGraph era -> Gen (Either [String] (Subst era))
genDependGraph :: forall era.
Bool
-> Proof era
-> DependGraph era
-> Gen (Either [String] (Subst era))
genDependGraph Bool
loud Proof era
Shelley (DependGraph [([Name era], [Pred era])]
pairs) = forall era.
Era era =>
Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
genOrFailList Bool
loud (forall a b. b -> Either a b
Right forall era. Subst era
emptySubst) [([Name era], [Pred era])]
pairs
genDependGraph Bool
loud Proof era
Allegra (DependGraph [([Name era], [Pred era])]
pairs) = forall era.
Era era =>
Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
genOrFailList Bool
loud (forall a b. b -> Either a b
Right forall era. Subst era
emptySubst) [([Name era], [Pred era])]
pairs
genDependGraph Bool
loud Proof era
Mary (DependGraph [([Name era], [Pred era])]
pairs) = forall era.
Era era =>
Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
genOrFailList Bool
loud (forall a b. b -> Either a b
Right forall era. Subst era
emptySubst) [([Name era], [Pred era])]
pairs
genDependGraph Bool
loud Proof era
Alonzo (DependGraph [([Name era], [Pred era])]
pairs) = forall era.
Era era =>
Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
genOrFailList Bool
loud (forall a b. b -> Either a b
Right forall era. Subst era
emptySubst) [([Name era], [Pred era])]
pairs
genDependGraph Bool
loud Proof era
Babbage (DependGraph [([Name era], [Pred era])]
pairs) = forall era.
Era era =>
Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
genOrFailList Bool
loud (forall a b. b -> Either a b
Right forall era. Subst era
emptySubst) [([Name era], [Pred era])]
pairs
genDependGraph Bool
loud Proof era
Conway (DependGraph [([Name era], [Pred era])]
pairs) = forall era.
Era era =>
Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
genOrFailList Bool
loud (forall a b. b -> Either a b
Right forall era. Subst era
emptySubst) [([Name era], [Pred era])]
pairs

-- | Solve for one variable, and add its solution to the substitution
solveOneVar :: Era era => Subst era -> ([Name era], [Pred era]) -> Gen (Subst era)
solveOneVar :: forall era.
Era era =>
Subst era -> ([Name era], [Pred era]) -> Gen (Subst era)
solveOneVar Subst era
subst ([Name (v :: V era t
v@(V String
_ Rep era t
r Access era s t
_))], [Pred era]
ps) = do
  !Gen t
genOneT <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall t era.
(HasCallStack, Era era) =>
V era t -> [Pred era] -> Typed (Gen t)
dispatch V era t
v (forall a b. (a -> b) -> [a] -> [b]
map (forall era. Subst era -> Pred era -> Pred era
substPred Subst era
subst) [Pred era]
ps)) -- Sub solution for previously solved variables
  !t
t <- Gen t
genOneT
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era t. V era t -> Term era t -> Subst era -> Subst era
extend V era t
v (forall era t. Rep era t -> t -> Term era t
Lit Rep era t
r t
t) Subst era
subst)
solveOneVar Subst era
subst0 ([Name era]
names, [Pred era]
preds) = case ([Name era]
names, forall a b. (a -> b) -> [a] -> [b]
map (forall era. Subst era -> Pred era -> Pred era
substPred Subst era
subst0) [Pred era]
preds) of
  ([Name era]
ns, [SumSplit c
small Term era c
tot OrdCond
EQL [Sum era c]
suml]) | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name era]
ns forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sum era c]
suml -> do
    !c
n <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era t. Term era t -> Typed t
simplify Term era c
tot
    ![c]
zs <-
      forall x. Adds x => x -> [String] -> Int -> x -> Gen [x]
partition
        c
small
        [String
"Partition, while solving multiple SumsTo vars.", forall a. Show a => a -> String
show [Name era]
ns, forall a. Show a => a -> String
show [Pred era]
preds]
        (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name era]
ns)
        c
n
    let rep :: Rep era c
rep = forall era t. Era era => Term era t -> Rep era t
termRep Term era c
tot
    forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' (\ !Subst era
sub (!Sum era c
sumx, !c
x) -> forall x era.
Adds x =>
Sum era x -> Rep era x -> x -> Subst era -> Gen (Subst era)
genSum (forall era t. Subst era -> Sum era t -> Sum era t
substSum Subst era
sub Sum era c
sumx) Rep era c
rep c
x Subst era
sub) Subst era
subst0 (forall a b. [a] -> [b] -> [(a, b)]
zip [Sum era c]
suml [c]
zs)
  ([Name era]
ns, [Pred era]
ps) -> forall a. HasCallStack => String -> [String] -> a
errorMess String
"Not yet. multiple vars in solveOneVar" [forall a. Show a => a -> String
show [Name era]
ns, forall a. Show a => a -> String
show [Pred era]
ps]

toolChainSub :: Era era => Proof era -> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub :: forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
_proof OrderInfo
order [Pred era]
cs Subst era
subst0 = do
  (Int
_count, DependGraph [([Name era], [Pred era])]
pairs) <- forall era.
Era era =>
OrderInfo -> Subst era -> [Pred era] -> Gen (Int, DependGraph era)
compileGenWithSubst OrderInfo
order Subst era
subst0 [Pred era]
cs
  Subst Map String (SubstElem era)
subst <- forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' forall era.
Era era =>
Subst era -> ([Name era], [Pred era]) -> Gen (Subst era)
solveOneVar Subst era
subst0 [([Name era], [Pred era])]
pairs
  let isTempV :: t Char -> Bool
isTempV t Char
k = Bool -> Bool
not (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
'.' t Char
k)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (forall era. Map String (SubstElem era) -> Subst era
Subst (forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\String
k SubstElem era
_ -> forall {t :: * -> *}. Foldable t => t Char -> Bool
isTempV String
k) Map String (SubstElem era)
subst))

toolChain :: Era era => Proof era -> OrderInfo -> [Pred era] -> Subst era -> Gen (Env era)
toolChain :: forall era.
Era era =>
Proof era -> OrderInfo -> [Pred era] -> Subst era -> Gen (Env era)
toolChain Proof era
_proof OrderInfo
order [Pred era]
cs Subst era
subst0 = do
  (Int
_count, DependGraph [([Name era], [Pred era])]
pairs) <- forall era.
Era era =>
OrderInfo -> Subst era -> [Pred era] -> Gen (Int, DependGraph era)
compileGenWithSubst OrderInfo
order Subst era
subst0 [Pred era]
cs
  Subst era
subst <- forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' forall era.
Era era =>
Subst era -> ([Name era], [Pred era]) -> Gen (Subst era)
solveOneVar Subst era
subst0 [([Name era], [Pred era])]
pairs
  forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst forall era. Env era
emptyEnv