Changeset 2952 for src/joint/joint_fullexec.ma

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:

• src/joint/joint_fullexec.ma (modified) (3 diffs)

src/joint/joint_fullexec.ma

@@ -2 +2 @@
 include "common/Measurable.ma".
 
-(* fullexec and co. *)
-record joint_global (p : sem_params) : Type[0] ≝
-{ jglobals : list ident
-; jgenv :> genv p jglobals
-}.
-
-definition eval_params_of_global : ∀p.joint_global p → evaluation_params ≝
-λp,gl.mk_evaluation_params (jglobals … gl) p gl.
-
-coercion eval_params_of_global : ∀p.∀gl : joint_global p.evaluation_params ≝
-eval_params_of_global on _gl : joint_global ? to evaluation_params.
-
-definition make_joint_global : ∀p : sem_params.
-  (joint_program p × (ident → option ℕ)) →
-  joint_global p ≝
-λpars, p_stack.
-let p ≝ \fst p_stack in
-let stack_sizes ≝ \snd p_stack in
-let ev_pars : evaluation_params ≝ mk_prog_params pars p stack_sizes in
-mk_joint_global pars
-  (globals … ev_pars)
-  (ev_genv … ev_pars).
-
 definition joint_exec: sem_params → trans_system io_out io_in ≝
-  λG.mk_trans_system ?? (joint_global G)  (λ_. state_pc G)
-   (λenv.joint_final G (jglobals … env) env)
+  λG.mk_trans_system ?? (evaluation_params G)  (λ_. state_pc G)
+   (λenv.joint_final … env)
    (λenv.λst.! st' ← eval_state … env st ;
-    let charge ≝ match joint_label_of_pc env (pc … st) with
+    let charge ≝ match joint_label_of_pc … env (pc … st) with
       [ Some c ⇒ Echarge c | None ⇒ E0 ] in
      return 〈charge, st'〉).
@@ -37 +14 @@
   λG.mk_fullexec ?? (joint_program G × (ident → option ℕ))
     (joint_exec G)
-    (make_joint_global G) 
+    (λpr.joint_make_global (mk_prog_params G (\fst pr) (\snd pr)))
     (λp_stacks.
       return make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))).
@@ -44 +21 @@
   preclassified_system ≝
   λG.mk_preclassified_system (joint_fullexec G)
-    (λenv.λst.¬is_none … (joint_label_of_pc (eval_params_of_global … env) (pc … st)))
-    (λenv.joint_classify (eval_params_of_global … env))
-    (λenv.λs.λ_.joint_call_ident (eval_params_of_global … env) s).
+    (λenv.λst.¬is_none … (joint_label_of_pc  … env (pc … st)))
+    (λenv.joint_classify … env)
+    (λenv.λs.λ_.joint_call_ident … env s).