{-# 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, 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
Rep era a
z

instance Eq a => FromList (Maybe a) a where
  makeFromList :: [a] -> Maybe a
makeFromList [] = Maybe a
forall a. Maybe a
Nothing
  makeFromList (a
x : [a]
_) = a -> Maybe 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 t1
z) = Rep era a
Rep era t1
z

instance (Ord k, Eq a) => FromList (Map k a) (k, a) where
  makeFromList :: [(k, a)] -> Map k a
makeFromList = [(k, a)] -> Map k a
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
  getList :: Map k a -> [(k, a)]
getList = Map k a -> [(k, a)]
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) = Rep era k -> Rep era a -> Rep era (k, a)
forall era a b. Rep era a -> Rep era b -> Rep era (a, b)
PairR Rep era k
Rep era a
k Rep era a
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 = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList
  getList :: Set a -> [a]
getList = Set a -> [a]
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
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
  HashS :: Reflect era => Term era (ScriptF era) -> Term era ScriptHash
  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 $m:⊆: :: forall {r} {era}.
Pred era
-> (forall {a}. Ord a => Term era (Set a) -> Term era (Set a) -> r)
-> ((# #) -> r)
-> r
$b:⊆: :: forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: y = Subset x y

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

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

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

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

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

pattern Word64 :: Era era => Word64 -> Term era Word64
pattern $mWord64 :: forall {r} {era}.
Era era =>
Term era Word64 -> (Word64 -> r) -> ((# #) -> r) -> r
$bWord64 :: forall era. Era era => Word64 -> Term era Word64
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 = V era t -> Term era t
forall era t. V era t -> Term era t
Var ([Char] -> Rep era t -> Access era Any t -> V era t
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
s Rep era t
r Access era Any t
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 = [Char] -> V era t
forall a. HasCallStack => [Char] -> a
error ([Char]
"Non Var in unVar: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era t -> [Char]
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) = V era field -> Term era field
forall era t. V era t -> Term era t
Var ([Char] -> Rep era field -> Access era rec field -> V era field
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
nm Rep era field
rep (Rep era rec -> Lens' rec field -> Access era rec field
forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era rec
repx (field -> f field) -> rec -> f rec
Lens' rec field
l))
fieldToTerm (FConst Rep era field
rep field
t Rep era rec
_ Lens' rec field
_) = Rep era field -> field -> Term era 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 = Lens' big t -> Rep era t -> Term era big -> Term era t
forall s t era. Lens' s t -> Rep era t -> Term era s -> Term era t
Proj (t -> f t) -> big -> f big
Lens' big t
lenz (Term era t -> Rep era t
forall era t. Era era => Term era t -> Rep era t
termRep Term era t
small) Term era big
big Term era t -> Term era t -> Pred era
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 = Direct (Term era big) -> [AnyF era big] -> Pred era
forall era s. Direct (Term era s) -> [AnyF era s] -> Pred era
Component (Term era big -> Direct (Term era big)
forall a b. a -> Either a b
Left Term era big
big) [Field era big t -> AnyF era big
forall era s t. Field era s t -> AnyF era s
AnyF ([Char]
-> Rep era t -> Rep era big -> Lens' big t -> Field era big t
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 (Term era big -> Rep era big
forall era t. Era era => Term era t -> Rep era t
termRep Term era big
big) (t -> f t) -> big -> f big
Lens' big t
lenz)]
select2 Term era t
t1 Term era big
t2 Lens' big t
_ =
  [Char] -> Pred era
forall a. HasCallStack => [Char] -> a
error ([Char]
"In (select " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
t1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era big -> [Char]
forall a. Show a => a -> [Char]
show Term era big
t2 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" lens)  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
t1 [Char] -> [Char] -> [Char]
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 Target era (a -> t)
-> RootTarget era Void a -> RootTarget era Void t
forall era r s b.
RootTarget era r (s -> b)
-> RootTarget era r s -> RootTarget era r b
:$ Term era a -> RootTarget era Void a
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 = [Char] -> (() -> t) -> RootTarget era Void (() -> t)
forall s a era. [Char] -> (s -> a) -> RootTarget era Void (s -> a)
Constr [Char]
"constTarget" (t -> () -> t
forall a b. a -> b -> a
const t
t) RootTarget era Void (() -> t) -> Term era () -> Target era t
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Rep era () -> () -> Term era ()
forall era t. Rep era t -> t -> Term era t
Lit Rep era ()
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 = [Char] -> TypeRep t -> (() -> t) -> RootTarget era t (() -> t)
forall root s a era.
[Char] -> TypeRep root -> (s -> a) -> RootTarget era root (s -> a)
Invert [Char]
"constRootTarget" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @t) (\() -> t
t) RootTarget era t (() -> t)
-> RootTarget era t () -> RootTarget era t t
forall era r s b.
RootTarget era r (s -> b)
-> RootTarget era r s -> RootTarget era r b
:$ Term era () -> SimpleGetter t () -> RootTarget era t ()
forall era t root.
Term era t -> SimpleGetter root t -> RootTarget era root t
Lensed (Rep era () -> () -> Term era ()
forall era t. Rep era t -> t -> Term era t
Lit Rep era ()
forall era. Rep era ()
UnitR ()) ((t -> ()) -> SimpleGetter t ()
forall s a. (s -> a) -> SimpleGetter s a
to (() -> t -> ()
forall a b. a -> b -> a
const ()))

emptyTarget :: Target era ()
emptyTarget :: forall era. Target era ()
emptyTarget = Term era () -> RootTarget era Void ()
forall era t. Term era t -> RootTarget era Void t
Simple (Rep era () -> () -> Term era ()
forall era t. Rep era t -> t -> Term era t
Lit Rep era ()
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 = [Char] -> (t -> Maybe t) -> RootTarget era Void (t -> Maybe t)
forall s a era. [Char] -> (s -> a) -> RootTarget era Void (s -> a)
Constr [Char]
"Just" t -> Maybe t
forall a. a -> Maybe a
Just RootTarget era Void (t -> Maybe t)
-> Term era t -> Target era (Maybe t)
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 = [Char] -> (t -> t) -> RootTarget era Void (t -> t)
forall s a era. [Char] -> (s -> a) -> RootTarget era Void (s -> a)
Constr [Char]
"id" t -> t
forall a. a -> a
id RootTarget era Void (t -> t) -> Term era t -> Target era t
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 = [Char]
-> (t -> Gen (Maybe t)) -> RootTarget era Void (t -> Gen (Maybe t))
forall s a era. [Char] -> (s -> a) -> RootTarget era Void (s -> a)
Constr [Char]
"maybeTarget" t -> Gen (Maybe t)
forall {a}. a -> Gen (Maybe a)
genMaybe
  where
    genMaybe :: a -> Gen (Maybe a)
genMaybe a
x = [Gen (Maybe a)] -> Gen (Maybe a)
forall a. HasCallStack => [Gen a] -> Gen a
oneof [Maybe a -> Gen (Maybe a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe a
forall a. Maybe a
Nothing, Maybe a -> Gen (Maybe a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Maybe a
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 = [Char] -> ([x] -> Set x) -> RootTarget era Void ([x] -> Set x)
forall s a era. [Char] -> (s -> a) -> RootTarget era Void (s -> a)
Constr [Char]
"FromList" [x] -> Set x
forall a. Ord a => [a] -> Set a
Set.fromList RootTarget era Void ([x] -> Set x)
-> Term era [x] -> Target era (Set x)
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 = [Char] -> (Set x -> [x]) -> RootTarget era Void (Set x -> [x])
forall s a era. [Char] -> (s -> a) -> RootTarget era Void (s -> a)
Constr [Char]
"toList" Set x -> [x]
forall a. Set a -> [a]
Set.toList RootTarget era Void (Set x -> [x])
-> Term era (Set x) -> Target era [x]
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 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
sep [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (t -> [Char]) -> [Char] -> [t] -> [Char]
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) = Rep era t -> t -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Map a b) -> [Char]
forall a. Show a => a -> [Char]
show Term era (Map a b)
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Rng Term era (Map a b)
x) = [Char]
"(Rng " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Map a b) -> [Char]
forall a. Show a => a -> [Char]
show Term era (Map a b)
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Elems Term era (Map a b)
x) = [Char]
"(Elems " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Map a b) -> [Char]
forall a. Show a => a -> [Char]
show Term era (Map a b)
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (ProjM Lens' b t
_ Rep era t
r Term era (Map a b)
t) = [Char]
"(ProjM " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Rep era t -> [Char]
forall a. Show a => a -> [Char]
show Rep era t
r [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Map a b) -> [Char]
forall a. Show a => a -> [Char]
show Term era (Map a b)
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (ProjS Lens' b t
_ Rep era t
r Term era (Set b)
t) = [Char]
"(ProjS " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Rep era t -> [Char]
forall a. Show a => a -> [Char]
show Rep era t
r [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Set b) -> [Char]
forall a. Show a => a -> [Char]
show Term era (Set b)
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Proj Lens' b t
_ Rep era t
r Term era b
t) = [Char]
"(Proj " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Rep era t -> [Char]
forall a. Show a => a -> [Char]
show Rep era t
r [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era b -> [Char]
forall a. Show a => a -> [Char]
show Term era b
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Delta Term era Coin
x) = [Char]
"(Delta " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era Coin -> [Char]
forall a. Show a => a -> [Char]
show Term era Coin
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Negate Term era DeltaCoin
x) = [Char]
"(Negate " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era DeltaCoin -> [Char]
forall a. Show a => a -> [Char]
show Term era DeltaCoin
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Restrict Term era (Set a)
r Term era (Map a b)
t) = [Char]
"(Restrict " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Set a) -> [Char]
forall a. Show a => a -> [Char]
show Term era (Set a)
r [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Map a b) -> [Char]
forall a. Show a => a -> [Char]
show Term era (Map a b)
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (HashS Term era (ScriptF era)
r) = [Char]
"(HashS " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (ScriptF era) -> [Char]
forall a. Show a => a -> [Char]
show Term era (ScriptF era)
r [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (HashD Term era (Data era)
r) = [Char]
"(HashD " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Data era) -> [Char]
forall a. Show a => a -> [Char]
show Term era (Data era)
r [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Pair Term era a
r Term era b
t) = [Char]
"(Pair " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era a -> [Char]
forall a. Show a => a -> [Char]
show Term era a
r [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era b -> [Char]
forall a. Show a => a -> [Char]
show Term era b
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  showList :: [Term era t] -> [Char] -> [Char]
showList [Term era t]
xs [Char]
ans = [[Char]] -> [Char]
unlines ([Char]
ans [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: (Term era t -> [Char]) -> [Term era t] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Term era t -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Map a c) -> [Char]
forall a. Show a => a -> [Char]
show Term era (Map a c)
t
  show (SumList Term era [c]
t) = [Char]
"sum " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era [c] -> [Char]
forall a. Show a => a -> [Char]
show Term era [c]
t
  show (One Term era c
t) = Term era c -> [Char]
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", Rep era c -> [Char]
forall a. Show a => a -> [Char]
show Rep era c
c, Term era x -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Rep era c -> [Char]
forall a. Show a => a -> [Char]
show Rep era c
crep [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Map a x) -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Size -> [Char]
forall a. Show a => a -> [Char]
show Size
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era Size -> [Char]
forall a. Show a => a -> [Char]
show Term era Size
t
  show (Sized Term era Size
n Term era t
t) = [Char]
"Sized " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era Size -> [Char]
forall a. Show a => a -> [Char]
show Term era Size
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
t
  show (Term era a
x :=: Term era a
y) = Term era a -> [Char]
forall a. Show a => a -> [Char]
show Term era a
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" :=: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era a -> [Char]
forall a. Show a => a -> [Char]
show Term era a
y
  show (Subset Term era (Set a)
x Term era (Set a)
y) = Term era (Set a) -> [Char]
forall a. Show a => a -> [Char]
show Term era (Set a)
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" ⊆  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Set a) -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Set a) -> [Char]
forall a. Show a => a -> [Char]
show Term era (Set a)
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Set a) -> [Char]
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 (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Direct c -> [Char]
forall a. Show a => a -> [Char]
show Direct c
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
") " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era c -> [Char]
forall a. Show a => a -> [Char]
show Term era c
c [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ OrdCond -> [Char]
forall a. Show a => a -> [Char]
show OrdCond
cond [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Sum era c -> [Char]) -> [Char] -> [Sum era c] -> [Char]
forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL Sum era c -> [Char]
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 (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ c -> [Char]
forall a. Show a => a -> [Char]
show c
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
") " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era c -> [Char]
forall a. Show a => a -> [Char]
show Term era c
c [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ OrdCond -> [Char]
forall a. Show a => a -> [Char]
show OrdCond
cond [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Sum era c -> [Char]) -> [Char] -> [Sum era c] -> [Char]
forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL Sum era c -> [Char]
forall a. Show a => a -> [Char]
show [Char]
" + " [Sum era c]
m
  show (Random Term era t
x) = [Char]
"Random " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
x
  show (Component Direct (Term era t)
t [AnyF era t]
ws) = [Char]
"Component (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Direct (Term era t) -> [Char]
forall a. Show a => a -> [Char]
show Direct (Term era t)
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
") " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [AnyF era t] -> [Char]
forall a. Show a => a -> [Char]
show [AnyF era t]
ws
  show (CanFollow Term era n
x Term era n
y) = [Char]
"CanFollow " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era n -> [Char]
forall a. Show a => a -> [Char]
show Term era n
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era n -> [Char]
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 (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Direct (Term era a) -> [Char]
forall a. Show a => a -> [Char]
show Direct (Term era a)
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
") " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Set a) -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era a -> [Char]
forall a. Show a => a -> [Char]
show Term era a
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Set a) -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era k -> [Char]
forall a. Show a => a -> [Char]
show Term era k
k [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era v -> [Char]
forall a. Show a => a -> [Char]
show Term era v
v [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Direct (Term era (Map k v)) -> [Char]
forall a. Show a => a -> [Char]
show Direct (Term era (Map k v))
m [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Term era t
x :<-: RootTarget era r t
y) = Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" :<-: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RootTarget era r t -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RootTarget era r (Gen t) -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era fs -> [Char]
forall a. Show a => a -> [Char]
show Term era fs
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" [" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Term era t -> [Char]) -> [Char] -> [Term era t] -> [Char]
forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL Term era t -> [Char]
forall a. Show a => a -> [Char]
show [Char]
", " [Term era t]
xs [Char] -> [Char] -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era Size -> [Char]
forall a. Show a => a -> [Char]
show Term era Size
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era [t] -> [Char]
forall a. Show a => a -> [Char]
show Term era [t]
term) [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: ((Int, Target era t, [Pred era]) -> [Char])
-> [(Int, Target era t, [Pred era])] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Target era t, [Pred era]) -> [Char]
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]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RootTarget era r t -> [Char]
forall era r t. RootTarget era r t -> [Char]
showAllTarget RootTarget era r t
target [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RootTarget era r t -> [Char]
forall era t r. RootTarget era r t -> [Char]
showT RootTarget era r t
target [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" | " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (t -> [Char]) -> [Char] -> [t] -> [Char]
forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL t -> [Char]
forall a. Show a => a -> [Char]
show [Char]
", " [t]
ps [Char] -> [Char] -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
term) [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: (((Int, RootTarget era t t, [Pred era]) -> [Char])
-> [(Int, RootTarget era t t, [Pred era])] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (Int, RootTarget era t t, [Pred era]) -> [Char]
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]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RootTarget era r t -> [Char]
forall era r t. RootTarget era r t -> [Char]
showAllTarget RootTarget era r t
target [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RootTarget era r t -> [Char]
forall era t r. RootTarget era r t -> [Char]
showT RootTarget era r t
target [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" | " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (t -> [Char]) -> [Char] -> [t] -> [Char]
forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL t -> [Char]
forall a. Show a => a -> [Char]
show [Char]
", " [t]
ps [Char] -> [Char] -> [Char]
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", Term era Size -> [Char]
forall a. Show a => a -> [Char]
show Term era Size
s, Term era fs -> [Char]
forall a. Show a => a -> [Char]
show Term era fs
term]
      , [Char]
"forall (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Pat era t -> [Char]
forall a. Show a => a -> [Char]
show Pat era t
pat [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" | " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Pred era -> [Char]) -> [Char] -> [Pred era] -> [Char]
forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL Pred era -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Maybe t) -> [Char]
forall a. Show a => a -> [Char]
show Term era (Maybe t)
term [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RootTarget era r t -> [Char]
forall era r t. RootTarget era r t -> [Char]
showAllTarget RootTarget era r t
target [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" | " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Pred era -> [Char]) -> [Char] -> [Pred era] -> [Char]
forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL Pred era -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Map k v) -> [Char]
forall a. Show a => a -> [Char]
show Term era (Map k v)
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era (Map k v) -> [Char]
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 (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RootTarget era r Bool -> [Char]
forall a. Show a => a -> [Char]
show RootTarget era r Bool
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
") (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Pred era -> [Char]
forall a. Show a => a -> [Char]
show Pred era
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
") (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Pred era -> [Char]
forall a. Show a => a -> [Char]
show Pred era
y [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  show (Before Term era a
x Term era b
y) = [Char]
"Before " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era a -> [Char]
forall a. Show a => a -> [Char]
show Term era a
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era b -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era Size -> [Char]
forall a. Show a => a -> [Char]
show Term era Size
sz [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era [t] -> [Char]
forall a. Show a => a -> [Char]
show Term era [t]
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RootTarget era t t -> [Char]
forall a. Show a => a -> [Char]
show RootTarget era t t
tar [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Pred era -> [Char]) -> [Char] -> [Pred era] -> [Char]
forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL Pred era -> [Char]
forall a. Show a => a -> [Char]
show [Char]
", " [Pred era]
ps [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  showList :: [Pred era] -> [Char] -> [Char]
showList [Pred era]
xs [Char]
ans = [[Char]] -> [Char]
unlines ([Char]
ans [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: ((Pred era -> [Char]) -> [Pred era] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Pred era -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Name era -> [Char]) -> [Char] -> [Name era] -> [Char]
forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL Name era -> [Char]
forall a. Show a => a -> [Char]
show [Char]
" " (HashSet (Name era) -> [Name era]
forall a. HashSet a -> [a]
HashSet.toList (HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget HashSet (Name era)
forall a. HashSet a
HashSet.empty RootTarget era r t
tar)) [Char] -> [Char] -> [Char]
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) = Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
x
  show (Lensed Term era t
x SimpleGetter r t
_) = Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
x
  show (Partial Term era t
x r -> Maybe t
_) = Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
x
  show (RootTarget era r (a -> t)
f :$ RootTarget era r a
x) = [Char]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RootTarget era r (a -> t) -> [Char]
forall a. Show a => a -> [Char]
show RootTarget era r (a -> t)
f [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" :$ " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Any (RootTarget era r) -> [Char])
-> [Char] -> [Any (RootTarget era r)] -> [Char]
forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL Any (RootTarget era r) -> [Char]
pp [Char]
" :$ " (RootTarget era r a -> [Any (RootTarget era r)]
forall era r t. RootTarget era r t -> [Any (RootTarget era r)]
args RootTarget era r a
x) [Char] -> [Char] -> [Char]
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) = RootTarget era r i -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RootTarget era root2 t -> [Char]
forall a. Show a => a -> [Char]
show RootTarget era root2 t
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" lens)"
  show (Mask RootTarget era r t
x) = RootTarget era r t -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ PDoc -> [Char]
forall a. Show a => a -> [Char]
show PDoc
y [Char] -> [Char] -> [Char]
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) = Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
x
showT (Lensed Term era t
x SimpleGetter r t
_) = Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
x
showT (Partial Term era t
x r -> Maybe t
_) = Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
x
showT (RootTarget era r (a -> t)
f :$ RootTarget era r a
x) = [Char]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RootTarget era r (a -> t) -> [Char]
forall era t r. RootTarget era r t -> [Char]
showT RootTarget era r (a -> t)
f [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Any (RootTarget era r) -> [Char])
-> [Char] -> [Any (RootTarget era r)] -> [Char]
forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL Any (RootTarget era r) -> [Char]
pp [Char]
" " (RootTarget era r a -> [Any (RootTarget era r)]
forall era r t. RootTarget era r t -> [Any (RootTarget era r)]
args RootTarget era r a
x) [Char] -> [Char] -> [Char]
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) = RootTarget era r i -> [Char]
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RootTarget era root2 t -> [Char]
forall era t r. RootTarget era r t -> [Char]
showT RootTarget era root2 t
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
showT (Mask RootTarget era r t
x) = RootTarget era r t -> [Char]
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
_) = PDoc -> [Char]
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) = RootTarget era r (a -> t) -> Any (RootTarget era r)
forall {k} (t :: k -> *) (i :: k). t i -> Any t
Univ.Any RootTarget era r (a -> t)
x Any (RootTarget era r)
-> [Any (RootTarget era r)] -> [Any (RootTarget era r)]
forall a. a -> [a] -> [a]
: RootTarget era r a -> [Any (RootTarget era r)]
forall era r t. RootTarget era r t -> [Any (RootTarget era r)]
args RootTarget era r a
xs
args RootTarget era r t
other = [RootTarget era r t -> Any (RootTarget era r)
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 = RootTarget era r t -> [(Text, PDoc)] -> PDoc
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 = RootTarget era r (a -> t) -> [(Text, PDoc)] -> PDoc
forall era r t. RootTarget era r t -> [(Text, PDoc)] -> PDoc
targetRecord RootTarget era r (a -> t)
ts (RootTarget era r a -> (Text, PDoc)
forall era r t. RootTarget era r t -> (Text, PDoc)
targetPair RootTarget era r a
t (Text, PDoc) -> [(Text, PDoc)] -> [(Text, PDoc)]
forall a. a -> [a] -> [a]
: [(Text, PDoc)]
xs)
targetRecord (Simple Term era t
e) [] = [Char] -> PDoc
forall a. [Char] -> Doc a
ppString (Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
e)
targetRecord (Lensed Term era t
e SimpleGetter r t
_) [] = [Char] -> PDoc
forall a. [Char] -> Doc a
ppString (Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
e)
targetRecord (Partial Term era t
e r -> Maybe t
_) [] = [Char] -> PDoc
forall a. [Char] -> Doc a
ppString (Term era t -> [Char]
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 = RootTarget era root2 t -> [(Text, PDoc)] -> PDoc
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 = RootTarget era r t -> [(Text, PDoc)] -> PDoc
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 (RootTarget era r t -> Text
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 ((Char -> Char) -> [Char] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower [Char]
cs [Char] -> [Char] -> [Char]
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 (Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
term)
nameOf (Lensed Term era t
term SimpleGetter r t
_) = [Char] -> Text
pack (Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
term)
nameOf (Partial Term era t
term r -> Maybe t
_) = [Char] -> Text
pack (Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
term)
nameOf (RootTarget era r (a -> t)
x :$ RootTarget era r a
_) = RootTarget era r (a -> t) -> Text
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 ((Char -> Char) -> [Char] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower [Char]
cs [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"T")
nameOf (Shift RootTarget era root2 t
x Lens' r root2
_) = RootTarget era root2 t -> Text
forall era r t. RootTarget era r t -> Text
nameOf RootTarget era root2 t
x
nameOf (Mask RootTarget era r t
x) = RootTarget era r t -> Text
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 (PDoc -> [Char]
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, [Char] -> PDoc
forall a. [Char] -> Doc a
ppString (Rep era t -> [Char]
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, [Char] -> PDoc
forall a. [Char] -> Doc a
ppString (Rep era t -> [Char]
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, [Char] -> PDoc
forall a. [Char] -> Doc a
ppString (Rep era t -> [Char]
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 (PDoc -> [Char]
forall a. Show a => a -> [Char]
show PDoc
newname), [Char] -> PDoc
forall a. [Char] -> Doc a
ppString (Rep era t -> [Char]
forall a. Show a => a -> [Char]
show Rep era t
rep))
targetPair RootTarget era r t
x = (RootTarget era r t -> Text
forall era r t. RootTarget era r t -> Text
nameOf RootTarget era r t
x, RootTarget era r t -> [(Text, PDoc)] -> PDoc
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
_) -> Name era -> HashSet (Name era) -> HashSet (Name era)
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert (V era t -> Name era
forall era t. V era t -> Name era
Name V era t
v) HashSet (Name era)
ans
  Dom Term era (Map a b)
x -> HashSet (Name era) -> Term era (Map a b) -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era (Map a b) -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era (Map a b) -> HashSet (Name era)
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) -> HashSet (Name era) -> Term era (Map a b) -> HashSet (Name era)
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) -> HashSet (Name era) -> Term era (Set b) -> HashSet (Name era)
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) -> HashSet (Name era) -> Term era b -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era Coin -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era DeltaCoin -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era (Map a b) -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era (Set a) -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era (ScriptF era) -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era (Data era) -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era b -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era a -> HashSet (Name era)
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 = HashSet (Name era) -> Term era t -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
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) -> HashSet (Name era) -> RootTarget era r a -> HashSet (Name era)
forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget (HashSet (Name era)
-> RootTarget era r (a -> t) -> HashSet (Name era)
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) -> HashSet (Name era) -> Term era t -> HashSet (Name era)
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
_) -> HashSet (Name era) -> Term era t -> HashSet (Name era)
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
_) -> HashSet (Name era) -> Term era t -> HashSet (Name era)
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
_) -> HashSet (Name era) -> RootTarget era root2 t -> HashSet (Name era)
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) -> HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
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
_) -> HashSet (Name era) -> Term era t -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era Size -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era t -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era Size -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era a -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era a -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era (Set a) -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era (Set a) -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era (Set a) -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era (Set a) -> HashSet (Name era)
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 -> (HashSet (Name era) -> Sum era c -> HashSet (Name era))
-> HashSet (Name era) -> [Sum era c] -> HashSet (Name era)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' HashSet (Name era) -> Sum era c -> HashSet (Name era)
forall era r. HashSet (Name era) -> Sum era r -> HashSet (Name era)
varsOfSum (HashSet (Name era) -> Term era c -> HashSet (Name era)
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 -> (HashSet (Name era) -> Sum era c -> HashSet (Name era))
-> HashSet (Name era) -> [Sum era c] -> HashSet (Name era)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' HashSet (Name era) -> Sum era c -> HashSet (Name era)
forall era r. HashSet (Name era) -> Sum era r -> HashSet (Name era)
varsOfSum (HashSet (Name era) -> Term era c -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era t -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era t -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm ((HashSet (Name era) -> AnyF era t -> HashSet (Name era))
-> HashSet (Name era) -> [AnyF era t] -> HashSet (Name era)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' HashSet (Name era) -> AnyF era t -> HashSet (Name era)
forall z. HashSet (Name era) -> AnyF era z -> HashSet (Name era)
varsOfComponent HashSet (Name era)
ans [AnyF era t]
cs) (Direct (Term era t) -> Term era t
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)) = Name era -> HashSet (Name era) -> HashSet (Name era)
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert (V era t -> Name era
forall era t. V era t -> Name era
Name (V era t -> Name era) -> V era t -> Name era
forall a b. (a -> b) -> a -> b
$ [Char] -> Rep era t -> Access era z t -> V era t
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
n Rep era t
r (Rep era z -> Lens' z t -> Access era z t
forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era z
rx (t -> f t) -> z -> f z
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 -> HashSet (Name era) -> Term era n -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era n -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era (Set a) -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era a -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
ans (Direct (Term era a) -> Term era a
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 -> HashSet (Name era) -> Term era (Set a) -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era a -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era (Map k v) -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era v -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era k -> HashSet (Name era)
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) (Direct (Term era (Map k v)) -> Term era (Map k v)
forall a. Direct a -> a
direct Direct (Term era (Map k v))
m)
  Term era t
a :<-: RootTarget era r t
b -> HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget (HashSet (Name era) -> Term era t -> HashSet (Name era)
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 -> HashSet (Name era)
-> RootTarget era r (Gen t) -> HashSet (Name era)
forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget (HashSet (Name era) -> Term era t -> HashSet (Name era)
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 -> (HashSet (Name era) -> Term era t -> HashSet (Name era))
-> HashSet (Name era) -> [Term era t] -> HashSet (Name era)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' HashSet (Name era) -> Term era t -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era fs -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era Size -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era [t] -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era)
-> [(Int, Target era t, [Pred era])] -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era t -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era)
-> [(Int, RootTarget era t t, [Pred era])] -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era Size -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era fs -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era)
-> [(Pat era t, [Pred era])] -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era (Maybe t) -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era)
-> [(RootTarget era r t, [Pred era])] -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era (Map k v) -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era (Map k v) -> HashSet (Name era)
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 -> HashSet (Name era) -> RootTarget era r Bool -> HashSet (Name era)
forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget (HashSet (Name era) -> Pred era -> HashSet (Name era)
forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred (HashSet (Name era) -> Pred era -> HashSet (Name era)
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 -> HashSet (Name era) -> Term era b -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era a -> HashSet (Name era)
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 -> HashSet (Name era) -> HashSet (Name era) -> HashSet (Name era)
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 = HashSet (Name era) -> Term era Size -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm (HashSet (Name era) -> Term era [t] -> HashSet (Name era)
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 = HashSet (Name era) -> RootTarget era t t -> HashSet (Name era)
forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget HashSet (Name era)
forall a. HashSet a
HashSet.empty RootTarget era t t
tar
      pvs :: HashSet (Name era)
pvs = (HashSet (Name era) -> Pred era -> HashSet (Name era))
-> HashSet (Name era) -> [Pred era] -> HashSet (Name era)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' HashSet (Name era) -> Pred era -> HashSet (Name era)
forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred HashSet (Name era)
forall a. HashSet a
HashSet.empty [Pred era]
ps
      others :: HashSet (Name era)
others = HashSet (Name era) -> HashSet (Name era) -> HashSet (Name era)
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) = HashSet (Name era)
-> [(Int, RootTarget era r t2, [Pred era])] -> HashSet (Name era)
forall era r t2.
Era era =>
HashSet (Name era)
-> [(Int, RootTarget era r t2, [Pred era])] -> HashSet (Name era)
varsOfTrips (HashSet (Name era)
-> RootTarget era r t2 -> [Pred era] -> HashSet (Name era)
forall {era} {t :: * -> *} {r} {t}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 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 =
      HashSet (Name era) -> HashSet (Name era) -> HashSet (Name era)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.union
        ( HashSet (Name era) -> HashSet (Name era) -> HashSet (Name era)
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.difference
            ((HashSet (Name era) -> Pred era -> HashSet (Name era))
-> HashSet (Name era) -> t (Pred era) -> HashSet (Name era)
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' HashSet (Name era) -> Pred era -> HashSet (Name era)
forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred HashSet (Name era)
forall a. HashSet a
HashSet.empty t (Pred era)
preds)
            (HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget HashSet (Name era)
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) = HashSet (Name era)
-> [(RootTarget era r t2, [Pred era])] -> HashSet (Name era)
forall era r t2.
Era era =>
HashSet (Name era)
-> [(RootTarget era r t2, [Pred era])] -> HashSet (Name era)
varsOfPairs (HashSet (Name era)
-> RootTarget era r t2 -> [Pred era] -> HashSet (Name era)
forall {era} {t :: * -> *} {r} {t}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 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 =
      HashSet (Name era) -> HashSet (Name era) -> HashSet (Name era)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.union
        ( HashSet (Name era) -> HashSet (Name era) -> HashSet (Name era)
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.difference
            ((HashSet (Name era) -> Pred era -> HashSet (Name era))
-> HashSet (Name era) -> t (Pred era) -> HashSet (Name era)
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' HashSet (Name era) -> Pred era -> HashSet (Name era)
forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred HashSet (Name era)
forall a. HashSet a
HashSet.empty t (Pred era)
preds)
            (HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget HashSet (Name era)
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) = HashSet (Name era)
-> [(Pat era t2, [Pred era])] -> HashSet (Name era)
forall era t2.
Era era =>
HashSet (Name era)
-> [(Pat era t2, [Pred era])] -> HashSet (Name era)
varsOfPats (HashSet (Name era)
-> Pat era t2 -> [Pred era] -> HashSet (Name era)
forall {era} {t :: * -> *} {t}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 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 =
      HashSet (Name era) -> HashSet (Name era) -> HashSet (Name era)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.union
        ( HashSet (Name era) -> HashSet (Name era) -> HashSet (Name era)
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.difference
            ((HashSet (Name era) -> Pred era -> HashSet (Name era))
-> HashSet (Name era) -> t (Pred era) -> HashSet (Name era)
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' HashSet (Name era) -> Pred era -> HashSet (Name era)
forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred HashSet (Name era)
forall a. HashSet a
HashSet.empty t (Pred era)
preds)
            (HashSet (Name era) -> Pat era t -> HashSet (Name era)
forall era t. HashSet (Name era) -> Pat era t -> HashSet (Name era)
varsOfPat HashSet (Name era)
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) = HashSet (Name era) -> Term era (Map a r) -> HashSet (Name era)
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) = HashSet (Name era) -> Term era [r] -> HashSet (Name era)
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) = HashSet (Name era) -> Term era r -> HashSet (Name era)
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) = HashSet (Name era) -> Term era x -> HashSet (Name era)
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) = HashSet (Name era) -> Term era (Map a x) -> HashSet (Name era)
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 = (Int -> Sum era c) -> [Int] -> [Sum era c]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> Term era c -> Sum era c
forall era c. Term era c -> Sum era c
One (V era c -> Term era c
forall era t. V era t -> Term era t
Var ([Char] -> Rep era c -> Access era s c -> V era c
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V ([Char]
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"." [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
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 = (Int -> Sum era c) -> [Int] -> [Sum era c]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> Lens' x c -> Rep era c -> Term era x -> Sum era c
forall s c era. Lens' s c -> Rep era c -> Term era s -> Sum era c
ProjOne (c -> f c) -> x -> f x
Lens' x c
l Rep era c
rep (V era x -> Term era x
forall era t. V era t -> Term era t
Var ([Char] -> Rep era x -> Access era s x -> V era x
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V ([Char]
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"." [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
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]
_ = [Char] -> [Sum era c]
forall a. HasCallStack => [Char] -> a
error ([Char]
"Bad Sum in expandSum: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Sum era c -> [Char]
forall a. Show a => a -> [Char]
show Sum era c
x)

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

pad :: Int -> String -> String
pad :: Int -> [Char] -> [Char]
pad Int
n [Char]
x = [Char]
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Char] -> Int
forall a. [a] -> Int
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
_) = Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" :: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Rep era t -> [Char]
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) = Map [Char] (SubstElem era) -> Subst era
forall era. Map [Char] (SubstElem era) -> Subst era
Subst ([Char]
-> SubstElem era
-> Map [Char] (SubstElem era)
-> Map [Char] (SubstElem era)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert [Char]
nm (Rep era t -> Term era t -> Access era s t -> SubstElem era
forall era s a.
Rep era s -> Term era s -> Access era a 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 ((([Char], SubstElem era) -> [Char])
-> [([Char], SubstElem era)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char], SubstElem era) -> [Char]
forall {era}. ([Char], SubstElem era) -> [Char]
f (Map [Char] (SubstElem era) -> [([Char], SubstElem era)]
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 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" -> " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
t

emptySubst :: Subst era
emptySubst :: forall era. Subst era
emptySubst = Map [Char] (SubstElem era) -> Subst era
forall era. Map [Char] (SubstElem era) -> Subst era
Subst Map [Char] (SubstElem era)
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 = (Typed (Env era) -> [Char] -> SubstElem era -> Typed (Env era))
-> Typed (Env era) -> Map [Char] (SubstElem era) -> Typed (Env era)
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' Typed (Env era) -> [Char] -> SubstElem era -> Typed (Env era)
forall {era}.
Typed (Env era) -> [Char] -> SubstElem era -> Typed (Env era)
accum (Env era -> Typed (Env era)
forall a. a -> Typed a
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
      Env era -> Typed (Env era)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env era -> Typed (Env era)) -> Env era -> Typed (Env era)
forall a b. (a -> b) -> a -> b
$ Map [Char] (Payload era) -> Env era
forall era. Map [Char] (Payload era) -> Env era
Env (Map [Char] (Payload era) -> Env era)
-> Map [Char] (Payload era) -> Env era
forall a b. (a -> b) -> a -> b
$ [Char]
-> Payload era
-> Map [Char] (Payload era)
-> Map [Char] (Payload era)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert [Char]
key (Rep era t -> t -> Access era s t -> Payload era
forall era t s. Rep era t -> t -> Access era s t -> 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
_) = [[Char]] -> Typed (Env era)
forall a. [[Char]] -> Typed a
failT [[Char]
"Not Literal expr in substToEnv: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era t -> [Char]
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) = Map [Char] (SubstElem era) -> Subst era
forall era. Map [Char] (SubstElem era) -> Subst era
Subst ((Payload era -> SubstElem era)
-> Map [Char] (Payload era) -> Map [Char] (SubstElem era)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Payload era -> SubstElem era
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) = Rep era t -> Term era t -> Access era s t -> SubstElem era
forall era s a.
Rep era s -> Term era s -> Access era a s -> SubstElem era
SubstElem Rep era t
rep (Rep era t -> t -> Term era t
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 [Char] -> Map [Char] (SubstElem era) -> Maybe (SubstElem era)
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 -> V era t -> Term era t
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 Rep era t -> Rep era t -> Maybe (t :~: t)
forall i j. Rep era i -> Rep era j -> Maybe (i :~: j)
forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql Rep era t
rep1 Rep era t
rep2 of
    Just t :~: t
Refl -> Term era t
Term era t
term
    Maybe (t :~: t)
Nothing ->
      [Char] -> Term era t
forall a. HasCallStack => [Char] -> a
error
        ( [Char]
"In findV, we found: "
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
n1
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", but the types did not match. "
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Rep era t -> [Char]
forall a. Show a => a -> [Char]
show Rep era t
rep1
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" =/= "
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Rep era t -> [Char]
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) = Map [Char] (SubstElem era) -> Subst era
forall era. Map [Char] (SubstElem era) -> Subst era
Subst (([Char]
 -> SubstElem era
 -> Map [Char] (SubstElem era)
 -> Map [Char] (SubstElem era))
-> Map [Char] (SubstElem era)
-> Map [Char] (SubstElem era)
-> Map [Char] (SubstElem era)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey' [Char]
-> SubstElem era
-> Map [Char] (SubstElem era)
-> Map [Char] (SubstElem era)
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 = Map [Char] (SubstElem era) -> Subst era
forall era. Map [Char] (SubstElem era) -> Subst era
Subst ([Char]
-> SubstElem era
-> Map [Char] (SubstElem era)
-> Map [Char] (SubstElem era)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert [Char]
n (Rep era t -> Term era t -> Access era s t -> SubstElem era
forall era s a.
Rep era s -> Term era s -> Access era a s -> SubstElem era
SubstElem Rep era t
r Term era t
expr Access era s t
access) Map [Char] (SubstElem era)
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 = Map [Char] (SubstElem era) -> Subst era
forall era. Map [Char] (SubstElem era) -> Subst era
Subst ((Map [Char] (SubstElem era)
 -> Name era -> Map [Char] (SubstElem era))
-> Map [Char] (SubstElem era)
-> HashSet (Name era)
-> Map [Char] (SubstElem era)
forall a b. (a -> b -> a) -> a -> HashSet b -> a
HashSet.foldl' Map [Char] (SubstElem era)
-> Name era -> Map [Char] (SubstElem era)
accum Map [Char] (SubstElem era)
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)) = [Char]
-> SubstElem era
-> Map [Char] (SubstElem era)
-> Map [Char] (SubstElem era)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert [Char]
n (Rep era t -> Term era t -> Access era s t -> SubstElem era
forall era s a.
Rep era s -> Term era s -> Access era a s -> SubstElem era
SubstElem Rep era t
r (V era t -> Term era t
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ V era t -> [Char]
forall a. Show a => a -> [Char]
show V era t
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
y [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

itemsToSubst :: [SubItem era] -> Subst era
itemsToSubst :: forall era. [SubItem era] -> Subst era
itemsToSubst [SubItem era]
ss = Map [Char] (SubstElem era) -> Subst era
forall era. Map [Char] (SubstElem era) -> Subst era
Subst ((SubItem era
 -> Map [Char] (SubstElem era) -> Map [Char] (SubstElem era))
-> Map [Char] (SubstElem era)
-> [SubItem era]
-> Map [Char] (SubstElem era)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
List.foldr SubItem era
-> Map [Char] (SubstElem era) -> Map [Char] (SubstElem era)
forall era.
SubItem era
-> Map [Char] (SubstElem era) -> Map [Char] (SubstElem era)
accum Map [Char] (SubstElem era)
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 = [Char]
-> SubstElem era
-> Map [Char] (SubstElem era)
-> Map [Char] (SubstElem era)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert [Char]
nm (Rep era t -> Term era t -> Access era s t -> SubstElem era
forall era s a.
Rep era s -> Term era s -> Access era a 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) = Subst era -> V era t -> Term era t
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) = Rep era t -> t -> Term era t
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) = Term era (Map a b) -> Term era (Set a)
forall s era a. Ord s => Term era (Map s a) -> Term era (Set s)
Dom (Subst era -> Term era (Map a b) -> Term era (Map a b)
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) = Term era (Map a b) -> Term era (Set b)
forall s a era.
(Ord s, Ord a) =>
Term era (Map s a) -> Term era (Set a)
Rng (Subst era -> Term era (Map a b) -> Term era (Map a b)
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) = Term era (Map a b) -> Term era [b]
forall s a era. (Ord s, Eq a) => Term era (Map s a) -> Term era [a]
Elems (Subst era -> Term era (Map a b) -> Term era (Map a b)
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) = Lens' b t -> Rep era t -> Term era (Map a b) -> Term era (Map a t)
forall s a t era.
Ord s =>
Lens' a t -> Rep era t -> Term era (Map s a) -> Term era (Map s t)
ProjM (t -> f t) -> b -> f b
Lens' b t
l Rep era t
r (Subst era -> Term era (Map a b) -> Term era (Map a b)
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) = Lens' b t -> Rep era t -> Term era (Set b) -> Term era (Set t)
forall s a era.
(Ord s, Ord a) =>
Lens' s a -> Rep era a -> Term era (Set s) -> Term era (Set a)
ProjS (t -> f t) -> b -> f b
Lens' b t
l Rep era t
r (Subst era -> Term era (Set b) -> Term era (Set b)
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) = Lens' b t -> Rep era t -> Term era b -> Term era t
forall s t era. Lens' s t -> Rep era t -> Term era s -> Term era t
Proj (t -> f t) -> b -> f b
Lens' b t
l Rep era t
r (Subst era -> Term era b -> Term era b
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) = Term era Coin -> Term era DeltaCoin
forall era. Term era Coin -> Term era DeltaCoin
Delta (Subst era -> Term era Coin -> Term era Coin
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) = Term era DeltaCoin -> Term era DeltaCoin
forall era. Term era DeltaCoin -> Term era DeltaCoin
Negate (Subst era -> Term era DeltaCoin -> Term era DeltaCoin
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) = Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
forall s era a.
Ord s =>
Term era (Set s) -> Term era (Map s a) -> Term era (Map s a)
Restrict (Subst era -> Term era (Set a) -> Term era (Set a)
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Set a)
s) (Subst era -> Term era (Map a b) -> Term era (Map a b)
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) = Term era (ScriptF era) -> Term era ScriptHash
forall era.
Reflect era =>
Term era (ScriptF era) -> Term era ScriptHash
HashS (Subst era -> Term era (ScriptF era) -> Term era (ScriptF era)
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) = Term era (Data era) -> Term era (SafeHash EraIndependentData)
forall era.
Era era =>
Term era (Data era) -> Term era (SafeHash EraIndependentData)
HashD (Subst era -> Term era (Data era) -> Term era (Data era)
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) = Term era a -> Term era b -> Term era (a, b)
forall era s a. Term era s -> Term era a -> Term era (s, a)
Pair (Subst era -> Term era a -> Term era a
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era a
a) (Subst era -> Term era b -> Term era b
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) = Size -> Term era Size -> Pred era
forall era. Size -> Term era Size -> Pred era
MetaSize Size
a (Subst era -> Term era Size -> Term era Size
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) = Term era Size -> Term era t -> Pred era
forall s era. Sizeable s => Term era Size -> Term era s -> Pred era
Sized (Subst era -> Term era Size -> Term era Size
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era Size
a) (Subst era -> Term era t -> Term era t
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) = Subst era -> Term era a -> Term era a
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era a
a Term era a -> Term era a -> Pred era
forall s era. Eq s => Term era s -> Term era s -> Pred era
:=: Subst era -> Term era a -> Term era a
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) = Subst era -> Term era (Set a) -> Term era (Set a)
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Set a)
a Term era (Set a) -> Term era (Set a) -> Pred era
forall s era.
Ord s =>
Term era (Set s) -> Term era (Set s) -> Pred era
`Subset` Subst era -> Term era (Set a) -> Term era (Set 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 (Disjoint Term era (Set a)
a Term era (Set a)
b) = Term era (Set a) -> Term era (Set a) -> Pred era
forall s era.
Ord s =>
Term era (Set s) -> Term era (Set s) -> Pred era
Disjoint (Subst era -> Term era (Set a) -> Term era (Set a)
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Set a)
a) (Subst era -> Term era (Set a) -> Term era (Set 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) = Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
forall era s.
(Era era, Adds s) =>
Direct s -> Term era s -> OrdCond -> [Sum era s] -> Pred era
SumsTo Direct c
i (Subst era -> Term era c -> Term era c
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era c
a) OrdCond
cond ((Sum era c -> Sum era c) -> [Sum era c] -> [Sum era c]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era -> Sum era c -> Sum era c
forall era t. Subst era -> Sum era t -> Sum era t
substSum Subst era
sub) [Sum era c]
b)
substPred Subst era
sub (SumSplit c
i Term era c
a OrdCond
cond [Sum era c]
b) = c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
forall era s.
(Era era, Adds s) =>
s -> Term era s -> OrdCond -> [Sum era s] -> Pred era
SumSplit c
i (Subst era -> Term era c -> Term era c
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era c
a) OrdCond
cond ((Sum era c -> Sum era c) -> [Sum era c] -> [Sum era c]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era -> Sum era c -> Sum era c
forall era t. Subst era -> Sum era t -> Sum era t
substSum Subst era
sub) [Sum era c]
b)
substPred Subst era
sub (Random Term era t
x) = Term era t -> Pred era
forall era s. Term era s -> Pred era
Random (Subst era -> Term era t -> Term era t
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 -> Direct (Term era t) -> [AnyF era t] -> Pred era
forall era s. Direct (Term era s) -> [AnyF era s] -> Pred era
Component (Term era t -> Direct (Term era t)
forall a b. a -> Either a b
Left (Subst era -> Term era t -> Term era t
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 (AnyF era t -> AnyF era t) -> [AnyF era t] -> [AnyF era t]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [AnyF era t]
cs)
  Right Term era t
x -> Direct (Term era t) -> [AnyF era t] -> Pred era
forall era s. Direct (Term era s) -> [AnyF era s] -> Pred era
Component (Term era t -> Direct (Term era t)
forall a b. b -> Either a b
Right (Subst era -> Term era t -> Term era t
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 (AnyF era t -> AnyF era t) -> [AnyF era t] -> [AnyF era t]
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)) = Field era t t -> AnyF era t
forall era s t. Field era s t -> AnyF era s
AnyF (Field era t t -> AnyF era t) -> Field era t t -> AnyF era t
forall a b. (a -> b) -> a -> b
$ case Subst era -> V era t -> Term era t
forall era t. Subst era -> V era t -> Term era t
findV Subst era
sub ([Char] -> Rep era t -> Access era t t -> V era t
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
n Rep era t
r (Rep era t -> Lens' t t -> Access era t t
forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era t
rx (t -> f t) -> t -> f t
Lens' t t
l)) of
      (Lit Rep era t
rep t
x) -> Rep era t -> t -> Rep era t -> Lens' t t -> Field era t t
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 (t -> f t) -> t -> f t
Lens' t t
l
      (Var (V [Char]
n2 Rep era t
r2 Access era s t
_a2)) -> [Char] -> Rep era t -> Rep era t -> Lens' t t -> Field era t t
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 (t -> f t) -> t -> f t
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) = Term era n -> Term era n -> Pred era
forall s era. Count s => Term era s -> Term era s -> Pred era
CanFollow (Subst era -> Term era n -> Term era n
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era n
a) (Subst era -> Term era n -> Term era n
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 -> Direct (Term era a) -> Term era (Set a) -> Pred era
forall s era.
Ord s =>
Direct (Term era s) -> Term era (Set s) -> Pred era
Member (Term era a -> Direct (Term era a)
forall a b. a -> Either a b
Left (Subst era -> Term era a -> Term era a
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era a
a)) (Subst era -> Term era (Set a) -> Term era (Set 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 -> Direct (Term era a) -> Term era (Set a) -> Pred era
forall s era.
Ord s =>
Direct (Term era s) -> Term era (Set s) -> Pred era
Member (Term era a -> Direct (Term era a)
forall a b. b -> Either a b
Right (Subst era -> Term era a -> Term era a
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era a
a)) (Subst era -> Term era (Set a) -> Term era (Set 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) = Term era a -> Term era (Set a) -> Pred era
forall s era. Ord s => Term era s -> Term era (Set s) -> Pred era
NotMember (Subst era -> Term era a -> Term era a
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era a
a) (Subst era -> Term era (Set a) -> Term era (Set 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 -> Term era k -> Term era v -> Direct (Term era (Map k v)) -> Pred era
forall s a era.
(Ord s, Eq a, Ord a) =>
Term era s -> Term era a -> Direct (Term era (Map s a)) -> Pred era
MapMember (Subst era -> Term era k -> Term era k
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era k
k) (Subst era -> Term era v -> Term era v
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era v
v) (Term era (Map k v) -> Direct (Term era (Map k v))
forall a b. a -> Either a b
Left (Subst era -> Term era (Map k v) -> Term era (Map k v)
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 -> Term era k -> Term era v -> Direct (Term era (Map k v)) -> Pred era
forall s a era.
(Ord s, Eq a, Ord a) =>
Term era s -> Term era a -> Direct (Term era (Map s a)) -> Pred era
MapMember (Subst era -> Term era k -> Term era k
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era k
k) (Subst era -> Term era v -> Term era v
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era v
v) (Term era (Map k v) -> Direct (Term era (Map k v))
forall a b. b -> Either a b
Right (Subst era -> Term era (Map k v) -> Term era (Map k v)
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) = Subst era -> Term era t -> Term era t
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
a Term era t -> RootTarget era r t -> Pred era
forall era s a. Term era s -> RootTarget era a s -> Pred era
:<-: Subst era -> RootTarget era r t -> RootTarget era r t
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) = Term era t -> RootTarget era r (Gen t) -> Pred era
forall era s a. Term era s -> RootTarget era a (Gen s) -> Pred era
GenFrom (Subst era -> Term era t -> Term era t
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
a) (Subst era -> RootTarget era r (Gen t) -> RootTarget era r (Gen t)
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) = Term era fs -> [Term era t] -> Pred era
forall s a era.
FromList s a =>
Term era s -> [Term era a] -> Pred era
List (Subst era -> Term era fs -> Term era fs
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era fs
a) ((Term era t -> Term era t) -> [Term era t] -> [Term era t]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era -> Term era t -> Term era t
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) = Term era Size
-> Term era [t] -> [(Int, Target era t, [Pred era])] -> Pred era
forall era s.
(Era era, Eq s) =>
Term era Size
-> Term era [s] -> [(Int, Target era s, [Pred era])] -> Pred era
Choose (Subst era -> Term era Size -> Term era Size
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era Size
sz) (Subst era -> Term era [t] -> Term era [t]
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era [t]
t) (((Int, Target era t, [Pred era])
 -> (Int, Target era t, [Pred era]))
-> [(Int, Target era t, [Pred era])]
-> [(Int, Target era t, [Pred era])]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era
-> (Int, Target era t, [Pred era])
-> (Int, Target era t, [Pred era])
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, (Pred era -> Pred era) -> [Pred era] -> [Pred era]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era -> Pred era -> Pred era
forall era. Subst era -> Pred era -> Pred era
substPred (Subst era -> Subst era -> Subst era
forall era. Subst era -> Subst era -> Subst era
composeSubst Subst era
sub1 Subst era
sub0)) [Pred era]
ps)
      where
        sub1 :: Subst era
sub1 = RootTarget era r t -> Subst era
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) = Term era t -> [(Int, RootTarget era t t, [Pred era])] -> Pred era
forall s era.
(Eq s, Era era) =>
Term era s -> [(Int, RootTarget era s s, [Pred era])] -> Pred era
Oneof (Subst era -> Term era t -> Term era t
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
t) (((Int, RootTarget era t t, [Pred era])
 -> (Int, RootTarget era t t, [Pred era]))
-> [(Int, RootTarget era t t, [Pred era])]
-> [(Int, RootTarget era t t, [Pred era])]
forall a b. (a -> b) -> [a] -> [b]
map (\(Int
i, RootTarget era t t
tr, [Pred era]
p) -> (Int
i, Subst era -> RootTarget era t t -> RootTarget era t t
forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
sub RootTarget era t t
tr, (Pred era -> Pred era) -> [Pred era] -> [Pred era]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era -> Pred era -> Pred era
forall era. Subst era -> Pred era -> Pred era
substPred Subst era
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) =
  Term era Size -> Term era fs -> Pat era t -> [Pred era] -> Pred era
forall era s a.
(Era era, FromList s a, Eq a) =>
Term era Size -> Term era s -> Pat era a -> [Pred era] -> Pred era
ForEach
    (Subst era -> Term era Size -> Term era Size
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era Size
sz)
    (Subst era -> Term era fs -> Term era fs
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era fs
t)
    Pat era t
pat
    ((Pred era -> Pred era) -> [Pred era] -> [Pred era]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era -> Pred era -> Pred era
forall era. Subst era -> Pred era -> Pred era
substPred Subst era
sub1) [Pred era]
ps)
  where
    sub1 :: Subst era
sub1 = Subst era -> Subst era -> Subst era
forall era. Subst era -> Subst era -> Subst era
composeSubst (Pat era t -> Subst era
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) = Term era (Maybe t) -> RootTarget era r t -> [Pred era] -> Pred era
forall s era a.
(Era era, Typeable s) =>
Term era (Maybe a) -> RootTarget era s a -> [Pred era] -> Pred era
Maybe (Subst era -> Term era (Maybe t) -> Term era (Maybe t)
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 ((Pred era -> Pred era) -> [Pred era] -> [Pred era]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era -> Pred era -> Pred era
forall era. Subst era -> Pred era -> Pred era
substPred (Subst era -> Subst era -> Subst era
forall era. Subst era -> Subst era -> Subst era
composeSubst Subst era
sub1 Subst era
sub)) [Pred era]
ps)
  where
    sub1 :: Subst era
sub1 = RootTarget era r t -> Subst era
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) = Term era (Map k v) -> Term era (Map k v) -> Pred era
forall s a era.
(Ord s, Eq a, Ord a) =>
Term era (Map s a) -> Term era (Map s a) -> Pred era
SubMap (Subst era -> Term era (Map k v) -> Term era (Map k v)
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era (Map k v)
a) (Subst era -> Term era (Map k v) -> Term era (Map k v)
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) = RootTarget era r Bool -> Pred era -> Pred era -> Pred era
forall era s.
RootTarget era s Bool -> Pred era -> Pred era -> Pred era
If (Subst era -> RootTarget era r Bool -> RootTarget era r Bool
forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
sub RootTarget era r Bool
t) (Subst era -> Pred era -> Pred era
forall era. Subst era -> Pred era -> Pred era
substPred Subst era
sub Pred era
x) (Subst era -> Pred era -> Pred era
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) = Term era a -> Term era b -> Pred era
forall era s a. Term era s -> Term era a -> Pred era
Before (Subst era -> Term era a -> Term era a
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era a
a) (Subst era -> Term era b -> Term era b
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) =
  Term era Size
-> Term era [t] -> RootTarget era t t -> [Pred era] -> Pred era
forall era s.
(Era era, Eq s) =>
Term era Size
-> Term era [s] -> RootTarget era s s -> [Pred era] -> Pred era
ListWhere (Subst era -> Term era Size -> Term era Size
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era Size
sz) (Subst era -> Term era [t] -> Term era [t]
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era [t]
t) RootTarget era t t
tar ((Pred era -> Pred era) -> [Pred era] -> [Pred era]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era -> Pred era -> Pred era
forall era. Subst era -> Pred era -> Pred era
substPred Subst era
newsub) [Pred era]
ps)
  where
    newsub :: Subst era
newsub = Subst era -> Subst era -> Subst era
forall era. Subst era -> Subst era -> Subst era
composeSubst (RootTarget era t t -> Subst era
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 = Subst era -> Pred era -> Pred era
forall era. Subst era -> Pred era -> Pred era
substPred Subst era
sub Pred era
oldpred
      freevars :: HashSet (Name era)
freevars = HashSet (Name era) -> Pred era -> HashSet (Name era)
forall era. HashSet (Name era) -> Pred era -> HashSet (Name era)
varsOfPred HashSet (Name era)
forall a. HashSet a
HashSet.empty Pred era
newpred
   in case HashSet (Name era) -> Bool
forall a. HashSet a -> Bool
HashSet.null HashSet (Name era)
freevars of
        Bool
False -> Pred era
newpred
        Bool
True ->
          [Char] -> Pred era
forall a. HasCallStack => [Char] -> a
error
            ( [[Char]] -> [Char]
unlines
                [ [Char]
"When solving: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Pred era -> [Char]
forall a. Show a => a -> [Char]
show Pred era
oldpred [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
","
                , [Char]
"we applied the Subst from earlier stages, and we obtain the pred:"
                , [Char]
"   " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Pred era -> [Char]
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 = HashSet (Name era) -> Subst era
forall era. HashSet (Name era) -> Subst era
substFromNames (HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
forall era r t.
HashSet (Name era) -> RootTarget era r t -> HashSet (Name era)
varsOfTarget HashSet (Name era)
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 = HashSet (Name era) -> Subst era
forall era. HashSet (Name era) -> Subst era
substFromNames (HashSet (Name era) -> Pat era t -> HashSet (Name era)
forall era t. HashSet (Name era) -> Pat era t -> HashSet (Name era)
varsOfPat HashSet (Name era)
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) = Term era (Map a t) -> Sum era t
forall c era s. Adds c => Term era (Map s c) -> Sum era c
SumMap (Subst era -> Term era (Map a t) -> Term era (Map a t)
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) = Term era [t] -> Sum era t
forall c era. Adds c => Term era [c] -> Sum era c
SumList (Subst era -> Term era [t] -> Term era [t]
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) = Term era t -> Sum era t
forall era c. Term era c -> Sum era c
One (Subst era -> Term era t -> Term era t
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) = Lens' x t -> Rep era t -> Term era x -> Sum era t
forall s c era. Lens' s c -> Rep era c -> Term era s -> Sum era c
ProjOne (t -> f t) -> x -> f x
Lens' x t
l Rep era t
r (Subst era -> Term era x -> Term era x
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) = Rep era t -> Lens' x t -> Term era (Map a x) -> Sum era t
forall s c a era.
Adds c =>
Rep era c -> Lens' s c -> Term era (Map a s) -> Sum era c
ProjMap Rep era t
crep (t -> f t) -> x -> f x
Lens' x t
l (Subst era -> Term era (Map a x) -> Term era (Map a x)
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) = Term era t -> RootTarget era Void t
forall era t. Term era t -> RootTarget era Void t
Simple (Subst era -> Term era t -> Term era t
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) = Term era t -> SimpleGetter r t -> RootTarget era r t
forall era t root.
Term era t -> SimpleGetter root t -> RootTarget era root t
Lensed (Subst era -> Term era t -> Term era t
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
e) Getting r r t
SimpleGetter r t
l
substTarget Subst era
sub (Partial Term era t
e r -> Maybe t
l) = Term era t -> (r -> Maybe t) -> RootTarget era r t
forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial (Subst era -> Term era t -> Term era t
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) = Subst era -> RootTarget era r (a -> t) -> RootTarget era r (a -> t)
forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
sub RootTarget era r (a -> t)
a RootTarget era r (a -> t)
-> RootTarget era r a -> RootTarget era r t
forall era r s b.
RootTarget era r (s -> b)
-> RootTarget era r s -> RootTarget era r b
:$ Subst era -> RootTarget era r a -> RootTarget era r a
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) = [Char] -> (a -> b) -> RootTarget era Void (a -> b)
forall s a era. [Char] -> (s -> a) -> RootTarget era Void (s -> a)
Constr [Char]
n a -> b
f
substTarget Subst era
_ (Invert [Char]
x TypeRep r
l a -> b
f) = [Char] -> TypeRep r -> (a -> b) -> RootTarget era r (a -> b)
forall root s a era.
[Char] -> TypeRep root -> (s -> a) -> RootTarget era root (s -> a)
Invert [Char]
x TypeRep r
l a -> b
f
substTarget Subst era
sub (Shift RootTarget era root2 t
x Lens' r root2
l) = RootTarget era root2 t -> Lens' r root2 -> RootTarget era r t
forall era s a root1.
RootTarget era s a -> Lens' root1 s -> RootTarget era root1 a
Shift (Subst era -> RootTarget era root2 t -> RootTarget era root2 t
forall era r t.
Subst era -> RootTarget era r t -> RootTarget era r t
substTarget Subst era
sub RootTarget era root2 t
x) (root2 -> f root2) -> r -> f r
Lens' r root2
l
substTarget Subst era
sub (Mask RootTarget era r t
x) = RootTarget era r t -> RootTarget era Void t
forall era s a. RootTarget era s a -> RootTarget era Void a
Mask (Subst era -> RootTarget era r t -> RootTarget era r t
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) = Term era t -> PDoc -> Lens' r t -> RootTarget era r t
forall era t root.
Term era t -> PDoc -> Lens' root t -> RootTarget era root t
Virtual (Subst era -> Term era t -> Term era t
forall era t. Subst era -> Term era t -> Term era t
substTerm Subst era
sub Term era t
x) PDoc
y (t -> f t) -> r -> f r
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) = t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
x
simplify (Dom (Lit Rep era (Map a b)
_ Map a b
x)) = t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map a b -> Set a
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)) = Term era t -> Typed t
forall era t. Term era t -> Typed t
simplify (Term era (Map a b) -> Term era (Set a)
forall s era a. Ord s => Term era (Map s a) -> Term era (Set s)
Dom Term era (Map a b)
t)
simplify (Dom Term era (Map a b)
x) = do
  Map a b
m <- Term era (Map a b) -> Typed (Map a b)
forall era t. Term era t -> Typed t
simplify Term era (Map a b)
x
  t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map a b -> Set a
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)) = t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([b] -> Set b
forall a. Ord a => [a] -> Set a
Set.fromList (Map a b -> [b]
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))) = t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([t] -> Set t
forall a. Ord a => [a] -> Set a
Set.fromList (Map a t -> [t]
forall k a. Map k a -> [a]
Map.elems ((b -> t) -> Map a b -> Map a t
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\b
x -> b
x b -> Getting t b t -> t
forall s a. s -> Getting a s a -> a
^. Getting t b t
Lens' b t
l) Map a b
m)))
simplify (Rng Term era (Map a b)
x) = do
  Map a b
m <- Term era (Map a b) -> Typed (Map a b)
forall era t. Term era t -> Typed t
simplify Term era (Map a b)
x
  t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([b] -> Set b
forall a. Ord a => [a] -> Set a
Set.fromList (Map a b -> [b]
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)) = t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map a b -> [b]
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))) = t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map a t -> [t]
forall k a. Map k a -> [a]
Map.elems ((b -> t) -> Map a b -> Map a t
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\b
x -> b
x b -> Getting t b t -> t
forall s a. s -> Getting a s a -> a
^. Getting t b t
Lens' b t
l) Map a b
m))
simplify (Elems Term era (Map a b)
x) = do
  Map a b
m <- Term era (Map a b) -> Typed (Map a b)
forall era t. Term era t -> Typed t
simplify Term era (Map a b)
x
  t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map a b -> [b]
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)) = t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((b -> t) -> Map a b -> Map a t
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\b
z -> b
z b -> Getting t b t -> t
forall s a. s -> Getting a s a -> a
^. Getting t b t
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 <- Term era (Map a b) -> Typed (Map a b)
forall era t. Term era t -> Typed t
simplify Term era (Map a b)
t
  t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((b -> t) -> Map a b -> Map a t
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\b
z -> b
z b -> Getting t b t -> t
forall s a. s -> Getting a s a -> a
^. Getting t b t
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)) = t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((b -> t) -> Set b -> Set t
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\b
z -> b
z b -> Getting t b t -> t
forall s a. s -> Getting a s a -> a
^. Getting t b t
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 <- Term era (Set b) -> Typed (Set b)
forall era t. Term era t -> Typed t
simplify Term era (Set b)
t
  t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((b -> t) -> Set b -> Set t
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\b
z -> b
z b -> Getting t b t -> t
forall s a. s -> Getting a s a -> a
^. Getting t b t
Lens' b t
l) Set b
s)
simplify (Proj Lens' b t
l Rep era t
_ (Lit Rep era b
_ b
x)) = t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b
x b -> Getting t b t -> t
forall s a. s -> Getting a s a -> a
^. Getting t b t
Lens' b t
l)
simplify (Proj Lens' b t
l Rep era t
_ Term era b
t) = do
  b
s <- Term era b -> Typed b
forall era t. Term era t -> Typed t
simplify Term era b
t
  t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b
s b -> Getting t b t -> t
forall s a. s -> Getting a s a -> a
^. Getting t b t
Lens' b t
l)
simplify (Delta (Lit Rep era Coin
CoinR (Coin Integer
n))) = t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> DeltaCoin
DeltaCoin Integer
n)
simplify (Negate (Lit Rep era DeltaCoin
DeltaCoinR (DeltaCoin Integer
n))) = t -> Typed t
forall a. a -> Typed a
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 <- Term era (Set a) -> Typed (Set a)
forall era t. Term era t -> Typed t
simplify Term era (Set a)
s
  Map a b
mv <- Term era (Map a b) -> Typed (Map a b)
forall era t. Term era t -> Typed t
simplify Term era (Map a b)
m
  t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map a b -> Set a -> Map a b
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 <- Term era (ScriptF era) -> Typed (ScriptF era)
forall era t. Term era t -> Typed t
simplify Term era (ScriptF era)
s
  t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Script era -> ScriptHash
forall era. EraScript era => Script era -> ScriptHash
hashScript Script era
sv)
simplify (HashD Term era (Data era)
s) = do
  Data era
sv <- Term era (Data era) -> Typed (Data era)
forall era t. Term era t -> Typed t
simplify Term era (Data era)
s
  t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Data era -> SafeHash EraIndependentData
forall era. Data era -> SafeHash EraIndependentData
hashData Data era
sv)
simplify (Pair Term era a
s Term era b
m) = do
  a
sv <- Term era a -> Typed a
forall era t. Term era t -> Typed t
simplify Term era a
s
  b
mv <- Term era b -> Typed b
forall era t. Term era t -> Typed t
simplify Term era b
m
  t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
sv, b
mv)
simplify Term era t
x = [[Char]] -> Typed t
forall a. [[Char]] -> Typed a
failT [[Char]
"Can't simplify term: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
x [Char] -> [Char] -> [Char]
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)) = c -> Typed c
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure c
x
simplifySum (One (Delta (Lit Rep era Coin
CoinR (Coin Integer
n)))) = c -> Typed c
forall a. a -> Typed a
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)))) = c -> Typed c
forall a. a -> Typed a
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)) = c -> Typed c
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (x
x x -> Getting c x c -> c
forall s a. s -> Getting a s a -> a
^. Getting c x c
Lens' x c
l)
simplifySum (SumMap (Lit Rep era (Map a c)
_ Map a c
m)) = c -> Typed c
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((c -> c -> c) -> c -> Map a c -> c
forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' c -> c -> c
forall x. Adds x => x -> x -> x
add c
forall x. Adds x => x
zero Map a c
m)
simplifySum (SumList (Lit Rep era [c]
_ [c]
m)) = c -> Typed c
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((c -> c -> c) -> c -> [c] -> c
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' c -> c -> c
forall x. Adds x => x -> x -> x
add c
forall x. Adds x => x
zero [c]
m)
simplifySum (ProjMap Rep era c
_ Lens' x c
l (Lit Rep era (Map a x)
_ Map a x
m)) = c -> Typed c
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((c -> x -> c) -> c -> Map a x -> c
forall b a. (b -> a -> b) -> b -> Map a a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\c
ans x
x -> c -> c -> c
forall x. Adds x => x -> x -> x
add c
ans (x
x x -> Getting c x c -> c
forall s a. s -> Getting a s a -> a
^. Getting c x c
Lens' x c
l)) c
forall x. Adds x => x
zero Map a x
m)
simplifySum Sum era c
x = [[Char]] -> Typed c
forall a. [[Char]] -> Typed a
failT [[Char]
"Can't simplify Sum: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Sum era c -> [Char]
forall a. Show a => a -> [Char]
show Sum era c
x [Char] -> [Char] -> [Char]
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) = t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
a -> b
f
simplifyTarget (Shift RootTarget era root2 t
x Lens' root root2
_) = RootTarget era root2 t -> Typed t
forall era t root. RootTarget era root t -> Typed t
simplifyTarget RootTarget era root2 t
x
simplifyTarget (Mask RootTarget era r t
x) = RootTarget era r t -> Typed t
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
_) = Term era t -> Typed t
forall era t. Term era t -> Typed t
simplify Term era t
x
simplifyTarget (Simple Term era t
t) = Term era t -> Typed t
forall era t. Term era t -> Typed t
simplify Term era t
t
simplifyTarget (Lensed Term era t
t SimpleGetter root t
_) = Term era t -> Typed t
forall era t. Term era t -> Typed t
simplify Term era t
t
simplifyTarget (Partial Term era t
t root -> Maybe t
_) = Term era t -> Typed t
forall era t. Term era t -> Typed t
simplify Term era t
t
simplifyTarget (Constr [Char]
_ a -> b
f) = t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
a -> b
f
simplifyTarget (RootTarget era root (a -> t)
x :$ RootTarget era root a
y) = do
  a -> t
f <- RootTarget era root (a -> t) -> Typed (a -> t)
forall era t root. RootTarget era root t -> Typed t
simplifyTarget RootTarget era root (a -> t)
x
  a
z <- RootTarget era root a -> Typed a
forall era t root. RootTarget era root t -> Typed t
simplifyTarget RootTarget era root a
y
  t -> Typed t
forall a. a -> Typed a
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) = t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
x
runTerm Env era
env (Dom Term era (Map a b)
x) = Map a b -> t
Map a b -> Set a
forall k a. Map k a -> Set k
Map.keysSet (Map a b -> t) -> Typed (Map a b) -> Typed t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env era -> Term era (Map a b) -> Typed (Map a 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) = [b] -> t
[b] -> Set b
forall a. Ord a => [a] -> Set a
Set.fromList ([b] -> t) -> (Map a b -> [b]) -> Map a b -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a b -> [b]
forall k a. Map k a -> [a]
Map.elems (Map a b -> t) -> Typed (Map a b) -> Typed t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env era -> Term era (Map a b) -> Typed (Map a 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) = Map a b -> t
Map a b -> [b]
forall k a. Map k a -> [a]
Map.elems (Map a b -> t) -> Typed (Map a b) -> Typed t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env era -> Term era (Map a b) -> Typed (Map a 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) = V era t -> Env era -> Typed t
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 <- Env era -> Term era (Map a b) -> Typed (Map a b)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map a b)
x
  t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((b -> t) -> Map a b -> Map a t
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\b
z -> b
z b -> Getting t b t -> t
forall s a. s -> Getting a s a -> a
^. Getting t b t
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 <- Env era -> Term era (Set b) -> Typed (Set b)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set b)
x
  t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((b -> t) -> Set b -> Set t
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\b
z -> b
z b -> Getting t b t -> t
forall s a. s -> Getting a s a -> a
^. Getting t b t
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 <- Env era -> Term era b -> Typed b
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era b
x
  t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b
m b -> Getting t b t -> t
forall s a. s -> Getting a s a -> a
^. Getting t b t
Lens' b t
l)
runTerm Env era
env (Delta Term era Coin
x) = do
  Coin Integer
n <- Env era -> Term era Coin -> Typed Coin
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era Coin
x
  t -> Typed t
forall a. a -> Typed a
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 <- Env era -> Term era DeltaCoin -> Typed DeltaCoin
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era DeltaCoin
x
  t -> Typed t
forall a. a -> Typed a
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 <- Env era -> Term era (Set a) -> Typed (Set a)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set a)
s
  Map a b
mv <- Env era -> Term era (Map a b) -> Typed (Map a b)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map a b)
m
  t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map a b -> Set a -> Map a b
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 <- Env era -> Term era (Data era) -> Typed (Data era)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Data era)
x
  t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Data era -> SafeHash EraIndependentData
forall era. Data era -> SafeHash EraIndependentData
hashData Data era
s)
runTerm Env era
env (HashS Term era (ScriptF era)
x) = do
  ScriptF Proof era
_ Script era
s <- Env era -> Term era (ScriptF era) -> Typed (ScriptF era)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (ScriptF era)
x
  t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Script era -> ScriptHash
forall era. EraScript era => Script era -> ScriptHash
hashScript Script era
s)
runTerm Env era
env (Pair Term era a
s Term era b
m) =
  do
    a
sv <- Env era -> Term era a -> Typed a
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
s
    b
mv <- Env era -> Term era b -> Typed b
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era b
m
    t -> Typed t
forall a. a -> Typed a
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) = t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
a -> b
f
runTarget Env era
env (Simple Term era t
t) = Env era -> Term era t -> Typed 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
_) = Env era -> Term era t -> Typed 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
_) = Env era -> Term era t -> Typed 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
_) = Env era -> RootTarget era root2 t -> Typed t
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) = Env era -> RootTarget era r t -> Typed t
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
_) = Env era -> Term era t -> Typed 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) = t -> Typed t
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
a -> b
f
runTarget Env era
env (RootTarget era x (a -> t)
x :$ RootTarget era x a
y) = do
  a -> t
f <- Env era -> RootTarget era x (a -> t) -> Typed (a -> t)
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env RootTarget era x (a -> t)
x
  a
z <- Env era -> RootTarget era x a -> Typed a
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env RootTarget era x a
y
  t -> Typed t
forall a. a -> Typed a
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 = V era t -> t -> Env era -> Env era
forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v (root
root root -> Getting t root t -> t
forall s a. s -> Getting a s a -> a
^. Getting t root t
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 -> V era t -> t -> Env era -> Env era
forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v t
val Env era
env
    Maybe t
Nothing ->
      [Char] -> Env era
forall a. HasCallStack => [Char] -> a
error
        ( [Char]
"A Partial RootTarget returned Nothing: "
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ V era t -> [Char]
forall a. Show a => a -> [Char]
show V era t
v
            [Char] -> [Char] -> [Char]
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 = root -> RootTarget era root (a -> t) -> Env era -> Env era
forall era root t.
root -> RootTarget era root t -> Env era -> Env era
getTarget root
root RootTarget era root (a -> t)
x (root -> RootTarget era root a -> Env era -> Env era
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 = root2 -> RootTarget era root2 t -> Env era -> Env era
forall era root t.
root -> RootTarget era root t -> Env era -> Env era
getTarget (root
root root -> Getting root2 root root2 -> root2
forall s a. s -> Getting a s a -> a
^. Getting root2 root root2
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 = V era t -> t -> Env era -> Env era
forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v (root
root root -> Getting t root t -> t
forall s a. s -> Getting a s a -> a
^. Getting t root t
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 = Env era -> Maybe (Env era)
forall a. a -> Maybe a
Just (V era t -> t -> Env era -> Env era
forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v (root
root root -> Getting t root t -> t
forall s a. s -> Getting a s a -> a
^. Getting t root t
SimpleGetter root t
l) Env era
env)
targetMaybeEnv root
root (Virtual (Var V era t
v) PDoc
_ Lens' root t
l) Env era
env = Env era -> Maybe (Env era)
forall a. a -> Maybe a
Just (V era t -> t -> Env era -> Env era
forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v (root
root root -> Getting t root t -> t
forall s a. s -> Getting a s a -> a
^. Getting t root t
Lens' root t
l) Env era
env)
targetMaybeEnv root
root (Shift RootTarget era root2 t
x Lens' root root2
l) Env era
env = root2 -> RootTarget era root2 t -> Env era -> Maybe (Env era)
forall era root t.
root -> RootTarget era root t -> Env era -> Maybe (Env era)
targetMaybeEnv (root
root root -> Getting root2 root root2 -> root2
forall s a. s -> Getting a s a -> a
^. Getting root2 root root2
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 -> Env era -> Maybe (Env era)
forall a. a -> Maybe a
Just (V era t -> t -> Env era -> Env era
forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v t
val Env era
env)
    Maybe t
Nothing -> Maybe (Env era)
forall a. Maybe a
Nothing
targetMaybeEnv root
root (RootTarget era root (a -> t)
x :$ RootTarget era root a
y) Env era
env =
  root -> RootTarget era root a -> Env era -> Maybe (Env era)
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 Maybe (Env era) -> (Env era -> Maybe (Env era)) -> Maybe (Env era)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= root -> RootTarget era root (a -> t) -> Env era -> Maybe (Env era)
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
_ = Maybe (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 <- Env era -> Term era Size -> Typed Size
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 -> Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Typed Bool) -> Bool -> Typed Bool
forall a b. (a -> b) -> a -> b
$ Int -> Size -> Bool
runSize Int
n Size
w
    Size
_ -> Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Typed Bool) -> Bool -> Typed Bool
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 <- Env era -> Term era Size -> Typed Size
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era Size
szt
  t
t <- Env era -> Term era t -> Typed t
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era t
tt
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Typed Bool) -> Bool -> Typed Bool
forall a b. (a -> b) -> a -> b
$ Int -> Size -> Bool
runSize (t -> Int
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 <- Env era -> Term era a -> Typed a
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
x
  a
y2 <- Env era -> Term era a -> Typed a
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
y
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
x2 a -> a -> Bool
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 <- Env era -> Term era (Set a) -> Typed (Set a)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set a)
x
  Set a
y2 <- Env era -> Term era (Set a) -> Typed (Set a)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set a)
y
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set a -> Set a -> Bool
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 <- Env era -> Term era (Set a) -> Typed (Set a)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set a)
x
  Set a
y2 <- Env era -> Term era (Set a) -> Typed (Set a)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set a)
y
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set a -> Set a -> Bool
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 <- Env era -> Term era c -> Typed c
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era c
x
  [c]
is <- (Sum era c -> Typed c) -> [Sum era c] -> Typed [c]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env era -> Sum era c -> Typed c
forall era c. Env era -> Sum era c -> Typed c
runSum Env era
env) [Sum era c]
ys
  let y2 :: c
y2 = (c -> c -> c) -> c -> [c] -> c
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' c -> c -> c
forall x. Adds x => x -> x -> x
add c
forall x. Adds x => x
zero [c]
is
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OrdCond -> c -> c -> Bool
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 <- Env era -> Term era c -> Typed c
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era c
x
  [c]
is <- (Sum era c -> Typed c) -> [Sum era c] -> Typed [c]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env era -> Sum era c -> Typed c
forall era c. Env era -> Sum era c -> Typed c
runSum Env era
env) [Sum era c]
ys
  let y2 :: c
y2 = (c -> c -> c) -> c -> [c] -> c
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' c -> c -> c
forall x. Adds x => x -> x -> x
add c
forall x. Adds x => x
zero [c]
is
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OrdCond -> c -> c -> Bool
forall x. Adds x => OrdCond -> x -> x -> Bool
runOrdCondition OrdCond
cond c
x2 c
y2)
runPred Env era
_ (Random Term era t
_) = Bool -> Typed Bool
forall a. a -> Typed a
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' <- Env era -> Term era t -> Typed t
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env (Direct (Term era t) -> Term era t
forall a. Direct a -> a
direct Direct (Term era t)
t)
  [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> Typed [Bool] -> Typed Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (AnyF era t -> Typed Bool) -> [AnyF era t] -> Typed [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env era -> t -> AnyF era t -> Typed Bool
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 <- Env era -> Term era n -> Typed n
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era n
x
  n
y2 <- Env era -> Term era n -> Typed n
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era n
y
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (n -> n -> Bool
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 <- Env era -> Term era a -> Typed a
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env (Direct (Term era a) -> Term era a
forall a. Direct a -> a
direct Direct (Term era a)
x)
  Set a
y2 <- Env era -> Term era (Set a) -> Typed (Set a)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set a)
y
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Set a -> Bool
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 <- Env era -> Term era a -> Typed a
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
x
  Set a
y2 <- Env era -> Term era (Set a) -> Typed (Set a)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set a)
y
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Set a -> Bool
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' <- Env era -> Term era k -> Typed k
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era k
k
  v
v' <- Env era -> Term era v -> Typed v
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era v
v
  Map k v
m' <- Env era -> Term era (Map k v) -> Typed (Map k v)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env (Direct (Term era (Map k v)) -> Term era (Map k v)
forall a. Direct a -> a
direct Direct (Term era (Map k v))
m)
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Typed Bool) -> Bool -> Typed Bool
forall a b. (a -> b) -> a -> b
$ Map k v -> Map k v -> Bool
forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
Map.isSubmapOf (k -> v -> Map k v
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 <- Env era -> Term era t -> Typed t
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era t
x
  t
_y2 <- Env era -> RootTarget era r t -> Typed t
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env RootTarget era r t
y
  Bool -> Typed Bool
forall a. a -> Typed a
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 <- Env era -> Term era t -> Typed t
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era t
x
  Gen t
_y2 <- Env era -> RootTarget era r (Gen t) -> Typed (Gen t)
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env RootTarget era r (Gen t)
y
  Bool -> Typed Bool
forall a. a -> Typed a
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 <- Env era -> Term era fs -> Typed fs
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era fs
x
  [t]
y2 <- (Term era t -> Typed t) -> [Term era t] -> Typed [t]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env era -> Term era t -> Typed t
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env) [Term era t]
y
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (fs
x2 fs -> fs -> Bool
forall a. Eq a => a -> a -> Bool
== [t] -> fs
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 <- Env era -> Term era (Maybe t) -> Typed (Maybe t)
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 -> Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    (Just t
y) -> do
      [Bool]
ans <- (Pred era -> Typed Bool) -> [Pred era] -> Typed [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env era -> Pred era -> Typed Bool
forall era. Env era -> Pred era -> Typed Bool
runPred (RootTarget era r t -> t -> Env era -> Env era
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
      Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Bool] -> Bool
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])]
_) = Bool -> Typed Bool
forall a. a -> Typed a
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 <- fs -> [t]
forall ts a. FromList ts a => ts -> [a]
getList (fs -> [t]) -> Typed fs -> Typed [t]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env era -> Term era fs -> Typed fs
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era fs
term
  [Bool]
bs <- (t -> Typed Bool) -> [t] -> Typed [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\t
t -> Env era -> [Pred era] -> Typed Bool
forall era. Env era -> [Pred era] -> Typed Bool
runPreds (t -> Env era -> Pat era t -> Env era
forall t era. t -> Env era -> Pat era t -> Env era
bindPat t
t Env era
env Pat era t
pat) ((Pred era -> Bool) -> [Pred era] -> [Pred era]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Pred era -> Bool) -> Pred era -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pat era t -> Pred era -> Bool
forall era t. Pat era t -> Pred era -> Bool
extendableSumsTo Pat era t
pat) [Pred era]
ps)) [t]
ts
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Bool] -> Bool
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 <- Env era -> Term era (Map k v) -> Typed (Map k v)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map k v)
x
  Map k v
y2 <- Env era -> Term era (Map k v) -> Typed (Map k v)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map k v)
y
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map k v -> Map k v -> Bool
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 <- Env era -> RootTarget era r Bool -> Typed Bool
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 Env era -> Pred era -> Typed Bool
forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env Pred era
x
    else Env era -> Pred era -> Typed Bool
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
_) = Bool -> Typed Bool
forall a. a -> Typed a
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 <- Env era -> Term era t -> Typed t
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 [] = Bool -> Typed Bool
forall a. a -> Typed a
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 t -> RootTarget era t t -> Env era -> Maybe (Env era)
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 <- (Pred era -> Typed Bool) -> [Pred era] -> Typed [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env era -> Pred era -> Typed Bool
forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env2) [Pred era]
ps
          if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
qs
            then Bool -> Typed Bool
forall a. a -> Typed a
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 <- Env era -> Term era [t] -> Typed [t]
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era [t]
name
  Size
size <- Env era -> Term era Size -> Typed 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 ([t] -> Int
forall a. [a] -> Int
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 = t -> RootTarget era t t -> Env era -> Env era
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 <- (Pred era -> Typed Bool) -> [Pred era] -> Typed [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env era -> Pred era -> Typed Bool
forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env2) [Pred era]
ps
        Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
bs)
  [Bool]
bs <- (t -> Typed Bool) -> [t] -> Typed [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM t -> Typed Bool
p [t]
xs
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Typed Bool) -> Bool -> Typed Bool
forall a b. (a -> b) -> a -> b
$ Bool
sizeOK Bool -> Bool -> 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 = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList (HashSet a -> [a]
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 = HashSet a -> Bool
forall a. HashSet a -> Bool
HashSet.null (HashSet a -> HashSet a -> HashSet a
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]) =
  HashSet (Name era) -> Int
forall a. HashSet a -> Int
HashSet.size HashSet (Name era)
boundS Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& HashSet (Name era) -> HashSet (Name era) -> 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
&& HashSet (Name era) -> HashSet (Name era) -> 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 = HashSet (Name era) -> Pat era t -> HashSet (Name era)
forall era t. HashSet (Name era) -> Pat era t -> HashSet (Name era)
varsOfPat HashSet (Name era)
forall a. HashSet a
HashSet.empty Pat era t
pat
    boundS :: HashSet (Name era)
boundS = HashSet (Name era) -> Term era c -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
forall a. HashSet a
HashSet.empty Term era c
s
    boundT :: HashSet (Name era)
boundT = HashSet (Name era) -> Term era c -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
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]) =
  HashSet (Name era) -> Int
forall a. HashSet a -> Int
HashSet.size HashSet (Name era)
boundS Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& HashSet (Name era) -> HashSet (Name era) -> 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
&& HashSet (Name era) -> HashSet (Name era) -> 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 = HashSet (Name era) -> Pat era t -> HashSet (Name era)
forall era t. HashSet (Name era) -> Pat era t -> HashSet (Name era)
varsOfPat HashSet (Name era)
forall a. HashSet a
HashSet.empty Pat era t
pat
    boundS :: HashSet (Name era)
boundS = HashSet (Name era) -> Term era c -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
forall a. HashSet a
HashSet.empty Term era c
s
    boundT :: HashSet (Name era)
boundT = HashSet (Name era) -> Term era c -> HashSet (Name era)
forall era t.
HashSet (Name era) -> Term era t -> HashSet (Name era)
varsOfTerm HashSet (Name era)
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 <- (Pred era -> Typed Bool) -> [Pred era] -> Typed [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env era -> Pred era -> Typed Bool
forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env) [Pred era]
ps
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Bool] -> Bool
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 = V era t -> t -> Env era -> Env era
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 = V era t -> t -> Env era -> Env era
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
_ = [Char] -> Env era
forall a. HasCallStack => [Char] -> a
error ([Char]
"Non simple Target in bind: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RootTarget era r t -> [Char]
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' <- Env era -> Term era t -> Typed t
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env (Term era t -> Typed t) -> Term era t -> Typed t
forall a b. (a -> b) -> a -> b
$ V era t -> Term era t
forall era t. V era t -> Term era t
Var ([Char] -> Rep era t -> Access era s t -> V era t
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
n Rep era t
rt (Rep era s -> Lens' s t -> Access era s t
forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era s
rx (t -> f t) -> s -> f s
Lens' s t
l))
  With s t1
_ <- Rep era t -> Rep era t -> Typed (HasConstraint Eq (Rep era t))
forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Eq (s t))
hasEq Rep era t
rt Rep era t
rt
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Typed Bool) -> Bool -> Typed Bool
forall a b. (a -> b) -> a -> b
$ s
t s -> Getting t s t -> t
forall s a. s -> Getting a s a -> a
^. Getting t s t
Lens' s t
l t -> t -> Bool
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 t1
_ <- Rep era t -> Rep era t -> Typed (HasConstraint Eq (Rep era t))
forall era t (s :: * -> *).
Rep era t -> s t -> Typed (HasConstraint Eq (s t))
hasEq Rep era t
r Rep era t
r
  Bool -> Typed Bool
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Typed Bool) -> Bool -> Typed Bool
forall a b. (a -> b) -> a -> b
$ s
t s -> Getting t s t -> t
forall s a. s -> Getting a s a -> a
^. Getting t s t
Lens' s t
l t -> t -> Bool
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 (Term era (Map a b) -> Rep era (Map a b)
forall era t. Era era => Term era t -> Rep era t
termRep -> MapR Rep era a
r Rep era b
_)) = Rep era a -> Rep era (Set a)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era a
r
termRep (Rng (Term era (Map a b) -> Rep era (Map a b)
forall era t. Era era => Term era t -> Rep era t
termRep -> MapR Rep era a
_ Rep era b
r)) = Rep era b -> Rep era (Set b)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era b
r
termRep (Elems (Term era (Map a b) -> Rep era (Map a b)
forall era t. Era era => Term era t -> Rep era t
termRep -> MapR Rep era a
_ Rep era b
r)) = Rep era b -> Rep era [b]
forall era a. Rep era a -> Rep era [a]
ListR Rep era b
r
termRep (ProjM Lens' b t
_ Rep era t
t (Term era (Map a b) -> Rep era (Map a b)
forall era t. Era era => Term era t -> Rep era t
termRep -> MapR Rep era a
a Rep era b
_)) = Rep era a -> Rep era t -> Rep era (Map a t)
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era a
a Rep era t
t
termRep (ProjS Lens' b t
_ Rep era t
t (Term era (Set b) -> Rep era (Set b)
forall era t. Era era => Term era t -> Rep era t
termRep -> SetR Rep era a
_)) = Rep era t -> Rep era (Set t)
forall a era. Ord a => Rep era a -> Rep era (Set a)
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
_) = Rep era t
Rep era DeltaCoin
forall era. Rep era DeltaCoin
DeltaCoinR
termRep (Negate Term era DeltaCoin
_) = Rep era t
Rep era DeltaCoin
forall era. Rep era DeltaCoin
DeltaCoinR
termRep (Restrict Term era (Set a)
_ Term era (Map a b)
m) = Term era t -> Rep era t
forall era t. Era era => Term era t -> Rep era t
termRep Term era t
Term era (Map a b)
m
termRep (HashD Term era (Data era)
_) = Rep era t
Rep era (SafeHash EraIndependentData)
forall era. Era era => Rep era (SafeHash EraIndependentData)
DataHashR
termRep (HashS Term era (ScriptF era)
_) = Rep era t
Rep era ScriptHash
forall era. Era era => Rep era ScriptHash
ScriptHashR
termRep (Pair Term era a
a Term era b
b) = Rep era a -> Rep era b -> Rep era (a, b)
forall era a b. Rep era a -> Rep era b -> Rep era (a, b)
PairR (Term era a -> Rep era a
forall era t. Era era => Term era t -> Rep era t
termRep Term era a
a) (Term era b -> Rep era b
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) = (c -> c -> c) -> c -> Map a c -> c
forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' c -> c -> c
forall x. Adds x => x -> x -> x
add c
forall x. Adds x => x
zero (Map a c -> c) -> Typed (Map a c) -> Typed c
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env era -> Term era (Map a c) -> Typed (Map a c)
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) = (c -> c -> c) -> c -> [c] -> c
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' c -> c -> c
forall x. Adds x => x -> x -> x
add c
forall x. Adds x => x
zero ([c] -> c) -> Typed [c] -> Typed c
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env era -> Term era [c] -> Typed [c]
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) = Env era -> Term era c -> Typed c
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 <- Env era -> Term era x -> Typed x
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era x
t
  c -> Typed c
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (x
x x -> Getting c x c -> c
forall s a. s -> Getting a s a -> a
^. Getting c x c
Lens' x c
l)
runSum Env era
env (ProjMap Rep era c
_ Lens' x c
l Term era (Map a x)
t) = (c -> x -> c) -> c -> Map a x -> c
forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' c -> x -> c
accum c
forall x. Adds x => x
zero (Map a x -> c) -> Typed (Map a x) -> Typed c
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env era -> Term era (Map a x) -> Typed (Map a x)
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 = c -> c -> c
forall x. Adds x => x -> x -> x
add c
ans (x
x x -> Getting c x c -> c
forall s a. s -> Getting a s a -> a
^. Getting c x c
Lens' x c
l)

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 <- Env era -> Pred era -> Typed Bool
forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env Pred era
c
  ([Char], Bool, Pred era) -> Typed ([Char], Bool, Pred era)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pred era -> [Char]
forall a. Show a => a -> [Char]
show Pred era
c [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" => " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Bool -> [Char]
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 <- Typed a -> IO a
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (V era a -> Env era -> Typed a
forall era t. V era t -> Env era -> Typed t
findVar V era a
v Env era
env)
  [Char] -> IO ()
putStrLn ([Char]
nm [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Rep era a -> a -> [Char]
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 <- Typed a -> IO a
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Env era -> Term era a -> Typed a
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
term)
  [Char] -> IO ()
putStrLn (Term era a -> [Char]
forall a. Show a => a -> [Char]
show Term era a
term [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Rep era a -> a -> [Char]
forall e t. Rep e t -> t -> [Char]
format (Term era a -> Rep era a
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) = [[AnyF era t]] -> [AnyF era t]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((Arg era t -> [AnyF era t]) -> [Arg era t] -> [[AnyF era t]]
forall a b. (a -> b) -> [a] -> [b]
map (Rep era t -> Arg era t -> [AnyF era t]
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) = [Field era t s -> AnyF era t
forall era s t. Field era s t -> 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) = Field era t s -> AnyF era t
forall era s t. Field era s t -> AnyF era s
AnyF Field era t s
f AnyF era t -> [AnyF era t] -> [AnyF era t]
forall a. a -> [a] -> [a]
: (AnyF era s -> AnyF era t) -> [AnyF era s] -> [AnyF era t]
forall a b. (a -> b) -> [a] -> [b]
map (Rep era t -> Lens' t s -> AnyF era s -> AnyF era t
forall era t s. Rep era t -> Lens' t s -> AnyF era s -> AnyF era t
push Rep era t
rept (s -> f s) -> t -> f t
Lens' t s
lensx) ([[AnyF era s]] -> [AnyF era s]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((Pat era s -> [AnyF era s]) -> [Pat era s] -> [[AnyF era s]]
forall a b. (a -> b) -> [a] -> [b]
map Pat era s -> [AnyF era s]
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) = Field era t s -> AnyF era t
forall era s t. Field era s t -> AnyF era s
AnyF Field era t s
f AnyF era t -> [AnyF era t] -> [AnyF era t]
forall a. a -> [a] -> [a]
: (AnyF era s -> AnyF era t) -> [AnyF era s] -> [AnyF era t]
forall a b. (a -> b) -> [a] -> [b]
map (Rep era t -> Lens' t s -> AnyF era s -> AnyF era t
forall era t s. Rep era t -> Lens' t s -> AnyF era s -> AnyF era t
push Rep era t
rept (s -> f s) -> t -> f t
Lens' t s
lensx) ([[AnyF era s]] -> [AnyF era s]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((Pat era s -> [AnyF era s]) -> [Pat era s] -> [[AnyF era s]]
forall a b. (a -> b) -> [a] -> [b]
map Pat era s -> [AnyF era s]
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)) = Field era t t -> AnyF era t
forall era s t. Field era s t -> AnyF era s
AnyF ([Char] -> Rep era t -> Rep era t -> Lens' t t -> Field era t t
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 ((s -> f s) -> t -> f t
Lens' t s
l1 ((s -> f s) -> t -> f t)
-> ((t -> f t) -> s -> f s) -> (t -> f t) -> t -> f t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t -> f t) -> s -> f s
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)) = Field era t t -> AnyF era t
forall era s t. Field era s t -> AnyF era s
AnyF (Rep era t -> t -> Rep era t -> Lens' t t -> Field era t t
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 ((s -> f s) -> t -> f t
Lens' t s
l1 ((s -> f s) -> t -> f t)
-> ((t -> f t) -> s -> f s) -> (t -> f t) -> t -> f t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t -> f t) -> s -> f s
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 = Rep era t1 -> [Arg era t1] -> Pat era t1
forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat Rep era t1
rep [Rep era t1 -> Term era t2 -> Arg era t1
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 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Rep era t -> [Char]
forall a. Show a => a -> [Char]
show Rep era t
r [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Arg era t -> [Char]) -> [Char] -> [Arg era t] -> [Char]
forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL Arg era t -> [Char]
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
_)) = Field era t s -> [Char]
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 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" [" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Pat era s -> [Char]) -> [Char] -> [Pat era s] -> [Char]
forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL Pat era s -> [Char]
forall a. Show a => a -> [Char]
show [Char]
", " [Pat era s]
qs [Char] -> [Char] -> [Char]
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) = Field era t s -> [Char]
forall a. Show a => a -> [Char]
show Field era t s
f [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" [" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Pat era s -> [Char]) -> [Char] -> [Pat era s] -> [Char]
forall t. (t -> [Char]) -> [Char] -> [t] -> [Char]
showL Pat era s -> [Char]
forall a. Show a => a -> [Char]
show [Char]
", " [Pat era s]
qs [Char] -> [Char] -> [Char]
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) = Name era -> HashSet (Name era) -> HashSet (Name era)
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert (V era t -> Name era
forall era t. V era t -> Name era
Name (V era t -> Name era) -> V era t -> Name era
forall a b. (a -> b) -> a -> b
$ [Char] -> Rep era t -> Access era s t -> V era t
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
n Rep era t
r (Rep era s -> Lens' s t -> Access era s t
forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era s
rx (t -> f t) -> s -> f s
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) = (HashSet (Name era) -> Arg era t -> HashSet (Name era))
-> HashSet (Name era) -> [Arg era t] -> HashSet (Name era)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' HashSet (Name era) -> Arg era t -> HashSet (Name era)
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) = (HashSet (Name era) -> Pat era s -> HashSet (Name era))
-> HashSet (Name era) -> [Pat era s] -> HashSet (Name era)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' HashSet (Name era) -> Pat era s -> HashSet (Name era)
forall era t. HashSet (Name era) -> Pat era t -> HashSet (Name era)
varsOfPat (HashSet (Name era) -> Field era t s -> HashSet (Name era)
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) = HashSet (Name era) -> Field era t s -> HashSet (Name era)
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 Subst era -> V era fld -> Term era fld
forall era t. Subst era -> V era t -> Term era t
findV Subst era
sub ([Char] -> Rep era fld -> Access era rec fld -> V era fld
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
n Rep era fld
r (Rep era rec -> Lens' rec fld -> Access era rec fld
forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era rec
rx (fld -> f fld) -> rec -> f rec
Lens' rec fld
l)) of
  (Lit Rep era fld
rep fld
x) -> Rep era fld
-> fld -> Rep era rec -> Lens' rec fld -> Field era rec fld
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 (fld -> f fld) -> rec -> f rec
Lens' rec fld
l
  (Var (V [Char]
n2 Rep era fld
r2 Access era s fld
_a2)) -> [Char]
-> Rep era fld -> Rep era rec -> Lens' rec fld -> Field era rec fld
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 (fld -> f fld) -> rec -> f rec
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) = Rep era t -> [Arg era t] -> Pat era t
forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat Rep era t
r ((Arg era t -> Arg era t) -> [Arg era t] -> [Arg era t]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era -> Arg era t -> Arg era t
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) = Field era t s -> [Pat era s] -> Arg era t
forall era t s. Field era t s -> [Pat era s] -> Arg era t
ArgPs (Subst era -> Field era t s -> Field era t s
forall era rec fld.
Subst era -> Field era rec fld -> Field era rec fld
substField Subst era
sub Field era t s
r) ((Pat era s -> Pat era s) -> [Pat era s] -> [Pat era s]
forall a b. (a -> b) -> [a] -> [b]
map (Subst era -> Pat era s -> Pat era s
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) = Field era t s -> Arg era t
forall era t s. Field era t s -> Arg era t
Arg (Subst era -> Field era t s -> Field era t s
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) = (Env era -> Arg era t -> Env era)
-> Env era -> [Arg era t] -> Env era
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (t -> Env era -> Arg era t -> Env era
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)) = V era s -> s -> Env era -> Env era
forall era t. V era t -> t -> Env era -> Env era
storeVar ([Char] -> Rep era s -> Access era t s -> V era s
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
n Rep era s
r (Rep era t -> Lens' t s -> Access era t s
forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era t
rx (s -> f s) -> t -> f t
Lens' t s
l)) (t
t t -> Getting s t s -> s
forall s a. s -> Getting a s a -> a
^. Getting s t s
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) = (Env era -> Pat era s -> Env era)
-> Env era -> [Pat era s] -> Env era
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (s -> Env era -> Pat era s -> Env era
forall t era. t -> Env era -> Pat era t -> Env era
bindPat (t
t t -> Getting s t s -> s
forall s a. s -> Getting a s a -> a
^. Getting s t s
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) =
  (Env era -> Pat era s -> Env era)
-> Env era -> [Pat era s] -> Env era
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (s -> Env era -> Pat era s -> Env era
forall t era. t -> Env era -> Pat era t -> Env era
bindPat (t
t t -> Getting s t s -> s
forall s a. s -> Getting a s a -> a
^. Getting s t s
Lens' t s
l)) (V era s -> s -> Env era -> Env era
forall era t. V era t -> t -> Env era -> Env era
storeVar ([Char] -> Rep era s -> Access era t s -> V era s
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
n Rep era s
r (Rep era t -> Lens' t s -> Access era t s
forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era t
rx (s -> f s) -> t -> f t
Lens' t s
l)) (t
t t -> Getting s t s -> s
forall s a. s -> Getting a s a -> a
^. Getting s t s
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 Rep era s -> Rep era s -> Maybe (s :~: s)
forall i j. Rep era i -> Rep era j -> Maybe (i :~: j)
forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql Rep era s
repS1 Rep era s
repS2 of
  Just s :~: s
Refl -> Field era s t -> [Pat era t] -> Arg era s
forall era t s. Field era t s -> [Pat era s] -> Arg era t
ArgPs ([Char] -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
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
Rep era s
repS2 (t -> f t) -> s -> f s
(t -> f t) -> s -> f s
Lens' s t
Lens' s t
ll) [Pat era t]
qs
  Maybe (s :~: s)
Nothing ->
    [Char] -> Arg era s
forall a. HasCallStack => [Char] -> a
error
      ( [[Char]] -> [Char]
unlines
          [ [Char]
"In 'argP' the given rep and lens target do not match: "
          , [Char]
"rep: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Rep era s -> [Char]
forall a. Show a => a -> [Char]
show Rep era s
repS1
          , [Char]
"lens target: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Rep era s -> [Char]
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]
_ = [Char] -> Arg era s
forall a. HasCallStack => [Char] -> a
error ([Char]
"argP applied to variable term with No access." [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
t)
argP Rep era s
_ Term era t
term [Pat era t]
_ = [Char] -> Arg era s
forall a. HasCallStack => [Char] -> a
error ([Char]
"argP can only be applied to variable terms: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era t -> [Char]
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 Rep era s -> Rep era s -> Maybe (s :~: s)
forall i j. Rep era i -> Rep era j -> Maybe (i :~: j)
forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql Rep era s
repS1 Rep era s
repS2 of
  Just s :~: s
Refl -> Field era s t -> Arg era s
forall era t s. Field era t s -> Arg era t
Arg ([Char] -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
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
Rep era s
repS2 (t -> f t) -> s -> f s
(t -> f t) -> s -> f s
Lens' s t
Lens' s t
l)
  Maybe (s :~: s)
Nothing ->
    [Char] -> Arg era s
forall a. HasCallStack => [Char] -> a
error
      ( [[Char]] -> [Char]
unlines
          [ [Char]
"In 'arg' the given rep and lens target do not match: "
          , [Char]
"rep: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Rep era s -> [Char]
forall a. Show a => a -> [Char]
show Rep era s
repS1
          , [Char]
"lens target: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Rep era s -> [Char]
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)) = [Char] -> Arg era s
forall a. HasCallStack => [Char] -> a
error ([Char]
"arg applied to variable term with No access." [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
t)
arg Rep era s
_ Term era t
term = [Char] -> Arg era s
forall a. HasCallStack => [Char] -> a
error ([Char]
"arg can only be applied to variable terms: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term era t -> [Char]
forall a. Show a => a -> [Char]
show Term era t
term)