rfsm 2.0 · OCaml Package

module Guest : Guest.SYNTAX

type typ = Guest.Types.typ

type expr = Guest.expr

type type_expr = Guest.type_expr

type lval = Guest.lval

type type_decl = Guest.type_decl

type program = {

type_decls : type_decl list;
fun_decls : fun_decl list;
cst_decls : cst_decl list;
models : model list;
globals : global list;
insts : inst list;

}

and model = (model_desc, typ) Annot.t

and model_desc = {

name : Ident.t;
states : state list;
params : (Ident.t * type_expr) list;
ios : (Ident.t * (io_cat * type_expr)) list;
inps : (Ident.t * type_expr) list;
outps : (Ident.t * type_expr) list;
inouts : (Ident.t * type_expr) list;
vars : (Ident.t * type_expr) list;
trans : transition list;
itrans : itransition;

}

and io_cat =

| In
| Out
| InOut

and state = (state_desc, unit) Annot.t

and state_desc = Ident.t * (Ident.t * expr) list

and cond = (cond_desc, typ) Annot.t

and cond_desc = Ident.t * expr list

and action = (action_desc, typ) Annot.t

and action_desc =

| Emit of Ident.t
| Assign of lval * expr

and transition = (transition_desc, typ) Annot.t

and transition_desc = Ident.t * cond * action list * Ident.t * int

and itransition = (itransition_desc, typ) Annot.t

and itransition_desc = Ident.t * action list

and global = (global_desc, typ) Annot.t

and global_desc = Ident.t * global_cat * type_expr * stimulus option

and global_cat =

| Input
| Output
| Shared

and stimulus = (stimulus_desc, typ) Annot.t

and stimulus_desc =

| Periodic of int * int * int
| Sporadic of int list
| Value_change of (int * expr) list

and inst = (inst_desc, typ) Annot.t

and inst_desc = Ident.t * Ident.t * expr list * Ident.t list

and fun_decl = (fun_decl_desc, typ) Annot.t

and fun_decl_desc = {

ff_name : Ident.t;
ff_args : (Ident.t * type_expr) list;
ff_res : type_expr;
ff_body : expr;

}

and cst_decl = (cst_decl_desc, typ) Annot.t

and cst_decl_desc = {

cc_name : Ident.t;
cc_typ : type_expr;
cc_val : expr;

}

val empty_program : program

val add_program : program -> program -> program

val subst_model_io : phi:Ident.t Subst.t -> model -> model

val subst_model_param : phi:expr Subst.t -> model -> model

val state_ios : 
  model ->
  Ident.t ->
  Ident.t list * Ident.t list * Ident.t list * Ident.t list

val normalize_model : model -> model

val ppr_program : program -> program

val pp_typ : Format.formatter -> typ -> unit

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

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

val pp_cond_desc : Format.formatter -> cond_desc -> unit

val pp_cond : Format.formatter -> cond -> unit

val ppf_cond : Format.formatter -> cond -> unit

val pp_action : Format.formatter -> action -> unit

val pp_action_desc : Format.formatter -> action_desc -> unit

val pp_transition : Format.formatter -> transition -> unit

val ppf_transition : Format.formatter -> transition -> unit

val pp_transition_desc : Format.formatter -> transition_desc -> unit

val pp_itransition : Format.formatter -> itransition -> unit

val pp_itransition_desc : Format.formatter -> itransition_desc -> unit

val pp_stimulus : Format.formatter -> stimulus -> unit

val pp_stimulus_desc : Format.formatter -> stimulus_desc -> unit

val pp_state : Format.formatter -> state -> unit

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

val pp_model : Format.formatter -> model -> unit

val pp_model_desc : Format.formatter -> model_desc -> unit

val pp_model_name : Format.formatter -> model -> unit

val pp_global : Format.formatter -> global -> unit

val pp_cst_decl : Format.formatter -> cst_decl -> unit

val pp_fun_decl : Format.formatter -> fun_decl -> unit

val pp_program : Format.formatter -> program -> unit

package rfsm