package alba

  1. Overview
  2. Docs
type pos = Fmlib.Position.t
type range = pos * pos
type t
type type_in_context = int list * Alba_core.Term.typ * Alba_core.Gamma.t

A 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 -> int
val count_base : t -> int
val count_entries : t -> int
val count_bounds : t -> int
val required_type_in_context : t -> type_in_context
val make : Alba_core.Gamma.t -> t

make 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 -> (t * Alba_core.Term.t * Alba_core.Term.typ, int list * Alba_core.Term.typ * Alba_core.Gamma.t) Stdlib.result


val base_candidate : range -> int -> Alba_core.Term.t -> int -> t -> t option

base_candidate range variant 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 find_last_ambiguous : t list -> range * (Alba_core.Term.t * Alba_core.Term.typ) list
val bound : int -> int -> t -> (t, type_in_context * type_in_context) Stdlib.result

bound level nargs bc

val next_formal_argument : string Fmlib.Character_parser.Located.t -> bool -> t -> t

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.

val find_first_untyped_formal : t -> range option
val find_first_name_violation : t -> (range * string * string) option

Product all (a: A) ... : RT

module Product : sig ... end

Typed expression exp: tp

module Typed : sig ... end

Function Application f a b c ...

module Application : sig ... end

Function Abstraction \ x y ... := t

module Lambda : sig ... end

Where expression exp where f ... := value

The where expression

exp where
    f := value

is treated like

(\f := exp) value


Appl ( Lambda (f, F, exp), value)

i.e. a beta redex, and finally converted to

Where (f, F, exp, value)
module Where : sig ... end