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.3.tar.gz
sha256=062f33c55ef39706c4290dff67d5a00bf009051fd757f9352be527f629ae21fc
md5=eb4edc4d6b7e15b83d6397bd34994153

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

Module Alba_core.TermSource

Sourceval bruijn_convert : int -> int -> int
Sourcemodule Value : sig ... end
Sourcemodule Sort : sig ... end
Sourcemodule Lambda_info : sig ... end
Sourcemodule Pi_info : sig ... end
Sourcemodule Application_info : sig ... end
Sourcetype t =
  1. | Sort of Sort.t
  2. | Value of Value.t
  3. | Variable of int
  4. | Typed of t * typ
  5. | Appl of t * t * Application_info.t
  6. | Lambda of typ * t * Lambda_info.t
  7. | Pi of typ * typ * Pi_info.t
  8. | Where of string * typ * t * t
    (*

    Where (name, tp, exp, def) is equivalent to the beta redex Appl ( Lambda (tp, exp, "name"), def)

    *)
Sourceand typ = t
Sourceand formal_argument = string * typ
Sourceand inductive
Sourcetype t_n = t * int
Sourcetype typ_n = typ * int
Sourceval proposition : t
Sourceval any : t
Sourceval any_uni : int -> t
Sourceval variable : int -> t
Sourceval application : t -> t -> t
Sourceval implicit_application : t -> t -> t
Sourceval binary : t -> t -> t -> t
Sourceval applications : t -> t list -> t
Sourceval lambda0 : string -> bool -> typ -> t -> t
Sourceval product0 : string -> bool -> typ -> typ -> typ
Sourceval lambda : string -> typ -> t -> t
Sourceval product : string -> typ -> typ -> t
Sourceval arrow : typ -> typ -> typ
Sourceval lambda_untyped : string -> typ -> t -> t
Sourceval product_untyped : string -> typ -> typ -> t
Sourceval lambda_in : formal_argument list -> t -> t
Sourceval product_in : formal_argument list -> t -> t
Sourceval expand_where : string -> typ -> t -> t -> t

Rewrite a where block as an application with a lambda term.

Sourceval char : int -> t

char code character value.

Sourceval string : string -> t

string str string value.

Sourceval number_values : string -> t list
Sourceval type_of_sort : Sort.t -> typ
Sourceval is_sort : typ -> bool
Sourceval pi_sort : typ -> typ -> typ
Sourceval split_application : t -> t * (t * Application_info.t) list

split_application t

Sourceval map : (int -> int) -> t -> t

map f t

Map the free variables with f

Sourceval up_from : int -> int -> t -> t

up_from start delta t: increases all free variables >= start in t by delta

requires: 0 <= delta

Sourceval up : int -> t -> t

up delta t: increases all free variables in t by delta

requires: 0 <= delta

Sourceval up1 : t -> t

up1 t: increases all free variable in t by 1

Sourceval down_from : int -> int -> t -> t option

down_from start delta t: decreases all free variables >= start in t by delta if possible. Returns None it there is a free variable in t with index i < delta.

requires: 0 <= delta

Sourceval down : int -> t -> t option

down delta t: decreases all free variables in t by delta if possible. Returns None if there is a free variable in t with index i < delta.

requires: 0 <= delta

Sourceval substitute0 : (int -> t) -> bool -> t -> t

substitute0 f beta_reduce t

Sourceval substitute : (int -> t) -> t -> t

substitute f term substitutes each free variable i in term by the term f i.

Sourceval substitute_with_beta : (int -> t) -> t -> t

substitute f term substitutes each free variable i in term by the term f i and do beta reduction in case that f i appears in a function position and is a function abstraction.

Sourceval apply : t -> t -> t
Sourceval apply_nargs : t -> int -> Application_info.t -> t

apply_nargs f n mode returns

f (Var (n-1)) ... (Var 0)

where all applications are done with mode mode.

Sourceval fold_free : (int -> 'a -> 'a) -> t -> 'a -> 'a
Sourceval to_index : int -> t -> t
Sourceval to_level : int -> t -> t
Sourceval has : (int -> bool) -> t -> bool

has p term does the term have a free variable satisfying p?

Sourceval forall : (int -> bool) -> t -> bool

forall p term do all free variables in term satisfy p?

Sourceval has_variable : int -> t -> bool
Sourcemodule Monadic (M : Fmlib.Module_types.MONAD) : sig ... end

Monadic functions

Sourcemodule Inductive : sig ... end

Inductive types