module Derivations:`sig`

..`end`

This file provides a representation of typing derivations, built by

`Permissions`

. A typing derivation can either represent success, or failure.This file provides a representation of typing derivations, built by

`Permissions`

. A typing derivation can either represent success, or failure.`type `

derivation =

`|` |
`Good of ` |
`(*` | We found a rule to apply. | `*)` |

`|` |
`Bad of ` |
`(*` | We found either no rule to apply, or we tried several rules, and none of them worked. In that case, we stop recording derivations as soon as we hit a rule that doesn't work; that rule will be the tail of the list. | `*)` |

type`rule =`

`rule_instance * derivation list`

type`rule_instance =`

`string`

`type `

judgement =

`|` |
`JSubType of ` |

`|` |
`JSubVar of ` |

`|` |
`JSubPerm of ` |

`|` |
`JSubPerms of ` |

`|` |
`JSubFloating of ` |

`|` |
`JSubConstraint of ` |

`|` |
`JSubConstraints of ` |

`|` |
`JEqual of ` |

`|` |
`JLt of ` |

`|` |
`JGt of ` |

`|` |
`JNothing` |

`|` |
`JAdd of ` |

`|` |
`JDebug of ` |

type`result =`

`(TypeCore.env * derivation, derivation) Either.either`

LazyList.t

Primitive operations return a result. A result is a lazy list of either a
derivation that "worked", meaning we have a "good" environment along with the
corresponding derivation, or a derivation that failed, meaning we have no
resulting environment.

`val no_proof : ``TypeCore.env -> judgement -> result`

Here is how to **not** prove a judgement. This means that you found no rules
to apply in order to prove that judgement.

`val apply_axiom : ``TypeCore.env ->`

judgement ->

rule_instance -> TypeCore.env -> result

This is a way of proving a judgement by using a rule without premises, i.e.
an axiom.

Please note that:
`apply_axiom env j r sub_env`

is equivalent to
`try_proof env j r (qed sub_env)`

`val try_several : ``TypeCore.env ->`

judgement ->

rule_instance ->

'a list ->

(TypeCore.env -> 'a list -> 'a -> result) -> result

This is another way of proving a judgement, namely by trying several
instances of the same rule on different items.

`try_several env j r items attempt`

will try to prove judgement `j`

in
environment `env`

, using rule `r`

; for each `item`

in `items`

, it will
`attempt item`

, hoping to find a successful result, passing it `env'`

(the
resulting environment), `remaining`

(the other items), and `item`

. If no item
in `items`

works, the result will be a conjunction of failures.

`val par : ``TypeCore.env ->`

judgement ->

rule_instance -> result list -> result

This is a slightly different combinator, that allows you to try several
rules to prove the same judgement.

`val nothing : ``TypeCore.env -> rule_instance -> result`

If you're iterating over a series of premises, it is sometimes convenient to
say that one of them requires no special operations because of a certain
rule...

`val option_of_result : ``result -> TypeCore.env option`

Get the

`env option`

part of a result.`val is_good : ``result -> bool`

This tells whether a result is successful or not.

`type `

state

The type of chained premises.

`val try_proof : ``TypeCore.env ->`

judgement ->

rule_instance -> state -> result

This is the most frequent way of trying to prove a judgement.

`try_proof env j r s`

tries to prove judgement `j`

in environment `env`

by
applying rule `r`

. The premises of rule `r`

are stored in `state`

.`val premises : ``TypeCore.env ->`

(TypeCore.env -> result) list -> state

The most intuitive way of writing down the premises for a judgement: you
just list all the results that have to be successful for this judgement to be
true, and

`premises`

takes care of chaining them left-to-right.`val (>>=) : ``result ->`

(TypeCore.env -> state) -> state

Use this operator to chain the premises of a rule in a monadic style. You ** must** terminate the sequence of operations by

`qed`

or `fail`

. This operator
passes the environments through and accumulates the premises (in case of
success), or just discards the remaining premises (in case of failure).`val qed : ``TypeCore.env -> state`

This is the final operator that finishes a derivation.

`val fail : ``state`

If a derivation fails...

`val (>>~) : ``state -> (TypeCore.env -> TypeCore.env) -> state`

Perform an operation on the

`env`

part of a state without giving any
justification for it.