Module Abstract_syntax.Abstract_syntax

type location = Stdlib.Lexing.position * Stdlib.Lexing.position

The type of location in the signature files

type associativity =
  1. | Left
  2. | Right
  3. | NonAss

The type of the kind of associativity for infix operators

type syntactic_behavior =
  1. | Default
  2. | Prefix
  3. | Infix of associativity * float
  4. | Binder

The type of the syntactic behaviour of constants defined in the signature

type abstraction =
  1. | Linear
  2. | Non_linear

The two types of abstraction

type term =
  1. | Var of string * location
    (*

    If the term is variable (bound by a binder)

    *)
  2. | Const of string * location
    (*

    If the term is a constant (not bound by a binder)

    *)
  3. | Abs of string * location * term * location
    (*

    If the term is a intuitionistic abstraction. The first location is the one of the variable, and the second one is the one of the whole term. The latter take into account the binder if the string is the first variable bound, and starts with the string otherwise

    *)
  4. | LAbs of string * location * term * location
    (*

    If the term is a linear abstraction

    *)
  5. | App of term * term * location
    (*

    If the term is an application

    *)

The type of terms provided by the parser.

val unlinearize_term : term -> term

The type of types as found in the signature files

type type_def =
  1. | Type_atom of string * location * term list
    (*

    If the type is atomic. The third parameter is the terms to which the type is applied in case of a dependent type. The list is empty if the type does not depend on any type

    *)
  2. | Linear_arrow of type_def * type_def * location
    (*

    If the type is described with a linear abstraction

    *)
  3. | Arrow of type_def * type_def * location
    (*

    If the type is described with a intuitionistic abstraction

    *)
type sig_entry =
  1. | Type_decl of string * location * kind
    (*

    The first parameter (string) is the name of the type, the second parameter is the place in the file where it was defined and the last parameter is its kind

    *)
  2. | Type_def of string * location * type_def * kind
    (*

    Tthe first parameter (string) is the name of the defined type, the second parameter is the place in the file where it was defined and the last parameter is its value

    *)
  3. | Term_decl of string * syntactic_behavior * location * type_def
    (*

    The first parameter (string) is the name of the constant, the second parameter is the place in the file where it was defined and the last parameter is its type

    *)
  4. | Term_def of string * syntactic_behavior * location * term * type_def
    (*

    The first parameter (string) is the name of the constant, the second parameter is the place in the file where it was defined and the last parameter is its value

    *)
and kind =
  1. | K of type_def list
type lex_entry =
  1. | Type of string * location * type_def
  2. | Constant of string * location * term