Module `Albalib.Build_context`Source

Sourcetype pos = Fmlib.Position.t

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

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

Source

val final : 
  t ->
  (t * Alba_core.Term.t * Alba_core.Term.typ,
    int list * Alba_core.Term.typ * Alba_core.Gamma.t)
    result

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

Source

val 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

Source

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.

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/alba.albalib/Albalib/Build_context/index.html

Module `Albalib.Build_context`Source

Terminals

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

Typed expression `exp: tp`

Function Application `f a b c ...`

Function Abstraction `\ x y ... := t`

Where expression `exp where f ... := value`

package alba

Install

Dune Dependency

Authors

Maintainers

Sources

doc/alba.albalib/Albalib/Build_context/index.html

Module Albalib.Build_contextSource

Terminals

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

Typed expression exp: tp

Function Application f a b c ...

Function Abstraction \ x y ... := t

Where expression exp where f ... := value

Module `Albalib.Build_context`Source

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

Typed expression `exp: tp`

Function Application `f a b c ...`

Function Abstraction `\ x y ... := t`

Where expression `exp where f ... := value`