Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

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
(* compile-command:"make -C .." *)

Also available in: Unified diff