## lustrec / src / stateless.ml @ 3cd040e3

History | View | Annotate | Download (3.61 KB)

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 Lustre_types |

13 |
open Corelang |

14 | |

15 |
type error = |

16 |
| Stateful_kwd of ident |

17 |
| Stateful_imp of ident |

18 |
| Stateful_ext_C of ident |

19 | |

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 |
(Basic_library.is_stateless_fun i || check_node (node_from_name i)) |

39 |
and compute_node nd = (* returns true iff the node is stateless.*) |

40 |
let eqs, aut = get_node_eqs nd in |

41 |
aut = [] && (* A node containinig an automaton will be stateful *) |

42 |
List.for_all (fun eq -> check_expr eq.eq_rhs) eqs |

43 |
and check_node td = |

44 |
match td.top_decl_desc with |

45 |
| Node nd -> ( |

46 |
match nd.node_stateless with |

47 |
| None -> |

48 |
begin |

49 |
let stateless = compute_node nd in |

50 |
nd.node_stateless <- Some stateless; |

51 |
if nd.node_dec_stateless && (not stateless) |

52 |
then raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id)) |

53 |
else (nd.node_dec_stateless <- stateless; stateless) |

54 |
end |

55 |
| Some stl -> stl) |

56 |
| ImportedNode nd -> |

57 |
begin |

58 |
(if nd.nodei_prototype = Some "C" && not nd.nodei_stateless |

59 |
then raise (Error (td.top_decl_loc, Stateful_ext_C nd.nodei_id))); |

60 |
nd.nodei_stateless |

61 |
end |

62 |
| _ -> true |

63 | |

64 |
let check_prog decls = |

65 |
List.iter (fun td -> ignore (check_node td)) decls |

66 | |

67 | |

68 |
let force_prog decls = |

69 |
let force_node td = |

70 |
match td.top_decl_desc with |

71 |
| Node nd -> ( |

72 |
nd.node_dec_stateless <- false; |

73 |
nd.node_stateless <- Some false) |

74 |
| _ -> () |

75 |
in |

76 |
List.iter (fun td -> ignore (force_node td)) decls |

77 | |

78 |
let check_compat_decl decl = |

79 |
match decl.top_decl_desc with |

80 |
| ImportedNode nd -> |

81 |
let td = Corelang.node_from_name nd.nodei_id in |

82 |
(match td.top_decl_desc with |

83 |
| Node nd' -> let stateless = check_node td in |

84 |
if nd.nodei_stateless && (not stateless) |

85 |
then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id)) |

86 |
else nd'.node_dec_stateless <- nd.nodei_stateless |

87 |
| _ -> assert false) |

88 |
| Node _ -> assert false |

89 |
| _ -> () |

90 | |

91 |
let check_compat header = |

92 |
List.iter check_compat_decl header |

93 | |

94 |
let pp_error fmt err = |

95 |
match err with |

96 |
| Stateful_kwd nd -> |

97 |
Format.fprintf fmt |

98 |
"node %s should be stateless but is actually stateful.@." |

99 |
nd |

100 |
| Stateful_imp nd -> |

101 |
Format.fprintf fmt |

102 |
"node %s is declared stateless but is actually stateful.@." |

103 |
nd |

104 |
| Stateful_ext_C nd -> |

105 |
Format.fprintf fmt |

106 |
"node %s with declared prototype C cannot be stateful, it has to be a function.@." |

107 |
nd |

108 | |

109 |
(* Local Variables: *) |

110 |
(* compile-command:"make -C .." *) |

111 |
(* End: *) |