lustrec / src / stateless.ml @ 2823bc51
History | View | Annotate | Download (3.47 KB)
1 | a2d97a3e | ploc | (********************************************************************) |
---|---|---|---|
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 | 01c7d5e1 | ploc | open LustreSpec |
13 | e135421f | xthirioux | open Corelang |
14 | |||
15 | type error = |
||
16 | 04a63d25 | xthirioux | | Stateful_kwd of ident |
17 | | Stateful_imp of ident |
||
18 | | Stateful_ext_C of ident |
||
19 | e135421f | xthirioux | |
20 | exception Error of Location.t * error |
||
21 | |||
22 | let rec check_expr expr = |
||
23 | match expr.expr_desc with |
||
24 | | Expr_const _ |
||
25 | | Expr_ident _ -> true |
||
26 | | Expr_tuple el |
||
27 | | Expr_array el -> List.for_all check_expr el |
||
28 | | Expr_access (e1, _) |
||
29 | | Expr_power (e1, _) -> check_expr e1 |
||
30 | | Expr_ite (c, t, e) -> check_expr c && check_expr t && check_expr e |
||
31 | | Expr_arrow _ |
||
32 | | Expr_fby _ |
||
33 | | Expr_pre _ -> false |
||
34 | | Expr_when (e', i, l)-> check_expr e' |
||
35 | | Expr_merge (i, hl) -> List.for_all (fun (t, h) -> check_expr h) hl |
||
36 | | Expr_appl (i, e', i') -> |
||
37 | check_expr e' && |
||
38 | 04a63d25 | xthirioux | (Basic_library.is_stateless_fun i || check_node (node_from_name i)) |
39 | e135421f | xthirioux | and compute_node nd = |
40 | b08ffca7 | xthirioux | List.for_all (fun eq -> check_expr eq.eq_rhs) (get_node_eqs nd) |
41 | e135421f | xthirioux | and check_node td = |
42 | match td.top_decl_desc with |
||
43 | | Node nd -> ( |
||
44 | match nd.node_stateless with |
||
45 | | None -> |
||
46 | begin |
||
47 | let stateless = compute_node nd in |
||
48 | nd.node_stateless <- Some stateless; |
||
49 | if nd.node_dec_stateless && (not stateless) |
||
50 | then raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id)) |
||
51 | else (nd.node_dec_stateless <- stateless; stateless) |
||
52 | end |
||
53 | | Some stl -> stl) |
||
54 | 04a63d25 | xthirioux | | ImportedNode nd -> |
55 | begin |
||
56 | (if nd.nodei_prototype = Some "C" && not nd.nodei_stateless |
||
57 | then raise (Error (td.top_decl_loc, Stateful_ext_C nd.nodei_id))); |
||
58 | nd.nodei_stateless |
||
59 | end |
||
60 | e135421f | xthirioux | | _ -> true |
61 | |||
62 | let check_prog decls = |
||
63 | List.iter (fun td -> ignore (check_node td)) decls |
||
64 | |||
65 | 04a63d25 | xthirioux | |
66 | let force_prog decls = |
||
67 | let force_node td = |
||
68 | match td.top_decl_desc with |
||
69 | | Node nd -> ( |
||
70 | nd.node_dec_stateless <- false; |
||
71 | nd.node_stateless <- Some false) |
||
72 | | _ -> () |
||
73 | in |
||
74 | List.iter (fun td -> ignore (force_node td)) decls |
||
75 | |||
76 | e135421f | xthirioux | let check_compat_decl decl = |
77 | match decl.top_decl_desc with |
||
78 | | ImportedNode nd -> |
||
79 | let td = Corelang.node_from_name nd.nodei_id in |
||
80 | (match td.top_decl_desc with |
||
81 | | Node nd' -> let stateless = check_node td in |
||
82 | if nd.nodei_stateless && (not stateless) |
||
83 | then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id)) |
||
84 | else nd'.node_dec_stateless <- nd.nodei_stateless |
||
85 | | _ -> assert false) |
||
86 | | Node _ -> assert false |
||
87 | | _ -> () |
||
88 | |||
89 | let check_compat header = |
||
90 | List.iter check_compat_decl header |
||
91 | |||
92 | let pp_error fmt err = |
||
93 | match err with |
||
94 | | Stateful_kwd nd -> |
||
95 | 04a63d25 | xthirioux | Format.fprintf fmt |
96 | "node %s should be stateless but is actually stateful.@." |
||
97 | nd |
||
98 | e135421f | xthirioux | | Stateful_imp nd -> |
99 | 04a63d25 | xthirioux | Format.fprintf fmt |
100 | "node %s is declared stateless but is actually stateful.@." |
||
101 | nd |
||
102 | | Stateful_ext_C nd -> |
||
103 | Format.fprintf fmt |
||
104 | "node %s with declared prototype C cannot be stateful, it has to be a function.@." |
||
105 | nd |
||
106 | e135421f | xthirioux | |
107 | (* Local Variables: *) |
||
108 | (* compile-command:"make -C .." *) |
||
109 | (* End: *) |