Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / stateless.ml @ 1eda3e78

History | View | Annotate | Download (2.88 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

    
19
exception Error of Location.t * error
20

    
21
let rec check_expr expr =
22
  match expr.expr_desc with
23
  | Expr_const _ 
24
  | Expr_ident _ -> true
25
  | Expr_tuple el
26
  | Expr_array el -> List.for_all check_expr el
27
  | Expr_access (e1, _)
28
  | Expr_power (e1, _) -> check_expr e1
29
  | Expr_ite (c, t, e) -> check_expr c && check_expr t && check_expr e
30
  | Expr_arrow _
31
  | Expr_fby _
32
  | Expr_pre _ -> false
33
  | Expr_when (e', i, l)-> check_expr e'
34
  | Expr_merge (i, hl) -> List.for_all (fun (t, h) -> check_expr h) hl 
35
  | Expr_appl (i, e', i') ->
36
    check_expr e' &&
37
      (Basic_library.is_internal_fun i || check_node (node_from_name i))
38
and compute_node nd =
39
 List.for_all (fun eq -> check_expr eq.eq_rhs) (get_node_eqs nd)
40
and check_node td =
41
  match td.top_decl_desc with 
42
  | Node nd         -> (
43
    match nd.node_stateless with
44
    | None     -> 
45
      begin
46
	let stateless = compute_node nd in
47
	nd.node_stateless <- Some stateless;
48
	if nd.node_dec_stateless && (not stateless)
49
	then raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id))
50
	else (nd.node_dec_stateless <- stateless; stateless)
51
      end
52
    | Some stl -> stl)
53
  | ImportedNode nd -> nd.nodei_stateless
54
  | _ -> true
55

    
56
let check_prog decls =
57
  List.iter (fun td -> ignore (check_node td)) decls
58

    
59
let check_compat_decl decl =
60
 match decl.top_decl_desc with
61
 | ImportedNode nd ->
62
   let td = Corelang.node_from_name nd.nodei_id in
63
   (match td.top_decl_desc with
64
   | Node nd' -> let stateless = check_node td in
65
		 if nd.nodei_stateless && (not stateless)
66
		 then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id))
67
		 else nd'.node_dec_stateless <- nd.nodei_stateless
68
   | _        -> assert false)
69
 | Node _          -> assert false
70
 | _               -> ()
71

    
72
let check_compat header =
73
  List.iter check_compat_decl header
74

    
75
let pp_error fmt err =
76
  match err with
77
  | Stateful_kwd nd ->
78
    Format.fprintf fmt
79
      "node %s should be stateless but is actually stateful.@."
80
      nd
81
  | Stateful_imp nd ->
82
    Format.fprintf fmt
83
      "node %s is declared stateless but is actually stateful.@."
84
      nd
85

    
86
(* Local Variables: *)
87
(* compile-command:"make -C .." *)
88
(* End: *)