Module `Abstract_syntax.Abstract_syntax`Source

Sourcetype location = Lexing.position * Lexing.position

The type of location in the signature files

Sourcetype associativity =

The type of the kind of associativity for infix operators

Sourcetype syntactic_behavior =

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

Sourcetype abstraction =

The two types of abstraction

Sourcetype term =

| Var of string * location
(*
If the term is variable (bound by a binder)
*)
| Const of string * location
(*
If the term is a constant (not bound by a binder)
*)
| 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
*)
| LAbs of string * location * term * location
(*
If the term is a linear abstraction
*)
| App of term * term * location
(*
If the term is an application
*)

The type of terms provided by the parser.

Sourceval unlinearize_term : term -> term

The type of types as found in the signature files

Sourcetype type_def =

| 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
*)
| Linear_arrow of type_def * type_def * location
(*
If the type is described with a linear abstraction
*)
| Arrow of type_def * type_def * location
(*
If the type is described with a intuitionistic abstraction
*)

Sourcetype sig_entry =

| 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
*)
| 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
*)
| 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
*)
| 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
*)

Sourceand kind =

Sourcetype lex_entry =

Install