lustrec / src / stateless.ml @ 01c7d5e1
History | View | Annotate | Download (3.2 KB)
1 |
(* ---------------------------------------------------------------------------- |
---|---|
2 |
* SchedMCore - A MultiCore Scheduling Framework |
3 |
* Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
4 |
* |
5 |
* This file is part of Prelude |
6 |
* |
7 |
* Prelude is free software; you can redistribute it and/or |
8 |
* modify it under the terms of the GNU Lesser General Public License |
9 |
* as published by the Free Software Foundation ; either version 2 of |
10 |
* the License, or (at your option) any later version. |
11 |
* |
12 |
* Prelude is distributed in the hope that it will be useful, but |
13 |
* WITHOUT ANY WARRANTY ; without even the implied warranty of |
14 |
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
15 |
* Lesser General Public License for more details. |
16 |
* |
17 |
* You should have received a copy of the GNU Lesser General Public |
18 |
* License along with this program ; if not, write to the Free Software |
19 |
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
20 |
* USA |
21 |
*---------------------------------------------------------------------------- *) |
22 |
open LustreSpec |
23 |
open Corelang |
24 |
|
25 |
type error = |
26 |
| Stateful_kwd of ident |
27 |
| Stateful_imp of ident |
28 |
|
29 |
exception Error of Location.t * error |
30 |
|
31 |
let rec check_expr expr = |
32 |
match expr.expr_desc with |
33 |
| Expr_const _ |
34 |
| Expr_ident _ -> true |
35 |
| Expr_tuple el |
36 |
| Expr_array el -> List.for_all check_expr el |
37 |
| Expr_access (e1, _) |
38 |
| Expr_power (e1, _) -> check_expr e1 |
39 |
| Expr_ite (c, t, e) -> check_expr c && check_expr t && check_expr e |
40 |
| Expr_arrow _ |
41 |
| Expr_fby _ |
42 |
| Expr_pre _ -> false |
43 |
| Expr_when (e', i, l)-> check_expr e' |
44 |
| Expr_merge (i, hl) -> List.for_all (fun (t, h) -> check_expr h) hl |
45 |
| Expr_appl (i, e', i') -> |
46 |
check_expr e' && |
47 |
(Basic_library.is_internal_fun i || check_node (node_from_name i)) |
48 |
and compute_node nd = |
49 |
List.for_all (fun eq -> check_expr eq.eq_rhs) nd.node_eqs |
50 |
and check_node td = |
51 |
match td.top_decl_desc with |
52 |
| Node nd -> ( |
53 |
match nd.node_stateless with |
54 |
| None -> |
55 |
begin |
56 |
let stateless = compute_node nd in |
57 |
nd.node_stateless <- Some stateless; |
58 |
if nd.node_dec_stateless && (not stateless) |
59 |
then raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id)) |
60 |
else (nd.node_dec_stateless <- stateless; stateless) |
61 |
end |
62 |
| Some stl -> stl) |
63 |
| ImportedNode nd -> nd.nodei_stateless |
64 |
| _ -> true |
65 |
|
66 |
let check_prog decls = |
67 |
List.iter (fun td -> ignore (check_node td)) decls |
68 |
|
69 |
let check_compat_decl decl = |
70 |
match decl.top_decl_desc with |
71 |
| ImportedNode nd -> |
72 |
let td = Corelang.node_from_name nd.nodei_id in |
73 |
(match td.top_decl_desc with |
74 |
| Node nd' -> let stateless = check_node td in |
75 |
if nd.nodei_stateless && (not stateless) |
76 |
then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id)) |
77 |
else nd'.node_dec_stateless <- nd.nodei_stateless |
78 |
| _ -> assert false) |
79 |
| Node _ -> assert false |
80 |
| _ -> () |
81 |
|
82 |
let check_compat header = |
83 |
List.iter check_compat_decl header |
84 |
|
85 |
let pp_error fmt err = |
86 |
match err with |
87 |
| Stateful_kwd nd -> |
88 |
Format.fprintf fmt |
89 |
"node %s should be stateless but is actually stateful.@." |
90 |
nd |
91 |
| Stateful_imp nd -> |
92 |
Format.fprintf fmt |
93 |
"node %s is declared stateless but is actually stateful.@." |
94 |
nd |
95 |
|
96 |
(* Local Variables: *) |
97 |
(* compile-command:"make -C .." *) |
98 |
(* End: *) |