Project

General

Profile

Download (2.07 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 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
}