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 =

40

List.for_all (fun eq > check_expr eq.eq_rhs) (get_node_eqs nd)

41

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

 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

 _ > true

61


62

let check_prog decls =

63

List.iter (fun td > ignore (check_node td)) decls

64


65


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

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

Format.fprintf fmt

96

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

97

nd

98

 Stateful_imp nd >

99

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


107

(* Local Variables: *)

108

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

109

(* End: *)
