Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / stateless.ml @ 4f26dcf5

History | View | Annotate | Download (3.61 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 8446bf03 ploc
open Lustre_types
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 333e3a25 ploc
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 e135421f xthirioux
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 04a63d25 xthirioux
  | 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 e135421f xthirioux
  | _ -> true
63
64
let check_prog decls =
65
  List.iter (fun td -> ignore (check_node td)) decls
66
67 04a63d25 xthirioux
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 e135421f xthirioux
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 04a63d25 xthirioux
     Format.fprintf fmt
98
       "node %s should be stateless but is actually stateful.@."
99
       nd
100 e135421f xthirioux
  | Stateful_imp nd ->
101 04a63d25 xthirioux
     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 e135421f xthirioux
109
(* Local Variables: *)
110
(* compile-command:"make -C .." *)
111
(* End: *)