Changeset 2214 for src

Timestamp:

Jul 19, 2012, 2:42:02 PM (9 years ago)

Author:

tranquil

Message:

• changed order of parameters of joint_internal_function and genv in semantics
• in semantics, unified more_sem_unserialized_params and more_sem_genv_params
• renamed all <language>_params to <LANGUAGE>

Location:

src

Files:

• ERTL/ERTLToLTL_paolo.ma (modified) (26 diffs)
• ERTL/ERTL_paolo.ma (modified) (3 diffs)
• ERTL/liveness_paolo.ma (modified) (7 diffs)
• LIN/LIN_paolo.ma (modified) (1 diff)
• LIN/joint_LTL_LIN_paolo.ma (modified) (1 diff)
• LTL/LTL_paolo.ma (modified) (1 diff)
• RTL/RTLTailcall_paolo.ma (modified) (5 diffs)
• RTL/RTLToERTL_paolo.ma (modified) (25 diffs)
• RTL/RTL_paolo.ma (modified) (4 diffs)
• RTLabs/RTLabsToRTL_paolo.ma (modified) (34 diffs)
• joint/Joint_paolo.ma (modified) (7 diffs)
• joint/TranslateUtils_paolo.ma (modified) (11 diffs)
• joint/blocks.ma (modified) (5 diffs)
• joint/linearise.ma (modified) (2 diffs)
• joint/semanticsUtils_paolo.ma (modified) (2 diffs)
• joint/semantics_paolo.ma (modified) (30 diffs)

src/ERTL/ERTLToLTL_paolo.ma

@@ +1 @@
+
 include "LTL/LTL_paolo.ma".
 include "ERTL/Interference_paolo.ma".
@@ -18 +19 @@
 coercion Reg_to_arg_dec : ∀r:Register.arg_decision ≝ arg_decision_colour on _r : Register to arg_decision.
 
-definition stacksize :
-  ∀globals.ℕ → joint_internal_function globals ertl_params → ℕ ≝
-  λglobals.
-  λspilled_no.
-  λint_fun.
-  spilled_no + joint_if_stacksize … int_fun.
-
 (* Paolo: I'm changing the following: before, spilled registers were
   assigned stack addresses going from SP + #frame_size - #stack_params
@@ -31 +25 @@
 
 definition preserve_carry_bit :
-  ∀globals.bool → list (joint_seq ltl_params globals) → list (joint_seq ltl_params globals) ≝
+  ∀globals.bool → list (joint_seq LTL globals) → list (joint_seq LTL globals) ≝
   λglobals,do_it,steps.
   if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps.
@@ -42 +36 @@
 (* spill should be byte-based from the start *)
 definition set_dp_by_offset :
-  ∀globals.nat → list (joint_seq ltl_params globals) ≝
+  ∀globals.nat → list (joint_seq LTL globals) ≝
   λglobals,off.
   [ A ← byte_of_nat off
@@ -53 +47 @@
 
 definition get_stack:
- ∀globals.Register → nat → list (joint_seq ltl_params globals) ≝
+ ∀globals.Register → nat → list (joint_seq LTL globals) ≝
  λglobals,r,off.
  set_dp_by_offset ? off @
@@ -60 +54 @@
 
 definition set_stack_not_a :
- ∀globals.nat → Register → list (joint_seq ltl_params globals) ≝
+ ∀globals.nat → Register → list (joint_seq LTL globals) ≝
  λglobals,off,r.
  set_dp_by_offset ? off @
@@ -67 +61 @@
 
 definition set_stack_a :
- ∀globals.nat → list (joint_seq ltl_params globals) ≝
+ ∀globals.nat → list (joint_seq LTL globals) ≝
  λglobals,off.
  [ RegisterST1 ← A ] @
@@ -73 +67 @@
 
 definition set_stack :
- ∀globals.nat → Register → list (joint_seq ltl_params globals) ≝
+ ∀globals.nat → Register → list (joint_seq LTL globals) ≝
  λglobals,off,r.
  if eq_Register r RegisterA then
@@ -81 +75 @@
  
 definition set_stack_int :
-  ∀globals.nat → beval →  list (joint_seq ltl_params globals) ≝
+  ∀globals.nat → beval →  list (joint_seq LTL globals) ≝
   λglobals,off,int.
   set_dp_by_offset ? off @
@@ -88 +82 @@
 
 definition move :
-  ∀globals.bool → decision → arg_decision → list (joint_seq ltl_params globals) ≝
+  ∀globals.bool → decision → arg_decision → list (joint_seq LTL globals) ≝
   λglobals,carry_lives_after,dst,src.
   match dst with
@@ -128 +122 @@
 
 definition newframe :
-  ∀globals.ℕ → list (joint_seq ltl_params globals) ≝
+  ∀globals.ℕ → list (joint_seq LTL globals) ≝
   λglobals,stack_sz.
   [ CLEAR_CARRY …
@@ -140 +134 @@
 
 definition delframe :
-  ∀globals.ℕ → list (joint_seq ltl_params globals) ≝
+  ∀globals.ℕ → list (joint_seq LTL globals) ≝
   λglobals,stack_sz.
   [ A ← RegisterSPL
@@ -176 +170 @@
 
 definition translate_op2 :
-  ∀globals.bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
+  ∀globals.bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
   λglobals,carry_lives_after,op,dst,arg1,arg2.
   (* this won't preserve the carry bit if op does not set it: left to next function *)
@@ -189 +183 @@
 
 definition translate_op2_smart :
-  ∀globals.bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
+  ∀globals.bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
   λglobals,carry_lives_after,op,dst,arg1,arg2.
   (* if op does not set carry bit (⇒ it does not use it either) then it must be
@@ -232 +226 @@
 
 definition translate_op1 :
-  ∀globals.bool → Op1 → decision → decision → list (joint_seq ltl_params globals) ≝
+  ∀globals.bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝
   λglobals,carry_lives_after,op,dst,arg.
   let preserve_carry ≝ carry_lives_after ∧ (is_spilled dst ∨ is_spilled arg) in
@@ -241 +235 @@
 
 definition translate_opaccs :
-  ∀globals.bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
+  ∀globals.bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
   λglobals,carry_lives_after,op,dst1,dst2,arg1,arg2.
   (* OPACCS always has dead carry bit and sets it to zero *)
@@ -255 +249 @@
 (* does not preserve carry bit *)
 definition move_to_dp :
-  ∀globals.arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
+  ∀globals.arg_decision → arg_decision → list (joint_seq LTL globals) ≝
   λglobals,arg1,arg2.
   if ¬arg_is_spilled arg1 then
@@ -272 +266 @@
 
 definition translate_store :  
-  ∀globals.bool → arg_decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
+  ∀globals.bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
   λglobals,carry_lives_after,addr1,addr2,src.
   (* requires src != RegisterA and RegisterB *)
@@ -286 +280 @@
 
 definition translate_load :  
-  ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
+  ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
   λglobals,carry_lives_after,dst,addr1,addr2.
   preserve_carry_bit ? (carry_lives_after ∧
@@ -296 +290 @@
 definition translate_address :
   ∀globals.bool → ∀i.member i (eq_identifier ?) globals → decision → decision →
-  list (joint_seq ltl_params globals) ≝
+  list (joint_seq LTL globals) ≝
   λglobals,carry_lives_after,id,prf,addr1,addr2.
   preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2))
-    (ADDRESS ltl_params ? id prf it it ::
+    (ADDRESS LTL ? id prf it it ::
      move ? false addr1 RegisterDPL @
      move ? false addr2 RegisterDPH).
@@ -306 +300 @@
   ∀globals.∀after : valuation register_lattice.
   coloured_graph after →
-  ℕ → label → joint_step ertl_params globals → seq_block ltl_params globals (joint_step ltl_params globals) ≝
+  ℕ → label → joint_step ERTL globals → seq_block LTL globals (joint_step LTL globals) ≝
   λglobals,after,grph,stack_sz,lbl,s.
   let lookup ≝ λr.colouring … grph (inl … r) in
@@ -317 +311 @@
   match s with
   [ step_seq s' ⇒
-    match s' return λ_.seq_block ltl_params globals (joint_step ltl_params globals) with
+    match s' return λ_.seq_block LTL globals (joint_step LTL globals) with
     [ COMMENT c ⇒ COMMENT … c
     | COST_LABEL cost_lbl ⇒ COST_LABEL … cost_lbl
@@ -373 +367 @@
         move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
       ]
-    | CALL_ID f n_args _ ⇒ CALL_ID ltl_params ? f n_args it
+    | CALL_ID f n_args _ ⇒ CALL_ID LTL ? f n_args it
     | extension_call abs ⇒ match abs in void with [ ]
     ]
@@ -381 +375 @@
 
 definition translate_fin_step:
-  ∀globals.label → joint_fin_step ertl_params → seq_block ltl_params globals (joint_fin_step ltl_params) ≝
+  ∀globals.label → joint_fin_step ERTL → seq_block LTL globals (joint_fin_step LTL) ≝
   λglobals,lbl,s.
-  match s return λ_.seq_block ltl_params globals (joint_fin_step ltl_params) with
+  match s return λ_.seq_block LTL globals (joint_fin_step LTL) with
   [ RETURN ⇒ RETURN ?
   | GOTO l ⇒ GOTO ? l
@@ -390 +384 @@
 
 definition translate_internal: ∀globals: list ident.
-  joint_internal_function globals ertl_params →
-  joint_internal_function globals ltl_params ≝
+  joint_internal_function ERTL globals →
+  joint_internal_function LTL globals ≝
   λglobals: list ident.
-  λint_fun: joint_internal_function globals ertl_params.
+  λint_fun: joint_internal_function ERTL globals.
   (* initialize graph *)
   let entry ≝ pi1 … (joint_if_entry … int_fun) in
@@ -405 +399 @@
   let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
   (* initialize internal function *)
-  let init ≝ mk_joint_internal_function globals ltl_params
+  let init ≝ mk_joint_internal_function LTL globals
     (joint_if_luniverse … int_fun)
     (joint_if_runiverse … int_fun)

src/ERTL/ERTL_paolo.ma

@@ +1 @@
+
 include "joint/Joint_paolo.ma".
 include "RTL/RTL_paolo.ma".
@@ -48 +49 @@
       (* localsT ≝ *) register).
 
-definition ertl_params ≝ mk_graph_params ertl_uns_params.
-definition ertl_program ≝ joint_program ertl_params.
+definition ERTL ≝ mk_graph_params ertl_uns_params.
+definition ertl_program ≝ joint_program ERTL.
 
 interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)).
@@ -56 +57 @@
 unification hint 0 ≔
 (*---------------*) ⊢
-pair_move ertl_params ≡ move_dst × move_src.
+pair_move ERTL ≡ move_dst × move_src.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_a_reg ertl_params ≡ register.
+acc_a_reg ERTL ≡ register.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_b_reg ertl_params ≡ register.
+acc_b_reg ERTL ≡ register.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_a_arg ertl_params ≡ psd_argument.
+acc_a_arg ERTL ≡ psd_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_b_arg ertl_params ≡ psd_argument.
+acc_b_arg ERTL ≡ psd_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-dpl_reg ertl_params ≡ register.
+dpl_reg ERTL ≡ register.
 unification hint 0 ≔
 (*---------------*) ⊢
-dph_reg ertl_params ≡ register.
+dph_reg ERTL ≡ register.
 unification hint 0 ≔
 (*---------------*) ⊢
-dpl_arg ertl_params ≡ psd_argument.
+dpl_arg ERTL ≡ psd_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-dph_arg ertl_params ≡ psd_argument.
+dph_arg ERTL ≡ psd_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-snd_arg ertl_params ≡ psd_argument.
+snd_arg ERTL ≡ psd_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-call_args ertl_params ≡ ℕ.
+call_args ERTL ≡ ℕ.
 unification hint 0 ≔
 (*---------------*) ⊢
-call_dest ertl_params ≡ unit.
+call_dest ERTL ≡ unit.
 
 unification hint 0 ≔
 (*---------------*) ⊢
-ext_seq ertl_params ≡ ertl_seq.
+ext_seq ERTL ≡ ertl_seq.
 unification hint 0 ≔
 (*---------------*) ⊢
-ext_call ertl_params ≡ void.
+ext_call ERTL ≡ void.
 unification hint 0 ≔
 (*---------------*) ⊢
-ext_tailcall ertl_params ≡ void.
+ext_tailcall ERTL ≡ void.
 
-coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ertl_params ≝
+coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ERTL ≝
   psd_argument_from_reg
-  on _r : register to snd_arg ertl_params.
-coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ertl_params ≝
+  on _r : register to snd_arg ERTL.
+coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ERTL ≝
   psd_argument_from_byte
-  on _b : Byte to snd_arg ertl_params.
+  on _b : Byte to snd_arg ERTL.
   
-definition ertl_seq_joint ≝ extension_seq ertl_params.
-coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ertl_params globals ≝ ertl_seq_joint
-  on _s : ertl_seq to joint_seq ertl_params.
-
+definition ertl_seq_joint ≝ extension_seq ERTL.
+coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint
+  on _s : ertl_seq to joint_seq ERTL.

src/ERTL/liveness_paolo.ma

@@ +1 @@
+
 include "ASM/Util.ma".
 include "ERTL/ERTL_paolo.ma".
@@ -42 +43 @@
 definition defined ≝
   λglobals: list ident.
-  λs: joint_statement ertl_params globals.
+  λs: joint_statement ERTL globals.
   match s with
   [ sequential seq l ⇒
@@ -100 +101 @@
 definition used ≝
   λglobals: list ident.
-  λs: joint_statement ertl_params globals.
+  λs: joint_statement ERTL globals.
   match s with
   [ sequential seq l ⇒
@@ -155 +156 @@
   λglobals: list ident.
   λl: register_lattice.
-  λs: joint_statement ertl_params globals.
+  λs: joint_statement ERTL globals.
   let pliveafter ≝ \fst l in
   let hliveafter ≝ \snd l in
@@ -225 +226 @@
 
 definition statement_semantics: ∀globals: list ident.
-  joint_statement ertl_params globals → register_lattice → register_lattice ≝
+  joint_statement ERTL globals → register_lattice → register_lattice ≝
   λglobals.
   λstmt.
@@ -236 +237 @@
 definition livebefore ≝
   λglobals: list ident.
-  λint_fun: joint_internal_function globals ertl_params.
+  λint_fun: joint_internal_function ERTL globals.
   λlabel.
   λliveafter: valuation register_lattice.
@@ -246 +247 @@
 definition liveafter ≝
    λglobals: list ident.
-  λint_fun: joint_internal_function globals ertl_params.
+  λint_fun: joint_internal_function ERTL globals.
   λlabel.
   λliveafter: valuation register_lattice.

src/LIN/LIN_paolo.ma

@@ -1 +1 @@
 include "LIN/joint_LTL_LIN_paolo.ma".
 
-definition lin_params ≝ mk_lin_params ltl_lin_params.
+definition LIN ≝ mk_lin_params LTL_LIN.
 
 (* aid unification *)
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_a_reg lin_params ≡ unit.
+acc_a_reg LIN ≡ unit.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_a_arg lin_params ≡ unit.
+acc_a_arg LIN ≡ unit.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_b_reg lin_params ≡ unit.
+acc_b_reg LIN ≡ unit.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_a_arg lin_params ≡ unit.
+acc_a_arg LIN ≡ unit.
 unification hint 0 ≔
 (*---------------*) ⊢
-snd_arg lin_params ≡ ltl_argument.
+snd_arg LIN ≡ hdw_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-ext_seq lin_params ≡ ltl_lin_seq.
+ext_seq LIN ≡ ltl_lin_seq.
 unification hint 0 ≔
 (*---------------*) ⊢
-pair_move lin_params ≡ registers_move.
+pair_move LIN ≡ registers_move.
 
-definition lin_program ≝ joint_program lin_params.
+definition lin_program ≝ joint_program LIN.

src/LIN/joint_LTL_LIN_paolo.ma

@@ -12 +12 @@
 | RESTORE_CARRY : ltl_lin_seq.
 
-definition ltl_lin_params : unserialized_params ≝ mk_unserialized_params
+definition LTL_LIN : unserialized_params ≝ mk_unserialized_params
   (mk_step_params
     (* acc_a_reg ≝ *) unit

src/LTL/LTL_paolo.ma

@@ -1 +1 @@
 include "LIN/joint_LTL_LIN_paolo.ma".
 
-definition ltl_params ≝ mk_graph_params ltl_lin_params.
+definition LTL ≝ mk_graph_params LTL_LIN.
 
 (* aid unification *)
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_a_reg ltl_params ≡ unit.
+acc_a_reg LTL ≡ unit.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_a_arg ltl_params ≡ unit.
+acc_a_arg LTL ≡ unit.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_b_reg ltl_params ≡ unit.
+acc_b_reg LTL ≡ unit.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_a_arg ltl_params ≡ unit.
+acc_a_arg LTL ≡ unit.
 unification hint 0 ≔
 (*---------------*) ⊢
-snd_arg ltl_params ≡ hdw_argument.
+snd_arg LTL ≡ hdw_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-ext_seq ltl_params ≡ ltl_lin_seq.
+ext_seq LTL ≡ ltl_lin_seq.
 unification hint 0 ≔
 (*---------------*) ⊢
-pair_move ltl_params ≡ registers_move.
+pair_move LTL ≡ registers_move.
 
-definition ltl_program ≝ joint_program ltl_params.
+definition ltl_program ≝ joint_program LTL.
 
-coercion byte_to_ltl_argument : ∀b: Byte.snd_arg ltl_params ≝
-  hdw_argument_from_byte on _b : Byte to snd_arg ltl_params.
-coercion reg_to_ltl_argument : ∀r: Register.snd_arg ltl_params ≝
-  hdw_argument_from_reg on _r : Register to snd_arg ltl_params.
+coercion byte_to_ltl_argument : ∀b: Byte.snd_arg LTL ≝
+  hdw_argument_from_byte on _b : Byte to snd_arg LTL.
+coercion reg_to_ltl_argument : ∀r: Register.snd_arg LTL ≝
+  hdw_argument_from_reg on _r : Register to snd_arg LTL.

src/RTL/RTLTailcall_paolo.ma

@@ -5 +5 @@
   λexit: label.
   λlbl: label.
-  λstmt: rtl_statement globals.
-  λgraph: codeT rtlntc_params globals.
+  λstmt: joint_statement RTL globals.
+  λgraph: codeT RTL_ntc globals.
   match stmt with
   [ final fin ⇒
@@ -13 +13 @@
          match ext with
           [ rtl_tailcall_id f args ⇒
-              add … graph lbl (sequential … (CALL_ID rtlntc_params ? f args [ ]) exit)
+              add … graph lbl (sequential … (CALL_ID RTL_ntc ? f args [ ]) exit)
           | rtl_tailcall_ptr f1 f2 args ⇒
-              add … graph lbl (sequential rtlntc_params ? (rtl_call_ptr f1 f2 args [ ] : ext_call rtlntc_params) exit)
+              add … graph lbl (sequential RTL_ntc ? (rtl_call_ptr f1 f2 args [ ] : ext_call RTL_ntc) exit)
           ]
       | _ ⇒ graph ]
@@ -23 +23 @@
   λglobals.
   λexit: label.
-  λgraph: codeT rtl_params globals.
+  λgraph: codeT RTL globals.
     foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).
 
 axiom simplify_graph_preserves_labels:
   ∀globals.
-  ∀g: codeT rtl_params globals.
+  ∀g: codeT RTL globals.
   ∀exit: label.
   ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g.
@@ -34 +34 @@
 definition simplify_internal :
  ∀globals.
-  joint_internal_function globals rtl_params →
-   joint_internal_function globals rtlntc_params
+  joint_internal_function RTL globals →
+   joint_internal_function RTL_ntc globals
 ≝
   λglobals,def.
@@ -48 +48 @@
 qed.
 
-definition tailcall_simplify : rtl_program → rtlntc_program ≝
+definition tailcall_simplify : rtl_program → rtl_ntc_program ≝
  λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)).

src/RTL/RTLToERTL_paolo.ma

@@ -8 +8 @@
 
 definition save_hdws :
-  ∀globals.list (register×Register) → list (joint_seq ertl_params globals) ≝
+  ∀globals.list (register×Register) → list (joint_seq ERTL globals) ≝
  λglobals.
   let save_hdws_internal ≝
@@ -15 +15 @@
 
 definition restore_hdws :
-  ∀globals.list (psd_argument×Register) → list (joint_seq ertl_params globals) ≝
+  ∀globals.list (psd_argument×Register) → list (joint_seq ERTL globals) ≝
   λglobals.
    let restore_hdws_internal ≝
@@ -22 +22 @@
 
 definition get_params_hdw :
-  ∀globals.list register → list (joint_seq ertl_params globals) ≝
+  ∀globals.list register → list (joint_seq ERTL globals) ≝
   λglobals,params.
   save_hdws … (zip_pottier … params RegisterParams).
@@ -28 +28 @@
 definition get_param_stack :
   ∀globals.register → register → register →
-  list (joint_seq ertl_params globals) ≝
+  list (joint_seq ERTL globals) ≝
   λglobals,addr1,addr2,destr.
   (* liveness analysis will erase the last useless ops *)
@@ -38 +38 @@
 definition get_params_stack :
   ∀globals.list register →
-  bind_new (localsT ertl_params) (list (joint_seq ertl_params globals)) ≝
+  bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
   λglobals,params.
   νtmpr,addr1,addr2 in
@@ -59 +59 @@
 definition prologue :
   ∀globals.list register → register → register → list (register×Register) →
-  bind_new (localsT ertl_params) (list (joint_seq ertl_params globals)) ≝
+  bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
   λglobals,params,sral,srah,sregs.
   [ (ertl_new_frame : joint_seq ??) ;
@@ -67 +67 @@
 
 definition save_return :
-  ∀globals.list psd_argument → list (joint_seq ertl_params globals) ≝
+  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
   λglobals,ret_regs.
   match reduce_strong ? ? RegisterSTS ret_regs with
@@ -79 +79 @@
   ].
 
-definition assign_result : ∀globals.list (joint_seq ertl_params globals) ≝
+definition assign_result : ∀globals.list (joint_seq ERTL globals) ≝
   λglobals.
   match reduce_strong ?? RegisterRets RegisterSTS with
@@ -90 +90 @@
 definition epilogue :
   ∀globals.list register → register → register → list (register × Register) →
-  list (joint_seq ertl_params globals) ≝
+  list (joint_seq ERTL globals) ≝
   λglobals,ret_regs,sral,srah,sregs.
   save_return … (map … (Reg ?) ret_regs) @
   restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @
-  [ PUSH ertl_params ? srah ;
+  [ PUSH ERTL ? srah ;
     PUSH … sral ;
     ertl_del_frame ] @
@@ -101 +101 @@
 definition allocate_regs :
   ∀globals,rs.rs_set rs →
-  state_monad (joint_internal_function globals ertl_params) (list (register×Register)) ≝
+  state_monad (joint_internal_function ERTL globals) (list (register×Register)) ≝
   λglobals,rs,saved,def.
    let allocate_regs_internal ≝
@@ -112 +112 @@
 definition add_pro_and_epilogue :
   ∀globals.list register → list register →
-  joint_internal_function globals ertl_params →
-  joint_internal_function globals ertl_params ≝
+  joint_internal_function ERTL globals →
+  joint_internal_function ERTL globals ≝
   λglobals,params,ret_regs,def.
   let start_lbl ≝ joint_if_entry … def in
@@ -129 +129 @@
 
 definition set_params_hdw :
-  ∀globals.list psd_argument → list (joint_seq ertl_params globals) ≝
+  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
   λglobals,params.
   restore_hdws globals (zip_pottier ? ? params RegisterParams).
@@ -137 +137 @@
 definition set_param_stack :
   ∀globals.register → register → psd_argument →
-  list (joint_seq ertl_params globals) ≝
+  list (joint_seq ERTL globals) ≝
   λglobals,addr1,addr2,arg.
   [ STORE … addr1 addr2 arg ;
@@ -145 +145 @@
 
 definition set_params_stack :
-  ∀globals.list psd_argument → bind_new (localsT ertl_params) ? ≝
+  ∀globals.list psd_argument → bind_new (localsT ERTL) ? ≝
   λglobals,params.
   νaddr1,addr2 in
@@ -166 +166 @@
 
 definition fetch_result :
-  ∀globals.list register → list (joint_seq ertl_params globals) ≝
+  ∀globals.list register → list (joint_seq ERTL globals) ≝
   λglobals,ret_regs.
   match reduce_strong ?? RegisterSTS RegisterRets with
@@ -182 +182 @@
 
 definition translate_step :
-  ∀globals.label → joint_step rtlntc_params globals →
-    bind_seq_block ertl_params globals (joint_step ertl_params globals) ≝
+  ∀globals.label → joint_step RTL_ntc globals →
+    bind_seq_block ERTL globals (joint_step ERTL globals) ≝
   λglobals.λ_.λs.
   match s return λ_.bind_seq_block ?? (joint_step ??) with
@@ -194 +194 @@
       COST_LABEL … lbl
     | ADDRESS x prf r1 r2 ⇒
-      ADDRESS ertl_params ? x prf r1 r2
+      ADDRESS ERTL ? x prf r1 r2
     | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
-      OPACCS ertl_params ? op destr1 destr2 srcr1 srcr2  
+      OPACCS ERTL ? op destr1 destr2 srcr1 srcr2  
     | OP1 op1 destr srcr ⇒
-      OP1 ertl_params ? op1 destr srcr
+      OP1 ERTL ? op1 destr srcr
     | OP2 op2 destr srcr1 srcr2 ⇒
-      OP2 ertl_params ? op2 destr srcr1 srcr2
+      OP2 ERTL ? op2 destr srcr1 srcr2
     | CLEAR_CARRY ⇒
       CLEAR_CARRY …
@@ -206 +206 @@
       SET_CARRY …
     | LOAD destr addr1 addr2 ⇒
-      LOAD ertl_params ? destr addr1 addr2
+      LOAD ERTL ? destr addr1 addr2
     | STORE addr1 addr2 srcr ⇒
-      STORE ertl_params ? addr1 addr2 srcr
+      STORE ERTL ? addr1 addr2 srcr
     | COMMENT msg ⇒
       COMMENT … msg
@@ -218 +218 @@
     | CALL_ID f args ret_regs ⇒
       set_params ? args @@
-      CALL_ID ertl_params ? f (|args|) it :::
+      CALL_ID ERTL ? f (|args|) it :::
       fetch_result ? ret_regs
     | extension_call c ⇒
@@ -227 +227 @@
     ]
   | COND r ltrue ⇒
-    COND ertl_params ? r ltrue
+    COND ERTL ? r ltrue
   ]. cases daemon (* pointer call to be ported yet *) qed.
 
 definition translate_fin_step :
-  ∀globals.label → joint_fin_step rtlntc_params →
-    bind_seq_block ertl_params globals (joint_fin_step ertl_params) ≝
+  ∀globals.label → joint_fin_step RTL_ntc →
+    bind_seq_block ERTL globals (joint_fin_step ERTL) ≝
   λglobals.λ_.λs.
   match s with
@@ -242 +242 @@
 (* hack with empty graphs used here *)
 definition translate_funct :
-  ∀globals.joint_internal_function globals rtlntc_params →
-    joint_internal_function globals ertl_params ≝
+  ∀globals.joint_internal_function RTL_ntc globals →
+    joint_internal_function ERTL globals ≝
   λglobals,def.
   let nb_params ≝ |joint_if_params ?? def| in
@@ -253 +253 @@
   let graph' ≝ add ? ? graph' exit' (RETURN …) in
   let def' ≝
-    mk_joint_internal_function globals ertl_params
+    mk_joint_internal_function ERTL globals
       (joint_if_luniverse … def) (joint_if_runiverse … def) it (*Paolo: to be checked, unit or list register? *)
       nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
@@ -272 +272 @@
   λglobals.
   λstmt.
-  λdef: joint_internal_function globals ertl_params.
+  λdef: joint_internal_function globals ERTL.
   let 〈entry, def〉 ≝ fresh_label … def in
   let graph ≝ add … (joint_if_code … def) entry stmt in
-   set_joint_if_graph … (ertl_params globals) graph def ??.
+   set_joint_if_graph … (ERTL globals) graph def ??.
   [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
   | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
@@ -295 +295 @@
          match inst with
           [ COST_LABEL cost_lbl ⇒
-             〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉
+             〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉
           | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
       | RETURN ⇒ 〈None …, def〉
@@ -310 +310 @@
   match cost_label with
   [ None ⇒ def
-  | Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
+  | Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
   ].
 

src/RTL/RTL_paolo.ma

@@ -11 +11 @@
   | rtl_tailcall_ptr: register → register → list psd_argument → rtl_tailcall.
 
-definition rtl_uns_params ≝ mk_unserialized_params
+definition RTL_uns ≝ mk_unserialized_params
   (mk_step_params
     (* acc_a_reg ≝ *) register
@@ -35 +35 @@
       (* localsT ≝ *) register).
 
-definition rtl_params ≝ mk_graph_params rtl_uns_params.
-definition lin_rtl_params ≝ mk_lin_params rtl_uns_params.
-definition rtl_internal_function ≝
-  λglobals. joint_internal_function globals rtl_params.
-definition rtl_program ≝ joint_program rtl_params.
-definition rtl_step ≝ joint_step rtl_params.
-definition rtl_seq ≝ joint_seq rtl_params.
-definition rtl_statement ≝ joint_statement rtl_params.
+definition RTL ≝ mk_graph_params RTL_uns.
+definition rtl_program ≝ joint_program RTL.
 
-interpretation "move" 'mov r a = (MOVE rtl_params ? (mk_Prod ? psd_argument r a)).
+interpretation "move" 'mov r a = (MOVE RTL ? (mk_Prod ? psd_argument r a)).
 
 (* aid unification *)
@@ -50 +44 @@
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_a_reg rtl_params ≡ register.
+acc_a_reg RTL ≡ register.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_b_reg rtl_params ≡ register.
+acc_b_reg RTL ≡ register.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_a_arg rtl_params ≡ psd_argument.
+acc_a_arg RTL ≡ psd_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-acc_b_arg rtl_params ≡ psd_argument.
+acc_b_arg RTL ≡ psd_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-dpl_reg rtl_params ≡ register.
+dpl_reg RTL ≡ register.
 unification hint 0 ≔
 (*---------------*) ⊢
-dph_reg rtl_params ≡ register.
+dph_reg RTL ≡ register.
 unification hint 0 ≔
 (*---------------*) ⊢
-dpl_arg rtl_params ≡ psd_argument.
+dpl_arg RTL ≡ psd_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-dph_arg rtl_params ≡ psd_argument.
+dph_arg RTL ≡ psd_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-snd_arg rtl_params ≡ psd_argument.
+snd_arg RTL ≡ psd_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-pair_move rtl_params ≡ register × psd_argument.
+pair_move RTL ≡ register × psd_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-call_args rtl_params ≡ list psd_argument.
+call_args RTL ≡ list psd_argument.
 unification hint 0 ≔
 (*---------------*) ⊢
-call_dest rtl_params ≡ list register.
+call_dest RTL ≡ list register.
 
 unification hint 0 ≔
 (*---------------*) ⊢
-ext_seq rtl_params ≡ rtl_seq.
+ext_seq RTL ≡ rtl_seq.
 unification hint 0 ≔
 (*---------------*) ⊢
-ext_call rtl_params ≡ rtl_call.
+ext_call RTL ≡ rtl_call.
 unification hint 0 ≔
 (*---------------*) ⊢
-ext_tailcall rtl_params ≡ rtl_tailcall.
-unification hint 0 ≔ globals
-(*---------------*) ⊢
-joint_step rtl_params globals ≡ rtl_step globals.
+ext_tailcall RTL ≡ rtl_tailcall.
 
-unification hint 0 ≔ globals
-(*---------------*) ⊢
-joint_seq rtl_params globals ≡ rtl_seq globals.
-unification hint 0 ≔ globals
-(*---------------*) ⊢
-joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
-
-coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ psd_argument_from_reg
-  on _r : register to snd_arg rtl_params.
-coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ psd_argument_from_byte
-  on _b : Byte to snd_arg rtl_params.
+coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg RTL ≝ psd_argument_from_reg
+  on _r : register to snd_arg RTL.
+coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg RTL ≝ psd_argument_from_byte
+  on _b : Byte to snd_arg RTL.
 
 
 (************ Same without tail calls ****************)
 
-definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
+definition RTL_ntc ≝ mk_graph_params (mk_unserialized_params
   (mk_step_params
     (* acc_a_reg ≝ *) register
@@ -137 +121 @@
       (* localsT ≝ *) register)).
 
-definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).
-
-definition rtlntc_internal_function ≝
-  λglobals. joint_internal_function … globals rtlntc_params.
-
-definition rtlntc_program ≝ joint_program rtlntc_params.
+definition rtl_ntc_program ≝ joint_program RTL_ntc.

src/RTLabs/RTLabsToRTL_paolo.ma

@@ -133 +133 @@
   ∀srcrs2 : list psd_argument.
   |dests| = |srcrs1| → |srcrs1| = |srcrs2| →
-  list (joint_seq rtl_params globals)
+  list (joint_seq RTL globals)
   ≝
   λglobals: list ident.
@@ -146 +146 @@
   | Sub ⇒ [CLEAR_CARRY ??]
   | _ ⇒ [ ]
-  ] @ map3 ???? (OP2 rtl_params globals op) destrs srcrs1 srcrs2 prf1 prf2.
+  ] @ map3 ???? (OP2 RTL globals op) destrs srcrs1 srcrs2 prf1 prf2.
 
 let rec nat_to_args (size : nat) (k : nat) on size : Σl : list psd_argument.|l| = size ≝
@@ -174 +174 @@
   ∀destrs: list register.
   |destrs| = size_of_cst ? cst_sig →
-  list (joint_seq rtl_params globals)
+  list (joint_seq RTL globals)
  ≝
   λty,globals,cst_sig,destrs.
@@ -186 +186 @@
   | Oaddrsymbol id offset ⇒ λcst_prf,prf.
     let 〈r1, r2〉 ≝ make_addr … destrs ? in
-    [ADDRESS rtl_params globals id ? r1 r2]
+    [ADDRESS RTL globals id ? r1 r2]
   | Oaddrstack offset ⇒ λcst_prf,prf.
     let 〈r1, r2〉 ≝ make_addr … destrs ? in
-    [(rtl_stack_address r1 r2 : joint_seq rtl_params globals)]
+    [(rtl_stack_address r1 r2 : joint_seq RTL globals)]
   ] (pi2 … cst_sig).
   [2: cases not_implemented
@@ -203 +203 @@
   ∀destrs: list register.
   ∀srcrs: list psd_argument.
-  |destrs| = |srcrs| → list (joint_seq rtl_params globals) ≝ 
+  |destrs| = |srcrs| → list (joint_seq RTL globals) ≝ 
   λglobals,destrs,srcrs,length_eq.
   map2 … (λdst,src.dst ← src) destrs srcrs length_eq.
@@ -216 +216 @@
 
 definition sign_mask : ∀globals.register → register →
-  list (joint_seq rtl_params globals) ≝
+  list (joint_seq RTL globals) ≝
     (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that:
        byte in destr if srcr is: neg   |  pos
@@ -234 +234 @@
   ∀globals : list ident.
   list register → register →
-  bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
+  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
   λglobals,destrs,srcr.
   ν tmp in
@@ -242 +242 @@
 definition translate_fill_with_zero :
   ∀globals : list ident.
-  list register → list (joint_seq rtl_params globals) ≝
+  list register → list (joint_seq RTL globals) ≝
   λglobals,destrs.
   match nat_to_args (|destrs|) 0 with
@@ -270 +270 @@
   ∀globals: list ident.
   signedness → list register → list register →
-    bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
+    bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
   λglobals,src_sign,destrs,srcrs.
   match reduce_strong ?? destrs srcrs with
@@ -299 +299 @@
   ∀destrs : list register.
   ∀srcrs_arg : list register.
-  |destrs| = |srcrs_arg| → list (joint_seq rtl_params globals) ≝
+  |destrs| = |srcrs_arg| → list (joint_seq RTL globals) ≝
   λglobals, destrs, srcrs, prf.
-  map2 ??? (OP1 rtl_params globals Cmpl) destrs srcrs prf.
-
-definition translate_negint : ∀globals.? → ? → ? → bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
+  map2 ??? (OP1 RTL globals Cmpl) destrs srcrs prf.
+
+definition translate_negint : ∀globals.? → ? → ? → bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
   λglobals: list ident.
   λdestrs: list register.
@@ -318 +318 @@
   ∀globals : list ident.
   list register → list register →
-    bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
+    bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
   λglobals,destrs,srcrs.
   match destrs with
@@ -328 +328 @@
     | cons srcr srcrs' ⇒
       (destr ← srcr) :::
-      map register (joint_seq rtl_params globals) (λr. destr ← destr .Or. r) srcrs' @@
+      map register (joint_seq RTL globals) (λr. destr ← destr .Or. r) srcrs' @@
       (* now destr is non-null iff srcrs was non-null *)
       CLEAR_CARRY ?? :::
@@ -341 +341 @@
 
 definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? →
-  bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
+  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
   λglobals.
   λty, ty'.
@@ -351 +351 @@
   match op1
   return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' →
-    bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) with
+    bind_new (localsT RTL) (list (joint_seq RTL globals)) with
   [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2.
     translate_cast globals src_sign destrs srcrs
@@ -410 +410 @@
   (Σi.i<S k) →
   (* the accumulator *)
-  list (joint_seq rtl_params globals) →
-    list (joint_seq rtl_params globals) ≝
+  list (joint_seq RTL globals) →
+    list (joint_seq RTL globals) ≝
   λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2,
     tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc.
@@ -456 +456 @@
 ] qed.
 
-definition translate_mul : ∀globals.?→?→?→?→?→bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
+definition translate_mul : ∀globals.?→?→?→?→?→bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
 λglobals : list ident.
 λdestrs : list register.
@@ -472 +472 @@
 (* the step calculating all products with least significant byte going in the
    k-th position of the result *)
-let translate_mul_k : (Σk.k<|destrs|) → list (joint_seq rtl_params globals) →
-  list (joint_seq rtl_params globals) ≝
+let translate_mul_k : (Σk.k<|destrs|) → list (joint_seq RTL globals) →
+  list (joint_seq RTL globals) ≝
   λk_sig,acc.match k_sig with
   [ mk_Sig k k_prf ⇒
@@ -496 +496 @@
 
 definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→
-    bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
+    bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
   λglobals: list ident.
   λdiv_not_mod: bool.
@@ -543 +543 @@
 
 definition translate_ne: ∀globals: list ident.?→?→?→?→
-  bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
+  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
   λglobals: list ident.
   λdestrs: list register.
@@ -559 +559 @@
       | cons srcr2 srcrs2' ⇒ λEQ.
         νtmpr in
-        let f : psd_argument → psd_argument → list (joint_seq rtl_params globals) → list (joint_seq rtl_params globals) ≝
+        let f : psd_argument → psd_argument → list (joint_seq RTL globals) → list (joint_seq RTL globals) ≝
           λs1,s2,acc.
           tmpr  ← s1 .Xor. s2 ::
           destr ← destr .Or. tmpr ::
           acc in
-        let epilogue : list (joint_seq rtl_params globals) ≝
+        let epilogue : list (joint_seq RTL globals) ≝
           [ CLEAR_CARRY ?? ;
             tmpr ← zero_byte .Sub. destr ;
@@ -577 +577 @@
 (* if destrs is 0 or 1, it inverses it. To be used after operations that
    ensure this. *)
-definition translate_toggle_bool : ∀globals.?→list (joint_seq rtl_params globals) ≝
+definition translate_toggle_bool : ∀globals.?→list (joint_seq RTL globals) ≝
   λglobals: list ident.
   λdestrs: list register.
@@ -591 +591 @@
   ∀srcrs2: list psd_argument.
   |srcrs1| = |srcrs2| →
-  bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
+  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
   λglobals,destrs,srcrs1,srcrs2,srcrs_prf.
   match destrs with
@@ -609 +609 @@
   (tmp : register)
   (srcrs : list psd_argument) on srcrs :
-  Σt : (list psd_argument) × (list (joint_seq rtl_params globals)).|\fst t| = |srcrs| ≝
+  Σt : (list psd_argument) × (list (joint_seq RTL globals)).|\fst t| = |srcrs| ≝
   let byte_128 : Byte ≝ true ::: bv_zero ? in
   match srcrs with
@@ -631 +631 @@
   ∀srcrs2: list psd_argument.
   |srcrs1| = |srcrs2| →
-  bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
+  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
   λglobals,destrs,srcrs1,srcrs2,srcrs_prf.
   νtmp_last_s1 in
@@ -649 +649 @@
 qed.
 
-definition translate_lt : bool→∀globals.?→?→?→?→bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
+definition translate_lt : bool→∀globals.?→?→?→?→bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
   λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs_prf.
   if is_unsigned then
@@ -684 +684 @@
   |srcrs1| = size_of_sig_type ty1 →
   |srcrs2| = size_of_sig_type ty2 →
-  bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
+  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
   λglobals,ty1,ty2,ty3,op2,destrs,srcrs1,srcrs2.
   match op2 return λty1,ty2,ty3.λx : binary_operation ty1 ty2 ty3.
@@ -728 +728 @@
 
 definition translate_cond: ∀globals: list ident. list register → label →
-  bind_seq_block rtl_params globals (joint_step rtl_params globals) ≝
+  bind_seq_block RTL globals (joint_step RTL globals) ≝
   λglobals: list ident.
   λsrcrs: list register.
   λlbl_true: label.
-  match srcrs return λ_.bind_seq_block rtl_params ? (joint_step ??) with
+  match srcrs return λ_.bind_seq_block RTL ? (joint_step ??) with
   [ nil ⇒ bret … 〈[ ], NOOP ??〉
   | cons srcr srcrs' ⇒
     ν tmpr in
-    let f : register → joint_seq rtl_params globals ≝
+    let f : register → joint_seq RTL globals ≝
       λr. tmpr ← tmpr .Or. r in 
-    bret … 〈MOVE rtl_params globals 〈tmpr,srcr〉 ::
+    bret … 〈MOVE RTL globals 〈tmpr,srcr〉 ::
     map ?? f srcrs', (COND … tmpr lbl_true : joint_step ??) 〉
   ].
 
 (* Paolo: to be controlled (original seemed overly complex) *)
-definition translate_load : ∀globals.?→?→?→bind_new (localsT rtl_params) ? ≝
+definition translate_load : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝
   λglobals: list ident.
   λaddr : list psd_argument.
@@ -750 +750 @@
   ν tmp_addr_l in
   ν tmp_addr_h in
-  let f ≝ λdestr : register.λacc : list (joint_seq rtl_params globals).
-    LOAD rtl_params globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) ::
+  let f ≝ λdestr : register.λacc : list (joint_seq RTL globals).
+    LOAD RTL globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) ::
     translate_op ? Add
       [tmp_addr_l ; tmp_addr_h]
@@ -761 +761 @@
 ] // qed.
   
-definition translate_store : ∀globals.?→?→?→bind_new (localsT rtl_params) ? ≝
+definition translate_store : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝
   λglobals: list ident.
   λaddr : list psd_argument.
@@ -768 +768 @@
   ν tmp_addr_l in
   ν tmp_addr_h in
-  let f ≝ λsrcr : psd_argument.λacc : list (joint_seq rtl_params globals).
-    STORE rtl_params globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr ::
+  let f ≝ λsrcr : psd_argument.λacc : list (joint_seq RTL globals).
+    STORE RTL globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr ::
     translate_op … Add
       [tmp_addr_l ; tmp_addr_h]
@@ -780 +780 @@
 definition translate_statement : ∀globals.local_env → statement →
   𝚺b :
-  bind_seq_block rtl_params globals (joint_step rtl_params globals) +
-  bind_seq_block rtl_params globals (joint_fin_step rtl_params).
+  bind_seq_block RTL globals (joint_step RTL globals) +
+  bind_seq_block RTL globals (joint_fin_step RTL).
   if is_inl … b then label else unit ≝
   λglobals,lenv,stmt.
@@ -812 +812 @@
     ❬(match retr with
       [ Some retr ⇒
-        CALL_ID rtl_params ? f (rtl_args args lenv ?) (find_local_env retr lenv ?)
+        CALL_ID RTL ? f (rtl_args args lenv ?) (find_local_env retr lenv ?)
       | None ⇒
-        CALL_ID rtl_params ? f (rtl_args args lenv ?) [ ]
+        CALL_ID RTL ? f (rtl_args args lenv ?) [ ]
       ] : bind_seq_block ???), lbl'❭
   | St_call_ptr f args retr lbl' ⇒
@@ -882 +882 @@
   let entry' ≝ f_entry def in
   let exit' ≝ f_exit def in
-  let graph' ≝ empty_map LabelTag (joint_statement rtl_params globals) in
+  let graph' ≝ empty_map LabelTag (joint_statement RTL globals) in
   let graph' ≝ add LabelTag ? graph' entry'
     (GOTO … exit') in 
@@ -891 +891 @@
     b_adds_graph … (rtl_ertl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in
   let res ≝
-    mk_joint_internal_function globals rtl_params luniverse' runiverse' result' params'
+    mk_joint_internal_function RTL globals luniverse' runiverse' result' params'
      locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in
     foldi … f_trans (f_graph def) res.  

src/joint/Joint_paolo.ma

@@ -472 +472 @@
   (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))).
 
-record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝
+record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
 { joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
   joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
@@ -489 +489 @@
 
 definition joint_closed_internal_function ≝
-  λglobals,p.
+  λp,globals.
     Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
 
@@ -495 +495 @@
   λglobals: list ident.
   λpars: params.
-  λint_fun: joint_internal_function globals pars.
+  λint_fun: joint_internal_function pars globals.
   λgraph: codeT pars globals.
   λentry.
   λexit.
-    mk_joint_internal_function globals pars
+    mk_joint_internal_function pars globals
       (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
       (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
@@ -507 +507 @@
   λglobals.λpars : graph_params.
   λgraph.
-  λp:joint_internal_function globals pars.
+  λp:joint_internal_function pars globals.
   λentry_prf.
   λexit_prf.
@@ -536 +536 @@
 definition add_graph ≝
   λg_pars : graph_params.λglobals.λl:label.λstmt.
-    λp:joint_internal_function globals g_pars.
+    λp:joint_internal_function g_pars globals.
    let code ≝ add … (joint_if_code … p) l stmt in
-    mk_joint_internal_function ? g_pars
+    mk_joint_internal_function …
      (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
      (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
@@ -550 +550 @@
 
 definition set_locals ≝
-  λglobals,pars.
-  λp : joint_internal_function globals pars.
+  λpars,globals.
+  λp : joint_internal_function pars globals.
   λlocals.
-   mk_joint_internal_function globals pars
+   mk_joint_internal_function pars globals
     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
     (joint_if_params … p) locals (joint_if_stacksize … p)
@@ -561 +561 @@
 
 definition joint_program ≝
- λp:params. program (λglobals. joint_function globals p) nat.
+ λp:params. program (joint_function p) nat.

src/joint/TranslateUtils_paolo.ma

@@ -5 +5 @@
 (* type T is the syntactic type of the generated things *)
 (* (sig for RTLabs registers, unit in others ) *)
-definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function … g pars).
+definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function pars g).
 
 definition rtl_ertl_fresh_reg: 
@@ -39 +39 @@
   (globals: list ident)
   (insts: list (joint_seq g_pars globals))
-  (src : label) on insts : state_monad (joint_internal_function … g_pars) label ≝
+  (src : label) on insts : state_monad (joint_internal_function g_pars globals) label ≝
   match insts with
   [ nil ⇒ return src
@@ -49 +49 @@
   ].
 
+definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with
+  [ inl _ ⇒ true
+  | inr _ ⇒ false
+  ].
+definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with
+  [ inl _ ⇒ true
+  | inr _ ⇒ false
+  ].
+
 definition adds_graph :
   ∀g_pars : graph_params.
@@ -55 +64 @@
        seq_block g_pars globals (joint_fin_step g_pars).
   label → if is_inl … b then label else unit →
-  joint_internal_function … g_pars → joint_internal_function … g_pars ≝
+  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
   λg_pars,globals,insts,src.
   match insts return λx.if is_inl … x then ? else ? → ? → ? with
@@ -69 +78 @@
 definition insert_prologue ≝
   λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
-  λdef : joint_internal_function globals g_pars.
+  λdef : joint_internal_function g_pars globals.
   let entry ≝ joint_if_entry … def in
   match stmt_at … entry
@@ -99 +108 @@
 definition insert_epilogue ≝
   λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
-  λdef : joint_internal_function globals g_pars.
+  λdef : joint_internal_function g_pars globals.
   let exit ≝ joint_if_exit … def in
   match stmt_at … exit
@@ -121 +130 @@
        bind_seq_block g_pars globals (joint_fin_step g_pars).
   label → if is_inl … b then label else unit →
-  joint_internal_function globals g_pars →
-  joint_internal_function globals g_pars ≝
+  joint_internal_function g_pars globals→
+  joint_internal_function g_pars globals ≝
   λg_pars,globals,fresh_r,insts,src.
   match insts return λx.if is_inl … x then ? else ? → ? → ? with
@@ -140 +149 @@
   freshT globals dst_g_pars (localsT dst_g_pars) →
   (* initialized function definition with empty graph *)
-  joint_internal_function globals dst_g_pars →
+  joint_internal_function dst_g_pars globals →
   (* functions dictating the translation *)
   (label → joint_step src_g_pars globals →
@@ -147 +156 @@
     bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
   (* source function *)
-  joint_internal_function globals src_g_pars →
+  joint_internal_function src_g_pars globals →
   (* destination function *)
-  joint_internal_function globals dst_g_pars ≝
+  joint_internal_function dst_g_pars globals ≝
   λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
   let f : label → joint_statement (src_g_pars : params) globals →
-    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝ 
+    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ 
     λlbl,stmt,def.
     match stmt with
@@ -167 +176 @@
   ∀globals: list ident.
   (* initialized function definition with empty graph *)
-  joint_internal_function … dst_g_pars →
+  joint_internal_function dst_g_pars globals →
   (* functions dictating the translation *)
   (label → joint_step src_g_pars globals →
@@ -174 +183 @@
     seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
   (* source function *)
-  joint_internal_function … src_g_pars →
+  joint_internal_function src_g_pars globals →
   (* destination function *)
-  joint_internal_function … dst_g_pars ≝ 
+  joint_internal_function dst_g_pars globals ≝ 
   λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
   let f : label → joint_statement (src_g_pars : params) globals →
-    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝ 
+    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝ 
     λlbl,stmt,def.
     match stmt with

src/joint/blocks.ma

@@ -2 +2 @@
 include "utilities/bindLists.ma".
 
-inductive block_step (p : stmt_params) (globals : list ident) : Type[0] ≝
+(* inductive block_step (p : stmt_params) (globals : list ident) : Type[0] ≝
   | block_seq : joint_seq p globals → block_step p globals
   | block_skip : label → block_step p globals.
@@ -40 +40 @@
 
 definition skip_block ≝ λp,globals,A.
-  (list (block_step p globals)) × A.
+  (list (block_step p globals)) × A.*)
 
 definition seq_block ≝ λp : stmt_params.λglobals,A.
   (list (joint_seq p globals)) × A.
 
-definition seq_to_skip_block :
+(*definition seq_to_skip_block :
   ∀p,g,A.seq_block p g A → skip_block p g A
  ≝ λp,g,A,b.〈\fst b, \snd b〉.
@@ -51 +51 @@
 coercion skip_from_seq_block :
   ∀p,g,A.∀b : seq_block p g A.skip_block p g A ≝
-  seq_to_skip_block on _b : seq_block ??? to skip_block ???.
+  seq_to_skip_block on _b : seq_block ??? to skip_block ???.*)
 
 definition bind_seq_block ≝ λp : stmt_params.λglobals,A.
@@ -70 +70 @@
 bind_seq_list p g ≡ bind_new R L.
 
-definition bind_skip_block ≝ λp : stmt_params.λglobals,A.
+(*definition bind_skip_block ≝ λp : stmt_params.λglobals,A.
   bind_new (localsT p) (skip_block p globals A).
 unification hint 0 ≔ p : stmt_params, g, A;
@@ -84 +84 @@
 coercion bind_skip_from_seq_block :
   ∀p,g,A.∀b:bind_seq_block p g A.bind_skip_block p g A ≝
-  bind_seq_to_skip_block on _b : bind_seq_block ??? to bind_skip_block ???.
+  bind_seq_to_skip_block on _b : bind_seq_block ??? to bind_skip_block ???.*)
 (*
 definition block_classifier ≝

src/joint/linearise.ma

@@ -652 +652 @@
   ∀p : unserialized_params.
   ∀globals.
-    joint_internal_function globals (mk_graph_params p) →
-    joint_internal_function globals (mk_lin_params p)
+    joint_internal_function (mk_graph_params p) globals →
+    joint_internal_function (mk_lin_params p) globals
      (* ∃sigma : identifier_map LabelTag ℕ. 
         let g ≝ joint_if_code ?? (pi1 … fin) in
@@ -670 +670 @@
                     (stmt_implicit_label … s)) (nth_opt … n c)*) ≝
   λp,globals,f_in.
-  mk_joint_internal_function globals (mk_lin_params p)
+  mk_joint_internal_function (mk_lin_params p) globals
    (joint_if_luniverse ?? f_in) (joint_if_runiverse ?? f_in)
    (joint_if_result ?? f_in) (joint_if_params ?? f_in) (joint_if_locals ?? f_in)

src/joint/semanticsUtils_paolo.ma

@@ -124 +124 @@
 definition make_sem_graph_params :
   ∀pars : graph_params.
-  ∀g_pars : more_sem_genv_params pars.
+  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
   sem_params ≝
   λpars,g_pars.
@@ -163 +163 @@
 definition make_sem_lin_params :
   ∀pars : lin_params.
-  ∀g_pars : more_sem_genv_params pars.
+  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
   sem_params ≝
   λpars,g_pars.

src/joint/semantics_paolo.ma

@@ -12 +12 @@
    only the head is kept (or Undef if the list is empty) ??? *)
 
-definition genv ≝ λglobals.λp:params. genv_t (joint_function globals p).
+definition genv ≝ λp:params.λglobals.genv_t (joint_function p globals).
 definition cpointer ≝ Σp.ptype p = Code.
 definition xpointer ≝ Σp.ptype p = XData.
@@ -68 +68 @@
  ∀pars : params.
  ∀globals.
-  genv globals pars →
+  genv pars globals →
   block →
-  res (joint_internal_function … pars) ≝
-  λpars,blobals,ge,b.
+  res (joint_internal_function pars globals) ≝
+  λpars,globals,ge,b.
   do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
   match def with
@@ -81 +81 @@
  ∀pars : params.
  ∀globals.
-  genv globals pars →
+  genv pars globals →
   cpointer →
-  res (joint_internal_function … pars) ≝
+  res (joint_internal_function pars globals) ≝
  λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
 
-inductive step_flow (p : params) (globals : list ident) : possible_flows → Type[0] ≝
-  | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p globals (Labels lbls) (* used for goto-like flow alteration *)
-  | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals Call (* call a function with given id, then proceed *)
-  | Proceed  : ∀flows.step_flow p globals flows. (* go to implicit successor *)
-
-(*
-definition step_flow_cons : ∀p,globals,l,lbls.
-  step_flow p globals lbls → step_flow p globals (l :: lbls) ≝
-  λp,globals,l1,l2,flow.match flow with
-  [ Redirect l ⇒ Redirect … «l, ?»
-  | Init id f args dest ⇒ Init … id f args dest
-  | Proceed ⇒ Proceed ???
-  ]. cases l /2 by or_intror/ qed.
-coercion step_flow_c : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1::l2) ≝
-  step_flow_cons on _flow : step_flow ??? to step_flow ?? (cons ???).
-
-definition step_flow_append_l : ∀p,globals,l1,l2.
-  step_flow p globals l1 → step_flow p globals (l1 @ l2) ≝
-  λp,globals,l1,l2,flow.match flow with
-  [ Redirect l ⇒ Redirect … «l, ?»
-  | Init id f args dest ⇒ Init … id f args dest
-  | Proceed ⇒ Proceed ???
-  ]. cases l /2 by Exists_append_l/ qed.
-coercion step_flow_l : ∀p,globals,l1,l2.∀flow : step_flow p globals l1.step_flow p globals (l1@l2) ≝
-  step_flow_append_l on _flow : step_flow ??? to step_flow ?? (append ???).
-
-definition step_flow_append_r : ∀p,globals,l1,l2.
-  step_flow p globals l2 → step_flow p globals (l1 @ l2) ≝
-  λp,globals,l1,l2,flow.match flow with
-  [ Redirect l ⇒ Redirect … «l, ?»
-  | Init id f args dest ⇒ Init … id f args dest
-  | Proceed ⇒ Proceed ???
-  ]. cases l /2 by Exists_append_r/ qed.
-coercion step_flow_r : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1@l2) ≝
-  step_flow_append_r on _flow : step_flow ??? to step_flow ?? (append ???).
-*)
-
-inductive fin_step_flow (p : params) (globals : list ident) : possible_flows → Type[0] ≝
-  | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p globals (Labels lbls)
-  | FTailInit : Z → joint_internal_function globals p → call_args p → fin_step_flow p globals Call
-  | FEnd1  : fin_step_flow p globals (Labels [ ]) (* end flow *)
-  | FEnd2  : fin_step_flow p globals Call. (* end flow *)
-
-(*
-definition fin_step_flow_cons : ∀p,globals,l,lbls.
-  fin_step_flow p globals lbls → fin_step_flow p globals (l :: lbls) ≝
-  λp,globals,l1,l2,flow.match flow with
-  [ FRedirect l ⇒ FRedirect … «l, ?»
-  | FTailInit id f args ⇒ FTailInit … id f args
-  | FEnd ⇒ FEnd ???
-  ]. cases l /2 by or_intror/ qed.
-coercion fin_step_flow_c : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1::l2) ≝
-  fin_step_flow_cons on _flow : fin_step_flow ??? to fin_step_flow ?? (cons ???).
-
-definition fin_step_flow_append_l : ∀p,globals,l1,l2.
-  fin_step_flow p globals l1 → fin_step_flow p globals (l1@l2) ≝
-  λp,globals,l1,l2,flow.match flow with
-  [ FRedirect l ⇒ FRedirect … «l, ?»
-  | FTailInit id f args ⇒ FTailInit … id f args
-  | FEnd ⇒ FEnd ???
-  ]. cases l /2 by Exists_append_l/ qed.
-coercion fin_step_flow_l : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l1.fin_step_flow p globals (l1@l2) ≝
-  fin_step_flow_append_l on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???).
-
-definition fin_step_flow_append_r : ∀p,globals,l1,l2.
-  fin_step_flow p globals l2 → fin_step_flow p globals (l1@l2) ≝
-  λp,globals,l1,l2,flow.match flow with
-  [ FRedirect l ⇒ FRedirect … «l, ?»
-  | FTailInit id f args ⇒ FTailInit … id f args
-  | FEnd ⇒ FEnd ???
-  ]. cases l /2 by Exists_append_r/ qed.
-coercion fin_step_flow_r : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1@l2) ≝
-  fin_step_flow_append_r on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???).
-*)
-
-record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
-  { st_pars :> sem_state_params
+inductive step_flow (p : step_params) (F : Type[0]) : possible_flows → Type[0] ≝
+  | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *)
+  | Init     : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *)
+  | Proceed  : ∀flows.step_flow p F flows. (* go to implicit successor *)
+
+inductive fin_step_flow (p : step_params) (F : Type[0]) : possible_flows → Type[0] ≝
+  | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls)
+  | FTailInit : Z → F → call_args p → fin_step_flow p F Call
+  | FEnd1  : fin_step_flow p F (Labels [ ]) (* end flow *)
+  | FEnd2  : fin_step_flow p F Call. (* end flow *)
+
+record more_sem_unserialized_params
+  (uns_pars : unserialized_params)
+  (F : list ident → Type[0]) : Type[1] ≝
+  { st_pars :> sem_state_params (* automatic coercion has issues *)
   ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
   ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
@@ -181 +119 @@
   ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
   (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
-  ; save_frame: cpointer → call_dest uns_pars → state st_pars → framesT st_pars
+  ; save_frame: cpointer → call_dest uns_pars → state st_pars → res (state st_pars)
    (*CSC: setup_call returns a res only because we can call a function with the wrong number and
      type of arguments. To be fixed using a dependent type *)
@@ -191 +129 @@
   ; call_args_for_main: call_args uns_pars
   ; call_dest_for_main: call_dest uns_pars
- }.
+
+  (* from now on, parameters that use the type of functions *)
+  ; read_result: ∀globals.genv_t (fundef (F globals)) → state st_pars → res (list beval)
+  (* change of pc must be left to *_flow execution *)
+  ; eval_ext_seq: ∀globals.genv_t (fundef (F globals)) → ext_seq uns_pars →
+      state st_pars → IO io_out io_in (state st_pars)
+  ; eval_ext_tailcall : ∀globals.genv_t (fundef (F globals)) → ext_tailcall uns_pars →
+      state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
+  ; eval_ext_call: ∀globals.genv_t (fundef (F globals)) → ∀s : ext_call uns_pars.
+      state st_pars →
+      IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars))
+  ; pop_frame: ∀globals.genv_t (fundef (F globals)) → state st_pars → res (state st_pars)
+  }.
+
+(*coercion msu_pars_to_ss_pars nocomposites :
+∀p,F.∀msup : more_sem_unserialized_params p F.sem_state_params
+ ≝ st_pars
+on _msup : more_sem_unserialized_params ?? to sem_state_params.*)
 
 
 definition helper_def_retrieve : 
-  ∀X : ? → ? → Type[0].
-  (∀up.∀p:more_sem_unserialized_params up. regsT p → X up p → res beval) →
-  ∀up.∀p : more_sem_unserialized_params up.state p → X up p → res beval ≝
-    λX,f,up,p,st.f ? p (regs … st).
+  ∀X : ? → ? → ? → Type[0].
+  (∀up,F.∀p:more_sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
+  ∀up,F.∀p : more_sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
+    λX,f,up,F,p,st.f ?? p (regs … st).
 
 definition helper_def_store :
-  ∀X : ? → ? → Type[0].
-  (∀up.∀p : more_sem_unserialized_params up.X up p → beval → regsT p → res (regsT p)) →
-  ∀up.∀p : more_sem_unserialized_params up.X up p → beval → state p → res (state p) ≝
-  λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return set_regs … r st.
+  ∀X : ? → ? → ? → Type[0].
+  (∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
+  ∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
+  λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st.
 
 definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
@@ -219 +174 @@
 definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
 definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
-definition pair_reg_move : ?→?→?→?→?  ≝
-  λup.λp : more_sem_unserialized_params up.λst : state p.λpm : pair_move up.
-    ! r ← pair_reg_move_ ? p (regs ? st) pm;
+definition pair_reg_move ≝
+  λup,F.λp : more_sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
+    ! r ← pair_reg_move_ ?? p (regs ? st) pm;
     return set_regs ? r st.
 
  
 axiom BadPointer : String.
- 
+
 (* this is preamble to all calls (including tail ones). The optional argument in
    input tells the function whether it has to save the frame for internal
@@ -235 +190 @@
    serialization and on whether the call is a tail one. *)
 definition eval_call_block:
- ∀globals.∀p : params.∀p':more_sem_unserialized_params p.
-  genv globals p → state p' → block → call_args p → call_dest p →
-    IO io_out io_in ((step_flow p globals Call)×(state p')) ≝
- λglobals,p,p',ge,st,b,args,dest.
-  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge b) : IO ? io_in ?); 
+ ∀p,F.∀p':more_sem_unserialized_params p F.∀globals.
+  genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p →
+    IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝
+ λp,F,p',globals,ge,st,b,args,dest.
+  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?); 
     match fd with
-    [ Internal fn ⇒
-      return 〈Init … (block_id b) fn args dest, st〉
+    [ Internal fd ⇒
+      return 〈Init ?? (block_id b) fd args dest, st〉
     | External fn ⇒
       ! params ← fetch_external_args … p' fn st : IO ???;
@@ -289 +244 @@
   return 〈st'', pr〉.
 
-(* parameters that need full params to have type of functions,
-   but are still independent of serialization *)
-record more_sem_genv_params (pp : params) : Type[1] ≝
-  { msu_pars :> more_sem_unserialized_params pp
-  ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
-  (* change of pc must be left to *_flow execution *)
-  ; eval_ext_seq: ∀globals.genv globals pp → ext_seq pp →
-      state msu_pars → IO io_out io_in (state msu_pars)
-  ; eval_ext_tailcall : ∀globals.genv globals pp → ext_tailcall pp →
-      state msu_pars → IO io_out io_in ((fin_step_flow pp globals Call)×(state msu_pars))
-  ; eval_ext_call: ∀globals.genv globals pp →∀s : ext_call pp.
-      state msu_pars →
-      IO io_out io_in ((step_flow pp globals Call)×(state msu_pars))
-  ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
-  }.
-
 (* parameters that are defined by serialization *)
 record more_sem_params (pp : params) : Type[1] ≝
-  { msg_pars :> more_sem_genv_params pp
+  { msu_pars :> more_sem_unserialized_params pp (joint_internal_function pp)
   ; offset_of_point : code_point pp → option offset (* can overflow *)
   ; point_of_offset : offset → code_point pp
@@ -315 +254 @@
     ∀o.offset_of_point (point_of_offset o) = Some ? o
   }.
+
+(*
+coercion ms_pars_to_msu_pars nocomposites :
+∀p : params.∀msp : more_sem_params p.more_sem_unserialized_params p (λglobals.joint_internal_function globals p)
+ ≝ msu_pars
+on _msp : more_sem_params ? to more_sem_unserialized_params ??.
+
+definition ss_pars_of_ms_pars ≝
+  λp.λpp : more_sem_params p.
+  st_pars … (msu_pars … pp).
+coercion ms_pars_to_ss_pars nocomposites :
+∀p : params.∀msp : more_sem_params p.sem_state_params ≝
+ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*)
 
 axiom CodePointerOverflow : String.
@@ -374 +326 @@
 
 definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
-  genv globals p → cpointer → res (joint_statement p globals) ≝
+  genv p globals → cpointer → res (joint_statement p globals) ≝
   λp,msp,globals,ge,ptr.
   let pt ≝ point_of_pointer ? msp ptr in
@@ -381 +333 @@
   
 definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
-  genv globals p → cpointer → label → res cpointer ≝
+  genv p globals → cpointer → label → res cpointer ≝
   λp,msp,globals,ge,ptr,lbl.
   ! fn ← fetch_function … ge ptr ;
@@ -399 +351 @@
   }.
 
+(* definition msu_pars_of_s_pars :
+∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p))
+≝ λp : sem_params.
+  msu_pars … (more_sem_pars p).
+coercion s_pars_to_msu_pars nocomposites :
+∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝
+msu_pars_of_s_pars
+on p : sem_params to more_sem_unserialized_params ??.
+
+definition ss_pars_of_s_pars :
+∀p : sem_params.sem_state_params
+≝ λp : sem_params.
+  st_pars … (msu_pars … (more_sem_pars p)).
+coercion s_pars_to_ss_pars nocomposites :
+∀p : sem_params.sem_state_params ≝
+ss_pars_of_s_pars
+on _p : sem_params to sem_state_params.
+
+definition ms_pars_of_s_pars :
+∀p : sem_params.more_sem_params (spp p)
+≝ more_sem_pars.
+coercion s_pars_to_ms_pars nocomposites :
+∀p : sem_params.more_sem_params (spp p) ≝
+ms_pars_of_s_pars
+on p : sem_params to more_sem_params ?.*)
+
 (* definition address_of_label: ∀globals. ∀p:sem_params.
   genv globals p → pointer → label → res address ≝
@@ -405 +383 @@
   OK … (address_of_code_pointer newptr). *)
 
-definition goto: ∀globals. ∀p:sem_params.
-  genv globals p → label → state p → cpointer → res (state_pc p) ≝
+definition goto: ∀globals.∀p : sem_params.
+  genv p globals → label → state p → cpointer → res (state_pc p) ≝
  λglobals,p,ge,l,st,b.
   ! newpc ← pointer_of_label ? p … ge b l ;
@@ -427 +405 @@
 
 definition eval_seq_no_pc :
- ∀globals.∀p:sem_params. genv globals p → state p →
+ ∀globals.∀p:sem_params. genv p globals → state p →
   ∀s:joint_seq p globals.
   IO io_out io_in (state p) ≝
@@ -433 +411 @@
   match seq return λx.IO ??? with
   [ extension_seq c ⇒
-    eval_ext_seq ??? ge c st
+    eval_ext_seq … ge c st
   | LOAD dst addrl addrh ⇒
     ! vaddrh ← dph_arg_retrieve … st addrh ;
@@ -484 +462 @@
   | POP dst ⇒
     ! 〈st',v〉 ← pop p st;
-    acca_store p p dst v st'
+    acca_store … p dst v st'
   | PUSH src ⇒
     ! v ← acca_arg_retrieve … st src;
@@ -495 +473 @@
     return st'
   | extension_call s ⇒
-    !〈flow, st'〉 ← eval_ext_call ??? ge s st ;
+    !〈flow, st'〉 ← eval_ext_call … ge s st ;
     return st'
   | _ ⇒ return st
@@ -504 +482 @@
 
 definition eval_seq_pc :
- ∀globals.∀p:sem_params. genv globals p → state p →
+ ∀globals.∀p:sem_params. genv p globals → state p →
   ∀s:joint_seq p globals.
-  IO io_out io_in (step_flow p globals (step_flows … s)) ≝
+  IO io_out io_in (step_flow p ? (step_flows … s)) ≝
   λg,p,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
   [ CALL_ID id args dest ⇒
@@ -513 +491 @@
     return flow
   | extension_call s ⇒
-    !〈flow, st'〉 ← eval_ext_call ??? ge s st ;
+    !〈flow, st'〉 ← eval_ext_call … ge s st ;
     return flow
   | _ ⇒ return Proceed ???
@@ -519 +497 @@
 
 definition eval_step :
- ∀globals.∀p:sem_params. genv globals p → state p →
+ ∀globals.∀p:sem_params. genv p globals → state p →
   ∀s:joint_step p globals.
-  IO io_out io_in ((step_flow p globals (step_flows … s))×(state p)) ≝
+  IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝
   λglobals,p,ge,st,s.
   match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with
@@ -538 +516 @@
   %1 % qed.
 
-definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv globals p →
+definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv p globals →
   state p → ∀s : joint_fin_step p.
   IO io_out io_in (state p) ≝
@@ -544 +522 @@
   match s return λx.IO ??? with
     [ tailcall c ⇒
-      !〈flow,st'〉 ← eval_ext_tailcall ??? ge c st ;
+      !〈flow,st'〉 ← eval_ext_tailcall … ge c st ;
       return st'
     | _ ⇒ return st
@@ -550 +528 @@
 
 definition eval_fin_step_pc :
- ∀globals.∀p:sem_params. genv globals p → state p →
+ ∀globals.∀p:sem_params. genv p globals → state p →
   ∀s:joint_fin_step p.
-  IO io_out io_in (fin_step_flow p globals (fin_step_flows … s)) ≝
+  IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
   λg,p,ge,st,s.
   match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
   [ tailcall c ⇒
-    !〈flow,st'〉 ← eval_ext_tailcall ??? ge c st ;
+    !〈flow,st'〉 ← eval_ext_tailcall … ge c st ;
     return flow  
   | GOTO l ⇒ return FRedirect … l
@@ -562 +540 @@
   ]. %1 % qed.
 
-definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p →
-  state p → Z → joint_internal_function globals p → call_args p →
+definition do_call : ∀globals: list ident.∀p:sem_params. genv p globals →
+  state p → Z → joint_internal_function p globals → call_args p →
   res (state_pc p) ≝
   λglobals,p,ge,st,id,fn,args.
     ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
               args st ;
-    let regs ≝ foldr ?? (allocate_local p p) (regs … st) (joint_if_locals … fn) in
+    let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in
     let l' ≝ joint_if_entry … fn in
     let st' ≝ set_regs p regs st in
@@ -577 +555 @@
 (* The pointer provided is the one to the *next* instruction. *)
 definition eval_step_flow :
- ∀globals.∀p:sem_params.∀flows.genv globals p →
- state p → cpointer → step_flow p globals flows → res (state_pc p) ≝
+ ∀globals.∀p:sem_params.∀flows.genv p globals →
+ state p → cpointer → step_flow p ? flows → res (state_pc p) ≝
  λglobals,p,flows,ge,st,nxt,cmd.
  match cmd with
@@ -584 +562 @@
     goto … ge l st nxt
   | Init id fn args dest ⇒
-    let st' ≝ set_frms … (save_frame … nxt dest st) st in
+    ! st' ← save_frame … nxt dest st ;
     do_call ?? ge st' id fn args
   | Proceed _ ⇒
@@ -590 +568 @@
   ].
 
-definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀flows. genv globals p →
-  state p → cpointer → fin_step_flow p globals flows → res (state_pc p) ≝
+definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀flows. genv p globals →
+  state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝
   λglobals,p,lbls,ge,st,curr,cmd.
   match cmd with
@@ -604 +582 @@
 
 definition eval_statement :
- ∀globals.∀p:sem_params.genv globals p →
+ ∀globals.∀p:sem_params.genv p globals →
   state_pc p → joint_statement p globals →
     IO io_out io_in (state_pc p) ≝
@@ -619 +597 @@
  ].
 
-definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →
+definition eval_state : ∀globals: list ident.∀p:sem_params. genv p globals →
   state_pc p → IO io_out io_in (state_pc p) ≝
   λglobals,p,ge,st.
@@ -629 +607 @@
   not static... *)
 definition is_final: ∀globals:list ident. ∀p: sem_params.
-  genv globals p → cpointer → state_pc p → option int ≝
+  genv p globals → cpointer → state_pc p → option int ≝
  λglobals,p,ge,exit,st.res_to_opt ? (
   do s ← fetch_statement ? p … ge (pc … st);