package alba

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

Module Alba_core.Gamma_holesSource

Gamma_holes is a context with holes which can be filled later. A hole is a local unnamed variable with a type (i.e. an assumption that an element with this type exists), initially without value. Later on the value can be provided.

Sourcetype t
Sourceval context : t -> Gamma.t

The current context with holes.

Sourceval base_context : t -> Gamma.t

The initial context without holes.

Sourceval count : t -> int

The size of the context.

Sourceval count_base : t -> int

The size of the base context.

Sourceval count_bounds : t -> int

The number of bound variables which have been entered.

Sourceval count_locals : t -> int

The number of holes and bound variable which have been entered.

Sourceval index_of_level : int -> t -> int
Sourceval definition_term : int -> t -> Term.t option
Sourceval is_hole : int -> t -> bool

Is the variable a hole?

Sourceval is_bound : int -> t -> bool

Is the variable a bound variable?

Sourceval bound_number : int -> t -> int

bound_number idx gh

Return the number of the bound variable at idx.

Precondition:

is_bound idx gh
Sourceval variable_of_bound : int -> t -> Term.t

variable_of_bound i gh

Compute the variable corresponding to the ith bound variable.

Precondition:

i < count_bounds gh
Sourceval has_value : int -> t -> bool

Has the variable a value i.e. is it a hole with value.

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

The optional value of the hole.

Sourceval unfilled_holes : int -> Term.t -> t -> Fmlib.Common.Int_set.t

unfilled_holes cnt0 term gh

List of unfilled holes in term starting at level cnt0.

The returned list contains the De Bruijn levels of the unfilled holes.

Precondition:

cnt0 <= count gh
Sourceval expand : Term.t -> t -> Term.t

expand term gh Replace all holes in term with its values, if available.

Sourceval is_expanded : Term.t -> t -> bool

is_expanded term gh Is the term term expanded i.e. does it not contain any filled holes?

Sourceval term_of_term_n : Term.t_n -> t -> Term.t

term_of_term_n tn gh

Lift the term tn into the context and expand it.

Sourceval fill_hole0 : int -> Term.t -> bool -> t -> t

fill_hole idx value gh Fill the hole at idx with value. In case that value is a function abstraction appearing in a function position and the flag beta_reduce is set, do a beta reduction.

Preconditions:

is_unfilled idx gh
Sourceval fill_hole : int -> Term.t -> t -> t

fill_hole idx value gh Fill the hole at idx with value.

Preconditions:

is_hole idx gh
  not (has_value idx gh)
  is_expanded value gh
Sourceval push_hole : Term.typ -> t -> t

push_hole typ gh Add a hole of type typ to gh.

Sourceval push_bound : string -> bool -> Term.typ -> t -> t

push_bound name is_typed gh adds a bound variable to the context. The bound variable can be later used to construct binders like Pi (arg_tp, res_tp, info or Lambda (arg_tp, exp, info. is_typed is used to construct the binder.

Sourceval remove_bounds : int -> t -> t

remove_bounds n gh

Remove the n last bound variables.

Sourceval push_local : string -> Term.typ -> t -> t

push_local name typ gh is synonym for push_bound name true gh

Sourceval type_at_level : int -> t -> Term.typ
Sourceval type_of_variable : int -> t -> Term.typ

type_of_variable idx gh

Return the expanded type of the variable idx.

Sourceval type_of_literal : Term.Value.t -> t -> Term.typ
Sourceval pi : int -> Term.typ -> t -> Term.typ

pi nbounds result_tp gh

Compute a product type with result_tp using the last nbounds bound variables.

all (a: A) (b: B) ... : RT

Preconditions:

nbounds <=  count_bounds gh
Sourceval lambda : int -> Term.t -> t -> Term.t

lambda nbounds exp gh

Compute a function term with the inner expression exp using the last nbounds bound variables.

\ (a: A) (b: B) ... := exp

Preconditions:

nbounds <= count_bounds gh
Sourceval make : Gamma.t -> t
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