Project

General

Profile

Download (2.08 KB) Statistics
| Branch: | Tag: | Revision:
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
}