Changeset 2481 for src/joint/Traces.ma


Ignore:
Timestamp:
Nov 20, 2012, 6:40:08 PM (8 years ago)
Author:
piccolo
Message:

corrected some inconsistencies
fixed some of lineariseProof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2477 r2481  
    1515 { prog_spars : sem_params
    1616 ; prog : joint_program prog_spars
    17  ; stack_sizes : (Σi.is_internal_function_of_program ?? prog i) → ℕ
     17 ; stack_sizes : (Σi.is_internal_function_of_program prog i) → ℕ
    1818(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
    1919 }.
     
    4040]
    4141qed.
     42
     43lemma Exists_mp : ∀A,P,Q,l.(∀x.P x → Q x) → Exists A P l → Exists A Q l.
     44#A #P #Q #l #H elim l -l [*] #hd #tl #IH * #G [ %1 | %2 ] /2/ qed.
    4245
    4346definition make_global : prog_params → evaluation_params
     
    5255  (prog_spars pars)
    5356  ptr
    54   (mk_genv_gen ?? (globalenv_noinit ? p) ? (λi.stack_sizes pars «i, ?»))
     57  (mk_genv_gen ?? (globalenv_noinit ? p) ? (stack_sizes pars))
    5558 (* (prog_io pars) *).
    56 [ @(is_internal_function_of_program_ok … (pi2 … i))
    57 | #s #H
    58   lapply (map_Exists … H) -H #H
    59   elim (Exists_In … H) -H ** #id #r #v * #id_in #EQ destruct(EQ)
    60   elim (find_symbol_exists ??????? id_in)
    61   [ #bl #EQ >EQ % #ABS destruct(ABS)|]
    62 ]
     59#s #H
     60elim (find_symbol_exists … p s ?)
     61[ #bl #EQ >EQ % #ABS destruct(ABS)|*:]
     62@Exists_append_r
     63@(Exists_mp … H) //
    6364qed.
    6465
     
    286287   (* as_status ≝ *) (state_pc p)
    287288   (* as_execute ≝ *)
    288     (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … p (ev_genv p) s1) = return s2)
     289    (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … (ev_genv p) s1) = return s2)
    289290   (* as_pc ≝ *) pcDeq
    290291   (* as_pc_of ≝ *) (pc …)
     
    297298      ])
    298299   (* as_after_return ≝ *) (joint_after_ret p)
    299    (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?)
     300   (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) (exit p) s ≠ None ?)
    300301   (* as_call_ident ≝ *) (joint_call_ident p).
Note: See TracChangeset for help on using the changeset viewer.