Project

General

Profile

Revision b8dfc744

View differences:

src/lustre_utils.ml
1 1
open Lustre_types
2 2

  
3
let expr_of_vars loc vl = 
4
  Corelang.expr_of_expr_list loc
5
    (List.map Corelang.expr_of_vdecl vl)
6
   
7
   
3 8
(* Create a node that checks whether two other nodes have the same output *)
4 9

  
5 10
let check_eq nd1 nd2 =
11
  (* TODO: check that nd1 and nd2 have the same signature *)
6 12
  let check_nd = Corelang.copy_node nd1 in (* to keep the type info *)
7 13
  let loc = Location.dummy_loc in 
8 14
  let ok_var =
......
13 19
         false,
14 20
       None,
15 21
       None)
16
  in 
22
  in
23
  let input_e = expr_of_vars loc check_nd.node_inputs in
24
  let mk_stmt nd out_vars =
25
    let call_e = Corelang.mkexpr loc (Expr_appl (nd.node_id, input_e , None)) in
26
    Eq (
27
        Corelang.mkeq loc
28
          (List.map (fun v -> v.var_id) out_vars, call_e)) in
29
  let copy_vars vl post =
30
    let f v = { (Corelang.copy_var_decl v) with var_id = v.var_id ^ "_" ^ post } in
31
    List.map f vl
32
  in
33
  let out_vars1 = copy_vars nd1.node_outputs "1" in
34
  let out_vars2 = copy_vars nd1.node_outputs "2" in
35
  let call_n1 = mk_stmt nd1 out_vars1 in
36
  let call_n2 = mk_stmt nd2 out_vars2 in
37
  let build_eq v1 v2 =
38
    let pair = expr_of_vars loc [v1;v2] in
39
    Corelang.mkexpr loc (Expr_appl ("=", pair, None))
40
  in
41
  let rec build_ok vl1 vl2 =
42
    match vl1, vl2 with
43
    | [v1], [v2] -> build_eq v1 v2
44
    | hd1::tl1, hd2::tl2 -> 
45
       let e1 = (build_eq hd1 hd2) in
46
       let e2 = build_ok tl1 tl2 in
47
       let e = Corelang.mkexpr loc (Expr_tuple [e1; e2]) in
48
       Corelang.mkexpr loc (Expr_appl ("&&", e, None))
49
    | _ -> assert false
50
  in
51
  let ok_expr  = build_ok out_vars1 out_vars2 in 
52
  let ok_stmt = Eq (Corelang.mkeq loc ([ok_var.var_id], ok_expr)) in
53

  
54
  (* Building contract *)
55
    let ok_e = Corelang.expr_of_vdecl ok_var in
56
  let contract = {
57
        consts = [];
58
        locals = [];
59
       stmts = [];
60
        assume = [];
61
        guarantees = [Corelang.mkeexpr loc ok_e];
62
       modes = [];
63
        imports = [];
64
        spec_loc = loc;              
65
       
66
      }
67
  in
17 68
  let check_nd = { check_nd with
18 69
                   node_id = "check_eq_" ^ nd1.node_id ^ "_" ^ nd2.node_id;
19
                   node_outputs = [ok_var]; 
70
                   node_outputs = [ok_var];
71
                   node_locals = out_vars1 @ out_vars2;
72
                   node_stmts = [call_n1; call_n2; ok_stmt];
73
                   node_spec = Some (Contract contract);
20 74
                 }
21 75
  in
22
  check_nd
23 76

  
77
  
78
  Global.type_env := Typing.type_node !Global.type_env check_nd loc;
79
  Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc check_nd;
80
   
81
  check_nd
24 82
    (*
25 83

  
26 84
                   TODO:
......
38 96
     *)
39 97
    
40 98
      (* (\* Build the contract: guarentee output = orig_node(input) *\)
41
   * let expr_of_vars vl = 
42
   *   Corelang.expr_of_expr_list loc
43
   *     (List.map Corelang.expr_of_vdecl vl)
44
   * in
99
   * 
45 100
   * let local_outputs = List.map (fun v -> { (Corelang.copy_var_decl v) with var_id = v.var_id ^ "_local" } ) copy_nd.node_outputs in
46 101
   * let input_e = expr_of_vars  copy_nd.node_inputs in
47 102
   * let call_orig_e =
src/tools/seal/seal_export.ml
101 101

  
102 102
  
103 103
let to_lustre basename prog m sw_init sw_step init_out update_out =
104
  let loc = Location.dummy_loc in
104 105
  let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in
105
  
106
  Global.type_env := Typing.type_node !Global.type_env new_node loc;
107
  Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc new_node;
108

  
106 109
  (* Format.eprintf "%a@." Printers.pp_node new_node; *)
107 110

  
108 111
  (* Main output *)
......
110 113
  let new_top =
111 114
    Corelang.mktop_decl Location.dummy_loc output_file false (Node new_node)
112 115
  in
113
let out = open_out output_file in
116
  let out = open_out output_file in
114 117
  let fmt = Format.formatter_of_out_channel out in
115 118
  Format.fprintf fmt "%a@." Printers.pp_prog  [new_top];
116 119

  

Also available in: Unified diff