| Portability | GHC only |
|---|---|
| Maintainer | Simon Meier <iridcode@gmail.com> |
| Safe Haskell | None |
Theory.Constraint.Solver.Types
Description
Common types for our constraint solver. They must be declared jointly because there is a recursive dependency between goals, proof contexts, and case distinctions.
- data ProofContext = ProofContext {}
- data InductionHint
- pcSignature :: forall arr. Arrow arr => Lens arr ProofContext SignatureWithMaude
- pcRules :: forall arr. Arrow arr => Lens arr ProofContext ClassifiedRules
- pcInjectiveFactInsts :: forall arr. Arrow arr => Lens arr ProofContext (Set FactTag)
- pcCaseDists :: forall arr. Arrow arr => Lens arr ProofContext [CaseDistinction]
- pcCaseDistKind :: forall arr. Arrow arr => Lens arr ProofContext CaseDistKind
- pcUseInduction :: forall arr. Arrow arr => Lens arr ProofContext InductionHint
- pcTraceQuantifier :: forall arr. Arrow arr => Lens arr ProofContext SystemTraceQuantifier
- pcMaudeHandle :: ProofContext :-> MaudeHandle
- data ClassifiedRules = ClassifiedRules {
- _crProtocol :: [RuleAC]
- _crDestruct :: [RuleAC]
- _crConstruct :: [RuleAC]
- emptyClassifiedRules :: ClassifiedRules
- crConstruct :: forall arr. Arrow arr => Lens arr ClassifiedRules [RuleAC]
- crDestruct :: forall arr. Arrow arr => Lens arr ClassifiedRules [RuleAC]
- crProtocol :: forall arr. Arrow arr => Lens arr ClassifiedRules [RuleAC]
- joinAllRules :: ClassifiedRules -> [RuleAC]
- nonSilentRules :: ClassifiedRules -> [RuleAC]
- data CaseDistinction = CaseDistinction {}
- cdGoal :: forall arr. Arrow arr => Lens arr CaseDistinction Goal
- cdCases :: forall arr. Arrow arr => Lens arr CaseDistinction (Disj ([String], System))
- prettyCaseDistinction :: HighlightDocument d => CaseDistinction -> d
Proof context
data ProofContext Source
A proof context contains the globally fresh facts, classified rewrite rules and the corresponding precomputed premise case distinction theorems.
Constructors
| ProofContext | |
Instances
data InductionHint Source
Constructors
| UseInduction | |
| AvoidInduction |
pcSignature :: forall arr. Arrow arr => Lens arr ProofContext SignatureWithMaudeSource
pcRules :: forall arr. Arrow arr => Lens arr ProofContext ClassifiedRulesSource
pcInjectiveFactInsts :: forall arr. Arrow arr => Lens arr ProofContext (Set FactTag)Source
pcCaseDists :: forall arr. Arrow arr => Lens arr ProofContext [CaseDistinction]Source
pcCaseDistKind :: forall arr. Arrow arr => Lens arr ProofContext CaseDistKindSource
pcUseInduction :: forall arr. Arrow arr => Lens arr ProofContext InductionHintSource
pcTraceQuantifier :: forall arr. Arrow arr => Lens arr ProofContext SystemTraceQuantifierSource
pcMaudeHandle :: ProofContext :-> MaudeHandleSource
The MaudeHandle of a proof-context.
Classified rules
data ClassifiedRules Source
Constructors
| ClassifiedRules | |
Fields
| |
emptyClassifiedRules :: ClassifiedRulesSource
The empty proof rule set.
crConstruct :: forall arr. Arrow arr => Lens arr ClassifiedRules [RuleAC]Source
crDestruct :: forall arr. Arrow arr => Lens arr ClassifiedRules [RuleAC]Source
crProtocol :: forall arr. Arrow arr => Lens arr ClassifiedRules [RuleAC]Source
joinAllRules :: ClassifiedRules -> [RuleAC]Source
joinAllRules rules computes the union of all rules classified in
rules.
nonSilentRules :: ClassifiedRules -> [RuleAC]Source
Extract all non-silent rules.
Precomputed case distinctions.
data CaseDistinction Source
A big-step case distinction.
prettyCaseDistinction :: HighlightDocument d => CaseDistinction -> dSource
Pretty print a case distinction