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 LustreSpec

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

(* compilecommand:"make C .." *)

111

(* End: *)
