Portability | GHC only |
---|---|
Maintainer | Simon Meier <iridcode@gmail.com> |
Safe Haskell | None |
Types representing constraints.
- module Theory.Constraint.System.Guarded
- type NodePrem = (NodeId, PremIdx)
- type NodeConc = (NodeId, ConcIdx)
- data Edge = Edge {}
- type Less = (NodeId, NodeId)
- data Goal
- isActionGoal :: Goal -> Bool
- isStandardActionGoal :: Goal -> Bool
- isPremiseGoal :: Goal -> Bool
- isChainGoal :: Goal -> Bool
- isSplitGoal :: Goal -> Bool
- isDisjGoal :: Goal -> Bool
- prettyNode :: HighlightDocument d => (NodeId, RuleACInst) -> d
- prettyNodePrem :: HighlightDocument d => NodePrem -> d
- prettyNodeConc :: HighlightDocument d => NodeConc -> d
- prettyEdge :: HighlightDocument d => Edge -> d
- prettyLess :: HighlightDocument d => Less -> d
- prettyGoal :: HighlightDocument d => Goal -> d
Guarded formulas
Graph constraints
A labeled edge in a derivation graph.
Goal constraints
A Goal
denotes that a constraint reduction rule is applicable, which
might result in case splits. We either use a heuristic to decide what goal
to solve next or leave the choice to user (in case of the interactive UI).
isActionGoal :: Goal -> BoolSource
isPremiseGoal :: Goal -> BoolSource
isChainGoal :: Goal -> BoolSource
isSplitGoal :: Goal -> BoolSource
isDisjGoal :: Goal -> BoolSource
Pretty-printing
prettyNode :: HighlightDocument d => (NodeId, RuleACInst) -> dSource
Pretty print a node.
prettyNodePrem :: HighlightDocument d => NodePrem -> dSource
Pretty print a node premise.
prettyNodeConc :: HighlightDocument d => NodeConc -> dSource
Pretty print a node conclusion.
prettyEdge :: HighlightDocument d => Edge -> dSource
Pretty print a edge as src >-i--j-> tgt
.
prettyLess :: HighlightDocument d => Less -> dSource
Pretty print a less-atom as src < tgt
.
prettyGoal :: HighlightDocument d => Goal -> dSource
Pretty print a goal.