Project

General

Profile

Download (2.08 KB) Statistics
| Branch: | Tag: | Revision:
1
(************ Machine code types *************)
2
open Lustre_types
3
open Spec_types
4

    
5
type value_t = {
6
  value_desc : value_t_desc;
7
  value_type : Types.type_expr;
8
  value_annot : expr_annot option;
9
}
10

    
11
and value_t_desc =
12
  | Cst of constant
13
  | Var of var_decl
14
  | 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
  | ResetFlag
19

    
20
type mc_formula_t = value_t formula_t
21

    
22
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
and instr_t_desc =
33
  | MLocalAssign of var_decl * value_t
34
  | MStateAssign of var_decl * value_t
35
  | MResetAssign of bool
36
  | MClearReset
37
  | MSetReset of ident
38
  | 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
  | MSpec of string
43

    
44
type step_t = {
45
  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

    
53
type static_call = top_decl * Dimension.dim_expr list
54

    
55
type mc_transition_t = value_t transition_t
56

    
57
type mc_memory_pack_t = value_t memory_pack_t
58

    
59
type machine_spec = {
60
  mnode_spec : node_spec_t option;
61
  mtransitions : mc_transition_t list;
62
  mmemory_packs : mc_memory_pack_t list;
63
}
64

    
65
type machine_t = {
66
  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
}
(35-35/66)