Module CoreAlgebra (.ml)

module CoreAlgebra: sig .. end

This module implements a core algebra of first order terms.

The type core algebra contains all the first order terms built using the following four symbols:

RowCons is the row constructor which appends a label to a row. RowUniform denotes the row which maps every label to a particular term. App is the application of a type to another type. Var is a type variable.

This definition is later augmented to be usable in a real programming language in MiniAlgebra.

type lname =

`\|`	`LName of string`

lname is the type of label.

module RowLabel: sig .. end

The universe of row labels.

Type as tree

type 'a term =

`\|`	`RowCons of RowLabel.t * 'a * 'a`
`\|`	`RowUniform of 'a`
`\|`	`App of 'a * 'a`
`\|`	`Var of 'a`

Terms whose parameters are of type 'a. This data structure represents a tree whose depth is exactly equal to 1.

type 'a arterm =

`\|`	`TVariable of 'a`
`\|`	`TTerm of 'a arterm term`

Terms whose parameters are either leaves of type 'a, or terms. arterm stands for ``abstract recursive term''.

Usual higher order functions

val iter : ('a -> unit) -> 'a term -> unit

iter f term applies f successively to every parameter of the term term.

val map : ('a -> 'b) -> 'a term -> 'b term

map f term returns a term whose head symbol is that of term and whose parameters are the images of term's parameters through f.

val fold : ('a -> 'b -> 'b) -> 'a term -> 'b -> 'b

fold f term accu folds f over term's parameters, using accu as initial value.

val fold2 : ('a -> 'b -> 'c -> 'c) ->
       'a term -> 'b term -> 'c -> 'c

fold2 f term term' accu folds f over term's parameters, using accu as initial value.

Type manipulation

val change_arterm_vars : ('a * 'a) list -> 'a arterm -> 'a arterm

val app : 'a arterm -> 'a arterm list -> 'a arterm

app t ts built the term corresponding to the (...((t t0) t1)... tn).

val uniform : 'a arterm -> 'a arterm

uniform t returns the row type that maps any label to t.

val rowcons : lname ->
       'a arterm -> 'a arterm -> 'a arterm

rowcons l t r returns the row type (l: t; r).

val n_rowcons : (lname * 'a arterm) list ->
       'a arterm -> 'a arterm

n_rowcons l ts r returns the row type (l0: t0; ...; ln: tn; r).