Module SocSource

Synchronous Object Components

The very last data structure. Soc.t is meant to be pretty-printed to generate, for instance, C code. It can also be interpreted (cf SocExec)

Sourcetype ident = string

ident are just strings because:

  • it's more ocamldebug-friendly
  • Name clashing issues ougth to have been fixed before
Sourcetype var = ident * Data.t
Sourcetype var_expr =
  1. | Var of var
  2. | Const of var
  3. | Field of var_expr * ident * Data.t
  4. | Index of var_expr * int * Data.t
  5. | Slice of var_expr * int * int * int * int * Data.t
Sourcetype key_opt =
  1. | Nomore
  2. | Slic of int * int * int
  3. | MemInit of var_expr
  4. | Curr of Lv6Id.long
Sourcetype key = ident * Data.t list * key_opt
Sourcetype instance = ident * key
Sourceval data_type_of_var_expr : var_expr -> Data.t
Sourcetype atomic_operation =
  1. | Assign
  2. | Method of instance * ident
  3. | Procedure of key
Sourcetype gao =
  1. | Case of ident * (ident * gao list) list * Lxm.t
  2. | Call of var_expr list * atomic_operation * var_expr list * Lxm.t
Sourcetype step_impl =
  1. | Predef
  2. | Gaol of var list * gao list
  3. | Iterator of string * key * int
  4. | Boolred of int * int * int
  5. | Condact of key * var_expr list
  6. | Extern

nb: Iterator and Boolred are removed with lv6 --expand-iterators

Sourcetype step_method = {
  1. name : ident;
  2. lxm : Lxm.t;
  3. idx_ins : int list;
  4. idx_outs : int list;
  5. impl : step_impl;
}
Sourcetype precedence = ident * ident list
Sourcetype memory =
  1. | No_mem
  2. | Mem of Data.t
  3. | Mem_hidden
Sourcetype t = {
  1. key : key;
  2. profile : var list * var list;
  3. clock_profile : (var * (var * Lv6Id.long)) list;
  4. step : step_method list;
  5. precedences : precedence list;
  6. instances : instance list;
  7. memory : memory;
  8. assertions : (Lxm.t * var) list;
}
Sourcemodule SocMap : sig ... end
Sourcetype tbl = t SocMap.t
Sourceval cpt : int ref
Sourceval make : key -> instance