Safe Haskell | None |
---|---|
Language | Haskell2010 |
- data ProofTreeGen a
- = Leaf Role a
- | Root Rule a [ProofTreeGen a]
- type ProofTree = ProofTreeGen String
- type ProofMap = Map String F
- type IdSet = Set (Int, String)
- buildProofTree :: ProofMap -> F -> ProofTree
- buildProofMap :: [F] -> ProofMap
- getParents :: ProofMap -> [Parent] -> [F]
- getParentsTree :: ProofMap -> [Parent] -> [ProofTree]
- unknownTree :: Show a => String -> a -> String -> ProofTree
Types
data ProofTreeGen a
Generic tree structure for representing the structure of a proof.
Leaf Role a |
|
Root Rule a [ProofTreeGen a] |
|
Functor ProofTreeGen | |
Foldable ProofTreeGen | |
Traversable ProofTreeGen | |
Eq a => Eq (ProofTreeGen a) | |
Ord a => Ord (ProofTreeGen a) | |
Show a => Show (ProofTreeGen a) |
type ProofTree = ProofTreeGen String
Concrete instance of ProofTreeGen
with String
as
contents. Each node contains the name of a corresponding formula,
along with its dependencies.
Constructors
:: ProofMap |
|
-> F | Root formula |
-> ProofTree | Tree of formulas with the given formula as root |
buildProofTree
m
f
, build a ProofTree
with f
as root,
and using m
for dependencies resolution. Depending on the root,
not all values in m
are used.
buildProofMap
lf
, given a list of functions lf
builds a ProofMap
Internals
getParents
m
p
, from a Map
m
and a list of parents p
returns a list of corresponding parent formulas.
getParentsTree
m
p
, from a Map
m
and a list of parents p
return a list of corresponding parent subtrees.