Project

General

Profile

Revision f9f06e7d src/corelang.ml

View differences:

src/corelang.ml
175 175

  
176 176
let empty_contract =
177 177
  {
178
    consts = []; locals = []; assume = []; guarantees = []; modes = []; imports = []; spec_loc = Location.dummy_loc;
178
    consts = []; locals = []; stmts = []; assume = []; guarantees = []; modes = []; imports = []; spec_loc = Location.dummy_loc;
179 179
  }
180
    
180

  
181
(* For const declaration we do as for regular lustre node.
182
But for local flows we registered the variable and the lustre flow definition *)
181 183
let mk_contract_var id is_const type_opt expr loc =
182 184
  let typ = match type_opt with None -> mktyp loc Tydec_any | Some t -> t in
183
  let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, Some expr, None) in
184 185
  if is_const then
186
  let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, Some expr, None) in
185 187
  { empty_contract with consts = [v]; spec_loc = loc; }
186 188
  else
187
    { empty_contract with locals = [v]; spec_loc = loc; }
189
    let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, None, None) in
190
    let eq = mkeq loc ([id], expr) in 
191
    { empty_contract with locals = [v]; stmts = [Eq eq]; spec_loc = loc; }
188 192

  
189 193
let mk_contract_guarantees eexpr =
190 194
  { empty_contract with guarantees = [eexpr]; spec_loc = eexpr.eexpr_loc }
......
202 206
let merge_contracts ann1 ann2 = (* keeping the first item loc *)
203 207
  { consts = ann1.consts @ ann2.consts;
204 208
    locals = ann1.locals @ ann2.locals;
209
    stmts = ann1.stmts @ ann2.stmts;
205 210
    assume = ann1.assume @ ann2.assume;
206 211
    guarantees = ann1.guarantees @ ann2.guarantees;
207 212
    modes = ann1.modes @ ann2.modes;

Also available in: Unified diff