package rfsm

The type of guest-level type expressions, denoting types

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.

pp_type_expr fmt te prints type expression te on formatter fmt.

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

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

pp_type_decl fmt td prints type declaration td on formatter fmt.

The type of guest-level expressions

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

pp_expr fmt e prints expression e on formatter fmt.

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 := ...).

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

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

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).

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.

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.

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.

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

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

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

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

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.

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

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

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

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