Project

General

Profile

Revision f4cba4b8 src/checks/stateless.ml

View differences:

src/checks/stateless.ml
76 76
  List.iter (fun td -> ignore (force_node td)) decls
77 77

  
78 78
let check_compat_decl decl =
79
 match decl.top_decl_desc with
80
 | ImportedNode nd ->
81
   let td = Corelang.node_from_name nd.nodei_id in
82
   (match td.top_decl_desc with
83
   | Node nd' -> let stateless = check_node td in
84
		 if nd.nodei_stateless && (not stateless)
85
		 then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id))
86
		 else nd'.node_dec_stateless <- nd.nodei_stateless
87
   | _        -> assert false)
88
 | Node _          -> assert false
89
 | _               -> ()
79
  match decl.top_decl_desc with
80
  | ImportedNode nd -> (* A node declared in the header (lusi) shall
81
                          be locally defined with compatible stateless
82
                          flag *)
83
     begin
84
       let td = Corelang.node_from_name nd.nodei_id in
85
       (match td.top_decl_desc with
86
        | Node nd' -> let stateless = check_node td in
87
		      if nd.nodei_stateless && (not stateless)
88
		      then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id))
89
		      else nd'.node_dec_stateless <- nd.nodei_stateless
90
        | _        -> assert false)
91
     end
92
  | Node nd -> (
93
     match nd.node_spec with
94
       Some (Contract _) -> (* A contract element in a header does not
95
                               need to be provided in the associed lus
96
                               file *)
97
        ()
98
     | _ -> assert false)
99
             
100
  | _               -> ()
90 101

  
91 102
let check_compat header =
92 103
  List.iter check_compat_decl header

Also available in: Unified diff