# Module `Alba_core__.Build`

A core internal module to support term building. Do not use outside of core directly.

Basic Idea ==========

There is a stack of to be built terms. When the construction of term starts, the term can get some type requirement.

Invariant =========

- Only terms which are welltyped in the context are constructed.

- All terms on the stack are welltyped and satisfy their requirements or have still a chance to satisfy their requirement. The satisfaction of the requirements is checked by putting a term to the stack.

Used Typing Rules =================

Product -------

Gamma |- A: sA Gamma, x:A |- B: sB Gamma |- pi_sort(sA,sB) <= s ----------------------------------- Gamma |- (all (x: A). B) : s

sA sR pi_sort(sA,sR) ---------------------------------------------- * Proposition Proposition Proposition Any(i) Any(i) Any(i) Any(j) Any(max(i,j))

At the start there is on top of the stack an empty term with an optional requirement of its return type. The required type, if present, must be a sort.

Depending of the required type we push a new item onto the stack. If the required type is a proposition, then the required type of the argument type is Any. If the required type of the whole product is `Any(i)`

, then the required type of the argument type is `Any(i)`

.

We build the argument type and pop it and push is as a bound variable.

Then we push a new item for the result type with the same required type as the requirement of the product term onto the stack and build the result type.

Finally we pop the result type and the binder and put the product term onto the top of the stack.

Application -----------

Gamma |- f: all (x: A). B Gamma |- a: A' Gamma |- A' <= A -- subtype ---------------------------------------- Gamma |- f a: B`x:=a`

We start to build `f a`

with a possible requirement which has to be satisfied after being applied to `nargs`

arguments.

`start_application`

increments nargs by one. Then it builds `f`

. The function term can only be built if its type is a product type.

Then we start a new term with the required type `A`

from the type of `f`

.

Lambda ------

Gamma |- (all (x: A): B) : s Gamma, x:A |- e: B -------------------------------------------- Gamma |- (\ (x: A) := e): all (x: A): B

`module Make : functor (Info : Fmlib.Module_types.ANY) -> sig ... end`