Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/machine_code_types.ml
2 2
open Lustre_types
3 3
open Spec_types
4 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
  }
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 11
and value_t_desc =
12 12
  | Cst of constant
13 13
  | Var of var_decl
......
19 19

  
20 20
type mc_formula_t = value_t formula_t
21 21

  
22
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
    instr_spec: mc_formula_t list
28
  }
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

  
29 32
and instr_t_desc =
30 33
  | MLocalAssign of var_decl * value_t
31 34
  | MStateAssign of var_decl * value_t
......
36 39
  | MStep of var_decl list * ident * value_t list
37 40
  | MBranch of value_t * (label * instr_t list) list
38 41
  | MComment of string
39
  | MSpec of string 
42
  | MSpec of string
40 43

  
41 44
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
  }
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
}
49 52

  
50
type static_call = top_decl * (Dimension.dim_expr list)
53
type static_call = top_decl * Dimension.dim_expr list
51 54

  
52 55
type mc_transition_t = value_t transition_t
56

  
53 57
type mc_memory_pack_t = value_t memory_pack_t
54 58

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

  
61 65
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
  mspec: machine_spec;
71
  mannot: expr_annot list;
72
  msch: Scheduling_type.schedule_report option; (* Equations scheduling *)
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 *)
73 81
}

Also available in: Unified diff