Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package alba
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type type_in_context = int list * Alba_core.Term.typ * Alba_core.Gamma.tA build context consists of a context with holes and a stack of to be constructed terms.
There is always a next to be constructed term. The term is either in a function position or an argument position.
val count : t -> intval count_base : t -> intval count_locals : t -> intval count_bounds : t -> intval required_type_in_context : t -> type_in_contextval make : Alba_core.Gamma.t -> tmake gamma
Make a build context based on gamma. Push 2 holes onto the context to get
Gamma, E: Any(2), e: E
The next to be constructed term points to e.
val final :
t ->
(Alba_core.Term.t * Alba_core.Term.typ,
int list * Alba_core.Term.typ * Alba_core.Gamma.t)
Stdlib.resultTerminals
val base_candidate : Alba_core.Term.t -> int -> t -> t optionbase_candidate term nargs bc
Receive the term term as a candidate for the next to be constructed term. The candidate is from the base context and in applied to nargs arguments.
Base candidates are either
- Literals (Numbers, characters, strings)
- Variables from the base context
val bound :
int ->
int ->
t ->
(t, type_in_context * type_in_context) Stdlib.resultbound level nargs bc
Add a bound variable based on the last argument type and push a placeholder for the next argument type or the result type. I.e. expect the next argument type or the result type.
Product all (a: A) ... : RT
module Product : sig ... endTyped expression exp: tp
module Typed : sig ... endFunction Application f a b c ...
module Application : sig ... endFunction Abstraction \ x y ... := t
module Lambda : sig ... endWhere expression exp where f ... := value
The where expression
exp where
f := valueis treated like
(\f := exp) valuei.e.
Appl ( Lambda (f, F, exp), value)i.e. a beta redex, and finally converted to
Where (f, F, exp, value)module Where : sig ... end