Project

General

Profile

« Previous | Next » 

Revision dccec723

Added by LĂ©lio Brun over 3 years ago

a version that almost work for the k-inuctive two_counters example

View differences:

src/corelang.ml
193 193
    modes = [];
194 194
    imports = [];
195 195
    spec_loc = Location.dummy;
196
    proof = None
196 197
  }
197 198

  
198 199
(* For const declaration we do as for regular lustre node. But for local flows
......
213 214

  
214 215
let eexpr_add_name eexpr eexpr_name = { eexpr with eexpr_name }
215 216

  
216
let mk_contract_guarantees name eexpr =
217
let mk_contract_guarantees name eexpr proof =
217 218
  {
218 219
    empty_contract with
219 220
    guarantees = [ eexpr_add_name eexpr name ];
220 221
    spec_loc = eexpr.eexpr_loc;
222
    proof
221 223
  }
222 224

  
223 225
let mk_contract_assume name eexpr =
......
242 244
    spec_loc = loc;
243 245
  }
244 246

  
247
let merge_proofs p1 p2 =
248
  let merge_proofs p1 p2 = match p1, p2 with
249
    | Kinduction k1, Kinduction k2 ->
250
      Kinduction (max k1 k2)
251
  in
252
  match p1, p2 with
253
  | Some p1, Some p2 -> Some (merge_proofs p1 p2)
254
  | Some p, None | None, Some p -> Some p
255
  | None, None -> None
256

  
245 257
let merge_contracts ann1 ann2 =
246 258
  (* keeping the first item loc *)
247 259
  {
......
253 265
    modes = ann1.modes @ ann2.modes;
254 266
    imports = ann1.imports @ ann2.imports;
255 267
    spec_loc = ann1.spec_loc;
268
    proof = merge_proofs ann1.proof ann2.proof
256 269
  }
257 270

  
258 271
let mkeexpr loc expr =
......
1105 1118
    option_map
1106 1119
      (fun s ->
1107 1120
        match s with
1108
        | NodeSpec (id, oc) ->
1109
          NodeSpec (f_node id, option_map (rename_contract f_var f_node) oc)
1121
        | NodeSpec id ->
1122
          NodeSpec (f_node id)
1110 1123
        | Contract c ->
1111 1124
          Contract (rename_contract f_var f_node c))
1112 1125
      nd.node_spec

Also available in: Unified diff