{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}

-- | The types that make up the Abstract Syntax Trees of the Language
module Test.Cardano.Ledger.Constrained.Ast where

import Cardano.Ledger.Coin (Coin (..), DeltaCoin (..))
import Cardano.Ledger.Core (Era (EraCrypto), hashScript)
import Cardano.Ledger.Hashes (DataHash, ScriptHash (..))
import Cardano.Ledger.Plutus.Data (Data (..), hashData)
import Data.Char (toLower)
import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import Data.Hashable (Hashable)
import qualified Data.List as List
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Text (Text, pack)
import qualified Data.Universe as Univ (Any (..))
import Data.Void (Void)
import Data.Word (Word64)
import Lens.Micro
import Test.Cardano.Ledger.Constrained.Classes (
  Adds (..),
  Count (..),
  OrdCond (..),
  ScriptF (..),
  Sizeable (..),
 )
import Test.Cardano.Ledger.Constrained.Env (
  Access (..),
  AnyF (..),
  Env (..),
  Field (..),
  Name (..),
  Payload (..),
  V (..),
  findVar,
  storeVar,
 )
import Test.Cardano.Ledger.Constrained.Monad (HasConstraint (With), Typed (..), failT, monadTyped)
import Test.Cardano.Ledger.Constrained.Size (Size (..), runSize, seps)
import Test.Cardano.Ledger.Constrained.TypeRep (
  Rep (..),
  format,
  hasEq,
  synopsis,
  testEql,
  (:~:) (Refl),
 )
import Test.Cardano.Ledger.Generic.PrettyCore (PDoc, ppRecord, ppString)
import Test.Cardano.Ledger.Generic.Proof (Reflect)
import Test.QuickCheck (Gen, oneof)
import Type.Reflection (TypeRep, Typeable, typeRep)

-- =========================================================
-- class FromList cannot be defined in Classes.hs because
-- (Rep era t) for method tsRep is not in scope

class (Eq a, Eq ts) => FromList ts a | ts -> a where
  makeFromList :: [a] -> ts
  getList :: ts -> [a]
  tsRep :: Rep era ts -> Rep era a

instance Eq a => FromList [a] a where
  makeFromList :: [a] -> [a]
makeFromList [a]
xs = [a]
xs
  getList :: [a] -> [a]
getList [a]
xs = [a]
xs
  tsRep :: forall era. Rep era [a] -> Rep era a
tsRep (ListR Rep era a
z) = Rep era a
z

instance Eq a => FromList (Maybe a) a where
  makeFromList :: [a] -> Maybe a
makeFromList [] = forall a. Maybe a
Nothing
  makeFromList (a
x : [a]
_) = forall a. a -> Maybe a
Just a
x
  getList :: Maybe a -> [a]
getList Maybe a
Nothing = []
  getList (Just a
x) = [a
x]
  tsRep :: forall era. Rep era (Maybe a) -> Rep era a
tsRep (MaybeR Rep era t
z) = Rep era t
z

instance (Ord k, Eq a) => FromList (Map k a) (k, a) where
  makeFromList :: [(k, a)] -> Map k a
makeFromList = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
  getList :: Map k a -> [(k, a)]
getList = forall k a. Map k a -> [(k, a)]
Map.toList
  tsRep :: forall era. Rep era (Map k a) -> Rep era (k, a)
tsRep (MapR Rep era a
k Rep era b
v) = forall era s b. Rep era s -> Rep era b -> Rep era (s, b)
PairR Rep era a
k Rep era b
v

-- | CAREFULL HERE, this instance may NOT be size preserving.
instance Ord a => FromList (Set a) a where
  makeFromList :: [a] -> Set a
makeFromList = forall a. Ord a => [a] -> Set a
Set.fromList
  getList :: Set a -> [a]
getList = forall a. Set a -> [a]
Set.toList
  tsRep :: forall era. Rep era (Set a) -> Rep era a
tsRep (SetR Rep era a
x) = Rep era a
x

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

type Direct a = Either a a

direct :: Direct a -> a
direct :: forall a. Direct a -> a
direct (Left a
a) = a
a
direct (Right a
a) = a
a

data Term era t where
  Lit :: Rep era t -> t -> Term era t
  Var :: V era t -> Term era t
  Dom :: Ord a => Term era (Map a b) -> Term era (Set a)
  Rng :: (Ord a, Ord b) => Term era (Map a b) -> Term era (Set b)
  Elems :: (Ord a, Eq b) => Term era (Map a b) -> Term era [b]
  ProjM :: Ord a => Lens' b t -> Rep era t -> Term era (Map a b) -> Term era (Map a t)
  ProjS :: (Ord b, Ord t) => Lens' b t -> Rep era t -> Term era (Set b) -> Term era (Set t)
  Proj :: Lens' b t -> Rep era t -> Term era b -> Term era t
  Delta :: Term era Coin -> Term era DeltaCoin
  Negate :: Term era DeltaCoin -> Term era DeltaCoin
  Restrict :: Ord a => Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
  HashD :: Era era => Term era (Data era) -> Term era (DataHash (EraCrypto era))
  HashS :: Reflect era => Term era (ScriptF era) -> Term era (ScriptHash (EraCrypto era))
  Pair :: Term era a -> Term era b -> Term era (a, b)

infix 4 :=:
infix 4 :<-:

data Pred era where
  MetaSize :: Size -> Term era Size -> Pred era
  Sized :: Sizeable t => Term era Size -> Term era t -> Pred era
  (:=:) :: Eq a => Term era a -> Term era a -> Pred era
  Subset :: Ord a => Term era (Set a) -> Term era (Set a) -> Pred era
  Disjoint :: Ord a => Term era (Set a) -> Term era (Set a) -> Pred era
  SumsTo :: (Era era, Adds c) => (Direct c) -> Term era c -> OrdCond -> [Sum era c] -> Pred era
  SumSplit :: (Era era, Adds c) => c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
  Random :: Term era t -> Pred era
  Component :: Direct (Term era t) -> [AnyF era t] -> Pred era
  CanFollow :: Count n => Term era n -> Term era n -> Pred era
  Member :: Ord a => Direct (Term era a) -> Term era (Set a) -> Pred era
  NotMember :: Ord a => Term era a -> Term era (Set a) -> Pred era
  MapMember ::
    (Ord k, Eq v, Ord v) => Term era k -> Term era v -> (Direct (Term era (Map k v))) -> Pred era
  (:<-:) :: Term era t -> RootTarget era r t -> Pred era
  GenFrom :: Term era t -> RootTarget era r (Gen t) -> Pred era
  List :: FromList fs t => Term era fs -> [Term era t] -> Pred era
  Choose ::
    (Era era, Eq t) => Term era Size -> Term era [t] -> [(Int, Target era t, [Pred era])] -> Pred era
  ForEach ::
    (Era era, FromList fs t, Eq t) =>
    Term era Size ->
    Term era fs ->
    Pat era t ->
    [Pred era] ->
    Pred era
  Maybe ::
    forall r era t.
    (Era era, Typeable r) =>
    Term era (Maybe t) ->
    RootTarget era r t ->
    [Pred era] ->
    Pred era
  Oneof :: (Eq t, Era era) => Term era t -> [(Int, RootTarget era t t, [Pred era])] -> Pred era
  SubMap :: (Ord k, Eq v, Ord v) => Term era (Map k v) -> Term era (Map k v) -> Pred era
  If :: RootTarget era r Bool -> Pred era -> Pred era -> Pred era
  Before :: Term era a -> Term era b -> Pred era
  ListWhere ::
    (Era era, Eq t) => Term era Size -> Term era [t] -> RootTarget era t t -> [Pred era] -> Pred era

data Sum era c where
  SumMap :: Adds c => Term era (Map a c) -> Sum era c
  SumList :: Adds c => Term era [c] -> Sum era c
  One :: Term era c -> Sum era c
  ProjOne :: forall x c era. Lens' x c -> Rep era c -> Term era x -> Sum era c
  ProjMap :: forall x c a era. Adds c => Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c

-- ====================================================================
-- Special patterns for building literal Terms of type Size and Word64

infix 4 :⊆:
pattern (:⊆:) :: forall era. (forall a. Ord a => Term era (Set a) -> Term era (Set a) -> Pred era)
pattern x $b:⊆: :: forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
$m:⊆: :: forall {r} {era}.
Pred era
-> (forall {a}. Ord a => Term era (Set a) -> Term era (Set a) -> r)
-> ((# #) -> r)
-> r
:⊆: y = Subset x y

pattern ExactSize :: Era era => Int -> Term era Size
pattern $bExactSize :: forall era. Era era => Int -> Term era Size
$mExactSize :: forall {r} {era}.
Era era =>
Term era Size -> (Int -> r) -> ((# #) -> r) -> r
ExactSize x <- (sameRng -> Just x)
  where
    ExactSize Int
x = forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Size
SizeR (Int -> Int -> Size
SzRng Int
x Int
x)

pattern AtLeast :: Era era => Int -> Term era Size
pattern $bAtLeast :: forall era. Era era => Int -> Term era Size
$mAtLeast :: forall {r} {era}.
Era era =>
Term era Size -> (Int -> r) -> ((# #) -> r) -> r
AtLeast n = Lit SizeR (SzLeast n)

pattern Size :: Era era => Size -> Term era Size
pattern $bSize :: forall era. Era era => Size -> Term era Size
$mSize :: forall {r} {era}.
Era era =>
Term era Size -> (Size -> r) -> ((# #) -> r) -> r
Size n = Lit SizeR n

pattern AtMost :: Era era => Int -> Term era Size
pattern $bAtMost :: forall era. Era era => Int -> Term era Size
$mAtMost :: forall {r} {era}.
Era era =>
Term era Size -> (Int -> r) -> ((# #) -> r) -> r
AtMost n = Lit SizeR (SzMost n)

pattern Range :: Era era => Int -> Int -> Term era Size
pattern $bRange :: forall era. Era era => Int -> Int -> Term era Size
$mRange :: forall {r} {era}.
Era era =>
Term era Size -> (Int -> Int -> r) -> ((# #) -> r) -> r
Range i j <- Lit SizeR (SzRng i j)
  where
    Range Int
i Int
j =
      if Int
i forall a. Ord a => a -> a -> Bool
<= Int
j
        then forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Size
SizeR (Int -> Int -> Size
SzRng Int
i Int
j)
        else
          forall a. HasCallStack => [Char] -> a
error
            ( [Char]
"Bad call to "
                forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Int -> Int -> Size
SzRng Int
i Int
j)
                forall a. [a] -> [a] -> [a]
++ [Char]
". It is not the case that ("
                forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i
                forall a. [a] -> [a] -> [a]
++ [Char]
" <= "
                forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
j
                forall a. [a] -> [a] -> [a]
++ [Char]
")."
            )

sameRng :: Term era Size -> Maybe Int
sameRng :: forall era. Term era Size -> Maybe Int
sameRng (Lit Rep era Size
SizeR (SzRng Int
x Int
y)) = if Int
x forall a. Eq a => a -> a -> Bool
== Int
y then forall a. a -> Maybe a
Just Int
x else forall a. Maybe a
Nothing
sameRng Term era Size
_ = forall a. Maybe a
Nothing

pattern Word64 :: Era era => Word64 -> Term era Word64
pattern $bWord64 :: forall era. Era era => Word64 -> Term era Word64
$mWord64 :: forall {r} {era}.
Era era =>
Term era Word64 -> (Word64 -> r) -> ((# #) -> r) -> r
Word64 x = Lit Word64R x

var :: Era era => String -> Rep era t -> Term era t
var :: forall era t. Era era => [Char] -> Rep era t -> Term era t
var [Char]
s Rep era t
r = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
s Rep era t
r forall era s t. Access era s t
No)

unVar :: Term era t -> V era t
unVar :: forall era t. Term era t -> V era t
unVar (Var V era t
v) = V era t
v
unVar Term era t
x = forall a. HasCallStack => [Char] -> a
error ([Char]
"Non Var in unVar: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era t
x)

fieldToTerm :: Field era rec field -> Term era field
fieldToTerm :: forall era rec field. Field era rec field -> Term era field
fieldToTerm (Field [Char]
nm Rep era field
rep Rep era rec
repx Lens' rec field
l) = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
nm Rep era field
rep (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era rec
repx Lens' rec field
l))
fieldToTerm (FConst Rep era field
rep field
t Rep era rec
_ Lens' rec field
_) = forall era t. Rep era t -> t -> Term era t
Lit Rep era field
rep field
t

-- | (select small big lens), 'big' is evaluated to a value, 'small' is a Var, constrain 'small'
--   such that it is bound to the 'lens' component of 'big'. Computes a (:=:) Pred
select :: (Eq t, Era era) => Term era t -> Term era big -> Lens' big t -> Pred era
select :: forall t era big.
(Eq t, Era era) =>
Term era t -> Term era big -> Lens' big t -> Pred era
select Term era t
small Term era big
big Lens' big t
lenz = forall s t era. Lens' s t -> Rep era t -> Term era s -> Term era t
Proj Lens' big t
lenz (forall era t. Era era => Term era t -> Rep era t
termRep Term era t
small) Term era big
big forall s era. Eq s => Term era s -> Term era s -> Pred era
:=: Term era t
small

-- | (select small big lens), 'big' is evaluated to a value, 'small' is a Var, constrain 'small'
--   such that it is bound to the 'lens' component of 'big'. Computes a 'Component' Pred
select2 :: Era era => Term era t -> Term era big -> Lens' big t -> Pred era
select2 :: forall era t big.
Era era =>
Term era t -> Term era big -> Lens' big t -> Pred era
select2 (Var (V [Char]
nm Rep era t
t Access era s t
_)) Term era big
big Lens' big t
lenz = forall era s. Direct (Term era s) -> [AnyF era s] -> Pred era
Component (forall a b. a -> Either a b
Left Term era big
big) [forall era s s. Field era s s -> AnyF era s
AnyF (forall era t s.
Era era =>
[Char] -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field [Char]
nm Rep era t
t (forall era t. Era era => Term era t -> Rep era t
termRep Term era big
big) Lens' big t
lenz)]
select2 Term era t
t1 Term era big
t2 Lens' big t
_ =
  forall a. HasCallStack => [Char] -> a
error ([Char]
"In (select " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era t
t1 forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era big
t2 forall a. [a] -> [a] -> [a]
++ [Char]
" lens)  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era t
t1 forall a. [a] -> [a] -> [a]
++ [Char]
" is not a Var term.")

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

infixl 0 :$

data RootTarget era root t where
  Simple :: Term era t -> RootTarget era Void t
  (:$) :: RootTarget era r (a -> b) -> RootTarget era r a -> RootTarget era r b
  Constr :: String -> (a -> b) -> RootTarget era Void (a -> b)
  Invert :: String -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
  Lensed :: Term era t -> SimpleGetter root t -> RootTarget era root t
  Partial ::
    Term era t ->
    (root -> Maybe t) ->
    -- | Partial designed to be used in Pred 'Oneof' where the RootTarget getter may fail.
    --   So use 'Partial' instead of 'Lensed' in 'Oneof'
    RootTarget era root t
  Shift :: RootTarget era root2 a -> Lens' root1 root2 -> RootTarget era root1 a
  Mask :: RootTarget era r a -> RootTarget era Void a
  Virtual ::
    Term era t ->
    PDoc ->
    Lens' root t ->
    -- | Just like Lensed but uses the String to name the field (instead of the Term)
    RootTarget era root t

-- Treat a Target as if it's (RootTarget era Void t)

type Target era t = RootTarget era Void t

infixl 0 ^$

-- | Version of (:$) That takes a Term on the right, rather than a Target
(^$) :: Target era (a -> t) -> Term era a -> Target era t
^$ :: forall era a t. Target era (a -> t) -> Term era a -> Target era t
(^$) Target era (a -> t)
f Term era a
x = Target era (a -> t)
f forall era r s b.
RootTarget era r (s -> b)
-> RootTarget era r s -> RootTarget era r b
:$ forall era t. Term era t -> RootTarget era Void t
Simple Term era a
x

constTarget :: t -> Target era t
constTarget :: forall t era. t -> Target era t
constTarget t
t = forall s b era. [Char] -> (s -> b) -> RootTarget era Void (s -> b)
Constr [Char]
"constTarget" (forall a b. a -> b -> a
const t
t) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era ()
UnitR ()

constRootTarget :: forall era t. Typeable t => t -> RootTarget era t t
constRootTarget :: forall era t. Typeable t => t -> RootTarget era t t
constRootTarget t
t = forall root s b era.
[Char] -> TypeRep root -> (s -> b) -> RootTarget era root (s -> b)
Invert [Char]
"constRootTarget" (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t) (\() -> t
t) forall era r s b.
RootTarget era r (s -> b)
-> RootTarget era r s -> RootTarget era r b
:$ forall era t root.
Term era t -> SimpleGetter root t -> RootTarget era root t
Lensed (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era ()
UnitR ()) (forall s a. (s -> a) -> SimpleGetter s a
to (forall a b. a -> b -> a
const ()))

emptyTarget :: Target era ()
emptyTarget :: forall era. Target era ()
emptyTarget = forall era t. Term era t -> RootTarget era Void t
Simple (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era ()
UnitR ())

justTarget :: Term era t -> Target era (Maybe t)
justTarget :: forall era t. Term era t -> Target era (Maybe t)
justTarget Term era t
x = forall s b era. [Char] -> (s -> b) -> RootTarget era Void (s -> b)
Constr [Char]
"Just" forall a. a -> Maybe a
Just forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era t
x

idTarget :: Term era t -> Target era t
idTarget :: forall era t. Term era t -> RootTarget era Void t
idTarget Term era t
x = forall s b era. [Char] -> (s -> b) -> RootTarget era Void (s -> b)
Constr [Char]
"id" forall a. a -> a
id forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era t
x

-- | Usefull when using the Pred 'FromGen'
--   E.g. (FromGen termMaybeT (maybeTarget ^$ termT))
maybeTarget :: Target era (t -> Gen (Maybe t))
maybeTarget :: forall era t. Target era (t -> Gen (Maybe t))
maybeTarget = forall s b era. [Char] -> (s -> b) -> RootTarget era Void (s -> b)
Constr [Char]
"maybeTarget" forall {a}. a -> Gen (Maybe a)
genMaybe
  where
    genMaybe :: a -> Gen (Maybe a)
genMaybe a
x = forall a. HasCallStack => [Gen a] -> Gen a
oneof [forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing, forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Maybe a
Just a
x)]

listToSetTarget :: Ord x => Term era [x] -> Target era (Set.Set x)
listToSetTarget :: forall x era. Ord x => Term era [x] -> Target era (Set x)
listToSetTarget Term era [x]
x = forall s b era. [Char] -> (s -> b) -> RootTarget era Void (s -> b)
Constr [Char]
"FromList" forall a. Ord a => [a] -> Set a
Set.fromList forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [x]
x

setToListTarget :: Term era (Set x) -> Target era [x]
setToListTarget :: forall era x. Term era (Set x) -> Target era [x]
setToListTarget Term era (Set x)
x = forall s b era. [Char] -> (s -> b) -> RootTarget era Void (s -> b)
Constr [Char]
"toList" forall a. Set a -> [a]
Set.toList forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set x)
x

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

showL :: (t -> String) -> [Char] -> [t] -> [Char]
showL :: forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL t -> [Char]
_f [Char]
_sep [] = [Char]
""
showL t -> [Char]
f [Char]
_sep [t
t] = t -> [Char]
f t
t
showL t -> [Char]
f [Char]
sep (t
t : [t]
ts) = t -> [Char]
f t
t forall a. [a] -> [a] -> [a]
++ [Char]
sep forall a. [a] -> [a] -> [a]
++ forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL t -> [Char]
f [Char]
sep [t]
ts

instance Show (Term era t) where
  show :: Term era t -> [Char]
show (Lit Rep era t
r t
k) = forall e t. Rep e t -> t -> [Char]
synopsis Rep era t
r t
k
  show (Var (V [Char]
nm Rep era t
_rep Access era s t
_)) = [Char]
nm -- ++ "::" ++ show _rep
  show (Dom Term era (Map a b)
x) = [Char]
"(Dom " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Map a b)
x forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Rng Term era (Map a b)
x) = [Char]
"(Rng " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Map a b)
x forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Elems Term era (Map a b)
x) = [Char]
"(Elems " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Map a b)
x forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (ProjM Lens' b t
_ Rep era t
r Term era (Map a b)
t) = [Char]
"(ProjM " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Rep era t
r forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Map a b)
t forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (ProjS Lens' b t
_ Rep era t
r Term era (Set b)
t) = [Char]
"(ProjS " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Rep era t
r forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Set b)
t forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Proj Lens' b t
_ Rep era t
r Term era b
t) = [Char]
"(Proj " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Rep era t
r forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era b
t forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Delta Term era Coin
x) = [Char]
"(Delta " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era Coin
x forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Negate Term era DeltaCoin
x) = [Char]
"(Negate " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era DeltaCoin
x forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Restrict Term era (Set a)
r Term era (Map a b)
t) = [Char]
"(Restrict " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Set a)
r forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Map a b)
t forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (HashS Term era (ScriptF era)
r) = [Char]
"(HashS " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (ScriptF era)
r forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (HashD Term era (Data era)
r) = [Char]
"(HashD " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Data era)
r forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Pair Term era a
r Term era b
t) = [Char]
"(Pair " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era a
r forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era b
t forall a. [a] -> [a] -> [a]
++ [Char]
")"
  showList :: [Term era t] -> ShowS
showList [Term era t]
xs [Char]
ans = [[Char]] -> [Char]
unlines ([Char]
ans forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> [Char]
show [Term era t]
xs)

instance Show (Sum era c) where
  show :: Sum era c -> [Char]
show (SumMap Term era (Map a c)
t) = [Char]
"sum " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Map a c)
t
  show (SumList Term era [c]
t) = [Char]
"sum " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era [c]
t
  show (One Term era c
t) = forall a. Show a => a -> [Char]
show Term era c
t
  show (ProjOne Lens' x c
_ Rep era c
c Term era x
t) = [[Char]] -> [Char]
seps [[Char]
"ProjOne", forall a. Show a => a -> [Char]
show Rep era c
c, forall a. Show a => a -> [Char]
show Term era x
t]
  show (ProjMap Rep era c
crep Lens' x c
_lens Term era (Map a x)
t) = [Char]
"ProjMap " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Rep era c
crep forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Map a x)
t

instance Show (Pred era) where
  show :: Pred era -> [Char]
show (MetaSize Size
n Term era Size
t) = [Char]
"MetaSize " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Size
n forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era Size
t
  show (Sized Term era Size
n Term era t
t) = [Char]
"Sized " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era Size
n forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era t
t
  show (Term era a
x :=: Term era a
y) = forall a. Show a => a -> [Char]
show Term era a
x forall a. [a] -> [a] -> [a]
++ [Char]
" :=: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era a
y
  show (Subset Term era (Set a)
x Term era (Set a)
y) = forall a. Show a => a -> [Char]
show Term era (Set a)
x forall a. [a] -> [a] -> [a]
++ [Char]
" ⊆  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Set a)
y
  show (Disjoint Term era (Set a)
x Term era (Set a)
y) = [Char]
"Disjoint " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Set a)
x forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Set a)
y
  show (SumsTo Direct c
i Term era c
c OrdCond
cond [Sum era c]
m) = [Char]
"SumsTo (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Direct c
i forall a. [a] -> [a] -> [a]
++ [Char]
") " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era c
c forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show OrdCond
cond forall a. [a] -> [a] -> [a]
++ forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL forall a. Show a => a -> [Char]
show [Char]
" + " [Sum era c]
m
  show (SumSplit c
i Term era c
c OrdCond
cond [Sum era c]
m) = [Char]
"SumSplit (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show c
i forall a. [a] -> [a] -> [a]
++ [Char]
") " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era c
c forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show OrdCond
cond forall a. [a] -> [a] -> [a]
++ forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL forall a. Show a => a -> [Char]
show [Char]
" + " [Sum era c]
m
  show (Random Term era t
x) = [Char]
"Random " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era t
x
  show (Component Direct (Term era t)
t [AnyF era t]
ws) = [Char]
"Component (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Direct (Term era t)
t forall a. [a] -> [a] -> [a]
++ [Char]
") " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [AnyF era t]
ws
  show (CanFollow Term era n
x Term era n
y) = [Char]
"CanFollow " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era n
x forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era n
y
  show (Member Direct (Term era a)
x Term era (Set a)
y) = [Char]
"Member (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Direct (Term era a)
x forall a. [a] -> [a] -> [a]
++ [Char]
") " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Set a)
y
  show (NotMember Term era a
x Term era (Set a)
y) = [Char]
"NotMember " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era a
x forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Set a)
y
  show (MapMember Term era k
k Term era v
v Direct (Term era (Map k v))
m) = [Char]
"MapMember " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era k
k forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era v
v forall a. [a] -> [a] -> [a]
++ [Char]
" (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Direct (Term era (Map k v))
m forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Term era t
x :<-: RootTarget era r t
y) = forall a. Show a => a -> [Char]
show Term era t
x forall a. [a] -> [a] -> [a]
++ [Char]
" :<-: " forall a. [a] -> [a] -> [a]
++ forall era t r. RootTarget era r t -> [Char]
showT RootTarget era r t
y
  show (GenFrom Term era t
x RootTarget era r (Gen t)
y) = [Char]
"GenFrom " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era t
x forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall era t r. RootTarget era r t -> [Char]
showT RootTarget era r (Gen t)
y
  show (List Term era fs
t [Term era t]
xs) = [Char]
"List " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era fs
t forall a. [a] -> [a] -> [a]
++ [Char]
" [" forall a. [a] -> [a] -> [a]
++ forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL forall a. Show a => a -> [Char]
show [Char]
", " [Term era t]
xs forall a. [a] -> [a] -> [a]
++ [Char]
"]"
  show (Choose Term era Size
s Term era [t]
term [(Int, Target era t, [Pred era])]
xs) = [[Char]] -> [Char]
unlines (([Char]
"Choose " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era Size
s forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era [t]
term) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall {a} {t} {era} {r} {t}.
(Show a, Show t) =>
(a, RootTarget era r t, [t]) -> [Char]
showchoices [(Int, Target era t, [Pred era])]
xs)
    where
      showchoices :: (a, RootTarget era r t, [t]) -> [Char]
showchoices (a
i, RootTarget era r t
target, [t]
ps) =
        [Char]
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
i forall a. [a] -> [a] -> [a]
++ [Char]
", " forall a. [a] -> [a] -> [a]
++ forall era r t. RootTarget era r t -> [Char]
showAllTarget RootTarget era r t
target forall a. [a] -> [a] -> [a]
++ forall era t r. RootTarget era r t -> [Char]
showT RootTarget era r t
target forall a. [a] -> [a] -> [a]
++ [Char]
" | " forall a. [a] -> [a] -> [a]
++ forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL forall a. Show a => a -> [Char]
show [Char]
", " [t]
ps forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Oneof Term era t
term [(Int, RootTarget era t t, [Pred era])]
xs) = [[Char]] -> [Char]
unlines (([Char]
"Oneof " forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era t
term) forall a. a -> [a] -> [a]
: (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {t} {era} {r} {t}.
(Show a, Show t) =>
(a, RootTarget era r t, [t]) -> [Char]
showchoices [(Int, RootTarget era t t, [Pred era])]
xs))
    where
      showchoices :: (a, RootTarget era r t, [t]) -> [Char]
showchoices (a
i, RootTarget era r t
target, [t]
ps) =
        [Char]
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
i forall a. [a] -> [a] -> [a]
++ [Char]
", " forall a. [a] -> [a] -> [a]
++ forall era r t. RootTarget era r t -> [Char]
showAllTarget RootTarget era r t
target forall a. [a] -> [a] -> [a]
++ forall era t r. RootTarget era r t -> [Char]
showT RootTarget era r t
target forall a. [a] -> [a] -> [a]
++ [Char]
" | " forall a. [a] -> [a] -> [a]
++ forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL forall a. Show a => a -> [Char]
show [Char]
", " [t]
ps forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (ForEach Term era Size
s Term era fs
term Pat era t
pat [Pred era]
ps) =
    [[Char]] -> [Char]
unlines
      [ [[Char]] -> [Char]
seps [[Char]
"ForEach", forall a. Show a => a -> [Char]
show Term era Size
s, forall a. Show a => a -> [Char]
show Term era fs
term]
      , [Char]
"forall (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Pat era t
pat forall a. [a] -> [a] -> [a]
++ [Char]
" | " forall a. [a] -> [a] -> [a]
++ forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL forall a. Show a => a -> [Char]
show [Char]
", " [Pred era]
ps
      ]
  show (Maybe Term era (Maybe t)
term RootTarget era r t
target [Pred era]
ps) = [Char]
"Maybe " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Maybe t)
term forall a. [a] -> [a] -> [a]
++ forall era r t. RootTarget era r t -> [Char]
showAllTarget RootTarget era r t
target forall a. [a] -> [a] -> [a]
++ [Char]
" | " forall a. [a] -> [a] -> [a]
++ forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL forall a. Show a => a -> [Char]
show [Char]
", " [Pred era]
ps
  show (SubMap Term era (Map k v)
x Term era (Map k v)
y) = [Char]
"SubMap " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Map k v)
x forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era (Map k v)
y
  show (If RootTarget era r Bool
t Pred era
x Pred era
y) = [Char]
"If (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show RootTarget era r Bool
t forall a. [a] -> [a] -> [a]
++ [Char]
") (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Pred era
x forall a. [a] -> [a] -> [a]
++ [Char]
") (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Pred era
y forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Before Term era a
x Term era b
y) = [Char]
"Before " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era a
x forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era b
y
  show (ListWhere Term era Size
sz Term era [t]
t RootTarget era t t
tar [Pred era]
ps) =
    [Char]
"(ListWhere " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era Size
sz forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era [t]
t forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show RootTarget era t t
tar forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL forall a. Show a => a -> [Char]
show [Char]
", " [Pred era]
ps forall a. [a] -> [a] -> [a]
++ [Char]
")"
  showList :: [Pred era] -> ShowS
showList [Pred era]
xs [Char]
ans = [[Char]] -> [Char]
unlines ([Char]
ans forall a. a -> [a] -> [a]
: (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> [Char]
show [Pred era]
xs))

showAllTarget :: RootTarget era r t -> [Char]
showAllTarget :: forall era r t. RootTarget era r t -> [Char]
showAllTarget RootTarget era r t
tar = [Char]
"   forall " forall a. [a] -> [a] -> [a]
++ forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL forall a. Show a => a -> [Char]
show [Char]
" " (forall a. HashSet a -> [a]
HashSet.toList (forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget forall a. HashSet a
HashSet.empty RootTarget era r t
tar)) forall a. [a] -> [a] -> [a]
++ [Char]
". "

instance Show (RootTarget era r t) where
  show :: RootTarget era r t -> [Char]
show (Constr [Char]
nm a -> b
_f) = [Char]
nm
  show (Simple Term era t
x) = forall a. Show a => a -> [Char]
show Term era t
x
  show (Lensed Term era t
x SimpleGetter r t
_) = forall a. Show a => a -> [Char]
show Term era t
x
  show (Partial Term era t
x r -> Maybe t
_) = forall a. Show a => a -> [Char]
show Term era t
x
  show (RootTarget era r (a -> t)
f :$ RootTarget era r a
x) = [Char]
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show RootTarget era r (a -> t)
f forall a. [a] -> [a] -> [a]
++ [Char]
" :$ " forall a. [a] -> [a] -> [a]
++ forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL Any (RootTarget era r) -> [Char]
pp [Char]
" :$ " (forall era r t. RootTarget era r t -> [Any (RootTarget era r)]
args RootTarget era r a
x) forall a. [a] -> [a] -> [a]
++ [Char]
")"
    where
      pp :: Univ.Any (RootTarget era r) -> String
      pp :: Any (RootTarget era r) -> [Char]
pp (Univ.Any RootTarget era r i
spec) = forall a. Show a => a -> [Char]
show RootTarget era r i
spec
  show (Invert [Char]
nm TypeRep r
_ a -> b
_) = [Char]
nm
  show (Shift RootTarget era root2 t
x Lens' r root2
_) = [Char]
"(Shift " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show RootTarget era root2 t
x forall a. [a] -> [a] -> [a]
++ [Char]
" lens)"
  show (Mask RootTarget era r t
x) = forall a. Show a => a -> [Char]
show RootTarget era r t
x
  show (Virtual Term era t
x PDoc
y Lens' r t
_) = [Char]
"(Virtual " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era t
x forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show PDoc
y forall a. [a] -> [a] -> [a]
++ [Char]
")"

-- | "Print a Target as nested applications"
showT :: forall era t r. RootTarget era r t -> String
showT :: forall era t r. RootTarget era r t -> [Char]
showT (Constr [Char]
nm a -> b
_f) = [Char]
nm
showT (Simple Term era t
x) = forall a. Show a => a -> [Char]
show Term era t
x
showT (Lensed Term era t
x SimpleGetter r t
_) = forall a. Show a => a -> [Char]
show Term era t
x
showT (Partial Term era t
x r -> Maybe t
_) = forall a. Show a => a -> [Char]
show Term era t
x
showT (RootTarget era r (a -> t)
f :$ RootTarget era r a
x) = [Char]
"(" forall a. [a] -> [a] -> [a]
++ forall era t r. RootTarget era r t -> [Char]
showT RootTarget era r (a -> t)
f forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL Any (RootTarget era r) -> [Char]
pp [Char]
" " (forall era r t. RootTarget era r t -> [Any (RootTarget era r)]
args RootTarget era r a
x) forall a. [a] -> [a] -> [a]
++ [Char]
")"
  where
    pp :: Univ.Any (RootTarget era r) -> String
    pp :: Any (RootTarget era r) -> [Char]
pp (Univ.Any RootTarget era r i
spec) = forall era t r. RootTarget era r t -> [Char]
showT RootTarget era r i
spec
showT (Invert [Char]
nm TypeRep r
_ a -> b
_) = [Char]
nm
showT (Shift RootTarget era root2 t
x Lens' r root2
_) = [Char]
"(Shift " forall a. [a] -> [a] -> [a]
++ forall era t r. RootTarget era r t -> [Char]
showT RootTarget era root2 t
x forall a. [a] -> [a] -> [a]
++ [Char]
")"
showT (Mask RootTarget era r t
x) = forall era t r. RootTarget era r t -> [Char]
showT RootTarget era r t
x
showT (Virtual Term era t
_ PDoc
y Lens' r t
_) = forall a. Show a => a -> [Char]
show PDoc
y

args :: RootTarget era r t -> [Univ.Any (RootTarget era r)]
args :: forall era r t. RootTarget era r t -> [Any (RootTarget era r)]
args (RootTarget era r (a -> t)
x :$ RootTarget era r a
xs) = forall {k} (t :: k -> *) (i :: k). t i -> Any t
Univ.Any RootTarget era r (a -> t)
x forall a. a -> [a] -> [a]
: forall era r t. RootTarget era r t -> [Any (RootTarget era r)]
args RootTarget era r a
xs
args RootTarget era r t
other = [forall {k} (t :: k -> *) (i :: k). t i -> Any t
Univ.Any RootTarget era r t
other]

-- | Print a Target as a record showing the struture and names of all
--   the variables involved. This documents what is in scope where
--   the Target value was defined.
ppTarget :: RootTarget era r t -> PDoc
ppTarget :: forall era r t. RootTarget era r t -> PDoc
ppTarget RootTarget era r t
x = forall era r t. RootTarget era r t -> [(Text, PDoc)] -> PDoc
targetRecord RootTarget era r t
x []

targetRecord :: RootTarget era r t -> [(Text, PDoc)] -> PDoc
targetRecord :: forall era r t. RootTarget era r t -> [(Text, PDoc)] -> PDoc
targetRecord (Constr [Char]
n a -> b
_) [(Text, PDoc)]
xs = Text -> [(Text, PDoc)] -> PDoc
ppRecord ([Char] -> Text
pack [Char]
n) [(Text, PDoc)]
xs
targetRecord (RootTarget era r (a -> t)
ts :$ RootTarget era r a
t) [(Text, PDoc)]
xs = forall era r t. RootTarget era r t -> [(Text, PDoc)] -> PDoc
targetRecord RootTarget era r (a -> t)
ts (forall era r t. RootTarget era r t -> (Text, PDoc)
targetPair RootTarget era r a
t forall a. a -> [a] -> [a]
: [(Text, PDoc)]
xs)
targetRecord (Simple Term era t
e) [] = forall a. [Char] -> Doc a
ppString (forall a. Show a => a -> [Char]
show Term era t
e)
targetRecord (Lensed Term era t
e SimpleGetter r t
_) [] = forall a. [Char] -> Doc a
ppString (forall a. Show a => a -> [Char]
show Term era t
e)
targetRecord (Partial Term era t
e r -> Maybe t
_) [] = forall a. [Char] -> Doc a
ppString (forall a. Show a => a -> [Char]
show Term era t
e)
targetRecord (Invert [Char]
n TypeRep r
_ a -> b
_) [(Text, PDoc)]
xs = Text -> [(Text, PDoc)] -> PDoc
ppRecord ([Char] -> Text
pack [Char]
n) [(Text, PDoc)]
xs
targetRecord (Shift RootTarget era root2 t
x Lens' r root2
_) [(Text, PDoc)]
xs = forall era r t. RootTarget era r t -> [(Text, PDoc)] -> PDoc
targetRecord RootTarget era root2 t
x [(Text, PDoc)]
xs
targetRecord (Mask RootTarget era r t
x) [(Text, PDoc)]
xs = forall era r t. RootTarget era r t -> [(Text, PDoc)] -> PDoc
targetRecord RootTarget era r t
x [(Text, PDoc)]
xs
targetRecord (Virtual Term era t
_ PDoc
e Lens' r t
_) [] = PDoc
e
targetRecord RootTarget era r t
other [(Text, PDoc)]
xs = Text -> [(Text, PDoc)] -> PDoc
ppRecord (forall era r t. RootTarget era r t -> Text
nameOf RootTarget era r t
other) [(Text, PDoc)]
xs

nameOf :: RootTarget era r t -> Text
nameOf :: forall era r t. RootTarget era r t -> Text
nameOf (Constr [Char]
cs a -> b
_) = [Char] -> Text
pack (forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower [Char]
cs forall a. [a] -> [a] -> [a]
++ [Char]
"T")
nameOf (Simple (Var (V [Char]
n Rep era t
_ Access era s t
_))) = [Char] -> Text
pack [Char]
n
nameOf (Lensed (Var (V [Char]
n Rep era t
_ Access era s t
_)) SimpleGetter r t
_) = [Char] -> Text
pack [Char]
n
nameOf (Partial (Var (V [Char]
n Rep era t
_ Access era s t
_)) r -> Maybe t
_) = [Char] -> Text
pack [Char]
n
nameOf (Simple Term era t
term) = [Char] -> Text
pack (forall a. Show a => a -> [Char]
show Term era t
term)
nameOf (Lensed Term era t
term SimpleGetter r t
_) = [Char] -> Text
pack (forall a. Show a => a -> [Char]
show Term era t
term)
nameOf (Partial Term era t
term r -> Maybe t
_) = [Char] -> Text
pack (forall a. Show a => a -> [Char]
show Term era t
term)
nameOf (RootTarget era r (a -> t)
x :$ RootTarget era r a
_) = forall era r t. RootTarget era r t -> Text
nameOf RootTarget era r (a -> t)
x
nameOf (Invert [Char]
cs TypeRep r
_ a -> b
_) = [Char] -> Text
pack (forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower [Char]
cs forall a. [a] -> [a] -> [a]
++ [Char]
"T")
nameOf (Shift RootTarget era root2 t
x Lens' r root2
_) = forall era r t. RootTarget era r t -> Text
nameOf RootTarget era root2 t
x
nameOf (Mask RootTarget era r t
x) = forall era r t. RootTarget era r t -> Text
nameOf RootTarget era r t
x
nameOf (Virtual Term era t
_ PDoc
x Lens' r t
_) = [Char] -> Text
pack (forall a. Show a => a -> [Char]
show PDoc
x)

targetPair :: RootTarget era r t -> (Text, PDoc)
targetPair :: forall era r t. RootTarget era r t -> (Text, PDoc)
targetPair (Simple (Var (V [Char]
n Rep era t
rep Access era s t
_))) = ([Char] -> Text
pack [Char]
n, forall a. [Char] -> Doc a
ppString (forall a. Show a => a -> [Char]
show Rep era t
rep))
targetPair (Lensed (Var (V [Char]
n Rep era t
rep Access era s t
_)) SimpleGetter r t
_) = ([Char] -> Text
pack [Char]
n, forall a. [Char] -> Doc a
ppString (forall a. Show a => a -> [Char]
show Rep era t
rep))
targetPair (Partial (Var (V [Char]
n Rep era t
rep Access era s t
_)) r -> Maybe t
_) = ([Char] -> Text
pack [Char]
n, forall a. [Char] -> Doc a
ppString (forall a. Show a => a -> [Char]
show Rep era t
rep))
targetPair (Virtual (Var (V [Char]
_ Rep era t
rep Access era s t
_)) PDoc
newname Lens' r t
_) = ([Char] -> Text
pack (forall a. Show a => a -> [Char]
show PDoc
newname), forall a. [Char] -> Doc a
ppString (forall a. Show a => a -> [Char]
show Rep era t
rep))
targetPair RootTarget era r t
x = (forall era r t. RootTarget era r t -> Text
nameOf RootTarget era r t
x, forall era r t. RootTarget era r t -> [(Text, PDoc)] -> PDoc
targetRecord RootTarget era r t
x [])

-- ===================================================
-- Computing the variables (V era t) in a Term, Pred, RootTarget
-- Their are no binders in any of these, so this is not so difficult
-- But (V era t) may have different 't', so we hide 't' in 'Name'

varsOfTerm :: HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm :: forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era t
s = case Term era t
s of
  Lit Rep era t
_ t
_ -> HashSet (Name era)
ans
  Var v :: V era t
v@(V [Char]
_ Rep era t
_ Access era s t
_) -> forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert (forall era s. V era s -> Name era
Name V era t
v) HashSet (Name era)
ans
  Dom Term era (Map a b)
x -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era (Map a b)
x
  Rng Term era (Map a b)
x -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era (Map a b)
x
  Elems Term era (Map a b)
x -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era (Map a b)
x
  (ProjM Lens' b t
_ Rep era t
_ Term era (Map a b)
x) -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era (Map a b)
x
  (ProjS Lens' b t
_ Rep era t
_ Term era (Set b)
x) -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era (Set b)
x
  (Proj Lens' b t
_ Rep era t
_ Term era b
x) -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era b
x
  Delta Term era Coin
x -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era Coin
x
  Negate Term era DeltaCoin
x -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era DeltaCoin
x
  Restrict Term era (Set a)
st Term era (Map a b)
mp -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era (Set a)
st) Term era (Map a b)
mp
  HashS Term era (ScriptF era)
st -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era (ScriptF era)
st
  HashD Term era (Data era)
st -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era (Data era)
st
  Pair Term era a
a Term era b
b -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era a
a) Term era b
b

vars :: Term era t -> HashSet (Name era)
vars :: forall era t. Term era t -> HashSet (Name era)
vars Term era t
x = forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm forall a. HashSet a
HashSet.empty Term era t
x

varsOfTarget :: HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget :: forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget HashSet (Name era)
ans RootTarget era r t
s = case RootTarget era r t
s of
  (RootTarget era r (a -> t)
a :$ RootTarget era r a
b) -> forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget (forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget HashSet (Name era)
ans RootTarget era r (a -> t)
a) RootTarget era r a
b
  (Simple Term era t
x) -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era t
x
  (Lensed Term era t
x SimpleGetter r t
_) -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era t
x
  (Partial Term era t
x r -> Maybe t
_) -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era t
x
  (Constr [Char]
_ a -> b
_) -> HashSet (Name era)
ans
  (Invert [Char]
_ TypeRep r
_ a -> b
_) -> HashSet (Name era)
ans
  (Shift RootTarget era root2 t
x Lens' r root2
_) -> forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget HashSet (Name era)
ans RootTarget era root2 t
x
  (Mask RootTarget era r t
x) -> forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget HashSet (Name era)
ans RootTarget era r t
x
  (Virtual Term era t
x PDoc
_ Lens' r t
_) -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era t
x

varsOfPred :: forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred :: forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred HashSet (Name era)
ans Pred era
s = case Pred era
s of
  MetaSize Size
_ Term era Size
term -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era Size
term
  Sized Term era Size
a Term era t
b -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era Size
a) Term era t
b
  Term era a
a :=: Term era a
b -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era a
a) Term era a
b
  Subset Term era (Set a)
a Term era (Set a)
b -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era (Set a)
a) Term era (Set a)
b
  Disjoint Term era (Set a)
a Term era (Set a)
b -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era (Set a)
a) Term era (Set a)
b
  SumsTo Direct c
_ Term era c
x OrdCond
_ [Sum era c]
xs -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era r. HashSet (Name era) -> Sum era r -> HashSet (Name era)
varsOfSum (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era c
x) [Sum era c]
xs
  SumSplit c
_ Term era c
x OrdCond
_ [Sum era c]
xs -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era r. HashSet (Name era) -> Sum era r -> HashSet (Name era)
varsOfSum (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era c
x) [Sum era c]
xs
  Random Term era t
x -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era t
x
  Component Direct (Term era t)
t [AnyF era t]
cs -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall z. HashSet (Name era) -> AnyF era z -> HashSet (Name era)
varsOfComponent HashSet (Name era)
ans [AnyF era t]
cs) (forall a. Direct a -> a
direct Direct (Term era t)
t)
    where
      varsOfComponent :: forall z. HashSet (Name era) -> AnyF era z -> HashSet (Name era)
      varsOfComponent :: forall z. HashSet (Name era) -> AnyF era z -> HashSet (Name era)
varsOfComponent HashSet (Name era)
l (AnyF (Field [Char]
n Rep era t
r Rep era z
rx Lens' z t
l2)) = forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert (forall era s. V era s -> Name era
Name forall a b. (a -> b) -> a -> b
$ forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
n Rep era t
r (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era z
rx Lens' z t
l2)) HashSet (Name era)
l
      varsOfComponent HashSet (Name era)
l (AnyF (FConst Rep era t
_ t
_ Rep era z
_ Lens' z t
_)) = HashSet (Name era)
l
  CanFollow Term era n
a Term era n
b -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era n
a) Term era n
b
  Member Direct (Term era a)
a Term era (Set a)
b -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans (forall a. Direct a -> a
direct Direct (Term era a)
a)) Term era (Set a)
b
  NotMember Term era a
a Term era (Set a)
b -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era a
a) Term era (Set a)
b
  MapMember Term era k
k Term era v
v Direct (Term era (Map k v))
m -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era k
k) Term era v
v) (forall a. Direct a -> a
direct Direct (Term era (Map k v))
m)
  Term era t
a :<-: RootTarget era r t
b -> forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era t
a) RootTarget era r t
b
  GenFrom Term era t
a RootTarget era r (Gen t)
b -> forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era t
a) RootTarget era r (Gen t)
b
  List Term era fs
a [Term era t]
bs -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era fs
a) [Term era t]
bs
  Choose Term era Size
sz Term era [t]
term [(Int, Target era t, [Pred era])]
pairs -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era r t2.
Era era =>
HashSet (Name era)
-> [(Int, RootTarget era r t2, [Pred era])] -> HashSet (Name era)
varsOfTrips HashSet (Name era)
ans [(Int, Target era t, [Pred era])]
pairs) Term era [t]
term) Term era Size
sz
  Oneof Term era t
term [(Int, RootTarget era t t, [Pred era])]
pairs -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era r t2.
Era era =>
HashSet (Name era)
-> [(Int, RootTarget era r t2, [Pred era])] -> HashSet (Name era)
varsOfTrips HashSet (Name era)
ans [(Int, RootTarget era t t, [Pred era])]
pairs) Term era t
term
  ForEach Term era Size
sz Term era fs
term Pat era t
pat [Pred era]
ps -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t2.
Era era =>
HashSet (Name era)
-> [(Pat era t2, [Pred era])] -> HashSet (Name era)
varsOfPats HashSet (Name era)
ans [(Pat era t
pat, [Pred era]
ps)]) Term era fs
term) Term era Size
sz
  Maybe Term era (Maybe t)
term RootTarget era r t
target [Pred era]
ps -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era r t2.
Era era =>
HashSet (Name era)
-> [(RootTarget era r t2, [Pred era])] -> HashSet (Name era)
varsOfPairs HashSet (Name era)
ans [(RootTarget era r t
target, [Pred era]
ps)]) Term era (Maybe t)
term
  SubMap Term era (Map k v)
a Term era (Map k v)
b -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era (Map k v)
a) Term era (Map k v)
b
  If RootTarget era r Bool
t Pred era
x Pred era
y -> forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget (forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred (forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred HashSet (Name era)
ans Pred era
x) Pred era
y) RootTarget era r Bool
t
  Before Term era a
a Term era b
b -> forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era a
a) Term era b
b
  ListWhere Term era Size
sz Term era [t]
t RootTarget era t t
tar [Pred era]
ps -> forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.union HashSet (Name era)
vs HashSet (Name era)
others
    where
      vs :: HashSet (Name era)
vs = forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era [t]
t) Term era Size
sz
      bound :: HashSet (Name era)
bound = forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget forall a. HashSet a
HashSet.empty RootTarget era t t
tar
      pvs :: HashSet (Name era)
pvs = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred forall a. HashSet a
HashSet.empty [Pred era]
ps
      others :: HashSet (Name era)
others = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.difference HashSet (Name era)
pvs HashSet (Name era)
bound

varsOfTrips ::
  Era era => HashSet (Name era) -> [(Int, RootTarget era r t2, [Pred era])] -> HashSet (Name era)
varsOfTrips :: forall era r t2.
Era era =>
HashSet (Name era)
-> [(Int, RootTarget era r t2, [Pred era])] -> HashSet (Name era)
varsOfTrips HashSet (Name era)
ans1 [] = HashSet (Name era)
ans1
varsOfTrips HashSet (Name era)
ans1 ((Int
_, RootTarget era r t2
t, [Pred era]
ps) : [(Int, RootTarget era r t2, [Pred era])]
more) = forall era r t2.
Era era =>
HashSet (Name era)
-> [(Int, RootTarget era r t2, [Pred era])] -> HashSet (Name era)
varsOfTrips (forall {era} {t :: * -> *} {r} {t}.
(Era era, Foldable t) =>
HashSet (Name era)
-> RootTarget era r t -> t (Pred era) -> HashSet (Name era)
act HashSet (Name era)
ans1 RootTarget era r t2
t [Pred era]
ps) [(Int, RootTarget era r t2, [Pred era])]
more
  where
    act :: HashSet (Name era)
-> RootTarget era r t -> t (Pred era) -> HashSet (Name era)
act HashSet (Name era)
ans2 RootTarget era r t
tar t (Pred era)
preds =
      forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.union
        ( forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.difference
            (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred forall a. HashSet a
HashSet.empty t (Pred era)
preds)
            (forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget forall a. HashSet a
HashSet.empty RootTarget era r t
tar)
        )
        HashSet (Name era)
ans2

varsOfPairs ::
  Era era => HashSet (Name era) -> [(RootTarget era r t2, [Pred era])] -> HashSet (Name era)
varsOfPairs :: forall era r t2.
Era era =>
HashSet (Name era)
-> [(RootTarget era r t2, [Pred era])] -> HashSet (Name era)
varsOfPairs HashSet (Name era)
ans1 [] = HashSet (Name era)
ans1
varsOfPairs HashSet (Name era)
ans1 ((RootTarget era r t2
t, [Pred era]
ps) : [(RootTarget era r t2, [Pred era])]
more) = forall era r t2.
Era era =>
HashSet (Name era)
-> [(RootTarget era r t2, [Pred era])] -> HashSet (Name era)
varsOfPairs (forall {era} {t :: * -> *} {r} {t}.
(Era era, Foldable t) =>
HashSet (Name era)
-> RootTarget era r t -> t (Pred era) -> HashSet (Name era)
act HashSet (Name era)
ans1 RootTarget era r t2
t [Pred era]
ps) [(RootTarget era r t2, [Pred era])]
more
  where
    act :: HashSet (Name era)
-> RootTarget era r t -> t (Pred era) -> HashSet (Name era)
act HashSet (Name era)
ans2 RootTarget era r t
tar t (Pred era)
preds =
      forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.union
        ( forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.difference
            (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred forall a. HashSet a
HashSet.empty t (Pred era)
preds)
            (forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget forall a. HashSet a
HashSet.empty RootTarget era r t
tar)
        )
        HashSet (Name era)
ans2

varsOfPats :: Era era => HashSet (Name era) -> [(Pat era t2, [Pred era])] -> HashSet (Name era)
varsOfPats :: forall era t2.
Era era =>
HashSet (Name era)
-> [(Pat era t2, [Pred era])] -> HashSet (Name era)
varsOfPats HashSet (Name era)
ans1 [] = HashSet (Name era)
ans1
varsOfPats HashSet (Name era)
ans1 ((Pat era t2
pat0, [Pred era]
ps) : [(Pat era t2, [Pred era])]
more) = forall era t2.
Era era =>
HashSet (Name era)
-> [(Pat era t2, [Pred era])] -> HashSet (Name era)
varsOfPats (forall {era} {t :: * -> *} {t}.
(Era era, Foldable t) =>
HashSet (Name era)
-> Pat era t -> t (Pred era) -> HashSet (Name era)
act HashSet (Name era)
ans1 Pat era t2
pat0 [Pred era]
ps) [(Pat era t2, [Pred era])]
more
  where
    act :: HashSet (Name era)
-> Pat era t -> t (Pred era) -> HashSet (Name era)
act HashSet (Name era)
ans2 Pat era t
pat t (Pred era)
preds =
      forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.union
        ( forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.difference
            (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred forall a. HashSet a
HashSet.empty t (Pred era)
preds)
            (forall era t. HashSet (Name era) -> Pat era t -> HashSet (Name era)
varsOfPat forall a. HashSet a
HashSet.empty Pat era t
pat)
        )
        HashSet (Name era)
ans2

varsOfSum :: HashSet (Name era) -> Sum era r -> HashSet (Name era)
varsOfSum :: forall era r. HashSet (Name era) -> Sum era r -> HashSet (Name era)
varsOfSum HashSet (Name era)
ans (SumMap Term era (Map a r)
y) = forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era (Map a r)
y
varsOfSum HashSet (Name era)
ans (SumList Term era [r]
y) = forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era [r]
y
varsOfSum HashSet (Name era)
ans (One Term era r
y) = forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era r
y
varsOfSum HashSet (Name era)
ans (ProjOne Lens' x r
_ Rep era r
_ Term era x
y) = forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era x
y
varsOfSum HashSet (Name era)
ans (ProjMap Rep era r
_ Lens' x r
_ Term era (Map a x)
x) = forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans Term era (Map a x)
x

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

expandSum :: Sum era c -> [Int] -> [Sum era c]
expandSum :: forall era c. Sum era c -> [Int] -> [Sum era c]
expandSum (One (Var (V [Char]
n Rep era c
r Access era s c
a))) [Int]
ns = forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> forall era c. Term era c -> Sum era c
One (forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V ([Char]
n forall a. [a] -> [a] -> [a]
++ [Char]
"." forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i) Rep era c
r Access era s c
a))) [Int]
ns
expandSum (ProjOne Lens' x c
l Rep era c
rep (Var (V [Char]
n Rep era x
r Access era s x
a))) [Int]
ns = forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> forall s c era. Lens' s c -> Rep era c -> Term era s -> Sum era c
ProjOne Lens' x c
l Rep era c
rep (forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V ([Char]
n forall a. [a] -> [a] -> [a]
++ [Char]
"." forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i) Rep era x
r Access era s x
a))) [Int]
ns
expandSum Sum era c
x [Int]
_ = forall a. HasCallStack => [Char] -> a
error ([Char]
"Bad Sum in expandSum: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Sum era c
x)

-- =====================================================================
-- Subst, the type of Substitutions

pad :: Int -> String -> String
pad :: Int -> ShowS
pad Int
n [Char]
x = [Char]
x forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate (Int
n forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
x) Char
' '

data SubstElem era where
  SubstElem :: Rep era t -> Term era t -> Access era s t -> SubstElem era

instance Show (SubstElem era) where
  show :: SubstElem era -> [Char]
show (SubstElem Rep era t
rep Term era t
t Access era s t
_) = forall a. Show a => a -> [Char]
show Term era t
t forall a. [a] -> [a] -> [a]
++ [Char]
" :: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Rep era t
rep

newtype Subst era = Subst (Map String (SubstElem era))

extend :: V era t -> Term era t -> Subst era -> Subst era
extend :: forall era t. V era t -> Term era t -> Subst era -> Subst era
extend (V [Char]
nm Rep era t
rep Access era s t
access) Term era t
term (Subst Map [Char] (SubstElem era)
m) = forall era. Map [Char] (SubstElem era) -> Subst era
Subst (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert [Char]
nm (forall era s b.
Rep era s -> Term era s -> Access era b s -> SubstElem era
SubstElem Rep era t
rep Term era t
term Access era s t
access) Map [Char] (SubstElem era)
m)

instance Show (Subst era) where
  show :: Subst era -> [Char]
show (Subst Map [Char] (SubstElem era)
m) = [[Char]] -> [Char]
unlines (forall a b. (a -> b) -> [a] -> [b]
map forall {era}. ([Char], SubstElem era) -> [Char]
f (forall k a. Map k a -> [(k, a)]
Map.toList Map [Char] (SubstElem era)
m))
    where
      f :: ([Char], SubstElem era) -> [Char]
f ([Char]
nm, SubstElem Rep era t
_ Term era t
t Access era s t
_) = [Char]
nm forall a. [a] -> [a] -> [a]
++ [Char]
" -> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era t
t

emptySubst :: Subst era
emptySubst :: forall era. Subst era
emptySubst = forall era. Map [Char] (SubstElem era) -> Subst era
Subst forall k a. Map k a
Map.empty

substToEnv :: Subst era -> Env era -> Typed (Env era)
substToEnv :: forall era. Subst era -> Env era -> Typed (Env era)
substToEnv (Subst Map [Char] (SubstElem era)
m) Env era
env = forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' forall {era}.
Typed (Env era) -> [Char] -> SubstElem era -> Typed (Env era)
accum (forall (f :: * -> *) a. Applicative f => a -> f a
pure Env era
env) Map [Char] (SubstElem era)
m
  where
    accum :: Typed (Env era) -> [Char] -> SubstElem era -> Typed (Env era)
accum Typed (Env era)
ansM [Char]
key (SubstElem Rep era t
r (Lit Rep era t
_ t
v) Access era s t
access) = do
      Env Map [Char] (Payload era)
ans <- Typed (Env era)
ansM
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era. Map [Char] (Payload era) -> Env era
Env forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert [Char]
key (forall era s b. Rep era s -> s -> Access era b s -> Payload era
Payload Rep era t
r t
v Access era s t
access) Map [Char] (Payload era)
ans
    accum Typed (Env era)
_ [Char]
_ (SubstElem Rep era t
_ Term era t
e Access era s t
_) = forall a. [[Char]] -> Typed a
failT [[Char]
"Not Literal expr in substToEnv: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era t
e]

envToSubst :: Env era -> Subst era
envToSubst :: forall era. Env era -> Subst era
envToSubst (Env Map [Char] (Payload era)
env) = forall era. Map [Char] (SubstElem era) -> Subst era
Subst (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall {era}. Payload era -> SubstElem era
f Map [Char] (Payload era)
env)
  where
    f :: Payload era -> SubstElem era
f (Payload Rep era t
rep t
t Access era s t
access) = forall era s b.
Rep era s -> Term era s -> Access era b s -> SubstElem era
SubstElem Rep era t
rep (forall era t. Rep era t -> t -> Term era t
Lit Rep era t
rep t
t) Access era s t
access

findV :: Subst era -> V era t -> Term era t
findV :: forall era t. Subst era -> V era t -> Term era t
findV (Subst Map [Char] (SubstElem era)
m) v :: V era t
v@(V [Char]
n1 Rep era t
rep1 Access era s t
_) = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup [Char]
n1 Map [Char] (SubstElem era)
m of
  Maybe (SubstElem era)
Nothing -> forall era t. V era t -> Term era t
Var V era t
v -- If its not in the Subst, return the Var
  Just (SubstElem Rep era t
rep2 Term era t
term Access era s t
_) -> case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql Rep era t
rep1 Rep era t
rep2 of
    Just t :~: t
Refl -> Term era t
term
    Maybe (t :~: t)
Nothing ->
      forall a. HasCallStack => [Char] -> a
error
        ( [Char]
"In findV, we found: "
            forall a. [a] -> [a] -> [a]
++ [Char]
n1
            forall a. [a] -> [a] -> [a]
++ [Char]
", but the types did not match. "
            forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Rep era t
rep1
            forall a. [a] -> [a] -> [a]
++ [Char]
" =/= "
            forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Rep era t
rep2
        )

--  | Not really a composition, just adding 'sub1' to 'sub2', but if any thing
--    is in both 'sub1' and 'sub2', the 'sub1' binding overrides the 'sub2' binding
composeSubst :: Subst era -> Subst era -> Subst era
composeSubst :: forall era. Subst era -> Subst era -> Subst era
composeSubst (Subst Map [Char] (SubstElem era)
sub1) (Subst Map [Char] (SubstElem era)
sub2) = forall era. Map [Char] (SubstElem era) -> Subst era
Subst (forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey' forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Map [Char] (SubstElem era)
sub2 Map [Char] (SubstElem era)
sub1)

singleSubst :: V era t -> Term era t -> Subst era
singleSubst :: forall era t. V era t -> Term era t -> Subst era
singleSubst (V [Char]
n Rep era t
r Access era s t
access) Term era t
expr = forall era. Map [Char] (SubstElem era) -> Subst era
Subst (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert [Char]
n (forall era s b.
Rep era s -> Term era s -> Access era b s -> SubstElem era
SubstElem Rep era t
r Term era t
expr Access era s t
access) forall k a. Map k a
Map.empty)

substFromNames :: forall era. HashSet (Name era) -> Subst era
substFromNames :: forall era. HashSet (Name era) -> Subst era
substFromNames HashSet (Name era)
names = forall era. Map [Char] (SubstElem era) -> Subst era
Subst (forall a b. (a -> b -> a) -> a -> HashSet b -> a
HashSet.foldl' Map [Char] (SubstElem era)
-> Name era -> Map [Char] (SubstElem era)
accum forall k a. Map k a
Map.empty HashSet (Name era)
names)
  where
    accum :: Map String (SubstElem era) -> Name era -> Map String (SubstElem era)
    accum :: Map [Char] (SubstElem era)
-> Name era -> Map [Char] (SubstElem era)
accum Map [Char] (SubstElem era)
ans (Name v :: V era t
v@(V [Char]
n Rep era t
r Access era s t
access)) = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert [Char]
n (forall era s b.
Rep era s -> Term era s -> Access era b s -> SubstElem era
SubstElem Rep era t
r (forall era t. V era t -> Term era t
Var V era t
v) Access era s t
access) Map [Char] (SubstElem era)
ans

data SubItem era where
  SubItem :: V era t -> Term era t -> SubItem era

instance Show (SubItem era) where
  show :: SubItem era -> [Char]
show (SubItem V era t
x Term era t
y) = [Char]
"(SubItem " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show V era t
x forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era t
y forall a. [a] -> [a] -> [a]
++ [Char]
")"

itemsToSubst :: [SubItem era] -> Subst era
itemsToSubst :: forall era. [SubItem era] -> Subst era
itemsToSubst [SubItem era]
ss = forall era. Map [Char] (SubstElem era) -> Subst era
Subst (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
List.foldr forall era.
SubItem era
-> Map [Char] (SubstElem era) -> Map [Char] (SubstElem era)
accum forall k a. Map k a
Map.empty [SubItem era]
ss)
  where
    accum :: SubItem era -> Map String (SubstElem era) -> Map String (SubstElem era)
    accum :: forall era.
SubItem era
-> Map [Char] (SubstElem era) -> Map [Char] (SubstElem era)
accum (SubItem (V [Char]
nm Rep era t
rep Access era s t
access) Term era t
term) !Map [Char] (SubstElem era)
ans = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert [Char]
nm (forall era s b.
Rep era s -> Term era s -> Access era b s -> SubstElem era
SubstElem Rep era t
rep Term era t
term Access era s t
access) Map [Char] (SubstElem era)
ans

-- =====================================================
-- Subtitution of (V era t) inside of (Spec era t)

substTerm :: Subst era -> Term era t -> Term era t
substTerm :: forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub (Var V era t
v) = forall era t. Subst era -> V era t -> Term era t
findV Subst era
sub V era t
v
substTerm Subst era
_ (Lit Rep era t
r t
k) = forall era t. Rep era t -> t -> Term era t
Lit Rep era t
r t
k
substTerm Subst era
sub (Dom Term era (Map a b)
x) = forall s era b. Ord s => Term era (Map s b) -> Term era (Set s)
Dom (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Map a b)
x)
substTerm Subst era
sub (Rng Term era (Map a b)
x) = forall s b era.
(Ord s, Ord b) =>
Term era (Map s b) -> Term era (Set b)
Rng (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Map a b)
x)
substTerm Subst era
sub (Elems Term era (Map a b)
x) = forall s b era. (Ord s, Eq b) => Term era (Map s b) -> Term era [b]
Elems (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Map a b)
x)
substTerm Subst era
sub (ProjM Lens' b t
l Rep era t
r Term era (Map a b)
x) = forall s b t era.
Ord s =>
Lens' b t -> Rep era t -> Term era (Map s b) -> Term era (Map s t)
ProjM Lens' b t
l Rep era t
r (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Map a b)
x)
substTerm Subst era
sub (ProjS Lens' b t
l Rep era t
r Term era (Set b)
x) = forall s b era.
(Ord s, Ord b) =>
Lens' s b -> Rep era b -> Term era (Set s) -> Term era (Set b)
ProjS Lens' b t
l Rep era t
r (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Set b)
x)
substTerm Subst era
sub (Proj Lens' b t
l Rep era t
r Term era b
x) = forall s t era. Lens' s t -> Rep era t -> Term era s -> Term era t
Proj Lens' b t
l Rep era t
r (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era b
x)
substTerm Subst era
sub (Delta Term era Coin
x) = forall era. Term era Coin -> Term era DeltaCoin
Delta (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era Coin
x)
substTerm Subst era
sub (Negate Term era DeltaCoin
x) = forall era. Term era DeltaCoin -> Term era DeltaCoin
Negate (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era DeltaCoin
x)
substTerm Subst era
sub (Restrict Term era (Set a)
s Term era (Map a b)
m) = forall s era b.
Ord s =>
Term era (Set s) -> Term era (Map s b) -> Term era (Map s b)
Restrict (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Set a)
s) (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Map a b)
m)
substTerm Subst era
sub (HashS Term era (ScriptF era)
s) = forall era.
Reflect era =>
Term era (ScriptF era) -> Term era (ScriptHash (EraCrypto era))
HashS (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (ScriptF era)
s)
substTerm Subst era
sub (HashD Term era (Data era)
s) = forall era.
Era era =>
Term era (Data era) -> Term era (DataHash (EraCrypto era))
HashD (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Data era)
s)
substTerm Subst era
sub (Pair Term era a
a Term era b
b) = forall era s b. Term era s -> Term era b -> Term era (s, b)
Pair (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era a
a) (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era b
b)

substPred :: Subst era -> Pred era -> Pred era
substPred :: forall era. Subst era -> Pred era -> Pred era
substPred Subst era
sub (MetaSize Size
a Term era Size
b) = forall era. Size -> Term era Size -> Pred era
MetaSize Size
a (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era Size
b)
substPred Subst era
sub (Sized Term era Size
a Term era t
b) = forall s era. Sizeable s => Term era Size -> Term era s -> Pred era
Sized (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era Size
a) (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
b)
substPred Subst era
sub (Term era a
a :=: Term era a
b) = forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era a
a forall s era. Eq s => Term era s -> Term era s -> Pred era
:=: forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era a
b
substPred Subst era
sub (Term era (Set a)
a `Subset` Term era (Set a)
b) = forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Set a)
a forall s era.
Ord s =>
Term era (Set s) -> Term era (Set s) -> Pred era
`Subset` forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Set a)
b
substPred Subst era
sub (Disjoint Term era (Set a)
a Term era (Set a)
b) = forall s era.
Ord s =>
Term era (Set s) -> Term era (Set s) -> Pred era
Disjoint (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Set a)
a) (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Set a)
b)
substPred Subst era
sub (SumsTo Direct c
i Term era c
a OrdCond
cond [Sum era c]
b) = forall era s.
(Era era, Adds s) =>
Direct s -> Term era s -> OrdCond -> [Sum era s] -> Pred era
SumsTo Direct c
i (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era c
a) OrdCond
cond (forall a b. (a -> b) -> [a] -> [b]
map (forall era t. Subst era -> Sum era t -> Sum era t
substSum Subst era
sub) [Sum era c]
b)
substPred Subst era
sub (SumSplit c
i Term era c
a OrdCond
cond [Sum era c]
b) = forall era s.
(Era era, Adds s) =>
s -> Term era s -> OrdCond -> [Sum era s] -> Pred era
SumSplit c
i (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era c
a) OrdCond
cond (forall a b. (a -> b) -> [a] -> [b]
map (forall era t. Subst era -> Sum era t -> Sum era t
substSum Subst era
sub) [Sum era c]
b)
substPred Subst era
sub (Random Term era t
x) = forall era s. Term era s -> Pred era
Random (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
x)
substPred Subst era
sub (Component Direct (Term era t)
t [AnyF era t]
cs) = case Direct (Term era t)
t of
  Left Term era t
x -> forall era s. Direct (Term era s) -> [AnyF era s] -> Pred era
Component (forall a b. a -> Either a b
Left (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
x)) (AnyF era t -> AnyF era t
substComp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [AnyF era t]
cs)
  Right Term era t
x -> forall era s. Direct (Term era s) -> [AnyF era s] -> Pred era
Component (forall a b. b -> Either a b
Right (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
x)) (AnyF era t -> AnyF era t
substComp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [AnyF era t]
cs)
  where
    substComp :: AnyF era t -> AnyF era t
substComp (AnyF w :: Field era t t
w@(Field [Char]
n Rep era t
r Rep era t
rx Lens' t t
l)) = forall era s s. Field era s s -> AnyF era s
AnyF forall a b. (a -> b) -> a -> b
$ case forall era t. Subst era -> V era t -> Term era t
findV Subst era
sub (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
n Rep era t
r (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era t
rx Lens' t t
l)) of
      (Lit Rep era t
rep t
x) -> forall era t s.
Rep era t -> t -> Rep era s -> Lens' s t -> Field era s t
FConst Rep era t
rep t
x Rep era t
rx Lens' t t
l
      (Var (V [Char]
n2 Rep era t
r2 Access era s t
_a2)) -> forall era t s.
Era era =>
[Char] -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field [Char]
n2 Rep era t
r2 Rep era t
rx Lens' t t
l
      Term era t
_ -> Field era t t
w
    substComp x :: AnyF era t
x@(AnyF (FConst Rep era t
_ t
_ Rep era t
_ Lens' t t
_)) = AnyF era t
x
substPred Subst era
sub (CanFollow Term era n
a Term era n
b) = forall s era. Count s => Term era s -> Term era s -> Pred era
CanFollow (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era n
a) (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era n
b)
substPred Subst era
sub (Member Direct (Term era a)
dirA Term era (Set a)
b) = case Direct (Term era a)
dirA of
  Left Term era a
a -> forall s era.
Ord s =>
Direct (Term era s) -> Term era (Set s) -> Pred era
Member (forall a b. a -> Either a b
Left (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era a
a)) (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Set a)
b)
  Right Term era a
a -> forall s era.
Ord s =>
Direct (Term era s) -> Term era (Set s) -> Pred era
Member (forall a b. b -> Either a b
Right (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era a
a)) (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Set a)
b)
substPred Subst era
sub (NotMember Term era a
a Term era (Set a)
b) = forall s era. Ord s => Term era s -> Term era (Set s) -> Pred era
NotMember (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era a
a) (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Set a)
b)
substPred Subst era
sub (MapMember Term era k
k Term era v
v Direct (Term era (Map k v))
dirM) = case Direct (Term era (Map k v))
dirM of
  Left Term era (Map k v)
m -> forall s b era.
(Ord s, Eq b, Ord b) =>
Term era s -> Term era b -> Direct (Term era (Map s b)) -> Pred era
MapMember (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era k
k) (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era v
v) (forall a b. a -> Either a b
Left (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Map k v)
m))
  Right Term era (Map k v)
m -> forall s b era.
(Ord s, Eq b, Ord b) =>
Term era s -> Term era b -> Direct (Term era (Map s b)) -> Pred era
MapMember (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era k
k) (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era v
v) (forall a b. b -> Either a b
Right (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Map k v)
m))
substPred Subst era
sub (Term era t
a :<-: RootTarget era r t
b) = forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
a forall era s b. Term era s -> RootTarget era b s -> Pred era
:<-: forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
sub RootTarget era r t
b
substPred Subst era
sub (GenFrom Term era t
a RootTarget era r (Gen t)
b) = forall era s b. Term era s -> RootTarget era b (Gen s) -> Pred era
GenFrom (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
a) (forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
sub RootTarget era r (Gen t)
b)
substPred Subst era
sub (List Term era fs
a [Term era t]
b) = forall s b era.
FromList s b =>
Term era s -> [Term era b] -> Pred era
List (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era fs
a) (forall a b. (a -> b) -> [a] -> [b]
map (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub) [Term era t]
b)
substPred Subst era
sub (Choose Term era Size
sz Term era [t]
t [(Int, Target era t, [Pred era])]
pairs) = forall era s.
(Era era, Eq s) =>
Term era Size
-> Term era [s] -> [(Int, Target era s, [Pred era])] -> Pred era
Choose (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era Size
sz) (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era [t]
t) (forall a b. (a -> b) -> [a] -> [b]
map (forall {era} {a} {r} {t}.
Subst era
-> (a, RootTarget era r t, [Pred era])
-> (a, RootTarget era r t, [Pred era])
subPair Subst era
sub) [(Int, Target era t, [Pred era])]
pairs)
  where
    subPair :: Subst era
-> (a, RootTarget era r t, [Pred era])
-> (a, RootTarget era r t, [Pred era])
subPair Subst era
sub0 (a
i, RootTarget era r t
tar, [Pred era]
ps) = (a
i, RootTarget era r t
tar, forall a b. (a -> b) -> [a] -> [b]
map (forall era. Subst era -> Pred era -> Pred era
substPred (forall era. Subst era -> Subst era -> Subst era
composeSubst Subst era
sub1 Subst era
sub0)) [Pred era]
ps)
      where
        sub1 :: Subst era
sub1 = forall era r t. RootTarget era r t -> Subst era
substFromTarget RootTarget era r t
tar
substPred Subst era
sub (Oneof Term era t
t [(Int, RootTarget era t t, [Pred era])]
ps) = forall s era.
(Eq s, Era era) =>
Term era s -> [(Int, RootTarget era s s, [Pred era])] -> Pred era
Oneof (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
t) (forall a b. (a -> b) -> [a] -> [b]
map (\(Int
i, RootTarget era t t
tr, [Pred era]
p) -> (Int
i, forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
sub RootTarget era t t
tr, forall a b. (a -> b) -> [a] -> [b]
map (forall era. Subst era -> Pred era -> Pred era
substPred Subst era
sub) [Pred era]
p)) [(Int, RootTarget era t t, [Pred era])]
ps)
substPred Subst era
sub (ForEach Term era Size
sz Term era fs
t Pat era t
pat [Pred era]
ps) =
  forall era s b.
(Era era, FromList s b, Eq b) =>
Term era Size -> Term era s -> Pat era b -> [Pred era] -> Pred era
ForEach
    (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era Size
sz)
    (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era fs
t)
    Pat era t
pat
    (forall a b. (a -> b) -> [a] -> [b]
map (forall era. Subst era -> Pred era -> Pred era
substPred Subst era
sub1) [Pred era]
ps)
  where
    sub1 :: Subst era
sub1 = forall era. Subst era -> Subst era -> Subst era
composeSubst (forall era t. Pat era t -> Subst era
substFromPat Pat era t
pat) Subst era
sub
substPred Subst era
sub (Maybe Term era (Maybe t)
term RootTarget era r t
target [Pred era]
ps) = forall s era b.
(Era era, Typeable s) =>
Term era (Maybe b) -> RootTarget era s b -> [Pred era] -> Pred era
Maybe (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Maybe t)
term) RootTarget era r t
target (forall a b. (a -> b) -> [a] -> [b]
map (forall era. Subst era -> Pred era -> Pred era
substPred (forall era. Subst era -> Subst era -> Subst era
composeSubst Subst era
sub1 Subst era
sub)) [Pred era]
ps)
  where
    sub1 :: Subst era
sub1 = forall era r t. RootTarget era r t -> Subst era
substFromTarget RootTarget era r t
target
substPred Subst era
sub (SubMap Term era (Map k v)
a Term era (Map k v)
b) = forall s b era.
(Ord s, Eq b, Ord b) =>
Term era (Map s b) -> Term era (Map s b) -> Pred era
SubMap (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Map k v)
a) (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Map k v)
b)
substPred Subst era
sub (If RootTarget era r Bool
t Pred era
x Pred era
y) = forall era s.
RootTarget era s Bool -> Pred era -> Pred era -> Pred era
If (forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
sub RootTarget era r Bool
t) (forall era. Subst era -> Pred era -> Pred era
substPred Subst era
sub Pred era
x) (forall era. Subst era -> Pred era -> Pred era
substPred Subst era
sub Pred era
y)
substPred Subst era
sub (Before Term era a
a Term era b
b) = forall era s b. Term era s -> Term era b -> Pred era
Before (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era a
a) (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era b
b)
substPred Subst era
sub (ListWhere Term era Size
sz Term era [t]
t RootTarget era t t
tar [Pred era]
ps) =
  forall era s.
(Era era, Eq s) =>
Term era Size
-> Term era [s] -> RootTarget era s s -> [Pred era] -> Pred era
ListWhere (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era Size
sz) (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era [t]
t) RootTarget era t t
tar (forall a b. (a -> b) -> [a] -> [b]
map (forall era. Subst era -> Pred era -> Pred era
substPred Subst era
newsub) [Pred era]
ps)
  where
    newsub :: Subst era
newsub = forall era. Subst era -> Subst era -> Subst era
composeSubst (forall era r t. RootTarget era r t -> Subst era
substFromTarget RootTarget era t t
tar) Subst era
sub

-- | Apply the Subst, and test if all variables are removed.
substPredWithVarTest :: Subst era -> Pred era -> Pred era
substPredWithVarTest :: forall era. Subst era -> Pred era -> Pred era
substPredWithVarTest Subst era
sub Pred era
oldpred =
  let newpred :: Pred era
newpred = forall era. Subst era -> Pred era -> Pred era
substPred Subst era
sub Pred era
oldpred
      freevars :: HashSet (Name era)
freevars = forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred forall a. HashSet a
HashSet.empty Pred era
newpred
   in case forall a. HashSet a -> Bool
HashSet.null HashSet (Name era)
freevars of
        Bool
False -> Pred era
newpred
        Bool
True ->
          forall a. HasCallStack => [Char] -> a
error
            ( [[Char]] -> [Char]
unlines
                [ [Char]
"When solving: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Pred era
oldpred forall a. [a] -> [a] -> [a]
++ [Char]
","
                , [Char]
"we applied the Subst from earlier stages, and we obtain the pred:"
                , [Char]
"   " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Pred era
newpred
                , [Char]
"with no free variables. This probably means an introductory pred like (Sized x)"
                , [Char]
"or (Random x), appears both in an earlier stage, and the current stage."
                ]
            )
  where

substFromTarget :: RootTarget era r t -> Subst era
substFromTarget :: forall era r t. RootTarget era r t -> Subst era
substFromTarget RootTarget era r t
tar = forall era. HashSet (Name era) -> Subst era
substFromNames (forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget forall a. HashSet a
HashSet.empty RootTarget era r t
tar)

substFromPat :: Pat era t -> Subst era
substFromPat :: forall era t. Pat era t -> Subst era
substFromPat Pat era t
pat = forall era. HashSet (Name era) -> Subst era
substFromNames (forall era t. HashSet (Name era) -> Pat era t -> HashSet (Name era)
varsOfPat forall a. HashSet a
HashSet.empty Pat era t
pat)

substSum :: Subst era -> Sum era t -> Sum era t
substSum :: forall era t. Subst era -> Sum era t -> Sum era t
substSum Subst era
sub (SumMap Term era (Map a t)
x) = forall c era s. Adds c => Term era (Map s c) -> Sum era c
SumMap (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Map a t)
x)
substSum Subst era
sub (SumList Term era [t]
x) = forall c era. Adds c => Term era [c] -> Sum era c
SumList (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era [t]
x)
substSum Subst era
sub (One Term era t
x) = forall era c. Term era c -> Sum era c
One (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
x)
substSum Subst era
sub (ProjOne Lens' x t
l Rep era t
r Term era x
x) = forall s c era. Lens' s c -> Rep era c -> Term era s -> Sum era c
ProjOne Lens' x t
l Rep era t
r (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era x
x)
substSum Subst era
sub (ProjMap Rep era t
crep Lens' x t
l Term era (Map a x)
x) = forall s c b era.
Adds c =>
Rep era c -> Lens' s c -> Term era (Map b s) -> Sum era c
ProjMap Rep era t
crep Lens' x t
l (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Map a x)
x)

substTarget :: Subst era -> RootTarget era r t -> RootTarget era r t
substTarget :: forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
sub (Simple Term era t
e) = forall era t. Term era t -> RootTarget era Void t
Simple (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
e)
substTarget Subst era
sub (Lensed Term era t
e SimpleGetter r t
l) = forall era t root.
Term era t -> SimpleGetter root t -> RootTarget era root t
Lensed (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
e) SimpleGetter r t
l
substTarget Subst era
sub (Partial Term era t
e r -> Maybe t
l) = forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
e) r -> Maybe t
l
substTarget Subst era
sub (RootTarget era r (a -> t)
a :$ RootTarget era r a
b) = forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
sub RootTarget era r (a -> t)
a forall era r s b.
RootTarget era r (s -> b)
-> RootTarget era r s -> RootTarget era r b
:$ forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
sub RootTarget era r a
b
substTarget Subst era
_ (Constr [Char]
n a -> b
f) = forall s b era. [Char] -> (s -> b) -> RootTarget era Void (s -> b)
Constr [Char]
n a -> b
f
substTarget Subst era
_ (Invert [Char]
x TypeRep r
l a -> b
f) = forall root s b era.
[Char] -> TypeRep root -> (s -> b) -> RootTarget era root (s -> b)
Invert [Char]
x TypeRep r
l a -> b
f
substTarget Subst era
sub (Shift RootTarget era root2 t
x Lens' r root2
l) = forall era s a root1.
RootTarget era s a -> Lens' root1 s -> RootTarget era root1 a
Shift (forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
sub RootTarget era root2 t
x) Lens' r root2
l
substTarget Subst era
sub (Mask RootTarget era r t
x) = forall era s a. RootTarget era s a -> RootTarget era Void a
Mask (forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
sub RootTarget era r t
x)
substTarget Subst era
sub (Virtual Term era t
x PDoc
y Lens' r t
l) = forall era t root.
Term era t -> PDoc -> Lens' root t -> RootTarget era root t
Virtual (forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
x) PDoc
y Lens' r t
l

-- ======================================================
-- Symbolic evaluators

-- | Simplify Terms that only contain Literals (or constant) sub-Terms
simplify :: Term era t -> Typed t
simplify :: forall era t. Term era t -> Typed t
simplify (Lit Rep era t
_ t
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure t
x
simplify (Dom (Lit Rep era (Map a b)
_ Map a b
x)) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Map k a -> Set k
Map.keysSet Map a b
x)
simplify (Dom (ProjM Lens' b t
_ Rep era t
_ Term era (Map a b)
t)) = forall era t. Term era t -> Typed t
simplify (forall s era b. Ord s => Term era (Map s b) -> Term era (Set s)
Dom Term era (Map a b)
t)
simplify (Dom Term era (Map a b)
x) = do
  Map a b
m <- forall era t. Term era t -> Typed t
simplify Term era (Map a b)
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Map k a -> Set k
Map.keysSet Map a b
m)
simplify (Rng (Lit Rep era (Map a b)
_ Map a b
x)) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Ord a => [a] -> Set a
Set.fromList (forall k a. Map k a -> [a]
Map.elems Map a b
x))
simplify (Rng (ProjM Lens' b t
l Rep era t
_ (Lit Rep era (Map a b)
_ Map a b
m))) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Ord a => [a] -> Set a
Set.fromList (forall k a. Map k a -> [a]
Map.elems (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\b
x -> b
x forall s a. s -> Getting a s a -> a
^. Lens' b t
l) Map a b
m)))
simplify (Rng Term era (Map a b)
x) = do
  Map a b
m <- forall era t. Term era t -> Typed t
simplify Term era (Map a b)
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Ord a => [a] -> Set a
Set.fromList (forall k a. Map k a -> [a]
Map.elems Map a b
m))
simplify (Elems (Lit Rep era (Map a b)
_ Map a b
x)) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Map k a -> [a]
Map.elems Map a b
x)
simplify (Elems (ProjM Lens' b t
l Rep era t
_ (Lit Rep era (Map a b)
_ Map a b
m))) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Map k a -> [a]
Map.elems (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\b
x -> b
x forall s a. s -> Getting a s a -> a
^. Lens' b t
l) Map a b
m))
simplify (Elems Term era (Map a b)
x) = do
  Map a b
m <- forall era t. Term era t -> Typed t
simplify Term era (Map a b)
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Map k a -> [a]
Map.elems Map a b
m)
simplify (ProjM Lens' b t
l Rep era t
_ (Lit Rep era (Map a b)
_ Map a b
x)) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\b
z -> b
z forall s a. s -> Getting a s a -> a
^. Lens' b t
l) Map a b
x)
simplify (ProjM Lens' b t
l Rep era t
_ Term era (Map a b)
t) = do
  Map a b
m <- forall era t. Term era t -> Typed t
simplify Term era (Map a b)
t
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\b
z -> b
z forall s a. s -> Getting a s a -> a
^. Lens' b t
l) Map a b
m)
simplify (ProjS Lens' b t
l Rep era t
_ (Lit Rep era (Set b)
_ Set b
x)) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\b
z -> b
z forall s a. s -> Getting a s a -> a
^. Lens' b t
l) Set b
x)
simplify (ProjS Lens' b t
l Rep era t
_ Term era (Set b)
t) = do
  Set b
s <- forall era t. Term era t -> Typed t
simplify Term era (Set b)
t
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\b
z -> b
z forall s a. s -> Getting a s a -> a
^. Lens' b t
l) Set b
s)
simplify (Proj Lens' b t
l Rep era t
_ (Lit Rep era b
_ b
x)) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (b
x forall s a. s -> Getting a s a -> a
^. Lens' b t
l)
simplify (Proj Lens' b t
l Rep era t
_ Term era b
t) = do
  b
s <- forall era t. Term era t -> Typed t
simplify Term era b
t
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (b
s forall s a. s -> Getting a s a -> a
^. Lens' b t
l)
simplify (Delta (Lit Rep era Coin
CoinR (Coin Integer
n))) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> DeltaCoin
DeltaCoin Integer
n)
simplify (Negate (Lit Rep era DeltaCoin
DeltaCoinR (DeltaCoin Integer
n))) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> DeltaCoin
DeltaCoin (-Integer
n))
simplify (Restrict Term era (Set a)
s Term era (Map a b)
m) = do
  Set a
sv <- forall era t. Term era t -> Typed t
simplify Term era (Set a)
s
  Map a b
mv <- forall era t. Term era t -> Typed t
simplify Term era (Map a b)
m
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map a b
mv Set a
sv)
simplify (HashS Term era (ScriptF era)
s) = do
  ScriptF Proof era
_ Script era
sv <- forall era t. Term era t -> Typed t
simplify Term era (ScriptF era)
s
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era.
EraScript era =>
Script era -> ScriptHash (EraCrypto era)
hashScript Script era
sv)
simplify (HashD Term era (Data era)
s) = do
  Data era
sv <- forall era t. Term era t -> Typed t
simplify Term era (Data era)
s
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era. Era era => Data era -> DataHash (EraCrypto era)
hashData Data era
sv)
simplify (Pair Term era a
s Term era b
m) = do
  a
sv <- forall era t. Term era t -> Typed t
simplify Term era a
s
  b
mv <- forall era t. Term era t -> Typed t
simplify Term era b
m
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
sv, b
mv)
simplify Term era t
x = forall a. [[Char]] -> Typed a
failT [[Char]
"Can't simplify term: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era t
x forall a. [a] -> [a] -> [a]
++ [Char]
", to a value."]

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

simplifyTarget :: forall era t root. RootTarget era root t -> Typed t
simplifyTarget :: forall era t root. RootTarget era root t -> Typed t
simplifyTarget (Invert [Char]
_ TypeRep root
_ a -> b
f) = forall (f :: * -> *) a. Applicative f => a -> f a
pure a -> b
f
simplifyTarget (Shift RootTarget era root2 t
x Lens' root root2
_) = forall era t root. RootTarget era root t -> Typed t
simplifyTarget RootTarget era root2 t
x
simplifyTarget (Mask RootTarget era r t
x) = forall era t root. RootTarget era root t -> Typed t
simplifyTarget RootTarget era r t
x
simplifyTarget (Virtual Term era t
x PDoc
_ Lens' root t
_) = forall era t. Term era t -> Typed t
simplify Term era t
x
simplifyTarget (Simple Term era t
t) = forall era t. Term era t -> Typed t
simplify Term era t
t
simplifyTarget (Lensed Term era t
t SimpleGetter root t
_) = forall era t. Term era t -> Typed t
simplify Term era t
t
simplifyTarget (Partial Term era t
t root -> Maybe t
_) = forall era t. Term era t -> Typed t
simplify Term era t
t
simplifyTarget (Constr [Char]
_ a -> b
f) = forall (f :: * -> *) a. Applicative f => a -> f a
pure a -> b
f
simplifyTarget (RootTarget era root (a -> t)
x :$ RootTarget era root a
y) = do
  a -> t
f <- forall era t root. RootTarget era root t -> Typed t
simplifyTarget RootTarget era root (a -> t)
x
  a
z <- forall era t root. RootTarget era root t -> Typed t
simplifyTarget RootTarget era root a
y
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> t
f a
z)

-- | Fully evaluate a `Term`, looking up the variables in the `Env`.
runTerm :: Env era -> Term era t -> Typed t
runTerm :: forall era t. Env era -> Term era t -> Typed t
runTerm Env era
_ (Lit Rep era t
_ t
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure t
x
runTerm Env era
env (Dom Term era (Map a b)
x) = forall k a. Map k a -> Set k
Map.keysSet forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map a b)
x
runTerm Env era
env (Rng Term era (Map a b)
x) = forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
Map.elems forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map a b)
x
runTerm Env era
env (Elems Term era (Map a b)
x) = forall k a. Map k a -> [a]
Map.elems forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map a b)
x
runTerm Env era
env (Var V era t
v) = forall era t. V era t -> Env era -> Typed t
findVar V era t
v Env era
env
runTerm Env era
env (ProjM Lens' b t
l Rep era t
_ Term era (Map a b)
x) = do
  Map a b
m <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map a b)
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\b
z -> b
z forall s a. s -> Getting a s a -> a
^. Lens' b t
l) Map a b
m)
runTerm Env era
env (ProjS Lens' b t
l Rep era t
_ Term era (Set b)
x) = do
  Set b
m <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set b)
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\b
z -> b
z forall s a. s -> Getting a s a -> a
^. Lens' b t
l) Set b
m)
runTerm Env era
env (Proj Lens' b t
l Rep era t
_ Term era b
x) = do
  b
m <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era b
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (b
m forall s a. s -> Getting a s a -> a
^. Lens' b t
l)
runTerm Env era
env (Delta Term era Coin
x) = do
  Coin Integer
n <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era Coin
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> DeltaCoin
DeltaCoin Integer
n)
runTerm Env era
env (Negate Term era DeltaCoin
x) = do
  DeltaCoin Integer
n <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era DeltaCoin
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> DeltaCoin
DeltaCoin (-Integer
n))
runTerm Env era
env (Restrict Term era (Set a)
s Term era (Map a b)
m) = do
  Set a
sv <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set a)
s
  Map a b
mv <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map a b)
m
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map a b
mv Set a
sv)
runTerm Env era
env (HashD Term era (Data era)
x) = do
  Data era
s <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Data era)
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era. Era era => Data era -> DataHash (EraCrypto era)
hashData Data era
s)
runTerm Env era
env (HashS Term era (ScriptF era)
x) = do
  ScriptF Proof era
_ Script era
s <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (ScriptF era)
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era.
EraScript era =>
Script era -> ScriptHash (EraCrypto era)
hashScript Script era
s)
runTerm Env era
env (Pair Term era a
s Term era b
m) =
  do
    a
sv <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
s
    b
mv <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era b
m
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
sv, b
mv)

runTarget :: Env era -> RootTarget era x t -> Typed t
runTarget :: forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
_ (Invert [Char]
_ TypeRep x
_ a -> b
f) = forall (f :: * -> *) a. Applicative f => a -> f a
pure a -> b
f
runTarget Env era
env (Simple Term era t
t) = forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era t
t
runTarget Env era
env (Lensed Term era t
t SimpleGetter x t
_) = forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era t
t
runTarget Env era
env (Partial Term era t
t x -> Maybe t
_) = forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era t
t
runTarget Env era
env (Shift RootTarget era root2 t
x Lens' x root2
_) = forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env RootTarget era root2 t
x
runTarget Env era
env (Mask RootTarget era r t
x) = forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env RootTarget era r t
x
runTarget Env era
env (Virtual Term era t
x PDoc
_ Lens' x t
_) = forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era t
x
runTarget Env era
_ (Constr [Char]
_ a -> b
f) = forall (f :: * -> *) a. Applicative f => a -> f a
pure a -> b
f
runTarget Env era
env (RootTarget era x (a -> t)
x :$ RootTarget era x a
y) = do
  a -> t
f <- forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env RootTarget era x (a -> t)
x
  a
z <- forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env RootTarget era x a
y
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> t
f a
z)

-- | Overwrite the bindings for the Vars in the Env that appear in the RootTarget, by updating the Env with the values picked from the root
--   When the target has type (RootTarget era Void x), the function is the identity on the Env.
getTarget :: forall era root t. root -> RootTarget era root t -> Env era -> Env era
getTarget :: forall era root t.
root -> RootTarget era root t -> Env era -> Env era
getTarget root
root (Lensed (Var V era t
v) SimpleGetter root t
l) Env era
env = forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v (root
root forall s a. s -> Getting a s a -> a
^. SimpleGetter root t
l) Env era
env
getTarget root
_ (Lensed Term era t
_ SimpleGetter root t
_) Env era
env = Env era
env
getTarget root
root (Partial (Var V era t
v) root -> Maybe t
f) Env era
env =
  case root -> Maybe t
f root
root of
    Just t
val -> forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v t
val Env era
env
    Maybe t
Nothing ->
      forall a. HasCallStack => [Char] -> a
error
        ( [Char]
"A Partial RootTarget returned Nothing: "
            forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show V era t
v
            forall a. [a] -> [a] -> [a]
++ [Char]
"\n Maybe use 'targetMaybeEnv' instead of 'getTarget' "
        )
getTarget root
_ (Partial Term era t
_ root -> Maybe t
_) Env era
env = Env era
env
getTarget root
root (RootTarget era root (a -> t)
x :$ RootTarget era root a
y) Env era
env = forall era root t.
root -> RootTarget era root t -> Env era -> Env era
getTarget root
root RootTarget era root (a -> t)
x (forall era root t.
root -> RootTarget era root t -> Env era -> Env era
getTarget root
root RootTarget era root a
y Env era
env)
getTarget root
root (Shift RootTarget era root2 t
x Lens' root root2
l) Env era
env = forall era root t.
root -> RootTarget era root t -> Env era -> Env era
getTarget (root
root forall s a. s -> Getting a s a -> a
^. Lens' root root2
l) RootTarget era root2 t
x Env era
env
getTarget root
_ (Invert [Char]
_ TypeRep root
_ a -> b
_) Env era
env = Env era
env
getTarget root
_ (Constr [Char]
_ a -> b
_) Env era
env = Env era
env
getTarget root
_ (Simple Term era t
_) Env era
env = Env era
env
getTarget root
_ (Mask RootTarget era r t
_) Env era
env = Env era
env
getTarget root
root (Virtual (Var V era t
v) PDoc
_ Lens' root t
l) Env era
env = forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v (root
root forall s a. s -> Getting a s a -> a
^. Lens' root t
l) Env era
env
getTarget root
_ (Virtual {}) Env era
env = Env era
env

targetMaybeEnv :: forall era root t. root -> RootTarget era root t -> Env era -> Maybe (Env era)
targetMaybeEnv :: forall era root t.
root -> RootTarget era root t -> Env era -> Maybe (Env era)
targetMaybeEnv root
root (Lensed (Var V era t
v) SimpleGetter root t
l) Env era
env = forall a. a -> Maybe a
Just (forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v (root
root forall s a. s -> Getting a s a -> a
^. SimpleGetter root t
l) Env era
env)
targetMaybeEnv root
root (Virtual (Var V era t
v) PDoc
_ Lens' root t
l) Env era
env = forall a. a -> Maybe a
Just (forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v (root
root forall s a. s -> Getting a s a -> a
^. Lens' root t
l) Env era
env)
targetMaybeEnv root
root (Shift RootTarget era root2 t
x Lens' root root2
l) Env era
env = forall era root t.
root -> RootTarget era root t -> Env era -> Maybe (Env era)
targetMaybeEnv (root
root forall s a. s -> Getting a s a -> a
^. Lens' root root2
l) RootTarget era root2 t
x Env era
env
targetMaybeEnv root
root (Partial (Var V era t
v) root -> Maybe t
f) Env era
env =
  case root -> Maybe t
f root
root of
    Just t
val -> forall a. a -> Maybe a
Just (forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v t
val Env era
env)
    Maybe t
Nothing -> forall a. Maybe a
Nothing
targetMaybeEnv root
root (RootTarget era root (a -> t)
x :$ RootTarget era root a
y) Env era
env =
  forall era root t.
root -> RootTarget era root t -> Env era -> Maybe (Env era)
targetMaybeEnv root
root RootTarget era root a
y Env era
env forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era root t.
root -> RootTarget era root t -> Env era -> Maybe (Env era)
targetMaybeEnv root
root RootTarget era root (a -> t)
x
targetMaybeEnv root
_ RootTarget era root t
_ Env era
_ = forall a. Maybe a
Nothing

runPred :: Env era -> Pred era -> Typed Bool
runPred :: forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env (MetaSize Size
w Term era Size
x) = do
  Size
sz <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era Size
x
  case Size
sz of
    SzExact Int
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Int -> Size -> Bool
runSize Int
n Size
w
    Size
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Bool
False
runPred Env era
env (Sized Term era Size
szt Term era t
tt) = do
  Size
sz <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era Size
szt
  t
t <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era t
tt
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Int -> Size -> Bool
runSize (forall t. Sizeable t => t -> Int
getSize t
t) Size
sz
runPred Env era
env (Term era a
x :=: Term era a
y) = do
  a
x2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
x
  a
y2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
y
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
x2 forall a. Eq a => a -> a -> Bool
== a
y2)
runPred Env era
env (Disjoint Term era (Set a)
x Term era (Set a)
y) = do
  Set a
x2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set a)
x
  Set a
y2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set a)
y
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set a
x2 Set a
y2)
runPred Env era
env (Subset Term era (Set a)
x Term era (Set a)
y) = do
  Set a
x2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set a)
x
  Set a
y2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set a)
y
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set a
x2 Set a
y2)
runPred Env era
env (SumsTo Direct c
_ Term era c
x OrdCond
cond [Sum era c]
ys) = do
  c
x2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era c
x
  [c]
is <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall era c. Env era -> Sum era c -> Typed c
runSum Env era
env) [Sum era c]
ys
  let y2 :: c
y2 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall x. Adds x => x -> x -> x
add forall x. Adds x => x
zero [c]
is
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall x. Adds x => OrdCond -> x -> x -> Bool
runOrdCondition OrdCond
cond c
x2 c
y2)
runPred Env era
env (SumSplit c
_ Term era c
x OrdCond
cond [Sum era c]
ys) = do
  c
x2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era c
x
  [c]
is <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall era c. Env era -> Sum era c -> Typed c
runSum Env era
env) [Sum era c]
ys
  let y2 :: c
y2 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall x. Adds x => x -> x -> x
add forall x. Adds x => x
zero [c]
is
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall x. Adds x => OrdCond -> x -> x -> Bool
runOrdCondition OrdCond
cond c
x2 c
y2)
runPred Env era
_ (Random Term era t
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
runPred Env era
env (Component Direct (Term era t)
t [AnyF era t]
cs) = do
  t
t' <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env (forall a. Direct a -> a
direct Direct (Term era t)
t)
  forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall era s. Env era -> s -> AnyF era s -> Typed Bool
runComp Env era
env t
t') [AnyF era t]
cs
runPred Env era
env (CanFollow Term era n
x Term era n
y) = do
  n
x2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era n
x
  n
y2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era n
y
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall t. Count t => t -> t -> Bool
canFollow n
x2 n
y2)
runPred Env era
env (Member Direct (Term era a)
x Term era (Set a)
y) = do
  a
x2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env (forall a. Direct a -> a
direct Direct (Term era a)
x)
  Set a
y2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set a)
y
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Ord a => a -> Set a -> Bool
Set.member a
x2 Set a
y2)
runPred Env era
env (NotMember Term era a
x Term era (Set a)
y) = do
  a
x2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
x
  Set a
y2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set a)
y
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Ord a => a -> Set a -> Bool
Set.notMember a
x2 Set a
y2)
runPred Env era
env (MapMember Term era k
k Term era v
v Direct (Term era (Map k v))
m) = do
  k
k' <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era k
k
  v
v' <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era v
v
  Map k v
m' <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env (forall a. Direct a -> a
direct Direct (Term era (Map k v))
m)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
Map.isSubmapOf (forall k a. k -> a -> Map k a
Map.singleton k
k' v
v') Map k v
m'
runPred Env era
env (Term era t
x :<-: RootTarget era r t
y) = do
  t
_x2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era t
x
  t
_y2 <- forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env RootTarget era r t
y
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
runPred Env era
env (GenFrom Term era t
x RootTarget era r (Gen t)
y) = do
  t
_x2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era t
x
  Gen t
_y2 <- forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env RootTarget era r (Gen t)
y
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
runPred Env era
env (List Term era fs
x [Term era t]
y) = do
  fs
x2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era fs
x
  [t]
y2 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env) [Term era t]
y
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (fs
x2 forall a. Eq a => a -> a -> Bool
== forall ts a. FromList ts a => [a] -> ts
makeFromList [t]
y2)
runPred Env era
env (Maybe Term era (Maybe t)
x RootTarget era r t
tar [Pred era]
ps) = do
  Maybe t
m <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Maybe t)
x
  case Maybe t
m of
    Maybe t
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    (Just t
y) -> do
      [Bool]
ans <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall era. Env era -> Pred era -> Typed Bool
runPred (forall era r t. RootTarget era r t -> t -> Env era -> Env era
bind RootTarget era r t
tar t
y Env era
env)) [Pred era]
ps
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
ans)
-- choose should have been removed by the Rewrite phase.
runPred Env era
_ (Choose Term era Size
_ Term era [t]
_ [(Int, Target era t, [Pred era])]
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True -- We can't really test this. failT ["Choose predicate in runPred", show p]
runPred Env era
env (ForEach Term era Size
_sz Term era fs
term Pat era t
pat [Pred era]
ps) = do
  -- size <- runTerm env _sz
  [t]
ts <- forall ts a. FromList ts a => ts -> [a]
getList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era fs
term
  [Bool]
bs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\t
t -> forall era. Env era -> [Pred era] -> Typed Bool
runPreds (forall t era. t -> Env era -> Pat era t -> Env era
bindPat t
t Env era
env Pat era t
pat) (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era t. Pat era t -> Pred era -> Bool
extendableSumsTo Pat era t
pat) [Pred era]
ps)) [t]
ts
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
bs)
runPred Env era
env (SubMap Term era (Map k v)
x Term era (Map k v)
y) = do
  Map k v
x2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map k v)
x
  Map k v
y2 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map k v)
y
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
Map.isSubmapOf Map k v
x2 Map k v
y2)
runPred Env era
env (If RootTarget era r Bool
t Pred era
x Pred era
y) = do
  Bool
b <- forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env RootTarget era r Bool
t
  if Bool
b
    then forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env Pred era
x
    else forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env Pred era
y
runPred Env era
_ (Before Term era a
_ Term era b
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
runPred Env era
env (Oneof Term era t
name [(Int, RootTarget era t t, [Pred era])]
triples) = do
  t
root <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era t
name
  let firstMatching :: [(Int, RootTarget era t t, [Pred era])] -> Typed Bool
firstMatching [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
      firstMatching ((Int
_, RootTarget era t t
tar, [Pred era]
ps) : [(Int, RootTarget era t t, [Pred era])]
more) = case forall era root t.
root -> RootTarget era root t -> Env era -> Maybe (Env era)
targetMaybeEnv t
root RootTarget era t t
tar Env era
env of
        Maybe (Env era)
Nothing -> [(Int, RootTarget era t t, [Pred era])] -> Typed Bool
firstMatching [(Int, RootTarget era t t, [Pred era])]
more
        Just Env era
env2 -> do
          [Bool]
qs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env2) [Pred era]
ps
          if forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
qs
            then forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
            else [(Int, RootTarget era t t, [Pred era])] -> Typed Bool
firstMatching [(Int, RootTarget era t t, [Pred era])]
more
  [(Int, RootTarget era t t, [Pred era])] -> Typed Bool
firstMatching [(Int, RootTarget era t t, [Pred era])]
triples
runPred Env era
env (ListWhere Term era Size
sz Term era [t]
name RootTarget era t t
target [Pred era]
ps) = do
  [t]
xs <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era [t]
name
  Size
size <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era Size
sz
  let sizeOK :: Bool
sizeOK = Int -> Size -> Bool
runSize (forall (t :: * -> *) a. Foldable t => t a -> Int
length [t]
xs) Size
size
  let p :: t -> Typed Bool
p t
x = do
        let env2 :: Env era
env2 = forall era root t.
root -> RootTarget era root t -> Env era -> Env era
getTarget t
x RootTarget era t t
target Env era
env
        [Bool]
bs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env2) [Pred era]
ps
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
bs)
  [Bool]
bs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM t -> Typed Bool
p [t]
xs
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Bool
sizeOK Bool -> Bool -> Bool
&& (forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
bs)

hashSetToSet :: Ord a => HashSet a -> Set a
hashSetToSet :: forall a. Ord a => HashSet a -> Set a
hashSetToSet HashSet a
x = forall a. Ord a => [a] -> Set a
Set.fromList (forall a. HashSet a -> [a]
HashSet.toList HashSet a
x)

hashSetDisjoint :: Hashable a => HashSet a -> HashSet a -> Bool
hashSetDisjoint :: forall a. Hashable a => HashSet a -> HashSet a -> Bool
hashSetDisjoint HashSet a
x HashSet a
y = forall a. HashSet a -> Bool
HashSet.null (forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.intersection HashSet a
x HashSet a
y)

-- | One type of Pred in ForEach is handled differently from others
--   if valCoin is amongst the free variables of `pat` and
--   'balanceCoin' is not amongst the free variables of `pat` then
--   SumsTo (Left (Coin 1)) balanceCoin EQL [One valCoin]  expands to
--   SumsTo (Left (Coin 1)) balanceCoin EQL [One valCoin.1,One valCoin.2,One valCoin.3]

--   SumSplit (Coin 1) balanceCoin EQL [One valCoin]  expands to
--   SumSplit (Coin 1) balanceCoin EQL [One valCoin.1,One valCoin.2,One valCoin.3]

--   other predicates P(x) would exapnd to 3 copies like P(x.1) P(x.2) P(x.3)
--   This is called Sum extension, is implemented by `extendSum`
extendableSumsTo :: Pat era t -> Pred era -> Bool
extendableSumsTo :: forall era t. Pat era t -> Pred era -> Bool
extendableSumsTo Pat era t
pat (SumsTo Direct c
_ Term era c
t OrdCond
_ [One Term era c
s]) =
  forall a. HashSet a -> Int
HashSet.size HashSet (Name era)
boundS forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> Bool
HashSet.isSubsetOf HashSet (Name era)
boundS HashSet (Name era)
free Bool -> Bool -> Bool
&& forall a. Hashable a => HashSet a -> HashSet a -> Bool
hashSetDisjoint HashSet (Name era)
boundT HashSet (Name era)
free
  where
    free :: HashSet (Name era)
free = forall era t. HashSet (Name era) -> Pat era t -> HashSet (Name era)
varsOfPat forall a. HashSet a
HashSet.empty Pat era t
pat
    boundS :: HashSet (Name era)
boundS = forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm forall a. HashSet a
HashSet.empty Term era c
s
    boundT :: HashSet (Name era)
boundT = forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm forall a. HashSet a
HashSet.empty Term era c
t
extendableSumsTo Pat era t
pat (SumSplit c
_ Term era c
t OrdCond
_ [One Term era c
s]) =
  forall a. HashSet a -> Int
HashSet.size HashSet (Name era)
boundS forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> Bool
HashSet.isSubsetOf HashSet (Name era)
boundS HashSet (Name era)
free Bool -> Bool -> Bool
&& forall a. Hashable a => HashSet a -> HashSet a -> Bool
hashSetDisjoint HashSet (Name era)
boundT HashSet (Name era)
free
  where
    free :: HashSet (Name era)
free = forall era t. HashSet (Name era) -> Pat era t -> HashSet (Name era)
varsOfPat forall a. HashSet a
HashSet.empty Pat era t
pat
    boundS :: HashSet (Name era)
boundS = forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm forall a. HashSet a
HashSet.empty Term era c
s
    boundT :: HashSet (Name era)
boundT = forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm forall a. HashSet a
HashSet.empty Term era c
t
extendableSumsTo Pat era t
_ Pred era
_ = Bool
False

-- | run a bunch of Preds, and and together the results
runPreds :: Env era -> [Pred era] -> Typed Bool
runPreds :: forall era. Env era -> [Pred era] -> Typed Bool
runPreds Env era
env [Pred era]
ps = do
  [Bool]
bs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env) [Pred era]
ps
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
bs)

bind :: RootTarget era r t -> t -> Env era -> Env era
bind :: forall era r t. RootTarget era r t -> t -> Env era -> Env era
bind (Simple (Var V era t
v)) t
x Env era
env = forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v t
x Env era
env
bind (Lensed (Var V era t
v) SimpleGetter r t
_) t
x Env era
env = forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v t
x Env era
env
bind RootTarget era r t
t t
_ Env era
_ = forall a. HasCallStack => [Char] -> a
error ([Char]
"Non simple Target in bind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show RootTarget era r t
t)

runComp :: Env era -> s -> AnyF era s -> Typed Bool
runComp :: forall era s. Env era -> s -> AnyF era s -> Typed Bool
runComp Env era
env s
t (AnyF (Field [Char]
n Rep era t
rt Rep era s
rx Lens' s t
l)) = do
  t
t' <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env forall a b. (a -> b) -> a -> b
$ forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
n Rep era t
rt (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era s
rx Lens' s t
l))
  With s t
_ <- forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Eq (s t))
hasEq Rep era t
rt Rep era t
rt
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ s
t forall s a. s -> Getting a s a -> a
^. Lens' s t
l forall a. Eq a => a -> a -> Bool
== t
t'
runComp Env era
_ s
t (AnyF (FConst Rep era t
r t
v Rep era s
_ Lens' s t
l)) = do
  With s t
_ <- forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Eq (s t))
hasEq Rep era t
r Rep era t
r
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ s
t forall s a. s -> Getting a s a -> a
^. Lens' s t
l forall a. Eq a => a -> a -> Bool
== t
v

termRep :: Era era => Term era t -> Rep era t
termRep :: forall era t. Era era => Term era t -> Rep era t
termRep (Lit Rep era t
r t
_) = Rep era t
r
termRep (Var (V [Char]
_ Rep era t
r Access era s t
_)) = Rep era t
r
termRep (Dom (forall era t. Era era => Term era t -> Rep era t
termRep -> MapR Rep era a
r Rep era b
_)) = forall s era. Ord s => Rep era s -> Rep era (Set s)
SetR Rep era a
r
termRep (Rng (forall era t. Era era => Term era t -> Rep era t
termRep -> MapR Rep era a
_ Rep era b
r)) = forall s era. Ord s => Rep era s -> Rep era (Set s)
SetR Rep era b
r
termRep (Elems (forall era t. Era era => Term era t -> Rep era t
termRep -> MapR Rep era a
_ Rep era b
r)) = forall era s. Rep era s -> Rep era [s]
ListR Rep era b
r
termRep (ProjM Lens' b t
_ Rep era t
t (forall era t. Era era => Term era t -> Rep era t
termRep -> MapR Rep era a
a Rep era b
_)) = forall s era b.
Ord s =>
Rep era s -> Rep era b -> Rep era (Map s b)
MapR Rep era a
a Rep era t
t
termRep (ProjS Lens' b t
_ Rep era t
t (forall era t. Era era => Term era t -> Rep era t
termRep -> SetR Rep era a
_)) = forall s era. Ord s => Rep era s -> Rep era (Set s)
SetR Rep era t
t
termRep (Proj Lens' b t
_ Rep era t
t Term era b
_) = Rep era t
t
termRep (Delta Term era Coin
_) = forall era. Rep era DeltaCoin
DeltaCoinR
termRep (Negate Term era DeltaCoin
_) = forall era. Rep era DeltaCoin
DeltaCoinR
termRep (Restrict Term era (Set a)
_ Term era (Map a b)
m) = forall era t. Era era => Term era t -> Rep era t
termRep Term era (Map a b)
m
termRep (HashD Term era (Data era)
_) = forall era. Era era => Rep era (DataHash (EraCrypto era))
DataHashR
termRep (HashS Term era (ScriptF era)
_) = forall era. Era era => Rep era (ScriptHash (EraCrypto era))
ScriptHashR
termRep (Pair Term era a
a Term era b
b) = forall era s b. Rep era s -> Rep era b -> Rep era (s, b)
PairR (forall era t. Era era => Term era t -> Rep era t
termRep Term era a
a) (forall era t. Era era => Term era t -> Rep era t
termRep Term era b
b)

runSum :: Env era -> Sum era c -> Typed c
runSum :: forall era c. Env era -> Sum era c -> Typed c
runSum Env era
env (SumMap Term era (Map a c)
t) = forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' forall x. Adds x => x -> x -> x
add forall x. Adds x => x
zero forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map a c)
t
runSum Env era
env (SumList Term era [c]
t) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall x. Adds x => x -> x -> x
add forall x. Adds x => x
zero forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era [c]
t
runSum Env era
env (One Term era c
t) = forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era c
t
runSum Env era
env (ProjOne Lens' x c
l Rep era c
_ Term era x
t) = do
  x
x <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era x
t
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (x
x forall s a. s -> Getting a s a -> a
^. Lens' x c
l)
runSum Env era
env (ProjMap Rep era c
_ Lens' x c
l Term era (Map a x)
t) = forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' c -> x -> c
accum forall x. Adds x => x
zero forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map a x)
t
  where
    accum :: c -> x -> c
accum c
ans x
x = forall x. Adds x => x -> x -> x
add c
ans (x
x forall s a. s -> Getting a s a -> a
^. Lens' x c
l)

makeTest :: Env era -> Pred era -> Typed (String, Bool, Pred era)
makeTest :: forall era. Env era -> Pred era -> Typed ([Char], Bool, Pred era)
makeTest Env era
env Pred era
c = do
  Bool
b <- forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env Pred era
c
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Show a => a -> [Char]
show Pred era
c forall a. [a] -> [a] -> [a]
++ [Char]
" => " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Bool
b, Bool
b, Pred era
c)

displayTerm :: Era era => Env era -> Term era a -> IO ()
displayTerm :: forall era a. Era era => Env era -> Term era a -> IO ()
displayTerm Env era
env (Var v :: V era a
v@(V [Char]
nm Rep era a
rep Access era s a
_)) = do
  a
x <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall era t. V era t -> Env era -> Typed t
findVar V era a
v Env era
env)
  [Char] -> IO ()
putStrLn ([Char]
nm forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> [Char]
format Rep era a
rep a
x)
displayTerm Env era
env Term era a
term = do
  a
x <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
term)
  [Char] -> IO ()
putStrLn (forall a. Show a => a -> [Char]
show Term era a
term forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> [Char]
format (forall era t. Era era => Term era t -> Rep era t
termRep Term era a
term) a
x)

-- =======================================================================
-- Patterns are used to indicate bound variables in a ForEach constraint

patToAnyF :: Pat era t -> [AnyF era t]
patToAnyF :: forall era t. Pat era t -> [AnyF era t]
patToAnyF (Pat Rep era t
rep [Arg era t]
as) = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a b. (a -> b) -> [a] -> [b]
map (forall era t. Rep era t -> Arg era t -> [AnyF era t]
argToAnyF Rep era t
rep) [Arg era t]
as)

argToAnyF :: Rep era t -> Arg era t -> [AnyF era t]
argToAnyF :: forall era t. Rep era t -> Arg era t -> [AnyF era t]
argToAnyF Rep era t
_ (Arg Field era t s
f) = [forall era s s. Field era s s -> AnyF era s
AnyF Field era t s
f]
argToAnyF Rep era t
rept (ArgPs f :: Field era t s
f@(Field [Char]
_ Rep era s
_ Rep era t
_ Lens' t s
lensx) [Pat era s]
ps) = forall era s s. Field era s s -> AnyF era s
AnyF Field era t s
f forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall era t s. Rep era t -> Lens' t s -> AnyF era s -> AnyF era t
push Rep era t
rept Lens' t s
lensx) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a b. (a -> b) -> [a] -> [b]
map forall era t. Pat era t -> [AnyF era t]
patToAnyF [Pat era s]
ps))
argToAnyF Rep era t
rept (ArgPs f :: Field era t s
f@(FConst Rep era s
_ s
_ Rep era t
_ Lens' t s
lensx) [Pat era s]
ps) = forall era s s. Field era s s -> AnyF era s
AnyF Field era t s
f forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall era t s. Rep era t -> Lens' t s -> AnyF era s -> AnyF era t
push Rep era t
rept Lens' t s
lensx) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a b. (a -> b) -> [a] -> [b]
map forall era t. Pat era t -> [AnyF era t]
patToAnyF [Pat era s]
ps))

push :: Rep era t -> Lens' t s -> AnyF era s -> AnyF era t
push :: forall era t s. Rep era t -> Lens' t s -> AnyF era s -> AnyF era t
push Rep era t
rept Lens' t s
l1 (AnyF (Field [Char]
nm Rep era t
rep Rep era s
_ Lens' s t
l2)) = forall era s s. Field era s s -> AnyF era s
AnyF (forall era t s.
Era era =>
[Char] -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field [Char]
nm Rep era t
rep Rep era t
rept (Lens' t s
l1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' s t
l2))
push Rep era t
rept Lens' t s
l1 (AnyF (FConst Rep era t
rep t
x Rep era s
_ Lens' s t
l2)) = forall era s s. Field era s s -> AnyF era s
AnyF (forall era t s.
Rep era t -> t -> Rep era s -> Lens' s t -> Field era s t
FConst Rep era t
rep t
x Rep era t
rept (Lens' t s
l1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' s t
l2))

data Pat era t where
  Pat :: !(Rep era t) -> ![Arg era t] -> Pat era t

data Arg era t where
  ArgPs :: !(Field era t s) -> ![Pat era s] -> Arg era t
  Arg :: !(Field era t s) -> Arg era t

-- | Succeds if 'term' is a variable with an embedded (Lens' t2 t1)
patt :: Rep era t1 -> Term era t2 -> Pat era t1
patt :: forall era t1 t2. Rep era t1 -> Term era t2 -> Pat era t1
patt Rep era t1
rep Term era t2
term = forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat Rep era t1
rep [forall era s t. Rep era s -> Term era t -> Arg era s
arg Rep era t1
rep Term era t2
term]

instance Show (Pat era t) where
  show :: Pat era t -> [Char]
show (Pat Rep era t
r [Arg era t]
xs) = [Char]
"Pat " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Rep era t
r forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL forall a. Show a => a -> [Char]
show [Char]
", " [Arg era t]
xs
instance Show (Arg era t) where
  show :: Arg era t -> [Char]
show (Arg (Field [Char]
nm Rep era s
_ Rep era t
_ Lens' t s
_)) = [Char]
nm
  show (Arg f :: Field era t s
f@(FConst Rep era s
_ s
_ Rep era t
_ Lens' t s
_)) = forall a. Show a => a -> [Char]
show Field era t s
f
  show (ArgPs (Field [Char]
nm Rep era s
_ Rep era t
_ Lens' t s
_) [Pat era s]
qs) = [Char]
nm forall a. [a] -> [a] -> [a]
++ [Char]
" [" forall a. [a] -> [a] -> [a]
++ forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL forall a. Show a => a -> [Char]
show [Char]
", " [Pat era s]
qs forall a. [a] -> [a] -> [a]
++ [Char]
"]"
  show (ArgPs f :: Field era t s
f@(FConst Rep era s
_ s
_ Rep era t
_ Lens' t s
_) [Pat era s]
qs) = forall a. Show a => a -> [Char]
show Field era t s
f forall a. [a] -> [a] -> [a]
++ [Char]
" [" forall a. [a] -> [a] -> [a]
++ forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL forall a. Show a => a -> [Char]
show [Char]
", " [Pat era s]
qs forall a. [a] -> [a] -> [a]
++ [Char]
"]"

varsOfField :: HashSet (Name era) -> Field era s t -> HashSet (Name era)
varsOfField :: forall era s t.
HashSet (Name era) -> Field era s t -> HashSet (Name era)
varsOfField HashSet (Name era)
l (Field [Char]
n Rep era t
r Rep era s
rx Lens' s t
l2) = forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert (forall era s. V era s -> Name era
Name forall a b. (a -> b) -> a -> b
$ forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
n Rep era t
r (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era s
rx Lens' s t
l2)) HashSet (Name era)
l
varsOfField HashSet (Name era)
l (FConst Rep era t
_ t
_ Rep era s
_ Lens' s t
_) = HashSet (Name era)
l

varsOfPat :: HashSet (Name era) -> Pat era t -> HashSet (Name era)
varsOfPat :: forall era t. HashSet (Name era) -> Pat era t -> HashSet (Name era)
varsOfPat HashSet (Name era)
ans (Pat Rep era t
_ [Arg era t]
qs) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era t. HashSet (Name era) -> Arg era t -> HashSet (Name era)
varsOfArg HashSet (Name era)
ans [Arg era t]
qs

varsOfArg :: HashSet (Name era) -> Arg era t -> HashSet (Name era)
varsOfArg :: forall era t. HashSet (Name era) -> Arg era t -> HashSet (Name era)
varsOfArg HashSet (Name era)
ans (ArgPs Field era t s
f [Pat era s]
qs) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era t. HashSet (Name era) -> Pat era t -> HashSet (Name era)
varsOfPat (forall era s t.
HashSet (Name era) -> Field era s t -> HashSet (Name era)
varsOfField HashSet (Name era)
ans Field era t s
f) [Pat era s]
qs
varsOfArg HashSet (Name era)
ans (Arg Field era t s
f) = forall era s t.
HashSet (Name era) -> Field era s t -> HashSet (Name era)
varsOfField HashSet (Name era)
ans Field era t s
f

substField :: Subst era -> Field era rec fld -> Field era rec fld
substField :: forall era rec fld.
Subst era -> Field era rec fld -> Field era rec fld
substField Subst era
_ w :: Field era rec fld
w@(FConst Rep era fld
_ fld
_ Rep era rec
_ Lens' rec fld
_) = Field era rec fld
w
substField Subst era
sub w :: Field era rec fld
w@(Field [Char]
n Rep era fld
r Rep era rec
rx Lens' rec fld
l) = case forall era t. Subst era -> V era t -> Term era t
findV Subst era
sub (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
n Rep era fld
r (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era rec
rx Lens' rec fld
l)) of
  (Lit Rep era fld
rep fld
x) -> forall era t s.
Rep era t -> t -> Rep era s -> Lens' s t -> Field era s t
FConst Rep era fld
rep fld
x Rep era rec
rx Lens' rec fld
l
  (Var (V [Char]
n2 Rep era fld
r2 Access era s fld
_a2)) -> forall era t s.
Era era =>
[Char] -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field [Char]
n2 Rep era fld
r2 Rep era rec
rx Lens' rec fld
l
  Term era fld
_ -> Field era rec fld
w

substPat :: Subst era -> Pat era t -> Pat era t
substPat :: forall era t. Subst era -> Pat era t -> Pat era t
substPat Subst era
sub (Pat Rep era t
r [Arg era t]
as) = forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat Rep era t
r (forall a b. (a -> b) -> [a] -> [b]
map (forall era t. Subst era -> Arg era t -> Arg era t
substArg Subst era
sub) [Arg era t]
as)

substArg :: Subst era -> Arg era t -> Arg era t
substArg :: forall era t. Subst era -> Arg era t -> Arg era t
substArg Subst era
sub (ArgPs Field era t s
r [Pat era s]
as) = forall era t s. Field era t s -> [Pat era s] -> Arg era t
ArgPs (forall era rec fld.
Subst era -> Field era rec fld -> Field era rec fld
substField Subst era
sub Field era t s
r) (forall a b. (a -> b) -> [a] -> [b]
map (forall era t. Subst era -> Pat era t -> Pat era t
substPat Subst era
sub) [Pat era s]
as)
substArg Subst era
sub (Arg Field era t s
r) = forall era t s. Field era t s -> Arg era t
Arg (forall era rec fld.
Subst era -> Field era rec fld -> Field era rec fld
substField Subst era
sub Field era t s
r)

bindPat :: t -> Env era -> Pat era t -> Env era
bindPat :: forall t era. t -> Env era -> Pat era t -> Env era
bindPat t
t Env era
env (Pat Rep era t
_ [Arg era t]
as) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (forall t era. t -> Env era -> Arg era t -> Env era
bindArg t
t) Env era
env [Arg era t]
as

bindArg :: t -> Env era -> Arg era t -> Env era
bindArg :: forall t era. t -> Env era -> Arg era t -> Env era
bindArg t
_ Env era
env (Arg (FConst Rep era s
_ s
_ Rep era t
_ Lens' t s
_)) = Env era
env
bindArg t
t Env era
env (Arg (Field [Char]
n Rep era s
r Rep era t
rx Lens' t s
l)) = forall era t. V era t -> t -> Env era -> Env era
storeVar (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
n Rep era s
r (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era t
rx Lens' t s
l)) (t
t forall s a. s -> Getting a s a -> a
^. Lens' t s
l) Env era
env
bindArg t
t Env era
env (ArgPs (FConst Rep era s
_ s
_ Rep era t
_ Lens' t s
l2) [Pat era s]
qs) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (forall t era. t -> Env era -> Pat era t -> Env era
bindPat (t
t forall s a. s -> Getting a s a -> a
^. Lens' t s
l2)) Env era
env [Pat era s]
qs
bindArg t
t Env era
env (ArgPs (Field [Char]
n Rep era s
r Rep era t
rx Lens' t s
l) [Pat era s]
qs) =
  forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (forall t era. t -> Env era -> Pat era t -> Env era
bindPat (t
t forall s a. s -> Getting a s a -> a
^. Lens' t s
l)) (forall era t. V era t -> t -> Env era -> Env era
storeVar (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
n Rep era s
r (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era t
rx Lens' t s
l)) (t
t forall s a. s -> Getting a s a -> a
^. Lens' t s
l) Env era
env) [Pat era s]
qs

-- | Construct a Arg with sub-patterns from
--   1) Rep era s, telling what type of Arg
--   2) A variable (Term era s) with a Yes Access,
--   3) A list of sub-patterns.
--   Check that all the embedded Access have the right Lens'.
--   If not throw an error.
argP :: Rep era s -> Term era t -> [Pat era t] -> Arg era s
argP :: forall era s t. Rep era s -> Term era t -> [Pat era t] -> Arg era s
argP Rep era s
repS1 (Var (V [Char]
name Rep era t
rept (Yes Rep era s
repS2 Lens' s t
ll))) [Pat era t]
qs = case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql Rep era s
repS1 Rep era s
repS2 of
  Just s :~: s
Refl -> forall era t s. Field era t s -> [Pat era s] -> Arg era t
ArgPs (forall era t s.
Era era =>
[Char] -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field [Char]
name Rep era t
rept Rep era s
repS2 Lens' s t
ll) [Pat era t]
qs
  Maybe (s :~: s)
Nothing ->
    forall a. HasCallStack => [Char] -> a
error
      ( [[Char]] -> [Char]
unlines
          [ [Char]
"In 'argP' the given rep and lens target do not match: "
          , [Char]
"rep: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Rep era s
repS1
          , [Char]
"lens target: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Rep era s
repS2
          ]
      )
argP Rep era s
_ t :: Term era t
t@(Var V era t
_) [Pat era t]
_ = forall a. HasCallStack => [Char] -> a
error ([Char]
"argP applied to variable term with No access." forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era t
t)
argP Rep era s
_ Term era t
term [Pat era t]
_ = forall a. HasCallStack => [Char] -> a
error ([Char]
"argP can only be applied to variable terms: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era t
term)

-- | Construct an Arg from a variable (Term era s) with a Yes Access.
--   Check that the Access has the right Lens'. If not throw an error.
arg :: Rep era s -> Term era t -> Arg era s
arg :: forall era s t. Rep era s -> Term era t -> Arg era s
arg Rep era s
repS1 (Var (V [Char]
name Rep era t
rept (Yes Rep era s
repS2 Lens' s t
l))) = case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql Rep era s
repS1 Rep era s
repS2 of
  Just s :~: s
Refl -> forall era t s. Field era t s -> Arg era t
Arg (forall era t s.
Era era =>
[Char] -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field [Char]
name Rep era t
rept Rep era s
repS2 Lens' s t
l)
  Maybe (s :~: s)
Nothing ->
    forall a. HasCallStack => [Char] -> a
error
      ( [[Char]] -> [Char]
unlines
          [ [Char]
"In 'arg' the given rep and lens target do not match: "
          , [Char]
"rep: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Rep era s
repS1
          , [Char]
"lens target: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Rep era s
repS2
          ]
      )
arg Rep era s
_ t :: Term era t
t@(Var (V [Char]
_ Rep era t
_ Access era s t
No)) = forall a. HasCallStack => [Char] -> a
error ([Char]
"arg applied to variable term with No access." forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era t
t)
arg Rep era s
_ Term era t
term = forall a. HasCallStack => [Char] -> a
error ([Char]
"arg can only be applied to variable terms: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term era t
term)