lustrec / src / access.ml @ 0cbf0839
History | View | Annotate | Download (3.92 KB)
1 |
(* ---------------------------------------------------------------------------- |
---|---|
2 |
* SchedMCore - A MultiCore Scheduling Framework |
3 |
* Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
4 |
* |
5 |
* This file is part of Prelude |
6 |
* |
7 |
* Prelude is free software; you can redistribute it and/or |
8 |
* modify it under the terms of the GNU Lesser General Public License |
9 |
* as published by the Free Software Foundation ; either version 2 of |
10 |
* the License, or (at your option) any later version. |
11 |
* |
12 |
* Prelude is distributed in the hope that it will be useful, but |
13 |
* WITHOUT ANY WARRANTY ; without even the implied warranty of |
14 |
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
15 |
* Lesser General Public License for more details. |
16 |
* |
17 |
* You should have received a copy of the GNU Lesser General Public |
18 |
* License along with this program ; if not, write to the Free Software |
19 |
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
20 |
* USA |
21 |
*---------------------------------------------------------------------------- *) |
22 |
|
23 |
(** Access checking module. Done after typing. Generates dimension constraints stored in nodes *) |
24 |
|
25 |
let debug fmt args = () (* Format.eprintf "%a" *) |
26 |
(* Though it shares similarities with the clock calculus module, no code |
27 |
is shared. Simple environments, very limited identifier scoping, no |
28 |
identifier redefinition allowed. *) |
29 |
|
30 |
open Utils |
31 |
(* Yes, opening both modules is dirty as some type names will be |
32 |
overwritten, yet this makes notations far lighter.*) |
33 |
open LustreSpec |
34 |
open Corelang |
35 |
open Types |
36 |
open Format |
37 |
|
38 |
module ConstraintModule = |
39 |
struct (* bool dimension module *) |
40 |
type t = Dimension.dim_expr |
41 |
let equal d1 d2 = Dimension.is_eq_dimension d1 d2 |
42 |
let compare d1 d2 = if equal d1 d2 then 0 else compare d1.Dimension.dim_id d2.Dimension.dim_id |
43 |
let hash n = Hashtbl.hash n |
44 |
end |
45 |
|
46 |
module CSet = Set.Make(ConstraintModule) |
47 |
|
48 |
(** [check_expr env expr] checks expression [expr] and gathers constraints |
49 |
in set [checks]. *) |
50 |
let rec check_expr checks expr = |
51 |
(*Format.eprintf "check_expr %a with type %a@." Printers.pp_expr expr Types.print_ty expr.expr_type;*) |
52 |
let res = |
53 |
match expr.expr_desc with |
54 |
| Expr_const _ |
55 |
| Expr_ident _ -> checks |
56 |
| Expr_array elist -> List.fold_left check_expr checks elist |
57 |
| Expr_access (e1, d) -> check_expr (CSet.add (Dimension.check_access expr.expr_loc (Types.array_type_dimension e1.expr_type) d) checks) e1 |
58 |
(* TODO: check dimensions *) |
59 |
|
60 |
| Expr_power (e1, _) -> check_expr checks e1 |
61 |
|
62 |
| Expr_tuple elist -> List.fold_left check_expr checks elist |
63 |
|
64 |
| Expr_ite (c, t, e) -> List.fold_left check_expr checks [c; t; e] |
65 |
|
66 |
| Expr_appl (_, args, _) -> check_expr checks args |
67 |
|
68 |
| Expr_fby (e1,e2) |
69 |
| Expr_arrow (e1,e2) -> check_expr (check_expr checks e1) e2 |
70 |
| Expr_pre e1 |
71 |
| Expr_when (e1,_,_) -> check_expr checks e1 |
72 |
|
73 |
| Expr_merge (_,hl) -> List.fold_left (fun checks (l, h) -> check_expr checks h) checks hl |
74 |
| _ -> assert false |
75 |
in (*Format.eprintf "typing %B %a at %a = %a@." const Printers.pp_expr expr Location.pp_loc expr.expr_loc Types.print_ty res;*) res |
76 |
|
77 |
let rec check_var_decl_type loc checks ty = |
78 |
if Types.is_array_type ty |
79 |
then |
80 |
check_var_decl_type loc |
81 |
(CSet.add (Dimension.check_bound loc (Types.array_type_dimension ty)) checks) |
82 |
(Types.array_element_type ty) |
83 |
else checks |
84 |
|
85 |
let check_var_decl checks vdecl = |
86 |
check_var_decl_type vdecl.var_loc checks vdecl.var_type |
87 |
|
88 |
(** [check_node nd] checks node [nd]. |
89 |
The resulting constraints are stored in nodes. *) |
90 |
let check_node nd = |
91 |
let checks = CSet.empty in |
92 |
let checks = |
93 |
List.fold_left check_var_decl checks (node_vars nd) in |
94 |
let checks = |
95 |
List.fold_left (fun checks eq -> check_expr checks eq.eq_rhs) checks nd.node_eqs in |
96 |
nd.node_checks <- CSet.elements checks |
97 |
|
98 |
let check_top_decl decl = |
99 |
match decl.top_decl_desc with |
100 |
| Node nd -> check_node nd |
101 |
| _ -> () |
102 |
|
103 |
let check_prog decls = |
104 |
List.iter check_top_decl decls |
105 |
|
106 |
|
107 |
(* Local Variables: *) |
108 |
(* compile-command:"make -C .." *) |
109 |
(* End: *) |