Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / stateless.ml @ 3b2bd83d

History | View | Annotate | Download (3.47 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 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
(* compile-command:"make -C .." *)
109
(* End: *)