Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
.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 |
Also available in: Unified diff
reformatting