Project

General

Profile

« Previous | Next » 

Revision 6cbbe1c1

Added by LĂ©lio Brun 8 months ago

start again with spec representation

View differences:

src/machine_code.ml
165 165

  
166 166
(* Datastructure updated while visiting equations *)
167 167
type machine_ctx = {
168
  (* machine name *)
169
  id: ident;
168 170
  (* Memories *)
169 171
  m: VSet.t;
170 172
  (* Reset instructions *)
......
181 183
  t: mc_formula_t list;
182 184
}
183 185

  
184
let ctx_init = {
186
let ctx_init id = {
187
  id;
185 188
  m = VSet.empty;
186 189
  si = [];
187 190
  j = IMap.empty;
......
191 194
  t = []
192 195
}
193 196

  
197
let ctx_dummy = ctx_init ""
198

  
194 199
(****************************************************************)
195 200
(* Main function to translate equations into this machine context we
196 201
   are building *) 
197 202
(****************************************************************)
198 203

  
199
let mk_control id vs v l inst =
204
let mk_control v l inst =
200 205
  mkinstr
201
    (Imply (mk_clocked_on id vs, inst.instr_spec))
206
    True
207
    (* (Imply (mk_clocked_on id vs, inst.instr_spec)) *)
202 208
    (MBranch (v, [l, [inst]]))
203 209

  
204
let control_on_clock env ctx ck inst =
205
  let rec aux (ck_ids, vs, ctx, inst as acc) ck =
210
let control_on_clock env ctx ck spec inst =
211
  let rec aux (ck_ids, vs, ctx, spec, inst as acc) ck =
206 212
    match (Clocks.repr ck).cdesc with
207 213
    | Con (ck, cr, l) ->
208 214
      let id = Clocks.const_of_carrier cr in
......
212 218
      let ck_spec = mk_condition v l in
213 219
      aux (id :: ck_ids,
214 220
           v :: vs,
215
           { ctx
216
             with c = IMap.add id ck_spec
217
                      (IMap.add id'
218
                         (And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c)
221
           { ctx with
222
             c = IMap.add id ck_spec
223
                 (IMap.add id' (And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c)
219 224
           },
220
           mk_control id' (v :: vs) v l inst) ck
225
           Imply (mk_clocked_on id' (v :: vs), spec),
226
           mk_control v l inst) ck
221 227
    | _ -> acc
222 228
  in
223
  let _, _, ctx, inst = aux ([], [], ctx, inst) ck in
224
  ctx, inst
229
  let _, _, ctx, spec, inst = aux ([], [], ctx, spec, inst) ck in
230
  ctx, spec, inst
225 231

  
226 232
let reset_instance env i r c =
227 233
  match r with
228 234
  | Some r ->
229
    [snd (control_on_clock env ctx_init c
230
            (mk_conditional
231
               (translate_guard env r)
232
               [mkinstr True (MReset i)]
233
               [mkinstr True (MNoReset i)]))]
235
    let _, _, inst = control_on_clock env ctx_dummy c True
236
        (mk_conditional
237
           (translate_guard env r)
238
           [mkinstr True (MReset i)]
239
           [mkinstr True (MNoReset i)]) in
240
    [ inst ]
234 241
  | None -> []
235 242

  
236 243

  
237
let translate_eq env ctx eq =
244
let translate_eq env ctx i eq =
238 245
  let translate_expr = translate_expr env in
239 246
  let translate_act = translate_act env in
240
  let control_on_clock ck inst =
241
    let ctx, ins = control_on_clock env ctx ck inst in
242
    { ctx with s = ins :: ctx.s }
247
  let control_on_clock ck spec inst =
248
    let ctx, _spec, inst = control_on_clock env ctx ck spec inst in
249
    { ctx with
250
      s = { inst with
251
            instr_spec = mk_transition ~i ctx.id [] } :: ctx.s }
243 252
  in
244 253
  let reset_instance = reset_instance env in
245 254
  let mkinstr' = mkinstr ~lustre_eq:eq True in
246
  let ctl ?(ck=eq.eq_rhs.expr_clock) instr =
247
    control_on_clock ck (mkinstr' instr) in
255
  let ctl ?(ck=eq.eq_rhs.expr_clock) spec instr =
256
    control_on_clock ck spec (mkinstr' instr) in
248 257

  
249 258
  (* Format.eprintf "translate_eq %a with clock %a@." 
250 259
     Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)
251 260
  match eq.eq_lhs, eq.eq_rhs.expr_desc with
252 261
  | [x], Expr_arrow (e1, e2)                     ->
253 262
    let var_x = env.get_var x in
254
    let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in
263
    let td = Arrow.arrow_top_decl () in
264
    let o = new_instance td eq.eq_rhs.expr_tag in
255 265
    let c1 = translate_expr e1 in
256 266
    let c2 = translate_expr e2 in
257
    let ctx = ctl (MStep ([var_x], o, [c1;c2])) in
267
    let ctx = ctl
268
        (mk_transition (node_name td) [])
269
        (MStep ([var_x], o, [c1;c2])) in
258 270
    { ctx with
259 271
      si = mkinstr True (MReset o) :: ctx.si;
260
      j = IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
272
      j = IMap.add o (td, []) ctx.j;
261 273
    }
274

  
262 275
  | [x], Expr_pre e1 when env.is_local x    ->
263 276
    let var_x = env.get_var x in
264
    let ctx = ctl (MStateAssign (var_x, translate_expr e1)) in
277
    let ctx = ctl
278
        True
279
        (MStateAssign (var_x, translate_expr e1)) in
265 280
    { ctx with
266 281
      m = VSet.add var_x ctx.m;
267 282
    }
283

  
268 284
  | [x], Expr_fby (e1, e2) when env.is_local x ->
269 285
    let var_x = env.get_var x in
270
    let ctx = ctl (MStateAssign (var_x, translate_expr e2)) in
286
    let ctx = ctl
287
        True
288
        (MStateAssign (var_x, translate_expr e2)) in
271 289
    { ctx with
272 290
      m = VSet.add var_x ctx.m;
273 291
      si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;
274 292
    }
293

  
275 294
  | p, Expr_appl (f, arg, r)
276 295
    when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
277 296
    let var_p = List.map (fun v -> env.get_var v) p in
......
284 303
        el [eq.eq_rhs.expr_clock] in
285 304
    let call_ck = Clock_calculus.compute_root_clock
286 305
        (Clock_predef.ck_tuple env_cks) in
287
    let ctx = ctl ~ck:call_ck (MStep (var_p, o, vl)) in
306
    let ctx = ctl
307
        ~ck:call_ck
308
        True
309
        (MStep (var_p, o, vl)) in
288 310
    (*Clocks.new_var true in
289 311
      Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
290 312
      Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)
......
297 319
           else reset_instance o r call_ck)
298 320
          @ ctx.s
299 321
    }
322

  
300 323
  | [x], _ ->
301 324
    let var_x = env.get_var x in
302
    control_on_clock eq.eq_rhs.expr_clock (translate_act (var_x, eq.eq_rhs))
325
    control_on_clock eq.eq_rhs.expr_clock True (translate_act (var_x, eq.eq_rhs))
326

  
303 327
  | _ ->
304 328
    Format.eprintf "internal error: Machine_code.translate_eq %a@?"
305 329
      Printers.pp_node_eq eq;
......
317 341
    locals []
318 342

  
319 343
let translate_eqs env ctx eqs =
320
  List.fold_right (fun eq ctx -> translate_eq env ctx eq) eqs ctx
344
  List.fold_right (fun eq (ctx, i) ->
345
      let ctx = translate_eq env ctx i eq in
346
      ctx, i - 1)
347
    eqs (ctx, List.length eqs)
348
  |> fst
321 349

  
322 350

  
323 351
(****************************************************************)
......
357 385
    in
358 386
    vars, eql, assertl
359 387

  
360
let translate_core sorted_eqs locals other_vars =
388
let translate_core nid sorted_eqs locals other_vars =
361 389
  let constant_eqs = constant_equations locals in
362 390

  
363 391
  let env = build_env locals other_vars  in
364 392

  
365 393
  (* Compute constants' instructions  *)
366
  let ctx0 = translate_eqs env ctx_init constant_eqs in
394
  let ctx0 = translate_eqs env (ctx_init nid) constant_eqs in
367 395
  assert (VSet.is_empty ctx0.m);
368 396
  assert (ctx0.si = []);
369 397
  assert (IMap.is_empty ctx0.j);
370 398

  
371 399
  (* Compute ctx for all eqs *)
372
  let ctx = translate_eqs env ctx_init sorted_eqs in
400
  let ctx = translate_eqs env (ctx_init nid) sorted_eqs in
373 401

  
374 402
  ctx, ctx0.s
375 403

  
......
402 430
   *   VSet.pp inout_vars
403 431
   * ; *)
404 432

  
405
  let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in
433
  let ctx, ctx0_s = translate_core
434
      nd.node_id (assert_instrs@sorted_eqs) locals inout_vars in
406 435

  
407 436
  (* Format.eprintf "ok4@.@?"; *)
408 437

  

Also available in: Unified diff