Ignore:
Timestamp:
Mar 26, 2013, 2:01:15 PM (8 years ago)
Author:
tranquil
Message:
  • corrected all back-end premains to not pass any arguments to the main
  • premain fetching is made by fetch_function in joint_semantics.ma
  • reorganised some definition between Traces.ma and joint_fullexec.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/joint_fullexec.ma

    r2946 r2952  
    22include "common/Measurable.ma".
    33
    4 (* fullexec and co. *)
    5 record joint_global (p : sem_params) : Type[0] ≝
    6 { jglobals : list ident
    7 ; jgenv :> genv p jglobals
    8 }.
    9 
    10 definition eval_params_of_global : ∀p.joint_global p → evaluation_params ≝
    11 λp,gl.mk_evaluation_params (jglobals … gl) p gl.
    12 
    13 coercion eval_params_of_global : ∀p.∀gl : joint_global p.evaluation_params ≝
    14 eval_params_of_global on _gl : joint_global ? to evaluation_params.
    15 
    16 definition make_joint_global : ∀p : sem_params.
    17   (joint_program p × (ident → option ℕ)) →
    18   joint_global p ≝
    19 λpars, p_stack.
    20 let p ≝ \fst p_stack in
    21 let stack_sizes ≝ \snd p_stack in
    22 let ev_pars : evaluation_params ≝ mk_prog_params pars p stack_sizes in
    23 mk_joint_global pars
    24   (globals … ev_pars)
    25   (ev_genv … ev_pars).
    26 
    274definition joint_exec: sem_params → trans_system io_out io_in ≝
    28   λG.mk_trans_system ?? (joint_global G)  (λ_. state_pc G)
    29    (λenv.joint_final G (jglobals … env) env)
     5  λG.mk_trans_system ?? (evaluation_params G)  (λ_. state_pc G)
     6   (λenv.joint_final env)
    307   (λenv.λst.! st' ← eval_state … env st ;
    31     let charge ≝ match joint_label_of_pc env (pc … st) with
     8    let charge ≝ match joint_label_of_pc env (pc … st) with
    329      [ Some c ⇒ Echarge c | None ⇒ E0 ] in
    3310     return 〈charge, st'〉).
     
    3714  λG.mk_fullexec ?? (joint_program G × (ident → option ℕ))
    3815    (joint_exec G)
    39     (make_joint_global G)
     16    (λpr.joint_make_global (mk_prog_params G (\fst pr) (\snd pr)))
    4017    (λp_stacks.
    4118      return make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
     
    4421  preclassified_system ≝
    4522  λG.mk_preclassified_system (joint_fullexec G)
    46     (λenv.λst.¬is_none … (joint_label_of_pc (eval_params_of_global … env) (pc … st)))
    47     (λenv.joint_classify (eval_params_of_global … env))
    48     (λenv.λs.λ_.joint_call_ident (eval_params_of_global … env) s).
     23    (λenv.λst.¬is_none … (joint_label_of_pc  … env (pc … st)))
     24    (λenv.joint_classify … env)
     25    (λenv.λs.λ_.joint_call_ident … env s).
Note: See TracChangeset for help on using the changeset viewer.