Module Value.Sort

Value Sorts.

A concrete and extensible representation of a value sort. The sort usually holds the static information about the value representation, like the width of a bitvector, the representation format of a floating point number, and so on.

This module is mostly needed when a new sort is defined. The Core Theory provides a predefined collection of sorts, here is the list:

This module defines a simple DSL for specifying sorts, the DSL grammar is made only from three rules:

           sort = sym | int | sort(sort)

The DSL is embedded into the host language with an infix operator @-> for application, e.g., OCaml grammar for sorts is:

v sort = sym exp | int exp | sort "@->" sort exp = ?a valid OCaml expression? v

Both symbols and numbers are indexed with a type index, which serves as a witness of the sort value, e.g.,

type int8
let int8 : int8 num sort = Sort.int 8

Type indices enable explicit reflection of the target language type system in the host type system, while still keeping the typing rules under designer's control.

As a working example, let's develop a sort for binary fixed-point numbers. We need to encode the type of the underlying bitvector as well as the scaling factor. Suppose, we chose to encode the scaling factor by an integer position of the point, e.g., 8 means scaling factor 2^8, i.e., a point fixed on 8th bit from the left.

The syntax of our sort will be Fixpoint(<num>,BitVec(<num>)), but we will keep it private to enable further extensions. The structure of the sort is explicitly captured in its type, in our case, it will be 'p num -> 's Bitv.t -> fixpoint sym, but since we want to keep it is hidden by our type ('p,'s) t. The same as with the built-in Bitv and Mem sorts.

We declare a fixpoint constructor and keep it private, to ensure that only we can construct (and refine) fixpoint sorts. Since the sort type is abstract, we also need to provide functions that access arguments of our sort.

Finally, we need to provide the refine function, that will cast an untyped sort to its type representation, essentially proving that the sort is a valid fixpoint sort.

module Fixpoint : sig
  type ('p, 's) t
  val define : int -> 's Bitv.t sort -> ('p,'s) t sort
  val refine : unit sort -> ('p,'s) t sort option
  val bits : ('p,'s) t sort -> 's Bitv.t sort
  val logscale : ('p,'s) t sort -> int
end = struct
  type fixpoint

  type ('m,'s) t =
    'm Value.Sort.num ->
    's Bitv.t ->
    fixpoint Value.Sort.sym

  let fixpoint = Value.Sort.Name.declare "FixPoint"

  let define p s = Value.Sort.(int p @-> s @-> sym fixpoint)
  let refine s = Value.Sort.refine fixpoint s
  let bits s = Value.Sort.(hd (tl s))
  let logscale s = Value.Sort.(hd s)
end

(* Example of usage: *)


type ('m,'s) fixpoint = Fixpoint.t Value.sort

type u32              (* type index for 32 bit ints *)
type p8               (* type index for points at 8th bit *)

(* a sort of 32-bit bitvectors, usually provided by the CPU model *)
let u32 : u32 Bitv.t Value.sort = Bitv.define 32

(* a sort of 8.32 fixed-point numbers. *)
let fp8_32 : (p8,u32) fixpoint = Fixpoint.define 8 u32
type +'a t = 'a sort
type +'a sym
type +'a num
type name
val sym : name -> 'a sym sort

sym name constructs a sort with the given name.

A symbolic sort could represent an abstract data type with no further information available, e.g., some machine status word of unknown size or representation; it may also be used to denote data with obvious representation, e.g., the Bool sort; finally, a symbolic sort could be used as a constructor name for an indexed sort, e.g., (BitVec(width)).

See the Example in the module description for more information.

val int : int -> 'a num sort

int x a numeric sort.

While it is possible to create a standalone numeric sort, it wouldn't be possible to refine it, since only symbolic sorts re refinable.

Numeric sorts are used mostly as parameters. See the Example section of the module documentation for more information.

val app : 'a sort -> 'b sort -> ('a -> 'b) sort

app s1 s2 constructs a sort of sort s1 and s2.

An application could be seen as a tuple building operators, thus this operation defines a sort that is described by two other sorts.

Basically, the app operator builds a heterogenous list, with elements which should be other sorts. The list could be then traversed using the Sort.hd and Sort.tl operators, and individual elements could be read with the value and name operators. Since the structure of the sort is fully encoded in this type, those operations are total.

val (@->) : 'a sort -> 'b sort -> ('a -> 'b) sort

s1 @-> s2 is app s1 s2

val value : 'a num sort -> int

value s returns the number associated with the numeric sort.

val name : 'a sym sort -> name

name s returns the symbol associated with a symbolic sort

val hd : ('a -> 'b) sort -> 'a sort

hd s the first argument of sort s

val tl : ('a -> 'b) sort -> 'b sort

tl the list of arguments of sort s excluding the first one

val refine : name -> unit sort -> 'a t option

refine witness s restores the type of the sort.

The sort type is an index type which could be lost, e.g., when the forget function is applied or when the sort is stored and read from its textual representation.

The refine function will re-instantiate the type index if the constructor name of the sort s is the name.

This function gives a mandate for the refine function to index the sort s with any type, which will breach the sort type safety, therefore this function should be used with care and be hidden behind the abstraction barrier and have a concrete type.

See the Example section in the module documentation for the demonstration of how refine should be used.

val forget : 'a t -> unit t

forget s forgets the type index associated with the sort s.

This is effectively an upcasting function, that could be used when the typing information is not necessary anymore or is not representable. The type index could be later restored with the refine function.

val same : 'a t -> 'b t -> bool

same x y is true if x and y are of the same structure.

val pp : Core_kernel.Caml.Format.formatter -> 'a t -> unit

prints the sort.

module Top : sig ... end

Sorts with erased type indices.

module Name : sig ... end

The name registry.