package alba

You can search for identifiers within the package.

in-package search v0.2.0

Alba compiler

Install

Dune Dependency

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

Authors

H

Helmut Brandl <helmut.brandl@gmx.net>

Maintainers

H

Helmut Brandl <helmut.brandl@gmx.net>

Sources

0.4.3.tar.gz

sha256=062f33c55ef39706c4290dff67d5a00bf009051fd757f9352be527f629ae21fc

md5=eb4edc4d6b7e15b83d6397bd34994153

doc/alba.core/Alba_core/Unifier/Make/argument-1-H/index.html

Parameter `Make.H`

include Gamma_algo.GAMMA

type t

val count : t -> int

Number of variables in the context.

val is_valid_index : int -> t -> bool

val name_of_index : int -> t -> string

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

push_local name typ gamma

Add the local variable with name and typ to the context.

Precondition

name <> ""

val type_of_literal : Term.Value.t -> t -> Term.typ

val type_of_variable : int -> t -> Term.typ

type_of_variable idx gamma

Return the type of the variable idx. idx is the De Bruijn index i.e. and index of 0 points to the last variable and an index of count gamma - 1 points to the first variable.

val definition_term : int -> t -> Term.t option

definition_term idx gamma

If the variable idx has a definition, then return it. Otherwise return None.

val context : t -> Gamma.t

val expand : Term.t -> t -> Term.t

val is_hole : int -> t -> bool

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

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

val fold_entries : 
  (int -> int -> string -> Term.typ -> bool -> Term.t option -> 'a -> 'a) ->
  t ->
  'a ->
  'a