cardano-ledger-test-9.9.9.9: Testing harness, tests and benchmarks for Shelley style cardano ledgers
Safe HaskellSafe-Inferred
LanguageHaskell2010

Test.Cardano.Ledger.Constrained.Ast

Description

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

Synopsis

Documentation

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

Methods

makeFromList ∷ [a] → ts Source #

getList ∷ ts → [a] Source #

tsRepRep 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 #

getListSet a → [a] Source #

tsRepRep 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 #

getListMaybe a → [a] Source #

tsRepRep 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 #

tsRepRep 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 #

getListMap k a → [(k, a)] Source #

tsRepRep era (Map k a) → Rep era (k, a) Source #

type Direct a = Either a a Source #

directDirect a → a Source #

data Term era t where Source #

Constructors

LitRep era t → t → Term era t 
VarV era t → Term era t 
DomOrd 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] 
ProjMOrd 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) 
ProjLens' b t → Rep era t → Term era b → Term era t 
DeltaTerm era CoinTerm era DeltaCoin 
NegateTerm era DeltaCoinTerm era DeltaCoin 
RestrictOrd a ⇒ Term era (Set a) → Term era (Map a b) → Term era (Map a b) 
HashDEra era ⇒ Term era (Data era) → Term era (DataHash (EraCrypto era)) 
HashSReflect era ⇒ Term era (ScriptF era) → Term era (ScriptHash (EraCrypto era)) 
PairTerm 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

showsPrecIntTerm era t → ShowS Source #

showTerm era t → String Source #

showList ∷ [Term era t] → ShowS Source #

data Pred era where Source #

Constructors

MetaSizeSizeTerm era SizePred era 
SizedSizeable t ⇒ Term era SizeTerm era t → Pred era 
(:=:)Eq a ⇒ Term era a → Term era a → Pred era infix 4 
SubsetOrd a ⇒ Term era (Set a) → Term era (Set a) → Pred era 
DisjointOrd 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 
RandomTerm era t → Pred era 
ComponentDirect (Term era t) → [AnyF era t] → Pred era 
CanFollowCount n ⇒ Term era n → Term era n → Pred era 
MemberOrd a ⇒ Direct (Term era a) → Term era (Set a) → Pred era 
NotMemberOrd 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 
GenFromTerm era t → RootTarget era r (Gen t) → Pred era 
ListFromList fs t ⇒ Term era fs → [Term era t] → Pred era 
Choose ∷ (Era era, Eq t) ⇒ Term era SizeTerm era [t] → [(Int, Target era t, [Pred era])] → Pred era 
ForEach ∷ (Era era, FromList fs t, Eq t) ⇒ Term era SizeTerm 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 
IfRootTarget era r BoolPred era → Pred era → Pred era 
BeforeTerm era a → Term era b → Pred era 
ListWhere ∷ (Era era, Eq t) ⇒ Term era SizeTerm 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

showsPrecIntPred era → ShowS Source #

showPred era → String Source #

showList ∷ [Pred era] → ShowS Source #

data Sum era c where Source #

Constructors

SumMapAdds c ⇒ Term era (Map a c) → Sum era c 
SumListAdds c ⇒ Term era [c] → Sum era c 
OneTerm 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

showsPrecIntSum era c → ShowS Source #

showSum 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 ExactSizeEra era ⇒ IntTerm era Size Source #

pattern AtLeastEra era ⇒ IntTerm era Size Source #

pattern SizeEra era ⇒ SizeTerm era Size Source #

pattern AtMostEra era ⇒ IntTerm era Size Source #

pattern RangeEra era ⇒ IntIntTerm era Size Source #

pattern Word64Era era ⇒ Word64Term era Word64 Source #

varEra era ⇒ StringRep era t → Term era t Source #

unVarTerm era t → V era t Source #

fieldToTermField 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

select2Era 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

SimpleTerm era t → RootTarget era Void t 
(:$)RootTarget era r (a → b) → RootTarget era r a → RootTarget era r b infixl 0 
ConstrString → (a → b) → RootTarget era Void (a → b) 
InvertStringTypeRep root → (a → b) → RootTarget era root (a → b) 
LensedTerm era t → SimpleGetter root t → RootTarget era root t 
Partial 

Fields

ShiftRootTarget era root2 a → Lens' root1 root2 → RootTarget era root1 a 
MaskRootTarget 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

showsPrecIntRootTarget era r t → ShowS Source #

showRootTarget 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 #

justTargetTerm era t → Target era (Maybe t) Source #

idTargetTerm era t → Target era t Source #

maybeTargetTarget era (t → Gen (Maybe t)) Source #

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

listToSetTargetOrd x ⇒ Term era [x] → Target era (Set x) Source #

setToListTargetTerm era (Set x) → Target era [x] Source #

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

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

"Print a Target as nested applications"

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

ppTargetRootTarget 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.

targetRecordRootTarget era r t → [(Text, PDoc)] → PDoc Source #

nameOfRootTarget era r t → Text Source #

targetPairRootTarget era r t → (Text, PDoc) Source #

varsOfTermHashSet (Name era) → Term era t → HashSet (Name era) Source #

varsTerm era t → HashSet (Name era) Source #

varsOfTargetHashSet (Name era) → RootTarget era r t → HashSet (Name era) Source #

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

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

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

varsOfPatsEra era ⇒ HashSet (Name era) → [(Pat era t2, [Pred era])] → HashSet (Name era) Source #

varsOfSumHashSet (Name era) → Sum era r → HashSet (Name era) Source #

expandSumSum era c → [Int] → [Sum era c] Source #

padIntStringString Source #

data SubstElem era where Source #

Constructors

SubstElemRep 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

showsPrecIntSubstElem era → ShowS Source #

showSubstElem 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

showsPrecIntSubst era → ShowS Source #

showSubst era → String Source #

showList ∷ [Subst era] → ShowS Source #

extendV era t → Term era t → Subst era → Subst era Source #

substToEnvSubst era → Env era → Typed (Env era) Source #

envToSubstEnv era → Subst era Source #

findVSubst era → V era t → Term era t Source #

composeSubstSubst era → Subst era → Subst era Source #

singleSubstV era t → Term era t → Subst era Source #

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

data SubItem era where Source #

Constructors

SubItemV era t → Term era t → SubItem era 

Instances

Instances details
Show (SubItem era) Source # 
Instance details

Defined in Test.Cardano.Ledger.Constrained.Ast

Methods

showsPrecIntSubItem era → ShowS Source #

showSubItem era → String Source #

showList ∷ [SubItem era] → ShowS Source #

itemsToSubst ∷ [SubItem era] → Subst era Source #

substTermSubst era → Term era t → Term era t Source #

substPredSubst era → Pred era → Pred era Source #

substPredWithVarTestSubst era → Pred era → Pred era Source #

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

substFromPatPat era t → Subst era Source #

substSumSubst era → Sum era t → Sum era t Source #

substTargetSubst era → RootTarget era r t → RootTarget era r t Source #

simplifyTerm era t → Typed t Source #

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

simplifySumSum era c → Typed c Source #

Simplify constant Sum's

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

runTermEnv era → Term era t → Typed t Source #

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

runTargetEnv 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 #

runPredEnv era → Pred era → Typed Bool Source #

hashSetToSetOrd a ⇒ HashSet a → Set a Source #

extendableSumsToPat 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]

runPredsEnv era → [Pred era] → Typed Bool Source #

run a bunch of Preds, and and together the results

bindRootTarget era r t → t → Env era → Env era Source #

runCompEnv era → s → AnyF era s → Typed Bool Source #

termRepEra era ⇒ Term era t → Rep era t Source #

runSumEnv era → Sum era c → Typed c Source #

makeTestEnv era → Pred era → Typed (String, Bool, Pred era) Source #

displayTermEra era ⇒ Env era → Term era a → IO () Source #

patToAnyFPat era t → [AnyF era t] Source #

argToAnyFRep era t → Arg era t → [AnyF era t] Source #

pushRep 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

showsPrecIntPat era t → ShowS Source #

showPat 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

showsPrecIntArg era t → ShowS Source #

showArg era t → String Source #

showList ∷ [Arg era t] → ShowS Source #

pattRep era t1 → Term era t2 → Pat era t1 Source #

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

varsOfFieldHashSet (Name era) → Field era s t → HashSet (Name era) Source #

varsOfPatHashSet (Name era) → Pat era t → HashSet (Name era) Source #

varsOfArgHashSet (Name era) → Arg era t → HashSet (Name era) Source #

substFieldSubst era → Field era rec fld → Field era rec fld Source #

substPatSubst era → Pat era t → Pat era t Source #

substArgSubst 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 #

argPRep 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.

argRep 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.