{-# 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 -> String -> a -> a
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 = HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t))
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t)))
-> HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t))
forall a b. (a -> b) -> a -> b
$ s t -> HasConstraint Adds (s t)
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 = HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t))
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t)))
-> HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t))
forall a b. (a -> b) -> a -> b
$ s t -> HasConstraint Adds (s t)
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 = HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t))
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t)))
-> HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t))
forall a b. (a -> b) -> a -> b
$ s t -> HasConstraint Adds (s t)
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 = HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t))
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t)))
-> HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t))
forall a b. (a -> b) -> a -> b
$ s t -> HasConstraint Adds (s t)
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 = HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t))
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t)))
-> HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t))
forall a b. (a -> b) -> a -> b
$ s t -> HasConstraint Adds (s t)
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 = HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t))
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t)))
-> HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t))
forall a b. (a -> b) -> a -> b
$ s t -> HasConstraint Adds (s t)
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 = HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t))
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t)))
-> HasConstraint Adds (s t) -> Typed (HasConstraint Adds (s t))
forall a b. (a -> b) -> a -> b
$ s t -> HasConstraint Adds (s t)
forall (c :: * -> Constraint) t1 (s :: * -> *).
c t1 =>
s t1 -> HasConstraint c (s t1)
With s t
x
hasAdds Rep era t
r s t
_ = [String] -> Typed (HasConstraint Adds (s t))
forall a. [String] -> Typed a
failT [Rep era t -> String
forall a. Show a => a -> String
show Rep era t
r String -> String -> String
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 Rep era t -> Rep era t -> Typed (HasConstraint Adds (Rep era t))
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 = HasConstraint Count (s t) -> Typed (HasConstraint Count (s t))
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasConstraint Count (s t) -> Typed (HasConstraint Count (s t)))
-> HasConstraint Count (s t) -> Typed (HasConstraint Count (s t))
forall a b. (a -> b) -> a -> b
$ s t -> HasConstraint Count (s t)
forall (c :: * -> Constraint) t1 (s :: * -> *).
c t1 =>
s t1 -> HasConstraint c (s t1)
With s t
x
hasCount (ProtVerR Proof era
_) s t
x = HasConstraint Count (s t) -> Typed (HasConstraint Count (s t))
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasConstraint Count (s t) -> Typed (HasConstraint Count (s t)))
-> HasConstraint Count (s t) -> Typed (HasConstraint Count (s t))
forall a b. (a -> b) -> a -> b
$ s t -> HasConstraint Count (s t)
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 = HasConstraint Count (s t) -> Typed (HasConstraint Count (s t))
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasConstraint Count (s t) -> Typed (HasConstraint Count (s t)))
-> HasConstraint Count (s t) -> Typed (HasConstraint Count (s t))
forall a b. (a -> b) -> a -> b
$ s t -> HasConstraint Count (s t)
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 = HasConstraint Count (s t) -> Typed (HasConstraint Count (s t))
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HasConstraint Count (s t) -> Typed (HasConstraint Count (s t)))
-> HasConstraint Count (s t) -> Typed (HasConstraint Count (s t))
forall a b. (a -> b) -> a -> b
$ s t -> HasConstraint Count (s t)
forall (c :: * -> Constraint) t1 (s :: * -> *).
c t1 =>
s t1 -> HasConstraint c (s t1)
With s t
x
hasCount Rep era t
r s t
_ = [String] -> Typed (HasConstraint Count (s t))
forall a. [String] -> Typed a
failT [Rep era t -> String
forall a. Show a => a -> String
show Rep era t
r String -> String -> String
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 Rep era t -> Rep era t -> Typed (HasConstraint Count (Rep era t))
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 Rep era i -> Rep era j -> Maybe (i :~: j)
forall i j. Rep era i -> Rep era j -> Maybe (i :~: j)
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 -> (i :~: j) -> Typed (i :~: j)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure i :~: j
x
  Maybe (i :~: j)
Nothing -> [String] -> Typed (i :~: j)
forall a. [String] -> Typed a
failT [String
"Type error in sameRep:\n  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rep era i -> String
forall a. Show a => a -> String
show Rep era i
r1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" =/=\n  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rep era j -> String
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 <- Term era t -> Typed t
forall era t. Term era t -> Typed t
simplify Term era t
term
  s :~: t
Refl <- Rep era s -> Rep era t -> Typed (s :~: t)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era s
r1 (Term era t -> Rep era t
forall era t. Era era => Term era t -> Rep era t
termRep Term era t
term)
  s -> Typed s
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure s
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 <- Term era y -> Typed y
forall era t. Term era t -> Typed t
simplify Term era y
term
  Set rng :~: y
Refl <- Rep era (Set rng) -> Rep era y -> Typed (Set rng :~: y)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep (Rep era rng -> Rep era (Set rng)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era rng
r1) (Term era y -> Rep era y
forall era t. Era era => Term era t -> Rep era t
termRep Term era y
term)
  HasConstraint Ord (Set rng) -> Typed (HasConstraint Ord (Set rng))
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set rng -> HasConstraint Ord (Set rng)
forall (c :: * -> Constraint) t1 (s :: * -> *).
c t1 =>
s t1 -> HasConstraint c (s t1)
With y
Set rng
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 <- Term era y -> Typed y
forall era t. Term era t -> Typed t
simplify Term era y
term
  [rng] :~: y
Refl <- Rep era [rng] -> Rep era y -> Typed ([rng] :~: y)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep (Rep era rng -> Rep era [rng]
forall era a. Rep era a -> Rep era [a]
ListR Rep era rng
r1) (Term era y -> Rep era y
forall era t. Era era => Term era t -> Rep era t
termRep Term era y
term)
  Rep era rng -> [rng] -> Typed (HasConstraint Eq [rng])
forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Eq (s t))
hasEq Rep era rng
r1 y
[rng]
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 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a c) -> Name era
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 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a x) -> Name era
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 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((a -> Bool) -> [a] -> [a]
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 <- (a -> Gen dom) -> [a] -> Gen [dom]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM a -> Gen dom
genThenOverwriteA (Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
setA)
  [(dom, rng)]
pairs <- (dom -> Gen (dom, rng)) -> [dom] -> Gen [(dom, rng)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\dom
d -> do rng
r <- Rep era rng -> Gen rng
forall era b. Rep era b -> Gen b
genRep Rep era rng
repRng; (dom, rng) -> Gen (dom, rng)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (dom
d, rng
r)) [dom]
ds
  Map dom rng -> Gen (Map dom rng)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(dom, rng)] -> Map dom rng
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(dom, rng)]
pairs)
  where
    genThenOverwriteA :: a -> Gen dom
genThenOverwriteA a
a = ASetter dom dom a a -> a -> dom -> dom
forall s t a b. ASetter s t a b -> b -> s -> t
Lens.set ASetter dom dom a a
Lens' dom a
lensDomA a
a (dom -> dom) -> Gen dom -> Gen dom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rep era dom -> Gen dom
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 = c -> c -> c
forall x. Adds x => x -> x -> x
add c
c (c -> c) -> Gen c -> Gen c
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rep era c -> Gen c
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 = String
-> Typed (MapSpec era dom rng) -> Typed (MapSpec era dom rng)
forall a. String -> Typed a -> Typed a
explain String
msg (Typed (MapSpec era dom rng) -> Typed (MapSpec era dom rng))
-> Typed (MapSpec era dom rng) -> Typed (MapSpec era dom rng)
forall a b. (a -> b) -> a -> b
$ case Pred era
predicate of
  (Before (Lit Rep era a
_ a
_) (Var V era b
v2)) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era b -> Name era
forall era t. V era t -> Name era
Name V era b
v2 -> MapSpec era dom rng -> Typed (MapSpec era dom rng)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure MapSpec era dom rng
forall a. Monoid a => a
mempty
  (Sized (Lit Rep era Size
SizeR Size
sz) (Var V era t
v2))
    | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom 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
sz RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
forall era rng. RngSpec era rng
RngAny
  (Sized (Lit Rep era Size
SizeR Size
sz) (Dom (Var V era (Map a b)
v2)))
    | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom 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
sz RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
forall era rng. RngSpec era rng
RngAny
  (Var V era a
v2 :=: Term era a
expr) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era a -> Name era
forall era t. V era t -> Name era
Name V era a
v2 -> do
    Map dom rng
m1 <- Rep era (Map dom rng) -> Term era a -> Typed (Map dom rng)
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
_ <- Rep era b -> Rep era b -> Typed (HasConstraint Eq (Rep era b))
forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Eq (s t))
hasEq Rep era b
rng Rep era b
rng
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom 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 (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era dom
Rep era a
dom (Map dom rng -> Set dom
forall k a. Map k a -> Set k
Map.keysSet Map dom rng
m1)) PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny (Rep era rng -> [rng] -> RngSpec era rng
forall rng era. Eq rng => Rep era rng -> [rng] -> RngSpec era rng
RngElem Rep era rng
Rep era b
rng (Map dom rng -> [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
_)) -> V era (Map dom rng) -> Pred era -> Typed (MapSpec era dom rng)
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 Term era a -> Term era a -> Pred era
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) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    Map dom rng :~: Map a b
Refl <- Rep era (Map dom rng)
-> Rep era (Map a b) -> Typed (Map dom rng :~: Map a b)
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 <- Rep era [b] -> Term era a -> Typed [b]
forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType (Rep era b -> Rep era [b]
forall era a. Rep era a -> Rep era [a]
ListR Rep era b
rng) Term era a
expr
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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 ([b] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
l)) RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny (Rep era rng -> [rng] -> RngSpec era rng
forall rng era. Eq rng => Rep era rng -> [rng] -> RngSpec era rng
RngElem Rep era rng
Rep era b
rng [rng]
[b]
l)
  (Term era a
expr :=: Elems Term era (Map a b)
v2) -> V era (Map dom rng) -> Pred era -> Typed (MapSpec era dom rng)
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 (Map a b) -> Term era [b]
forall a b era. (Ord a, Eq b) => Term era (Map a b) -> Term era [b]
Elems Term era (Map a b)
v2 Term era [b] -> Term era [b] -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era a
Term era [b]
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)
_))) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
a Rep era a
dom
    a
val1 <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify Term era a
expr1
    Set a
val2 <- Term era (Set a) -> Typed (Set a)
forall era t. Term era t -> Typed t
simplify Term era (Set a)
expr2
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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 (Map dom b -> Int
forall k a. Map k a -> Int
Map.size a
Map dom b
val1)) (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era dom
Rep era a
dom Set dom
Set a
val2) PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
forall era rng. RngSpec era rng
RngAny
  (Restrict Term era (Set a)
expr1 Term era (Map a b)
expr2 :=: Term era a
expr3) -> V era (Map dom rng) -> Pred era -> Typed (MapSpec era dom rng)
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 Term era a -> Term era a -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
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) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
brep
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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 (Set t1 -> Int
forall a. Set a -> Int
Set.size a
Set t1
x)) (Lens' dom t1
-> Rep era dom -> Rep era t1 -> RelSpec era t1 -> RelSpec era dom
forall b dom era.
Ord b =>
Lens' dom b
-> Rep era dom -> Rep era b -> RelSpec era b -> RelSpec era dom
RelLens (t1 -> f t1) -> dom -> f dom
(t1 -> f t1) -> b -> f b
Lens' dom t1
Lens' b t1
lensbt Rep era dom
Rep era a
dom Rep era t1
trep (Rep era t1 -> Set t1 -> RelSpec era t1
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era t1
Rep era a
drep a
Set t1
x)) PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
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))
    | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
brep
        Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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 (Map a b -> Int
forall k a. Map k a -> Int
Map.size Map a b
x))
          (Lens' dom t1
-> Rep era dom -> Rep era t1 -> RelSpec era t1 -> RelSpec era dom
forall b dom era.
Ord b =>
Lens' dom b
-> Rep era dom -> Rep era b -> RelSpec era b -> RelSpec era dom
RelLens (t1 -> f t1) -> dom -> f dom
(t1 -> f t1) -> b -> f b
Lens' dom t1
Lens' b t1
lensbt Rep era dom
Rep era a
dom Rep era t1
trep (Rep era t1 -> Set t1 -> RelSpec era t1
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era t1
Rep era a
drep (Map t1 b -> Set t1
forall k a. Map k a -> Set k
Map.keysSet Map t1 b
Map a b
x)))
          PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny
          RngSpec era rng
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))
    | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
brep
        Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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 (Map a b -> Int
forall k a. Map k a -> Int
Map.size Map a b
x))
          (Lens' dom t1
-> Rep era dom -> Rep era t1 -> RelSpec era t1 -> RelSpec era dom
forall b dom era.
Ord b =>
Lens' dom b
-> Rep era dom -> Rep era b -> RelSpec era b -> RelSpec era dom
RelLens (t1 -> f t1) -> dom -> f dom
(t1 -> f t1) -> b -> f b
Lens' dom t1
Lens' b t1
lensbt Rep era dom
Rep era a
dom Rep era t1
trep (Rep era t1 -> Set t1 -> RelSpec era t1
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era t1
Rep era a
drep (Map t1 b -> Set t1
forall k a. Map k a -> Set k
Map.keysSet Map t1 b
Map a b
x)))
          PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny
          RngSpec era rng
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)
_))) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
brep
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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 (Set a -> Int
forall a. Set a -> Int
Set.size a
Set a
x)) (Lens' dom t1
-> Rep era dom -> Rep era t1 -> RelSpec era t1 -> RelSpec era dom
forall b dom era.
Ord b =>
Lens' dom b
-> Rep era dom -> Rep era b -> RelSpec era b -> RelSpec era dom
RelLens (t1 -> f t1) -> dom -> f dom
(t1 -> f t1) -> b -> f b
Lens' dom t1
Lens' b t1
lensbt Rep era dom
Rep era a
dom Rep era t1
trep (Rep era t1 -> Set t1 -> RelSpec era t1
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
Rep era t1
drep a
Set t1
x)) PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
forall era rng. RngSpec era rng
RngAny
  (Term era a
expr :=: Rng (Var V era (Map a b)
v2))
    | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        a
s <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify Term era a
expr
        let SetR Rep era b
Rep era a
a = Term era a -> Rep era a
forall era t. Era era => Term era t -> Rep era t
termRep Term era a
expr
        b :~: b
Refl <- Rep era b -> Rep era b -> Typed (b :~: b)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
rng Rep era b
a
        Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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 (Set rng -> Int
forall a. Set a -> Int
Set.size a
Set rng
s)) RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny (RelSpec era rng -> RngSpec era rng
forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (Rep era rng -> Set rng -> RelSpec era rng
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era rng
Rep era b
rng a
Set rng
s))
  (Rng (Var V era (Map a b)
v2) :=: Term era a
expr)
    | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        a
s <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify Term era a
expr
        let SetR Rep era b
Rep era a
a = Term era a -> Rep era a
forall era t. Era era => Term era t -> Rep era t
termRep Term era a
expr
        b :~: b
Refl <- Rep era b -> Rep era b -> Typed (b :~: b)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
rng Rep era b
a
        Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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 (Set rng -> Int
forall a. Set a -> Int
Set.size a
Set rng
s)) RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny (RelSpec era rng -> RngSpec era rng
forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (Rep era rng -> Set rng -> RelSpec era rng
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era rng
Rep era b
rng a
Set rng
s))
  (Rng (Var V era (Map a b)
v2) `Subset` Term era (Set a)
expr)
    | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        With s t1
_ <- Rep era b -> Rep era b -> Typed (HasConstraint Ord (Rep era b))
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 <- Rep era b -> Term era (Set a) -> Typed (HasConstraint Ord (Set b))
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
        Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom 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 RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny (RelSpec era rng -> RngSpec era rng
forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (Rep era rng -> Set rng -> RelSpec era rng
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era rng
Rep era b
rng s t1
Set rng
n))
  (Term era (Set a)
expr `Subset` Rng (Var V era (Map a b)
v2))
    | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        With s t1
_ <- Rep era b -> Rep era b -> Typed (HasConstraint Ord (Rep era b))
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 <- Rep era b -> Term era (Set a) -> Typed (HasConstraint Ord (Set b))
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
        Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom 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 RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny (RelSpec era rng -> RngSpec era rng
forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (Rep era rng -> Set rng -> RelSpec era rng
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era rng
Rep era b
rng s t1
Set rng
n))
  (Rng Term era (Map a b)
expr `Subset` (Var V era (Set a)
v2))
    | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
        With s t1
_ <- Rep era b -> Rep era b -> Typed (HasConstraint Ord (Rep era b))
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 <- Rep era b
-> Term era (Map a b) -> Typed (HasConstraint Ord (Set b))
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
        Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom 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 RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny (RelSpec era rng -> RngSpec era rng
forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (Rep era rng -> Set rng -> RelSpec era rng
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era rng
Rep era b
rng s t1
Set rng
n))
  (Term era a
expr :=: Dom (Var V era (Map a b)
v2))
    | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
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 = Term era a -> Rep era a
forall era t. Era era => Term era t -> Rep era t
termRep Term era a
expr
        a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
a
        a
mm <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify Term era a
expr
        Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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 (Set dom -> Int
forall a. Set a -> Int
Set.size a
Set dom
mm)) (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era dom
Rep era a
dom a
Set dom
mm) PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
forall era rng. RngSpec era rng
RngAny
  (Dom (Var V era (Map a b)
v2) :=: Term era a
expr)
    | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
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 = Term era a -> Rep era a
forall era t. Era era => Term era t -> Rep era t
termRep Term era a
expr
        a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
a
        a
mm <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify Term era a
expr
        Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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 (Set dom -> Int
forall a. Set a -> Int
Set.size a
Set dom
mm)) (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era dom
Rep era a
dom a
Set dom
mm) PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
forall era rng. RngSpec era rng
RngAny
  (Dom (Var V era (Map a b)
v2) `Subset` Term era (Set a)
expr)
    | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        With s t1
_ <- Rep era a -> Rep era a -> Typed (HasConstraint Ord (Rep era a))
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 <- Rep era a -> Term era (Set a) -> Typed (HasConstraint Ord (Set a))
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
        Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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 (Set t1 -> Int
forall a. Set a -> Int
Set.size s t1
Set t1
n)) (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era dom
Rep era a
dom s t1
Set dom
n) PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
forall era rng. RngSpec era rng
RngAny
  (Term era (Set a)
expr `Subset` Dom (Var V era (Map a b)
v2))
    | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
        With s t1
_ <- Rep era a -> Rep era a -> Typed (HasConstraint Ord (Rep era a))
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 <- Rep era a -> Term era (Set a) -> Typed (HasConstraint Ord (Set a))
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
        Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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 (Set t1 -> Int
forall a. Set a -> Int
Set.size s t1
Set t1
n)) (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era dom
Rep era a
dom s t1
Set dom
n) PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
forall era rng. RngSpec era rng
RngAny
  (SumsTo Direct c
small Term era c
expr OrdCond
cond [Sum era c]
xs) | (Sum era c -> Bool) -> [Sum era c] -> Bool
forall a. (a -> Bool) -> [a] -> Bool
exactlyOne (Name era -> Sum era c -> Bool
forall era c. Name era -> Sum era c -> Bool
isMapVar (V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1)) [Sum era c]
xs -> do
    c
t <- Term era c -> Typed c
forall era t. Term era t -> Typed t
simplify Term era c
expr
    RngSpec era rng
rngspec <- c
-> c
-> [String]
-> OrdCond
-> V era (Map dom rng)
-> c
-> [Sum era c]
-> Typed (RngSpec era rng)
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 (Direct c -> c
forall a. Direct a -> a
direct Direct c
small) c
t [String
msg] OrdCond
cond V era (Map dom rng)
v1 c
forall x. Adds x => x
zero [Sum era c]
xs
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom 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 RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
rngspec
  (Random (Var V era t
v2)) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom 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 RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
forall era rng. RngSpec era rng
RngAny
  (Sized (Size Size
sz) (Var V era t
v2)) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom 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
sz RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
forall era rng. RngSpec era rng
RngAny
  (Disjoint Term era (Set a)
expr (Dom (Var V era (Map a b)
v2))) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    With s t1
set <- Rep era a -> Term era (Set a) -> Typed (HasConstraint Ord (Set a))
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
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom 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 (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era dom
Rep era a
dom s t1
Set dom
set) PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
forall era rng. RngSpec era rng
RngAny
  (Disjoint (Dom (Var V era (Map a b)
v2)) Term era (Set a)
expr) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    With s t1
set <- Rep era a -> Term era (Set a) -> Typed (HasConstraint Ord (Set a))
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
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom 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 (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era dom
Rep era a
dom s t1
Set dom
set) PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
forall era rng. RngSpec era rng
RngAny
  (Disjoint Term era (Set a)
expr (Rng (Var V era (Map a b)
v2))) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    With s t1
_ <- Rep era b -> Rep era b -> Typed (HasConstraint Ord (Rep era b))
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 <- Rep era b -> Term era (Set a) -> Typed (HasConstraint Ord (Set b))
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
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom 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 RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny (RelSpec era rng -> RngSpec era rng
forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (RelSpec era rng -> RngSpec era rng)
-> RelSpec era rng -> RngSpec era rng
forall a b. (a -> b) -> a -> b
$ Rep era rng -> Set rng -> RelSpec era rng
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era rng
Rep era b
rng s t1
Set rng
set)
  (Disjoint (Rng (Var V era (Map a b)
v2)) Term era (Set a)
expr) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    With s t1
_ <- Rep era b -> Rep era b -> Typed (HasConstraint Ord (Rep era b))
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 <- Rep era b -> Term era (Set a) -> Typed (HasConstraint Ord (Set b))
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
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom 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 RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny (RelSpec era rng -> RngSpec era rng
forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (RelSpec era rng -> RngSpec era rng)
-> RelSpec era rng -> RngSpec era rng
forall a b. (a -> b) -> a -> b
$ Rep era rng -> Set rng -> RelSpec era rng
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era rng
Rep era b
rng s t1
Set rng
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)
_)))) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
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 <- Rep era (ScriptF era)
-> Term era (ScriptF era) -> Typed (ScriptF era)
forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType (Proof era -> Rep era (ScriptF era)
forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR Proof era
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
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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) (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era dom
Rep era a
dom (dom -> Set dom
forall a. a -> Set a
Set.singleton dom
ScriptHash
hash)) PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
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)
_)))) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
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 <- Rep era (ScriptF era)
-> Term era (ScriptF era) -> Typed (ScriptF era)
forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType (Proof era -> Rep era (ScriptF era)
forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR Proof era
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
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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) (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era dom
Rep era a
dom (dom -> Set dom
forall a. a -> Set a
Set.singleton dom
ScriptHash
hash)) PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
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)
_)))) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
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 <- Rep era (Data era) -> Term era (Data era) -> Typed (Data era)
forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era (Data era)
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
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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) (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era dom
Rep era a
dom (dom -> Set dom
forall a. a -> Set a
Set.singleton dom
SafeHash EraIndependentData
hash)) PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
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)
_)))) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
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 <- Rep era (Data era) -> Term era (Data era) -> Typed (Data era)
forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era (Data era)
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
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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) (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era dom
Rep era a
dom (dom -> Set dom
forall a. a -> Set a
Set.singleton dom
SafeHash EraIndependentData
hash)) PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
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)
_)))) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
a
    a
x <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify (Direct (Term era a) -> Term era a
forall a. Direct a -> a
direct Direct (Term era a)
expr)
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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) (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era dom
Rep era a
dom (dom -> Set dom
forall a. a -> Set a
Set.singleton dom
a
x)) PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
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)
_)))) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    b :~: b
Refl <- Rep era b -> Rep era b -> Typed (b :~: b)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
rng Rep era b
b
    a
x <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify (Direct (Term era a) -> Term era a
forall a. Direct a -> a
direct Direct (Term era a)
expr)
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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) RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny (RelSpec era rng -> RngSpec era rng
forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (Rep era rng -> Set rng -> RelSpec era rng
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era rng
Rep era b
rng (rng -> Set rng
forall a. a -> Set a
Set.singleton rng
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)
_)))) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
dom Rep era a
a
    a
x <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify Term era a
expr
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom 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 (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era dom
Rep era a
dom (dom -> Set dom
forall a. a -> Set a
Set.singleton dom
a
x)) PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
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)
_)))) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map a b) -> Name era
forall era t. V era t -> Name era
Name V era (Map a b)
v2 -> do
    b :~: b
Refl <- Rep era b -> Rep era b -> Typed (b :~: b)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
rng Rep era b
b
    a
x <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify Term era a
expr
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom 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 RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny (RelSpec era rng -> RngSpec era rng
forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (Rep era rng -> Set rng -> RelSpec era rng
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era rng
Rep era b
rng (rng -> Set rng
forall a. a -> Set a
Set.singleton rng
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)
_)))) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map k v) -> Name era
forall era t. V era t -> Name era
Name V era (Map k v)
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
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 <- Rep era b -> Rep era b -> Typed (b :~: b)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
rng Rep era b
rng2
    k
k <- Term era k -> Typed k
forall era t. Term era t -> Typed t
simplify Term era k
exprK
    v
v <- Term era v -> Typed v
forall era t. Term era t -> Typed t
simplify Term era v
exprV
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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)
      (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era dom
Rep era a
dom (dom -> Set dom
forall a. a -> Set a
Set.singleton dom
k
k))
      (Rep era dom
-> Rep era rng -> PairSide -> Map dom rng -> PairSpec era dom rng
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 dom
Rep era a
dom Rep era rng
Rep era b
rng PairSide
VarOnRight (dom -> rng -> Map dom rng
forall k a. k -> a -> Map k a
Map.singleton dom
k
k rng
v
v))
      (RelSpec era rng -> RngSpec era rng
forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (Rep era rng -> Set rng -> RelSpec era rng
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era rng
Rep era b
rng (rng -> Set rng
forall a. a -> Set a
Set.singleton rng
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)
_)))) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map k v) -> Name era
forall era t. V era t -> Name era
Name V era (Map k v)
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
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 <- Rep era b -> Rep era b -> Typed (b :~: b)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
rng Rep era b
rng2
    k
k <- Term era k -> Typed k
forall era t. Term era t -> Typed t
simplify Term era k
exprK
    v
v <- Term era v -> Typed v
forall era t. Term era t -> Typed t
simplify Term era v
exprV
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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)
      (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era dom
Rep era a
dom (dom -> Set dom
forall a. a -> Set a
Set.singleton dom
k
k))
      (Rep era dom
-> Rep era rng -> PairSide -> Map dom rng -> PairSpec era dom rng
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 dom
Rep era a
dom Rep era rng
Rep era b
rng PairSide
VarOnRight (dom -> rng -> Map dom rng
forall k a. k -> a -> Map k a
Map.singleton dom
k
k rng
v
v))
      (RelSpec era rng -> RngSpec era rng
forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (Rep era rng -> Set rng -> RelSpec era rng
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era rng
Rep era b
rng (rng -> Set rng
forall a. a -> Set a
Set.singleton rng
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 <- V era (Map dom rng) -> V era fs -> Maybe (Map dom rng :~: fs)
forall era t s. V era t -> V era s -> Maybe (t :~: s)
sameName V era (Map dom rng)
v1 V era fs
v2
    , [Term era t] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term era t]
xs ->
        Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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) RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
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 <- V era (Map dom rng) -> V era fs -> Maybe (Map dom rng :~: fs)
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
_) <- Typed (HasConstraint Ord (Rep era b))
-> Either [String] (HasConstraint Ord (Rep era b))
forall x. Typed x -> Either [String] x
runTyped (Typed (HasConstraint Ord (Rep era b))
 -> Either [String] (HasConstraint Ord (Rep era b)))
-> Typed (HasConstraint Ord (Rep era b))
-> Either [String] (HasConstraint Ord (Rep era b))
forall a b. (a -> b) -> a -> b
$ Rep era b -> Rep era b -> Typed (HasConstraint Ord (Rep era 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 <- Term era t -> Rep era t
forall era t. Era era => Term era t -> Rep era t
termRep Term era t
x -> do
        a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
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 <- Rep era b -> Rep era b -> Typed (b :~: b)
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 <- (Term era t -> Typed (a, b)) -> [Term era t] -> Typed [(a, b)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Rep era (a, b) -> Term era t -> Typed (a, b)
forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType (Rep era a -> Rep era b -> Rep era (a, b)
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) = [(a, b)] -> ([a], [b])
forall a b. [(a, b)] -> ([a], [b])
unzip [(a, b)]
ys
        Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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 ([(a, b)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(a, b)]
ys))
          (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era dom
Rep era a
dl (forall ts a. FromList ts a => [a] -> ts
makeFromList @(Set dom) [a]
ds))
          (Rep era dom
-> Rep era rng -> PairSide -> Map dom rng -> PairSpec era dom rng
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 dom
Rep era a
dom Rep era rng
Rep era b
rng PairSide
VarOnRight ([(dom, rng)] -> Map dom rng
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(dom, rng)]
[(a, b)]
ys))
          (RelSpec era rng -> RngSpec era rng
forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (Rep era rng -> Set rng -> RelSpec era rng
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era rng
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)
_))) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map k v) -> Name era
forall era t. V era t -> Name era
Name V era (Map k v)
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
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 <- Rep era b -> Rep era b -> Typed (b :~: b)
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 <- Term era (Map k v) -> Typed (Map k v)
forall era t. Term era t -> Typed t
simplify Term era (Map k v)
subMapExpr
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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 (Map k v -> Int
forall k a. Map k a -> Int
Map.size Map k v
m))
      (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era dom
Rep era a
dom (Map dom v -> Set dom
forall k a. Map k a -> Set k
Map.keysSet Map dom v
Map k v
m))
      (Rep era dom
-> Rep era rng -> PairSide -> Map dom rng -> PairSpec era dom rng
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 dom
Rep era a
dom Rep era rng
Rep era b
rng PairSide
VarOnRight Map dom rng
Map k v
m)
      (RelSpec era rng -> RngSpec era rng
forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (Rep era rng -> Set rng -> RelSpec era rng
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era rng
Rep era b
rng ([rng] -> Set rng
forall a. Ord a => [a] -> Set a
Set.fromList (Map k rng -> [rng]
forall k a. Map k a -> [a]
Map.elems Map k rng
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) | V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Map k v) -> Name era
forall era t. V era t -> Name era
Name V era (Map k v)
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
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 <- Rep era b -> Rep era b -> Typed (b :~: b)
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 <- Term era (Map k v) -> Typed (Map k v)
forall era t. Term era t -> Typed t
simplify Term era (Map k v)
subMapExpr
    Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> Typed (MapSpec era dom rng)
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 (Map k v -> Int
forall k a. Map k a -> Int
Map.size Map k v
m))
      (Rep era dom -> Set dom -> RelSpec era dom
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era dom
Rep era a
dom (Map dom v -> Set dom
forall k a. Map k a -> Set k
Map.keysSet Map dom v
Map k v
m))
      (Rep era dom
-> Rep era rng -> PairSide -> Map dom rng -> PairSpec era dom rng
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 dom
Rep era a
dom Rep era rng
Rep era b
rng PairSide
VarOnLeft Map dom rng
Map k v
m)
      (RelSpec era rng -> RngSpec era rng
forall rng era. Ord rng => RelSpec era rng -> RngSpec era rng
RngRel (Rep era rng -> Set rng -> RelSpec era rng
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era rng
Rep era b
rng ([rng] -> Set rng
forall a. Ord a => [a] -> Set a
Set.fromList (Map k rng -> [rng]
forall k a. Map k a -> [a]
Map.elems Map k rng
Map k v
m))))
  Pred era
other -> [String] -> Typed (MapSpec era dom rng)
forall a. [String] -> Typed a
failT [String
"Cannot solve map condition: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pred era -> String
forall a. Show a => a -> String
show Pred era
other]
  where
    msg :: String
msg = (String
"Solving for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ V era (Map dom rng) -> String
forall a. Show a => a -> String
show V era (Map dom rng)
v1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nPredicate = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pred era -> String
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 <- Rep era b -> Rep era b -> Typed (b :~: b)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
r Rep era b
r1
  RngSpec era rng -> Typed (RngSpec era rng)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (rng -> Size -> RngSpec era rng
forall rng era. Adds rng => rng -> Size -> RngSpec era rng
RngSum c
rng
small ([String] -> c -> OrdCond -> c -> String -> Size
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 <- Rep era b -> Rep era b -> Typed (b :~: b)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
r Rep era b
r1
  RngSpec era rng -> Typed (RngSpec era rng)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (c -> Rep era rng -> Lens' rng c -> Size -> RngSpec era rng
forall c era rng.
Adds c =>
c -> Rep era rng -> Lens' rng c -> Size -> RngSpec era rng
RngProj c
small Rep era rng
Rep era b
r (c -> f c) -> rng -> f rng
(c -> f c) -> x -> f x
Lens' rng c
Lens' x c
l ([String] -> c -> OrdCond -> c -> String -> Size
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 <- Rep era b -> Rep era b -> Typed (b :~: b)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era b
r Rep era b
r1
  RngSpec era rng -> Typed (RngSpec era rng)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (rng -> Size -> RngSpec era rng
forall rng era. Adds rng => rng -> Size -> RngSpec era rng
RngSum c
rng
small ([String] -> c -> OrdCond -> c -> String -> Size
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)
  | Name era -> Sum era c -> Bool
forall era c. Name era -> Sum era c -> Bool
isMapVar (V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v) Sum era c
s =
      c
-> c
-> [String]
-> OrdCond
-> V era (Map dom rng)
-> c
-> [Sum era c]
-> Typed (RngSpec era rng)
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 [Sum era c] -> [Sum era c] -> [Sum era c]
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 <- Sum era c -> Typed Int
forall c era. Adds c => Sum era c -> Typed Int
summandAsInt Sum era c
s
  c
-> c
-> [String]
-> OrdCond
-> V era (Map dom rng)
-> c
-> [Sum era c]
-> Typed (RngSpec era rng)
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 -> c
forall x. Adds x => x -> x -> x
add c
c (c -> c) -> c -> c
forall a b. (a -> b) -> a -> b
$ [String] -> Int -> c
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
_ [] = [String] -> Typed (RngSpec era rng)
forall a. [String] -> Typed a
failT ((String
"Does not have exactly one summand with variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name era -> String
forall a. Show a => a -> String
show (V era (Map dom rng) -> Name era
forall era t. V era t -> Name era
Name V era (Map dom rng)
v)) String -> [String] -> [String]
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 =
  (MapSpec era dom rng -> Pred era -> Typed (MapSpec era dom rng))
-> MapSpec era dom rng -> [Pred era] -> Typed (MapSpec era dom rng)
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 (Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
SzAny RelSpec era dom
forall era dom. RelSpec era dom
RelAny PairSpec era dom rng
forall era a b. PairSpec era a b
PairAny RngSpec era rng
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 <- V era (Map dom rng) -> Pred era -> Typed (MapSpec era dom rng)
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
      MapSpec era dom rng -> Typed (MapSpec era dom rng)
forall x. LiftT x => x -> Typed x
liftT (MapSpec era dom rng
spec MapSpec era dom rng -> MapSpec era dom rng -> MapSpec era dom rng
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)) | V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec Size
sz RelSpec era a
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 <- V era (Set a) -> V era fs -> Maybe (Set a :~: fs)
forall era t s. V era t -> V era s -> Maybe (t :~: s)
sameName V era (Set a)
v1 V era fs
v2 -> Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzExact Int
0) RelSpec era a
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 <- V era (Set a) -> V era fs -> Maybe (Set a :~: fs)
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 <- Rep era t -> Rep era a -> Typed (t :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep (Term era t -> Rep era t
forall era t. Era era => Term era t -> Rep era t
termRep Term era t
x) Rep era a
r2
    [a]
xs <- (Term era t -> Typed a) -> [Term era t] -> Typed [a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Rep era a -> Term era t -> Typed a
forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era a
r2) [Term era t]
expr
    Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzMost ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs)) (Rep era a -> Set a -> RelSpec era a
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
Rep era a
r (forall ts a. FromList ts a => [a] -> ts
makeFromList @(Set a) @a [a]
[a]
xs))
  (Var V era a
v2 :=: Term era a
expr) | V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era a -> Name era
forall era t. V era t -> Name era
Name V era a
v2 -> do
    With s t1
set <- Rep era a -> Term era a -> Typed (HasConstraint Ord (Set a))
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
    Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzExact (Set t1 -> Int
forall a. Set a -> Int
Set.size s t1
Set t1
set)) (Rep era a -> Set a -> RelSpec era a
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
Rep era a
r s t1
Set a
set)
  (Var v2 :: V era t
v2@(V String
_ (SetR Rep era a
r2) Access era s t
_) :<-: RootTarget era r t
target) | (V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2) -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
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
RootTarget era r (Set a)
target
    Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzExact (Set a -> Int
forall a. Set a -> Int
Set.size Set a
x)) (Rep era a -> Set a -> RelSpec era a
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
Rep era a
r Set a
x)
  (Term era a
expr :=: v2 :: Term era a
v2@(Var V era a
_)) -> V era (Set a) -> Pred era -> Typed (SetSpec 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 Term era a -> Term era a -> Pred era
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) | V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
a Rep era a
r
    a
val1 <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify Term era a
expr1
    Map a b
val2 <- Term era (Map a b) -> Typed (Map a b)
forall era t. Term era t -> Typed t
simplify Term era (Map a b)
expr2
    Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzExact (Map a b -> Int
forall k a. Map k a -> Int
Map.size a
Map a b
val1)) (Rep era a -> Set a -> RelSpec era a
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
Rep era a
r (Map a b -> Set a
forall k a. Map k a -> Set k
Map.keysSet Map a b
Map a b
val2))
  (Restrict Term era (Set a)
expr1 Term era (Map a b)
expr2 :=: Term era a
expr3) -> V era (Set a) -> Pred era -> Typed (SetSpec 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
expr3 Term era a -> Term era a -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
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) | V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    With s t1
set <- Rep era a -> Term era (Set a) -> Typed (HasConstraint Ord (Set a))
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
    Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzMost (Set t1 -> Int
forall a. Set a -> Int
Set.size s t1
Set t1
set)) (Rep era a -> Set a -> RelSpec era a
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era a
Rep era a
r s t1
Set a
set)
  (Term era (Set a)
expr `Subset` Var V era (Set a)
v2) | V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    With s t1
set <- Rep era a -> Term era (Set a) -> Typed (HasConstraint Ord (Set a))
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
    Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzLeast (Set t1 -> Int
forall a. Set a -> Int
Set.size s t1
Set t1
set)) (Rep era a -> Set a -> RelSpec era a
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
Rep era a
r s t1
Set a
set)
  (Disjoint (Var V era (Set a)
v2) Term era (Set a)
expr) | V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    With s t1
set <- Rep era a -> Term era (Set a) -> Typed (HasConstraint Ord (Set a))
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
    Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec Size
SzAny (Rep era a -> Set a -> RelSpec era a
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era a
Rep era a
r s t1
Set a
set)
  (Disjoint Term era (Set a)
expr (Var V era (Set a)
v2)) -> V era (Set a) -> Pred era -> Typed (SetSpec 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 (Set a) -> Term era (Set a) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint (V era (Set a) -> Term era (Set a)
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)
_))) | V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    a :~: ScriptHash
Refl <- Rep era a -> Rep era ScriptHash -> Typed (a :~: ScriptHash)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r Rep era ScriptHash
forall era. Era era => Rep era ScriptHash
ScriptHashR
    ScriptF Proof era
_ Script era
x <- Rep era (ScriptF era)
-> Term era (ScriptF era) -> Typed (ScriptF era)
forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType (Proof era -> Rep era (ScriptF era)
forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR Proof era
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
    Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzLeast Int
1) (Rep era a -> Set a -> RelSpec era a
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
Rep era a
r (a -> Set a
forall a. a -> Set a
Set.singleton a
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)
_))) | V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    a :~: ScriptHash
Refl <- Rep era a -> Rep era ScriptHash -> Typed (a :~: ScriptHash)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r Rep era ScriptHash
forall era. Era era => Rep era ScriptHash
ScriptHashR
    ScriptF Proof era
_ Script era
x <- Rep era (ScriptF era)
-> Term era (ScriptF era) -> Typed (ScriptF era)
forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType (Proof era -> Rep era (ScriptF era)
forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR Proof era
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
    Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzLeast Int
1) (Rep era a -> Set a -> RelSpec era a
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
Rep era a
r (a -> Set a
forall a. a -> Set a
Set.singleton a
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)
_))) | V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    a :~: SafeHash EraIndependentData
Refl <- Rep era a
-> Rep era (SafeHash EraIndependentData)
-> Typed (a :~: SafeHash EraIndependentData)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r Rep era (SafeHash EraIndependentData)
forall era. Era era => Rep era (SafeHash EraIndependentData)
DataHashR
    Data era
x <- Rep era (Data era) -> Term era (Data era) -> Typed (Data era)
forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era (Data era)
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
    Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzLeast Int
1) (Rep era a -> Set a -> RelSpec era a
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
Rep era a
r (a -> Set a
forall a. a -> Set a
Set.singleton a
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)
_))) | V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    a :~: SafeHash EraIndependentData
Refl <- Rep era a
-> Rep era (SafeHash EraIndependentData)
-> Typed (a :~: SafeHash EraIndependentData)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r Rep era (SafeHash EraIndependentData)
forall era. Era era => Rep era (SafeHash EraIndependentData)
DataHashR
    Data era
x <- Rep era (Data era) -> Term era (Data era) -> Typed (Data era)
forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era (Data era)
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
    Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzLeast Int
1) (Rep era a -> Set a -> RelSpec era a
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
Rep era a
r (a -> Set a
forall a. a -> Set a
Set.singleton a
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)
_))) | V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
a Rep era a
r
    a
x <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify (Direct (Term era a) -> Term era a
forall a. Direct a -> a
direct Direct (Term era a)
expr)
    Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzLeast Int
1) (Rep era a -> Set a -> RelSpec era a
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era a
Rep era a
r (a -> Set a
forall a. a -> Set a
Set.singleton a
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)
_))) | V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
a Rep era a
r
    a
x <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify Term era a
expr
    Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec Size
SzAny (Rep era a -> Set a -> RelSpec era a
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era a
Rep era a
r (a -> Set a
forall a. a -> Set a
Set.singleton a
a
x))
  (List (Var v2 :: V era fs
v2@(V String
_ (SetR Rep era a
r2) Access era s fs
_)) [Term era t]
xs) | V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era fs -> Name era
forall era t. V era t -> Name era
Name V era fs
v2 -> do
    a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r Rep era a
r2
    [t]
ys <- (Term era t -> Typed t) -> [Term era t] -> Typed [t]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Term era t -> Typed t
forall era t. Term era t -> Typed t
simplify [Term era t]
xs
    SetSpec era a -> Typed (SetSpec era a)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SetSpec era a -> Typed (SetSpec era a))
-> SetSpec era a -> Typed (SetSpec era a)
forall a b. (a -> b) -> a -> b
$ Size -> RelSpec era a -> SetSpec era a
forall a era. Ord a => Size -> RelSpec era a -> SetSpec era a
SetSpec (Int -> Size
SzMost ([t] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [t]
ys)) (Rep era a -> Set a -> RelSpec era a
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era a
Rep era a
r ([t] -> Set a
forall ts a. FromList ts a => [a] -> ts
makeFromList [t]
ys))
  (Random (Var V era t
v2)) | V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec Size
SzAny RelSpec era a
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))
    | V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Set b) -> Name era
forall era t. V era t -> Name era
Name V era (Set b)
v2 -> do
        a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r Rep era a
brep
        Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzExact (Map a b -> Int
forall k a. Map k a -> Int
Map.size Map a b
x)) (Lens' a t1
-> Rep era a -> Rep era t1 -> RelSpec era t1 -> RelSpec era a
forall b dom era.
Ord b =>
Lens' dom b
-> Rep era dom -> Rep era b -> RelSpec era b -> RelSpec era dom
RelLens (t1 -> f t1) -> a -> f a
(t1 -> f t1) -> b -> f b
Lens' a t1
Lens' b t1
lensbt Rep era a
Rep era a
r Rep era t1
trep (Rep era t1 -> Set t1 -> RelSpec era t1
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era t1
Rep era a
drep (Map t1 b -> Set t1
forall k a. Map k a -> Set k
Map.keysSet Map t1 b
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))
    | V era (Set a) -> Name era
forall era t. V era t -> Name era
Name V era (Set a)
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Set b) -> Name era
forall era t. V era t -> Name era
Name V era (Set b)
v2 -> do
        a :~: a
Refl <- Rep era a -> Rep era a -> Typed (a :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r Rep era a
brep
        Size -> RelSpec era a -> Typed (SetSpec era a)
forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Int -> Size
SzMost (Map a b -> Int
forall k a. Map k a -> Int
Map.size Map a b
x)) (Lens' a t1
-> Rep era a -> Rep era t1 -> RelSpec era t1 -> RelSpec era a
forall b dom era.
Ord b =>
Lens' dom b
-> Rep era dom -> Rep era b -> RelSpec era b -> RelSpec era dom
RelLens (t1 -> f t1) -> a -> f a
(t1 -> f t1) -> b -> f b
Lens' a t1
Lens' b t1
lensbt Rep era a
Rep era a
r Rep era t1
trep (Rep era t1 -> Set t1 -> RelSpec era t1
forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era t1
Rep era a
drep (Map t1 b -> Set t1
forall k a. Map k a -> Set k
Map.keysSet Map t1 b
Map a b
x)))
  Pred era
cond -> [String] -> Typed (SetSpec era a)
forall a. [String] -> Typed a
failT [String
"Can't solveSet " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pred era -> String
forall a. Show a => a -> String
show Pred era
cond String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" for variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ V era (Set a) -> String
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 =
  String -> Typed (SetSpec era a) -> Typed (SetSpec era a)
forall a. String -> Typed a -> Typed a
explain (String
"\nSolving for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", Set Predicates\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines ((Pred era -> String) -> [Pred era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Pred era -> String) -> Pred era -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred era -> String
forall a. Show a => a -> String
show) [Pred era]
cs)) (Typed (SetSpec era a) -> Typed (SetSpec era a))
-> Typed (SetSpec era a) -> Typed (SetSpec era a)
forall a b. (a -> b) -> a -> b
$
    (SetSpec era a -> Pred era -> Typed (SetSpec era a))
-> SetSpec era a -> [Pred era] -> Typed (SetSpec era a)
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 SetSpec era a
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 <- V era (Set a) -> Pred era -> Typed (SetSpec era a)
forall era a.
Era era =>
V era (Set a) -> Pred era -> Typed (SetSpec era a)
solveSet V era (Set a)
v Pred era
cond
      SetSpec era a -> Typed (SetSpec era a)
forall x. LiftT x => x -> Typed x
liftT (SetSpec era a
spec SetSpec era a -> SetSpec era a -> SetSpec era a
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
_))) | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> do
      Size
sz <- Term era Size -> Typed Size
forall era t. Term era t -> Typed t
simplify Term era Size
expr
      AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AddsSpec t -> Typed (AddsSpec t))
-> AddsSpec t -> Typed (AddsSpec t)
forall a b. (a -> b) -> a -> b
$ String -> Size -> AddsSpec t
forall c. String -> Size -> AddsSpec c
AddsSpecSize String
nm Size
sz
    (Sized (Var V era Size
v2) Term era t
expr) | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era Size -> Name era
forall era t. V era t -> Name era
Name V era Size
v2 -> do
      t
n <- Rep era t -> Term era t -> Typed t
forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era t
r Term era t
expr
      AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AddsSpec t -> Typed (AddsSpec t))
-> AddsSpec t -> Typed (AddsSpec t)
forall a b. (a -> b) -> a -> b
$ String -> OrdCond -> t -> AddsSpec t
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)) | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era a -> Name era
forall era t. V era t -> Name era
Name V era a
v2 -> do
      t
n <- Rep era t -> Term era a -> Typed t
forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era t
r Term era a
expr
      AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AddsSpec t -> Typed (AddsSpec t))
-> AddsSpec t -> Typed (AddsSpec t)
forall a b. (a -> b) -> a -> b
$ String -> OrdCond -> t -> AddsSpec t
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) | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era a -> Name era
forall era t. V era t -> Name era
Name V era a
v2 -> do
      t
n <- Rep era t -> Term era a -> Typed t
forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era t
r Term era a
expr
      AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AddsSpec t -> Typed (AddsSpec t))
-> AddsSpec t -> Typed (AddsSpec t)
forall a b. (a -> b) -> a -> b
$ String -> OrdCond -> t -> AddsSpec t
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
_))) | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era Coin -> Name era
forall era t. V era t -> Name era
Name V era Coin
v2 -> do
      DeltaCoin Integer
n <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify Term era a
expr
      AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AddsSpec t -> Typed (AddsSpec t))
-> AddsSpec t -> Typed (AddsSpec t)
forall a b. (a -> b) -> a -> b
$ String -> OrdCond -> Coin -> AddsSpec t
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) -> V era t -> Pred era -> Typed (AddsSpec t)
forall era t.
(Adds t, Era era) =>
V era t -> Pred era -> Typed (AddsSpec t)
solveSum V era t
v1 (Term era a
expr Term era a -> Term era a -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (Term era Coin -> Term era DeltaCoin
forall era. Term era Coin -> Term era DeltaCoin
Delta (V era Coin -> Term era Coin
forall era t. V era t -> Term era t
Var V era Coin
v2)))
    (Term era a
expr :=: Negate (Var V era DeltaCoin
v2)) | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era DeltaCoin -> Name era
forall era t. V era t -> Name era
Name V era DeltaCoin
v2 -> do
      t :~: DeltaCoin
Refl <- Rep era t -> Rep era DeltaCoin -> Typed (t :~: DeltaCoin)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r Rep era DeltaCoin
forall era. Rep era DeltaCoin
DeltaCoinR
      DeltaCoin Integer
n <- Rep era DeltaCoin -> Term era a -> Typed DeltaCoin
forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era DeltaCoin
forall era. Rep era DeltaCoin
DeltaCoinR Term era a
expr
      AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AddsSpec t -> Typed (AddsSpec t))
-> AddsSpec t -> Typed (AddsSpec t)
forall a b. (a -> b) -> a -> b
$ String -> OrdCond -> DeltaCoin -> AddsSpec t
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) | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era DeltaCoin -> Name era
forall era t. V era t -> Name era
Name V era DeltaCoin
v2 -> do
      t :~: DeltaCoin
Refl <- Rep era t -> Rep era DeltaCoin -> Typed (t :~: DeltaCoin)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r Rep era DeltaCoin
forall era. Rep era DeltaCoin
DeltaCoinR
      DeltaCoin Integer
n <- Rep era DeltaCoin -> Term era a -> Typed DeltaCoin
forall era s t. Era era => Rep era s -> Term era t -> Typed s
simplifyAtType Rep era DeltaCoin
forall era. Rep era DeltaCoin
DeltaCoinR Term era a
expr
      AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AddsSpec t -> Typed (AddsSpec t))
-> AddsSpec t -> Typed (AddsSpec t)
forall a b. (a -> b) -> a -> b
$ String -> OrdCond -> DeltaCoin -> AddsSpec t
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)) | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure AddsSpec t
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) <- V era t -> [Sum era c] -> Typed (Int, Bool)
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 AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Coin -> OrdCond -> Coin -> String -> AddsSpec t
forall a c. Adds a => a -> OrdCond -> a -> String -> AddsSpec c
varOnRightNeg Coin
n OrdCond
cond ([String] -> Int -> Coin
forall x. Adds x => [String] -> Int -> x
fromI [String
"solveSum-SumsTo 1"] Int
rhsTotal) String
nam)
            else
              if Int
rhsTotal Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
                then
                  AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                    ([String] -> Coin -> OrdCond -> Coin -> String -> AddsSpec t
forall a c.
Adds a =>
[String] -> a -> OrdCond -> a -> String -> AddsSpec c
varOnRight [String
"CASE1", Pred era -> String
forall a. Show a => a -> String
show Pred era
predx] (Coin -> Coin -> Coin
forall x. Adds x => x -> x -> x
add Coin
n (Integer -> Coin
Coin (Integer -> Coin) -> Integer -> Coin
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Int -> Int
forall a. Num a => a -> a
negate Int
rhsTotal)) OrdCond
cond (Integer -> Coin
Coin Integer
0) String
nam)
                else
                  AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                    ( [String] -> Coin -> OrdCond -> Coin -> String -> AddsSpec t
forall a c.
Adds a =>
[String] -> a -> OrdCond -> a -> String -> AddsSpec c
varOnRight
                        [String
"CASE2", Pred era -> String
forall a. Show a => a -> String
show Pred era
predx]
                        Coin
n
                        OrdCond
cond
                        ([String] -> Int -> Coin
forall x. Adds x => [String] -> Int -> x
fromI [String
"solveSum-SumsTo 2", Coin -> String
forall a. Show a => a -> String
show Coin
n, Int -> String
forall a. Show a => a -> String
show Int
rhsTotal, Direct c -> String
forall a. Show a => a -> String
show Direct c
x, V era t -> String
forall a. Show a => a -> String
show V era t
v1] Int
rhsTotal)
                        String
nam
                    )
        Rep era t
DeltaCoinR ->
          if Bool
needsNeg
            then AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DeltaCoin -> OrdCond -> DeltaCoin -> String -> AddsSpec t
forall a c. Adds a => a -> OrdCond -> a -> String -> AddsSpec c
varOnRightNeg (Integer -> DeltaCoin
DeltaCoin Integer
i) OrdCond
cond ([String] -> Int -> DeltaCoin
forall x. Adds x => [String] -> Int -> x
fromI [String
"solveSum-SumsTo 3"] Int
rhsTotal) String
nam)
            else
              AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ([String]
-> DeltaCoin -> OrdCond -> DeltaCoin -> String -> AddsSpec t
forall a c.
Adds a =>
[String] -> a -> OrdCond -> a -> String -> AddsSpec c
varOnRight [String
"CASE3", Pred era -> String
forall a. Show a => a -> String
show Pred era
predx] (Integer -> DeltaCoin
DeltaCoin Integer
i) OrdCond
cond ([String] -> Int -> DeltaCoin
forall x. Adds x => [String] -> Int -> x
fromI [String
"solveSum-SumsTo 4"] Int
rhsTotal) String
nam)
        Rep era t
other -> [String] -> Typed (AddsSpec t)
forall a. [String] -> Typed a
failT [Pred era -> String
forall a. Show a => a -> String
show Pred era
predx, Rep era t -> String
forall a. Show a => a -> String
show Rep era t
other String -> String -> String
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) <- V era t -> [Sum era c] -> Typed (Int, Bool)
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 <- Rep era t -> Rep era c -> Typed (t :~: c)
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 AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (c -> OrdCond -> c -> String -> AddsSpec t
forall a c. Adds a => a -> OrdCond -> a -> String -> AddsSpec c
varOnRightNeg c
n OrdCond
cond ([String] -> Int -> c
forall x. Adds x => [String] -> Int -> x
fromI [String
"solveSum-SumsTo 5"] Int
rhsTotal) String
nam)
        else AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([String] -> c -> OrdCond -> c -> String -> AddsSpec t
forall a c.
Adds a =>
[String] -> a -> OrdCond -> a -> String -> AddsSpec c
varOnRight [String
"CASE4", Pred era -> String
forall a. Show a => a -> String
show Pred era
predx] c
n OrdCond
cond ([String] -> Int -> c
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]
_)) | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era c -> Name era
forall era t. V era t -> Name era
Name V era c
v2 -> do
      Int
rhsTotal <- [Sum era c] -> Typed Int
forall c era. (Adds c, Era era) => [Sum era c] -> Typed Int
summandsAsInt [Sum era c]
xs
      t :~: c
Refl <- Rep era t -> Rep era c -> Typed (t :~: c)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r Rep era c
r2
      AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AddsSpec t -> Typed (AddsSpec t))
-> AddsSpec t -> Typed (AddsSpec t)
forall a b. (a -> b) -> a -> b
$ String -> OrdCond -> Int -> AddsSpec t
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]
_)) | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era Coin -> Name era
forall era t. V era t -> Name era
Name V era Coin
v2 -> do
      Int
rhsTotal <- [Sum era c] -> Typed Int
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 -> AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AddsSpec t -> Typed (AddsSpec t))
-> AddsSpec t -> Typed (AddsSpec t)
forall a b. (a -> b) -> a -> b
$ String -> OrdCond -> Int -> AddsSpec t
forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
nam OrdCond
cond Int
rhsTotal
        Rep era t
DeltaCoinR -> AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AddsSpec t -> Typed (AddsSpec t))
-> AddsSpec t -> Typed (AddsSpec t)
forall a b. (a -> b) -> a -> b
$ String -> OrdCond -> Int -> AddsSpec t
forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
nam OrdCond
cond Int
rhsTotal
        Rep era t
other -> [String] -> Typed (AddsSpec t)
forall a. [String] -> Typed a
failT [Pred era -> String
forall a. Show a => a -> String
show Pred era
predx, Rep era t -> String
forall a. Show a => a -> String
show Rep era t
other String -> String -> String
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) | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> do
      t :~: t
Refl <- Rep era t -> Rep era t -> Typed (t :~: t)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r Rep era t
r2
      t
x <- RootTarget era r t -> Typed t
forall era t root. RootTarget era root t -> Typed t
simplifyTarget RootTarget era r t
tar
      AddsSpec t -> Typed (AddsSpec t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Size -> AddsSpec t
forall c. String -> Size -> AddsSpec c
AddsSpecSize String
nm (Int -> Size
SzExact (t -> Int
forall x. Adds x => x -> Int
toI t
x)))
    Pred era
other -> [String] -> Typed (AddsSpec t)
forall a. [String] -> Typed a
failT [String
"Can't solveSum " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name era -> String
forall a. Show a => a -> String
show (V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pred era -> String
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 =
  String -> Typed (AddsSpec t) -> Typed (AddsSpec t)
forall a. String -> Typed a -> Typed a
explain
    ( String
"\nGiven (Add "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rep era t -> String
forall a. Show a => a -> String
show Rep era t
r
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"), Solving for "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rep era t -> String
forall a. Show a => a -> String
show Rep era t
r
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
",  with Predicates \n"
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines ((Pred era -> String) -> [Pred era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Pred era -> String) -> Pred era -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred era -> String
forall a. Show a => a -> String
show) [Pred era]
cs)
    )
    (Typed (AddsSpec t) -> Typed (AddsSpec t))
-> Typed (AddsSpec t) -> Typed (AddsSpec t)
forall a b. (a -> b) -> a -> b
$ (AddsSpec t -> Pred era -> Typed (AddsSpec t))
-> AddsSpec t -> [Pred era] -> Typed (AddsSpec t)
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 AddsSpec t
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 <- V era t -> Pred era -> Typed (AddsSpec t)
forall era t.
(Adds t, Era era) =>
V era t -> Pred era -> Typed (AddsSpec t)
solveSum V era t
v Pred era
cond
      String -> Typed (AddsSpec t) -> Typed (AddsSpec t)
forall a. String -> Typed a -> Typed a
explain
        (String
"Solving Sum constraint (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pred era -> String
forall a. Show a => a -> String
show Pred era
cond String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") for variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm)
        (AddsSpec t -> Typed (AddsSpec t)
forall x. LiftT x => x -> Typed x
liftT (AddsSpec t
spec AddsSpec t -> AddsSpec t -> AddsSpec t
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)) = Int -> Typed Int
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (c -> Int
forall x. Adds x => x -> Int
toI c
x)
summandAsInt (One (Delta (Lit Rep era Coin
CoinR (Coin Integer
n)))) = Int -> Typed Int
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DeltaCoin -> Int
forall x. Adds x => x -> Int
toI (Integer -> DeltaCoin
DeltaCoin Integer
n))
summandAsInt (One (Negate (Lit Rep era DeltaCoin
DeltaCoinR (DeltaCoin Integer
n)))) = Int -> Typed Int
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DeltaCoin -> Int
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)) = Int -> Typed Int
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (c -> Int
forall x. Adds x => x -> Int
toI (x
x x -> Getting c x c -> c
forall s a. s -> Getting a s a -> a
^. Getting c x c
Lens' x c
l))
summandAsInt (SumMap (Lit Rep era (Map a c)
_ Map a c
m)) = Int -> Typed Int
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (c -> Int
forall x. Adds x => x -> Int
toI ((c -> c -> c) -> c -> Map a c -> c
forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' c -> c -> c
forall x. Adds x => x -> x -> x
add c
forall x. Adds x => x
zero Map a c
m))
summandAsInt (SumList (Lit Rep era [c]
_ [c]
m)) = Int -> Typed Int
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (c -> Int
forall x. Adds x => x -> Int
toI ((c -> c -> c) -> c -> [c] -> c
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' c -> c -> c
forall x. Adds x => x -> x -> x
add c
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)) = Int -> Typed Int
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (c -> Int
forall x. Adds x => x -> Int
toI ((c -> x -> c) -> c -> Map a x -> c
forall b a. (b -> a -> b) -> b -> Map a a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\c
ans x
x -> c -> c -> c
forall x. Adds x => x -> x -> x
add c
ans (x
x x -> Getting c x c -> c
forall s a. s -> Getting a s a -> a
^. Getting c x c
Lens' x c
l)) c
forall x. Adds x => x
zero Map a x
m))
summandAsInt Sum era c
x = [String] -> Typed Int
forall a. [String] -> Typed a
failT [String
"Can't compute summandAsInt: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Sum era c -> String
forall a. Show a => a -> String
show Sum era c
x String -> String -> String
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 = Subst era -> Gen (Subst era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst era -> Gen (Subst era)) -> Subst era -> Gen (Subst era)
forall a b. (a -> b) -> a -> b
$ V era x -> Term era x -> Subst era -> Subst era
forall era t. V era t -> Term era t -> Subst era -> Subst era
extend V era x
v (Rep era x -> x -> Term era x
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 = Subst era -> Gen (Subst era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst era -> Gen (Subst era)) -> Subst era -> Gen (Subst era)
forall a b. (a -> b) -> a -> b
$ V era Coin -> Term era Coin -> Subst era -> Subst era
forall era t. V era t -> Term era t -> Subst era -> Subst era
extend V era Coin
v (Rep era Coin -> Coin -> Term era Coin
forall era t. Rep era t -> t -> Term era t
Lit Rep era Coin
forall era. Rep era Coin
CoinR ([String] -> Int -> Coin
forall x. Adds x => [String] -> Int -> x
fromI [] (x -> Int
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 = Subst era -> Gen (Subst era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst era -> Gen (Subst era)) -> Subst era -> Gen (Subst era)
forall a b. (a -> b) -> a -> b
$ V era DeltaCoin -> Term era DeltaCoin -> Subst era -> Subst era
forall era t. V era t -> Term era t -> Subst era -> Subst era
extend V era DeltaCoin
v (Rep era DeltaCoin -> DeltaCoin -> Term era DeltaCoin
forall era t. Rep era t -> t -> Term era t
Lit Rep era DeltaCoin
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
_ = String -> [String] -> Gen (Subst era)
forall a. HasCallStack => String -> [String] -> a
errorMess (String
"Can't genSum " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Sum era x -> String
forall a. Show a => a -> String
show Sum era x
other) [Rep era x -> String
forall a. Show a => a -> String
show Rep era x
rep, x -> String
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 [] = Int -> Typed Int
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
0
summandsAsInt (Sum era c
x : [Sum era c]
xs) = do
  Int
n <- Sum era c -> Typed Int
forall c era. Adds c => Sum era c -> Typed Int
summandAsInt Sum era c
x
  Int
m <- [Sum era c] -> Typed Int
forall c era. (Adds c, Era era) => [Sum era c] -> Typed Int
summandsAsInt [Sum era c]
xs
  Int -> Typed Int
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
m Int -> Int -> Int
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
_) = Rep era s -> Rep era t -> Typed (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 V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era c -> Name era
forall era t. V era t -> Name era
Name V era c
v2
    then (Int, Bool, [Name era]) -> Typed (Int, Bool, [Name era])
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
c, Bool
b, V era c -> Name era
forall era t. V era t -> Name era
Name V era c
v2 Name era -> [Name era] -> [Name era]
forall a. a -> [a] -> [a]
: [Name era]
ns)
    else [String] -> Typed (Int, Bool, [Name era])
forall a. [String] -> Typed a
failT [String
"Unexpected Name in 'unique' " String -> String -> String
forall a. [a] -> [a] -> [a]
++ V era c -> String
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 V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era Coin -> Name era
forall era t. V era t -> Name era
Name V era Coin
v2
    then (Int, Bool, [Name era]) -> Typed (Int, Bool, [Name era])
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
c, Bool
b, V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> [Name era] -> [Name era]
forall a. a -> [a] -> [a]
: [Name era]
ns)
    else [String] -> Typed (Int, Bool, [Name era])
forall a. [String] -> Typed a
failT [String
"Unexpected Name in 'unique' " String -> String -> String
forall a. [a] -> [a] -> [a]
++ V era Coin -> String
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 V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era DeltaCoin -> Name era
forall era t. V era t -> Name era
Name V era DeltaCoin
v2
    then (Int, Bool, [Name era]) -> Typed (Int, Bool, [Name era])
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
c, Bool
True, V era DeltaCoin -> Name era
forall era t. V era t -> Name era
Name V era DeltaCoin
v2 Name era -> [Name era] -> [Name era]
forall a. a -> [a] -> [a]
: [Name era]
ns)
    else [String] -> Typed (Int, Bool, [Name era])
forall a. [String] -> Typed a
failT [String
"Unexpected Name in 'unique' " String -> String -> String
forall a. [a] -> [a] -> [a]
++ V era DeltaCoin -> String
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 V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era x -> Name era
forall era t. V era t -> Name era
Name V era x
v2
    then (Int, Bool, [Name era]) -> Typed (Int, Bool, [Name era])
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
c, Bool
b, V era x -> Name era
forall era t. V era t -> Name era
Name V era x
v2 Name era -> [Name era] -> [Name era]
forall a. a -> [a] -> [a]
: [Name era]
ns)
    else [String] -> Typed (Int, Bool, [Name era])
forall a. [String] -> Typed a
failT [String
"Unexpected Name in 'unique' " String -> String -> String
forall a. [a] -> [a] -> [a]
++ V era x -> String
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 <- Sum era c -> Typed Int
forall c era. Adds c => Sum era c -> Typed Int
summandAsInt Sum era c
sumexpr; (Int, Bool, [Name era]) -> Typed (Int, Bool, [Name era])
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
c1 Int -> Int -> Int
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) <- ((Int, Bool, [Name era])
 -> Sum era c -> Typed (Int, Bool, [Name era]))
-> (Int, Bool, [Name era])
-> [Sum era c]
-> Typed (Int, Bool, [Name era])
forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' (V era t
-> (Int, Bool, [Name era])
-> Sum era c
-> Typed (Int, Bool, [Name era])
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
_] -> (Int, Bool) -> Typed (Int, Bool)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
c, Bool
b)
    [] -> [String] -> Typed (Int, Bool)
forall a. [String] -> Typed a
failT [String
"Failed to find the unique name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nam String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Sum era c] -> String
forall a. Show a => a -> String
show [Sum era c]
ss]
    (Name era
_ : Name era
_ : [Name era]
_) -> [String] -> Typed (Int, Bool)
forall a. [String] -> Typed a
failT [String
"The expected unique name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nam String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" occurs more than once in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Sum era c] -> String
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)) | V era [a] -> Name era
forall era t. V era t -> Name era
Name V era [a]
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> ListSpec era a -> Typed (ListSpec era a)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ListSpec era a -> Typed (ListSpec era a))
-> ListSpec era a -> Typed (ListSpec era a)
forall a b. (a -> b) -> a -> b
$ Size -> ElemSpec era a -> ListSpec era a
forall era t. Size -> ElemSpec era t -> ListSpec era t
ListSpec Size
sz ElemSpec era a
forall era t. ElemSpec era t
ElemAny
  (Var V era a
v2 :=: Term era a
expr) | V era [a] -> Name era
forall era t. V era t -> Name era
Name V era [a]
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era a -> Name era
forall era t. V era t -> Name era
Name V era a
v2 -> do
    With s t1
xs <- Rep era a -> Term era a -> Typed (HasConstraint Eq [a])
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
    ListSpec era a -> Typed (ListSpec era a)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ListSpec era a -> Typed (ListSpec era a))
-> ListSpec era a -> Typed (ListSpec era a)
forall a b. (a -> b) -> a -> b
$ Size -> ElemSpec era a -> ListSpec era a
forall era t. Size -> ElemSpec era t -> ListSpec era t
ListSpec (Int -> Size
SzExact (s t1 -> Int
forall a. s a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length s t1
xs)) (Rep era a -> [a] -> ElemSpec era a
forall t era. Eq t => Rep era t -> [t] -> ElemSpec era t
ElemEqual Rep era a
Rep era a
r s t1
[a]
xs)
  (Term era a
expr :=: v2 :: Term era a
v2@(Var V era a
_)) -> V era [a] -> Pred era -> Typed (ListSpec 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 Term era a -> Term era a -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era a
expr)
  (Random (Var V era t
v2)) | V era [a] -> Name era
forall era t. V era t -> Name era
Name V era [a]
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> ListSpec era a -> Typed (ListSpec era a)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ListSpec era a -> Typed (ListSpec era a))
-> ListSpec era a -> Typed (ListSpec era a)
forall a b. (a -> b) -> a -> b
$ Size -> ElemSpec era a -> ListSpec era a
forall era t. Size -> ElemSpec era t -> ListSpec era t
ListSpec Size
SzAny ElemSpec era a
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) | V era [a] -> Name era
forall era t. V era t -> Name era
Name V era [a]
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era fs -> Name era
forall era t. V era t -> Name era
Name V era fs
v2 -> do
    let r3 :: Rep era t
r3 = Rep era fs -> Rep era t
forall era. Rep era fs -> Rep era t
forall ts a era. FromList ts a => Rep era ts -> Rep era a
tsRep Rep era fs
r2
    a :~: t
Refl <- Rep era a -> Rep era t -> Typed (a :~: t)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era a
r Rep era t
r3
    [t]
ys <- (Term era t -> Typed t) -> [Term era t] -> Typed [t]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Term era t -> Typed t
forall era t. Term era t -> Typed t
simplify [Term era t]
xs
    ListSpec era a -> Typed (ListSpec era a)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ListSpec era a -> Typed (ListSpec era a))
-> ListSpec era a -> Typed (ListSpec era a)
forall a b. (a -> b) -> a -> b
$ Size -> ElemSpec era a -> ListSpec era a
forall era t. Size -> ElemSpec era t -> ListSpec era t
ListSpec (Int -> Size
SzExact ([t] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [t]
ys)) (Rep era a -> [a] -> ElemSpec era a
forall t era. Eq t => Rep era t -> [t] -> ElemSpec era t
ElemEqual Rep era a
Rep era a
r [a]
[t]
ys)
  Pred era
cond -> [String] -> Typed (ListSpec era a)
forall a. [String] -> Typed a
failT [String
"Can't solveList " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pred era -> String
forall a. Show a => a -> String
show Pred era
cond String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" for variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ V era [a] -> String
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 =
  String -> Typed (ListSpec era a) -> Typed (ListSpec era a)
forall a. String -> Typed a -> Typed a
explain (String
"\nSolving for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", List Predicates\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines ((Pred era -> String) -> [Pred era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Pred era -> String) -> Pred era -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred era -> String
forall a. Show a => a -> String
show) [Pred era]
cs)) (Typed (ListSpec era a) -> Typed (ListSpec era a))
-> Typed (ListSpec era a) -> Typed (ListSpec era a)
forall a b. (a -> b) -> a -> b
$
    (ListSpec era a -> Pred era -> Typed (ListSpec era a))
-> ListSpec era a -> [Pred era] -> Typed (ListSpec era a)
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 ListSpec era a
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 <- V era [a] -> Pred era -> Typed (ListSpec era a)
forall era a.
Era era =>
V era [a] -> Pred era -> Typed (ListSpec era a)
solveList V era [a]
v Pred era
cond
      ListSpec era a -> Typed (ListSpec era a)
forall x. LiftT x => x -> Typed x
liftT (ListSpec era a
spec ListSpec era a -> ListSpec era a -> ListSpec era a
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)] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 = Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Rep era t -> Gen t
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] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era a -> Name era
forall era t. V era t -> Name era
Name V era a
v2 = do
  t :~: a
Refl <- Rep era t -> Rep era a -> Typed (t :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era a
r2
  a
val <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify Term era a
expr
  Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
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
_)] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era a -> Name era
forall era t. V era t -> Name era
Name V era a
v2 = do
  t :~: a
Refl <- Rep era t -> Rep era a -> Typed (t :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era a
r2
  a
val <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify Term era a
expr
  Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
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
_))] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era n -> Name era
forall era t. V era t -> Name era
Name V era n
v2 = do
  t :~: n
Refl <- Rep era t -> Rep era n -> Typed (t :~: n)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era n
r2
  n
succVal <- Term era n -> Typed n
forall era t. Term era t -> Typed t
simplify Term era n
succExpr
  Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> Gen t
forall t. Count t => t -> Gen t
genPred t
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] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era n -> Name era
forall era t. V era t -> Name era
Name V era n
v2 = do
  t :~: n
Refl <- Rep era t -> Rep era n -> Typed (t :~: n)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era n
r2
  n
predVal <- Term era n -> Typed n
forall era t. Term era t -> Typed t
simplify Term era n
predExpr
  Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> Gen t
forall t. Count t => t -> Gen t
genSucc t
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
_))] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 = do
  t :~: EpochNo
Refl <- Rep era t -> Rep era EpochNo -> Typed (t :~: EpochNo)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era EpochNo
forall era. Rep era EpochNo
EpochR
  Size
size <- Term era Size -> Typed Size
forall era t. Term era t -> Typed t
simplify Term era Size
sz
  Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen t -> Typed (Gen t)) -> Gen t -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ do
    Int
n <- Size -> Gen Int
genFromIntRange Size
size
    t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> Gen t) -> t -> Gen t
forall a b. (a -> b) -> a -> b
$ Word64 -> EpochNo
EpochNo (Word64 -> EpochNo) -> Word64 -> EpochNo
forall a b. (a -> b) -> a -> b
$ Int -> Word64
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
_))] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 = do
  t :~: SlotNo
Refl <- Rep era t -> Rep era SlotNo -> Typed (t :~: SlotNo)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era SlotNo
forall era. Rep era SlotNo
SlotNoR
  Size
size <- Term era Size -> Typed Size
forall era t. Term era t -> Typed t
simplify Term era Size
sz
  Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen t -> Typed (Gen t)) -> Gen t -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ do
    Int
n <- Size -> Gen Int
genFromIntRange Size
size
    t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> Gen t) -> t -> Gen t
forall a b. (a -> b) -> a -> b
$ Word64 -> SlotNo
SlotNo (Word64 -> SlotNo) -> Word64 -> SlotNo
forall a b. (a -> b) -> a -> b
$ Int -> Word64
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 = [String] -> Typed (Gen t)
forall a. [String] -> Typed a
failT [String]
zs
  where
    zs :: [String]
zs = (String
"Cannot solve: genCount " String -> String -> String
forall a. [a] -> [a] -> [a]
++ V era t -> String
forall a. Show a => a -> String
show V era t
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" at type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rep era t -> String
forall a. Show a => a -> String
show Rep era t
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" on Predicates") String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Pred era -> String) -> [Pred era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Pred era -> String
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) = t -> [Update t] -> t
forall t. t -> [Update t] -> t
update (ASetter t t s s -> s -> t -> t
forall s t a b. ASetter s t a b -> b -> s -> t
Lens.set ASetter t t s s
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 <- Rep era t1 -> Rep era t2 -> Typed (t1 :~: t2)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t1
rep1 Rep era t2
rep2
  Update t1 -> Typed (Update t1)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> Lens' t1 t -> Update t1
forall s t. s -> Lens' t s -> Update t
Update t
s (t -> f t) -> t1 -> f t1
(t -> f t) -> t2 -> f t2
Lens' t1 t
Lens' t2 t
l)
anyToUpdate Rep era t1
_ AnyF era t2
x = [String] -> Typed (Update t1)
forall a. [String] -> Typed a
failT [String
"component is not FConst: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AnyF era t2 -> String
forall a. Show a => a -> String
show AnyF era t2
x]

intToNatural :: Int -> Natural
intToNatural :: Int -> Natural
intToNatural Int
n = Int -> Natural
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) <- (Pred era -> Bool) -> [Pred era] -> Maybe (Pred era)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find Pred era -> Bool
forall era. Pred era -> Bool
isIf [Pred era]
preds = do
  Bool
b <- RootTarget era r Bool -> Typed Bool
forall era t root. RootTarget era root t -> Typed t
simplifyTarget RootTarget era r Bool
tar
  let others :: [Pred era]
others = (Pred era -> Bool) -> [Pred era] -> [Pred era]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Pred era -> Bool) -> Pred era -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred era -> Bool
forall era. Pred era -> Bool
isIf) [Pred era]
preds
  if Bool
b then V era t -> [Pred era] -> Typed (Gen t)
forall t era.
(HasCallStack, Era era) =>
V era t -> [Pred era] -> Typed (Gen t)
dispatch V era t
v1 (Pred era
x Pred era -> [Pred era] -> [Pred era]
forall a. a -> [a] -> [a]
: [Pred era]
others) else V era t -> [Pred era] -> Typed (Gen t)
forall t era.
(HasCallStack, Era era) =>
V era t -> [Pred era] -> Typed (Gen t)
dispatch V era t
v1 (Pred era
y Pred era -> [Pred era] -> [Pred era]
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 = String -> Typed (Gen t) -> Typed (Gen t)
forall a. String -> Typed a -> Typed a
explain (String
"Solving for variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nam String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines ((Pred era -> String) -> [Pred era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Pred era -> String
forall a. Show a => a -> String
show [Pred era]
preds)) (Typed (Gen t) -> Typed (Gen t)) -> Typed (Gen t) -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ case [Pred era]
preds of
  [Var V era a
v2 :=: Lit Rep era a
r2 a
t] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era a -> Name era
forall era t. V era t -> Name era
Name V era a
v2 -> do
    t :~: a
Refl <- Rep era t -> Rep era a -> Typed (t :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era a
r2
    Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
a
t)
  [Lit Rep era a
r2 a
t :=: Var V era a
v2] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era a -> Name era
forall era t. V era t -> Name era
Name V era a
v2 -> do
    t :~: a
Refl <- Rep era t -> Rep era a -> Typed (t :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era a
r2
    Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
a
t)
  [Term era a
expr :=: Var V era a
v2] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era a -> Name era
forall era t. V era t -> Name era
Name V era a
v2 -> do
    t :~: a
Refl <- Rep era t -> Rep era a -> Typed (t :~: a)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 (Term era a -> Rep era a
forall era t. Era era => Term era t -> Rep era t
termRep Term era a
expr)
    a
t <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify Term era a
expr
    Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
a
t)
  [Sized (Var v2 :: V era Size
v2@(V String
_ Rep era Size
r2 Access era s Size
_)) Term era t
term] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era Size -> Name era
forall era t. V era t -> Name era
Name V era Size
v2 -> do
    t :~: Size
Refl <- Rep era t -> Rep era Size -> Typed (t :~: Size)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era Size
r2
    t
x <- Term era t -> Typed t
forall era t. Term era t -> Typed t
simplify Term era t
term
    Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen t -> Typed (Gen t)) -> Gen t -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Size
SzExact (t -> Int
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
_))] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> do
    t :~: t
Refl <- Rep era t -> Rep era t -> Typed (t :~: t)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era t
r2
    Size
sz <- Term era Size -> Typed Size
forall era t. Term era t -> Typed t
simplify Term era Size
sizeterm
    Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen t -> Typed (Gen t)) -> Gen t -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ do Int
n <- Size -> Gen Int
genFromSize Size
sz; Int -> Rep era t -> Gen t
forall era t. Int -> Rep era t -> Gen t
genSizedRep Int
n Rep era t
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)])] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name (String -> Rep era t -> Access era Any t -> V era t
forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
nm Rep era t
t Access era Any t
forall era s t. Access era s t
No) -> String -> Typed (Gen t) -> Typed (Gen t)
forall a. String -> Typed a -> Typed a
explain (String
"Solving " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pred era -> String
forall a. Show a => a -> String
show Pred era
cc) (Typed (Gen t) -> Typed (Gen t)) -> Typed (Gen t) -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ do
    t :~: t
Refl <- V era t -> V era t -> Typed (t :~: t)
forall era s t. V era s -> V era t -> Typed (s :~: t)
sameV V era t
v1 (String -> Rep era t -> Access era Any t -> V era t
forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
nm Rep era t
t Access era Any t
forall era s t. Access era s t
No)
    t
x <- Term era t -> Typed t
forall era t. Term era t -> Typed t
simplify Term era t
term
    Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t
x t -> Getting t t t -> t
forall s a. s -> Getting a s a -> a
^. Getting t t t
(t -> Const t t) -> t -> Const t t
Lens' t t
lenz))
  [cc :: Pred era
cc@(Component (Right (Var V era t
v2)) [AnyF era t]
cs)] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> String -> Typed (Gen t) -> Typed (Gen t)
forall a. String -> Typed a -> Typed a
explain (String
"Solving " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pred era -> String
forall a. Show a => a -> String
show Pred era
cc) (Typed (Gen t) -> Typed (Gen t)) -> Typed (Gen t) -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ do
    [Update t]
pairs <- (AnyF era t -> Typed (Update t))
-> [AnyF era t] -> Typed [Update t]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Rep era t -> AnyF era t -> Typed (Update t)
forall era t1 t2. Rep era t1 -> AnyF era t2 -> Typed (Update t1)
anyToUpdate Rep era t
r1) [AnyF era t]
cs
    Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen t -> Typed (Gen t)) -> Gen t -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ do t
t <- Rep era t -> Gen t
forall era b. Rep era b -> Gen b
genRep Rep era t
r1; t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> [Update t] -> t
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)] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 Bool -> Bool -> Bool
&& V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v3 -> do
    [Update t]
pairs <- (AnyF era t -> Typed (Update t))
-> [AnyF era t] -> Typed [Update t]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Rep era t -> AnyF era t -> Typed (Update t)
forall era t1 t2. Rep era t1 -> AnyF era t2 -> Typed (Update t1)
anyToUpdate Rep era t
r1) [AnyF era t]
cs
    Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen t -> Typed (Gen t)) -> Gen t -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ do
      t
t <- Rep era t -> Gen t
forall era b. Rep era b -> Gen b
genRep Rep era t
r1
      t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> [Update t] -> t
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] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 Bool -> Bool -> Bool
&& V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v3 -> do
    [Update t]
pairs <- (AnyF era t -> Typed (Update t))
-> [AnyF era t] -> Typed [Update t]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Rep era t -> AnyF era t -> Typed (Update t)
forall era t1 t2. Rep era t1 -> AnyF era t2 -> Typed (Update t1)
anyToUpdate Rep era t
r1) [AnyF era t]
cs
    Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen t -> Typed (Gen t)) -> Gen t -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ do
      t
t <- Rep era t -> Gen t
forall era b. Rep era b -> Gen b
genRep Rep era t
r1
      t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> [Update t] -> t
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)] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era Size -> Name era
forall era t. V era t -> Name era
Name V era Size
v2 -> do
    t :~: Size
Refl <- Rep era t -> Rep era Size -> Typed (t :~: Size)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era Size
forall era. Rep era Size
SizeR
    Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Size
SzExact (t -> Int
forall t. Sizeable t => t -> Int
getSize t
x)))
  [Sized (Lit Rep era Size
SizeR Size
sz) (Var V era t
v2)] | Rep era t -> Bool
forall era t. Rep era t -> Bool
isAddsType Rep era t
r1 Bool -> Bool -> Bool
&& V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> do
    With s t1
_ <- Rep era t -> Rep era t -> Typed (HasConstraint Adds (Rep era t))
forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Adds (s t))
hasAdds Rep era t
r1 Rep era t
r1
    Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen t -> Typed (Gen t)) -> Gen t -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ [String] -> Int -> t
forall x. Adds x => [String] -> Int -> x
fromI [String
"dispatch " String -> String -> String
forall a. [a] -> [a] -> [a]
++ V era t -> String
forall a. Show a => a -> String
show V era t
v1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Pred era] -> String
forall a. Show a => a -> String
show [Pred era]
preds] (Int -> t) -> Gen Int -> Gen t
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] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> do
    t :~: t
Refl <- Rep era t -> Rep era t -> Typed (t :~: t)
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)
RootTarget era r (Gen t)
target
    Gen t -> Typed (Gen t)
forall a. a -> Typed a
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] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> do
    t :~: t
Refl <- Rep era t -> Rep era t -> Typed (t :~: t)
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
RootTarget era r t
target
    Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> Gen t
forall a. a -> Gen a
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))] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (ScriptF era) -> Name era
forall era t. V era t -> Name era
Name V era (ScriptF era)
v2 -> do
    t :~: ScriptF era
Refl <- Rep era t -> Rep era (ScriptF era) -> Typed (t :~: ScriptF era)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 (Proof era -> Rep era (ScriptF era)
forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR Proof era
p)
    case Term era (Map a b) -> Rep era (Map a b)
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 <- Rep era (Map a b) -> Term era (Map a b) -> Typed (Map a b)
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
        Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((a, t) -> t
forall a b. (a, b) -> b
snd ((a, t) -> t) -> Gen (a, t) -> Gen t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String] -> Map a t -> Gen (a, t)
forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"dispatch " String -> String -> String
forall a. [a] -> [a] -> [a]
++ V era t -> String
forall a. Show a => a -> String
show V era t
v1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Pred era] -> String
forall a. Show a => a -> String
show [Pred era]
preds] Map a t
Map a b
m)
      Rep era (Map a b)
other ->
        [String] -> Typed (Gen t)
forall a. [String] -> Typed a
failT
          [String
"The Pred: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pred era -> String
forall a. Show a => a -> String
show Pred era
pred1, String
"Can only be applied to a map whose range is 'Script'.", Rep era (Map a b) -> String
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))] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (ScriptF era) -> Name era
forall era t. V era t -> Name era
Name V era (ScriptF era)
v2 -> do
    t :~: ScriptF era
Refl <- Rep era t -> Rep era (ScriptF era) -> Typed (t :~: ScriptF era)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 (Proof era -> Rep era (ScriptF era)
forall era. Era era => Proof era -> Rep era (ScriptF era)
ScriptR Proof era
p)
    case Term era (Map a b) -> Rep era (Map a b)
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 <- Rep era (Map a b) -> Term era (Map a b) -> Typed (Map a b)
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
        Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((a, t) -> t
forall a b. (a, b) -> b
snd ((a, t) -> t) -> Gen (a, t) -> Gen t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String] -> Map a t -> Gen (a, t)
forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"dispatch " String -> String -> String
forall a. [a] -> [a] -> [a]
++ V era t -> String
forall a. Show a => a -> String
show V era t
v1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Pred era] -> String
forall a. Show a => a -> String
show [Pred era]
preds] Map a t
Map a b
m)
      Rep era (Map a b)
other ->
        [String] -> Typed (Gen t)
forall a. [String] -> Typed a
failT
          [String
"The Pred: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pred era -> String
forall a. Show a => a -> String
show Pred era
pred1, String
"Can only be applied to a map whose range is 'Script'.", Rep era (Map a b) -> String
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))] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Data era) -> Name era
forall era t. V era t -> Name era
Name V era (Data era)
v2 -> do
    t :~: Data era
Refl <- Rep era t -> Rep era (Data era) -> Typed (t :~: Data era)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era (Data era)
forall era. Era era => Rep era (Data era)
DataR
    case Term era (Map a b) -> Rep era (Map a b)
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 <- Rep era (Map a b) -> Term era (Map a b) -> Typed (Map a b)
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
        Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((a, t) -> t
forall a b. (a, b) -> b
snd ((a, t) -> t) -> Gen (a, t) -> Gen t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String] -> Map a t -> Gen (a, t)
forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"dispatch " String -> String -> String
forall a. [a] -> [a] -> [a]
++ V era t -> String
forall a. Show a => a -> String
show V era t
v1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Pred era] -> String
forall a. Show a => a -> String
show [Pred era]
preds] Map a t
Map a b
m)
      Rep era (Map a b)
other ->
        [String] -> Typed (Gen t)
forall a. [String] -> Typed a
failT
          [String
"The Pred: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pred era -> String
forall a. Show a => a -> String
show Pred era
pred1, String
"Can only be applied to a map whose range is 'Data'.", Rep era (Map a b) -> String
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))] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era (Data era) -> Name era
forall era t. V era t -> Name era
Name V era (Data era)
v2 -> do
    t :~: Data era
Refl <- Rep era t -> Rep era (Data era) -> Typed (t :~: Data era)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 Rep era (Data era)
forall era. Era era => Rep era (Data era)
DataR
    case Term era (Map a b) -> Rep era (Map a b)
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 <- Rep era (Map a b) -> Term era (Map a b) -> Typed (Map a b)
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
        Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((a, t) -> t
forall a b. (a, b) -> b
snd ((a, t) -> t) -> Gen (a, t) -> Gen t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String] -> Map a t -> Gen (a, t)
forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"dispatch " String -> String -> String
forall a. [a] -> [a] -> [a]
++ V era t -> String
forall a. Show a => a -> String
show V era t
v1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Pred era] -> String
forall a. Show a => a -> String
show [Pred era]
preds] Map a t
Map a b
m)
      Rep era (Map a b)
other ->
        [String] -> Typed (Gen t)
forall a. [String] -> Typed a
failT
          [String
"The Pred: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Pred era -> String
forall a. Show a => a -> String
show Pred era
pred1, String
"Can only be applied to a map whose range is 'Data'.", Rep era (Map a b) -> String
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] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era a -> Name era
forall era t. V era t -> Name era
Name V era a
v2 -> do
    t :~: a
Refl <- Rep era t -> Rep era a -> Typed (t :~: a)
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 <- Term era (Set a) -> Typed (Set a)
forall era t. Term era t -> Typed t
simplify Term era (Set a)
expr
    let msgs :: [String]
msgs = (String
"Solving for variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nam) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Pred era -> String) -> [Pred era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Pred era -> String
forall a. Show a => a -> String
show [Pred era]
preds
    if Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
set
      then
        [String] -> Typed (Gen t)
forall a. [String] -> Typed a
failT ((String
"The set is empty " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rep era (Set a) -> Set a -> String
forall e t. Rep e t -> t -> String
synopsis (Term era (Set a) -> Rep era (Set a)
forall era t. Era era => Term era t -> Rep era t
termRep Term era (Set a)
expr) Set a
set String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", can't find an element.") String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
msgs)
      else Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((t, Set t) -> t
forall a b. (a, b) -> a
fst ((t, Set t) -> t) -> Gen (t, Set t) -> Gen t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String] -> Set t -> Gen (t, Set t)
forall a. [String] -> Set a -> Gen (a, Set a)
itemFromSet [String]
msgs Set t
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] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era a -> Name era
forall era t. V era t -> Name era
Name V era a
v2 -> do
    t :~: a
Refl <- Rep era t -> Rep era a -> Typed (t :~: a)
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 <- Term era (Set a) -> Typed (Set a)
forall era t. Term era t -> Typed t
simplify Term era (Set a)
expr
    let msgs :: [String]
msgs = (String
"Solving for variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nam) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Pred era -> String) -> [Pred era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Pred era -> String
forall a. Show a => a -> String
show [Pred era]
preds
    if Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
set
      then
        [String] -> Typed (Gen t)
forall a. [String] -> Typed a
failT ((String
"The set is empty " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rep era (Set a) -> Set a -> String
forall e t. Rep e t -> t -> String
synopsis (Term era (Set a) -> Rep era (Set a)
forall era t. Era era => Term era t -> Rep era t
termRep Term era (Set a)
expr) Set a
set String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", can't find an element.") String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
msgs)
      else Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((t, Set t) -> t
forall a b. (a, b) -> a
fst ((t, Set t) -> t) -> Gen (t, Set t) -> Gen t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String] -> Set t -> Gen (t, Set t)
forall a. [String] -> Set a -> Gen (a, Set a)
itemFromSet [String]
msgs Set t
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] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era a -> Name era
forall era t. V era t -> Name era
Name V era a
v2 -> do
    t :~: a
Refl <- Rep era t -> Rep era a -> Typed (t :~: a)
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 <- Term era (Set a) -> Typed (Set a)
forall era t. Term era t -> Typed t
simplify Term era (Set a)
expr
    let msgs :: [String]
msgs = (String
"Solving for variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nam) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Pred era -> String) -> [Pred era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Pred era -> String
forall a. Show a => a -> String
show [Pred era]
preds
    Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen t -> Typed (Gen t)) -> Gen t -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ [String] -> Gen t -> (t -> Bool) -> Gen t
forall a. [String] -> Gen a -> (a -> Bool) -> Gen a
suchThatErr [String]
msgs (Rep era t -> Gen t
forall era b. Rep era b -> Gen b
genRep Rep era t
Rep era a
r2) (t -> Set t -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set t
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] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era k -> Name era
forall era t. V era t -> Name era
Name V era k
v2 -> do
    t :~: k
Refl <- Rep era t -> Rep era k -> Typed (t :~: k)
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 <- Term era (Map k v) -> Typed (Map k v)
forall era t. Term era t -> Typed t
simplify (Direct (Term era (Map k v)) -> Term era (Map k v)
forall a. Direct a -> a
direct Direct (Term era (Map k v))
exprMap)
    v
v <- Term era v -> Typed v
forall era t. Term era t -> Typed t
simplify Term era v
exprVal
    let m2 :: Map k v
m2 = (v -> Bool) -> Map k v -> Map k v
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v) Map k v
m
    let msgs :: [String]
msgs = (String
"Solving for variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nam) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Pred era -> String) -> [Pred era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Pred era -> String
forall a. Show a => a -> String
show [Pred era]
preds
    if Map k v -> Bool
forall k a. Map k a -> Bool
Map.null Map k v
m2
      then
        [String] -> Typed (Gen t)
forall a. [String] -> Typed a
failT ((String
"The value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rep era v -> v -> String
forall e t. Rep e t -> t -> String
synopsis (Term era v -> Rep era v
forall era t. Era era => Term era t -> Rep era t
termRep Term era v
exprVal) v
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not in the range of the map.") String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
msgs)
      else Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((t, Set t) -> t
forall a b. (a, b) -> a
fst ((t, Set t) -> t) -> Gen (t, Set t) -> Gen t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String] -> Set t -> Gen (t, Set t)
forall a. [String] -> Set a -> Gen (a, Set a)
itemFromSet [String]
msgs (Map t v -> Set t
forall k a. Map k a -> Set k
Map.keysSet Map t v
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] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era v -> Name era
forall era t. V era t -> Name era
Name V era v
v2 -> do
    t :~: v
Refl <- Rep era t -> Rep era v -> Typed (t :~: v)
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 <- Term era (Map k v) -> Typed (Map k v)
forall era t. Term era t -> Typed t
simplify (Direct (Term era (Map k v)) -> Term era (Map k v)
forall a. Direct a -> a
direct Direct (Term era (Map k v))
exprMap)
    k
k <- Term era k -> Typed k
forall era t. Term era t -> Typed t
simplify Term era k
exprKey
    let msgs :: [String]
msgs = (String
"Solving for variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nam) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Pred era -> String) -> [Pred era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Pred era -> String
forall a. Show a => a -> String
show [Pred era]
preds
    case k -> Map k v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k Map k v
m of
      Just v
v -> Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
v
v)
      Maybe v
Nothing -> [String] -> Typed (Gen t)
forall a. [String] -> Typed a
failT ((String
"The key: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rep era k -> k -> String
forall e t. Rep e t -> t -> String
synopsis (Term era k -> Rep era k
forall era t. Era era => Term era t -> Rep era t
termRep Term era k
exprKey) k
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not in the map.") String -> [String] -> [String]
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] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era fs -> Name era
forall era t. V era t -> Name era
Name V era fs
v2 -> do
    t :~: Maybe t1
Refl <- Rep era t -> Rep era (Maybe t1) -> Typed (t :~: Maybe t1)
forall era i j. Rep era i -> Rep era j -> Typed (i :~: j)
sameRep Rep era t
r1 (Rep era t1 -> Rep era (Maybe t1)
forall era t1. Rep era t1 -> Rep era (Maybe t1)
MaybeR Rep era t1
r2)
    [t]
xs <- (Term era t -> Typed t) -> [Term era t] -> Typed [t]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Term era t -> Typed t
forall era t. Term era t -> Typed t
simplify [Term era t]
expr
    Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen t -> Typed (Gen t)) -> Gen t -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([t] -> t
forall ts a. FromList ts a => [a] -> ts
makeFromList [t]
xs)
  [Random (Var V era t
v2)] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen t -> Typed (Gen t)) -> Gen t -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ Rep era t -> Gen t
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 <- V era t -> V era a -> Maybe (t :~: a)
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 <- V era t -> V era a -> Maybe (t :~: a)
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 <- Term era (Set a) -> Typed (Set a)
forall era t. Term era t -> Typed t
simplify Term era (Set a)
y
        Set a
zval <- Term era (Set a) -> Typed (Set a)
forall era t. Term era t -> Typed t
simplify Term era (Set a)
z
        Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
          ( (t, Set t) -> t
forall a b. (a, b) -> a
fst
              ((t, Set t) -> t) -> Gen (t, Set t) -> Gen t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String] -> Set t -> Gen (t, Set t)
forall a. [String] -> Set a -> Gen (a, Set a)
itemFromSet
                [String
"Solving (Member & NotMember), for variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nam, Pred era -> String
forall a. Show a => a -> String
show Pred era
p1, Pred era -> String
forall a. Show a => a -> String
show Pred era
p2]
                (Set t -> Set t -> Set t
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set t
Set a
yval Set t
Set a
zval)
          )
  [nm :: Pred era
nm@(NotMember {}), m :: Pred era
m@(Member {})] -> V era t -> [Pred era] -> Typed (Gen t)
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)] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> V era t -> [Pred era] -> Typed (Gen t)
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] | V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v1 Name era -> Name era -> Bool
forall a. Eq a => a -> a -> Bool
== V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v2 -> V era t -> [Pred era] -> Typed (Gen t)
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 <- V era (Map a b) -> [Pred era] -> Typed (MapSpec era a b)
forall era dom rng.
(Era era, Ord dom) =>
V era (Map dom rng) -> [Pred era] -> Typed (MapSpec era dom rng)
solveMaps V era t
V era (Map a b)
v1 [Pred era]
cs
      Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen t -> Typed (Gen t)) -> Gen t -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ String
-> [String] -> Gen a -> Gen b -> MapSpec era a b -> Gen (Map 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 ((Pred era -> String) -> [Pred era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Pred era -> String
forall a. Show a => a -> String
show [Pred era]
cs) (Rep era a -> Gen a
forall era b. Rep era b -> Gen b
genRep Rep era a
dom) (Rep era b -> Gen b
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 <- V era (Set a) -> [Pred era] -> Typed (SetSpec era a)
forall era a.
Era era =>
V era (Set a) -> [Pred era] -> Typed (SetSpec era a)
solveSets V era t
V era (Set a)
v1 [Pred era]
cs
      Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen t -> Typed (Gen t)) -> Gen t -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ [String] -> Gen a -> SetSpec era a -> Gen (Set a)
forall era a.
Era era =>
[String] -> Gen a -> SetSpec era a -> Gen (Set a)
genFromSetSpec [] (Rep era a -> Gen a
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 <- V era [a] -> [Pred era] -> Typed (ListSpec era a)
forall era a.
Era era =>
V era [a] -> [Pred era] -> Typed (ListSpec era a)
solveLists V era t
V era [a]
v1 [Pred era]
cs
      Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen t -> Typed (Gen t)) -> Gen t -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ [String] -> Gen a -> ListSpec era a -> Gen [a]
forall era r. [String] -> Gen r -> ListSpec era r -> Gen [r]
genFromListSpec [] (Rep era a -> Gen a
forall era b. Rep era b -> Gen b
genRep Rep era a
r) ListSpec era a
spec
    Rep era t
_other
      | Rep era t -> Bool
forall era t. Rep era t -> Bool
isAddsType Rep era t
r1 -> do
          With s t1
v2 <- Rep era t -> V era t -> Typed (HasConstraint Adds (V era t))
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 <- V era t1 -> [Pred era] -> Typed (AddsSpec t1)
forall t era.
(Adds t, Era era) =>
V era t -> [Pred era] -> Typed (AddsSpec t)
solveSums s t1
V era t1
v2 [Pred era]
cs
          let msgs :: [String]
msgs = (String
"Solving for variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nam) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Pred era -> String) -> [Pred era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Pred era -> String
forall a. Show a => a -> String
show [Pred era]
preds
          Gen t -> Typed (Gen t)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Gen t -> Typed (Gen t)) -> Gen t -> Typed (Gen t)
forall a b. (a -> b) -> a -> b
$ [String] -> AddsSpec t -> Gen t
forall x. Adds x => [String] -> AddsSpec x -> Gen x
genAdds [String]
msgs AddsSpec t
AddsSpec t1
sumv
      | Rep era t -> Bool
forall era t. Rep era t -> Bool
isCountType Rep era t
r1 -> do
          With s t1
v2 <- Rep era t -> V era t -> Typed (HasConstraint Count (V era t))
forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Count (s t))
hasCount Rep era t
r1 V era t
v1
          V era t -> [Pred era] -> Typed (Gen t)
forall t era. Count t => V era t -> [Pred era] -> Typed (Gen t)
genCount s t1
V era t
v2 [Pred era]
cs
      | Bool
otherwise ->
          [String] -> Typed (Gen t)
forall a. [String] -> Typed a
failT
            [ String
"No solution for "
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nam
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" at type "
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rep era t -> String
forall a. Show a => a -> String
show Rep era t
r1
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" for conditions:\n"
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Pred era] -> String
forall a. Show a => a -> String
show ((Pred era -> Pred era -> Bool) -> [Pred era] -> [Pred era]
forall a. (a -> a -> Bool) -> [a] -> [a]
List.nubBy Pred era -> Pred era -> Bool
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 Typed (Gen t) -> Either [String] (Gen t)
forall x. Typed x -> Either [String] x
runTyped (Typed (Gen t) -> Either [String] (Gen t))
-> Typed (Gen t) -> Either [String] (Gen t)
forall a b. (a -> b) -> a -> b
$
    Bool -> String -> Typed (Gen t) -> Typed (Gen t)
forall a. Bool -> String -> a -> a
ifTrace
      Bool
loud
      (Int -> String -> String
pad Int
20 (Name era -> String
forall a. Show a => a -> String
show (V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" | " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Pred era -> String) -> String -> [Pred era] -> String
forall t. (t -> String) -> String -> [t] -> String
showL Pred era -> String
forall a. Show a => a -> String
show String
"," ((Pred era -> Pred era) -> [Pred era] -> [Pred era]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era -> Pred era -> Pred era
forall era. Subst era -> Pred era -> Pred era
substPred Subst era
subst) [Pred era]
conds))
      (V era t -> [Pred era] -> Typed (Gen t)
forall t era.
(HasCallStack, Era era) =>
V era t -> [Pred era] -> Typed (Gen t)
dispatch V era t
v ((Pred era -> Pred era) -> [Pred era] -> [Pred era]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era -> Pred era -> Pred era
forall era. Subst era -> Pred era -> Pred era
substPred Subst era
subst) [Pred era]
conds)) of
    Right Gen t
gen -> do
      t
t <- Gen t
gen
      Bool
-> String
-> Gen (Either [String] (Subst era))
-> Gen (Either [String] (Subst era))
forall a. Bool -> String -> a -> a
ifTrace
        Bool
loud
        (String
"   " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rep era t -> t -> String
forall e t. Rep e t -> t -> String
synopsis Rep era t
rep t
t)
        (Either [String] (Subst era) -> Gen (Either [String] (Subst era))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst era -> Either [String] (Subst era)
forall a b. b -> Either a b
Right (V era t -> Term era t -> Subst era -> Subst era
forall era t. V era t -> Term era t -> Subst era -> Subst era
extend V era t
v (Rep era t -> t -> Term era t
forall era t. Rep era t -> t -> Term era t
Lit Rep era t
rep t
t) Subst era
subst)))
    Left [String]
msgs -> Either [String] (Subst era) -> Gen (Either [String] (Subst era))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([String] -> Either [String] (Subst era)
forall a b. a -> Either a b
Left [String]
msgs)
genOrFail Bool
_ (Right Subst era
_) ([Name era]
names, [Pred era]
_) = String -> Gen (Either [String] (Subst era))
forall a. HasCallStack => String -> a
error (String
"Multiple names not handed yet " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name era] -> String
forall a. Show a => a -> String
show [Name era]
names)
genOrFail Bool
_ (Left [String]
msgs) ([Name era], [Pred era])
_ = Either [String] (Subst era) -> Gen (Either [String] (Subst era))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([String] -> Either [String] (Subst era)
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 = (Either [String] (Subst era)
 -> ([Name era], [Pred era]) -> Gen (Either [String] (Subst era)))
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' (Bool
-> Either [String] (Subst era)
-> ([Name era], [Pred era])
-> Gen (Either [String] (Subst era))
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) = Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
forall era.
Era era =>
Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
genOrFailList Bool
loud (Subst era -> Either [String] (Subst era)
forall a b. b -> Either a b
Right Subst era
forall era. Subst era
emptySubst) [([Name era], [Pred era])]
pairs
genDependGraph Bool
loud Proof era
Allegra (DependGraph [([Name era], [Pred era])]
pairs) = Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
forall era.
Era era =>
Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
genOrFailList Bool
loud (Subst era -> Either [String] (Subst era)
forall a b. b -> Either a b
Right Subst era
forall era. Subst era
emptySubst) [([Name era], [Pred era])]
pairs
genDependGraph Bool
loud Proof era
Mary (DependGraph [([Name era], [Pred era])]
pairs) = Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
forall era.
Era era =>
Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
genOrFailList Bool
loud (Subst era -> Either [String] (Subst era)
forall a b. b -> Either a b
Right Subst era
forall era. Subst era
emptySubst) [([Name era], [Pred era])]
pairs
genDependGraph Bool
loud Proof era
Alonzo (DependGraph [([Name era], [Pred era])]
pairs) = Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
forall era.
Era era =>
Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
genOrFailList Bool
loud (Subst era -> Either [String] (Subst era)
forall a b. b -> Either a b
Right Subst era
forall era. Subst era
emptySubst) [([Name era], [Pred era])]
pairs
genDependGraph Bool
loud Proof era
Babbage (DependGraph [([Name era], [Pred era])]
pairs) = Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
forall era.
Era era =>
Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
genOrFailList Bool
loud (Subst era -> Either [String] (Subst era)
forall a b. b -> Either a b
Right Subst era
forall era. Subst era
emptySubst) [([Name era], [Pred era])]
pairs
genDependGraph Bool
loud Proof era
Conway (DependGraph [([Name era], [Pred era])]
pairs) = Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
forall era.
Era era =>
Bool
-> Either [String] (Subst era)
-> [([Name era], [Pred era])]
-> Gen (Either [String] (Subst era))
genOrFailList Bool
loud (Subst era -> Either [String] (Subst era)
forall a b. b -> Either a b
Right Subst era
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 <- Typed (Gen t) -> Gen (Gen t)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (V era t -> [Pred era] -> Typed (Gen t)
forall t era.
(HasCallStack, Era era) =>
V era t -> [Pred era] -> Typed (Gen t)
dispatch V era t
v ((Pred era -> Pred era) -> [Pred era] -> [Pred era]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era -> Pred era -> Pred era
forall era. Subst era -> Pred era -> Pred era
substPred Subst era
subst) [Pred era]
ps)) -- Sub solution for previously solved variables
  !t
t <- Gen t
genOneT
  Subst era -> Gen (Subst era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (V era t -> Term era t -> Subst era -> Subst era
forall era t. V era t -> Term era t -> Subst era -> Subst era
extend V era t
v (Rep era t -> t -> Term era t
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, (Pred era -> Pred era) -> [Pred era] -> [Pred era]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era -> Pred era -> Pred era
forall era. Subst era -> Pred era -> Pred era
substPred Subst era
subst0) [Pred era]
preds) of
  ([Name era]
ns, [SumSplit c
small Term era c
tot OrdCond
EQL [Sum era c]
suml]) | [Name era] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name era]
ns Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Sum era c] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sum era c]
suml -> do
    !c
n <- Typed c -> Gen c
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed c -> Gen c) -> Typed c -> Gen c
forall a b. (a -> b) -> a -> b
$ Term era c -> Typed c
forall era t. Term era t -> Typed t
simplify Term era c
tot
    ![c]
zs <-
      c -> [String] -> Int -> c -> Gen [c]
forall x. Adds x => x -> [String] -> Int -> x -> Gen [x]
partition
        c
small
        [String
"Partition, while solving multiple SumsTo vars.", [Name era] -> String
forall a. Show a => a -> String
show [Name era]
ns, [Pred era] -> String
forall a. Show a => a -> String
show [Pred era]
preds]
        ([Name era] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name era]
ns)
        c
n
    let rep :: Rep era c
rep = Term era c -> Rep era c
forall era t. Era era => Term era t -> Rep era t
termRep Term era c
tot
    (Subst era -> (Sum era c, c) -> Gen (Subst era))
-> Subst era -> [(Sum era c, c)] -> Gen (Subst era)
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) -> Sum era c -> Rep era c -> c -> Subst era -> Gen (Subst era)
forall x era.
Adds x =>
Sum era x -> Rep era x -> x -> Subst era -> Gen (Subst era)
genSum (Subst era -> Sum era c -> Sum era c
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 ([Sum era c] -> [c] -> [(Sum era c, c)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Sum era c]
suml [c]
zs)
  ([Name era]
ns, [Pred era]
ps) -> String -> [String] -> Gen (Subst era)
forall a. HasCallStack => String -> [String] -> a
errorMess String
"Not yet. multiple vars in solveOneVar" [[Name era] -> String
forall a. Show a => a -> String
show [Name era]
ns, [Pred era] -> String
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) <- OrderInfo -> Subst era -> [Pred era] -> Gen (Int, DependGraph era)
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 <- (Subst era -> ([Name era], [Pred era]) -> Gen (Subst era))
-> Subst era -> [([Name era], [Pred era])] -> Gen (Subst era)
forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' Subst era -> ([Name era], [Pred era]) -> Gen (Subst era)
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 (Char -> t Char -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
'.' t Char
k)
  Subst era -> Gen (Subst era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst era -> Gen (Subst era)) -> Subst era -> Gen (Subst era)
forall a b. (a -> b) -> a -> b
$ (Map String (SubstElem era) -> Subst era
forall era. Map String (SubstElem era) -> Subst era
Subst ((String -> SubstElem era -> Bool)
-> Map String (SubstElem era) -> Map String (SubstElem era)
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\String
k SubstElem era
_ -> String -> Bool
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) <- OrderInfo -> Subst era -> [Pred era] -> Gen (Int, DependGraph era)
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 <- (Subst era -> ([Name era], [Pred era]) -> Gen (Subst era))
-> Subst era -> [([Name era], [Pred era])] -> Gen (Subst era)
forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' Subst era -> ([Name era], [Pred era]) -> Gen (Subst era)
forall era.
Era era =>
Subst era -> ([Name era], [Pred era]) -> Gen (Subst era)
solveOneVar Subst era
subst0 [([Name era], [Pred era])]
pairs
  Typed (Env era) -> Gen (Env era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env era) -> Gen (Env era))
-> Typed (Env era) -> Gen (Env era)
forall a b. (a -> b) -> a -> b
$ Subst era -> Env era -> Typed (Env era)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst Env era
forall era. Env era
emptyEnv