package alba

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

Module Albalib.Build_contextSource

Sourcetype t
Sourcetype type_in_context = int list * Term.typ * 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_locals : t -> int
Sourceval count_bounds : t -> int
Sourceval required_type_in_context : t -> type_in_context
Sourceval make : 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.

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

Terminals

Sourceval base_candidate : Term.t -> int -> t -> t option

base_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
Sourceval bound : int -> int -> t -> (t, type_in_context * type_in_context) result

bound level nargs bc

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