module type PROOFRULE =`sig`

..`end`

`type `

seq_t

`type `

proof_t

type`axiom_f =`

`seq_t -> string option`

type`infrule_app =`

`(seq_t * Tagpairs.t * Tagpairs.t) list * string`

type`infrule_f =`

`seq_t -> infrule_app list`

type`backrule_f =`

`seq_t -> seq_t -> (Tagpairs.t * string) list`

type`select_f =`

`int -> proof_t -> int list`

type`t =`

`int -> proof_t -> (int list * proof_t) Blist.t`

The type of proof rules:
Proof rules are functions that take an open node in a proof (i.e. an int
identifying the node, and the proof structure containing the node) and
return a list of new proofs that are obtained by applying the rule in all
applicable ways to the open node in the provided proof, along with a list
for each new proof of the newly added open nodes (i.e. the premises)
*

`val mk_axiom : ``axiom_f -> t`

Axioms are modeled as functions that return

`Some string`

when the
input sequent is an instance of an axiom described by `string`

, else
`None`

.`val mk_infrule : ``infrule_f -> t`

Rules are functions that break down a sequent to a choice of applications
where each application is a list of premises, including tag information,
and a description.

`val mk_backrule : ``bool ->`

select_f -> backrule_f -> t

Backlink rules take:

- a boolean
`eager`

- a selection function
`s`

- a matching function
`m`

The selection function is applied on the current subgoal and proof, and a list of goal indices is returned that represents possible back-link targets. This allows flexibility e.g., in changing from ancestral-only back-links to general ones.

`m`

is applied to every pair consisting of the current subgoal
and a goal returned from the selection function. `m`

returns a list of
tag information and string descriptions, each describing a different
way to form a back-link.
If `eager`

is true then the first result in this iteration will be chosen
and no back-tracking will even happen over later possible matches.
Otherwise all possible matches are returned as different choices.

`val all_nodes : ``select_f`

Ready-made selection functions doing the obvious.

`val closed_nodes : ``select_f`

`val ancestor_nodes : ``select_f`

`val syntactically_equal_nodes : ``select_f`

`val fail : ``t`

The rule that always fails.

Return current subgoal and proof as application.

`val identity : ``t`

`val attempt : ``t -> t`

Try a rule and if it fails act as

`identity`

.
Apply the second rule on all premises generated by applying the first.

`val compose : ``t -> t -> t`

Apply the list of rules in the second argument in a pairwise fashion to
the premises generated by applying the first rule

`val compose_pairwise : ``t -> t list -> t`

`val choice : ``t list -> t`

Apply a list of rules on current subgoal and return all applications.

Try rules from a list until the first rule is found that has some
applications on current sugboal and return only those.

`val first : ``t list -> t`

Apply a sequence of rules iteratively through

`compose`

.`val sequence : ``t list -> t`

`val conditional : ``(seq_t -> bool) -> t -> t`

`val combine_axioms : ``t -> t -> t`