Project

General

Profile

Revision 3de9f6e4

View differences:

src/backends/Ada/ada_backend.ml
71 71
let pp_project_name fmt main_machine =
72 72
  fprintf fmt "%a.gpr" pp_package_name main_machine
73 73

  
74

  
75
let get_typed_instances machines m =
76
  let submachines = List.map (get_machine machines) m.minstances in
77
  List.map2
78
    (fun instance submachine ->
79
      let ident = (fst instance) in
80
      ident, (get_substitution m ident submachine, submachine))
81
    m.minstances submachines
82

  
74 83
(** Main function of the Ada backend. It calls all the subfunction creating all
75 84
the file and fill them with Ada code representing the machines list given.
76 85
   @param basename useless
......
83 92
  let module Adb = Ada_backend_adb.Main in
84 93
  let module Wrapper = Ada_backend_wrapper.Main in
85 94

  
95
  let typed_instances_machines =
96
    List.map (get_typed_instances machines) machines in
97

  
98
  let _machines = List.combine typed_instances_machines machines in
99

  
100
  let _pp_filename ext fmt (typed_instances, machine) =
101
    pp_machine_filename ext fmt machine in
102

  
86 103
  (* Extract the main machine if there is one *)
87 104
  let main_machine = (match !Options.main_node with
88 105
  | "" -> None
......
101 118
  List.iter check machines;
102 119

  
103 120
  log_str_level_two 1 "Generating ads";
104
  List.iter (write_file destname (pp_machine_filename "ads") (Ads.pp_file machines) ) machines;
121
  List.iter (write_file destname (_pp_filename "ads") Ads.pp_file) _machines;
105 122

  
106 123
  log_str_level_two 1 "Generating adb";
107
  List.iter (write_file destname (pp_machine_filename "adb") (Adb.pp_file machines)) machines;
124
  List.iter (write_file destname (_pp_filename "adb") Adb.pp_file) _machines;
108 125

  
109 126
  (* If a main node is given we generate a main adb file and a project file *)
110 127
  log_str_level_two 1 "Generating wrapper files";
src/backends/Ada/ada_backend_adb.ml
43 43
   **)
44 44
  let pp_assign m pp_var fmt var_name value = pp_basic_assign m
45 45

  
46
  (* Printing function for reset function *)
47
  (* TODO: clean the call to extract_node *)
48
  (** Printing function for reset function name.
46
  (** Extract from a machine the instance corresponding to the identifier,
47
        assume that the identifier exists in the instances of the machine.
49 48

  
50
      @param machines list of all machines
51
      @param machine the current machine
52
      @param fmt the formater to use
53
      @param encapsulated_node the node encapsulated in a pair
54
             [(instance, (node, static))]
55
   **)
56
  let pp_machine_reset_name machines m fmt encapsulated_node =
57
    let submachine = get_machine machines encapsulated_node in
58
    let substitution = get_substitution m (fst encapsulated_node) submachine in
59
    fprintf fmt "%a.reset" (pp_package_name_with_polymorphic substitution) submachine
49
     @param identifier the instance identifier
50
     @param machine a machine
51
     @return the instance of machine.minstances corresponding to identifier
52
  **)
53
  let get_instance identifier typed_instances =
54
    try
55
      List.assoc identifier typed_instances
56
    with Not_found -> assert false
60 57

  
61
  (** Printing function for reset function.
58
  (** Printing the reset function. call
62 59

  
63
      @param machines list of all machines
60
      @param typed_instances list of all typed machine instances of this machine
64 61
      @param machine the current machine
65
      @param fmt the formater to use
66 62
      @param instance the considered instance
63
      @param fmt the formater to use
67 64
   **)
68
  let pp_machine_reset machines (machine: machine_t) fmt instance =
69
    let node =
70
      try
71
        List.assoc instance machine.minstances
72
      with Not_found -> (Format.eprintf "internal error: pp_machine_reset %s %s:@." machine.mname.node_id instance; raise Not_found) in
73
    fprintf fmt "%a(%t.%s)"
74
      (pp_machine_reset_name machines machine) (instance, node)
65
  let pp_machine_reset typed_instances (machine: machine_t) fmt identifier =
66
    let (substitution, submachine) = get_instance identifier typed_instances in
67
    fprintf fmt "%a.%t(%t.%s)"
68
      (pp_package_name_with_polymorphic substitution) submachine
69
      pp_reset_procedure_name
75 70
      pp_state_name
76
      instance
71
      identifier
77 72

  
78 73
  (** Printing function for instruction. See
79 74
      {!type:Machine_code_types.instr_t} for more details on
80 75
      machine types.
81 76

  
82
      @param machines list of all machines
77
      @param typed_instances list of all typed machine instances of this machine
83 78
      @param machine the current machine
84 79
      @param fmt the formater to print on
85 80
      @param instr the instruction to print
86 81
   **)
87
  let pp_machine_instr machines machine fmt instr =
82
  let pp_machine_instr typed_instances machine fmt instr =
88 83
    match get_instr_desc instr with
89
    (* no reset *)
90
    | MNoReset _ -> ()
91
    (* reset  *)
92
    | MReset ident ->
93
      pp_machine_reset machines machine fmt ident
94
    | MLocalAssign (ident, value) ->
95
      pp_basic_assign machine fmt ident value
96
    | MStateAssign (ident, value) ->
97
      pp_basic_assign machine fmt ident value
98
    | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun
99
          (mk_val (Fun (i, vl)) i0.var_type)  ->
100
      fprintf fmt "Null"
101
    (* pp_machine_instr dependencies m self fmt
102
     *   (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type))) *)
103
    | MStep (il, i, vl) -> fprintf fmt "Null"
104

  
105
    (* pp_basic_instance_call m self fmt i vl il *)
106
    | MBranch (_, []) -> fprintf fmt "Null"
107

  
108
    (* (Format.eprintf "internal error: C_backend_src.pp_machine_instr %a@." (pp_instr m) instr; assert false) *)
109
    | MBranch (g, hl) -> fprintf fmt "Null"
110
    (* if let t = fst (List.hd hl) in t = tag_true || t = tag_false
111
     * then (\* boolean case, needs special treatment in C because truth value is not unique *\)
112
     *   (\* may disappear if we optimize code by replacing last branch test with default *\)
113
     *   let tl = try List.assoc tag_true  hl with Not_found -> [] in
114
     *   let el = try List.assoc tag_false hl with Not_found -> [] in
115
     *   pp_conditional dependencies m self fmt g tl el
116
     * else (\* enum type case *\)
117
     *   (\*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*\)
118
     *   fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
119
     *     (pp_c_val m self (pp_c_var_read m)) g
120
     *     (Utils.fprintf_list ~sep:"@," (pp_machine_branch dependencies m self)) hl *)
121
    | MComment s  ->
122
      fprintf fmt "-- %s@ " s
123
    | _ -> fprintf fmt "Don't  know"
124

  
125

  
126
(** Keep only the MReset from an instruction list.
127
  @param list to filter
128
**)
129
let filter_reset instr_list = List.map
130
    (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false)
131
  instr_list
84
      (* no reset *)
85
      | MNoReset _ -> ()
86
      (* reset  *)
87
      | MReset ident ->
88
          pp_machine_reset typed_instances machine fmt ident
89
      | MLocalAssign (ident, value) ->
90
          pp_basic_assign machine fmt ident value
91
      | MStateAssign (ident, value) ->
92
          pp_basic_assign machine fmt ident value
93
      | MStep ([i0], i, vl) when Basic_library.is_internal_fun i
94
                                   (List.map (fun v -> v.value_type) vl) ->
95
          let value = mk_val (Fun (i, vl)) i0.var_type in
96
          pp_basic_assign machine fmt i0 value
97
      | MStep (il, i, vl) -> fprintf fmt "Null"
98
      (* pp_basic_instance_call m self fmt i vl il *)
99
      | MBranch (_, []) -> fprintf fmt "Null"
100

  
101
      (* (Format.eprintf "internal error: C_backend_src.pp_machine_instr %a@." (pp_instr m) instr; assert false) *)
102
      | MBranch (g, hl) -> fprintf fmt "Null"
103
      (* if let t = fst (List.hd hl) in t = tag_true || t = tag_false
104
       * then (\* boolean case, needs special treatment in C because truth value is not unique *\)
105
       *   (\* may disappear if we optimize code by replacing last branch test with default *\)
106
       *   let tl = try List.assoc tag_true  hl with Not_found -> [] in
107
       *   let el = try List.assoc tag_false hl with Not_found -> [] in
108
       *   pp_conditional dependencies m self fmt g tl el
109
       * else (\* enum type case *\)
110
       *   (\*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*\)
111
       *   fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
112
       *     (pp_c_val m self (pp_c_var_read m)) g
113
       *     (Utils.fprintf_list ~sep:"@," (pp_machine_branch dependencies m self)) hl *)
114
      | MComment s  ->
115
        let lines = String.split_on_char '\n' s in
116
        fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines
132 117

  
133 118
(** Print the definition of the step procedure from a machine.
134 119

  
135
   @param machines list of all machines
120
   @param typed_instances list of all typed machine instances of this machine
136 121
   @param fmt the formater to print on
137 122
   @param machine the machine
138 123
**)
139
let pp_step_definition machines fmt m = pp_procedure_definition
124
let pp_step_definition typed_instances fmt m = pp_procedure_definition
140 125
      pp_step_procedure_name
141 126
      (pp_step_prototype m)
142 127
      (pp_machine_var_decl NoMode)
143
      (pp_machine_instr machines m)
128
      (pp_machine_instr typed_instances m)
144 129
      fmt
145 130
      (m.mstep.step_locals, m.mstep.step_instrs)
146 131

  
147 132
(** Print the definition of the reset procedure from a machine.
148 133

  
149
   @param machines list of all machines
134
   @param typed_instances list of all typed machine instances of this machine
150 135
   @param fmt the formater to print on
151 136
   @param machine the machine
152 137
**)
153
let pp_reset_definition machines fmt m = pp_procedure_definition
138
let pp_reset_definition typed_instances fmt m = pp_procedure_definition
154 139
      pp_reset_procedure_name
155 140
      (pp_reset_prototype m)
156 141
      (pp_machine_var_decl NoMode)
157
      (pp_machine_instr machines m)
142
      (pp_machine_instr typed_instances m)
158 143
      fmt
159 144
      ([], m.minit)
160 145

  
161
(** Print the package definition(adb) of a machine.
162

  
163
   @param machines list of all machines
146
(** Print the package definition(ads) of a machine.
147
  It requires the list of all typed instance.
148
  A typed submachine instance is (ident, type_machine) with ident
149
  the instance name and typed_machine is (substitution, machine) with machine
150
  the machine associated to the instance and substitution the instanciation of
151
  all its polymorphic types.
164 152
   @param fmt the formater to print on
165
   @param machine the machine
153
   @param typed_instances list of all typed machine instances of this machine
154
   @param m the machine
166 155
**)
167
let pp_file machines fmt machine =
156
let pp_file fmt (typed_instances, machine) =
168 157
  fprintf fmt "%a@,  @[<v>@,%a;@,@,%a;@,@]@,%a;@."
169 158
    (pp_begin_package true) machine (*Begin the package*)
170
    (pp_reset_definition machines) machine (*Define the reset procedure*)
171
    (pp_step_definition machines) machine (*Define the step procedure*)
159
    (pp_reset_definition typed_instances) machine (*Define the reset procedure*)
160
    (pp_step_definition typed_instances) machine (*Define the step procedure*)
172 161
    pp_end_package machine  (*End the package*)
173 162

  
174 163
end
src/backends/Ada/ada_backend_ads.ml
29 29
   @param ident the identifier of the subinstance
30 30
   @param submachine the submachine of the subinstance
31 31
**)
32
let pp_machine_subinstance_state_decl fmt (substitution, ident, submachine) =
32
let pp_machine_subinstance_state_decl fmt (ident, (substitution, submachine)) =
33 33
  pp_node_state_decl substitution ident fmt submachine
34 34

  
35 35
(** Print the state record for a machine.
36 36
   @param fmt the formater to print on
37 37
   @param var_list list of all state var
38
   @param typed_submachines list of pairs of instantiated types and machine
38
   @param typed_instances list typed instances
39 39
**)
40
let pp_state_record_definition fmt (var_list, typed_submachines) =
40
let pp_state_record_definition fmt (var_list, typed_instances) =
41 41
  fprintf fmt "@,  @[<v>record@,  @[<v>%a%t%a%t@]@,end record@]"
42 42
    (Utils.fprintf_list ~sep:";@;" pp_machine_subinstance_state_decl)
43
    typed_submachines
44
    (Utils.pp_final_char_if_non_empty ";@," typed_submachines)
43
    typed_instances
44
    (Utils.pp_final_char_if_non_empty ";@," typed_instances)
45 45
    (Utils.fprintf_list ~sep:";@;" (pp_machine_var_decl NoMode))
46 46
    var_list
47 47
    (Utils.pp_final_char_if_non_empty ";" var_list)
......
71 71
(** Print a new statement instantiating a generic package.
72 72
   @param fmt the formater to print on
73 73
   @param substitutions the instanciation substitution
74
   @param ident the name of the instance, useless in this function
75
   @param submachine the submachine to instanciate
74
   @param machine the machine to instanciate
76 75
**)
77
let pp_new_package fmt (substitutions, ident, submachine) =
76
let pp_new_package fmt (substitutions, machine) =
78 77
  fprintf fmt "package %a is new %a @[<v>(%a)@]"
79
    (pp_package_name_with_polymorphic substitutions) submachine
80
    pp_package_name submachine
78
    (pp_package_name_with_polymorphic substitutions) machine
79
    pp_package_name machine
81 80
    (Utils.fprintf_list ~sep:",@," pp_generic_instanciation) substitutions
82 81

  
83 82
let pp_eexpr fmt eexpr = fprintf fmt "true"
......
122 121
      fmt
123 122
      m.mspec
124 123

  
124
(** Remove duplicates from a list according to a given predicate.
125
   @param eq the predicate defining equality
126
   @param l the list to parse
127
**)
128
let remove_duplicates eq l =
129
  let aux l x = if List.exists (eq x) l then l else x::l in
130
  List.fold_left aux [] l
131

  
132

  
133
(** Compare two typed machines.
134
**)
135
let eq_typed_machine (subst1, machine1) (subst2, machine2) =
136
  (String.equal machine1.mname.node_id machine2.mname.node_id) &&
137
  (List.for_all2 (fun a b -> pp_eq_type (snd a) (snd b)) subst1 subst2)
138

  
139

  
125 140
(** Print the package declaration(ads) of a machine.
141
  It requires the list of all typed instance.
142
  A typed submachine instance is (ident, type_machine) with ident
143
  the instance name and typed_machine is (substitution, machine) with machine
144
  the machine associated to the instance and substitution the instanciation of
145
  all its polymorphic types.
126 146
   @param fmt the formater to print on
147
   @param typed_instances list of all typed machine instances of this machine
127 148
   @param m the machine
128 149
**)
129
let pp_file machines fmt m =
130
  let submachines = List.map (get_machine machines) m.minstances in
131
  let names = List.map fst m.minstances in
132
  let var_list = m.mmemory in
133
  let typed_submachines = List.map2
134
    (fun instance submachine ->
135
      let ident = (fst instance) in
136
      get_substitution m ident submachine, ident, submachine)
137
    m.minstances submachines in
138
  let extract_identifier (subst, _, submachine) =
139
    submachine.mname.node_id^"####"^(String.concat "####" (List.map (function (_, typ) -> (asprintf "%a" pp_type typ)) subst))
140
  in
141
  let identifiers = List.map extract_identifier typed_submachines in
142
  let typed_submachines_identified = List.combine identifiers typed_submachines in
143
  let typed_submachines_identified_set = List.fold_left (fun l x -> if List.mem_assoc (fst x) l then l else x::l) [] typed_submachines_identified in
144
  let submachines_set = List.map (function (_, (_, _, machine)) -> machine) typed_submachines_identified_set in
145
  let typed_submachines_set = snd (List.split typed_submachines_identified_set) in
146
  let pp_record fmt =
147
    pp_state_record_definition fmt (var_list, typed_submachines) in
148
  let typed_submachines_filtered =
149
    List.filter (function (l, _, _) -> l != []) typed_submachines_set in
150
let pp_file fmt (typed_instances, m) =
151
  let typed_machines = snd (List.split typed_instances) in
152
  let typed_machines_set = remove_duplicates eq_typed_machine typed_machines in
153
  
154
  let machines_to_import = snd (List.split typed_machines_set) in
155

  
150 156
  let polymorphic_types = find_all_polymorphic_type m in
157
  
158
  let typed_machines_to_instanciate =
159
    List.filter (fun (l, _) -> l != []) typed_machines_set in
160
  
161
  let pp_record fmt =
162
    pp_state_record_definition fmt (m.mmemory, typed_instances) in
163
  
164
  
151 165
  fprintf fmt "@[<v>%a%t%a%a@,  @[<v>@,%a;@,@,%t;@,@,%a;@,@,private@,@,%a%t%a;@,@]@,%a;@.@]"
152 166
    
153 167
    (* Include all the subinstance*)
154
    (Utils.fprintf_list ~sep:";@," pp_with_machine) submachines_set
155
    (Utils.pp_final_char_if_non_empty ";@,@," submachines_set)
168
    (Utils.fprintf_list ~sep:";@," pp_with_machine) machines_to_import
169
    (Utils.pp_final_char_if_non_empty ";@,@," machines_to_import)
156 170
    
157 171
    pp_generic polymorphic_types
158 172
    
......
168 182
    (*Declare the step procedure*)
169 183
    pp_step_prototype_contract m
170 184
    
171
    (*Instantiate the polymorphic type that need to be instantiate*)
172
    (Utils.fprintf_list ~sep:";@," pp_new_package) typed_submachines_filtered
173
    (Utils.pp_final_char_if_non_empty ";@,@," typed_submachines_filtered)
185
    (*Instantiate the polymorphic type that need to be instantiated*)
186
    (Utils.fprintf_list ~sep:";@," pp_new_package) typed_machines_to_instanciate
187
    (Utils.pp_final_char_if_non_empty ";@,@," typed_machines_to_instanciate)
174 188
    
175 189
    (*Define the state type*)
176 190
    pp_type_decl (pp_state_type, pp_record)
src/backends/Ada/ada_backend_common.ml
150 150
    | _ -> assert false (*TODO*)
151 151

  
152 152
(** Extract from a machine list the one corresponding to the given instance.
153
      assume that the machine is in the list.
153 154
   @param machines list of all machines
154 155
   @param instance instance of a machine
155 156
   @return the machine corresponding to hte given instance
156 157
**)
157 158
let get_machine machines instance =
158 159
    let id = (extract_node instance).node_id in
159
    List.find  (function m -> m.mname.node_id=id) machines
160
    try
161
      List.find (function m -> m.mname.node_id=id) machines
162
    with
163
      Not_found -> assert false
160 164

  
161 165

  
162 166
(* Type pretty print functions *)
......
218 222
    | Types.Tbasic Types.Basic.Treal -> pp_float_type fmt
219 223
    | Types.Tbasic Types.Basic.Tbool -> pp_boolean_type fmt
220 224
    | Types.Tunivar _                -> pp_polymorphic_type fmt typ.tid
225
    | Types.Tbasic _                 -> eprintf "Tbasic@."; assert false (*TODO*)
221 226
    | Types.Tconst _                 -> eprintf "Tconst@."; assert false (*TODO*)
222 227
    | Types.Tclock _                 -> eprintf "Tclock@."; assert false (*TODO*)
223 228
    | Types.Tarrow _                 -> eprintf "Tarrow@."; assert false (*TODO*)
......
231 236
    | _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false (*TODO*)
232 237
  )
233 238

  
239

  
240
(** Test if two types are the same.
241
   @param typ1 the first type
242
   @param typ2 the second type
243
**)
244
let pp_eq_type typ1 typ2 = 
245
  let get_basic typ = match (Types.repr typ).Types.tdesc with
246
    | Types.Tbasic Types.Basic.Tint -> Types.Basic.Tint
247
    | Types.Tbasic Types.Basic.Treal -> Types.Basic.Treal
248
    | Types.Tbasic Types.Basic.Tbool -> Types.Basic.Tbool
249
    | _ -> assert false (*TODO*)
250
  in
251
  get_basic typ1 = get_basic typ2
252

  
253

  
234 254
(** Print the type of a variable.
235 255
   @param fmt the formater to print on
236 256
   @param id the variable
......
438 458
let pp_clear_prototype m fmt =
439 459
  pp_base_prototype InOut m.mstatic [] fmt pp_clear_procedure_name
440 460

  
461
(** Print a one line comment with the final new line character to avoid
462
      commenting anything else.
463
   @param fmt the formater to print on
464
   @param s the comment without newline character
465
**)
466
let pp_oneline_comment fmt s =
467
  assert (not (String.contains s '\n'));
468
  fprintf fmt "-- %s@," s
441 469

  
442 470
(* Functions which computes the substitution for polymorphic type *)
443 471
(** Find a submachine step call in a list of instructions.
......
487 515
    begin
488 516
      (* We check that the type corresponding to type_poly in the subsitution
489 517
         match typ *)
490
      assert(check_type_equal (List.assoc type_poly.tid substituion) typ);
518
      (try
519
        assert(check_type_equal (List.assoc type_poly.tid substituion) typ)
520
      with
521
        Not_found -> assert false);
491 522
      (* We return the original substituion, it is already correct *)
492 523
      substituion
493 524
    end
......
556 587
       polymorphic type of the node *)
557 588
  let polymorphic_types = find_all_polymorphic_type submachine in
558 589
  assert (List.length polymorphic_types = List.length substitution);
559
  assert (List.for_all (function x->List.mem_assoc x substitution) polymorphic_types);
590
  (try
591
    assert (List.for_all (fun x -> List.mem_assoc x substitution) polymorphic_types)
592
  with
593
    Not_found -> assert false);
560 594
  substitution
561 595

  
562 596

  

Also available in: Unified diff