Safe Haskell	None
Language	Haskell2010

Data.Proof

Contents

Types
Constructors
Internals

Synopsis

Types

data ProofTreeGen a

Generic tree structure for representing the structure of a proof.

Constructors

Leaf Role a	`Leaf` `r` `a` is a node with `Role` `r` and content `a` (usually `String`, `F` or `Formula`) and with no dependencies in other nodes.
Root Rule a [ProofTreeGen a]	`Root` `r` `a` `d` is a node with deduction `Rule` `r`, content `a` (usually `String`, `F` or `Formula`), and dependencies `d`.

Instances

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.

type ProofMap = Map String F

Map from formula names to an F formula type, useful to get more information from a node in a ProofTree.

type IdSet = Set (Int, String)

Simple type for sets of identifiers whit associated scopes

Constructors

buildProofTree

Arguments

:: ProofMap	`Map` for resolving dependencies
-> 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

Arguments

:: [F]	List of functions
-> ProofMap	Map of the given functions indexed by its names

buildProofMap lf, given a list of functions lf builds a ProofMap

Internals

getParents

Arguments

:: ProofMap	`Map`
-> [Parent]	List of 'Parents
-> [F]	List of parent formulas

getParents m p, from a Map m and a list of parents p returns a list of corresponding parent formulas.

getParentsTree

Arguments

:: ProofMap	`Map`
-> [Parent]	List of parents
-> [ProofTree]	List of parents subtrees

getParentsTree m p, from a Map m and a list of parents p return a list of corresponding parent subtrees.

unknownTree

Arguments

:: Show a
=> String	Description of the unexpected data type
-> a	Unexpected data
-> String	Formula name
-> ProofTree	`Unknown` node

When an unknown Rule, Source, or other unexpected data type is found a Leaf With an Unknown Role and error message is created.