OCaml logo

lutin

Lutin: modeling stochastic reactive systems
IN THIS PACKAGE
Module Expand

Les paramètres de l'expansion sont : -------------------------------------------------------

  • Le CheckEnv.t qui résulte du type/binding check. Il permet de retrouver le type effectif (sémantique) de toute expression source et l'info associée à toute instance d'identificateur. -------------------------------------------------------
  • Le code source (type Syntaxe.package) -------------------------------------------------------
  • Le node "main" (string) -------------------------------------------------------

Le résultat de l'expansion consiste en 3 tables indexées par des idents cibles (CoIdent.t) :

  • Table des variables (support)
  • Table des alias (d'expressions algébriques)
  1. la liste d'alias
  • Table des traces
type support_scope

Info et table des variables support

type support_nature =
| Input
| Output
| LocalIn
| LocalOut
type support_info = {
si_ident : CoIdent.t;
si_nature : support_nature;
si_type : CkTypeEff.t;
si_ref_exp : CoAlgExp.t;
si_src : CoIdent.src_stack;
si_pre_ref_exp : CoAlgExp.t option;
si_default : CoAlgExp.t option;
si_scope : support_scope option;
si_init : CoAlgExp.t option;
si_range : (CoAlgExp.t * CoAlgExp.t) option;
}
and t
val support_tab : t -> support_info Util.StringMap.t
val support_pres : t -> (CoIdent.t * support_info) list
val input_list : t -> CoIdent.t list
val output_list : t -> CoIdent.t list
val local_in_list : t -> CoIdent.t list
val local_out_list : t -> CoIdent.t list
val ident_space : t -> CoIdent.space
val node_name : t -> string
type alias_info = {
ai_type : CkTypeEff.t;
ai_def_exp : CoAlgExp.t;
ai_ref_exp : CoAlgExp.t;
ai_src : CoIdent.src_stack;
}

Info et table des alias algébriques

val alias_tab : t -> alias_info Util.StringMap.t
val alias_list : t -> CoIdent.t list
val get_run_expanded_code : t -> CoIdent.t -> t

Info et table des alias trace

type tbl = {
arg_opt : MainArg.t;
expanded_code : t;
in_vars : Exp.var list;
out_vars : Exp.var list;
loc_vars : Exp.var list;
init_pres : Value.OfIdent.t;
id2var_tab : Exp.var Util.StringMap.t;
out_var_names : string list;
bool_vars_to_gen : Exp.formula;
num_vars_to_gen : Exp.var list;
snt : Solver.t;
}
and trace_info = {
ti_def_exp : tbl CoTraceExp.t;
ti_src : CoIdent.src_stack;
}
val make : CheckEnv.t -> Syntaxe.package -> string -> t
val trace_tab : t -> trace_info Util.StringMap.t
val get_trace_info : t -> CoIdent.t -> trace_info

Info et table des externes utilisées on garde le CkIdentInfo.t tel quel pour usage ultérieur (génération de code) N.B. le source est un lexeme

type extern_info = {
xi_decl : Syntaxe.let_info;
xi_prof : CkTypeEff.profile;
xi_src : Lexeme.t;
}
val extern_tab : t -> extern_info Util.StringMap.t
val main_trace : t -> CoIdent.t

Identificateur (target) de la trace principale

val dump : t -> unit

DUMP pour debug etc.

val dump_src_ctx : t -> string