Changeset 3262 for src/joint


Ignore:
Timestamp:
May 9, 2013, 11:31:48 AM (7 years ago)
Author:
piccolo
Message:

reverted status_simulation_utils

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/StatusSimulationUtils.ma

    r3259 r3262  
    1212(*                                                                        *)
    1313(**************************************************************************)
    14 
     14 
    1515include "joint/semanticsUtils.ma".
    1616include "joint/Traces.ma".
     
    419419  ∀n.stack_sizes f1 = return n → 
    420420  ∀st1'.
    421   setup_call ?? P_in … (joint_globalenv P_in prog stack_sizes) … n (joint_if_params … fn1)
    422    arg f1 st1_pre = return st1' →
     421  setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' →
    423422  st_rel st1 st2 → 
    424423  ∀t_fn1.
     
    445444         (mk_state_pc ? st2_pre_call pc' (last_pop … st2)) = return st2_pre ∧
    446445       ∃st2_after_call.
    447          setup_call ?? P_out … (joint_globalenv P_out trans_prog stack_sizes) … n
    448           (joint_if_params … t_fn1) arg' f1 st2_pre
     446         setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre
    449447          = return st2_after_call ∧
    450448       bind_new_P' ??
     
    517515   ∀ssize_f1.stack_sizes f1 = return ssize_f1 →   
    518516   ∀st1'.
    519     setup_call ?? P_in … (joint_globalenv P_in prog stack_sizes) … ssize_f1
    520      (joint_if_params … fn1) arg f1
     517    setup_call ?? P_in ssize_f1 (joint_if_params … fn1) arg
    521518     (decrement_stack_usage P_in ssize_f (st_no_pc … st1)) = return st1' →
    522519   st_rel st1 st2 → 
     
    536533         st2_pre_call = return bl ∧
    537534       ∃st2_after.
    538         setup_call ?? P_out … (joint_globalenv P_out trans_prog stack_sizes) …
    539          ssize_f1 (joint_if_params … t_fn1) arg' f1
     535        setup_call ?? P_out ssize_f1 (joint_if_params … t_fn1) arg'
    540536         (decrement_stack_usage P_out ssize_f st2_pre_call) = return st2_after ∧
    541537       bind_new_P' ??
Note: See TracChangeset for help on using the changeset viewer.