Module Derivations

module Derivations: sig .. end

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

The type of derivations

type derivation =

`\|`	`Good of TypeCore.env * judgement * rule`	`(*`	We found a rule to apply.	`*)`
`\|`	`Bad of TypeCore.env * judgement * rule list`	`(*`	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 TypeCore.typ * TypeCore.typ`
`\|`	`JSubVar of TypeCore.var * TypeCore.typ`
`\|`	`JSubPerm of TypeCore.typ`
`\|`	`JSubPerms of TypeCore.typ list`
`\|`	`JSubFloating of TypeCore.typ`
`\|`	`JSubConstraint of TypeCore.mode_constraint`
`\|`	`JSubConstraints of TypeCore.mode_constraint list`
`\|`	`JEqual of TypeCore.typ * TypeCore.typ`
`\|`	`JLt of TypeCore.typ * TypeCore.typ`
`\|`	`JGt of TypeCore.typ * TypeCore.typ`
`\|`	`JNothing`
`\|`	`JAdd of TypeCore.typ`
`\|`	`JDebug of TypeCore.typ * TypeCore.typ`

The type of primitive functions

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...

Convenient helpers to deal with results

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.

State, i.e. chaining premises in order to prove a judgement

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...

Misc.

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

Perform an operation on the env part of a state without giving any justification for it.