| Portability | GHC only |
|---|---|
| Maintainer | Simon Meier <iridcode@gmail.com> |
| Safe Haskell | None |
Theory.Constraint.Solver.CaseDistinctions
Description
Big-step proofs using case distinctions on the possible sources of a fact.
- unsolvedChainConstraints :: CaseDistinction -> [Int]
- precomputeCaseDistinctions :: ProofContext -> [LNGuarded] -> [CaseDistinction]
- refineWithTypingAsms :: [LNGuarded] -> ProofContext -> [CaseDistinction] -> [CaseDistinction]
- solveWithCaseDistinction :: ProofContext -> [CaseDistinction] -> Goal -> Maybe (Reduction [String])
- removeRedundantCases :: ProofContext -> [LVar] -> (a -> System) -> [a] -> [a]
Precomputed case distinctions
Queries
unsolvedChainConstraints :: CaseDistinction -> [Int]Source
The number of remaining chain constraints of each case.
Construction
precomputeCaseDistinctionsSource
Arguments
| :: ProofContext | |
| -> [LNGuarded] | Axioms. |
| -> [CaseDistinction] |
Precompute a saturated set of case distinctions.
Arguments
| :: [LNGuarded] | Typing assumptions to use. |
| -> ProofContext | Proof context to use. |
| -> [CaseDistinction] | Original, untyped case distinctions. |
| -> [CaseDistinction] | Refined, typed case distinctions. |
Refine a set of case distinction by exploiting additional typing assumptions.
Application
solveWithCaseDistinction :: ProofContext -> [CaseDistinction] -> Goal -> Maybe (Reduction [String])Source
Try to solve a premise goal or KU action using the first precomputed
case distinction with a matching premise.
Redundant cases
removeRedundantCases :: ProofContext -> [LVar] -> (a -> System) -> [a] -> [a]Source
Given a list of stable variables (that are referenced from outside and cannot be simply renamed) and a list containing systems, this function returns a subsequence of the list such that for all removed systems, there is a remaining system that is equal modulo renaming of non-stable variables.