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.S
with type key = var
Hashtbl
with variables as keys.
val create_universal : int -> var
val create_parametric : int -> var
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).
var
into an indicator variable.var
into a non-indicator variable.val id_of_var : var -> int
val hash_of_var : var -> int
val is_universal : var -> bool
val is_parametric : var -> bool
val equal : var -> var -> bool
val compare : var -> var -> int
val to_string : var -> string
var
with id
isid
for a universal variableid
for a parameter
and a * as an additional prefix for an indicator variable.