module Var:universal and parameteric variablessig..end
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.
type var
module VarTable:Hashtbl.Swith type key = var
Hashtbl with variables as keys.
val create_universal : int -> varval create_parametric : int -> varval clone_renumbered : var -> int -> varVar.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).
var into an indicator variable.var into a non-indicator variable.val id_of_var : var -> intval hash_of_var : var -> intval is_universal : var -> boolval is_parametric : var -> boolval equal : var -> var -> boolval compare : var -> var -> intval to_string : var -> stringvar with id isid for a universal variableid for a parameter
and a * as an additional prefix for an indicator variable.