Module Albalib.Build_contextSource

Sourcetype range = pos * pos
Sourcetype t
Sourcetype 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.

Sourceval count : t -> int
Sourceval count_base : t -> int
Sourceval count_entries : t -> int
Sourceval count_bounds : t -> int
Sourceval required_type_in_context : t -> type_in_context

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.

Terminals

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

bound level nargs bc

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

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

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

Sourcemodule Product : sig ... end

Typed expression exp: tp

Sourcemodule Typed : sig ... end

Function Application f a b c ...

Sourcemodule Application : sig ... end

Function Abstraction \ x y ... := t

Sourcemodule Lambda : sig ... end

Where expression exp where f ... := value

The where expression

    exp where
        f := value

is treated like

    (\f := exp) value

i.e.

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

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

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