Project

General

Profile

« Previous | Next » 

Revision a7062da6

Added by LĂ©lio Brun over 3 years ago

another step towards refactoring

View differences:

src/backends/Ada/ada_backend_adb.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11

  
12
open Utils
12 13
open Format
13 14
open Machine_code_types
14 15
open Lustre_types
......
20 21
open Ada_backend_common
21 22

  
22 23
(** Main module for generating packages bodies **)
23
module Main = struct
24
  (** Printing function for basic assignement [var := value].
25 24

  
26
      @param fmt the formater to print on @param var_name the name of the
27
      variable @param value the value to be assigned **)
28
  let pp_assign env fmt var value =
29
    fprintf fmt "%a := %a" (pp_var env) var (pp_value env) value
25
(** Printing function for basic assignement [var := value].
30 26

  
31
  (** Printing function for instruction. See {!type:Machine_code_types.instr_t}
32
      for more details on machine types.
27
    @param fmt the formater to print on @param var_name the name of the
28
    variable @param value the value to be assigned **)
29
let pp_assign env fmt var value =
30
  fprintf fmt "%a := %a" (pp_var env) var (pp_value env) value
33 31

  
34
      @param typed_submachines list of all typed machine instances of this
35
      machine @param machine the current machine @param fmt the formater to
36
      print on @param instr the instruction to print **)
37
  let rec pp_machine_instr typed_submachines env instr fmt =
38
    let pp_instr = pp_machine_instr typed_submachines env in
39
    (* Print args for a step call *)
40
    let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in
41
    (* Print a when branch of a case *)
42
    let pp_when (cond, instrs) fmt =
43
      fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs)
44
    in
45
    (* Print a case *)
46
    let pp_case fmt (g, hl) =
47
      fprintf fmt "case %a is@,%aend case" (pp_value env) g pp_block
48
        (List.map pp_when hl)
49
    in
50
    (* Print a if *)
51
    (* If neg is true the we must test for the negation of the condition. It
52
       first check that we don't have a negation and a else case, if so it
53
       inverses the two branch and remove the negation doing a recursive call. *)
54
    let pp_if fmt (neg, g, instrs1, instrs2) =
55
      let pp_cond =
56
        if neg then fun fmt x -> fprintf fmt "! (%a)" (pp_value env) x
57
        else pp_value env
58
      in
59
      let pp_else =
60
        match instrs2 with
61
        | None ->
62
          fun fmt -> fprintf fmt ""
63
        | Some i2 ->
64
          fun fmt -> fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
65
      in
66
      fprintf fmt "if %a then@,%a%tend if" pp_cond g pp_block
67
        (List.map pp_instr instrs1)
68
        pp_else
69
    in
70
    match get_instr_desc instr with
71
    (* no reset *)
72
    | MNoReset _ ->
73
      ()
74
    (* TODO: handle clear_reset *)
75
    | MClearReset ->
76
      ()
77
    (* reset *)
78
    | MSetReset i when List.mem_assoc i typed_submachines ->
79
      let substitution, submachine = get_instance i typed_submachines in
80
      let pp_package =
81
        pp_package_name_with_polymorphic substitution submachine
82
      in
83
      let args =
84
        if is_machine_statefull submachine then [ [ pp_state i ] ] else []
85
      in
86
      pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
87
    | MLocalAssign (ident, value) ->
88
      pp_assign env fmt ident value
89
    | MStateAssign (ident, value) ->
90
      pp_assign env fmt ident value
91
    | MStep ([ i0 ], i, vl) when is_builtin_fun i ->
92
      let value = mk_val (Fun (i, vl)) i0.var_type in
93
      pp_assign env fmt i0 value
94
    | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
95
      let substitution, submachine = get_instance i typed_submachines in
96
      let pp_package =
97
        pp_package_name_with_polymorphic substitution submachine
98
      in
99
      let input = List.map (fun x fmt -> pp_value env fmt x) vl in
100
      let output = List.map pp_var_name il in
101
      let args =
102
        (if is_machine_statefull submachine then [ [ pp_state i ] ] else [])
103
        @ (if input != [] then [ input ] else [])
104
        @ if output != [] then [ output ] else []
105
      in
106
      pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)
107
    | MBranch (_, []) ->
108
      assert false
109
    | MBranch (g, (c1, i1) :: tl) when c1 = tag_false || c1 = tag_true ->
110
      pp_if fmt (build_if g c1 i1 tl)
111
    | MBranch (g, hl) ->
112
      pp_case fmt (g, hl)
113
    | MComment s ->
114
      let lines = String.split_on_char '\n' s in
115
      fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines
116
    | _ ->
117
      assert false
32
(** Printing function for instruction. See {!type:Machine_code_types.instr_t}
33
    for more details on machine types.
118 34

  
119
  (** Print the definition of the step procedure from a machine.
120

  
121
      @param typed_submachines list of all typed machine instances of this
122
      machine @param fmt the formater to print on @param machine the machine **)
123
  let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
124
    let transform_local_to_state_assign instr =
125
      match instr.instr_desc with
126
      | MLocalAssign (ident, value) ->
127
        { instr with instr_desc = MStateAssign (ident, value) }
128
      | _ ->
129
        instr
35
    @param typed_submachines list of all typed machine instances of this
36
    machine @param machine the current machine @param fmt the formater to
37
    print on @param instr the instruction to print **)
38
let rec pp_machine_instr typed_submachines env instr fmt =
39
  let pp_instr = pp_machine_instr typed_submachines env in
40
  (* Print args for a step call *)
41
  let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in
42
  (* Print a when branch of a case *)
43
  let pp_when (cond, instrs) fmt =
44
    fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs)
45
  in
46
  (* Print a case *)
47
  let pp_case fmt (g, hl) =
48
    fprintf fmt "case %a is@,%aend case" (pp_value env) g pp_block
49
      (List.map pp_when hl)
50
  in
51
  (* Print a if *)
52
  (* If neg is true the we must test for the negation of the condition. It
53
     first check that we don't have a negation and a else case, if so it
54
     inverses the two branch and remove the negation doing a recursive call. *)
55
  let pp_if fmt (neg, g, instrs1, instrs2) =
56
    let pp_cond =
57
      if neg then fun fmt x -> fprintf fmt "! (%a)" (pp_value env) x
58
      else pp_value env
130 59
    in
131
    let pp_local_ghost_list, spec_instrs =
132
      match m_spec_opt with
60
    let pp_else =
61
      match instrs2 with
133 62
      | None ->
134
        [], []
135
      | Some m_spec ->
136
        ( List.map
137
            (build_pp_var_decl_local (Some (true, false, [], [])))
138
            (List.filter
139
               (fun x -> not (List.mem x.var_id guarantees))
140
               m_spec.mstep.step_locals),
141
          List.map transform_local_to_state_assign m_spec.mstep.step_instrs )
63
        fun fmt -> fprintf fmt ""
64
      | Some i2 ->
65
        fun fmt -> fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
66
    in
67
    fprintf fmt "if %a then@,%a%tend if" pp_cond g pp_block
68
      (List.map pp_instr instrs1)
69
      pp_else
70
  in
71
  match get_instr_desc instr with
72
  (* no reset *)
73
  | MNoReset _ ->
74
    ()
75
  (* TODO: handle clear_reset *)
76
  | MClearReset ->
77
    ()
78
  (* reset *)
79
  | MSetReset i when List.mem_assoc i typed_submachines ->
80
    let substitution, submachine = get_instance i typed_submachines in
81
    let pp_package =
82
      pp_package_name_with_polymorphic substitution submachine
142 83
    in
143
    let pp_local_list =
144
      List.map (build_pp_var_decl_local None) m.mstep.step_locals
84
    let args =
85
      if is_machine_statefull submachine then [ [ pp_state i ] ] else []
145 86
    in
146
    let pp_instr_list =
147
      List.map
148
        (pp_machine_instr typed_submachines env)
149
        (m.mstep.step_instrs @ spec_instrs)
87
    pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
88
  | MLocalAssign (ident, value) ->
89
    pp_assign env fmt ident value
90
  | MStateAssign (ident, value) ->
91
    pp_assign env fmt ident value
92
  | MStep ([ i0 ], i, vl) when is_builtin_fun i ->
93
    let value = mk_val (Fun (i, vl)) i0.var_type in
94
    pp_assign env fmt i0 value
95
  | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
96
    let substitution, submachine = get_instance i typed_submachines in
97
    let pp_package =
98
      pp_package_name_with_polymorphic substitution submachine
150 99
    in
151
    let content =
152
      AdaProcedureContent
153
        ( ((if pp_local_ghost_list = [] then [] else [ pp_local_ghost_list ])
154
          @ if pp_local_list = [] then [] else [ pp_local_list ]),
155
          pp_instr_list )
100
    let input = List.map (fun x fmt -> pp_value env fmt x) vl in
101
    let output = List.map pp_var_name il in
102
    let args =
103
      (if is_machine_statefull submachine then [ [ pp_state i ] ] else [])
104
      @ (if input != [] then [ input ] else [])
105
      @ if output != [] then [ output ] else []
156 106
    in
157
    pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
107
    pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)
108
  | MBranch (_, []) ->
109
    assert false
110
  | MBranch (g, (c1, i1) :: tl) when c1 = tag_false || c1 = tag_true ->
111
    pp_if fmt (build_if g c1 i1 tl)
112
  | MBranch (g, hl) ->
113
    pp_case fmt (g, hl)
114
  | MComment s ->
115
    let lines = String.split_on_char '\n' s in
116
    fprintf fmt "%a" (pp_print_list ~pp_sep:pp_print_nothing pp_oneline_comment) lines
117
  | _ ->
118
    assert false
158 119

  
159
  (** Print the definition of the reset procedure from a machine.
120
(** Print the definition of the step procedure from a machine.
160 121

  
161
      @param typed_submachines list of all typed machine instances of this
162
      machine @param fmt the formater to print on @param machine the machine **)
163
  let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
164
    let build_assign = function
165
      | var ->
166
        mkinstr (MStateAssign (var, mk_default_value var.var_type))
167
    in
168
    let env, memory =
169
      match m_spec_opt with None -> env, m.mmemory | Some _ -> env, m.mmemory
170
    in
171
    let assigns = List.map build_assign memory in
172
    let pp_instr_list =
173
      List.map (pp_machine_instr typed_submachines env) (assigns @ m.minit)
174
    in
175
    pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt
176
      (AdaProcedureContent ([], pp_instr_list))
122
    @param typed_submachines list of all typed machine instances of this
123
    machine @param fmt the formater to print on @param machine the machine **)
124
let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
125
  let transform_local_to_state_assign instr =
126
    match instr.instr_desc with
127
    | MLocalAssign (ident, value) ->
128
      { instr with instr_desc = MStateAssign (ident, value) }
129
    | _ ->
130
      instr
131
  in
132
  let pp_local_ghost_list, spec_instrs =
133
    match m_spec_opt with
134
    | None ->
135
      [], []
136
    | Some m_spec ->
137
      ( List.map
138
          (build_pp_var_decl_local (Some (true, false, [], [])))
139
          (List.filter
140
             (fun x -> not (List.mem x.var_id guarantees))
141
             m_spec.mstep.step_locals),
142
        List.map transform_local_to_state_assign m_spec.mstep.step_instrs )
143
  in
144
  let pp_local_list =
145
    List.map (build_pp_var_decl_local None) m.mstep.step_locals
146
  in
147
  let pp_instr_list =
148
    List.map
149
      (pp_machine_instr typed_submachines env)
150
      (m.mstep.step_instrs @ spec_instrs)
151
  in
152
  let content =
153
    AdaProcedureContent
154
      ( ((if pp_local_ghost_list = [] then [] else [ pp_local_ghost_list ])
155
         @ if pp_local_list = [] then [] else [ pp_local_list ]),
156
        pp_instr_list )
157
  in
158
  pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
177 159

  
178
  (** Print the package definition(ads) of a machine. It requires the list of
179
      all typed instance. A typed submachine instance is (ident, type_machine)
180
      with ident the instance name and typed_machine is (substitution, machine)
181
      with machine the machine associated to the instance and substitution the
182
      instanciation of all its polymorphic types. @param fmt the formater to
183
      print on @param typed_submachines list of all typed machine instances of
184
      this machine @param m the machine **)
185
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine))
186
      =
187
    let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
188
    let pp_reset fmt =
189
      if is_machine_statefull machine then
190
        fprintf fmt "%a;@,@,"
191
          (pp_reset_definition env typed_submachines)
192
          (machine, opt_spec_machine)
193
      else fprintf fmt ""
194
    in
195
    let aux pkgs (id, _) =
196
      try
197
        let pkg, _ = List.assoc id ada_supported_funs in
198
        if List.mem pkg pkgs then pkgs else pkg :: pkgs
199
      with Not_found -> pkgs
200
    in
201
    let packages = List.map pp_str (List.fold_left aux [] machine.mcalls) in
202
    let pp_content fmt =
203
      fprintf fmt "%t%a" (*Define the reset procedure*) pp_reset
204
        (*Define the step procedure*)
205
        (pp_step_definition env typed_submachines)
206
        (machine, opt_spec_machine, guarantees)
207
    in
208
    fprintf fmt "%a%t%a;@."
209
      (* Include all the required packages*)
210
      (Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate))
211
      packages
212
      (Utils.pp_final_char_if_non_empty ";@,@," packages)
213
      (*Print package*)
214
      (pp_package (pp_package_name machine) [] true)
215
      pp_content
216
end
160
(** Print the definition of the reset procedure from a machine.
161

  
162
    @param typed_submachines list of all typed machine instances of this
163
    machine @param fmt the formater to print on @param machine the machine **)
164
let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
165
  let build_assign = function
166
    | var ->
167
      mkinstr (MStateAssign (var, mk_default_value var.var_type))
168
  in
169
  let env, memory =
170
    match m_spec_opt with None -> env, m.mmemory | Some _ -> env, m.mmemory
171
  in
172
  let assigns = List.map build_assign memory in
173
  let pp_instr_list =
174
    List.map (pp_machine_instr typed_submachines env) (assigns @ m.minit)
175
  in
176
  pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt
177
    (AdaProcedureContent ([], pp_instr_list))
178

  
179
(** Print the package definition(ads) of a machine. It requires the list of
180
    all typed instance. A typed submachine instance is (ident, type_machine)
181
    with ident the instance name and typed_machine is (substitution, machine)
182
    with machine the machine associated to the instance and substitution the
183
    instanciation of all its polymorphic types. @param fmt the formater to
184
    print on @param typed_submachines list of all typed machine instances of
185
    this machine @param m the machine **)
186
let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine))
187
  =
188
  let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
189
  let pp_reset fmt =
190
    if is_machine_statefull machine then
191
      fprintf fmt "%a;@,@,"
192
        (pp_reset_definition env typed_submachines)
193
        (machine, opt_spec_machine)
194
    else fprintf fmt ""
195
  in
196
  let aux pkgs (id, _) =
197
    try
198
      let pkg, _ = List.assoc id ada_supported_funs in
199
      if List.mem pkg pkgs then pkgs else pkg :: pkgs
200
    with Not_found -> pkgs
201
  in
202
  let packages = List.map pp_str (List.fold_left aux [] machine.mcalls) in
203
  let pp_content fmt =
204
    fprintf fmt "%t%a" (*Define the reset procedure*) pp_reset
205
      (*Define the step procedure*)
206
      (pp_step_definition env typed_submachines)
207
      (machine, opt_spec_machine, guarantees)
208
  in
209
  fprintf fmt "%a%a;@."
210
    (* Include all the required packages*)
211
    (pp_print_list
212
       ~pp_sep:pp_print_semicolon
213
       ~pp_epilogue:(fun fmt () -> fprintf fmt ";@,@,")
214
       (pp_with AdaPrivate))
215
    packages
216
    (*Print package*)
217
    (pp_package (pp_package_name machine) [] true)
218
    pp_content
217 219

  
218 220
(* Local Variables: *)
219 221
(* compile-command: "make -C ../../.." *)

Also available in: Unified diff