package rfsm

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Types = Types

Type expressions

type type_expr = (type_expr_desc, Types.typ) Annot.t
and type_expr_desc

The type of guest-level type expressions, denoting types

val is_bool_type : type_expr -> bool
val is_event_type : type_expr -> bool
val is_array_type : type_expr -> bool

is_xxx_type te should return true iff the type denoted by te is xxx. Returns false if the guest language has no such type.

val pp_type_expr : Stdlib.Format.formatter -> type_expr -> unit

pp_type_expr fmt te prints type expression te on formatter fmt.

Type declarations

type type_decl = (type_decl_desc, Types.typ) Annot.t
and type_decl_desc

The type of guest-level type declarations (ex: type aliases, records, ...)

val mk_alias_type_decl : Ident.t -> type_expr -> type_decl

mk_alias_type_decl name te should return an alias type declaration, i.e. the type declaration making name a synonym for te.

val pp_type_decl : Stdlib.Format.formatter -> type_decl -> unit

pp_type_decl fmt td prints type declaration td on formatter fmt.

Expressions

type expr = (expr_desc, Types.typ) Annot.t
and expr_desc

The type of guest-level expressions

val vars_of_expr : expr -> Ident.t list

vars_of_expr e should return the list of variables occuring in expression e.

val pp_expr : Stdlib.Format.formatter -> expr -> unit

pp_expr fmt e prints expression e on formatter fmt.

L-Values

type lval_desc

The type of l-values, occuring at the left of the := symbol in assignations. A guest language will typically have variables as l-values but can also support more elaborated forms, such as array indices (ex: a[i]:=...) or record fields (ex: r.f := ...).

val mk_simple_lval : Ident.t -> lval

mk_simple_lval name should return the l-value designating a simple variable with name name.

val is_simple_lval : lval -> bool

is_simple_lval l should return true iff l-value l is a simple variable

val lval_base_name : lval -> Ident.t

lval_base_name l should return the base name of l-value l. If l is a simple variable, this is simply its name. For array or record access, this will typically the name of target array (resp. record).

val lval_prefix : string -> lval -> lval

lval_prefix p l should return the l-value obtained by adding prefix "p." to the base name of l-value l. For example, if l is a simple variable named "v", lval_prefix "foo" l is the "foo.v". This function is used to generated name scopes when dumping VCD traces.

val lval_vcd_repr : lval -> Ident.t

lval_vcd_repr l should return a representation of l-value l to be used in a VCD trace file. If l is a simple variable, this is simply its name. Other cases will depend on the l-value definition and the version of VCD format used. See for example the definition of lval_vcd_repr for the full guest language.

val vars_of_lval : lval -> Ident.t list

vars_of_lval l should return the list of variables occuring in l-value l. This includes simple variables but also the name of the target array, record, etc.

val pp_lval : Stdlib.Format.formatter -> lval -> unit

pp_lval fmt l prints l-value l on formatter fmt.

val pp_qual_lval : Stdlib.Format.formatter -> lval -> unit

Same as pp_lval but with an indication of the Ident.scope of the l-value

Substitutions

val subst_expr : Ident.t Subst.t -> expr -> expr

subst_id phi e applies substitution phi to expression e, substituting each occurrence of identifier id by identifier phi id

val subst_lval : Ident.t Subst.t -> lval -> lval

subst_lval phi l applies substitution phi to l-value l, substituting each occurrence of identifier id by identifier phi id

val subst_param_type_expr : expr Subst.t -> type_expr -> type_expr

subst_type_expr phi te applies substitution phi to type_expression te, replacing all occurences of parameter name id in type expression te by phi id.

val subst_param_expr : expr Subst.t -> expr -> expr

subst_expr phi e applies substitution phi to expression e, substituting each occurrence of parameter name id by expression phi id

Pre-processing

type ppr_env = type_expr Env.t

Since pre-processing takes place at the syntax level, before typing, type information has to be provided explicitely by mapping identifiers to type expressions.

val ppr_expr : ppr_env -> ?expected_type:type_expr option -> expr -> expr

ppr_expr env e should return the result of pre-processing expression e in env env. The optional argument expected_type can be used to perform type-dependent transformations. A typical usage is to rewrite 0 (resp 1) as false (resp. true). See guests/core/lib/syntax.ml for example

val ppr_lval : ppr_env -> lval -> lval

ppr_lval env e should return the result of pre-processing l-value e in env env.

OCaml

Innovation. Community. Security.