Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.Cardano.Ledger.Constrained.Ast

Description

The types that make up the Abstract Syntax Trees of the Language

Synopsis

class (Eq a, Eq ts) ⇒ FromList ts a | ts → a where
- makeFromList ∷ [a] → ts
- getList ∷ ts → [a]
- tsRep ∷ Rep era ts → Rep era a
type Direct a = Either a a
direct ∷ Direct 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)
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 ∷ ∀ 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 ∷ ∀ x c era. Lens' x c → Rep era c → Term era x → Sum era c
- ProjMap ∷ ∀ x c a era. Adds c ⇒ Rep era c → Lens' x c → Term era (Map a x) → Sum era c
pattern (:⊆:) ∷ ∀ era. ∀ a. Ord a ⇒ Term era (Set a) → Term era (Set a) → Pred era
pattern ExactSize ∷ Era era ⇒ Int → Term era Size
pattern AtLeast ∷ Era era ⇒ Int → Term era Size
pattern Size ∷ Era era ⇒ Size → Term era Size
pattern AtMost ∷ Era era ⇒ Int → Term era Size
pattern Range ∷ Era era ⇒ Int → Int → Term era Size
sameRng ∷ Term era Size → Maybe Int
pattern Word64 ∷ Era era ⇒ Word64 → Term era Word64
var ∷ Era era ⇒ String → Rep era t → Term era t
unVar ∷ Term era t → V era t
fieldToTerm ∷ Field era rec field → Term era field
select ∷ (Eq t, Era era) ⇒ Term era t → Term era big → Lens' big t → Pred era
select2 ∷ Era era ⇒ Term era t → Term era big → Lens' big t → Pred era
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) → 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 → RootTarget era root t
type Target era t = RootTarget era Void t
(^$) ∷ Target era (a → t) → Term era a → Target era t
constTarget ∷ t → Target era t
constRootTarget ∷ ∀ era t. Typeable t ⇒ t → RootTarget era t t
emptyTarget ∷ Target era ()
justTarget ∷ Term era t → Target era (Maybe t)
idTarget ∷ Term era t → Target era t
maybeTarget ∷ Target era (t → Gen (Maybe t))
listToSetTarget ∷ Ord x ⇒ Term era [x] → Target era (Set x)
setToListTarget ∷ Term era (Set x) → Target era [x]
showL ∷ (t → String) → [Char] → [t] → [Char]
showAllTarget ∷ RootTarget era r t → [Char]
showT ∷ ∀ era t r. RootTarget era r t → String
args ∷ RootTarget era r t → [Any (RootTarget era r)]
ppTarget ∷ RootTarget era r t → PDoc
targetRecord ∷ RootTarget era r t → [(Text, PDoc)] → PDoc
nameOf ∷ RootTarget era r t → Text
targetPair ∷ RootTarget era r t → (Text, PDoc)
varsOfTerm ∷ HashSet (Name era) → Term era t → HashSet (Name era)
vars ∷ Term era t → HashSet (Name era)
varsOfTarget ∷ HashSet (Name era) → RootTarget era r t → HashSet (Name era)
varsOfPred ∷ ∀ era. HashSet (Name era) → Pred era → HashSet (Name era)
varsOfTrips ∷ Era era ⇒ HashSet (Name era) → [(Int, RootTarget era r t2, [Pred era])] → HashSet (Name era)
varsOfPairs ∷ Era era ⇒ HashSet (Name era) → [(RootTarget era r t2, [Pred era])] → HashSet (Name era)
varsOfPats ∷ Era era ⇒ HashSet (Name era) → [(Pat era t2, [Pred era])] → HashSet (Name era)
varsOfSum ∷ HashSet (Name era) → Sum era r → HashSet (Name era)
expandSum ∷ Sum era c → [Int] → [Sum era c]
pad ∷ Int → String → String
data SubstElem era where
- SubstElem ∷ Rep era t → Term era t → Access era s t → SubstElem era
newtype Subst era = Subst (Map String (SubstElem era))
extend ∷ V era t → Term era t → Subst era → Subst era
emptySubst ∷ Subst era
substToEnv ∷ Subst era → Env era → Typed (Env era)
envToSubst ∷ Env era → Subst era
findV ∷ Subst era → V era t → Term era t
composeSubst ∷ Subst era → Subst era → Subst era
singleSubst ∷ V era t → Term era t → Subst era
substFromNames ∷ ∀ era. HashSet (Name era) → Subst era
data SubItem era where
- SubItem ∷ V era t → Term era t → SubItem era
itemsToSubst ∷ [SubItem era] → Subst era
substTerm ∷ Subst era → Term era t → Term era t
substPred ∷ Subst era → Pred era → Pred era
substPredWithVarTest ∷ Subst era → Pred era → Pred era
substFromTarget ∷ RootTarget era r t → Subst era
substFromPat ∷ Pat era t → Subst era
substSum ∷ Subst era → Sum era t → Sum era t
substTarget ∷ Subst era → RootTarget era r t → RootTarget era r t
simplify ∷ Term era t → Typed t
simplifySum ∷ Sum era c → Typed c
simplifyTarget ∷ ∀ era t root. RootTarget era root t → Typed t
runTerm ∷ Env era → Term era t → Typed t
runTarget ∷ Env era → RootTarget era x t → Typed t
getTarget ∷ ∀ era root t. root → RootTarget era root t → Env era → Env era
targetMaybeEnv ∷ ∀ era root t. root → RootTarget era root t → Env era → Maybe (Env era)
runPred ∷ Env era → Pred era → Typed Bool
hashSetToSet ∷ Ord a ⇒ HashSet a → Set a
hashSetDisjoint ∷ Hashable a ⇒ HashSet a → HashSet a → Bool
extendableSumsTo ∷ Pat era t → Pred era → Bool
runPreds ∷ Env era → [Pred era] → Typed Bool
bind ∷ RootTarget era r t → t → Env era → Env era
runComp ∷ Env era → s → AnyF era s → Typed Bool
termRep ∷ Era era ⇒ Term era t → Rep era t
runSum ∷ Env era → Sum era c → Typed c
makeTest ∷ Env era → Pred era → Typed (String, Bool, Pred era)
displayTerm ∷ Era era ⇒ Env era → Term era a → IO ()
patToAnyF ∷ Pat era t → [AnyF era t]
argToAnyF ∷ Rep era t → Arg era t → [AnyF era t]
push ∷ Rep era t → Lens' t s → AnyF era s → AnyF era t
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
patt ∷ Rep era t1 → Term era t2 → Pat era t1
varsOfField ∷ HashSet (Name era) → Field era s t → HashSet (Name era)
varsOfPat ∷ HashSet (Name era) → Pat era t → HashSet (Name era)
varsOfArg ∷ HashSet (Name era) → Arg era t → HashSet (Name era)
substField ∷ Subst era → Field era rec fld → Field era rec fld
substPat ∷ Subst era → Pat era t → Pat era t
substArg ∷ Subst era → Arg era t → Arg era t
bindPat ∷ t → Env era → Pat era t → Env era
bindArg ∷ t → Env era → Arg era t → Env era
argP ∷ Rep era s → Term era t → [Pat era t] → Arg era s
arg ∷ Rep era s → Term era t → Arg era s

Documentation

class (Eq a, Eq ts) ⇒ FromList ts a | ts → a where Source #

Methods

makeFromList ∷ [a] → ts Source #

getList ∷ ts → [a] Source #

tsRep ∷ Rep era ts → Rep era a Source #

Instances

Instances details

Ord a ⇒ FromList (Set a) a Source #	CAREFULL HERE, this instance may NOT be size preserving.
Instance details Defined in Test.Cardano.Ledger.Constrained.Ast Methods makeFromList ∷ [a] → Set a Source # getList ∷ Set a → [a] Source # tsRep ∷ Rep era (Set a) → Rep era a Source #
Eq a ⇒ FromList (Maybe a) a Source #
Instance details Defined in Test.Cardano.Ledger.Constrained.Ast Methods makeFromList ∷ [a] → Maybe a Source # getList ∷ Maybe a → [a] Source # tsRep ∷ Rep era (Maybe a) → Rep era a Source #
Eq a ⇒ FromList [a] a Source #
Instance details Defined in Test.Cardano.Ledger.Constrained.Ast Methods makeFromList ∷ [a] → [a] Source # getList ∷ [a] → [a] Source # tsRep ∷ Rep era [a] → Rep era a Source #
(Ord k, Eq a) ⇒ FromList (Map k a) (k, a) Source #
Instance details Defined in Test.Cardano.Ledger.Constrained.Ast Methods makeFromList ∷ [(k, a)] → Map k a Source # getList ∷ Map k a → [(k, a)] Source # tsRep ∷ Rep era (Map k a) → Rep era (k, a) Source #

type Direct a = Either a a Source #

direct ∷ Direct a → a Source #

data Term era t where Source #

Constructors

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)

Instances

Instances details

Show (Term era t) Source #
Instance details Defined in Test.Cardano.Ledger.Constrained.Ast Methods showsPrec ∷ Int → Term era t → ShowS Source # show ∷ Term era t → String Source # showList ∷ [Term era t] → ShowS Source #

data Pred era where Source #

Constructors

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 infix 4
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 infix 4
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 ∷ ∀ 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

Instances

Instances details

Show (Pred era) Source #
Instance details Defined in Test.Cardano.Ledger.Constrained.Ast Methods showsPrec ∷ Int → Pred era → ShowS Source # show ∷ Pred era → String Source # showList ∷ [Pred era] → ShowS Source #

data Sum era c where Source #

Constructors

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 ∷ ∀ x c era. Lens' x c → Rep era c → Term era x → Sum era c
ProjMap ∷ ∀ x c a era. Adds c ⇒ Rep era c → Lens' x c → Term era (Map a x) → Sum era c

Instances

Instances details

Show (Sum era c) Source #
Instance details Defined in Test.Cardano.Ledger.Constrained.Ast Methods showsPrec ∷ Int → Sum era c → ShowS Source # show ∷ Sum era c → String Source # showList ∷ [Sum era c] → ShowS Source #

pattern (:⊆:) ∷ ∀ era. ∀ a. Ord a ⇒ Term era (Set a) → Term era (Set a) → Pred era infix 4 Source #

pattern ExactSize ∷ Era era ⇒ Int → Term era Size Source #

pattern AtLeast ∷ Era era ⇒ Int → Term era Size Source #

pattern Size ∷ Era era ⇒ Size → Term era Size Source #

pattern AtMost ∷ Era era ⇒ Int → Term era Size Source #

pattern Range ∷ Era era ⇒ Int → Int → Term era Size Source #

sameRng ∷ Term era Size → Maybe Int Source #

pattern Word64 ∷ Era era ⇒ Word64 → Term era Word64 Source #

var ∷ Era era ⇒ String → Rep era t → Term era t Source #

unVar ∷ Term era t → V era t Source #

fieldToTerm ∷ Field era rec field → Term era field Source #

select ∷ (Eq t, Era era) ⇒ Term era t → Term era big → Lens' big t → Pred era Source #

(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

select2 ∷ Era era ⇒ Term era t → Term era big → Lens' big t → Pred era Source #

(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

data RootTarget era root t where Source #

Constructors

Simple ∷ Term era t → RootTarget era Void t
(:$) ∷ RootTarget era r (a → b) → RootTarget era r a → RootTarget era r b infixl 0
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
Fields ∷ Term era t → (root → Maybe t) → RootTarget era root t Partial designed to be used in Pred `Oneof` where the RootTarget getter may fail. So use `Partial` instead of `Lensed` in `Oneof`
Shift ∷ RootTarget era root2 a → Lens' root1 root2 → RootTarget era root1 a
Mask ∷ RootTarget era r a → RootTarget era Void a
Virtual
Fields ∷ Term era t → PDoc → Lens' root t → RootTarget era root t Just like Lensed but uses the String to name the field (instead of the Term)

Instances

Instances details

Show (RootTarget era r t) Source #
Instance details Defined in Test.Cardano.Ledger.Constrained.Ast Methods showsPrec ∷ Int → RootTarget era r t → ShowS Source # show ∷ RootTarget era r t → String Source # showList ∷ [RootTarget era r t] → ShowS Source #

type Target era t = RootTarget era Void t Source #

(^$) ∷ Target era (a → t) → Term era a → Target era t infixl 0 Source #

Version of (:$) That takes a Term on the right, rather than a Target

constTarget ∷ t → Target era t Source #

constRootTarget ∷ ∀ era t. Typeable t ⇒ t → RootTarget era t t Source #

emptyTarget ∷ Target era () Source #

justTarget ∷ Term era t → Target era (Maybe t) Source #

idTarget ∷ Term era t → Target era t Source #

maybeTarget ∷ Target era (t → Gen (Maybe t)) Source #

Usefull when using the Pred FromGen E.g. (FromGen termMaybeT (maybeTarget ^$ termT))

listToSetTarget ∷ Ord x ⇒ Term era [x] → Target era (Set x) Source #

setToListTarget ∷ Term era (Set x) → Target era [x] Source #

showL ∷ (t → String) → [Char] → [t] → [Char] Source #

showAllTarget ∷ RootTarget era r t → [Char] Source #

showT ∷ ∀ era t r. RootTarget era r t → String Source #

"Print a Target as nested applications"

args ∷ RootTarget era r t → [Any (RootTarget era r)] Source #

ppTarget ∷ RootTarget era r t → PDoc Source #

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.

targetRecord ∷ RootTarget era r t → [(Text, PDoc)] → PDoc Source #

nameOf ∷ RootTarget era r t → Text Source #

targetPair ∷ RootTarget era r t → (Text, PDoc) Source #

varsOfTerm ∷ HashSet (Name era) → Term era t → HashSet (Name era) Source #

vars ∷ Term era t → HashSet (Name era) Source #

varsOfTarget ∷ HashSet (Name era) → RootTarget era r t → HashSet (Name era) Source #

varsOfPred ∷ ∀ era. HashSet (Name era) → Pred era → HashSet (Name era) Source #

varsOfTrips ∷ Era era ⇒ HashSet (Name era) → [(Int, RootTarget era r t2, [Pred era])] → HashSet (Name era) Source #

varsOfPairs ∷ Era era ⇒ HashSet (Name era) → [(RootTarget era r t2, [Pred era])] → HashSet (Name era) Source #

varsOfPats ∷ Era era ⇒ HashSet (Name era) → [(Pat era t2, [Pred era])] → HashSet (Name era) Source #

varsOfSum ∷ HashSet (Name era) → Sum era r → HashSet (Name era) Source #

expandSum ∷ Sum era c → [Int] → [Sum era c] Source #

pad ∷ Int → String → String Source #

data SubstElem era where Source #

Constructors

SubstElem ∷ Rep era t → Term era t → Access era s t → SubstElem era

Instances

Instances details

Show (SubstElem era) Source #
Instance details Defined in Test.Cardano.Ledger.Constrained.Ast Methods showsPrec ∷ Int → SubstElem era → ShowS Source # show ∷ SubstElem era → String Source # showList ∷ [SubstElem era] → ShowS Source #

newtype Subst era Source #

Constructors

Subst (Map String (SubstElem era))

Instances

Instances details

Show (Subst era) Source #
Instance details Defined in Test.Cardano.Ledger.Constrained.Ast Methods showsPrec ∷ Int → Subst era → ShowS Source # show ∷ Subst era → String Source # showList ∷ [Subst era] → ShowS Source #

extend ∷ V era t → Term era t → Subst era → Subst era Source #

emptySubst ∷ Subst era Source #

substToEnv ∷ Subst era → Env era → Typed (Env era) Source #

envToSubst ∷ Env era → Subst era Source #

findV ∷ Subst era → V era t → Term era t Source #

composeSubst ∷ Subst era → Subst era → Subst era Source #

singleSubst ∷ V era t → Term era t → Subst era Source #

substFromNames ∷ ∀ era. HashSet (Name era) → Subst era Source #

data SubItem era where Source #

Constructors

SubItem ∷ V era t → Term era t → SubItem era

Instances

Instances details

Show (SubItem era) Source #
Instance details Defined in Test.Cardano.Ledger.Constrained.Ast Methods showsPrec ∷ Int → SubItem era → ShowS Source # show ∷ SubItem era → String Source # showList ∷ [SubItem era] → ShowS Source #

itemsToSubst ∷ [SubItem era] → Subst era Source #

substTerm ∷ Subst era → Term era t → Term era t Source #

substPred ∷ Subst era → Pred era → Pred era Source #

substPredWithVarTest ∷ Subst era → Pred era → Pred era Source #

Apply the Subst, and test if all variables are removed.

substFromTarget ∷ RootTarget era r t → Subst era Source #

substFromPat ∷ Pat era t → Subst era Source #

substSum ∷ Subst era → Sum era t → Sum era t Source #

substTarget ∷ Subst era → RootTarget era r t → RootTarget era r t Source #

simplify ∷ Term era t → Typed t Source #

Simplify Terms that only contain Literals (or constant) sub-Terms

simplifySum ∷ Sum era c → Typed c Source #

Simplify constant Sum's

simplifyTarget ∷ ∀ era t root. RootTarget era root t → Typed t Source #

runTerm ∷ Env era → Term era t → Typed t Source #

Fully evaluate a Term, looking up the variables in the Env.

runTarget ∷ Env era → RootTarget era x t → Typed t Source #

getTarget ∷ ∀ era root t. root → RootTarget era root t → Env era → Env era Source #

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.

targetMaybeEnv ∷ ∀ era root t. root → RootTarget era root t → Env era → Maybe (Env era) Source #

runPred ∷ Env era → Pred era → Typed Bool Source #

hashSetToSet ∷ Ord a ⇒ HashSet a → Set a Source #

hashSetDisjoint ∷ Hashable a ⇒ HashSet a → HashSet a → Bool Source #

extendableSumsTo ∷ Pat era t → Pred era → Bool Source #

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]

runPreds ∷ Env era → [Pred era] → Typed Bool Source #

run a bunch of Preds, and and together the results

bind ∷ RootTarget era r t → t → Env era → Env era Source #

runComp ∷ Env era → s → AnyF era s → Typed Bool Source #

termRep ∷ Era era ⇒ Term era t → Rep era t Source #

runSum ∷ Env era → Sum era c → Typed c Source #

makeTest ∷ Env era → Pred era → Typed (String, Bool, Pred era) Source #

displayTerm ∷ Era era ⇒ Env era → Term era a → IO () Source #

patToAnyF ∷ Pat era t → [AnyF era t] Source #

argToAnyF ∷ Rep era t → Arg era t → [AnyF era t] Source #

push ∷ Rep era t → Lens' t s → AnyF era s → AnyF era t Source #

data Pat era t where Source #

Constructors

Pat ∷ !(Rep era t) → ![Arg era t] → Pat era t

Instances

Instances details

Show (Pat era t) Source #
Instance details Defined in Test.Cardano.Ledger.Constrained.Ast Methods showsPrec ∷ Int → Pat era t → ShowS Source # show ∷ Pat era t → String Source # showList ∷ [Pat era t] → ShowS Source #

data Arg era t where Source #

Constructors

ArgPs ∷ !(Field era t s) → ![Pat era s] → Arg era t
Arg ∷ !(Field era t s) → Arg era t

Instances

Instances details

Show (Arg era t) Source #
Instance details Defined in Test.Cardano.Ledger.Constrained.Ast Methods showsPrec ∷ Int → Arg era t → ShowS Source # show ∷ Arg era t → String Source # showList ∷ [Arg era t] → ShowS Source #

patt ∷ Rep era t1 → Term era t2 → Pat era t1 Source #

Succeds if term is a variable with an embedded (Lens' t2 t1)

varsOfField ∷ HashSet (Name era) → Field era s t → HashSet (Name era) Source #

varsOfPat ∷ HashSet (Name era) → Pat era t → HashSet (Name era) Source #

varsOfArg ∷ HashSet (Name era) → Arg era t → HashSet (Name era) Source #

substField ∷ Subst era → Field era rec fld → Field era rec fld Source #

substPat ∷ Subst era → Pat era t → Pat era t Source #

substArg ∷ Subst era → Arg era t → Arg era t Source #

bindPat ∷ t → Env era → Pat era t → Env era Source #

bindArg ∷ t → Env era → Arg era t → Env era Source #

argP ∷ Rep era s → Term era t → [Pat era t] → Arg era s Source #

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.

arg ∷ Rep era s → Term era t → Arg era s Source #

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.