bap-knowledge 2.5.0 · OCaml Package

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.

parameter public
(defaults to false) if specified, then the class will referenced in the Knowledge documentation output.

val refine : ('k, _) cls -> 's -> ('k, 's) cls

refine cls s refines the sort of class 'k to s.

val same : ('a, _) cls -> ('b, _) cls -> bool

same x y is true if x and y denote the same class k

val equal : 
  ('a, _) cls ->
  ('b, _) cls ->
  ('a obj, 'b obj) Core_kernel.Type_equal.t option

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.

val assert_equal : 
  ('a, _) cls ->
  ('b, _) cls ->
  ('a obj, 'b obj) Core_kernel.Type_equal.t

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.

parameter persistent
is an instance of the persistent class that will be used to persist the property.

parameter desc
is a property documentation.

parameter public
(defaults to false) if specified, then the property will referenced in the Knowledge documentation output.

val name : ('a, _) cls -> name

name cls is the class name.

val sort : ('k, 's) cls -> 's

sort cls returns the sort index of the class k.

package bap-knowledge