package rfsm

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Legend:
Library
Module
Module type
Parameter
Class
Class type

Actions associated to transitions

type t =

and lhs = {

}

and lhs_desc =

| LhsVar of string
(*
v := ...
*)
| LhsArrInd of string * Expr.t
(*
vi := ... when v is an array
*)
| LhsArrRange of string * Expr.t * Expr.t
(*
vhi:lo := ... when v is an int
*)
| LhsRField of string * string
(*
v.field_name when v has a record type
*)

val mk_lhs : string -> lhs

val lhs_name : lhs -> string

val vars_of : t -> Expr.VarSet.t * Expr.VarSet.t

vars_of a returns the name of the variables read (resp. written) by action a

val rename : (string -> string) -> t -> t

rename f a renames f v each variable v occurring in a

val subst : Eval.env -> t -> t

subst env a replaces each variable v occuring in a by its value if found in env, simplifying the resulting expression whenever possible.

val string_of_lhs : lhs -> string

val to_string : t -> string