CristalCaveGem » LustreC

  let checks =

    List.fold_left check_var_decl checks (get_node_vars nd) in

  let checks =

  nd.node_checks <- CSet.elements checks

let check_top_decl decl =

open LustreSpec

open Corelang

let mkbool loc b =

 mkexpr loc (Expr_const (const_of_bool b))

let add_branch (loc, expr, restart, st) cont =

 mkexpr loc (Expr_ite (expr, mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st]), cont))

 {hand_state = st;

  hand_unless = unless;

  hand_until = until;

  hand_locals = locals;

  hand_asserts = asserts;

  hand_annots = annots;

  hand_loc = loc}

   aut_handlers = handlers;

   aut_loc = loc}

let node_of_handler node aut_id handler =

  {

    node_id = Format.sprintf "%s_%s_handler" aut_id handler.hand_state;

    node_type = Types.new_var ();

    node_clock = Clocks.new_var true;

    node_locals = handler.hand_locals;

    node_gencalls = [];

    node_checks = [];

    node_asserts = handler.hand_asserts; 

    node_dec_stateless = false;

    node_stateless = None;

    node_spec = None;

  let arg = mkexpr loc (Expr_tuple (List.map (fun v -> mkident loc v.var_id) node.node_inputs)) in

  mkexpr loc (Expr_when (mkexpr loc (Expr_appl (node.node_id, arg, Some (restart, tag_true))), state, tag))

  let outputs = (snd (List.hd hnodes)).node_outputs in

  let assign_handlers = List.map (fun (hs, n) -> (hs, expr_of_handler loc actual_r actual_s n hs)) hnodes in

  let assign_expr = mkexpr loc (Expr_merge (actual_s, assign_handlers)) in

  { tydef_id = tname;

    tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers)

  }

let expand_automata top_node aut =

  let node = node_of_top top_node in

  let fby_until_expr = mkfby aut.aut_loc (init aut.aut_loc tag_false initial) until_expr in

  let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in

  let hnodes = List.map (fun h -> (h.hand_state, node_of_handler node aut.aut_id h)) aut.aut_handlers in

  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in

  let tydec_const id = { ty_dec_desc = Tydec_const id; ty_dec_loc = aut.aut_loc } in

  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in

                 mkvar_decl aut.aut_loc (actual_r  , tydec_bool, ckdec_any, false);

                 mkvar_decl aut.aut_loc (incoming_s, tydec_const typedef.tydef_id, ckdec_any, false);

                 mkvar_decl aut.aut_loc (actual_s  , tydec_const typedef.tydef_id, ckdec_any, false)] in

  (mktop_decl aut.aut_loc owner false (TypeDef typedef)) ::

  { top_node with top_decl_desc = Node node' } ::

  (List.map2 (fun h (hs, n) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes)

  match top_decl.top_decl_desc with

  | _ -> [top_decl]

(*

let extract_automata top_decls =

(* Generation of a non-clashing name for the self memory variable (for step and reset functions) *)

let mk_self m =

(* Generation of a non-clashing name for the instance variable of static allocation macro *)

let mk_instance m =

(* Generation of a non-clashing name for the attribute variable of static allocation macro *)

let mk_attribute m =

let mk_call_var_decl loc id =

  { var_id = id;

  else

    begin

      let static_inputs = List.filter (fun v -> v.var_dec_const) inode.nodei_inputs in

      fprintf fmt "extern %a;@.@."

	(print_reset_prototype self) (inode.nodei_id, static_inputs);

  match_mem eq.eq_lhs eq.eq_rhs mems

let node_memory_variables nd =

let node_input_variables nd =

 List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty nd.node_inputs

    let first = List.hd eq.eq_lhs in

    List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs

  )

  eq_equiv

(* Create a tuple of right dimension, according to [expr] type, *)

  instance_var_cpt := 0;

  let g = new_graph (), new_graph () in

  (* Basic dependencies *)

  g

end

	| Node nd ->

	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)

	  let accu = add_vertices [nd.node_id] accu in

	   (*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)

	  add_edges [nd.node_id] deps accu

	| _ -> assert false (* should not happen *)

	match td.top_decl_desc with 

	| Node nd ->

	  let prednode n = is_generic_node (Hashtbl.find node_table n) in

	| _ -> ()

      ) prog

  module Cycles = Graph.Components.Make (IdentDepGraph)

  let mk_copy_var n id =

  let mk_copy_eq n var =

    let var_decl = get_node_var var n in

   - a modified acyclic version of [g]

*)

  let break_cycles node mems g =

    let rec break vdecls mem_eqs g =

      let scc_l = Cycles.scc_list g in

      let wrong = List.filter (wrong_partition g) scc_l in

  begin

    merge_with g_non_mems g_mems';

    add_external_dependency outputs mems g_non_mems;

    g_non_mems

  end

  let new_env = clock_var_decl_list env false nd.node_inputs in

  let new_env = clock_var_decl_list new_env true nd.node_outputs in

  let new_env = clock_var_decl_list new_env true nd.node_locals in

  let ck_ins = clock_of_vlist nd.node_inputs in

  let ck_outs = clock_of_vlist nd.node_outputs in

  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in

    var_clock = Clocks.new_var false;

    var_loc = c.const_loc }

  let rec new_name name cpt =

    then new_name (sprintf "_%s_%i" id cpt) (cpt+1)

    else name

  in new_name id 1

let get_node_var id node = get_var id (get_node_vars node)

let get_node_eq id node =

let get_nodes prog = 

  List.fold_left (

	  rename_expr f_node f_var f_const expr})

    nd.node_asserts

  in

  let spec = 

    Utils.option_map 

      (fun s -> rename_node_annot f_node f_var f_const s) 

    node_gencalls = gen_calls;

    node_checks = node_checks;

    node_asserts = node_asserts;

    node_dec_stateless = nd.node_dec_stateless;

    node_stateless = nd.node_stateless;

    node_spec = spec;

and get_eq_calls nodes eq =

  get_expr_calls nodes eq.eq_rhs

and get_node_calls nodes node =

let rec get_expr_vars vars e =

  get_expr_desc_vars vars e.expr_desc

and eq_has_arrows eq =

  expr_has_arrows eq.eq_rhs

and node_has_arrows node =

(* Local Variables: *)

(* compile-command:"make -C .." *)

val mkassert: Location.t -> expr -> assert_t

val mktop_decl: Location.t -> ident -> bool -> top_decl_desc -> top_decl

val mkpredef_call: Location.t -> ident -> expr list -> expr

val node_table : (ident, top_decl) Hashtbl.t

val get_node_vars: node_desc -> var_decl list

val get_node_var: ident -> node_desc -> var_decl

val get_node_eq: ident -> node_desc -> eq

val get_node_interface: node_desc -> imported_node_desc

      node.node_id uid v;

    Format.flush_str_formatter ())

  in

  in

  let rename_var v = { v with var_id = rename v.var_id } in

  let inputs' = List.map rename_var node.node_inputs in

	inline_expr eq.eq_rhs locals nodes 

      in

      locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts

  in

  { nd with

    node_locals = new_locals;

    node_asserts = asserts;

  }

  (* Building main node *)

  let main_node = {

    node_id = "check";

    node_type = Types.new_var ();

    node_gencalls = [];

    node_checks = [];

    node_asserts = [];

    node_dec_stateless = false;

    node_stateless = None;

    node_spec = Some 

    {

      assert_expr: expr;

      assert_loc: Location.t;

  {aut_id : ident;

   aut_handlers: handler_desc list;

   aut_loc: Location.t}

   hand_unless: (Location.t * expr * bool * ident) list;

   hand_until: (Location.t * expr * bool * ident) list;

   hand_locals: var_decl list;

   hand_asserts: assert_t list;

   hand_annots: expr_annot list;

   hand_loc: Location.t}

type node_desc =

    {node_id: ident;

     mutable node_type: Types.type_expr;

     mutable node_gencalls: expr list;

     mutable node_checks: Dimension.dim_expr list;

     node_asserts: assert_t list; 

     mutable node_dec_stateless: bool;

     mutable node_stateless: bool option;

     node_spec: node_annot option;

    node_gencalls = [];

    node_checks = [];

    node_asserts = [];

    node_dec_stateless = false;

    node_stateless = Some false;

    node_spec = None;

(*  Format.eprintf "%s schedule: %a@."

		 nd.node_id

		 (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch;*)

  let eqs_rev, remainder =

    List.fold_left 

      (fun (accu, node_eqs_remainder) vl -> 

    if List.length remainder > 0 then (

      Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?"

		     Printers.pp_node_eqs remainder

      assert false);

    List.rev eqs_rev

  end

    List.for_all ((!=) v) inputs_outputs in

  let orig_vars = inputs_outputs@node.node_locals in

  let defs, vars = 

  (* Normalize the asserts *)

  let vars, assert_defs, asserts = 

    List.fold_left (

  let node =

  { node with 

    node_locals = new_locals; 

    node_asserts = asserts;

    node_annot = norm_traceability::node.node_annot;

  }

  { eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs }

let node_unfold_consts consts node = 

let prog_unfold_consts prog =

  let consts = List.map const_of_top (get_consts prog) in

  { eq with eq_rhs = expr_distribute_when eq.eq_rhs }

let node_distribute_when node =

let prog_distribute_when prog =

    List.map (

top_decl:

| CONST cdecl_list { List.rev ($2 false) }

     let nd = mktop_decl false (Node

				  {node_id = $3;

				   node_type = Types.new_var ();

				   node_gencalls = [];

				   node_checks = [];

				   node_asserts = asserts; 

				   node_dec_stateless = $2;

				   node_stateless = None;

				   node_spec = $1;

field_list:                           { [] }

| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }

  { [], [], [] }

automaton:

 AUTOMATON type_ident handler_list { (Automata.mkautomata (get_loc ()) $2 $3); failwith "not implemented" }

| handler handler_list { $1::$2 }

handler:

unless_list:

    { [] }

    pp_eq_lhs eq.eq_lhs

    pp_expr eq.eq_rhs

let rec pp_var_struct_type_field fmt (label, tdesc) =

  fprintf fmt "%a : %a;" pp_print_string label pp_var_type_dec_desc tdesc

      checks

  ) nd.node_checks

  (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot

  pp_asserts nd.node_asserts

(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)

    check_expr e' &&

      (Basic_library.is_internal_fun i || check_node (node_from_name i))

and compute_node nd =

and check_node td =

  match td.top_decl_desc with 

  | Node nd         -> (

      (fun uvs v -> IMap.add v.var_id () uvs)

      IMap.empty vd_env_ol in

  let undefined_vars =

  in

  (* Typing asserts *)

  List.iter (fun assert_ ->