package alba

  1. Overview
  2. Docs
Alba compiler

Install 

dune-project
 Dependency

albatross-lang.sourceforge.net Readme Edit opam file Versions (5)

Authors

  1. H
    Helmut Brandl <helmut.brandl@gmx.net>

Maintainers

  1. H
    Helmut Brandl <helmut.brandl@gmx.net>

Sources

0.4.2.tar.gz
sha256=203ee151ce793a977b2d3e66f8b3a0cd7a82cc7f15550c63d88cb30c71eb5f95
md5=64367c393f80ca784f88d07155da4fb0

doc/alba.core/Alba_core/Gamma_holes/index.html

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