Module type Grammar.Mem

type t

an abstract type denoting a Core Theory memory term.

type exp

the type of expressions of the target language

val error : t

an ill-formed term.

val store : exp -> exp -> exp -> t

store s k x is store (mem s) (bitv k) (bitv x)

val store_word : exp -> exp -> exp -> exp -> t

store_word d s k x is storew (bool d) (mem s) (bitv k) (bitv x).

val var : string -> int -> int -> t

var s m n is var (ctxt s) (mems (bits m) (bits n))

val unknown : int -> int -> t

unknown m n is unk (mems (bits m) (bits n))

val ite : exp -> exp -> exp -> t

ite c x y is ite (bool c) (mem x) (mem y)

val let_bit : string -> exp -> exp -> t

let_bit s x y is scoped @@ fun v -> (bool x) (mem [y|s->v]).

Note, the let_bit rule is not mapped to the let_ term, but instead a scoped fresh variable v is created and s is substituted with v in y.

val let_reg : string -> exp -> exp -> t

let_reg s x y is scoped @@ fun v -> (bitv x) (mem [y|s->v]).

Note, the let_reg rule is not mapped to the let_ term, but instead a scoped fresh variable v is created and s is substituted with v in y.

val let_mem : string -> exp -> exp -> t

let_mem s x y is scoped @@ fun v -> (mem x) (mem [y|s->v]).

Note, the let_mem rule is not mapped to the let_ term, but instead a scoped fresh variable v is created and s is substituted with v in y.

val let_float : string -> exp -> exp -> t

let_float s x y is scoped @@ fun v -> (float x) (mem [y|s->v]).

Note, the let_float rule is not mapped to the let_ term, but instead a scoped fresh variable v is created and s is substituted with v in y.