Module Var (.ml)


module Var: sig .. end
universal and parameteric variables

Variable is an ambiguous term in the context of the model evolution calculus, as there exist the usual universal variables, and special variables called parameters. Thus variables might be used to talk only about universal variables, but also to talk about universal variables and parameters. This ambiguity is from case to case clarified by context or explicit naming.

Note: the substitution tree module is not supported for the time being. The term indexing provided by the module Substitution_tree needs another type differentiation. Here, a variable may also be an indicator variable. This is orthogonal to universal and parametric.

A variable is identified by an identification number. Thus two variables are considered to be equal if they are of the same type (universal or parameteric, indicator or non-indicator) and if they have the same id.



Types

type var 
a universal variable or a parameter
module VarTable: Hashtbl.S  with type key = var
a specialized Hashtbl with variables as keys.

Functions


Creation


val create_universal : int -> var
creation of a universal variable by id.
val create_parametric : int -> var
creation of a parametric variable by id.

creation of a universal indicator variable by id.

creation of a parametric indicator variable by id.
val clone_renumbered : var -> int -> var
Var.clone_renumbered var id creates a variable of the same type (i.e. variable or parameter) as var with the new id id.

(Just a shortcut for the combination of Var.is_universal with Var.create_universal resp. Var.is_parametric with Var.create_parametric). (Used e.g. in term normalization).


transforms var into an indicator variable.

transforms var into a non-indicator variable.

Decomposition


val id_of_var : var -> int
retrieval of a variable's id.
val hash_of_var : var -> int
a good hash value for a variable.
val is_universal : var -> bool
is this a universal variable?
val is_parametric : var -> bool
is this a parametric variable?

is this an indicator variable?

Comparison


val equal : var -> var -> bool
see module description above.
val compare : var -> var -> int
total order.

Representation


val to_string : var -> string
the string representation of var with id is