Changeset 2481 for src/joint/Traces.ma
 Timestamp:
 Nov 20, 2012, 6:40:08 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Traces.ma
r2477 r2481 15 15 { prog_spars : sem_params 16 16 ; 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) → ℕ 18 18 (* ; prog_io : state prog_spars → ∀o.res (io_in o) *) 19 19 }. … … 40 40 ] 41 41 qed. 42 43 lemma 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. 42 45 43 46 definition make_global : prog_params → evaluation_params … … 52 55 (prog_spars pars) 53 56 ptr 54 (mk_genv_gen ?? (globalenv_noinit ? p) ? ( λi.stack_sizes pars «i, ?»))57 (mk_genv_gen ?? (globalenv_noinit ? p) ? (stack_sizes pars)) 55 58 (* (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 60 elim (find_symbol_exists … p s ?) 61 [ #bl #EQ >EQ % #ABS destruct(ABS)*:] 62 @Exists_append_r 63 @(Exists_mp … H) // 63 64 qed. 64 65 … … 286 287 (* as_status ≝ *) (state_pc p) 287 288 (* 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) 289 290 (* as_pc ≝ *) pcDeq 290 291 (* as_pc_of ≝ *) (pc …) … … 297 298 ]) 298 299 (* 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 ?) 300 301 (* as_call_ident ≝ *) (joint_call_ident p).
Note: See TracChangeset
for help on using the changeset viewer.