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