Portability | GHC only |
---|---|

Maintainer | Simon Meier <iridcode@gmail.com> |

Safe Haskell | None |

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

:: ProofContext | |

-> [LNGuarded] | Axioms. |

-> [CaseDistinction] |

Precompute a saturated set of case distinctions.

:: [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.