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.

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


val (>>~) : state -> (TypeCore.env -> TypeCore.env) -> state
Perform an operation on the env part of a state without giving any justification for it.