CristalCaveGem » LustreC

  let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =

    let transform_local_to_state_assign instr = match instr.instr_desc with

      | MLocalAssign (ident, value) -> 

      | _ -> instr

    in

    let pp_local_ghost_list, spec_instrs = match m_spec_opt with

  **)

  let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =

    let build_assign = function var ->

    in

    let env, memory = match m_spec_opt with

      | None -> env, m.mmemory