Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.Cardano.Ledger.Constrained.Solver

Synopsis

ifTrace ∷ Bool → String → a → a
hasAdds ∷ Rep era t → s t → Typed (HasConstraint Adds (s t))
isAddsType ∷ ∀ era t. Rep era t → Bool
hasCount ∷ Rep era t → s t → Typed (HasConstraint Count (s t))
isCountType ∷ ∀ era t. Rep era t → Bool
sameRep ∷ Rep era i → Rep era j → Typed (i :~: j)
simplifyAtType ∷ Era era ⇒ Rep era s → Term era t → Typed s
simplifySet ∷ (Ord rng, Era era) ⇒ Rep era rng → Term era y → Typed (HasConstraint Ord (Set rng))
simplifyList ∷ Era era ⇒ Rep era rng → Term era y → Typed (HasConstraint Eq [rng])
isMapVar ∷ Name era → Sum era c → Bool
exactlyOne ∷ (a → Bool) → [a] → Bool
projOnDom ∷ ∀ era a dom rng. Ord dom ⇒ Set a → Lens' dom a → Rep era dom → Rep era rng → Gen (Map dom rng)
atLeast ∷ Adds c ⇒ Rep era c → c → Gen c
solveMap ∷ ∀ dom rng era. Era era ⇒ V era (Map dom rng) → Pred era → Typed (MapSpec era dom rng)
solveMapSummands ∷ (Era era, Adds c) ⇒ c → c → [String] → OrdCond → V era (Map dom rng) → c → [Sum era c] → Typed (RngSpec era rng)
solveMaps ∷ (Era era, Ord dom) ⇒ V era (Map dom rng) → [Pred era] → Typed (MapSpec era dom rng)
solveSet ∷ ∀ era a. Era era ⇒ V era (Set a) → Pred era → Typed (SetSpec era a)
solveSets ∷ Era era ⇒ V era (Set a) → [Pred era] → Typed (SetSpec era a)
solveSum ∷ ∀ era t. (Adds t, Era era) ⇒ V era t → Pred era → Typed (AddsSpec t)
solveSums ∷ (Adds t, Era era) ⇒ V era t → [Pred era] → Typed (AddsSpec t)
summandAsInt ∷ Adds c ⇒ Sum era c → Typed Int
genSum ∷ Adds x ⇒ Sum era x → Rep era x → x → Subst era → Gen (Subst era)
summandsAsInt ∷ (Adds c, Era era) ⇒ [Sum era c] → Typed Int
sameV ∷ V era s → V era t → Typed (s :~: t)
unique2 ∷ Adds c ⇒ V era t → (Int, Bool, [Name era]) → Sum era c → Typed (Int, Bool, [Name era])
intSumWithUniqueV ∷ Adds c ⇒ V era t → [Sum era c] → Typed (Int, Bool)
solveList ∷ Era era ⇒ V era [a] → Pred era → Typed (ListSpec era a)
solveLists ∷ Era era ⇒ V era [a] → [Pred era] → Typed (ListSpec era a)
genCount ∷ Count t ⇒ V era t → [Pred era] → Typed (Gen t)
data Update t where
- Update ∷ s → Lens' t s → Update t
update ∷ t → [Update t] → t
anyToUpdate ∷ Rep era t1 → AnyF era t2 → Typed (Update t1)
intToNatural ∷ Int → Natural
isIf ∷ Pred era → Bool
dispatch ∷ ∀ t era. (HasCallStack, Era era) ⇒ V era t → [Pred era] → Typed (Gen t)
genOrFail ∷ Era era ⇒ Bool → Either [String] (Subst era) → ([Name era], [Pred era]) → Gen (Either [String] (Subst era))
genOrFailList ∷ Era era ⇒ Bool → Either [String] (Subst era) → [([Name era], [Pred era])] → Gen (Either [String] (Subst era))
genDependGraph ∷ Bool → Proof era → DependGraph era → Gen (Either [String] (Subst era))
solveOneVar ∷ Era era ⇒ Subst era → ([Name era], [Pred era]) → Gen (Subst era)
toolChainSub ∷ Era era ⇒ Proof era → OrderInfo → [Pred era] → Subst era → Gen (Subst era)
toolChain ∷ Era era ⇒ Proof era → OrderInfo → [Pred era] → Subst era → Gen (Env era)

Documentation

ifTrace ∷ Bool → String → a → a Source #

hasAdds ∷ Rep era t → s t → Typed (HasConstraint Adds (s t)) Source #

Is there an Adds instance for t

isAddsType ∷ ∀ era t. Rep era t → Bool Source #

hasCount ∷ Rep era t → s t → Typed (HasConstraint Count (s t)) Source #

Is there an Count instance for t

isCountType ∷ ∀ era t. Rep era t → Bool Source #

sameRep ∷ Rep era i → Rep era j → Typed (i :~: j) Source #

simplifyAtType ∷ Era era ⇒ Rep era s → Term era t → Typed s Source #

Simplify and return with evidence that expr has type s

simplifySet ∷ (Ord rng, Era era) ⇒ Rep era rng → Term era y → Typed (HasConstraint Ord (Set rng)) Source #

simplifyList ∷ Era era ⇒ Rep era rng → Term era y → Typed (HasConstraint Eq [rng]) Source #

isMapVar ∷ Name era → Sum era c → Bool Source #

Is the Sum a variable (of a map). Only SumMap and Project store maps.

exactlyOne ∷ (a → Bool) → [a] → Bool Source #

projOnDom ∷ ∀ era a dom rng. Ord dom ⇒ Set a → Lens' dom a → Rep era dom → Rep era rng → Gen (Map dom rng) Source #

Make a generator for a Map type when there is a Projection from the domain of the map. This has been superceeded by the RelLens RelSpec

atLeast ∷ Adds c ⇒ Rep era c → c → Gen c Source #

solveMap ∷ ∀ dom rng era. Era era ⇒ V era (Map dom rng) → Pred era → Typed (MapSpec era dom rng) Source #

solveMapSummands ∷ (Era era, Adds c) ⇒ c → c → [String] → OrdCond → V era (Map dom rng) → c → [Sum era c] → Typed (RngSpec era rng) Source #

We are solving for a (V era (Map d r)). This must occurr exactly once in the [Sum era c] That can only happen in a (RngSum cond c) or a (RngProj cond rep c) constructor of Sum Because we don't know if c can have negative values, we do the summation as an Integer

solveMaps ∷ (Era era, Ord dom) ⇒ V era (Map dom rng) → [Pred era] → Typed (MapSpec era dom rng) Source #

solveSet ∷ ∀ era a. Era era ⇒ V era (Set a) → Pred era → Typed (SetSpec era a) Source #

Given a variable: v1, with a Set type, compute a SetSpec which describes the constraints implied by the Pred predicate

solveSets ∷ Era era ⇒ V era (Set a) → [Pred era] → Typed (SetSpec era a) Source #

solveSum ∷ ∀ era t. (Adds t, Era era) ⇒ V era t → Pred era → Typed (AddsSpec t) Source #

solveSums ∷ (Adds t, Era era) ⇒ V era t → [Pred era] → Typed (AddsSpec t) Source #

summandAsInt ∷ Adds c ⇒ Sum era c → Typed Int Source #

genSum ∷ Adds x ⇒ Sum era x → Rep era x → x → Subst era → Gen (Subst era) Source #

summandsAsInt ∷ (Adds c, Era era) ⇒ [Sum era c] → Typed Int Source #

sameV ∷ V era s → V era t → Typed (s :~: t) Source #

unique2 ∷ Adds c ⇒ V era t → (Int, Bool, [Name era]) → Sum era c → Typed (Int, Bool, [Name era]) Source #

intSumWithUniqueV ∷ Adds c ⇒ V era t → [Sum era c] → Typed (Int, Bool) Source #

Check that there is exactly 1 occurence of v, and return the sum of the other terms in ss which should all be constants.

solveList ∷ Era era ⇒ V era [a] → Pred era → Typed (ListSpec era a) Source #

Given a variable: v1, with a List type, compute a ListSpec which describes the constraints implied by the Pred predicate

solveLists ∷ Era era ⇒ V era [a] → [Pred era] → Typed (ListSpec era a) Source #

genCount ∷ Count t ⇒ V era t → [Pred era] → Typed (Gen t) Source #

Combine solving an generating for a variable with a Counts instance

data Update t where Source #

Used in solving Projections

Constructors

Update ∷ s → Lens' t s → Update t

update ∷ t → [Update t] → t Source #

anyToUpdate ∷ Rep era t1 → AnyF era t2 → Typed (Update t1) Source #

intToNatural ∷ Int → Natural Source #

isIf ∷ Pred era → Bool Source #

dispatch ∷ ∀ t era. (HasCallStack, Era era) ⇒ V era t → [Pred era] → Typed (Gen t) Source #

Dispatch on the type of the variable v1 being solved.

genOrFail ∷ Era era ⇒ Bool → Either [String] (Subst era) → ([Name era], [Pred era]) → Gen (Either [String] (Subst era)) Source #

genOrFailList ∷ Era era ⇒ Bool → Either [String] (Subst era) → [([Name era], [Pred era])] → Gen (Either [String] (Subst era)) Source #

genDependGraph ∷ Bool → Proof era → DependGraph era → Gen (Either [String] (Subst era)) Source #

solveOneVar ∷ Era era ⇒ Subst era → ([Name era], [Pred era]) → Gen (Subst era) Source #

Solve for one variable, and add its solution to the substitution

toolChainSub ∷ Era era ⇒ Proof era → OrderInfo → [Pred era] → Subst era → Gen (Subst era) Source #

toolChain ∷ Era era ⇒ Proof era → OrderInfo → [Pred era] → Subst era → Gen (Env era) Source #