Revision ca7ff3f7
Added by LĂ©lio Brun over 1 year ago
src/checks/access.ml  

9  9 
(* *) 
10  10 
(********************************************************************) 
11  11  
12 
(** Access checking module. Done after typing. Generates dimension constraints stored in nodes *) 

12 
(** Access checking module. Done after typing. Generates dimension constraints 

13 
stored in nodes *) 

13  14  
14 
let debug _fmt _args = () (* Format.eprintf "%a" *) 

15 
(* Though it shares similarities with the clock calculus module, no code 

16 
is shared. Simple environments, very limited identifier scoping, no 

17 
identifier redefinition allowed. *) 

15 
let debug _fmt _args = () 

16  
17 
(* Format.eprintf "%a" *) 

18 
(* Though it shares similarities with the clock calculus module, no code is 

19 
shared. Simple environments, very limited identifier scoping, no identifier 

20 
redefinition allowed. *) 

18  21  
19  22 
open Utils 
20 
(* Yes, opening both modules is dirty as some type names will be 

21 
overwritten, yet this makes notations far lighter.*) 

23  
24 
(* Yes, opening both modules is dirty as some type names will be overwritten, 

25 
yet this makes notations far lighter.*) 

22  26 
open Lustre_types 
23  27 
open Corelang 
24  28  
25 
module ConstraintModule = 

26 
struct (* bool dimension module *)


29 
module ConstraintModule = struct


30 
(* bool dimension module *)


27  31 
type t = Dimension.dim_expr 
32  
28  33 
let equal d1 d2 = Dimension.is_eq_dimension d1 d2 
29 
let compare d1 d2 = if equal d1 d2 then 0 else compare d1.Dimension.dim_id d2.Dimension.dim_id 

34  
35 
let compare d1 d2 = 

36 
if equal d1 d2 then 0 else compare d1.Dimension.dim_id d2.Dimension.dim_id 

37  
30  38 
let hash n = Hashtbl.hash n 
31  39 
end 
32  40  
33 
module CSet = Set.Make(ConstraintModule) 

41 
module CSet = Set.Make (ConstraintModule)


34  42  
35 
(** [check_expr env expr] checks expression [expr] and gathers constraints 

36 
in set [checks]. *)


43 
(** [check_expr env expr] checks expression [expr] and gathers constraints in


44 
set [checks]. *) 

37  45 
let rec check_expr checks expr = 
38 
(*Format.eprintf "check_expr %a with type %a@." Printers.pp_expr expr Types.print_ty expr.expr_type;*) 

39 
let res = 

40 
match expr.expr_desc with 

41 
 Expr_const _ 

42 
 Expr_ident _ > checks 

43 
 Expr_array elist > List.fold_left check_expr checks elist 

44 
 Expr_access (e1, d) > check_expr (CSet.add (Dimension.check_access expr.expr_loc (Types.array_type_dimension e1.expr_type) d) checks) e1 

46 
(*Format.eprintf "check_expr %a with type %a@." Printers.pp_expr expr 

47 
Types.print_ty expr.expr_type;*) 

48 
let res = 

49 
match expr.expr_desc with 

50 
 Expr_const _  Expr_ident _ > 

51 
checks 

52 
 Expr_array elist > 

53 
List.fold_left check_expr checks elist 

54 
 Expr_access (e1, d) > 

55 
check_expr 

56 
(CSet.add 

57 
(Dimension.check_access expr.expr_loc 

58 
(Types.array_type_dimension e1.expr_type) 

59 
d) 

60 
checks) 

61 
e1 

45  62 
(* TODO: check dimensions *) 
46 


47 
 Expr_power (e1, _) > check_expr checks e1 

48 


49 
 Expr_tuple elist > List.fold_left check_expr checks elist 

50  
51 
 Expr_ite (c, t, e) > List.fold_left check_expr checks [c; t; e] 

52 


53 
 Expr_appl (_, args, _) > check_expr checks args 

54 


55 
 Expr_fby (e1,e2) 

56 
 Expr_arrow (e1,e2) > check_expr (check_expr checks e1) e2 

57 
 Expr_pre e1 

58 
 Expr_when (e1,_,_) > check_expr checks e1 

59 


60 
 Expr_merge (_,hl) > List.fold_left (fun checks (_, h) > check_expr checks h) checks hl 

61 
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 

63 
 Expr_power (e1, _) > 

64 
check_expr checks e1 

65 
 Expr_tuple elist > 

66 
List.fold_left check_expr checks elist 

67 
 Expr_ite (c, t, e) > 

68 
List.fold_left check_expr checks [ c; t; e ] 

69 
 Expr_appl (_, args, _) > 

70 
check_expr checks args 

71 
 Expr_fby (e1, e2)  Expr_arrow (e1, e2) > 

72 
check_expr (check_expr checks e1) e2 

73 
 Expr_pre e1  Expr_when (e1, _, _) > 

74 
check_expr checks e1 

75 
 Expr_merge (_, hl) > 

76 
List.fold_left (fun checks (_, h) > check_expr checks h) checks hl 

77 
in 

78 
(*Format.eprintf "typing %B %a at %a = %a@." const Printers.pp_expr expr 

79 
Location.pp_loc expr.expr_loc Types.print_ty res;*) 

80 
res 

62  81  
63  82 
let rec check_var_decl_type loc checks ty = 
64 
if Types.is_array_type ty 

65 
then 

83 
if Types.is_array_type ty then 

66  84 
check_var_decl_type loc 
67 
(CSet.add (Dimension.check_bound loc (Types.array_type_dimension ty)) checks) 

68 
(Types.array_element_type ty) 

85 
(CSet.add 

86 
(Dimension.check_bound loc (Types.array_type_dimension ty)) 

87 
checks) 

88 
(Types.array_element_type ty) 

69  89 
else checks 
70  90  
71  91 
let check_var_decl checks vdecl = 
72  92 
check_var_decl_type vdecl.var_loc checks vdecl.var_type 
73  93  
74 
(** [check_node nd] checks node [nd]. 

75 
The resulting constraints are stored in nodes. *)


94 
(** [check_node nd] checks node [nd]. The resulting constraints are stored in


95 
nodes. *) 

76  96 
let check_node nd = 
77  97 
let checks = CSet.empty in 
78 
let checks = 

79 
List.fold_left check_var_decl checks (get_node_vars nd) in 

98 
let checks = List.fold_left check_var_decl checks (get_node_vars nd) in 

80  99 
let checks = 
81  100 
let eqs, auts = get_node_eqs nd in 
82 
assert (auts = []); (* Not checking automata yet . *) 

83 
List.fold_left (fun checks eq > check_expr checks eq.eq_rhs) checks eqs in 

101 
assert (auts = []); 

102 
(* Not checking automata yet . *) 

103 
List.fold_left (fun checks eq > check_expr checks eq.eq_rhs) checks eqs 

104 
in 

84  105 
nd.node_checks < CSet.elements checks 
85  106  
86  107 
let check_top_decl decl = 
87 
match decl.top_decl_desc with 

88 
 Node nd > check_node nd 

89 
 _ > () 

90  
91 
let check_prog decls = 

92 
List.iter check_top_decl decls 

108 
match decl.top_decl_desc with Node nd > check_node nd  _ > () 

93  109  
110 
let check_prog decls = List.iter check_top_decl decls 

94  111  
95  112 
(* Local Variables: *) 
96  113 
(* compilecommand:"make C .." *) 
Also available in: Unified diff
reformatting