| 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 ∷ 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
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 #
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
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
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
genCount ∷ Count t ⇒ V era t → [Pred era] → Typed (Gen t) Source #
Combine solving an generating for a variable with a Counts instance
Used in solving Projections
intToNatural ∷ Int → Natural 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 #