CristalCaveGem » LustreC

open Lustre_types

let expr_of_vars loc vl = 

  Corelang.expr_of_expr_list loc

    (List.map Corelang.expr_of_vdecl vl)

(* Create a node that checks whether two other nodes have the same output *)

let check_eq nd1 nd2 =

  (* TODO: check that nd1 and nd2 have the same signature *)

  let check_nd = Corelang.copy_node nd1 in (* to keep the type info *)

  let loc = Location.dummy_loc in 

  let ok_var =

    Corelang.mkvar_decl loc ~orig:false

      ("__OK",

       Corelang.mktyp loc Tydec_bool,

       Corelang.mkclock loc Ckdec_any,

         false,

       None,

       None)

  in

  let input_e = expr_of_vars loc check_nd.node_inputs in

  let mk_stmt nd out_vars =

    let call_e = Corelang.mkexpr loc (Expr_appl (nd.node_id, input_e , None)) in

    Eq (

        Corelang.mkeq loc

          (List.map (fun v -> v.var_id) out_vars, call_e)) in

  let copy_vars vl post =

    let f v = { (Corelang.copy_var_decl v) with var_id = v.var_id ^ "_" ^ post } in

    List.map f vl

  in

  let out_vars1 = copy_vars nd1.node_outputs "1" in

  let out_vars2 = copy_vars nd1.node_outputs "2" in

  let call_n1 = mk_stmt nd1 out_vars1 in

  let call_n2 = mk_stmt nd2 out_vars2 in

  let build_eq v1 v2 =

    let pair = expr_of_vars loc [v1;v2] in

    Corelang.mkexpr loc (Expr_appl ("=", pair, None))

  in

  let rec build_ok vl1 vl2 =

    match vl1, vl2 with

    | [v1], [v2] -> build_eq v1 v2

    | hd1::tl1, hd2::tl2 -> 

       let e1 = (build_eq hd1 hd2) in

       let e2 = build_ok tl1 tl2 in

       let e = Corelang.mkexpr loc (Expr_tuple [e1; e2]) in

       Corelang.mkexpr loc (Expr_appl ("&&", e, None))

    | _ -> assert false

  in

  let ok_expr  = build_ok out_vars1 out_vars2 in 

  let ok_stmt = Eq (Corelang.mkeq loc ([ok_var.var_id], ok_expr)) in

  (* Building contract *)

    let ok_e = Corelang.expr_of_vdecl ok_var in

  let contract = {

        consts = [];

        locals = [];

       stmts = [];

        assume = [];

        guarantees = [Corelang.mkeexpr loc ok_e];

       modes = [];

        imports = [];

        spec_loc = loc;              

      }

  in

  let check_nd = { check_nd with

                   node_id = "check_eq_" ^ nd1.node_id ^ "_" ^ nd2.node_id;

                   node_outputs = [ok_var];

                   node_locals = out_vars1 @ out_vars2;

                   node_stmts = [call_n1; call_n2; ok_stmt];

                   node_spec = Some (Contract contract);

                 }

  in

  Global.type_env := Typing.type_node !Global.type_env check_nd loc;

  Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc check_nd;

  check_nd

    (*

                   TODO:

                   construire

                   les variables temporaires pour les outputs de l'un et de l'autre

                   les statements d'appels de nodes

                   ok = and (o1 = o2)

                          et on ajoute le contrat guarantee ok

  in

  check_nd 

     *)

      (* (\* Build the contract: guarentee output = orig_node(input) *\)

   * 

   * let local_outputs = List.map (fun v -> { (Corelang.copy_var_decl v) with var_id = v.var_id ^ "_local" } ) copy_nd.node_outputs in

   * let input_e = expr_of_vars  copy_nd.node_inputs in

   * let call_orig_e =

   *   Corelang.mkexpr loc (Expr_appl (orig_nd.node_id, input_e , None)) in 

   * let build_orig_outputs =

   *   Eq (

   *       Corelang.mkeq loc

   *         (List.map (fun v -> v.var_id) local_outputs, call_orig_e)) in

   * let eq_expr =  Corelang.expr_of_expr_list loc (

   *                    List.map2 (fun v1 v2 ->

   *                        let args = expr_of_vars [v1;v2] in

   *                          Corelang.mkexpr loc (Expr_appl ("=", args, None)))

   *                  copy_nd.node_outputs local_outputs

   *                  )

   * in

   * let contract = {

   *     consts = [];

   *     locals = local_outputs;

   *     stmts = [build_orig_outputs];

   *     assume = [];

   *     guarantees = [Corelang.mkeexpr loc eq_expr];

   *     modes = [];

   *     imports = [];

   *     spec_loc = loc;              

   *    

   *   }

   * in *)