Knowledge.Class
Class is a collection of sorts.
A class k
is denoted by an indexed type (k,s) cls
, where s
is a sort.
A class denotes a set of properties that describe objects and values of the given class. Thus, a class fully defines the structure of an object or a value. Sorts could be used to further partition the class into subsets, if needed.
Classes are declarative and each class should have a unique name. To prevent name clashing the Knowledge Library employs a Common Lisp style namespaces, where each name belongs to a package.
The type index, associated with the class, should be protected by the module that declares the class. For example, it is a bad idea to use the unit
type as an index of a class.
type (+'k, 's) t = ('k, 's) cls
val declare :
?public:bool ->
?desc:string ->
?package:string ->
string ->
's ->
('k, 's) cls
declare name sort
declares a new class with the given name
and sort
index.
Since classes are declarative each new declaration creates a new class that is not equal to any other.
The package
and name
pair should be unique. If there is already a class with the given package:name
then the declaration fails.
equal x y
constructs a type witness of classes equality.
The witness could be used to cast objects of the same class, e.g.,
match equal bitv abs with
| Some t -> Object.cast t x y
| _ -> ...
Note that the equality is reflexive, so the obtained witness could be used in both direction, for upcasting and downcasting.
assert_equal x y
asserts the equality of two classes.
Usefull, in the context where the class is known for sure, (e.g., constrained by the module signature), but has to be recreated. The let T = assert_equal x y
expression, establishes a type equality between objects in the typing context, so there is no need to invoke Object.cast
.
let add : value obj -> value obj -> value obj = fun x y ->
let T = assert_equal bitv value in
x + y (* where (+) has type [bitv obj -> bitv obj -> bit obj] *)
val property :
?public:bool ->
?desc:string ->
?persistent:'p persistent ->
?package:string ->
('k, _) cls ->
string ->
'p domain ->
('k, 'p) slot
property cls name dom
declares a new property of all instances of class k
.
Each property should have a unique name. If a property with the given name was already, then the declaration fails.
The returned slot can be used to access the declarated property. If the property is expected to be public then it should be published via a library interface.
val sort : ('k, 's) cls -> 's
sort cls
returns the sort index of the class k
.