Project

General

Profile

Download (8.55 KB) Statistics
| Branch: | Tag: | Revision:
1 f20d8ac7 Christophe Garion
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11
12 48a6309c Guillaume DAVY
open Format
13 bdc471f3 Guillaume DAVY
14 48a6309c Guillaume DAVY
open Machine_code_types
15
open Lustre_types
16
open Corelang
17
open Machine_code_common
18 230b168e Guillaume DAVY
19
open Misc_printer
20
open Misc_lustre_function
21
open Ada_printer
22 bdc471f3 Guillaume DAVY
open Ada_backend_common
23
24 768f60f0 Christophe Garion
(** Main module for generating packages bodies
25
 **)
26 f20d8ac7 Christophe Garion
module Main =
27
struct
28 48a6309c Guillaume DAVY
29 b5b745fb Guillaume DAVY
  (** Printing function for basic assignement [var := value].
30 768f60f0 Christophe Garion
31
      @param fmt the formater to print on
32
      @param var_name the name of the variable
33
      @param value the value to be assigned
34
   **)
35 b5b745fb Guillaume DAVY
  let pp_assign env fmt var value =
36 c85c2e3d Christophe Garion
    fprintf fmt "%a := %a"
37 b5b745fb Guillaume DAVY
      (pp_var env) var
38
      (pp_value env) value
39 768f60f0 Christophe Garion
40
  (** Printing function for instruction. See
41
      {!type:Machine_code_types.instr_t} for more details on
42
      machine types.
43
44 09d7b39f Guillaume DAVY
      @param typed_submachines list of all typed machine instances of this machine
45 768f60f0 Christophe Garion
      @param machine the current machine
46
      @param fmt the formater to print on
47
      @param instr the instruction to print
48
   **)
49 b5b745fb Guillaume DAVY
  let rec pp_machine_instr typed_submachines env instr fmt =
50
    let pp_instr = pp_machine_instr typed_submachines env in
51 6e3cdaf6 Guillaume DAVY
    (* Print args for a step call *)
52 826063db Guillaume DAVY
    let pp_state i fmt = fprintf fmt "%t.%s" pp_state_name i in
53 6e3cdaf6 Guillaume DAVY
    (* Print a when branch of a case *)
54 230b168e Guillaume DAVY
    let pp_when (cond, instrs) fmt =
55
      fprintf fmt "when %s =>@,%a" cond pp_block (List.map pp_instr instrs)
56 6e3cdaf6 Guillaume DAVY
    in
57
    (* Print a case *)
58 525eebd1 Guillaume DAVY
    let pp_case fmt (g, hl) =
59
      fprintf fmt "case %a is@,%aend case"
60 b5b745fb Guillaume DAVY
        (pp_value env) g
61 230b168e Guillaume DAVY
        pp_block (List.map pp_when hl)
62 525eebd1 Guillaume DAVY
    in
63
    (* Print a if *)
64
    (* If neg is true the we must test for the negation of the condition. It
65
       first check that we don't have a negation and a else case, if so it
66
       inverses the two branch and remove the negation doing a recursive
67
       call. *)
68 b5b745fb Guillaume DAVY
    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
84 6e3cdaf6 Guillaume DAVY
    in
85 768f60f0 Christophe Garion
    match get_instr_desc instr with
86 3de9f6e4 Guillaume DAVY
      (* no reset *)
87
      | MNoReset _ -> ()
88
      (* reset  *)
89 826063db Guillaume DAVY
      | MReset i when List.mem_assoc i typed_submachines ->
90
          let (substitution, submachine) = get_instance i typed_submachines in
91 230b168e Guillaume DAVY
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
92
          let args = if is_machine_statefull submachine then [[pp_state i]] else [] in
93
          pp_call fmt (pp_package_access (pp_package, pp_reset_procedure_name), args)
94 3de9f6e4 Guillaume DAVY
      | MLocalAssign (ident, value) ->
95 b5b745fb Guillaume DAVY
          pp_assign env fmt ident value
96 3de9f6e4 Guillaume DAVY
      | MStateAssign (ident, value) ->
97 b5b745fb Guillaume DAVY
          pp_assign env fmt ident value
98 09d7b39f Guillaume DAVY
      | MStep ([i0], i, vl) when is_builtin_fun i ->
99 3de9f6e4 Guillaume DAVY
          let value = mk_val (Fun (i, vl)) i0.var_type in
100 b5b745fb Guillaume DAVY
            pp_assign env fmt i0 value
101 09d7b39f Guillaume DAVY
      | MStep (il, i, vl) when List.mem_assoc i typed_submachines ->
102 826063db Guillaume DAVY
          let (substitution, submachine) = get_instance i typed_submachines in
103 230b168e Guillaume DAVY
          let pp_package = pp_package_name_with_polymorphic substitution submachine in
104 b5b745fb Guillaume DAVY
          let input = List.map (fun x fmt -> pp_value env fmt x) vl in
105
          let output = List.map pp_var_name il in
106 230b168e Guillaume DAVY
          let args =
107
            (if is_machine_statefull submachine then [[pp_state i]] else [])
108
              @(if input!=[] then [input] else [])
109
              @(if output!=[] then [output] else [])
110
          in
111
          pp_call fmt (pp_package_access (pp_package, pp_step_procedure_name), args)
112 6e3cdaf6 Guillaume DAVY
      | MBranch (_, []) -> assert false
113 525eebd1 Guillaume DAVY
      | MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
114 b5b745fb Guillaume DAVY
          pp_if fmt (build_if g c1 i1 tl)
115 6e3cdaf6 Guillaume DAVY
      | MBranch (g, hl) -> pp_case fmt (g, hl)
116 3de9f6e4 Guillaume DAVY
      | MComment s  ->
117 6e3cdaf6 Guillaume DAVY
          let lines = String.split_on_char '\n' s in
118
          fprintf fmt "%a" (Utils.fprintf_list ~sep:"" pp_oneline_comment) lines
119 09d7b39f Guillaume DAVY
      | _ -> assert false
120 3d85297f Guillaume DAVY
121 8d22ea35 Guillaume DAVY
  (** Print the definition of the step procedure from a machine.
122
123
     @param typed_submachines list of all typed machine instances of this machine
124
     @param fmt the formater to print on
125
     @param machine the machine
126
  **)
127 173a2a8f Guillaume DAVY
  let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
128 b5b745fb Guillaume DAVY
    let transform_local_to_state_assign instr = match instr.instr_desc with
129
      | MLocalAssign (ident, value) -> 
130 75c459f4 Lélio Brun
        { instr with instr_desc = MStateAssign (ident, value) }
131 ca7e8027 Lélio Brun
      | _ -> instr
132 230b168e Guillaume DAVY
    in
133 173a2a8f Guillaume DAVY
    let pp_local_ghost_list, spec_instrs = match m_spec_opt with
134
      | None -> [], []
135
      | Some m_spec ->
136 05f85b44 Guillaume DAVY
          List.map (build_pp_var_decl_local (Some (true, false, [], []))) (List.filter (fun x -> not (List.mem x.var_id guarantees)) m_spec.mstep.step_locals),
137 173a2a8f Guillaume DAVY
          List.map transform_local_to_state_assign m_spec.mstep.step_instrs
138 230b168e Guillaume DAVY
    in
139 b5b745fb Guillaume DAVY
    let pp_local_list = List.map (build_pp_var_decl_local None) (m.mstep.step_locals) in
140
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (m.mstep.step_instrs@spec_instrs) in
141 173a2a8f Guillaume DAVY
    let content = AdaProcedureContent ((if pp_local_ghost_list = [] then [] else [pp_local_ghost_list])@(if pp_local_list = [] then [] else [pp_local_list]), pp_instr_list) in
142 230b168e Guillaume DAVY
    pp_procedure pp_step_procedure_name (build_pp_arg_step m) None fmt content
143 8d22ea35 Guillaume DAVY
144
  (** Print the definition of the reset procedure from a machine.
145
146
     @param typed_submachines list of all typed machine instances of this machine
147
     @param fmt the formater to print on
148
     @param machine the machine
149
  **)
150 173a2a8f Guillaume DAVY
  let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
151 61e0c3c4 Guillaume DAVY
    let build_assign = function var ->
152 75c459f4 Lélio Brun
      mkinstr Spec_types.True (MStateAssign (var, mk_default_value var.var_type))
153 61e0c3c4 Guillaume DAVY
    in
154 173a2a8f Guillaume DAVY
    let env, memory = match m_spec_opt with
155
      | None -> env, m.mmemory
156 ca7e8027 Lélio Brun
      | Some _ ->
157 173a2a8f Guillaume DAVY
          env,
158
          (m.mmemory)
159
    in
160
    let assigns = List.map build_assign memory in
161 b5b745fb Guillaume DAVY
    let pp_instr_list = List.map (pp_machine_instr typed_submachines env) (assigns@m.minit) in
162 230b168e Guillaume DAVY
    pp_procedure pp_reset_procedure_name (build_pp_arg_reset m) None fmt (AdaProcedureContent ([], pp_instr_list))
163 8d22ea35 Guillaume DAVY
164
  (** Print the package definition(ads) of a machine.
165
    It requires the list of all typed instance.
166
    A typed submachine instance is (ident, type_machine) with ident
167
    the instance name and typed_machine is (substitution, machine) with machine
168
    the machine associated to the instance and substitution the instanciation of
169
    all its polymorphic types.
170
     @param fmt the formater to print on
171
     @param typed_submachines list of all typed machine instances of this machine
172
     @param m the machine
173
  **)
174 05f85b44 Guillaume DAVY
  let pp_file fmt (typed_submachines, ((opt_spec_machine, guarantees), machine)) =
175 b5b745fb Guillaume DAVY
    let env = List.map (fun x -> x.var_id, pp_state_name) machine.mmemory in
176 8d22ea35 Guillaume DAVY
    let pp_reset fmt =
177
      if is_machine_statefull machine then
178 173a2a8f Guillaume DAVY
        fprintf fmt "%a;@,@," (pp_reset_definition env typed_submachines) (machine, opt_spec_machine)
179 09d7b39f Guillaume DAVY
      else
180 8d22ea35 Guillaume DAVY
        fprintf fmt ""
181
    in
182
    let aux pkgs (id, _) =
183
      try
184
        let (pkg, _) = List.assoc id ada_supported_funs in
185
        if List.mem pkg pkgs then
186
          pkgs
187
        else
188
          pkg::pkgs
189
      with Not_found -> pkgs
190
    in
191 230b168e Guillaume DAVY
    let packages = List.map pp_str (List.fold_left aux [] machine.mcalls) in
192
    let pp_content fmt =
193
      fprintf fmt "%t%a"
194
        (*Define the reset procedure*)
195
        pp_reset
196
        
197
        (*Define the step procedure*)
198 173a2a8f Guillaume DAVY
        (pp_step_definition env typed_submachines) (machine, opt_spec_machine, guarantees)
199 230b168e Guillaume DAVY
    in
200
    fprintf fmt "%a%t%a;@."
201 8d22ea35 Guillaume DAVY
      
202
      (* Include all the required packages*)
203 173a2a8f Guillaume DAVY
      (Utils.fprintf_list ~sep:";@," (pp_with AdaPrivate)) packages
204 8d22ea35 Guillaume DAVY
      (Utils.pp_final_char_if_non_empty ";@,@," packages)
205
      
206 230b168e Guillaume DAVY
      (*Print package*)
207
      (pp_package (pp_package_name machine) [] true ) pp_content
208 48a6309c Guillaume DAVY
209 f20d8ac7 Christophe Garion
end
210 768f60f0 Christophe Garion
211
(* Local Variables: *)
212
(* compile-command: "make -C ../../.." *)
213
(* End: *)