Module Syntax.Ty

Implementation of simple types. This module exports the functor MakeSType, a Sort module of type Symb.NAME, and a concrete simple types implementation in SType.

Abstract Interface

The abstract interface for simple types is the functor MakeSType.

module MakeSType (B : Symb.NAME) : sig ... end

Functor building simple types module. It guarantees that simple types use Symb.NAME for representing sorts.

Provided Implementations

The default implementations for the type of sort and simple type.

module Sort : Symb.NAME

The provided sort module.

module SType : sig ... end

Provided simple types module.

val make_args_names : SType.ty -> string list

make_args_names t return a list of names for each argument of a type t.

Example: Given a simple type t1 -> ... -> tn -> b, the returned list is s1, ..., sn. Each si, with 1 <= i <= n, is written as exactly "xi" or "Fi" depending if the corresponding type ti is a base or arrow type.