CristalCaveGem » LustreC

| Stateful_kwd   of ident

| Stateful_imp   of ident

| Stateful_ext_C of ident

  | Expr_const _ 

    | Expr_ident _ -> true

  | Expr_tuple el

    | Expr_array el -> List.for_all check_expr el

  | Expr_access (e1, _)

    | Expr_power (e1, _) -> check_expr e1

  | Expr_ite (c, t, e) -> check_expr c && check_expr t && check_expr e

  | Expr_arrow _

    | Expr_fby _

    | Expr_pre _ -> false

  | Expr_when (e', _, _)-> check_expr e'

  | Expr_merge (_, hl) -> List.for_all (fun (_, h) -> check_expr h) hl

     let reset_opt = (match i' with None -> true | Some e'' -> check_expr e'') in

     let stateless_node =

       (Basic_library.is_stateless_fun i || (

          try

            check_node (node_from_name i)

          with Not_found ->

            let loc = expr.expr_loc in

            Error.pp_error loc (fun fmt -> Format.fprintf fmt "Unable to find node %s in expression %a" i Printers.pp_expr expr);

            raise (Error.Error (loc, Error.Unbound_symbol i))

       ))

     in

     (* Warning message when trying to reset a stateless node *)

     if stateless_node && not reset_opt then

       Error.pp_warning expr.expr_loc (fun fmt -> Format.fprintf fmt "Trying to reset call the stateless node or op %s" i)

     ;

     check_expr e' && reset_opt && stateless_node

and compute_node nd = (* returns true iff the node is stateless.*)

  aut = [] && (* A node containinig an automaton will be stateful *)

    List.for_all (fun eq -> check_expr eq.eq_rhs) eqs

  match td.top_decl_desc with 

  | Node nd         -> (

    | None     -> 

       begin

	 let stateless = compute_node nd in

	 nd.node_stateless <- Some stateless;

	 if nd.node_dec_stateless && (not stateless)

	 then raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id))

	 else (nd.node_dec_stateless <- stateless; stateless)

       end

    | Some stl -> stl)

     begin

       (if nd.nodei_prototype = Some "C" && not nd.nodei_stateless

	then raise (Error (td.top_decl_loc, Stateful_ext_C nd.nodei_id)));

       nd.nodei_stateless

     end

  | _ -> true

let check_prog decls =

  List.iter (fun td -> ignore (check_node td)) decls

    match td.top_decl_desc with 

    | Node nd         -> (

      nd.node_stateless <- Some false)

    | _ -> ()

  | ImportedNode nd -> (* A node declared in the header (lusi) shall

                          be locally defined with compatible stateless

                          flag *)

     begin

       let td = Corelang.node_from_name nd.nodei_id in

       (match td.top_decl_desc with

        | Node nd' -> let stateless = check_node td in

		      if nd.nodei_stateless && (not stateless)

		      then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id))

		      else nd'.node_dec_stateless <- nd.nodei_stateless

        | _        -> assert false)

     end

     match nd.node_spec with

       Some (Contract _) -> (* A contract element in a header does not

                               need to be provided in the associed lus

                               file *)

        ()

     | _ -> assert false)

  | _               -> ()

let check_compat header =

  List.iter check_compat_decl header

     Format.fprintf fmt

       "node %s should be stateless but is actually stateful.@."

       nd

     Format.fprintf fmt

       "node %s is declared stateless but is actually stateful.@."

       nd

     Format.fprintf fmt

       "node %s with declared prototype C cannot be stateful, it has to be a function.@."

       nd