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 module provides printing functions for derivations.

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`
`\|`	`JSubFloating of TypeCore.typ`
`\|`	`JSubConstraint of TypeCore.mode_constraint`
`\|`	`JEqual of TypeCore.typ * TypeCore.typ`
`\|`	`JLt of TypeCore.typ * TypeCore.typ`
`\|`	`JGt of TypeCore.typ * TypeCore.typ`
`\|`	`JNothing`
`\|`	`JAdd of TypeCore.typ`

The type of primitive functions

type result = TypeCore.env option * derivation

Primitive operations return a result, that is, either Some env along with a good derivation, or None with a bad derivation.

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 (the first item in the list that yielded a successful result). If no item in items works, the result will be a conjunction of failures.

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

Composition of results

val (>>|) : result ->
       (TypeCore.env -> TypeCore.env option) -> TypeCore.env option

Simple composition that discards derivations. Terminate a sequence with drop.

val drop : TypeCore.env -> TypeCore.env option

Tie the knot.

Convenient helpers to deal with results

val drop_derivation : 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.