package alba

  1. Overview
  2. Docs
package alba
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct