Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

.ocamlformat
1
version=0.18.0
2
parens-tuple=multi-line-only
3
wrap-comments=true
4
cases-exp-indent=2
5
break-cases=nested
dune
1 1
; too bad dune does not support glob in install stanza
2 2
; (see https://discuss.ocaml.org/t/installing-many-files-with-dune/4143)
3 3
; TODO: open an issue?
4

  
4 5
(install
5
 (section (site (lustrec include_)))
6
 (section
7
  (site
8
   (lustrec include_)))
6 9
 (files
7
   include/conv.c
8
   include/conv.lusi
9
   include/conv.lusic
10
   include/mpfr_lustre.c
11
   include/mpfr_lustre.lusi
12
   include/mpfr_lustre.lusic
13
   include/mpfr_lustre.h
14
   include/simulink_math_fcn.c
15
   include/simulink_math_fcn.lusi
16
   include/simulink_math_fcn.lusic
17
   include/simulink_math_fcn.h
18
   include/lustrec_math.lusi
19
   include/lustrec_math.lusic
20
   include/lustrec_math.h
21
   include/arrow.c
22
   include/arrow.h
23
   include/arrow_spec.h
24
   include/arrow_spec.c
25
   include/arrow.cpp
26
   include/arrow.hpp
27
   include/io_frontend.c
28
   include/io_frontend.h
29
   include/io_frontend.hpp
30
   include/lustrec_math.smt2
31
   include/StdIn.java))
10
  include/conv.c
11
  include/conv.lusi
12
  include/conv.lusic
13
  include/mpfr_lustre.c
14
  include/mpfr_lustre.lusi
15
  include/mpfr_lustre.lusic
16
  include/mpfr_lustre.h
17
  include/simulink_math_fcn.c
18
  include/simulink_math_fcn.lusi
19
  include/simulink_math_fcn.lusic
20
  include/simulink_math_fcn.h
21
  include/lustrec_math.lusi
22
  include/lustrec_math.lusic
23
  include/lustrec_math.h
24
  include/arrow.c
25
  include/arrow.h
26
  include/arrow_spec.h
27
  include/arrow_spec.c
28
  include/arrow.cpp
29
  include/arrow.hpp
30
  include/io_frontend.c
31
  include/io_frontend.h
32
  include/io_frontend.hpp
33
  include/lustrec_math.smt2
34
  include/StdIn.java))
32 35

  
33 36
(install
34
 (section (site (lustrec testgen)))
35
 (files
36
   share/FindLustre.cmake
37
   share/helpful_functions.cmake))
37
 (section
38
  (site
39
   (lustrec testgen)))
40
 (files share/FindLustre.cmake share/helpful_functions.cmake))
38 41

  
39 42
(rule
40 43
 (alias runtest)
41
 (deps (source_tree tests/regression_tests))
42
 (action (chdir tests/regression_tests
43
          (progn
44
           (run cmake "-DSUBPROJ=\"unstable\"" "-DLUSTRE_INCLUDE_DIR=%{project_root}/include" .)
45
           (run ctest -D Experimental -R "COMPIL_LUS|MAKE|BIN|DIFF" -E LUSTRET --progress)))))
44
 (deps
45
  (source_tree tests/regression_tests))
46
 (action
47
  (chdir
48
   tests/regression_tests
49
   (progn
50
    (run
51
     cmake
52
     "-DSUBPROJ=\"unstable\""
53
     "-DLUSTRE_INCLUDE_DIR=%{project_root}/include"
54
     .)
55
    (run
56
     ctest
57
     -D
58
     Experimental
59
     -R
60
     "COMPIL_LUS|MAKE|BIN|DIFF"
61
     -E
62
     LUSTRET
63
     --progress)))))
include/dune
4 4

  
5 5
(rule
6 6
 (target conv.lusic)
7
 (action (run lustrec -verbose 0 -I . -d . %{dep:conv.lusi}))
7
 (action
8
  (run lustrec -verbose 0 -I . -d . %{dep:conv.lusi}))
8 9
 (alias install))
9 10

  
10 11
(rule
11 12
 (targets simulink_math_fcn.lusic simulink_math_fcn.h)
12
 (action (run lustrec -verbose 0 -I . -d . %{dep:simulink_math_fcn.lusi}))
13
 (action
14
  (run lustrec -verbose 0 -I . -d . %{dep:simulink_math_fcn.lusi}))
13 15
 (alias install))
14 16

  
15 17
(rule
16 18
 (targets lustrec_math.lusic lustrec_math.h)
17
 (action (run lustrec -verbose 0 -I . -d . %{dep:lustrec_math.lusi}))
19
 (action
20
  (run lustrec -verbose 0 -I . -d . %{dep:lustrec_math.lusi}))
18 21
 (alias install))
19 22

  
20 23
(rule
21 24
 (targets mpfr_lustre.lusic mpfr_lustre.h)
22
 (action (run lustrec -verbose 0 -mpfr 1 -d . %{dep:mpfr_lustre.lusi}))
25
 (action
26
  (run lustrec -verbose 0 -mpfr 1 -d . %{dep:mpfr_lustre.lusi}))
23 27
 (alias install))
src/annotations.ml
11 11

  
12 12
open Lustre_types
13 13

  
14

  
15 14
(* Associate to each annotation key the pair (node, expr tag) *)
16
let expr_annotations : (string list, ident * tag) Hashtbl.t=  Hashtbl.create 13
17
let node_annotations : (string list, ident) Hashtbl.t=  Hashtbl.create 13
15
let expr_annotations : (string list, ident * tag) Hashtbl.t = Hashtbl.create 13
16

  
17
let node_annotations : (string list, ident) Hashtbl.t = Hashtbl.create 13
18

  
19
let add_expr_ann node_id expr_tag key =
20
  Hashtbl.add expr_annotations key (node_id, expr_tag)
18 21

  
19
let add_expr_ann node_id expr_tag key = Hashtbl.add expr_annotations key (node_id, expr_tag)
20 22
let add_node_ann node_id key = Hashtbl.add node_annotations key node_id
21 23

  
22 24
let get_expr_annotations key = Hashtbl.find_all expr_annotations key
src/arrow.ml
9 9
    node_id = arrow_id;
10 10
    node_type = Type_predef.type_bin_poly_op;
11 11
    node_clock = Clock_predef.ck_bin_univ;
12
    node_inputs= [Corelang.dummy_var_decl "_in1" arrow_typ; Corelang.dummy_var_decl "_in2" arrow_typ];
13
    node_outputs= [Corelang.dummy_var_decl "_out" arrow_typ];
14
    node_locals= [];
12
    node_inputs =
13
      [
14
        Corelang.dummy_var_decl "_in1" arrow_typ;
15
        Corelang.dummy_var_decl "_in2" arrow_typ;
16
      ];
17
    node_outputs = [ Corelang.dummy_var_decl "_out" arrow_typ ];
18
    node_locals = [];
15 19
    node_gencalls = [];
16 20
    node_checks = [];
17 21
    node_asserts = [];
18
    node_stmts= [];
22
    node_stmts = [];
19 23
    node_dec_stateless = false;
20 24
    node_stateless = Some false;
21 25
    node_spec = None;
22 26
    node_annot = [];
23 27
    node_iscontract = false;
24
}
28
  }
25 29

  
26 30
let arrow_top_decl () =
27 31
  {
28 32
    top_decl_desc = Node arrow_desc;
29
    top_decl_owner = (Options_management.core_dependency "arrow");
33
    top_decl_owner = Options_management.core_dependency "arrow";
30 34
    top_decl_itf = false;
31
    top_decl_loc = Location.dummy_loc
35
    top_decl_loc = Location.dummy_loc;
32 36
  }
33 37

  
34
let td_is_arrow td =
35
  Corelang.node_name td = arrow_id
38
let td_is_arrow td = Corelang.node_name td = arrow_id
src/arrow.mli
1
val arrow_id: string
2
val arrow_top_decl: unit -> Lustre_types.top_decl
3
val arrow_desc: Lustre_types.node_desc
4
val td_is_arrow: Lustre_types.top_decl -> bool
1
val arrow_id : string
2

  
3
val arrow_top_decl : unit -> Lustre_types.top_decl
4

  
5
val arrow_desc : Lustre_types.node_desc
6

  
7
val td_is_arrow : Lustre_types.top_decl -> bool
src/automata.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
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
open Utils
13
open Lustre_types
14
open Corelang
15

  
16

  
17
type aut_state =
18
    {
19
      incoming_r' : var_decl;
20
      incoming_s' : var_decl;
21
      incoming_r : var_decl;
22
      incoming_s : var_decl;
23
      actual_r : var_decl;
24
      actual_s : var_decl
25
    }
26

  
27
let as_clock var_decl =
28
  let tydec = var_decl.var_dec_type in
29
  { var_decl with var_dec_type = { ty_dec_desc = Tydec_clock tydec.ty_dec_desc; ty_dec_loc = tydec.ty_dec_loc } }
30

  
31
let mkbool loc b =
32
 mkexpr loc (Expr_const (const_of_bool b))
33

  
34
let mkident loc id =
35
 mkexpr loc (Expr_ident id)
36

  
37
let mkconst loc id =
38
 mkexpr loc (Expr_const (Const_tag id))
39

  
40
let mkfby loc e1 e2 =
41
 mkexpr loc (Expr_arrow (e1, mkexpr loc (Expr_pre e2)))
42

  
43
let mkpair loc e1 e2 =
44
 mkexpr loc (Expr_tuple [e1; e2])
45

  
46
let mkidentpair loc restart state =
47
 mkexpr loc (Expr_tuple [mkident loc restart; mkident loc state])
48

  
49
let add_branch (loc, expr, restart, st) cont =
50
 mkexpr loc (Expr_ite (expr, mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st]), cont))
51

  
52
let mkhandler loc st unless until locals (stmts, asserts, annots) =
53
 {hand_state = st;
54
  hand_unless = unless;
55
  hand_until = until;
56
  hand_locals = locals;
57
  hand_stmts = stmts;
58
  hand_asserts = asserts;
59
  hand_annots = annots;
60
  hand_loc = loc}
61

  
62
let mkautomata loc id handlers =
63
  {aut_id = id;
64
   aut_handlers = handlers;
65
   aut_loc = loc}
66

  
67
let expr_of_exit loc restart state conds tag =
68
  mkexpr loc (Expr_when (List.fold_right add_branch conds (mkidentpair loc restart state), state, tag))
69

  
70
let unless_read reads handler =
71
  let res =
72
  List.fold_left (fun read (_, c, _, _) -> Utils.ISet.union read (get_expr_vars c)) reads handler.hand_unless
73
  in
74
(
75
(*
76
Format.eprintf "unless_reads %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements reads);
77
Format.eprintf "unless_reads' %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res);
78
*)
79
res
80
)
81

  
82
let until_read reads handler =
83
  List.fold_left (fun read (_, c, _, _) -> Utils.ISet.union read (get_expr_vars c)) reads handler.hand_until
84

  
85
let rec handler_read reads handler =
86
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
87
  let allvars =
88
    List.fold_left (fun read stmt ->
89
      match stmt with
90
      | Eq eq -> Utils.ISet.union read (get_expr_vars eq.eq_rhs)
91
      | Aut aut -> automata_read read aut) reads handler.hand_stmts
92
  in let res = ISet.diff allvars locals
93
     in
94
(
95
(*
96
Format.eprintf "handler_allvars %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements allvars);
97
Format.eprintf "handler_read %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res);
98
*)
99
res
100
)
101

  
102
and automata_read reads aut =
103
  List.fold_left (fun read handler -> until_read (handler_read (unless_read read handler) handler) handler) reads aut.aut_handlers
104

  
105
let rec handler_write writes handler =
106
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
107
  let allvars =
108
    List.fold_left (fun write stmt ->
109
      match stmt with
110
      | Eq eq -> List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs
111
      | Aut aut -> List.fold_left handler_write write aut.aut_handlers) writes handler.hand_stmts
112
  in ISet.diff allvars locals
113

  
114
let node_vars_of_idents node iset =
115
  List.fold_right (fun v res -> if ISet.mem v.var_id iset then v :: res else res) (get_node_vars node) []
116

  
117
let mkautomata_state nodeid used typedef loc id =
118
  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = loc } in
119
  let tydec_state id = { ty_dec_desc = Tydec_const id; ty_dec_loc = loc } in
120
  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = loc } in
121
  let incoming_r' = mk_new_name used (id ^ "__next_restart_in") in
122
  let incoming_s' = mk_new_name used (id ^ "__next_state_in") in
123
  let incoming_r = mk_new_name used (id ^ "__restart_in") in
124
  let incoming_s = mk_new_name used (id ^ "__state_in") in
125
  let actual_r = mk_new_name used (id ^ "__restart_act") in
126
  let actual_s = mk_new_name used (id ^ "__state_act") in
127
  {
128
    incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false, None, Some nodeid);
129
    incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid);
130
    incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false, None, Some nodeid);
131
    incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid);
132
    actual_r = mkvar_decl loc (actual_r  , tydec_bool, ckdec_any, false, None, Some nodeid);
133
    actual_s = mkvar_decl loc (actual_s  , tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid)
134
  }
135

  
136
let vars_of_aut_state aut_state =
137
  [aut_state.incoming_r'; aut_state.incoming_r; aut_state.actual_r; aut_state.incoming_s'; as_clock aut_state.incoming_s; as_clock aut_state.actual_s]
138

  
139
let node_of_unless nused node aut_id aut_state handler =
140
(*Format.eprintf "node_of_unless %s@." node.node_id;*)
141
  let inputs = unless_read ISet.empty handler in
142
  let var_inputs = aut_state.incoming_r (*:: aut_state.incoming_s*) :: (node_vars_of_idents node inputs) in
143
  let var_outputs = aut_state.actual_r :: aut_state.actual_s :: [] in
144
  let init_expr = mkpair handler.hand_loc (mkident handler.hand_loc aut_state.incoming_r.var_id) (mkconst handler.hand_loc handler.hand_state) in
145
(*  let init_expr = mkidentpair handler.hand_loc aut_state.incoming_r.var_id aut_state.incoming_s.var_id in *)
146
  let expr_outputs = List.fold_right add_branch handler.hand_unless init_expr in
147
  let eq_outputs = Eq (mkeq handler.hand_loc ([aut_state.actual_r.var_id; aut_state.actual_s.var_id], expr_outputs)) in
148
  let node_id = mk_new_name nused (Format.sprintf "%s__%s_unless" aut_id handler.hand_state) in
149
  let args = List.map (fun v -> mkexpr handler.hand_loc (Expr_when (mkident handler.hand_loc v.var_id, aut_state.incoming_s.var_id, handler.hand_state))) var_inputs in
150
  let reset = Some (mkident handler.hand_loc aut_state.incoming_r.var_id) in
151
  {
152
    node_id = node_id;
153
    node_type = Types.new_var ();
154
    node_clock = Clocks.new_var true;
155
    node_inputs = List.map copy_var_decl var_inputs;
156
    node_outputs = List.map copy_var_decl var_outputs;
157
    node_locals = [];
158
    node_gencalls = [];
159
    node_checks = [];
160
    node_asserts = []; 
161
    node_stmts = [ eq_outputs ];
162
    node_dec_stateless = false;
163
    node_stateless = None;
164
    node_spec = None;
165
    node_annot = [];
166
    node_iscontract = false;
167
  },
168
  mkexpr handler.hand_loc (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset))
169

  
170

  
171
let rename_output used name = mk_new_name used (Format.sprintf "%s_out" name)
172

  
173
let rec rename_stmts_outputs frename stmts =
174
  match stmts with
175
  | []           -> []
176
  | (Eq eq) :: q   -> let eq' = Eq { eq with eq_lhs = List.map frename eq.eq_lhs } in
177
		      eq' :: rename_stmts_outputs frename q
178
  | (Aut aut) :: q -> let handlers' = List.map (fun h -> { h with hand_stmts = rename_stmts_outputs frename h.hand_stmts}) aut.aut_handlers in
179
                      let aut' = Aut { aut with aut_handlers = handlers' } in
180
		      aut' :: rename_stmts_outputs frename q
181

  
182
let mk_frename used outputs =
183
  let table = ISet.fold (fun name table -> IMap.add name (rename_output used name) table) outputs IMap.empty in
184
  (fun name -> try IMap.find name table with Not_found -> name)
185

  
186
let node_of_assign_until nused used node aut_id aut_state handler =
187
(*Format.eprintf "node_of_assign_until %s@." node.node_id;*)
188
  let writes = handler_write ISet.empty handler in
189
  let inputs = ISet.diff (handler_read (until_read ISet.empty handler) handler) writes in
190
  let frename = mk_frename used writes in
191
  let var_inputs = aut_state.actual_r (*:: aut_state.actual_s*) :: node_vars_of_idents node inputs in
192
  let new_var_locals = node_vars_of_idents node writes in
193
  let var_outputs = List.sort IdentModule.compare (node_vars_of_idents node writes) in
194
  let new_var_outputs = List.map (fun vdecl -> { vdecl with var_id = frename vdecl.var_id }) var_outputs in
195
  let new_output_eqs = List.map2 (fun o o' -> Eq (mkeq handler.hand_loc ([o'.var_id], mkident handler.hand_loc o.var_id))) var_outputs new_var_outputs in
196
  let init_until = mkpair handler.hand_loc (mkconst handler.hand_loc tag_false) (mkconst handler.hand_loc handler.hand_state) in
197
  let until_expr = List.fold_right add_branch handler.hand_until init_until in
198
  let until_eq = Eq (mkeq handler.hand_loc ([aut_state.incoming_r.var_id; aut_state.incoming_s.var_id], until_expr)) in
199
  let node_id = mk_new_name nused (Format.sprintf "%s__%s_handler_until" aut_id handler.hand_state) in
200
  let args = List.map (fun v -> mkexpr handler.hand_loc (Expr_when (mkident handler.hand_loc v.var_id, aut_state.actual_s.var_id, handler.hand_state))) var_inputs in
201
  let reset = Some (mkident handler.hand_loc aut_state.actual_r.var_id) in
202
  List.fold_left (fun res v -> ISet.add v.var_id res) ISet.empty var_outputs,
203
  {
204
    node_id = node_id;
205
    node_type = Types.new_var ();
206
    node_clock = Clocks.new_var true;
207
    node_inputs = List.map copy_var_decl var_inputs;
208
    node_outputs = List.map copy_var_decl (aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs);
209
    node_locals = List.map copy_var_decl (new_var_locals @ handler.hand_locals);
210
    node_gencalls = [];
211
    node_checks = [];
212
    node_asserts = handler.hand_asserts; 
213
    node_stmts = until_eq :: new_output_eqs @ handler.hand_stmts;
214
    node_dec_stateless = false;
215
    node_stateless = None;
216
    node_spec = None;
217
    node_annot = handler.hand_annots;
218
    node_iscontract = false;
219
  },
220
  mkexpr handler.hand_loc (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset))
221

  
222
let typedef_of_automata aut =
223
  let tname = Format.sprintf "%s__type" aut.aut_id in
224
  { tydef_id = tname;
225
    tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers)
226
  }
227

  
228
let expand_automata nused used owner typedef node aut =
229
  let initial = (List.hd aut.aut_handlers).hand_state in
230
  let aut_state = mkautomata_state node.node_id used typedef aut.aut_loc aut.aut_id in
231
  let unodes = List.map (fun h -> node_of_unless nused node aut.aut_id aut_state h) aut.aut_handlers in
232
  let aunodes = List.map (fun h -> node_of_assign_until nused used node aut.aut_id aut_state h) aut.aut_handlers in
233
  let all_outputs = List.fold_left (fun all (outputs, _, _) -> ISet.union outputs all) ISet.empty aunodes in
234
  let unless_handlers = List.map2 (fun h (_, c) -> (h.hand_state, c)) aut.aut_handlers unodes in
235
  let unless_expr = mkexpr aut.aut_loc (Expr_merge (aut_state.incoming_s.var_id, unless_handlers)) in
236
  let unless_eq = mkeq aut.aut_loc ([aut_state.actual_r.var_id; aut_state.actual_s.var_id], unless_expr) in
237
  let assign_until_handlers = List.map2 (fun h (_, _, c) -> (h.hand_state, c)) aut.aut_handlers aunodes in
238
  let assign_until_expr = mkexpr aut.aut_loc (Expr_merge (aut_state.actual_s.var_id, assign_until_handlers)) in
239
  let assign_until_vars = [aut_state.incoming_r'.var_id; aut_state.incoming_s'.var_id] @ (ISet.elements all_outputs) in
240
  let assign_until_eq = mkeq aut.aut_loc (assign_until_vars, assign_until_expr) in
241
  let fby_incoming_expr = mkfby aut.aut_loc (mkpair aut.aut_loc (mkconst aut.aut_loc tag_false) (mkconst aut.aut_loc initial)) (mkidentpair aut.aut_loc aut_state.incoming_r'.var_id aut_state.incoming_s'.var_id) in
242
  let incoming_eq = mkeq aut.aut_loc ([aut_state.incoming_r.var_id; aut_state.incoming_s.var_id], fby_incoming_expr) in
243
  let locals' = vars_of_aut_state aut_state in
244
  let eqs' = [Eq unless_eq; Eq assign_until_eq; Eq incoming_eq] in
245
  (  List.map2 (fun h (n, _) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers unodes
246
   @ List.map2 (fun h (_, n, _) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers aunodes,
247
  locals',
248
  eqs')
249

  
250
let expand_node_stmt nused used owner node (top_types, top_nodes, locals, eqs) stmt =
251
  match stmt with
252
  | Eq eq -> (top_types, top_nodes, locals, (Eq eq)::eqs)
253
  | Aut aut ->
254
    let typedef = typedef_of_automata aut in
255
    let used' name = used name || List.exists (fun v -> v.var_id = name) locals in
256
    let nused' name =
257
      nused name ||
258
      List.exists (fun t -> match t.top_decl_desc with
259
      | ImportedNode nd -> nd.nodei_id = name | Node nd -> nd.node_id = name
260
      | _ -> false) top_nodes in
261
    let (top_decls', locals', eqs') = expand_automata nused' used' owner typedef node aut in
262
    let top_typedef = mktop_decl aut.aut_loc owner false (TypeDef typedef) in
263
    (top_typedef :: top_types, top_decls'@top_nodes, locals'@locals, eqs'@eqs)
264

  
265
let expand_node_stmts nused used loc owner node =
266
  let top_types', top_nodes', locals', eqs' =
267
    List.fold_left (expand_node_stmt nused used owner node) ([], [], [], []) node.node_stmts in
268
  let node' = 
269
    { node with node_locals = locals'@node.node_locals; node_stmts = eqs' } in
270
  let top_node = mktop_decl loc owner false (Node node') in
271
  top_types', top_node, top_nodes'
272

  
273
let rec expand_decls_rec nused top_decls =
274
  match top_decls with
275
  | [] -> []
276
  | top_decl::q ->
277
    match top_decl.top_decl_desc with
278
    | Node nd ->
279
      let used name =
280
        List.exists (fun v -> v.var_id = name) nd.node_inputs
281
        || List.exists (fun v -> v.var_id = name) nd.node_outputs
282
        || List.exists (fun v -> v.var_id = name) nd.node_locals in
283
      let top_types', top_decl', top_nodes' = expand_node_stmts nused used top_decl.top_decl_loc top_decl.top_decl_owner nd in
284
      top_types' @ (top_decl' :: expand_decls_rec nused (top_nodes'@q))
285
    | _       -> top_decl :: expand_decls_rec nused q
286

  
287
let expand_decls top_decls =
288
  let top_names = List.fold_left (fun names t -> match t.top_decl_desc with
289
      | Node nd         -> ISet.add nd.node_id names
290
      | ImportedNode nd -> ISet.add nd.nodei_id names
291
      | _               -> names) ISet.empty top_decls in
292
  let nused name = ISet.mem name top_names in
293
  expand_decls_rec nused top_decls
294

  
295
(* Local Variables: *)
296
(* compile-command:"make -C .." *)
297
(* End: *)
298

  
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
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
open Utils
13
open Lustre_types
14
open Corelang
15

  
16
type aut_state = {
17
  incoming_r' : var_decl;
18
  incoming_s' : var_decl;
19
  incoming_r : var_decl;
20
  incoming_s : var_decl;
21
  actual_r : var_decl;
22
  actual_s : var_decl;
23
}
24

  
25
let as_clock var_decl =
26
  let tydec = var_decl.var_dec_type in
27
  {
28
    var_decl with
29
    var_dec_type =
30
      {
31
        ty_dec_desc = Tydec_clock tydec.ty_dec_desc;
32
        ty_dec_loc = tydec.ty_dec_loc;
33
      };
34
  }
35

  
36
let mkbool loc b = mkexpr loc (Expr_const (const_of_bool b))
37

  
38
let mkident loc id = mkexpr loc (Expr_ident id)
39

  
40
let mkconst loc id = mkexpr loc (Expr_const (Const_tag id))
41

  
42
let mkfby loc e1 e2 = mkexpr loc (Expr_arrow (e1, mkexpr loc (Expr_pre e2)))
43

  
44
let mkpair loc e1 e2 = mkexpr loc (Expr_tuple [ e1; e2 ])
45

  
46
let mkidentpair loc restart state =
47
  mkexpr loc (Expr_tuple [ mkident loc restart; mkident loc state ])
48

  
49
let add_branch (loc, expr, restart, st) cont =
50
  mkexpr loc
51
    (Expr_ite
52
       ( expr,
53
         mkexpr loc (Expr_tuple [ mkbool loc restart; mkident loc st ]),
54
         cont ))
55

  
56
let mkhandler loc st unless until locals (stmts, asserts, annots) =
57
  {
58
    hand_state = st;
59
    hand_unless = unless;
60
    hand_until = until;
61
    hand_locals = locals;
62
    hand_stmts = stmts;
63
    hand_asserts = asserts;
64
    hand_annots = annots;
65
    hand_loc = loc;
66
  }
67

  
68
let mkautomata loc id handlers =
69
  { aut_id = id; aut_handlers = handlers; aut_loc = loc }
70

  
71
let expr_of_exit loc restart state conds tag =
72
  mkexpr loc
73
    (Expr_when
74
       ( List.fold_right add_branch conds (mkidentpair loc restart state),
75
         state,
76
         tag ))
77

  
78
let unless_read reads handler =
79
  let res =
80
    List.fold_left
81
      (fun read (_, c, _, _) -> Utils.ISet.union read (get_expr_vars c))
82
      reads handler.hand_unless
83
  in
84
  (* Format.eprintf "unless_reads %s = %a@." handler.hand_state (fprintf_list
85
     ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements reads);
86
     Format.eprintf "unless_reads' %s = %a@." handler.hand_state (fprintf_list
87
     ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res); *)
88
  res
89

  
90
let until_read reads handler =
91
  List.fold_left
92
    (fun read (_, c, _, _) -> Utils.ISet.union read (get_expr_vars c))
93
    reads handler.hand_until
94

  
95
let rec handler_read reads handler =
96
  let locals =
97
    List.fold_left
98
      (fun locals v -> ISet.add v.var_id locals)
99
      ISet.empty handler.hand_locals
100
  in
101
  let allvars =
102
    List.fold_left
103
      (fun read stmt ->
104
        match stmt with
105
        | Eq eq ->
106
          Utils.ISet.union read (get_expr_vars eq.eq_rhs)
107
        | Aut aut ->
108
          automata_read read aut)
109
      reads handler.hand_stmts
110
  in
111
  let res = ISet.diff allvars locals in
112
  (* Format.eprintf "handler_allvars %s = %a@." handler.hand_state (fprintf_list
113
     ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements
114
     allvars); Format.eprintf "handler_read %s = %a@." handler.hand_state
115
     (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v))
116
     (ISet.elements res); *)
117
  res
118

  
119
and automata_read reads aut =
120
  List.fold_left
121
    (fun read handler ->
122
      until_read (handler_read (unless_read read handler) handler) handler)
123
    reads aut.aut_handlers
124

  
125
let rec handler_write writes handler =
126
  let locals =
127
    List.fold_left
128
      (fun locals v -> ISet.add v.var_id locals)
129
      ISet.empty handler.hand_locals
130
  in
131
  let allvars =
132
    List.fold_left
133
      (fun write stmt ->
134
        match stmt with
135
        | Eq eq ->
136
          List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs
137
        | Aut aut ->
138
          List.fold_left handler_write write aut.aut_handlers)
139
      writes handler.hand_stmts
140
  in
141
  ISet.diff allvars locals
142

  
143
let node_vars_of_idents node iset =
144
  List.fold_right
145
    (fun v res -> if ISet.mem v.var_id iset then v :: res else res)
146
    (get_node_vars node) []
147

  
148
let mkautomata_state nodeid used typedef loc id =
149
  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = loc } in
150
  let tydec_state id = { ty_dec_desc = Tydec_const id; ty_dec_loc = loc } in
151
  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = loc } in
152
  let incoming_r' = mk_new_name used (id ^ "__next_restart_in") in
153
  let incoming_s' = mk_new_name used (id ^ "__next_state_in") in
154
  let incoming_r = mk_new_name used (id ^ "__restart_in") in
155
  let incoming_s = mk_new_name used (id ^ "__state_in") in
156
  let actual_r = mk_new_name used (id ^ "__restart_act") in
157
  let actual_s = mk_new_name used (id ^ "__state_act") in
158
  {
159
    incoming_r' =
160
      mkvar_decl loc
161
        (incoming_r', tydec_bool, ckdec_any, false, None, Some nodeid);
162
    incoming_s' =
163
      mkvar_decl loc
164
        ( incoming_s',
165
          tydec_state typedef.tydef_id,
166
          ckdec_any,
167
          false,
168
          None,
169
          Some nodeid );
170
    incoming_r =
171
      mkvar_decl loc
172
        (incoming_r, tydec_bool, ckdec_any, false, None, Some nodeid);
173
    incoming_s =
174
      mkvar_decl loc
175
        ( incoming_s,
176
          tydec_state typedef.tydef_id,
177
          ckdec_any,
178
          false,
179
          None,
180
          Some nodeid );
181
    actual_r =
182
      mkvar_decl loc (actual_r, tydec_bool, ckdec_any, false, None, Some nodeid);
183
    actual_s =
184
      mkvar_decl loc
185
        ( actual_s,
186
          tydec_state typedef.tydef_id,
187
          ckdec_any,
188
          false,
189
          None,
190
          Some nodeid );
191
  }
192

  
193
let vars_of_aut_state aut_state =
194
  [
195
    aut_state.incoming_r';
196
    aut_state.incoming_r;
197
    aut_state.actual_r;
198
    aut_state.incoming_s';
199
    as_clock aut_state.incoming_s;
200
    as_clock aut_state.actual_s;
201
  ]
202

  
203
let node_of_unless nused node aut_id aut_state handler =
204
  (*Format.eprintf "node_of_unless %s@." node.node_id;*)
205
  let inputs = unless_read ISet.empty handler in
206
  let var_inputs =
207
    aut_state.incoming_r
208
    (*:: aut_state.incoming_s*)
209
    :: node_vars_of_idents node inputs
210
  in
211
  let var_outputs = [ aut_state.actual_r; aut_state.actual_s ] in
212
  let init_expr =
213
    mkpair handler.hand_loc
214
      (mkident handler.hand_loc aut_state.incoming_r.var_id)
215
      (mkconst handler.hand_loc handler.hand_state)
216
  in
217
  (* let init_expr = mkidentpair handler.hand_loc aut_state.incoming_r.var_id
218
     aut_state.incoming_s.var_id in *)
219
  let expr_outputs = List.fold_right add_branch handler.hand_unless init_expr in
220
  let eq_outputs =
221
    Eq
222
      (mkeq handler.hand_loc
223
         ([ aut_state.actual_r.var_id; aut_state.actual_s.var_id ], expr_outputs))
224
  in
225
  let node_id =
226
    mk_new_name nused (Format.sprintf "%s__%s_unless" aut_id handler.hand_state)
227
  in
228
  let args =
229
    List.map
230
      (fun v ->
231
        mkexpr handler.hand_loc
232
          (Expr_when
233
             ( mkident handler.hand_loc v.var_id,
234
               aut_state.incoming_s.var_id,
235
               handler.hand_state )))
236
      var_inputs
237
  in
238
  let reset = Some (mkident handler.hand_loc aut_state.incoming_r.var_id) in
239
  ( {
240
      node_id;
241
      node_type = Types.new_var ();
242
      node_clock = Clocks.new_var true;
243
      node_inputs = List.map copy_var_decl var_inputs;
244
      node_outputs = List.map copy_var_decl var_outputs;
245
      node_locals = [];
246
      node_gencalls = [];
247
      node_checks = [];
248
      node_asserts = [];
249
      node_stmts = [ eq_outputs ];
250
      node_dec_stateless = false;
251
      node_stateless = None;
252
      node_spec = None;
253
      node_annot = [];
254
      node_iscontract = false;
255
    },
256
    mkexpr handler.hand_loc
257
      (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset)) )
258

  
259
let rename_output used name = mk_new_name used (Format.sprintf "%s_out" name)
260

  
261
let rec rename_stmts_outputs frename stmts =
262
  match stmts with
263
  | [] ->
264
    []
265
  | Eq eq :: q ->
266
    let eq' = Eq { eq with eq_lhs = List.map frename eq.eq_lhs } in
267
    eq' :: rename_stmts_outputs frename q
268
  | Aut aut :: q ->
269
    let handlers' =
270
      List.map
271
        (fun h ->
272
          { h with hand_stmts = rename_stmts_outputs frename h.hand_stmts })
273
        aut.aut_handlers
274
    in
275
    let aut' = Aut { aut with aut_handlers = handlers' } in
276
    aut' :: rename_stmts_outputs frename q
277

  
278
let mk_frename used outputs =
279
  let table =
280
    ISet.fold
281
      (fun name table -> IMap.add name (rename_output used name) table)
282
      outputs IMap.empty
283
  in
284
  fun name -> try IMap.find name table with Not_found -> name
285

  
286
let node_of_assign_until nused used node aut_id aut_state handler =
287
  (*Format.eprintf "node_of_assign_until %s@." node.node_id;*)
288
  let writes = handler_write ISet.empty handler in
289
  let inputs =
290
    ISet.diff (handler_read (until_read ISet.empty handler) handler) writes
291
  in
292
  let frename = mk_frename used writes in
293
  let var_inputs =
294
    aut_state.actual_r
295
    (*:: aut_state.actual_s*)
296
    :: node_vars_of_idents node inputs
297
  in
298
  let new_var_locals = node_vars_of_idents node writes in
299
  let var_outputs =
300
    List.sort IdentModule.compare (node_vars_of_idents node writes)
301
  in
302
  let new_var_outputs =
303
    List.map
304
      (fun vdecl -> { vdecl with var_id = frename vdecl.var_id })
305
      var_outputs
306
  in
307
  let new_output_eqs =
308
    List.map2
309
      (fun o o' ->
310
        Eq
311
          (mkeq handler.hand_loc
312
             ([ o'.var_id ], mkident handler.hand_loc o.var_id)))
313
      var_outputs new_var_outputs
314
  in
315
  let init_until =
316
    mkpair handler.hand_loc
317
      (mkconst handler.hand_loc tag_false)
318
      (mkconst handler.hand_loc handler.hand_state)
319
  in
320
  let until_expr = List.fold_right add_branch handler.hand_until init_until in
321
  let until_eq =
322
    Eq
323
      (mkeq handler.hand_loc
324
         ( [ aut_state.incoming_r.var_id; aut_state.incoming_s.var_id ],
325
           until_expr ))
326
  in
327
  let node_id =
328
    mk_new_name nused
329
      (Format.sprintf "%s__%s_handler_until" aut_id handler.hand_state)
330
  in
331
  let args =
332
    List.map
333
      (fun v ->
334
        mkexpr handler.hand_loc
335
          (Expr_when
336
             ( mkident handler.hand_loc v.var_id,
337
               aut_state.actual_s.var_id,
338
               handler.hand_state )))
339
      var_inputs
340
  in
341
  let reset = Some (mkident handler.hand_loc aut_state.actual_r.var_id) in
342
  ( List.fold_left (fun res v -> ISet.add v.var_id res) ISet.empty var_outputs,
343
    {
344
      node_id;
345
      node_type = Types.new_var ();
346
      node_clock = Clocks.new_var true;
347
      node_inputs = List.map copy_var_decl var_inputs;
348
      node_outputs =
349
        List.map copy_var_decl
350
          (aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs);
351
      node_locals = List.map copy_var_decl (new_var_locals @ handler.hand_locals);
352
      node_gencalls = [];
353
      node_checks = [];
354
      node_asserts = handler.hand_asserts;
355
      node_stmts = until_eq :: new_output_eqs @ handler.hand_stmts;
356
      node_dec_stateless = false;
357
      node_stateless = None;
358
      node_spec = None;
359
      node_annot = handler.hand_annots;
360
      node_iscontract = false;
361
    },
362
    mkexpr handler.hand_loc
363
      (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset)) )
364

  
365
let typedef_of_automata aut =
366
  let tname = Format.sprintf "%s__type" aut.aut_id in
367
  {
368
    tydef_id = tname;
369
    tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers);
370
  }
371

  
372
let expand_automata nused used owner typedef node aut =
373
  let initial = (List.hd aut.aut_handlers).hand_state in
374
  let aut_state =
375
    mkautomata_state node.node_id used typedef aut.aut_loc aut.aut_id
376
  in
377
  let unodes =
378
    List.map
379
      (fun h -> node_of_unless nused node aut.aut_id aut_state h)
380
      aut.aut_handlers
381
  in
382
  let aunodes =
383
    List.map
384
      (fun h -> node_of_assign_until nused used node aut.aut_id aut_state h)
385
      aut.aut_handlers
386
  in
387
  let all_outputs =
388
    List.fold_left
389
      (fun all (outputs, _, _) -> ISet.union outputs all)
390
      ISet.empty aunodes
391
  in
392
  let unless_handlers =
393
    List.map2 (fun h (_, c) -> h.hand_state, c) aut.aut_handlers unodes
394
  in
395
  let unless_expr =
396
    mkexpr aut.aut_loc
397
      (Expr_merge (aut_state.incoming_s.var_id, unless_handlers))
398
  in
399
  let unless_eq =
400
    mkeq aut.aut_loc
401
      ([ aut_state.actual_r.var_id; aut_state.actual_s.var_id ], unless_expr)
402
  in
403
  let assign_until_handlers =
404
    List.map2 (fun h (_, _, c) -> h.hand_state, c) aut.aut_handlers aunodes
405
  in
406
  let assign_until_expr =
407
    mkexpr aut.aut_loc
408
      (Expr_merge (aut_state.actual_s.var_id, assign_until_handlers))
409
  in
410
  let assign_until_vars =
411
    [ aut_state.incoming_r'.var_id; aut_state.incoming_s'.var_id ]
412
    @ ISet.elements all_outputs
413
  in
414
  let assign_until_eq =
415
    mkeq aut.aut_loc (assign_until_vars, assign_until_expr)
416
  in
417
  let fby_incoming_expr =
418
    mkfby aut.aut_loc
419
      (mkpair aut.aut_loc
420
         (mkconst aut.aut_loc tag_false)
421
         (mkconst aut.aut_loc initial))
422
      (mkidentpair aut.aut_loc aut_state.incoming_r'.var_id
423
         aut_state.incoming_s'.var_id)
424
  in
425
  let incoming_eq =
426
    mkeq aut.aut_loc
427
      ( [ aut_state.incoming_r.var_id; aut_state.incoming_s.var_id ],
428
        fby_incoming_expr )
429
  in
430
  let locals' = vars_of_aut_state aut_state in
431
  let eqs' = [ Eq unless_eq; Eq assign_until_eq; Eq incoming_eq ] in
432
  ( List.map2
433
      (fun h (n, _) -> mktop_decl h.hand_loc owner false (Node n))
434
      aut.aut_handlers unodes
435
    @ List.map2
436
        (fun h (_, n, _) -> mktop_decl h.hand_loc owner false (Node n))
437
        aut.aut_handlers aunodes,
438
    locals',
439
    eqs' )
440

  
441
let expand_node_stmt nused used owner node (top_types, top_nodes, locals, eqs)
442
    stmt =
443
  match stmt with
444
  | Eq eq ->
445
    top_types, top_nodes, locals, Eq eq :: eqs
446
  | Aut aut ->
447
    let typedef = typedef_of_automata aut in
448
    let used' name =
449
      used name || List.exists (fun v -> v.var_id = name) locals
450
    in
451
    let nused' name =
452
      nused name
453
      || List.exists
454
           (fun t ->
455
             match t.top_decl_desc with
456
             | ImportedNode nd ->
457
               nd.nodei_id = name
458
             | Node nd ->
459
               nd.node_id = name
460
             | _ ->
461
               false)
462
           top_nodes
463
    in
464
    let top_decls', locals', eqs' =
465
      expand_automata nused' used' owner typedef node aut
466
    in
467
    let top_typedef = mktop_decl aut.aut_loc owner false (TypeDef typedef) in
468
    ( top_typedef :: top_types,
469
      top_decls' @ top_nodes,
470
      locals' @ locals,
471
      eqs' @ eqs )
472

  
473
let expand_node_stmts nused used loc owner node =
474
  let top_types', top_nodes', locals', eqs' =
475
    List.fold_left
476
      (expand_node_stmt nused used owner node)
477
      ([], [], [], []) node.node_stmts
478
  in
479
  let node' =
480
    { node with node_locals = locals' @ node.node_locals; node_stmts = eqs' }
481
  in
482
  let top_node = mktop_decl loc owner false (Node node') in
483
  top_types', top_node, top_nodes'
484

  
485
let rec expand_decls_rec nused top_decls =
486
  match top_decls with
487
  | [] ->
488
    []
489
  | top_decl :: q -> (
490
    match top_decl.top_decl_desc with
491
    | Node nd ->
492
      let used name =
493
        List.exists (fun v -> v.var_id = name) nd.node_inputs
494
        || List.exists (fun v -> v.var_id = name) nd.node_outputs
495
        || List.exists (fun v -> v.var_id = name) nd.node_locals
496
      in
497
      let top_types', top_decl', top_nodes' =
498
        expand_node_stmts nused used top_decl.top_decl_loc
499
          top_decl.top_decl_owner nd
500
      in
501
      top_types' @ top_decl' :: expand_decls_rec nused (top_nodes' @ q)
502
    | _ ->
503
      top_decl :: expand_decls_rec nused q)
504

  
505
let expand_decls top_decls =
506
  let top_names =
507
    List.fold_left
508
      (fun names t ->
509
        match t.top_decl_desc with
510
        | Node nd ->
511
          ISet.add nd.node_id names
512
        | ImportedNode nd ->
513
          ISet.add nd.nodei_id names
514
        | _ ->
515
          names)
516
      ISet.empty top_decls
517
  in
518
  let nused name = ISet.mem name top_names in
519
  expand_decls_rec nused top_decls
520

  
521
(* Local Variables: *)
522
(* compile-command:"make -C .." *)
523
(* End: *)
src/backends/Ada/ada_backend.ml
11 11

  
12 12
open Format
13 13
open Machine_code_types
14

  
15 14
open Misc_lustre_function
16 15
open Ada_backend_common
17 16

  
18 17
let indent_size = 2
19 18

  
20
(** Log at level 2 a string message with some indentation.
21
   @param indent the indentation level
22
   @param info the message
23
**)
19
(** Log at level 2 a string message with some indentation. @param indent the
20
    indentation level @param info the message **)
24 21
let log_str_level_two indent info =
25
  let str_indent = String.make (indent*indent_size) ' ' in
22
  let str_indent = String.make (indent * indent_size) ' ' in
26 23
  let pp_message fmt = fprintf fmt "%s.. %s@." str_indent info in
27 24
  Log.report ~level:2 pp_message;
28 25
  Format.pp_print_flush Format.err_formatter ()
29 26

  
30
(** Write a new file with formatter
31
   @param destname folder where the file shoudl be created
32
   @param pp_filename function printing the filename
33
   @param pp_file function wich pretty print the file
34
   @param arg will be given to pp_filename and pp_file
35
**)
27
(** Write a new file with formatter @param destname folder where the file shoudl
28
    be created @param pp_filename function printing the filename @param pp_file
29
    function wich pretty print the file @param arg will be given to pp_filename
30
    and pp_file **)
36 31
let write_file destname pp_filename pp_file arg =
37 32
  let path = asprintf "%s%a" destname pp_filename arg in
38 33
  let out = open_out path in
39 34
  let fmt = formatter_of_out_channel out in
40
  log_str_level_two 2 ("generating "^path);
35
  log_str_level_two 2 ("generating " ^ path);
41 36
  pp_file fmt arg;
42 37
  pp_print_flush fmt ();
43 38
  close_out out
44 39

  
45

  
46
(** Exception raised when a machine contains a feature not supported by the
47
  Ada backend*)
48 40
exception CheckFailed of string
41
(** Exception raised when a machine contains a feature not supported by the Ada
42
    backend*)
49 43

  
50

  
51
(** Check that a machine match the requirement for an Ada compilation :
52
      - No constants.
53
   @param machine the machine to test
54
**)
44
(** Check that a machine match the requirement for an Ada compilation : - No
45
    constants. @param machine the machine to test **)
55 46
let check machine =
56 47
  match machine.mconst with
57
    | [] -> ()
58
    | _ -> raise (CheckFailed "machine.mconst should be void")
59

  
48
  | [] ->
49
    ()
50
  | _ ->
51
    raise (CheckFailed "machine.mconst should be void")
60 52

  
61 53
let get_typed_submachines machines m =
62
  let instances = List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls in
54
  let instances =
55
    List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls
56
  in
63 57
  let submachines = List.map (get_machine machines) instances in
64 58
  List.map2
65 59
    (fun instance submachine ->
66
      let ident = (fst instance) in
60
      let ident = fst instance in
67 61
      ident, (get_substitution m ident submachine, submachine))
68 62
    instances submachines
69 63

  
70 64
let extract_contract machines m =
71 65
  let rec find_submachine_from_ident ident = function
72
    | [] -> raise Not_found
73
    | h::_ when h.mname.node_id = ident -> h
74
    | _::t -> find_submachine_from_ident ident t
66
    | [] ->
67
      raise Not_found
68
    | h :: _ when h.mname.node_id = ident ->
69
      h
70
    | _ :: t ->
71
      find_submachine_from_ident ident t
75 72
  in
76 73
  let extract_ident eexpr =
77 74
    match eexpr.Lustre_types.eexpr_qfexpr.expr_desc with
78
      | Expr_ident ident -> ident
79
      | _ -> assert false
80
      (*
81
      | Expr_const cst -> assert false
82
      | Expr_tuple exprs -> assert false
83
      | Expr_ite (expr1, expr2, expr3) -> assert false
84
      | Expr_arrow (expr1, expr2)  -> assert false
85
      | Expr_fby (expr1, expr2) -> assert false
86
      | Expr_array exprs -> assert false
87
      | Expr_access (expr1, dim) -> assert false
88
      | Expr_power (expr1, dim) -> assert false
89
      | Expr_pre expr -> assert false
90
      | Expr_when (expr,ident,label) -> assert false
91
      | Expr_merge (ident, l) -> assert false
92
      | Expr_appl call -> assert false
93
      *)
75
    | Expr_ident ident ->
76
      ident
77
    | _ ->
78
      assert false
79
    (* | Expr_const cst -> assert false | Expr_tuple exprs -> assert false |
80
       Expr_ite (expr1, expr2, expr3) -> assert false | Expr_arrow (expr1,
81
       expr2) -> assert false | Expr_fby (expr1, expr2) -> assert false |
82
       Expr_array exprs -> assert false | Expr_access (expr1, dim) -> assert
83
       false | Expr_power (expr1, dim) -> assert false | Expr_pre expr -> assert
84
       false | Expr_when (expr,ident,label) -> assert false | Expr_merge (ident,
85
       l) -> assert false | Expr_appl call -> assert false *)
94 86
  in
95 87
  match m.mspec.mnode_spec with
96
    | Some (NodeSpec ident) ->
97
      begin
98
        let machine_spec = find_submachine_from_ident ident machines in
99
        let guarantees =
100
          match machine_spec.mspec.mnode_spec with
101
            | Some (Contract contract) ->
102
                assert (contract.consts=[]);
103
                assert (contract.locals=[]);
104
                assert (contract.stmts=[]);
105
                assert (contract.assume=[]);
106
                List.map extract_ident contract.guarantees
107
            | _ -> assert false
108
        in
109
        let opt_machine_spec =
110
          match machine_spec.mstep.step_instrs with
111
            | [] -> None
112
            | _ -> Some machine_spec
113
        in
114
        (opt_machine_spec, guarantees)
115
      end
116
    | _ -> None, []
88
  | Some (NodeSpec ident) ->
89
    let machine_spec = find_submachine_from_ident ident machines in
90
    let guarantees =
91
      match machine_spec.mspec.mnode_spec with
92
      | Some (Contract contract) ->
93
        assert (contract.consts = []);
94
        assert (contract.locals = []);
95
        assert (contract.stmts = []);
96
        assert (contract.assume = []);
97
        List.map extract_ident contract.guarantees
98
      | _ ->
99
        assert false
100
    in
101
    let opt_machine_spec =
102
      match machine_spec.mstep.step_instrs with
103
      | [] ->
104
        None
105
      | _ ->
106
        Some machine_spec
107
    in
108
    opt_machine_spec, guarantees
109
  | _ ->
110
    None, []
117 111

  
118 112
(** Main function of the Ada backend. It calls all the subfunction creating all
119
the file and fill them with Ada code representing the machines list given.
120
   @param basename name of the lustre file
121
   @param prog list of machines to translate
122
**)
113
    the file and fill them with Ada code representing the machines list given.
114
    @param basename name of the lustre file @param prog list of machines to
115
    translate **)
123 116
let translate_to_ada basename machines =
124 117
  let module Ads = Ada_backend_ads.Main in
125 118
  let module Adb = Ada_backend_adb.Main in
126 119
  let module Wrapper = Ada_backend_wrapper.Main in
127

  
128 120
  let is_real_machine m =
129
    match m.mspec.mnode_spec with
130
      | Some (Contract _) -> false
131
      | _ -> true
121
    match m.mspec.mnode_spec with Some (Contract _) -> false | _ -> true
132 122
  in
133 123

  
134 124
  let filtered_machines = List.filter is_real_machine machines in
135 125

  
136 126
  let typed_submachines =
137
    List.map (get_typed_submachines machines) filtered_machines in
138
  
127
    List.map (get_typed_submachines machines) filtered_machines
128
  in
129

  
139 130
  let contracts = List.map (extract_contract machines) filtered_machines in
140 131

  
141 132
  let _machines = List.combine contracts filtered_machines in
......
143 134
  let _machines = List.combine typed_submachines _machines in
144 135

  
145 136
  let _pp_filename ext fmt (_, (_, machine)) =
146
    pp_machine_filename ext fmt machine in
137
    pp_machine_filename ext fmt machine
138
  in
147 139

  
148 140
  (* Extract the main machine if there is one *)
149
  let main_machine = (match !Options.main_node with
150
  | "" -> None
151
  | main_node -> (
152
    match Machine_code_common.get_machine_opt filtered_machines main_node with
153
    | None -> begin
154
      Format.eprintf "Ada Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
155
      raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
156
    end
157
    | Some m -> Some m
158
  )) in
141
  let main_machine =
142
    match !Options.main_node with
143
    | "" ->
144
      None
145
    | main_node -> (
146
      match Machine_code_common.get_machine_opt filtered_machines main_node with
147
      | None ->
148
        Format.eprintf "Ada Code generation error: %a@." Error.pp_error_msg
149
          Error.Main_not_found;
150
        raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
151
      | Some m ->
152
        Some m)
153
  in
159 154

  
160 155
  let destname = !Options.dest_dir ^ "/" in
161 156

  
......
171 166
  (* If a main node is given we generate a main adb file and a project file *)
172 167
  log_str_level_two 1 "Generating wrapper files";
173 168
  (match main_machine with
174
    | None -> ()
175
    | Some machine ->
176
      write_file destname
177
        pp_main_filename
178
        (Wrapper.pp_main_adb (*get_typed_submachines filtered_machines machine*))
179
        machine;
180
      write_file destname
181
        (fun fmt _ -> Wrapper.pp_project_name (basename^"_exe") fmt)
182
        (Wrapper.pp_project_file filtered_machines basename)
183
        main_machine);
184
  write_file destname
185
    Wrapper.pp_project_configuration_name
169
  | None ->
170
    ()
171
  | Some machine ->
172
    write_file destname pp_main_filename Wrapper.pp_main_adb
173
      (*get_typed_submachines filtered_machines machine*)
174
      machine;
175
    write_file destname
176
      (fun fmt _ -> Wrapper.pp_project_name (basename ^ "_exe") fmt)
177
      (Wrapper.pp_project_file filtered_machines basename)
178
      main_machine);
179
  write_file destname Wrapper.pp_project_configuration_name
186 180
    (fun fmt _ -> Wrapper.pp_project_configuration_file fmt)
187 181
    basename;
188 182
  write_file destname
189
    (fun fmt _ -> Wrapper.pp_project_name (basename^"_lib") fmt)
183
    (fun fmt _ -> Wrapper.pp_project_name (basename ^ "_lib") fmt)
190 184
    (Wrapper.pp_project_file filtered_machines basename)
191
    None;
192

  
185
    None
193 186

  
194 187
(* Local Variables: *)
195 188
(* compile-command:"make -C ../../.." *)
src/backends/Ada/ada_backend_adb.ml
10 10
(********************************************************************)
11 11

  
12 12
open Format
13

  
14 13
open Machine_code_types
15 14
open Lustre_types
16 15
open Corelang
17 16
open Machine_code_common
18

  
19 17
open Misc_printer
20 18
open Misc_lustre_function
21 19
open Ada_printer
22 20
open Ada_backend_common
23 21

  
24
(** Main module for generating packages bodies
25
 **)
26
module Main =
27
struct
28

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

  
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
   **)
26
      @param fmt the formater to print on @param var_name the name of the
27
      variable @param value the value to be assigned **)
35 28
  let pp_assign env fmt var value =
36
    fprintf fmt "%a := %a"
37
      (pp_var env) var
38
      (pp_value env) value
29
    fprintf fmt "%a := %a" (pp_var env) var (pp_value env) value
39 30

  
40
  (** Printing function for instruction. See
41
      {!type:Machine_code_types.instr_t} for more details on
42
      machine types.
31
  (** Printing function for instruction. See {!type:Machine_code_types.instr_t}
32
      for more details on machine types.
43 33

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

Also available in: Unified diff