Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

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
let expr_of_vars loc vl =
4
  Corelang.expr_of_expr_list loc (List.map Corelang.expr_of_vdecl vl)
5

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

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

  
54 56
  (* 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
      }
57
  let ok_e = Corelang.expr_of_vdecl ok_var in
58
  let contract =
59
    {
60
      consts = [];
61
      locals = [];
62
      stmts = [];
63
      assume = [];
64
      guarantees = [ Corelang.mkeexpr loc ok_e ];
65
      modes = [];
66
      imports = [];
67
      spec_loc = loc;
68
    }
67 69
  in
68
  let check_nd = { check_nd with
69
                   node_id = "check_eq_" ^ nd1.node_id ^ "_" ^ nd2.node_id;
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);
74
                 }
70
  let check_nd =
71
    {
72
      check_nd with
73
      node_id = "check_eq_" ^ nd1.node_id ^ "_" ^ nd2.node_id;
74
      node_outputs = [ ok_var ];
75
      node_locals = out_vars1 @ out_vars2;
76
      node_stmts = [ call_n1; call_n2; ok_stmt ];
77
      node_spec = Some (Contract contract);
78
    }
75 79
  in
76 80

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

  
84
                   TODO:
84
  check_nd
85
(* TODO:
85 86

  
86
                   construire
87
   construire
87 88

  
88
                   les variables temporaires pour les outputs de l'un et de l'autre
89
                   les statements d'appels de nodes
90
                   ok = and (o1 = o2)
89
   les variables temporaires pour les outputs de l'un et de l'autre les
90
   statements d'appels de nodes ok = and (o1 = o2)
91 91

  
92
                          et on ajoute le contrat guarantee ok
93
  in
94
  check_nd 
92
   et on ajoute le contrat guarantee ok in check_nd *)
95 93

  
96
     *)
97
    
98
      (* (\* Build the contract: guarentee output = orig_node(input) *\)
99
   * 
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
101
   * let input_e = expr_of_vars  copy_nd.node_inputs in
102
   * let call_orig_e =
103
   *   Corelang.mkexpr loc (Expr_appl (orig_nd.node_id, input_e , None)) in 
104
   * let build_orig_outputs =
105
   *   Eq (
106
   *       Corelang.mkeq loc
107
   *         (List.map (fun v -> v.var_id) local_outputs, call_orig_e)) in
108
   * let eq_expr =  Corelang.expr_of_expr_list loc (
109
   *                    List.map2 (fun v1 v2 ->
110
   *                        let args = expr_of_vars [v1;v2] in
111
   *                          Corelang.mkexpr loc (Expr_appl ("=", args, None)))
112
   *                  copy_nd.node_outputs local_outputs
113
   *                  )
114
   * in
115
   * let contract = {
116
   *     consts = [];
117
   *     locals = local_outputs;
118
   *     stmts = [build_orig_outputs];
119
   *     assume = [];
120
   *     guarantees = [Corelang.mkeexpr loc eq_expr];
121
   *     modes = [];
122
   *     imports = [];
123
   *     spec_loc = loc;              
124
   *    
125
   *   }
126
   * in *)
127
  
94
(* (\* Build the contract: guarentee output = orig_node(input) *\) * * let
95
   local_outputs = List.map (fun v -> { (Corelang.copy_var_decl v) with var_id =
96
   v.var_id ^ "_local" } ) copy_nd.node_outputs in * let input_e = expr_of_vars
97
   copy_nd.node_inputs in * let call_orig_e = * Corelang.mkexpr loc (Expr_appl
98
   (orig_nd.node_id, input_e , None)) in * let build_orig_outputs = * Eq ( *
99
   Corelang.mkeq loc * (List.map (fun v -> v.var_id) local_outputs,
100
   call_orig_e)) in * let eq_expr = Corelang.expr_of_expr_list loc ( * List.map2
101
   (fun v1 v2 -> * let args = expr_of_vars [v1;v2] in * Corelang.mkexpr loc
102
   (Expr_appl ("=", args, None))) * copy_nd.node_outputs local_outputs * ) * in
103
   * let contract = { * consts = []; * locals = local_outputs; * stmts =
104
   [build_orig_outputs]; * assume = []; * guarantees = [Corelang.mkeexpr loc
105
   eq_expr]; * modes = []; * imports = []; * spec_loc = loc; * * } * in *)

Also available in: Unified diff