Project

General

Profile

Download (1.93 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
19 75c459f4 Lélio Brun
type mc_formula_t = value_t formula_t
20
21 8446bf03 ploc
type instr_t =
22
  {
23
    instr_desc: instr_t_desc; (* main data: the content *)
24
    (* lustre_expr: expr option; (* possible representation as a lustre expression *) *)
25
    lustre_eq: eq option;     (* possible representation as a lustre flow equation *)
26 75c459f4 Lélio Brun
    instr_spec: mc_formula_t
27 8446bf03 ploc
  }
28
and instr_t_desc =
29
  | MLocalAssign of var_decl * value_t
30
  | MStateAssign of var_decl * value_t
31
  | MReset of ident
32
  | MNoReset of ident
33
  | MStep of var_decl list * ident * value_t list
34
  | MBranch of value_t * (label * instr_t list) list
35
  | MComment of string
36 1fd3d002 ploc
  | MSpec of string 
37 089f94be ploc
38 f4cba4b8 ploc
type step_t = {
39
    step_checks: (Location.t * value_t) list;
40
    step_inputs: var_decl list;
41
    step_outputs: var_decl list;
42
    step_locals: var_decl list;
43
    step_instrs: instr_t list;
44
    step_asserts: value_t list;
45
  }
46 089f94be ploc
47
type static_call = top_decl * (Dimension.dim_expr list)
48
49 6cbbe1c1 Lélio Brun
type mc_transition_t = value_t transition_t
50
51 7ee5f69e Lélio Brun
type machine_spec = {
52
  mnode_spec: node_spec_t option;
53 6cbbe1c1 Lélio Brun
  mtransitions: mc_transition_t list
54 7ee5f69e Lélio Brun
}
55 f4cba4b8 ploc
  
56 089f94be ploc
type machine_t = {
57
  mname: node_desc;
58
  mmemory: var_decl list;
59
  mcalls: (ident * static_call) list; (* map from stateful/stateless instance to node, no internals *)
60
  minstances: (ident * static_call) list; (* sub-map of mcalls, from stateful instance to node *)
61
  minit: instr_t list;
62
  mstatic: var_decl list; (* static inputs only *)
63
  mconst: instr_t list; (* assignments of node constant locals *)
64
  mstep: step_t;
65 7ee5f69e Lélio Brun
  mspec: machine_spec;
66 089f94be ploc
  mannot: expr_annot list;
67 95fb046e ploc
  msch: Scheduling_type.schedule_report option; (* Equations scheduling *)
68 089f94be ploc
}