| 1 |
8446bf03
|
ploc
|
(************ Machine code types *************)
|
| 2 |
|
|
open Lustre_types
|
| 3 |
7ee5f69e
|
Lélio Brun
|
open Spec_types
|
| 4 |
75c459f4
|
Lélio Brun
|
|
| 5 |
8446bf03
|
ploc
|
type value_t =
|
| 6 |
|
|
{
|
| 7 |
|
|
value_desc: value_t_desc;
|
| 8 |
|
|
value_type: Types.type_expr;
|
| 9 |
|
|
value_annot: expr_annot option
|
| 10 |
|
|
}
|
| 11 |
|
|
and value_t_desc =
|
| 12 |
|
|
| Cst of constant
|
| 13 |
c35de73b
|
ploc
|
| Var of var_decl
|
| 14 |
8446bf03
|
ploc
|
| Fun of ident * value_t list
|
| 15 |
|
|
| Array of value_t list
|
| 16 |
|
|
| Access of value_t * value_t
|
| 17 |
|
|
| Power of value_t * value_t
|
| 18 |
c4780a6a
|
Lélio Brun
|
| ResetFlag
|
| 19 |
8446bf03
|
ploc
|
|
| 20 |
75c459f4
|
Lélio Brun
|
type mc_formula_t = value_t formula_t
|
| 21 |
|
|
|
| 22 |
8446bf03
|
ploc
|
type instr_t =
|
| 23 |
|
|
{
|
| 24 |
|
|
instr_desc: instr_t_desc; (* main data: the content *)
|
| 25 |
|
|
(* lustre_expr: expr option; (* possible representation as a lustre expression *) *)
|
| 26 |
|
|
lustre_eq: eq option; (* possible representation as a lustre flow equation *)
|
| 27 |
6d1693b9
|
Lélio Brun
|
instr_spec: mc_formula_t list
|
| 28 |
8446bf03
|
ploc
|
}
|
| 29 |
|
|
and instr_t_desc =
|
| 30 |
|
|
| MLocalAssign of var_decl * value_t
|
| 31 |
|
|
| MStateAssign of var_decl * value_t
|
| 32 |
c4780a6a
|
Lélio Brun
|
| MResetAssign of bool
|
| 33 |
6d1693b9
|
Lélio Brun
|
| MClearReset
|
| 34 |
|
|
| MSetReset of ident
|
| 35 |
8446bf03
|
ploc
|
| MNoReset of ident
|
| 36 |
|
|
| MStep of var_decl list * ident * value_t list
|
| 37 |
|
|
| MBranch of value_t * (label * instr_t list) list
|
| 38 |
|
|
| MComment of string
|
| 39 |
1fd3d002
|
ploc
|
| MSpec of string
|
| 40 |
089f94be
|
ploc
|
|
| 41 |
f4cba4b8
|
ploc
|
type step_t = {
|
| 42 |
|
|
step_checks: (Location.t * value_t) list;
|
| 43 |
|
|
step_inputs: var_decl list;
|
| 44 |
|
|
step_outputs: var_decl list;
|
| 45 |
|
|
step_locals: var_decl list;
|
| 46 |
|
|
step_instrs: instr_t list;
|
| 47 |
|
|
step_asserts: value_t list;
|
| 48 |
|
|
}
|
| 49 |
089f94be
|
ploc
|
|
| 50 |
|
|
type static_call = top_decl * (Dimension.dim_expr list)
|
| 51 |
|
|
|
| 52 |
6cbbe1c1
|
Lélio Brun
|
type mc_transition_t = value_t transition_t
|
| 53 |
6d1693b9
|
Lélio Brun
|
type mc_memory_pack_t = value_t memory_pack_t
|
| 54 |
6cbbe1c1
|
Lélio Brun
|
|
| 55 |
7ee5f69e
|
Lélio Brun
|
type machine_spec = {
|
| 56 |
|
|
mnode_spec: node_spec_t option;
|
| 57 |
6d1693b9
|
Lélio Brun
|
mtransitions: mc_transition_t list;
|
| 58 |
|
|
mmemory_packs: mc_memory_pack_t list
|
| 59 |
7ee5f69e
|
Lélio Brun
|
}
|
| 60 |
f4cba4b8
|
ploc
|
|
| 61 |
089f94be
|
ploc
|
type machine_t = {
|
| 62 |
|
|
mname: node_desc;
|
| 63 |
|
|
mmemory: var_decl list;
|
| 64 |
|
|
mcalls: (ident * static_call) list; (* map from stateful/stateless instance to node, no internals *)
|
| 65 |
|
|
minstances: (ident * static_call) list; (* sub-map of mcalls, from stateful instance to node *)
|
| 66 |
|
|
minit: instr_t list;
|
| 67 |
|
|
mstatic: var_decl list; (* static inputs only *)
|
| 68 |
|
|
mconst: instr_t list; (* assignments of node constant locals *)
|
| 69 |
|
|
mstep: step_t;
|
| 70 |
7ee5f69e
|
Lélio Brun
|
mspec: machine_spec;
|
| 71 |
089f94be
|
ploc
|
mannot: expr_annot list;
|
| 72 |
95fb046e
|
ploc
|
msch: Scheduling_type.schedule_report option; (* Equations scheduling *)
|
| 73 |
089f94be
|
ploc
|
}
|