Project

General

Profile

« Previous | Next » 

Revision b5b745fb

Added by Guillaume DAVY almost 3 years ago

Ada: First support for transition predicate generation.

View differences:

src/backends/Ada/ada_backend_adb.ml
26 26
module Main =
27 27
struct
28 28

  
29
  (** Printing function for basic assignement [var_name := value].
29
  (** Printing function for basic assignement [var := value].
30 30

  
31 31
      @param fmt the formater to print on
32 32
      @param var_name the name of the variable
33 33
      @param value the value to be assigned
34 34
   **)
35
  let pp_basic_assign m fmt var_name value =
35
  let pp_assign env fmt var value =
36 36
    fprintf fmt "%a := %a"
37
      (pp_access_var m) var_name
38
      (pp_value m) value
37
      (pp_var env) var
38
      (pp_value env) value
39 39

  
40 40
  (** Printing function for instruction. See
41 41
      {!type:Machine_code_types.instr_t} for more details on
......
46 46
      @param fmt the formater to print on
47 47
      @param instr the instruction to print
48 48
   **)
49
  let rec pp_machine_instr typed_submachines machine instr fmt =
50
    let pp_instr = pp_machine_instr typed_submachines machine in
49
  let rec pp_machine_instr typed_submachines env instr fmt =
50
    let pp_instr = pp_machine_instr typed_submachines env in
51 51
    (* Print args for a step call *)
52 52
    let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in
53 53
    (* Print a when branch of a case *)
......
57 57
    (* Print a case *)
58 58
    let pp_case fmt (g, hl) =
59 59
      fprintf fmt "case %a is@,%aend case"
60
        (pp_value machine) g
60
        (pp_value env) g
61 61
        pp_block (List.map pp_when hl)
62 62
    in
63 63
    (* Print a if *)
......
65 65
       first check that we don't have a negation and a else case, if so it
66 66
       inverses the two branch and remove the negation doing a recursive
67 67
       call. *)
68
    let rec pp_if neg fmt (g, instrs1, instrs2) =
69
      match neg, instrs2 with
70
        | true, Some x -> pp_if false fmt (g, x, Some instrs1)
71
        | _ ->
72
          let pp_cond =
73
            if neg then
74
              fun fmt x -> fprintf fmt "! (%a)" (pp_value machine) x
75
            else
76
              pp_value machine
77
          in
78
          let pp_else = match instrs2 with
79
            | None -> fun fmt -> fprintf fmt ""
80
            | Some i2 -> fun fmt ->
81
                fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
82
          in
83
          fprintf fmt "if %a then@,%a%tend if"
84
            pp_cond g
85
            pp_block (List.map pp_instr instrs1)
86
            pp_else
68
    let pp_if fmt (neg, g, instrs1, instrs2) =
69
      let pp_cond =
70
        if neg then
71
          fun fmt x -> fprintf fmt "! (%a)" (pp_value env) x
72
        else
73
          pp_value env
74
      in
75
      let pp_else = match instrs2 with
76
        | None -> fun fmt -> fprintf fmt ""
77
        | Some i2 -> fun fmt ->
78
            fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
79
      in
80
      fprintf fmt "if %a then@,%a%tend if"
81
        pp_cond g
82
        pp_block (List.map pp_instr instrs1)
83
        pp_else
87 84
    in
88 85
    match get_instr_desc instr with
89 86
      (* no reset *)
......
95 92
          let args = if is_machine_statefull submachine then [[pp_state i]] else [] in
96 93
          pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
97 94
      | MLocalAssign (ident, value) ->
98
          pp_basic_assign machine fmt ident value
95
          pp_assign env fmt ident value
99 96
      | MStateAssign (ident, value) ->
100
          pp_basic_assign machine fmt ident value
97
          pp_assign env fmt ident value
101 98
      | MStep ([i0], i, vl) when is_builtin_fun i ->
102 99
          let value = mk_val (Fun (i, vl)) i0.var_type in
103
          pp_basic_assign machine fmt i0 value
100
            pp_assign env fmt i0 value
104 101
      | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
105 102
          let (substitution, submachine) = get_instance i typed_submachines in
106 103
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
107
          let input = List.map (fun x fmt -> pp_value machine fmt x) vl in
108
          let output = List.map (fun x fmt -> pp_var_name fmt x) il in
104
          let input = List.map (fun x fmt -> pp_value env fmt x) vl in
105
          let output = List.map pp_var_name il in
109 106
          let args =
110 107
            (if is_machine_statefull submachine then [[pp_state i]] else [])
111 108
              @(if input!=[] then [input] else [])
......
114 111
          pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)
115 112
      | MBranch (_, []) -> assert false
116 113
      | MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
117
          let neg = c1=tag_false in
118
          let other = match tl with
119
            | []         -> None
120
            | [(c2, i2)] -> Some i2
121
            | _          -> assert false
122
          in
123
          pp_if neg fmt (g, i1, other)
114
          pp_if fmt (build_if g c1 i1 tl)
124 115
      | MBranch (g, hl) -> pp_case fmt (g, hl)
125 116
      | MComment s  ->
126 117
          let lines = String.split_on_char '\n' s in
......
133 124
     @param fmt the formater to print on
134 125
     @param machine the machine
135 126
  **)
136
  let pp_step_definition typed_submachines fmt (m, m_spec_opt) =
137
    let spec_instrs = match m_spec_opt with
138
      | None -> []
139
      | Some m -> m.mstep.step_instrs
127
  let pp_step_definition env typed_submachines fmt (m, m_spec_opt) =
128
    let transform_local_to_state_assign instr = match instr.instr_desc with
129
      | MLocalAssign (ident, value) -> 
130
          { instr_desc = MStateAssign (ident, value);
131
            lustre_eq= instr.lustre_eq }
132
      | x -> instr
140 133
    in
141
    let spec_locals = match m_spec_opt with
134
    let spec_instrs = match m_spec_opt with
142 135
      | None -> []
143
      | Some m -> m.mstep.step_locals
136
      | Some m_spec -> List.map transform_local_to_state_assign m_spec.mstep.step_instrs
144 137
    in
145
    let pp_local_list = List.map build_pp_var_decl_local (m.mstep.step_locals@spec_locals) in
146
    let pp_instr_list = List.map (pp_machine_instr typed_submachines m) (m.mstep.step_instrs@spec_instrs) in
138
    let pp_local_list = List.map (build_pp_var_decl_local None) (m.mstep.step_locals) in
139
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (m.mstep.step_instrs@spec_instrs) in
147 140
    let content = AdaProcedureContent ((if pp_local_list = [] then [] else [pp_local_list]), pp_instr_list) in
148 141
    pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
149 142

  
......
153 146
     @param fmt the formater to print on
154 147
     @param machine the machine
155 148
  **)
156
  let pp_reset_definition typed_submachines fmt m =
149
  let pp_reset_definition env typed_submachines fmt m =
157 150
    let build_assign = function var ->
158 151
      mkinstr (MStateAssign (var, mk_default_value var.var_type))
159 152
    in
160 153
    let assigns = List.map build_assign m.mmemory in
161
    let pp_instr_list = List.map (pp_machine_instr typed_submachines m) (assigns@m.minit) in
154
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (assigns@m.minit) in
162 155
    pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt (AdaProcedureContent ([], pp_instr_list))
163 156

  
164 157
  (** Print the package definition(ads) of a machine.
......
172 165
     @param m the machine
173 166
  **)
174 167
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine)) =
168
    let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
175 169
    let pp_reset fmt =
176 170
      if is_machine_statefull machine then
177
        fprintf fmt "%a;@,@," (pp_reset_definition typed_submachines) machine
171
        fprintf fmt "%a;@,@," (pp_reset_definition env typed_submachines) machine
178 172
      else
179 173
        fprintf fmt ""
180 174
    in
......
194 188
        pp_reset
195 189
        
196 190
        (*Define the step procedure*)
197
        (pp_step_definition typed_submachines) (machine, opt_spec_machine)
191
        (pp_step_definition env typed_submachines) (machine, opt_spec_machine)
198 192
    in
199 193
    fprintf fmt "%a%t%a;@."
200 194
      
src/backends/Ada/ada_backend_ads.ml
25 25
module Main =
26 26
struct
27 27

  
28
  (** Print a new statement instantiating a generic package.
29
     @param fmt the formater to print on
30
     @param substitutions the instanciation substitution
31
     @param machine the machine to instanciate
32
  **)
33
  let pp_new_package fmt (substitutions, machine) =
34
    let pp_name = pp_package_name machine in
35
    let pp_new_name = pp_package_name_with_polymorphic substitutions machine in
36
    let instanciations = List.map (fun (id, typ) -> (pp_polymorphic_type id, fun fmt -> pp_type fmt typ)) substitutions in
37
    pp_package_instanciation pp_new_name pp_name fmt instanciations
38 28

  
39
  (** Print a precondition in aspect
40
     @param fmt the formater to print on
41
     @param expr the expession to print as pre
42
  **)
43
  let pp_pre fmt expr =
44
    fprintf fmt "Pre => %a"
45
      pp_clean_ada_identifier expr
29
  let suffixOld = "_old"
30
  let suffixNew = "_new"
31
  let pp_transition_name fmt = fprintf fmt "transition"
32
  let pp_state_name_transition suffix fmt = fprintf fmt "%t%s" pp_state_name suffix
46 33

  
47
  (** Print a postcondition in aspect
48
     @param fmt the formater to print on
49
     @param expr the expession to print as pre
50
  **)
51
  let pp_post fmt ident =
52
    fprintf fmt "Post => %a"
53
      pp_clean_ada_identifier ident
54 34

  
55
  (** Print the declaration of a procedure with a contract
56
     @param pp_prototype the prototype printer
57
     @param fmt the formater to print on
58
     @param contract the contract for the function to declare
59
  **)
60
  let pp_contract guarantees fmt =
61
    fprintf fmt "@,  @[<v>Global => null%t%a@]"
62
      (Utils.pp_final_char_if_non_empty ",@," guarantees)
63
      (Utils.fprintf_list ~sep:",@," pp_post) guarantees
64 35

  
65
(*
66
  let pp_transition_name fmt = fprintf fmt "transition"
67
  let pp_state_name_transition suffix fmt = fprintf fmt "%t_%s" pp_state_name suffix
68 36

  
69
  (** Printing function for basic assignement [var_name := value].
37
  (** Printing function for basic assignement [var := value].
70 38

  
71 39
      @param fmt the formater to print on
72 40
      @param var_name the name of the variable
73 41
      @param value the value to be assigned
74 42
   **)
75
  let pp_basic_assign m fmt var_name value =
76
    fprintf fmt "%a = %a"
77
      (pp_access_var m) var_name
78
      (pp_value m) value
43
  let pp_local_eq env fmt var value =
44
    fprintf fmt "%t = %a"
45
      (pp_var_name var)
46
      (pp_value env) value
79 47

  
48
  (** Printing function for basic assignement [var := value].
49

  
50
      @param fmt the formater to print on
51
      @param var_name the name of the variable
52
      @param value the value to be assigned
53
   **)
54
  let pp_state_eq env fmt var value =
55
    fprintf fmt "%t = %a"
56
      (pp_access (pp_state_name_transition suffixNew) (pp_var_name var))
57
      (pp_value env) value
80 58

  
81 59
  (** Printing function for instruction. See
82 60
      {!type:Machine_code_types.instr_t} for more details on
......
87 65
      @param fmt the formater to print on
88 66
      @param instr the instruction to print
89 67
   **)
90
  let rec pp_machine_instr typed_submachines machine instr fmt =
91
    let pp_instr = pp_machine_instr typed_submachines machine in
92
    (* Print args for a step call *)
93
    let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in
94
    let pp_args vl il fmt =
95
      fprintf fmt "@[%a@]%t@[%a@]"
96
        (Utils.fprintf_list ~sep:",@ " (pp_value machine)) vl
97
        (Utils.pp_final_char_if_non_empty ",@," il)
98
        (Utils.fprintf_list ~sep:",@ " pp_var_name) il
99
    in
100
    (* Print a when branch of a case *)
101
    let pp_when (cond, instrs) fmt =
102
      fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs)
103
    in
104
    (* Print a case *)
105
    let pp_case fmt (g, hl) =
106
      fprintf fmt "case %a is@,%aend case"
107
        (pp_value machine) g
108
        pp_block (List.map pp_when hl)
109
    in
110
    (* Print a if *)
111
    (* If neg is true the we must test for the negation of the condition. It
112
       first check that we don't have a negation and a else case, if so it
113
       inverses the two branch and remove the negation doing a recursive
114
       call. *)
115
    let rec pp_if neg fmt (g, instrs1, instrs2) =
116
      match neg, instrs2 with
117
        | true, Some x -> pp_if false fmt (g, x, Some instrs1)
118
        | _ ->
119
          let pp_cond =
120
            if neg then
121
              fun fmt x -> fprintf fmt "! (%a)" (pp_value machine) x
122
            else
123
              pp_value machine
124
          in
125
          let pp_else = match instrs2 with
126
            | None -> fun fmt -> fprintf fmt ""
127
            | Some i2 -> fun fmt ->
128
                fprintf fmt "else@,%a" pp_block (List.map pp_instr i2)
129
          in
130
          fprintf fmt "if %a then@,%a%tend if"
131
            pp_cond g
132
            pp_block (List.map pp_instr instrs1)
133
            pp_else
134
    in
68
  let rec pp_machine_instr typed_submachines env instr fmt =
69
    let pp_instr = pp_machine_instr typed_submachines env in
70
    let pp_state suffix i fmt = fprintf fmt "%t.%s" (pp_state_name_transition suffix) i in
135 71
    match get_instr_desc instr with
136 72
      (* no reset *)
137 73
      | MNoReset _ -> ()
......
139 75
      | MReset i when List.mem_assoc i typed_submachines ->
140 76
          let (substitution, submachine) = get_instance i typed_submachines in
141 77
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
142
          pp_call fmt (pp_package_access (pp_package, pp_name), [pp_state i])
78
          let args = if is_machine_statefull submachine then [[pp_state suffixOld i;pp_state suffixNew i]] else [] in
79
          pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
143 80
      | MLocalAssign (ident, value) ->
144
          pp_basic_assign machine fmt ident value
81
          pp_local_eq env fmt ident value
145 82
      | MStateAssign (ident, value) ->
146
          pp_basic_assign machine fmt ident value
83
          pp_state_eq env fmt ident value
147 84
      | MStep ([i0], i, vl) when is_builtin_fun i ->
148 85
          let value = mk_val (Fun (i, vl)) i0.var_type in
149
          pp_basic_assign machine fmt i0 value
86
          if List.mem_assoc i0.var_id env then
87
            pp_state_eq env fmt i0 value
88
          else
89
            pp_local_eq env fmt i0 value
90
          
150 91
      | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
151 92
          let (substitution, submachine) = get_instance i typed_submachines in
152
          pp_package_call
153
            pp_step_procedure_name
154
            fmt
155
            (substitution, submachine, pp_state i, Some (pp_args vl il))
156
      | MBranch (_, []) -> assert false
157
      | MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
158
          let neg = c1=tag_false in
159
          let other = match tl with
160
            | []         -> None
161
            | [(c2, i2)] -> Some i2
162
            | _          -> assert false
93
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
94
          let input = List.map (fun x fmt -> pp_value env fmt x) vl in
95
          let output = List.map pp_var_name il in
96
          let args =
97
            (if is_machine_statefull submachine then [[pp_state suffixOld i;pp_state suffixNew i]] else [])
98
              @(if input!=[] then [input] else [])
99
              @(if output!=[] then [output] else [])
163 100
          in
164
          pp_if neg fmt (g, i1, other)
165
      | MBranch (g, hl) -> pp_case fmt (g, hl)
166
      | MComment s  ->
167
          let lines = String.split_on_char '\n' s in
168
          fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines
101
          fprintf fmt "(%a)" pp_call (pp_package_access (pp_package, pp_transition_name), args)
102
      | MComment s -> ()
169 103
      | _ -> assert false
170 104

  
105

  
106

  
107

  
108

  
109

  
110

  
111

  
112

  
113

  
114

  
115

  
116

  
117

  
118

  
119

  
120

  
121

  
171 122
  (** Print the expression function representing the transition predicate.
172 123
     @param fmt the formater to print on
173 124
     @param machine the machine
174 125
  **)
175
  let pp_transition_predicate typed_submachines fmt (opt_spec_machine, m) =
176
    let spec_instrs = match opt_spec_machine with
177
      | None -> []
178
      | Some m -> m.mstep.step_instrs
179
    in
180
    fprintf fmt "function %t (%a; %a) return Boolean is (@,  @[<v>%a@,@]) with Ghost"
181
      pp_transition_name
182
      pp_var_decl_mode (In, pp_state_name_transition "old", pp_state_type)
183
      pp_var_decl_mode (In, pp_state_name_transition "new", pp_state_type)
184
      (Utils.fprintf_list ~sep:" and@," (pp_machine_instr typed_submachines m)) (m.mstep.step_instrs@spec_instrs)*)
126
  let pp_transition_predicate prototype typed_submachines fmt (opt_spec_machine, m) =
127
    let old_state = (AdaIn, pp_state_name_transition suffixOld, pp_state_type, None) in
128
    let new_state = (AdaIn, pp_state_name_transition suffixNew, pp_state_type, None) in
129
    let env = List.map (fun x -> x.var_id, pp_state_name_transition suffixOld) m.mmemory in
130
    let inputs = build_pp_var_decl_step_input AdaIn None m in
131
    let outputs = build_pp_var_decl_step_output AdaIn None m in
132
    let instrs = push_if_in_expr m.mstep.step_instrs in
133
    let content = List.map (pp_machine_instr typed_submachines env) instrs in
134
    let locals = List.map (fun x-> (pp_var_name x, fun fmt -> pp_var_type fmt x)) m.mstep.step_locals in
135
    pp_predicate pp_transition_name ([[old_state; new_state]]@inputs@outputs) fmt (if prototype then None else Some (locals, content))
185 136
    
137

  
138

  
139

  
140

  
141

  
142

  
143

  
144

  
145

  
146

  
147

  
148

  
149
  (** Print a new statement instantiating a generic package.
150
     @param fmt the formater to print on
151
     @param substitutions the instanciation substitution
152
     @param machine the machine to instanciate
153
  **)
154
  let pp_new_package fmt (substitutions, machine) =
155
    let pp_name = pp_package_name machine in
156
    let pp_new_name = pp_package_name_with_polymorphic substitutions machine in
157
    let instanciations = List.map (fun (id, typ) -> (pp_polymorphic_type id, fun fmt -> pp_type fmt typ)) substitutions in
158
    pp_package_instanciation pp_new_name pp_name fmt instanciations
159

  
186 160
  (** Remove duplicates from a list according to a given predicate.
187 161
     @param eq the predicate defining equality
188 162
     @param l the list to parse
......
210 184
     @param typed_submachines list of all typed submachines of this machine
211 185
     @param m the machine
212 186
  **)
213
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), m)) =
187
  let pp_file fmt (typed_submachines, ((m_spec_opt, guarantees), m)) =
214 188
    let typed_machines = snd (List.split typed_submachines) in
215 189
    let typed_machines_set = remove_duplicates eq_typed_machine typed_machines in
216 190
    
......
225 199

  
226 200
    let pp_state_decl_and_reset fmt = fprintf fmt "%t;@,@,%a;@,@,"
227 201
      (*Declare the state type*)
228
      (pp_type_decl pp_state_type AdaLimitedPrivate)
202
      (pp_type_decl pp_state_type AdaPrivate)
229 203
      (*Declare the reset procedure*)
230 204
      (pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None) AdaNoContent
231 205
    in
232

  
233
    let vars = List.map (build_pp_var_decl AdaNoMode) m.mmemory in
234
    let states = List.map build_pp_state_decl_from_subinstance typed_instances in
235
    let var_lists = (if vars = [] then [] else [vars])@(if states = [] then [] else [states]) in
236

  
237
    let pp_private_section fmt = fprintf fmt "@,private@,@,%a%t%a"
238
      (*Instantiate the polymorphic type that need to be instantiated*)
239
      (Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
240
      (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
241
      (*Define the state type*)
242
      (pp_record pp_state_type) var_lists
206
    
207
    let vars_spec = match m_spec_opt with
208
      | None -> []
209
      | Some m_spec -> List.map (build_pp_var_decl AdaNoMode None) m_spec.mstep.step_locals
243 210
    in
211
    let vars = List.map (build_pp_var_decl AdaNoMode None) m.mmemory in
212
    let states = List.map (build_pp_state_decl_from_subinstance AdaNoMode None) typed_instances in
213
    let var_lists =
214
      (if states = [] then [] else [states]) @
215
      (if vars = [] then [] else [vars])@
216
      (if vars_spec = [] then [] else [vars_spec]) in
244 217
    
245 218
    let pp_ifstatefull fmt pp =
246 219
      if is_machine_statefull m then
......
249 222
        fprintf fmt ""
250 223
    in
251 224

  
225
    let pp_private_section fmt = fprintf fmt "@,private@,@,%a%t%a;@,@,%a"
226
      (*Instantiate the polymorphic type that need to be instantiated*)
227
      (Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
228
      (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
229
      (*Define the state type*)
230
      pp_ifstatefull (fun fmt-> pp_record pp_state_type fmt var_lists)
231
        
232
      (*Declare the transition predicate*)
233
      (pp_transition_predicate false typed_submachines) (m_spec_opt, m)
234
    in
235

  
252 236
    let pp_content fmt =
253
      let pp_contract_opt = match guarantees with
254
                              | [] -> None
255
                              | _ ->  Some (pp_contract guarantees) in
256
      fprintf fmt "%a%a%a%a" (* %a;@, *)
237
      let pp_contract_opt =
238
        let ghost_memory = match m_spec_opt with
239
          | None -> []
240
          | Some m_spec -> m_spec.mstep.step_locals
241
        in
242
        let pp_var x fmt =
243
          if List.exists (fun var -> var.var_id == x) ghost_memory then
244
            pp_access pp_state_name (fun fmt -> pp_clean_ada_identifier fmt x) fmt
245
          else
246
            pp_clean_ada_identifier fmt x
247
        in
248
        let input = List.map pp_var_name m.mstep.step_inputs in
249
        let output = List.map pp_var_name m.mstep.step_outputs in
250
        let args =
251
          (if is_machine_statefull m then [[pp_old pp_state_name;pp_state_name]] else [])
252
            @(if input!=[] then [input] else [])
253
            @(if output!=[] then [output] else [])
254
        in
255
        let transition fmt = pp_call fmt (pp_transition_name, args) in
256
        match guarantees with
257
          | [] -> Some (false, [], [transition])
258
          | _ ->  Some (false, [], transition::(List.map pp_var guarantees))
259
      in
260
      fprintf fmt "%a%a%a@,@,%a;%t" (* %a;@, *)
257 261
        pp_ifstatefull pp_state_decl_and_reset
258 262
        
259
        (*Declare the transition predicate*)
260
        (* pp_transition_predicate typed_submachines) (opt_spec_machine, m) *)
261
        
262 263
        (*Declare the step procedure*)
263 264
        (pp_procedure pp_step_procedure_name (build_pp_arg_step m) pp_contract_opt) AdaNoContent
264 265
        
265 266
        pp_ifstatefull (fun fmt -> fprintf fmt ";@,")
266 267
        
268
        (*Declare the transition predicate*)
269
        (pp_transition_predicate true typed_submachines) (m_spec_opt, m)
270
        
267 271
        (*Print the private section*)
268
        pp_ifstatefull pp_private_section
272
        pp_private_section
269 273
    in
270 274
    
271 275
    let pp_poly_types id = pp_type_decl (pp_polymorphic_type id) AdaPrivate in
src/backends/Ada/ada_backend_common.ml
93 93
  else
94 94
      fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id
95 95

  
96

  
97
(** Print the integer type name.
98
   @param fmt the formater to print on
99
**)
100
let pp_integer_type fmt = fprintf fmt "Integer"
101

  
102
(** Print the float type name.
103
   @param fmt the formater to print on
104
**)
105
let pp_float_type fmt = fprintf fmt "Float"
106

  
107
(** Print the boolean type name.
108
   @param fmt the formater to print on
109
**)
110
let pp_boolean_type fmt = fprintf fmt "Boolean"
111

  
112

  
113 96
(** Print a type.
114 97
   @param fmt the formater to print on
115 98
   @param type the type
......
179 162
   @param fmt the formater to print on
180 163
   @param id the variable
181 164
**)
182
let pp_var_name fmt id =
165
let pp_var_name id fmt =
183 166
  fprintf fmt "%a" pp_clean_ada_identifier id.var_id
184 167

  
185 168
(** Print the complete name of variable.
......
187 170
   @param fmt the formater to print on
188 171
   @param var the variable
189 172
**)
190
let pp_access_var m fmt var =
191
  if is_memory m var then
192
    fprintf fmt "%t.%a" pp_state_name pp_var_name var
193
  else
194
    pp_var_name fmt var
195

  
173
let pp_var env fmt var =
174
  match List.assoc_opt var.var_id env with
175
    | None -> pp_var_name var fmt
176
    | Some pp_state -> pp_access pp_state (pp_var_name var) fmt
196 177

  
197 178
(* Expression print functions *)
198 179

  
......
296 277
    Format.fprintf fmt "(%a %s %a)" pp_value v1 "or else" pp_value v2
297 278
  | "!=", [v1; v2]    ->
298 279
    Format.fprintf fmt "(%a %s %a)" pp_value v1 "/=" pp_value v2
280
  | "ite", [v1; v2; v3]    ->
281
    Format.fprintf fmt "(if %a then %a else %a)" pp_value v1 pp_value v2 pp_value v3
299 282
  | op, [v1; v2]     ->
300 283
    Format.fprintf fmt "(%a %s %a)" pp_value v1 op pp_value v2
301 284
  | op, [v1] when  List.mem_assoc ident ada_supported_funs ->
......
313 296
    @param value the value to print. Should be a
314 297
           {!type:Machine_code_types.value_t} value
315 298
 **)
316
let rec pp_value m fmt value =
299
let rec pp_value env fmt value =
317 300
  match value.value_desc with
318 301
  | Cst c             -> pp_ada_const fmt c
319
  | Var var      -> pp_access_var m fmt var
320
  | Fun (f_ident, vl) -> pp_basic_lib_fun (pp_value m) f_ident fmt vl
302
  | Var var      -> pp_var env fmt var (* Find better to test if it is memory or not *)
303
  | Fun (f_ident, vl) -> pp_basic_lib_fun (pp_value env) f_ident fmt vl
321 304
  | _                 ->
322 305
    raise (Ada_not_supported
323 306
             "unsupported: Ada_backend.adb.pp_value does not support this value type")
......
341 324
   @param ident the identifier of the subinstance
342 325
   @param submachine the submachine of the subinstance
343 326
**)
344
let build_pp_state_decl_from_subinstance (name, (substitution, machine)) =
327
let build_pp_state_decl_from_subinstance mode with_statement (name, (substitution, machine)) =
345 328
  let pp_package = pp_package_name_with_polymorphic substitution machine in
346 329
  let pp_type = pp_package_access (pp_package, pp_state_type) in
347 330
  let pp_name fmt = pp_clean_ada_identifier fmt name in
348
  (AdaNoMode, pp_name, pp_type)
331
  (mode, pp_name, pp_type, with_statement)
349 332

  
350 333
(** Print variable declaration for a local state variable
351 334
   @param fmt the formater to print on
352 335
   @param mode input/output mode of the parameter
353 336
**)
354
let build_pp_state_decl mode =
355
  (mode, pp_state_name, pp_state_type)
337
let build_pp_state_decl mode with_statement =
338
  (mode, pp_state_name, pp_state_type, with_statement)
356 339

  
357
let build_pp_var_decl mode var =
358
  let pp_name = function fmt -> pp_var_name fmt var in
340
let build_pp_var_decl mode with_statement var =
341
  let pp_name = function fmt -> pp_var_name var fmt in
359 342
  let pp_type = function fmt -> pp_var_type fmt var in
360
  (mode, pp_name, pp_type)
343
  (mode, pp_name, pp_type, with_statement)
361 344

  
362
let build_pp_var_decl_local var =
363
  AdaLocalVar (build_pp_var_decl AdaNoMode var)
345
let build_pp_var_decl_local with_statement var =
346
  AdaLocalVar (build_pp_var_decl AdaNoMode with_statement var)
364 347

  
365
let build_pp_var_decl_step_input mode m =
348
let build_pp_var_decl_step_input mode with_statement m =
366 349
  if m.mstep.step_inputs=[] then [] else
367
    [List.map (build_pp_var_decl mode) m.mstep.step_inputs]
350
    [List.map (build_pp_var_decl mode with_statement) m.mstep.step_inputs]
368 351

  
369
let build_pp_var_decl_step_output mode m =
352
let build_pp_var_decl_step_output mode with_statement m =
370 353
  if m.mstep.step_outputs=[] then [] else
371
    [List.map (build_pp_var_decl mode) m.mstep.step_outputs]
354
    [List.map (build_pp_var_decl mode with_statement) m.mstep.step_outputs]
372 355

  
373
let build_pp_var_decl_static mode m =
356
let build_pp_var_decl_static mode with_statement m =
374 357
  if m.mstatic=[] then [] else
375
    [List.map (build_pp_var_decl mode) m.mstatic]
358
    [List.map (build_pp_var_decl mode with_statement) m.mstatic]
376 359

  
377 360
let build_pp_arg_step m =
378
  (if is_machine_statefull m then [[build_pp_state_decl AdaInOut]] else [])
379
    @ (build_pp_var_decl_step_input AdaIn m)
380
    @ (build_pp_var_decl_step_output AdaOut m)
361
  (if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])
362
    @ (build_pp_var_decl_step_input AdaIn None m)
363
    @ (build_pp_var_decl_step_output AdaOut None m)
381 364

  
382 365
let build_pp_arg_reset m =
383
  (if is_machine_statefull m then [[build_pp_state_decl AdaOut]] else [])
384
    @ (build_pp_var_decl_static AdaIn m)
366
  (if is_machine_statefull m then [[build_pp_state_decl AdaOut None]] else [])
367
    @ (build_pp_var_decl_static AdaIn None m)
368

  
369

  
370
let build_pp_arg_transition m =
371
  (if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])
372
    @ (build_pp_var_decl_step_input AdaIn None m)
373
    @ (build_pp_var_decl_step_output AdaOut None m)
374

  
src/backends/Ada/ada_backend_common.mli
17 17
val is_builtin_fun : string -> bool
18 18
val ada_supported_funs : (string*(string*string)) list
19 19

  
20
val pp_access_var : machine_t -> formatter -> var_decl -> unit
21
val pp_value : machine_t -> formatter -> value_t -> unit
22
val pp_var_name : formatter -> var_decl -> unit
20
val pp_var_name : var_decl -> formatter -> unit
21
val pp_var : ((string*printer) list) -> formatter -> var_decl -> unit
22
val pp_value : ((string*printer) list) -> formatter -> value_t -> unit
23 23
val pp_type : formatter -> type_expr -> unit
24 24
val pp_var_type : formatter -> var_decl -> unit
25 25

  
......
28 28

  
29 29
val mk_default_value : type_expr -> value_t
30 30

  
31
val build_pp_var_decl : parameter_mode -> var_decl -> ada_var_decl
32
val build_pp_var_decl_local : var_decl -> ada_local_decl
31
val build_pp_var_decl : parameter_mode -> ada_with -> var_decl -> ada_var_decl
32
val build_pp_var_decl_local : ada_with -> var_decl -> ada_local_decl
33
val build_pp_var_decl_step_input : parameter_mode -> ada_with -> machine_t -> (ada_var_decl list list)
34
val build_pp_var_decl_step_output : parameter_mode -> ada_with -> machine_t -> (ada_var_decl list list)
33 35
val build_pp_arg_step : machine_t -> (ada_var_decl list list)
34 36
val build_pp_arg_reset : machine_t -> (ada_var_decl list list)
35
val build_pp_state_decl_from_subinstance : (string * ((int * Types.type_expr) list * Machine_code_types.machine_t)) -> ada_var_decl
37
val build_pp_state_decl_from_subinstance : parameter_mode -> ada_with -> (string * ((int * Types.type_expr) list * Machine_code_types.machine_t)) -> ada_var_decl
36 38

  
37 39
val pp_machine_filename : string -> formatter -> machine_t -> unit
38 40
val pp_main_filename : formatter -> machine_t -> unit
src/backends/Ada/ada_backend_wrapper.ml
43 43
    (* Locals *)
44 44
    let locals =
45 45
      [[build_text_io_package_local "Integer";build_text_io_package_local "Float"]]
46
      @(if statefull then [[AdaLocalVar (build_pp_state_decl_from_subinstance (asprintf "%t" pp_state_name, ([], machine)))]] else [])
47
      @(if machine.mstep.step_inputs != [] then [List.map build_pp_var_decl_local machine.mstep.step_inputs] else [])
48
      @(if machine.mstep.step_outputs != [] then [List.map build_pp_var_decl_local machine.mstep.step_outputs] else [])
46
      @(if statefull then [[AdaLocalVar (build_pp_state_decl_from_subinstance AdaNoMode None (asprintf "%t" pp_state_name, ([], machine)))]] else [])
47
      @(if machine.mstep.step_inputs != [] then [List.map (build_pp_var_decl_local None) machine.mstep.step_inputs] else [])
48
      @(if machine.mstep.step_outputs != [] then [List.map (build_pp_var_decl_local None) machine.mstep.step_outputs] else [])
49 49
    in
50 50

  
51 51
    (* Stream instructions *)
......
54 54
    let pp_read fmt var =
55 55
      match get_basic var with
56 56
        | Types.Basic.Tbool ->
57
            fprintf fmt "%a := Integer'Value(Ada.Text_IO.Get_Line) /= 0"
58
              pp_var_name var
57
            fprintf fmt "%t := Integer'Value(Ada.Text_IO.Get_Line) /= 0"
58
              (pp_var_name var)
59 59
        | _ ->
60
            fprintf fmt "%a := %a'Value(Ada.Text_IO.Get_Line)"
61
              pp_var_name var
60
            fprintf fmt "%t := %a'Value(Ada.Text_IO.Get_Line)"
61
              (pp_var_name var)
62 62
              pp_var_type var
63 63
    in
64 64
    let pp_write fmt var =
65 65
      match get_basic var with
66 66
        | Types.Basic.Tbool ->
67
            fprintf fmt "Ada.Text_IO.Put_Line(\"'%a': '\" & (if %a then \"1\" else \"0\") & \"' \")"
68
              pp_var_name var
69
              pp_var_name var
67
            fprintf fmt "Ada.Text_IO.Put_Line(\"'%t': '\" & (if %t then \"1\" else \"0\") & \"' \")"
68
              (pp_var_name var)
69
              (pp_var_name var)
70 70
        | Types.Basic.Tint ->
71
            fprintf fmt "Ada.Text_IO.Put(\"'%a': '\");@,Integer_IO.Put(%a);@,Ada.Text_IO.Put_Line(\"' \")"
72
              pp_var_name var
73
              pp_var_name var
71
            fprintf fmt "Ada.Text_IO.Put(\"'%t': '\");@,Integer_IO.Put(%t);@,Ada.Text_IO.Put_Line(\"' \")"
72
              (pp_var_name var)
73
              (pp_var_name var)
74 74
        | Types.Basic.Treal ->
75
            fprintf fmt "Ada.Text_IO.Put(\"'%a': '\");@,Float_IO.Put(%a, Fore=>0, Aft=> 15, Exp => 0);@,Ada.Text_IO.Put_Line(\"' \")"
76
              pp_var_name var
77
              pp_var_name var
75
            fprintf fmt "Ada.Text_IO.Put(\"'%t': '\");@,Float_IO.Put(%t, Fore=>0, Aft=> 15, Exp => 0);@,Ada.Text_IO.Put_Line(\"' \")"
76
              (pp_var_name var)
77
              (pp_var_name var)
78 78
        | Types.Basic.Tstring | Types.Basic.Trat -> assert false (* Could not be the top level inputs *)
79 79
    in
80 80

  
81 81
    (* Loop instructions *)
82 82
    let pp_loop fmt =
83
      let args = pp_state_name::(List.map (fun x fmt -> pp_var_name fmt x) (machine.mstep.step_inputs@machine.mstep.step_outputs)) in
83
      let args = pp_state_name::(List.map pp_var_name (machine.mstep.step_inputs@machine.mstep.step_outputs)) in
84 84
      fprintf fmt "while not Ada.Text_IO.End_Of_File loop@,  @[<v>%a;@,%a;@,%a;@]@,end loop"
85 85
        (Utils.fprintf_list ~sep:";@," pp_read) machine.mstep.step_inputs
86 86
        pp_call (pp_package_access (pp_package, pp_step_procedure_name), [args])
src/backends/Ada/ada_printer.ml
9 9

  
10 10
type printer = Format.formatter -> unit
11 11

  
12
type ada_var_decl = parameter_mode * printer * printer
12
type ada_with = (bool * (printer list) * (printer list)) option
13

  
14
type ada_var_decl = parameter_mode * printer * printer * ada_with
13 15

  
14 16
type ada_local_decl =
15 17
  | AdaLocalVar of ada_var_decl
......
17 19

  
18 20
type def_content =
19 21
  | AdaNoContent
20
  | AdaPackageContent of (Format.formatter -> unit)
22
  | AdaPackageContent of printer
23
  | AdaSimpleContent of printer
21 24
  | AdaVisibilityDefinition of visibility
22 25
  | AdaProcedureContent of ((ada_local_decl list list) * (printer list))
23 26
  | AdaRecord of ((ada_var_decl list) list)
......
48 51
                     | AdaPrivate          -> "private"
49 52
                     | AdaLimitedPrivate   -> "limited private")
50 53

  
54
(** Print the integer type name.
55
   @param fmt the formater to print on
56
**)
57
let pp_integer_type fmt = fprintf fmt "Integer"
58

  
59
(** Print the float type name.
60
   @param fmt the formater to print on
61
**)
62
let pp_float_type fmt = fprintf fmt "Float"
63

  
64
(** Print the boolean type name.
65
   @param fmt the formater to print on
66
**)
67
let pp_boolean_type fmt = fprintf fmt "Boolean"
68

  
51 69
let pp_group ~sep:sep pp_list fmt =
52 70
  assert(pp_list != []);
53 71
  fprintf fmt "@[%a@]"
......
63 81
    (Utils.fprintf_list ~sep:";@," (fun fmt pp -> pp fmt)) pp_item_list
64 82
    (Utils.pp_final_char_if_non_empty ";@," pp_item_list)
65 83

  
84

  
85
let pp_ada_with fmt = function
86
  | None -> fprintf fmt ""
87
  | Some (ghost, pres, posts) ->
88
      assert(ghost || (pres != []) || (posts != []));
89
      let contract = pres@posts in
90
      let pp_ghost fmt = if not ghost then fprintf fmt "" else
91
        fprintf fmt " Ghost%t" (Utils.pp_final_char_if_non_empty ",@," contract)
92
      in
93
      let pp_aspect aspect fmt pps = if pps = [] then fprintf fmt "" else
94
        fprintf fmt "%s => %t" aspect (pp_group ~sep:"@,and " pps)
95
      in
96
      let pp_contract fmt = if contract = [] then fprintf fmt "" else
97
        let sep = if pres != [] && posts != [] then ",@," else "" in
98
        fprintf fmt "@,  @[<v>%a%s%a@]"
99
          (pp_aspect "Pre") pres
100
          sep
101
          (pp_aspect "Post") posts
102
      in
103
      fprintf fmt " with%t%t"
104
        pp_ghost
105
        pp_contract
106

  
66 107
(** Print instanciation of a generic type in a new statement.
67 108
   @param fmt the formater to print on
68 109
   @param id id of the polymorphic type
......
78 119
   @param fmt the formater to print on
79 120
   @param id the variable
80 121
**)
81
let pp_var_decl (mode, pp_name, pp_type) fmt =
82
  fprintf fmt "%t: %a%s%t"
122
let pp_var_decl (mode, pp_name, pp_type, with_statement) fmt =
123
  fprintf fmt "%t: %a%s%t%a"
83 124
    pp_name
84 125
    pp_parameter_mode mode
85 126
    (if mode = AdaNoMode then "" else " ")
86 127
    pp_type
128
    pp_ada_with with_statement
87 129

  
88 130
let apply_var_decl_lists var_list =
89 131
  List.map (fun l-> List.map pp_var_decl l) var_list
......
108 150
      fprintf fmt " is %a" pp_visibility visbility
109 151
  | AdaPackageContent pp_package ->
110 152
      fprintf fmt " is@,  @[<v>%t;@]@,end %t" pp_package pp_name
153
  | AdaSimpleContent pp_content ->
154
      fprintf fmt " is@,  @[<v 2>(%t)@]" pp_content
111 155
  | AdaProcedureContent (local_list, pp_instr_list) ->
112 156
      fprintf fmt " is@,%abegin@,%aend %t"
113
        pp_block (List.map (fun l -> pp_group ~sep:";@," (List.map pp_local l)) local_list)
157
        pp_block (List.map (fun l -> pp_group ~sep:";@;" (List.map pp_local l)) local_list)
114 158
        pp_block pp_instr_list
115 159
        pp_name
116 160
  | AdaRecord var_list ->
117 161
      assert(var_list != []);
118 162
      let pp_lists = apply_var_decl_lists var_list in
119 163
      fprintf fmt " is@,  @[<v>record@,  @[<v>%a@]@,end record@]"
120
        pp_block (List.map (pp_group ~sep:";@,") pp_lists)
164
        pp_block (List.map (pp_group ~sep:";@;") pp_lists)
121 165
  | AdaPackageInstanciation (pp_name, instanciations) ->
122 166
      fprintf fmt " is new %t%a"
123 167
        pp_name
124 168
        (pp_args ~sep:",@,") (List.map pp_generic_instanciation instanciations)
125
and pp_def fmt (pp_generics, kind_def, pp_name, args, pp_type_opt, content, pp_spec_opt) =
169
and pp_def fmt (pp_generics, kind_def, pp_name, args, pp_type_opt, content, pp_with_opt) =
126 170
  let pp_arg_lists = apply_var_decl_lists args in
127 171
  fprintf fmt "%a%a %t%a%a%a%a"
128 172
    pp_generic pp_generics
......
131 175
    (pp_args ~sep:";@,") (List.map (pp_group ~sep:";@,") pp_arg_lists)
132 176
    (pp_opt "return") pp_type_opt
133 177
    (pp_content pp_name) content
134
    (pp_opt   "with") pp_spec_opt
178
    pp_ada_with pp_with_opt
135 179
and pp_package_instanciation pp_name pp_base_name fmt instanciations =
136 180
  pp_def fmt ([], AdaPackageDecl, pp_name, [], None, (AdaPackageInstanciation (pp_base_name, instanciations)), None)
137 181

  
......
165 209
let pp_procedure pp_name args pp_with_opt fmt content =
166 210
  pp_def fmt ([], AdaProcedure, pp_name, args, None, content, pp_with_opt)
167 211

  
212
let pp_predicate pp_name args fmt content_opt =
213
  let rec quantify pp_content = function
214
    | [] -> pp_content
215
    | (pp_var, pp_type)::q -> fun fmt ->
216
      fprintf fmt "for some %t in %t => (@,  @[<v>%t@])" pp_var pp_type (quantify pp_content q)
217
  in
218
  let content, with_st = match content_opt with
219
    | Some (locals, booleans) -> AdaSimpleContent (quantify (fun fmt -> Utils.fprintf_list ~sep:"@;and " (fun fmt pp->pp fmt) fmt booleans) locals), None
220
    | None -> AdaNoContent, Some (true, [], [])
221
  in
222
  pp_def fmt ([], AdaFunction, pp_name, args, Some pp_boolean_type, content, with_st)
223

  
168 224

  
169 225

  
170 226

  
......
228 284
let pp_call fmt (pp_name, args) =
229 285
  fprintf fmt "%t%a"
230 286
    pp_name
231
    (pp_args ~sep:",@ ") (List.map (pp_group ~sep:",@ ") args)
287
    (pp_args ~sep:",@ ") (List.map (pp_group ~sep:",@,") args)
232 288

  
233 289

  
234
(*
235

  
236
(** Print a precondition in aspect
290
(** Print the complete name of variable.
291
   @param m the machine to check if it is memory
237 292
   @param fmt the formater to print on
238
   @param expr the expession to print as pre
293
   @param var the variable
239 294
**)
240
let pp_pre fmt expr =
241
  fprintf fmt "Pre => %a"
242
    pp_clean_ada_identifier expr
243

  
244
(** Print a postcondition in aspect
245
   @param fmt the formater to print on
246
   @param expr the expession to print as pre
247
**)
248
let pp_post fmt ident =
249
  fprintf fmt "Post => %a"
250
    pp_clean_ada_identifier ident
251

  
252
(** Print the declaration of a procedure with a contract
253
   @param pp_prototype the prototype printer
254
   @param fmt the formater to print on
255
   @param contract the contract for the function to declare
256
**)
257
let pp_contract guarantees fmt =
258
  fprintf fmt "@,  @[<v>Global => null%t%a@]"
259
    (Utils.pp_final_char_if_non_empty ",@," guarantees)
260
    (Utils.fprintf_list ~sep:",@," pp_post) guarantees
261

  
262
*)
263

  
264

  
265

  
295
let pp_access pp_state pp_var fmt =
296
  fprintf fmt "%t.%t" pp_state pp_var
266 297

  
298
let pp_old pp fmt = fprintf fmt "%t'Old" pp
267 299

  
src/backends/Ada/ada_printer.mli
7 7

  
8 8
type visibility = AdaNoVisibility | AdaPrivate | AdaLimitedPrivate
9 9

  
10
type ada_var_decl = parameter_mode*printer*printer
10
type ada_with = (bool * (printer list) * (printer list)) option
11

  
12
type ada_var_decl = parameter_mode * printer * printer * ada_with
11 13

  
12 14
type ada_local_decl =
13 15
  | AdaLocalVar of ada_var_decl
......
16 18
type def_content =
17 19
  | AdaNoContent
18 20
  | AdaPackageContent of printer
21
  | AdaSimpleContent of printer
19 22
  | AdaVisibilityDefinition of visibility
20 23
  | AdaProcedureContent of ((ada_local_decl list list) * (printer list))
21 24
  | AdaRecord of (ada_var_decl list list)
22 25
  | AdaPackageInstanciation of (printer * ((printer*printer) list))
23 26

  
27
val pp_integer_type : printer
28
val pp_float_type : printer
29
val pp_boolean_type : printer
24 30

  
25 31
val pp_clean_ada_identifier : formatter -> string -> unit
26 32
val pp_package_access : (printer*printer) -> printer
......
28 34
val pp_oneline_comment : formatter -> string -> unit
29 35
val pp_with : visibility -> formatter -> printer -> unit
30 36
val pp_var_decl : ada_var_decl -> printer
37
val pp_access :  printer -> printer -> formatter -> unit
31 38
val pp_call : formatter -> (printer*(printer list list)) -> unit
39
val pp_old : printer -> printer
32 40

  
33 41
(* declaration printer *)
34 42
val pp_package : printer -> printer list -> bool -> formatter -> printer -> unit
35 43
val pp_package_instanciation : printer -> printer -> formatter -> (printer*printer) list -> unit
36 44
val pp_type_decl : printer -> visibility -> printer
37 45
val pp_record : printer -> formatter -> ada_var_decl list list -> unit
38
val pp_procedure : printer -> (ada_var_decl list list) -> printer option -> formatter -> def_content -> unit
46
val pp_procedure : printer -> (ada_var_decl list list) -> ada_with -> formatter -> def_content -> unit
47
val pp_predicate : printer -> (ada_var_decl list list) -> formatter -> ((((printer*printer) list)*(printer list)) option) -> unit
48

  
39 49
(* Local function :
40 50

  
41 51
val pp_parameter_mode : formatter -> parameter_mode -> unit
src/backends/Ada/misc_lustre_function.ml
1 1

  
2 2
open Machine_code_types
3 3
open Lustre_types
4
(*
5 4
open Corelang
5
(*
6 6
open Machine_code_common
7 7
*)
8 8

  
9
let is_machine_statefull m = m.mmemory != [] || m.mcalls != []
9
let is_machine_statefull m = not m.mname.node_dec_stateless
10 10

  
11 11
(** Return true if its the arrow machine
12 12
   @param machine the machine to test
......
35 35
    with
36 36
      Not_found -> assert false (*TODO*)
37 37

  
38
(** Test if two types are the same.
39
   @param typ1 the first type
40
   @param typ2 the second type
41
**)
42
let pp_eq_type typ1 typ2 = 
43
  let get_basic typ = match (Types.repr typ).Types.tdesc with
44
    | Types.Tbasic Types.Basic.Tint -> Types.Basic.Tint
45
    | Types.Tbasic Types.Basic.Treal -> Types.Basic.Treal
46
    | Types.Tbasic Types.Basic.Tbool -> Types.Basic.Tbool
47
    | _ -> assert false (*TODO*)
48
  in
49
  get_basic typ1 = get_basic typ2
50

  
51 38
(** Extract all the inputs and outputs.
52 39
   @param machine the machine
53 40
   @return a list of all the var_decl of a macine
......
97 84
  in
98 85
  List.flatten (List.map search_instr instr_list)
99 86

  
87
(* Replace this function by check_type_equal but be careful to the fact that
88
   this function chck equality and that it is both basic type.
89
   This might be a required feature when it used *)
90
(** Test if two types are the same.
91
   @param typ1 the first type
92
   @param typ2 the second type
93
**)
94
let pp_eq_type typ1 typ2 = 
95
  let get_basic typ = match (Types.repr typ).Types.tdesc with
96
    | Types.Tbasic Types.Basic.Tint -> Types.Basic.Tint
97
    | Types.Tbasic Types.Basic.Treal -> Types.Basic.Treal
98
    | Types.Tbasic Types.Basic.Tbool -> Types.Basic.Tbool
99
    | _ -> assert false (*TODO*)
100
  in
101
  get_basic typ1 = get_basic typ2
102

  
100 103
(** Check that two types are the same.
101 104
   @param t1 a type
102 105
   @param t2 an other type
......
218 221
    List.assoc identifier typed_submachines
219 222
  with Not_found -> assert false
220 223

  
224
(*Usefull for debug*)
225
let pp_type_debug fmt typ = 
226
  (match (Types.repr typ).Types.tdesc with
227
    | Types.Tbasic Types.Basic.Tint  -> Format.fprintf fmt "INTEGER"
228
    | Types.Tbasic Types.Basic.Treal -> Format.fprintf fmt "FLOAT"
229
    | Types.Tbasic Types.Basic.Tbool -> Format.fprintf fmt "BOOLEAN"
230
    | Types.Tunivar                  -> Format.fprintf fmt "POLY(%i)" typ.Types.tid
231
    | _ -> assert false
232
  )
233

  
234
let build_if g c1 i1 tl =
235
  let neg = c1=tag_false in
236
  let other = match tl with
237
    | []         -> None
238
    | [(c2, i2)] -> Some i2
239
    | _          -> assert false
240
  in
241
  match neg, other with
242
    | true, Some x -> (false, g, x, Some i1)
243
    | _ ->
244
  (neg, g, i1, other)
245

  
246
let rec push_if_in_expr = function
247
  | [] -> []
248
  | instr::q ->
249
    (
250
      match get_instr_desc instr with
251
        | MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
252
            let (neg, g, instrs1, instrs2) = build_if g c1 i1 tl in
253
            let instrs1_pushed = push_if_in_expr instrs1 in
254
            let get_assign instr = match get_instr_desc instr with
255
              | MLocalAssign (id, value) -> (false, id, value)
256
              | MStateAssign (id, value) -> (true, id, value)
257
              | _ -> assert false
258
            in
259
            let gen_eq ident state value1 value2 =
260
              assert(check_type_equal ident.var_type value1.value_type);
261
              assert(check_type_equal ident.var_type value2.value_type);
262
              let value = {
263
                            value_desc   = Fun ("ite", [g;value1;value2]);
264
                            value_type   = ident.var_type;
265
                            value_annot  = None
266
                          }
267
              in
268
              let assign = if state then MStateAssign (ident, value) else MLocalAssign (ident, value) in
269
              { instr_desc = assign;
270
                lustre_eq  = None
271
              }
272
            in
273
            let mkval_var id = {
274
                              value_desc   = Var id;
275
                              value_type   = id.var_type;
276
                              value_annot  = None
277
                            }
278
            in
279
            let rec find_split s1 id1 accu = function
280
              | [] -> [], accu, mkval_var id1
281
              | (s2, id2, v2)::q when s1 = s2
282
                                  && id1.var_id = id2.var_id -> accu, q, v2
283
              | t::q -> find_split s1 id1 (t::accu) q
284
            in
285
            let gen_from_else l =
286
              List.map
287
                (fun (s2, id2, v2) -> gen_eq id2 s2 (mkval_var id2) v2)
288
                l
289
            in
290
            let rec gen_assigns if_assigns else_assigns =
291
              let res, accu_else = match if_assigns with
292
                | (s1, id1, v1)::q ->
293
                  let accu, remain, v2 = find_split s1 id1 [] else_assigns in
294
                  (gen_eq id1 s1 v1 v2)::(gen_assigns q remain), accu
295
                | [] -> [], else_assigns
296
              in
297
              (gen_from_else accu_else)@res
298
            in
299
            let if_assigns = List.map get_assign instrs1_pushed in
300
            let else_assigns = match instrs2 with
301
              | None -> []
302
              | Some instrs2 -> 
303
                  let instrs2_pushed = push_if_in_expr instrs2 in
304
                  List.map get_assign instrs2_pushed
305
            in
306
            gen_assigns if_assigns else_assigns
307
        | x -> [instr]
308
      )@(push_if_in_expr q)
309

  
310

  
311

  
312

  

Also available in: Unified diff