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.4.tar.gz
sha256=4817038301d3e45bac9edf7e6f2fc8bf0a6d78e76e02ad7ea33ef69bcc17df3b
md5=25234357587126685d64f16236167937

doc/alba.core/Alba_core/Gamma_algo/Make/index.html

Module Gamma_algo.Make

Parameters

module Gamma : GAMMA

Signature

val type_of_term : Term.t -> Gamma.t -> Term.typ

type_of_term term gamma

Compute the type of term

Precondition: term must be welltyped and the context valid.

val split_type : Term.typ -> Gamma.t -> (Term.Pi_info.t * Term.typ) list * Term.typ
val split_kind : Term.typ -> Gamma.t -> ((Term.Pi_info.t * Term.typ) list * Sort.t) option

split_kind k gamma:

Compute the arguments and the sort of the kind k. If typ does not reduce to a kind, then return None.

Precondition: k must be welltyped and the context gamma must be valid.

A kind has the form

all (x: A) (y: B) .... : s

where s is a sort.

val sort_of_kind : Term.typ -> Gamma.t -> Sort.t option

sort_of_kind typ gamma

Compute the sort of the kind typ. If typ does not reduce to a kind, then return None.

Precondition: typ must be welltyped and the context gamma must be valid.

A kind has the form

all (x: A) (y: B) .... : s

where s is a sort.

val is_kind : Term.typ -> Gamma.t -> bool

is_kind typ gamma

Is the welltyped term typ in the valid context gamma a kind?

val key_split : Term.t -> Gamma.t -> Term.t * (Term.t * Term.Application_info.t) list
val key_normal : Term.t -> Gamma.t -> Term.t

keynormal term gamma

Compute the key normal form of the welltyped term term in the valid context gamma.

val normalize_pi : Term.typ -> Gamma.t -> Term.typ

normalize_pi typ gamma

Precondition:

typ must be a valid type

Result: typ is expanded until the form

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

is reached where R cannot be expanded further into a product type.

val normalize : Term.t -> Gamma.t -> Term.t

normalize term gamma

Compute the normal form of the welltyped term term in the valid context gamma.

val check_naming_convention : string -> Term.typ -> Gamma.t -> (unit, name_violation) result