Sigma.Make
Chunk Extension functor.
This functor promote an individual chunk type of some memory model into an uniform chunk.
module C : ChunkType
type ckind +=
| Mu of C.t
Chunk Extension.
val chunk : C.t -> chunk
Individual promotion of a model chunk to a uniform chunk.
val singleton : C.t -> domain
Promoted Domain.singleton.
Domain.singleton
val mem : sigma -> C.t -> bool
Specialized Sigma.mem, equivalent to Sigma.mem s (chunk c).
Sigma.mem
Sigma.mem s (chunk c)
val get : sigma -> C.t -> F.var
Specialized Sigma.get, equivalent to Sigma.get s (chunk c).
Sigma.get
Sigma.get s (chunk c)
val value : sigma -> C.t -> F.term
Specialized Sigma.value, equivalent to Sigma.value s (chunk c).
Sigma.value
Sigma.value s (chunk c)