Theory.Constraint.System

This is the public interface for constructing and deconstructing constraint systems. The interface for performing constraint solving provided by Theory.Constraint.Solver.

Constraints

module Theory.Constraint.System.Constraints

Constraint systems

data System

A constraint system.

Instances

Eq System

Ord System

Show System

Binary System

NFData System

HasFrees System

Construction

emptySystem :: CaseDistKind -> System

The empty constraint system, which is logically equivalent to true.

data SystemTraceQuantifier

Whether we are checking for the existence of a trace satisfiying a the current constraint system or whether we're checking that no traces satisfies the current constraint system.

Constructors

ExistsSomeTrace

ExistsNoTrace

Instances

Eq SystemTraceQuantifier

Ord SystemTraceQuantifier

Show SystemTraceQuantifier

Binary SystemTraceQuantifier

NFData SystemTraceQuantifier

formulaToSystem

Arguments

:: [LNGuarded]

Axioms to add

-> CaseDistKind

Case distinction kind

-> SystemTraceQuantifier

Trace quantifier

-> LNFormula

-> System

Returns the constraint system that has to be proven to show that given formula holds in the context of the given theory.

Node constraints

sNodes :: forall arr. Arrow arr => Lens arr System (Map NodeId RuleACInst)

allKDConcs :: System -> [(NodeId, RuleACInst, LNTerm)]

A list of all KD-conclusions in the System.

nodeRule :: NodeId -> System -> RuleACInst

nodeRule v accesses the rule label of node v under the assumption that it is present in the sequent.

nodeConcNode :: NodeConc -> NodeId

nodeConcNode c compute the node-id of the node conclusion c.

nodePremNode :: NodePrem -> NodeId

nodePremNode prem is the node that this premise is referring to.

nodePremFact :: NodePrem -> System -> LNFact

nodePremFact prem se computes the fact associated to premise prem in sequent se under the assumption that premise prem is a a premise in se.

nodeConcFact :: NodeConc -> System -> LNFact

nodeConcFact (NodeConc (v, i)) accesses the i-th conclusion of the rule associated with node v under the assumption that v is labeled with a rule that has an i-th conclusion.

resolveNodePremFact :: NodePrem -> System -> Maybe LNFact

All facts associated to this node premise.

resolveNodeConcFact :: NodeConc -> System -> Maybe LNFact

The fact associated with this node conclusion, if there is one.

Actions

allActions :: System -> [(NodeId, LNFact)]

All actions that hold in a sequent.

allKUActions :: System -> [(NodeId, LNFact, LNTerm)]

All actions that hold in a sequent.

unsolvedActionAtoms :: System -> [(NodeId, LNFact)]

All actions that hold in a sequent.

kuActionAtoms :: System -> [(NodeId, LNFact, LNTerm)]

All KU-actions.

standardActionAtoms :: System -> [(NodeId, LNFact)]

The standard actions, i.e., non-KU-actions.

Edge and chain constraints

sEdges :: forall arr. Arrow arr => Lens arr System (Set Edge)

unsolvedChains :: System -> [(NodeConc, NodePrem)]

All unsolved destruction chains in the constraint system.

Temporal ordering

sLessAtoms :: forall arr. Arrow arr => Lens arr System (Set (NodeId, NodeId))

rawLessRel :: System -> [(NodeId, NodeId)]

(from,to) is in rawLessRel se iff we can prove that there is a path (possibly using the Less relation) from from to to in se without appealing to transitivity.

rawEdgeRel :: System -> [(NodeId, NodeId)]

(from,to) is in rawEdgeRel se iff we can prove that there is an edge-path from from to to in se without appealing to transitivity.

alwaysBefore :: System -> NodeId -> NodeId -> Bool

Returns a predicate that is True iff the first argument happens before the second argument in all models of the sequent.

isInTrace :: System -> NodeId -> Bool

True iff the given node id is guaranteed to be instantiated to an index in the trace.

The last node

sLastAtom :: forall arr. Arrow arr => Lens arr System (Maybe NodeId)

isLast :: System -> NodeId -> Bool

True iff the given node id is guaranteed to be instantiated to the last index of the trace.

Equations

module Theory.Tools.EquationStore

sEqStore :: forall arr. Arrow arr => Lens arr System EqStore

sSubst :: System :-> LNSubst

Label to access the free substitution of the equation store.

sConjDisjEqs :: System :-> Conj (SplitId, Set LNSubstVFresh)

Label to access the conjunction of disjunctions of fresh substutitution in the equation store.

Formulas

sFormulas :: forall arr. Arrow arr => Lens arr System (Set LNGuarded)

sSolvedFormulas :: forall arr. Arrow arr => Lens arr System (Set LNGuarded)

Lemmas

sLemmas :: forall arr. Arrow arr => Lens arr System (Set LNGuarded)

insertLemmas :: [LNGuarded] -> System -> System

Add lemmas / additional assumptions to a constraint system.

Keeping track of typing assumptions

data CaseDistKind

Case dinstinction kind that are allowed. The order of the kinds corresponds to the subkinding relation: untyped < typed.

Constructors

UntypedCaseDist

TypedCaseDist

Instances

Eq CaseDistKind

Ord CaseDistKind

Read CaseDistKind

Show CaseDistKind

Binary CaseDistKind

NFData CaseDistKind

Apply CaseDistKind

HasFrees CaseDistKind

sCaseDistKind :: forall arr. Arrow arr => Lens arr System CaseDistKind

Goals

data GoalStatus

The status of a Goal. Use its Semigroup instance to combine the status info of goals that collapse.

Constructors

GoalStatus

Fields

_gsSolved :: Bool

_gsNr :: Integer

_gsLoopBreaker :: Bool

Instances

Eq GoalStatus

Ord GoalStatus

Show GoalStatus

Binary GoalStatus

NFData GoalStatus

HasFrees GoalStatus

gsSolved :: forall arr. Arrow arr => Lens arr GoalStatus Bool

gsLoopBreaker :: forall arr. Arrow arr => Lens arr GoalStatus Bool

gsNr :: forall arr. Arrow arr => Lens arr GoalStatus Integer

sGoals :: forall arr. Arrow arr => Lens arr System (Map Goal GoalStatus)

sNextGoalNr :: forall arr. Arrow arr => Lens arr System Integer

Pretty-printing

prettySystem :: HighlightDocument d => System -> d

Pretty print a sequent

prettyNonGraphSystem :: HighlightDocument d => System -> d

Pretty print the non-graph part of the sequent; i.e. equation store and clauses.