Changeset 2946 for src/joint/joint_fullexec.ma
- Timestamp:
- Mar 24, 2013, 11:29:01 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/joint_fullexec.ma
r2821 r2946 20 20 let p ≝ \fst p_stack in 21 21 let stack_sizes ≝ \snd p_stack in 22 let genv ≝ globalenv_noinit ? p in 23 let get_pc_lbl ≝ λid,lbl. 24 ! bl ← block_of_funct_id … pars genv id ; 25 pc_of_label … genv bl lbl in 22 let ev_pars : evaluation_params ≝ mk_prog_params pars p stack_sizes in 26 23 mk_joint_global pars 27 (prog_var_names ?? p) 28 (mk_genv_gen ?? genv ? stack_sizes get_pc_lbl). 29 (* (prog_io pars) *). 30 #s #H 31 elim (find_symbol_exists … p s ?) 32 [ #bl #EQ >EQ % #ABS destruct(ABS)|*:] 33 @Exists_append_r 34 @(Exists_mp … H) // 35 qed. 24 (globals … ev_pars) 25 (ev_genv … ev_pars). 36 26 37 27 definition joint_exec: sem_params → trans_system io_out io_in ≝ 38 28 λG.mk_trans_system ?? (joint_global G) (λ_. state_pc G) 39 (λenv. is_final G (jglobals … env) env exit_pc)29 (λenv.joint_final G (jglobals … env) env) 40 30 (λenv.λst.! st' ← eval_state … env st ; 41 31 let charge ≝ match joint_label_of_pc env (pc … st) with … … 49 39 (make_joint_global G) 50 40 (λp_stacks. 51 make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).41 return make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))). 52 42 53 43 definition joint_preclassified_system : sem_params →
Note: See TracChangeset
for help on using the changeset viewer.