Module Object.Make

Parameters

Signature

val create : Kind.t -> t Machine.t

create kind creates a fresh new object identifier with the specified kind.

The created value is never equal to any value created before in the given machine. And the same kind can be shared by several different objects. Thus create establishes a surjection of objects onto the set of their kinds, i.e., it partitions the set of objects.

val kind : t -> Kind.t Machine.t

kind obj returns the kind of the object.

include Value with type t := t and type 'a m := 'a Machine.t

to_value x injects x into the value domain

of_value v project the value v to the abstract domain of t