Project

General

Profile

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

    
5
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
  | 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

    
19
type mc_formula_t = value_t formula_t
20

    
21
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
    instr_spec: mc_formula_t list
27
  }
28
and instr_t_desc =
29
  | MLocalAssign of var_decl * value_t
30
  | MStateAssign of var_decl * value_t
31
  | MClearReset
32
  | MSetReset of ident
33
  | MNoReset of ident
34
  | MStep of var_decl list * ident * value_t list
35
  | MBranch of value_t * (label * instr_t list) list
36
  | MComment of string
37
  | MSpec of string 
38

    
39
type step_t = {
40
    step_checks: (Location.t * value_t) list;
41
    step_inputs: var_decl list;
42
    step_outputs: var_decl list;
43
    step_locals: var_decl list;
44
    step_instrs: instr_t list;
45
    step_asserts: value_t list;
46
  }
47

    
48
type static_call = top_decl * (Dimension.dim_expr list)
49

    
50
type mc_transition_t = value_t transition_t
51
type mc_memory_pack_t = value_t memory_pack_t
52

    
53
type machine_spec = {
54
  mnode_spec: node_spec_t option;
55
  mtransitions: mc_transition_t list;
56
  mmemory_packs: mc_memory_pack_t list
57
}
58
  
59
type machine_t = {
60
  mname: node_desc;
61
  mmemory: var_decl list;
62
  mcalls: (ident * static_call) list; (* map from stateful/stateless instance to node, no internals *)
63
  minstances: (ident * static_call) list; (* sub-map of mcalls, from stateful instance to node *)
64
  minit: instr_t list;
65
  mstatic: var_decl list; (* static inputs only *)
66
  mconst: instr_t list; (* assignments of node constant locals *)
67
  mstep: step_t;
68
  mspec: machine_spec;
69
  mannot: expr_annot list;
70
  msch: Scheduling_type.schedule_report option; (* Equations scheduling *)
71
}
(35-35/66)