Changeset 2214


Ignore:
Timestamp:
Jul 19, 2012, 2:42:02 PM (5 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:
16 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL_paolo.ma

    r2208 r2214  
     1
    12include "LTL/LTL_paolo.ma".
    23include "ERTL/Interference_paolo.ma".
     
    1819coercion Reg_to_arg_dec : ∀r:Register.arg_decision ≝ arg_decision_colour on _r : Register to arg_decision.
    1920
    20 definition stacksize :
    21   ∀globals.ℕ → joint_internal_function globals ertl_params → ℕ ≝
    22   λglobals.
    23   λspilled_no.
    24   λint_fun.
    25   spilled_no + joint_if_stacksize … int_fun.
    26 
    2721(* Paolo: I'm changing the following: before, spilled registers were
    2822  assigned stack addresses going from SP + #frame_size - #stack_params
     
    3125
    3226definition preserve_carry_bit :
    33   ∀globals.bool → list (joint_seq ltl_params globals) → list (joint_seq ltl_params globals) ≝
     27  ∀globals.bool → list (joint_seq LTL globals) → list (joint_seq LTL globals) ≝
    3428  λglobals,do_it,steps.
    3529  if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps.
     
    4236(* spill should be byte-based from the start *)
    4337definition set_dp_by_offset :
    44   ∀globals.nat → list (joint_seq ltl_params globals) ≝
     38  ∀globals.nat → list (joint_seq LTL globals) ≝
    4539  λglobals,off.
    4640  [ A ← byte_of_nat off
     
    5347
    5448definition get_stack:
    55  ∀globals.Register → nat → list (joint_seq ltl_params globals) ≝
     49 ∀globals.Register → nat → list (joint_seq LTL globals) ≝
    5650 λglobals,r,off.
    5751 set_dp_by_offset ? off @
     
    6054
    6155definition set_stack_not_a :
    62  ∀globals.nat → Register → list (joint_seq ltl_params globals) ≝
     56 ∀globals.nat → Register → list (joint_seq LTL globals) ≝
    6357 λglobals,off,r.
    6458 set_dp_by_offset ? off @
     
    6761
    6862definition set_stack_a :
    69  ∀globals.nat → list (joint_seq ltl_params globals) ≝
     63 ∀globals.nat → list (joint_seq LTL globals) ≝
    7064 λglobals,off.
    7165 [ RegisterST1 ← A ] @
     
    7367
    7468definition set_stack :
    75  ∀globals.nat → Register → list (joint_seq ltl_params globals) ≝
     69 ∀globals.nat → Register → list (joint_seq LTL globals) ≝
    7670 λglobals,off,r.
    7771 if eq_Register r RegisterA then
     
    8175 
    8276definition set_stack_int :
    83   ∀globals.nat → beval →  list (joint_seq ltl_params globals) ≝
     77  ∀globals.nat → beval →  list (joint_seq LTL globals) ≝
    8478  λglobals,off,int.
    8579  set_dp_by_offset ? off @
     
    8882
    8983definition move :
    90   ∀globals.bool → decision → arg_decision → list (joint_seq ltl_params globals) ≝
     84  ∀globals.bool → decision → arg_decision → list (joint_seq LTL globals) ≝
    9185  λglobals,carry_lives_after,dst,src.
    9286  match dst with
     
    128122
    129123definition newframe :
    130   ∀globals.ℕ → list (joint_seq ltl_params globals) ≝
     124  ∀globals.ℕ → list (joint_seq LTL globals) ≝
    131125  λglobals,stack_sz.
    132126  [ CLEAR_CARRY …
     
    140134
    141135definition delframe :
    142   ∀globals.ℕ → list (joint_seq ltl_params globals) ≝
     136  ∀globals.ℕ → list (joint_seq LTL globals) ≝
    143137  λglobals,stack_sz.
    144138  [ A ← RegisterSPL
     
    176170
    177171definition translate_op2 :
    178   ∀globals.bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
     172  ∀globals.bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    179173  λglobals,carry_lives_after,op,dst,arg1,arg2.
    180174  (* this won't preserve the carry bit if op does not set it: left to next function *)
     
    189183
    190184definition translate_op2_smart :
    191   ∀globals.bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
     185  ∀globals.bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    192186  λglobals,carry_lives_after,op,dst,arg1,arg2.
    193187  (* if op does not set carry bit (⇒ it does not use it either) then it must be
     
    232226
    233227definition translate_op1 :
    234   ∀globals.bool → Op1 → decision → decision → list (joint_seq ltl_params globals) ≝
     228  ∀globals.bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝
    235229  λglobals,carry_lives_after,op,dst,arg.
    236230  let preserve_carry ≝ carry_lives_after ∧ (is_spilled dst ∨ is_spilled arg) in
     
    241235
    242236definition translate_opaccs :
    243   ∀globals.bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
     237  ∀globals.bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    244238  λglobals,carry_lives_after,op,dst1,dst2,arg1,arg2.
    245239  (* OPACCS always has dead carry bit and sets it to zero *)
     
    255249(* does not preserve carry bit *)
    256250definition move_to_dp :
    257   ∀globals.arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
     251  ∀globals.arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    258252  λglobals,arg1,arg2.
    259253  if ¬arg_is_spilled arg1 then
     
    272266
    273267definition translate_store : 
    274   ∀globals.bool → arg_decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
     268  ∀globals.bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    275269  λglobals,carry_lives_after,addr1,addr2,src.
    276270  (* requires src != RegisterA and RegisterB *)
     
    286280
    287281definition translate_load : 
    288   ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
     282  ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    289283  λglobals,carry_lives_after,dst,addr1,addr2.
    290284  preserve_carry_bit ? (carry_lives_after ∧
     
    296290definition translate_address :
    297291  ∀globals.bool → ∀i.member i (eq_identifier ?) globals → decision → decision →
    298   list (joint_seq ltl_params globals) ≝
     292  list (joint_seq LTL globals) ≝
    299293  λglobals,carry_lives_after,id,prf,addr1,addr2.
    300294  preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2))
    301     (ADDRESS ltl_params ? id prf it it ::
     295    (ADDRESS LTL ? id prf it it ::
    302296     move ? false addr1 RegisterDPL @
    303297     move ? false addr2 RegisterDPH).
     
    306300  ∀globals.∀after : valuation register_lattice.
    307301  coloured_graph after →
    308   ℕ → label → joint_step ertl_params globals → seq_block ltl_params globals (joint_step ltl_params globals) ≝
     302  ℕ → label → joint_step ERTL globals → seq_block LTL globals (joint_step LTL globals) ≝
    309303  λglobals,after,grph,stack_sz,lbl,s.
    310304  let lookup ≝ λr.colouring … grph (inl … r) in
     
    317311  match s with
    318312  [ step_seq s' ⇒
    319     match s' return λ_.seq_block ltl_params globals (joint_step ltl_params globals) with
     313    match s' return λ_.seq_block LTL globals (joint_step LTL globals) with
    320314    [ COMMENT c ⇒ COMMENT … c
    321315    | COST_LABEL cost_lbl ⇒ COST_LABEL … cost_lbl
     
    373367        move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
    374368      ]
    375     | CALL_ID f n_args _ ⇒ CALL_ID ltl_params ? f n_args it
     369    | CALL_ID f n_args _ ⇒ CALL_ID LTL ? f n_args it
    376370    | extension_call abs ⇒ match abs in void with [ ]
    377371    ]
     
    381375
    382376definition translate_fin_step:
    383   ∀globals.label → joint_fin_step ertl_params → seq_block ltl_params globals (joint_fin_step ltl_params) ≝
     377  ∀globals.label → joint_fin_step ERTL → seq_block LTL globals (joint_fin_step LTL) ≝
    384378  λglobals,lbl,s.
    385   match s return λ_.seq_block ltl_params globals (joint_fin_step ltl_params) with
     379  match s return λ_.seq_block LTL globals (joint_fin_step LTL) with
    386380  [ RETURN ⇒ RETURN ?
    387381  | GOTO l ⇒ GOTO ? l
     
    390384
    391385definition translate_internal: ∀globals: list ident.
    392   joint_internal_function globals ertl_params →
    393   joint_internal_function globals ltl_params ≝
     386  joint_internal_function ERTL globals →
     387  joint_internal_function LTL globals ≝
    394388  λglobals: list ident.
    395   λint_fun: joint_internal_function globals ertl_params.
     389  λint_fun: joint_internal_function ERTL globals.
    396390  (* initialize graph *)
    397391  let entry ≝ pi1 … (joint_if_entry … int_fun) in
     
    405399  let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
    406400  (* initialize internal function *)
    407   let init ≝ mk_joint_internal_function globals ltl_params
     401  let init ≝ mk_joint_internal_function LTL globals
    408402    (joint_if_luniverse … int_fun)
    409403    (joint_if_runiverse … int_fun)
  • src/ERTL/ERTL_paolo.ma

    r2208 r2214  
     1
    12include "joint/Joint_paolo.ma".
    23include "RTL/RTL_paolo.ma".
     
    4849      (* localsT ≝ *) register).
    4950
    50 definition ertl_params ≝ mk_graph_params ertl_uns_params.
    51 definition ertl_program ≝ joint_program ertl_params.
     51definition ERTL ≝ mk_graph_params ertl_uns_params.
     52definition ertl_program ≝ joint_program ERTL.
    5253
    5354interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)).
     
    5657unification hint 0 ≔
    5758(*---------------*) ⊢
    58 pair_move ertl_params ≡ move_dst × move_src.
     59pair_move ERTL ≡ move_dst × move_src.
    5960unification hint 0 ≔
    6061(*---------------*) ⊢
    61 acc_a_reg ertl_params ≡ register.
     62acc_a_reg ERTL ≡ register.
    6263unification hint 0 ≔
    6364(*---------------*) ⊢
    64 acc_b_reg ertl_params ≡ register.
     65acc_b_reg ERTL ≡ register.
    6566unification hint 0 ≔
    6667(*---------------*) ⊢
    67 acc_a_arg ertl_params ≡ psd_argument.
     68acc_a_arg ERTL ≡ psd_argument.
    6869unification hint 0 ≔
    6970(*---------------*) ⊢
    70 acc_b_arg ertl_params ≡ psd_argument.
     71acc_b_arg ERTL ≡ psd_argument.
    7172unification hint 0 ≔
    7273(*---------------*) ⊢
    73 dpl_reg ertl_params ≡ register.
     74dpl_reg ERTL ≡ register.
    7475unification hint 0 ≔
    7576(*---------------*) ⊢
    76 dph_reg ertl_params ≡ register.
     77dph_reg ERTL ≡ register.
    7778unification hint 0 ≔
    7879(*---------------*) ⊢
    79 dpl_arg ertl_params ≡ psd_argument.
     80dpl_arg ERTL ≡ psd_argument.
    8081unification hint 0 ≔
    8182(*---------------*) ⊢
    82 dph_arg ertl_params ≡ psd_argument.
     83dph_arg ERTL ≡ psd_argument.
    8384unification hint 0 ≔
    8485(*---------------*) ⊢
    85 snd_arg ertl_params ≡ psd_argument.
     86snd_arg ERTL ≡ psd_argument.
    8687unification hint 0 ≔
    8788(*---------------*) ⊢
    88 call_args ertl_params ≡ ℕ.
     89call_args ERTL ≡ ℕ.
    8990unification hint 0 ≔
    9091(*---------------*) ⊢
    91 call_dest ertl_params ≡ unit.
     92call_dest ERTL ≡ unit.
    9293
    9394unification hint 0 ≔
    9495(*---------------*) ⊢
    95 ext_seq ertl_params ≡ ertl_seq.
     96ext_seq ERTL ≡ ertl_seq.
    9697unification hint 0 ≔
    9798(*---------------*) ⊢
    98 ext_call ertl_params ≡ void.
     99ext_call ERTL ≡ void.
    99100unification hint 0 ≔
    100101(*---------------*) ⊢
    101 ext_tailcall ertl_params ≡ void.
     102ext_tailcall ERTL ≡ void.
    102103
    103 coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ertl_params
     104coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ERTL
    104105  psd_argument_from_reg
    105   on _r : register to snd_arg ertl_params.
    106 coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ertl_params
     106  on _r : register to snd_arg ERTL.
     107coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ERTL
    107108  psd_argument_from_byte
    108   on _b : Byte to snd_arg ertl_params.
     109  on _b : Byte to snd_arg ERTL.
    109110 
    110 definition ertl_seq_joint ≝ extension_seq ertl_params.
    111 coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ertl_params globals ≝ ertl_seq_joint
    112   on _s : ertl_seq to joint_seq ertl_params.
    113 
     111definition ertl_seq_joint ≝ extension_seq ERTL.
     112coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint
     113  on _s : ertl_seq to joint_seq ERTL.
  • src/ERTL/liveness_paolo.ma

    r2208 r2214  
     1
    12include "ASM/Util.ma".
    23include "ERTL/ERTL_paolo.ma".
     
    4243definition defined ≝
    4344  λglobals: list ident.
    44   λs: joint_statement ertl_params globals.
     45  λs: joint_statement ERTL globals.
    4546  match s with
    4647  [ sequential seq l ⇒
     
    100101definition used ≝
    101102  λglobals: list ident.
    102   λs: joint_statement ertl_params globals.
     103  λs: joint_statement ERTL globals.
    103104  match s with
    104105  [ sequential seq l ⇒
     
    155156  λglobals: list ident.
    156157  λl: register_lattice.
    157   λs: joint_statement ertl_params globals.
     158  λs: joint_statement ERTL globals.
    158159  let pliveafter ≝ \fst l in
    159160  let hliveafter ≝ \snd l in
     
    225226
    226227definition statement_semantics: ∀globals: list ident.
    227   joint_statement ertl_params globals → register_lattice → register_lattice ≝
     228  joint_statement ERTL globals → register_lattice → register_lattice ≝
    228229  λglobals.
    229230  λstmt.
     
    236237definition livebefore ≝
    237238  λglobals: list ident.
    238   λint_fun: joint_internal_function globals ertl_params.
     239  λint_fun: joint_internal_function ERTL globals.
    239240  λlabel.
    240241  λliveafter: valuation register_lattice.
     
    246247definition liveafter ≝
    247248   λglobals: list ident.
    248   λint_fun: joint_internal_function globals ertl_params.
     249  λint_fun: joint_internal_function ERTL globals.
    249250  λlabel.
    250251  λliveafter: valuation register_lattice.
  • src/LIN/LIN_paolo.ma

    r2182 r2214  
    11include "LIN/joint_LTL_LIN_paolo.ma".
    22
    3 definition lin_params ≝ mk_lin_params ltl_lin_params.
     3definition LIN ≝ mk_lin_params LTL_LIN.
    44
    55(* aid unification *)
    66unification hint 0 ≔
    77(*---------------*) ⊢
    8 acc_a_reg lin_params ≡ unit.
     8acc_a_reg LIN ≡ unit.
    99unification hint 0 ≔
    1010(*---------------*) ⊢
    11 acc_a_arg lin_params ≡ unit.
     11acc_a_arg LIN ≡ unit.
    1212unification hint 0 ≔
    1313(*---------------*) ⊢
    14 acc_b_reg lin_params ≡ unit.
     14acc_b_reg LIN ≡ unit.
    1515unification hint 0 ≔
    1616(*---------------*) ⊢
    17 acc_a_arg lin_params ≡ unit.
     17acc_a_arg LIN ≡ unit.
    1818unification hint 0 ≔
    1919(*---------------*) ⊢
    20 snd_arg lin_params ≡ ltl_argument.
     20snd_arg LIN ≡ hdw_argument.
    2121unification hint 0 ≔
    2222(*---------------*) ⊢
    23 ext_seq lin_params ≡ ltl_lin_seq.
     23ext_seq LIN ≡ ltl_lin_seq.
    2424unification hint 0 ≔
    2525(*---------------*) ⊢
    26 pair_move lin_params ≡ registers_move.
     26pair_move LIN ≡ registers_move.
    2727
    28 definition lin_program ≝ joint_program lin_params.
     28definition lin_program ≝ joint_program LIN.
  • src/LIN/joint_LTL_LIN_paolo.ma

    r2208 r2214  
    1212| RESTORE_CARRY : ltl_lin_seq.
    1313
    14 definition ltl_lin_params : unserialized_params ≝ mk_unserialized_params
     14definition LTL_LIN : unserialized_params ≝ mk_unserialized_params
    1515  (mk_step_params
    1616    (* acc_a_reg ≝ *) unit
  • src/LTL/LTL_paolo.ma

    r2208 r2214  
    11include "LIN/joint_LTL_LIN_paolo.ma".
    22
    3 definition ltl_params ≝ mk_graph_params ltl_lin_params.
     3definition LTL ≝ mk_graph_params LTL_LIN.
    44
    55(* aid unification *)
    66unification hint 0 ≔
    77(*---------------*) ⊢
    8 acc_a_reg ltl_params ≡ unit.
     8acc_a_reg LTL ≡ unit.
    99unification hint 0 ≔
    1010(*---------------*) ⊢
    11 acc_a_arg ltl_params ≡ unit.
     11acc_a_arg LTL ≡ unit.
    1212unification hint 0 ≔
    1313(*---------------*) ⊢
    14 acc_b_reg ltl_params ≡ unit.
     14acc_b_reg LTL ≡ unit.
    1515unification hint 0 ≔
    1616(*---------------*) ⊢
    17 acc_a_arg ltl_params ≡ unit.
     17acc_a_arg LTL ≡ unit.
    1818unification hint 0 ≔
    1919(*---------------*) ⊢
    20 snd_arg ltl_params ≡ hdw_argument.
     20snd_arg LTL ≡ hdw_argument.
    2121unification hint 0 ≔
    2222(*---------------*) ⊢
    23 ext_seq ltl_params ≡ ltl_lin_seq.
     23ext_seq LTL ≡ ltl_lin_seq.
    2424unification hint 0 ≔
    2525(*---------------*) ⊢
    26 pair_move ltl_params ≡ registers_move.
     26pair_move LTL ≡ registers_move.
    2727
    28 definition ltl_program ≝ joint_program ltl_params.
     28definition ltl_program ≝ joint_program LTL.
    2929
    30 coercion byte_to_ltl_argument : ∀b: Byte.snd_arg ltl_params
    31   hdw_argument_from_byte on _b : Byte to snd_arg ltl_params.
    32 coercion reg_to_ltl_argument : ∀r: Register.snd_arg ltl_params
    33   hdw_argument_from_reg on _r : Register to snd_arg ltl_params.
     30coercion byte_to_ltl_argument : ∀b: Byte.snd_arg LTL
     31  hdw_argument_from_byte on _b : Byte to snd_arg LTL.
     32coercion reg_to_ltl_argument : ∀r: Register.snd_arg LTL
     33  hdw_argument_from_reg on _r : Register to snd_arg LTL.
  • src/RTL/RTLTailcall_paolo.ma

    r2162 r2214  
    55  λexit: label.
    66  λlbl: label.
    7   λstmt: rtl_statement globals.
    8   λgraph: codeT rtlntc_params globals.
     7  λstmt: joint_statement RTL globals.
     8  λgraph: codeT RTL_ntc globals.
    99  match stmt with
    1010  [ final fin ⇒
     
    1313         match ext with
    1414          [ rtl_tailcall_id f args ⇒
    15               add … graph lbl (sequential … (CALL_ID rtlntc_params ? f args [ ]) exit)
     15              add … graph lbl (sequential … (CALL_ID RTL_ntc ? f args [ ]) exit)
    1616          | rtl_tailcall_ptr f1 f2 args ⇒
    17               add … graph lbl (sequential rtlntc_params ? (rtl_call_ptr f1 f2 args [ ] : ext_call rtlntc_params) exit)
     17              add … graph lbl (sequential RTL_ntc ? (rtl_call_ptr f1 f2 args [ ] : ext_call RTL_ntc) exit)
    1818          ]
    1919      | _ ⇒ graph ]
     
    2323  λglobals.
    2424  λexit: label.
    25   λgraph: codeT rtl_params globals.
     25  λgraph: codeT RTL globals.
    2626    foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).
    2727
    2828axiom simplify_graph_preserves_labels:
    2929  ∀globals.
    30   ∀g: codeT rtl_params globals.
     30  ∀g: codeT RTL globals.
    3131  ∀exit: label.
    3232  ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g.
     
    3434definition simplify_internal :
    3535 ∀globals.
    36   joint_internal_function globals rtl_params →
    37    joint_internal_function globals rtlntc_params
     36  joint_internal_function RTL globals →
     37   joint_internal_function RTL_ntc globals
    3838
    3939  λglobals,def.
     
    4848qed.
    4949
    50 definition tailcall_simplify : rtl_program → rtlntc_program ≝
     50definition tailcall_simplify : rtl_program → rtl_ntc_program ≝
    5151 λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)).
  • src/RTL/RTLToERTL_paolo.ma

    r2208 r2214  
    88
    99definition save_hdws :
    10   ∀globals.list (register×Register) → list (joint_seq ertl_params globals) ≝
     10  ∀globals.list (register×Register) → list (joint_seq ERTL globals) ≝
    1111 λglobals.
    1212  let save_hdws_internal ≝
     
    1515
    1616definition restore_hdws :
    17   ∀globals.list (psd_argument×Register) → list (joint_seq ertl_params globals) ≝
     17  ∀globals.list (psd_argument×Register) → list (joint_seq ERTL globals) ≝
    1818  λglobals.
    1919   let restore_hdws_internal ≝
     
    2222
    2323definition get_params_hdw :
    24   ∀globals.list register → list (joint_seq ertl_params globals) ≝
     24  ∀globals.list register → list (joint_seq ERTL globals) ≝
    2525  λglobals,params.
    2626  save_hdws … (zip_pottier … params RegisterParams).
     
    2828definition get_param_stack :
    2929  ∀globals.register → register → register →
    30   list (joint_seq ertl_params globals) ≝
     30  list (joint_seq ERTL globals) ≝
    3131  λglobals,addr1,addr2,destr.
    3232  (* liveness analysis will erase the last useless ops *)
     
    3838definition get_params_stack :
    3939  ∀globals.list register →
    40   bind_new (localsT ertl_params) (list (joint_seq ertl_params globals)) ≝
     40  bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
    4141  λglobals,params.
    4242  νtmpr,addr1,addr2 in
     
    5959definition prologue :
    6060  ∀globals.list register → register → register → list (register×Register) →
    61   bind_new (localsT ertl_params) (list (joint_seq ertl_params globals)) ≝
     61  bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
    6262  λglobals,params,sral,srah,sregs.
    6363  [ (ertl_new_frame : joint_seq ??) ;
     
    6767
    6868definition save_return :
    69   ∀globals.list psd_argument → list (joint_seq ertl_params globals) ≝
     69  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
    7070  λglobals,ret_regs.
    7171  match reduce_strong ? ? RegisterSTS ret_regs with
     
    7979  ].
    8080
    81 definition assign_result : ∀globals.list (joint_seq ertl_params globals) ≝
     81definition assign_result : ∀globals.list (joint_seq ERTL globals) ≝
    8282  λglobals.
    8383  match reduce_strong ?? RegisterRets RegisterSTS with
     
    9090definition epilogue :
    9191  ∀globals.list register → register → register → list (register × Register) →
    92   list (joint_seq ertl_params globals) ≝
     92  list (joint_seq ERTL globals) ≝
    9393  λglobals,ret_regs,sral,srah,sregs.
    9494  save_return … (map … (Reg ?) ret_regs) @
    9595  restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @
    96   [ PUSH ertl_params ? srah ;
     96  [ PUSH ERTL ? srah ;
    9797    PUSH … sral ;
    9898    ertl_del_frame ] @
     
    101101definition allocate_regs :
    102102  ∀globals,rs.rs_set rs →
    103   state_monad (joint_internal_function globals ertl_params) (list (register×Register)) ≝
     103  state_monad (joint_internal_function ERTL globals) (list (register×Register)) ≝
    104104  λglobals,rs,saved,def.
    105105   let allocate_regs_internal ≝
     
    112112definition add_pro_and_epilogue :
    113113  ∀globals.list register → list register →
    114   joint_internal_function globals ertl_params →
    115   joint_internal_function globals ertl_params ≝
     114  joint_internal_function ERTL globals →
     115  joint_internal_function ERTL globals ≝
    116116  λglobals,params,ret_regs,def.
    117117  let start_lbl ≝ joint_if_entry … def in
     
    129129
    130130definition set_params_hdw :
    131   ∀globals.list psd_argument → list (joint_seq ertl_params globals) ≝
     131  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
    132132  λglobals,params.
    133133  restore_hdws globals (zip_pottier ? ? params RegisterParams).
     
    137137definition set_param_stack :
    138138  ∀globals.register → register → psd_argument →
    139   list (joint_seq ertl_params globals) ≝
     139  list (joint_seq ERTL globals) ≝
    140140  λglobals,addr1,addr2,arg.
    141141  [ STORE … addr1 addr2 arg ;
     
    145145
    146146definition set_params_stack :
    147   ∀globals.list psd_argument → bind_new (localsT ertl_params) ? ≝
     147  ∀globals.list psd_argument → bind_new (localsT ERTL) ? ≝
    148148  λglobals,params.
    149149  νaddr1,addr2 in
     
    166166
    167167definition fetch_result :
    168   ∀globals.list register → list (joint_seq ertl_params globals) ≝
     168  ∀globals.list register → list (joint_seq ERTL globals) ≝
    169169  λglobals,ret_regs.
    170170  match reduce_strong ?? RegisterSTS RegisterRets with
     
    182182
    183183definition translate_step :
    184   ∀globals.label → joint_step rtlntc_params globals →
    185     bind_seq_block ertl_params globals (joint_step ertl_params globals) ≝
     184  ∀globals.label → joint_step RTL_ntc globals →
     185    bind_seq_block ERTL globals (joint_step ERTL globals) ≝
    186186  λglobals.λ_.λs.
    187187  match s return λ_.bind_seq_block ?? (joint_step ??) with
     
    194194      COST_LABEL … lbl
    195195    | ADDRESS x prf r1 r2 ⇒
    196       ADDRESS ertl_params ? x prf r1 r2
     196      ADDRESS ERTL ? x prf r1 r2
    197197    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
    198       OPACCS ertl_params ? op destr1 destr2 srcr1 srcr2 
     198      OPACCS ERTL ? op destr1 destr2 srcr1 srcr2 
    199199    | OP1 op1 destr srcr ⇒
    200       OP1 ertl_params ? op1 destr srcr
     200      OP1 ERTL ? op1 destr srcr
    201201    | OP2 op2 destr srcr1 srcr2 ⇒
    202       OP2 ertl_params ? op2 destr srcr1 srcr2
     202      OP2 ERTL ? op2 destr srcr1 srcr2
    203203    | CLEAR_CARRY ⇒
    204204      CLEAR_CARRY …
     
    206206      SET_CARRY …
    207207    | LOAD destr addr1 addr2 ⇒
    208       LOAD ertl_params ? destr addr1 addr2
     208      LOAD ERTL ? destr addr1 addr2
    209209    | STORE addr1 addr2 srcr ⇒
    210       STORE ertl_params ? addr1 addr2 srcr
     210      STORE ERTL ? addr1 addr2 srcr
    211211    | COMMENT msg ⇒
    212212      COMMENT … msg
     
    218218    | CALL_ID f args ret_regs ⇒
    219219      set_params ? args @@
    220       CALL_ID ertl_params ? f (|args|) it :::
     220      CALL_ID ERTL ? f (|args|) it :::
    221221      fetch_result ? ret_regs
    222222    | extension_call c ⇒
     
    227227    ]
    228228  | COND r ltrue ⇒
    229     COND ertl_params ? r ltrue
     229    COND ERTL ? r ltrue
    230230  ]. cases daemon (* pointer call to be ported yet *) qed.
    231231
    232232definition translate_fin_step :
    233   ∀globals.label → joint_fin_step rtlntc_params
    234     bind_seq_block ertl_params globals (joint_fin_step ertl_params) ≝
     233  ∀globals.label → joint_fin_step RTL_ntc
     234    bind_seq_block ERTL globals (joint_fin_step ERTL) ≝
    235235  λglobals.λ_.λs.
    236236  match s with
     
    242242(* hack with empty graphs used here *)
    243243definition translate_funct :
    244   ∀globals.joint_internal_function globals rtlntc_params →
    245     joint_internal_function globals ertl_params ≝
     244  ∀globals.joint_internal_function RTL_ntc globals →
     245    joint_internal_function ERTL globals ≝
    246246  λglobals,def.
    247247  let nb_params ≝ |joint_if_params ?? def| in
     
    253253  let graph' ≝ add ? ? graph' exit' (RETURN …) in
    254254  let def' ≝
    255     mk_joint_internal_function globals ertl_params
     255    mk_joint_internal_function ERTL globals
    256256      (joint_if_luniverse … def) (joint_if_runiverse … def) it (*Paolo: to be checked, unit or list register? *)
    257257      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
     
    272272  λglobals.
    273273  λstmt.
    274   λdef: joint_internal_function globals ertl_params.
     274  λdef: joint_internal_function globals ERTL.
    275275  let 〈entry, def〉 ≝ fresh_label … def in
    276276  let graph ≝ add … (joint_if_code … def) entry stmt in
    277    set_joint_if_graph … (ertl_params globals) graph def ??.
     277   set_joint_if_graph … (ERTL globals) graph def ??.
    278278  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
    279279  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
     
    295295         match inst with
    296296          [ COST_LABEL cost_lbl ⇒
    297              〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉
     297             〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉
    298298          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
    299299      | RETURN ⇒ 〈None …, def〉
     
    310310  match cost_label with
    311311  [ None ⇒ def
    312   | Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
     312  | Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
    313313  ].
    314314
  • src/RTL/RTL_paolo.ma

    r2208 r2214  
    1111  | rtl_tailcall_ptr: register → register → list psd_argument → rtl_tailcall.
    1212
    13 definition rtl_uns_params ≝ mk_unserialized_params
     13definition RTL_uns ≝ mk_unserialized_params
    1414  (mk_step_params
    1515    (* acc_a_reg ≝ *) register
     
    3535      (* localsT ≝ *) register).
    3636
    37 definition rtl_params ≝ mk_graph_params rtl_uns_params.
    38 definition lin_rtl_params ≝ mk_lin_params rtl_uns_params.
    39 definition rtl_internal_function ≝
    40   λglobals. joint_internal_function globals rtl_params.
    41 definition rtl_program ≝ joint_program rtl_params.
    42 definition rtl_step ≝ joint_step rtl_params.
    43 definition rtl_seq ≝ joint_seq rtl_params.
    44 definition rtl_statement ≝ joint_statement rtl_params.
     37definition RTL ≝ mk_graph_params RTL_uns.
     38definition rtl_program ≝ joint_program RTL.
    4539
    46 interpretation "move" 'mov r a = (MOVE rtl_params ? (mk_Prod ? psd_argument r a)).
     40interpretation "move" 'mov r a = (MOVE RTL ? (mk_Prod ? psd_argument r a)).
    4741
    4842(* aid unification *)
     
    5044unification hint 0 ≔
    5145(*---------------*) ⊢
    52 acc_a_reg rtl_params ≡ register.
     46acc_a_reg RTL ≡ register.
    5347unification hint 0 ≔
    5448(*---------------*) ⊢
    55 acc_b_reg rtl_params ≡ register.
     49acc_b_reg RTL ≡ register.
    5650unification hint 0 ≔
    5751(*---------------*) ⊢
    58 acc_a_arg rtl_params ≡ psd_argument.
     52acc_a_arg RTL ≡ psd_argument.
    5953unification hint 0 ≔
    6054(*---------------*) ⊢
    61 acc_b_arg rtl_params ≡ psd_argument.
     55acc_b_arg RTL ≡ psd_argument.
    6256unification hint 0 ≔
    6357(*---------------*) ⊢
    64 dpl_reg rtl_params ≡ register.
     58dpl_reg RTL ≡ register.
    6559unification hint 0 ≔
    6660(*---------------*) ⊢
    67 dph_reg rtl_params ≡ register.
     61dph_reg RTL ≡ register.
    6862unification hint 0 ≔
    6963(*---------------*) ⊢
    70 dpl_arg rtl_params ≡ psd_argument.
     64dpl_arg RTL ≡ psd_argument.
    7165unification hint 0 ≔
    7266(*---------------*) ⊢
    73 dph_arg rtl_params ≡ psd_argument.
     67dph_arg RTL ≡ psd_argument.
    7468unification hint 0 ≔
    7569(*---------------*) ⊢
    76 snd_arg rtl_params ≡ psd_argument.
     70snd_arg RTL ≡ psd_argument.
    7771unification hint 0 ≔
    7872(*---------------*) ⊢
    79 pair_move rtl_params ≡ register × psd_argument.
     73pair_move RTL ≡ register × psd_argument.
    8074unification hint 0 ≔
    8175(*---------------*) ⊢
    82 call_args rtl_params ≡ list psd_argument.
     76call_args RTL ≡ list psd_argument.
    8377unification hint 0 ≔
    8478(*---------------*) ⊢
    85 call_dest rtl_params ≡ list register.
     79call_dest RTL ≡ list register.
    8680
    8781unification hint 0 ≔
    8882(*---------------*) ⊢
    89 ext_seq rtl_params ≡ rtl_seq.
     83ext_seq RTL ≡ rtl_seq.
    9084unification hint 0 ≔
    9185(*---------------*) ⊢
    92 ext_call rtl_params ≡ rtl_call.
     86ext_call RTL ≡ rtl_call.
    9387unification hint 0 ≔
    9488(*---------------*) ⊢
    95 ext_tailcall rtl_params ≡ rtl_tailcall.
    96 unification hint 0 ≔ globals
    97 (*---------------*) ⊢
    98 joint_step rtl_params globals ≡ rtl_step globals.
     89ext_tailcall RTL ≡ rtl_tailcall.
    9990
    100 unification hint 0 ≔ globals
    101 (*---------------*) ⊢
    102 joint_seq rtl_params globals ≡ rtl_seq globals.
    103 unification hint 0 ≔ globals
    104 (*---------------*) ⊢
    105 joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
    106 
    107 coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ psd_argument_from_reg
    108   on _r : register to snd_arg rtl_params.
    109 coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ psd_argument_from_byte
    110   on _b : Byte to snd_arg rtl_params.
     91coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg RTL ≝ psd_argument_from_reg
     92  on _r : register to snd_arg RTL.
     93coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg RTL ≝ psd_argument_from_byte
     94  on _b : Byte to snd_arg RTL.
    11195
    11296
    11397(************ Same without tail calls ****************)
    11498
    115 definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
     99definition RTL_ntc ≝ mk_graph_params (mk_unserialized_params
    116100  (mk_step_params
    117101    (* acc_a_reg ≝ *) register
     
    137121      (* localsT ≝ *) register)).
    138122
    139 definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).
    140 
    141 definition rtlntc_internal_function ≝
    142   λglobals. joint_internal_function … globals rtlntc_params.
    143 
    144 definition rtlntc_program ≝ joint_program rtlntc_params.
     123definition rtl_ntc_program ≝ joint_program RTL_ntc.
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r2208 r2214  
    133133  ∀srcrs2 : list psd_argument.
    134134  |dests| = |srcrs1| → |srcrs1| = |srcrs2| →
    135   list (joint_seq rtl_params globals)
     135  list (joint_seq RTL globals)
    136136  ≝
    137137  λglobals: list ident.
     
    146146  | Sub ⇒ [CLEAR_CARRY ??]
    147147  | _ ⇒ [ ]
    148   ] @ map3 ???? (OP2 rtl_params globals op) destrs srcrs1 srcrs2 prf1 prf2.
     148  ] @ map3 ???? (OP2 RTL globals op) destrs srcrs1 srcrs2 prf1 prf2.
    149149
    150150let rec nat_to_args (size : nat) (k : nat) on size : Σl : list psd_argument.|l| = size ≝
     
    174174  ∀destrs: list register.
    175175  |destrs| = size_of_cst ? cst_sig →
    176   list (joint_seq rtl_params globals)
     176  list (joint_seq RTL globals)
    177177 ≝
    178178  λty,globals,cst_sig,destrs.
     
    186186  | Oaddrsymbol id offset ⇒ λcst_prf,prf.
    187187    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    188     [ADDRESS rtl_params globals id ? r1 r2]
     188    [ADDRESS RTL globals id ? r1 r2]
    189189  | Oaddrstack offset ⇒ λcst_prf,prf.
    190190    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    191     [(rtl_stack_address r1 r2 : joint_seq rtl_params globals)]
     191    [(rtl_stack_address r1 r2 : joint_seq RTL globals)]
    192192  ] (pi2 … cst_sig).
    193193  [2: cases not_implemented
     
    203203  ∀destrs: list register.
    204204  ∀srcrs: list psd_argument.
    205   |destrs| = |srcrs| → list (joint_seq rtl_params globals) ≝
     205  |destrs| = |srcrs| → list (joint_seq RTL globals) ≝
    206206  λglobals,destrs,srcrs,length_eq.
    207207  map2 … (λdst,src.dst ← src) destrs srcrs length_eq.
     
    216216
    217217definition sign_mask : ∀globals.register → register →
    218   list (joint_seq rtl_params globals) ≝
     218  list (joint_seq RTL globals) ≝
    219219    (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that:
    220220       byte in destr if srcr is: neg   |  pos
     
    234234  ∀globals : list ident.
    235235  list register → register →
    236   bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     236  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    237237  λglobals,destrs,srcr.
    238238  ν tmp in
     
    242242definition translate_fill_with_zero :
    243243  ∀globals : list ident.
    244   list register → list (joint_seq rtl_params globals) ≝
     244  list register → list (joint_seq RTL globals) ≝
    245245  λglobals,destrs.
    246246  match nat_to_args (|destrs|) 0 with
     
    270270  ∀globals: list ident.
    271271  signedness → list register → list register →
    272     bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     272    bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    273273  λglobals,src_sign,destrs,srcrs.
    274274  match reduce_strong ?? destrs srcrs with
     
    299299  ∀destrs : list register.
    300300  ∀srcrs_arg : list register.
    301   |destrs| = |srcrs_arg| → list (joint_seq rtl_params globals) ≝
     301  |destrs| = |srcrs_arg| → list (joint_seq RTL globals) ≝
    302302  λglobals, destrs, srcrs, prf.
    303   map2 ??? (OP1 rtl_params globals Cmpl) destrs srcrs prf.
    304 
    305 definition translate_negint : ∀globals.? → ? → ? → bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     303  map2 ??? (OP1 RTL globals Cmpl) destrs srcrs prf.
     304
     305definition translate_negint : ∀globals.? → ? → ? → bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    306306  λglobals: list ident.
    307307  λdestrs: list register.
     
    318318  ∀globals : list ident.
    319319  list register → list register →
    320     bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     320    bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    321321  λglobals,destrs,srcrs.
    322322  match destrs with
     
    328328    | cons srcr srcrs' ⇒
    329329      (destr ← srcr) :::
    330       map register (joint_seq rtl_params globals) (λr. destr ← destr .Or. r) srcrs' @@
     330      map register (joint_seq RTL globals) (λr. destr ← destr .Or. r) srcrs' @@
    331331      (* now destr is non-null iff srcrs was non-null *)
    332332      CLEAR_CARRY ?? :::
     
    341341
    342342definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? →
    343   bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     343  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    344344  λglobals.
    345345  λty, ty'.
     
    351351  match op1
    352352  return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' →
    353     bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) with
     353    bind_new (localsT RTL) (list (joint_seq RTL globals)) with
    354354  [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2.
    355355    translate_cast globals src_sign destrs srcrs
     
    410410  (Σi.i<S k) →
    411411  (* the accumulator *)
    412   list (joint_seq rtl_params globals) →
    413     list (joint_seq rtl_params globals) ≝
     412  list (joint_seq RTL globals) →
     413    list (joint_seq RTL globals) ≝
    414414  λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2,
    415415    tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc.
     
    456456] qed.
    457457
    458 definition translate_mul : ∀globals.?→?→?→?→?→bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     458definition translate_mul : ∀globals.?→?→?→?→?→bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    459459λglobals : list ident.
    460460λdestrs : list register.
     
    472472(* the step calculating all products with least significant byte going in the
    473473   k-th position of the result *)
    474 let translate_mul_k : (Σk.k<|destrs|) → list (joint_seq rtl_params globals) →
    475   list (joint_seq rtl_params globals) ≝
     474let translate_mul_k : (Σk.k<|destrs|) → list (joint_seq RTL globals) →
     475  list (joint_seq RTL globals) ≝
    476476  λk_sig,acc.match k_sig with
    477477  [ mk_Sig k k_prf ⇒
     
    496496
    497497definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→
    498     bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     498    bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    499499  λglobals: list ident.
    500500  λdiv_not_mod: bool.
     
    543543
    544544definition translate_ne: ∀globals: list ident.?→?→?→?→
    545   bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     545  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    546546  λglobals: list ident.
    547547  λdestrs: list register.
     
    559559      | cons srcr2 srcrs2' ⇒ λEQ.
    560560        νtmpr in
    561         let f : psd_argument → psd_argument → list (joint_seq rtl_params globals) → list (joint_seq rtl_params globals) ≝
     561        let f : psd_argument → psd_argument → list (joint_seq RTL globals) → list (joint_seq RTL globals) ≝
    562562          λs1,s2,acc.
    563563          tmpr  ← s1 .Xor. s2 ::
    564564          destr ← destr .Or. tmpr ::
    565565          acc in
    566         let epilogue : list (joint_seq rtl_params globals) ≝
     566        let epilogue : list (joint_seq RTL globals) ≝
    567567          [ CLEAR_CARRY ?? ;
    568568            tmpr ← zero_byte .Sub. destr ;
     
    577577(* if destrs is 0 or 1, it inverses it. To be used after operations that
    578578   ensure this. *)
    579 definition translate_toggle_bool : ∀globals.?→list (joint_seq rtl_params globals) ≝
     579definition translate_toggle_bool : ∀globals.?→list (joint_seq RTL globals) ≝
    580580  λglobals: list ident.
    581581  λdestrs: list register.
     
    591591  ∀srcrs2: list psd_argument.
    592592  |srcrs1| = |srcrs2| →
    593   bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     593  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    594594  λglobals,destrs,srcrs1,srcrs2,srcrs_prf.
    595595  match destrs with
     
    609609  (tmp : register)
    610610  (srcrs : list psd_argument) on srcrs :
    611   Σt : (list psd_argument) × (list (joint_seq rtl_params globals)).|\fst t| = |srcrs| ≝
     611  Σt : (list psd_argument) × (list (joint_seq RTL globals)).|\fst t| = |srcrs| ≝
    612612  let byte_128 : Byte ≝ true ::: bv_zero ? in
    613613  match srcrs with
     
    631631  ∀srcrs2: list psd_argument.
    632632  |srcrs1| = |srcrs2| →
    633   bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     633  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    634634  λglobals,destrs,srcrs1,srcrs2,srcrs_prf.
    635635  νtmp_last_s1 in
     
    649649qed.
    650650
    651 definition translate_lt : bool→∀globals.?→?→?→?→bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     651definition translate_lt : bool→∀globals.?→?→?→?→bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    652652  λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs_prf.
    653653  if is_unsigned then
     
    684684  |srcrs1| = size_of_sig_type ty1 →
    685685  |srcrs2| = size_of_sig_type ty2 →
    686   bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     686  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    687687  λglobals,ty1,ty2,ty3,op2,destrs,srcrs1,srcrs2.
    688688  match op2 return λty1,ty2,ty3.λx : binary_operation ty1 ty2 ty3.
     
    728728
    729729definition translate_cond: ∀globals: list ident. list register → label →
    730   bind_seq_block rtl_params globals (joint_step rtl_params globals) ≝
     730  bind_seq_block RTL globals (joint_step RTL globals) ≝
    731731  λglobals: list ident.
    732732  λsrcrs: list register.
    733733  λlbl_true: label.
    734   match srcrs return λ_.bind_seq_block rtl_params ? (joint_step ??) with
     734  match srcrs return λ_.bind_seq_block RTL ? (joint_step ??) with
    735735  [ nil ⇒ bret … 〈[ ], NOOP ??〉
    736736  | cons srcr srcrs' ⇒
    737737    ν tmpr in
    738     let f : register → joint_seq rtl_params globals ≝
     738    let f : register → joint_seq RTL globals ≝
    739739      λr. tmpr ← tmpr .Or. r in
    740     bret … 〈MOVE rtl_params globals 〈tmpr,srcr〉 ::
     740    bret … 〈MOVE RTL globals 〈tmpr,srcr〉 ::
    741741    map ?? f srcrs', (COND … tmpr lbl_true : joint_step ??) 〉
    742742  ].
    743743
    744744(* Paolo: to be controlled (original seemed overly complex) *)
    745 definition translate_load : ∀globals.?→?→?→bind_new (localsT rtl_params) ? ≝
     745definition translate_load : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝
    746746  λglobals: list ident.
    747747  λaddr : list psd_argument.
     
    750750  ν tmp_addr_l in
    751751  ν tmp_addr_h in
    752   let f ≝ λdestr : register.λacc : list (joint_seq rtl_params globals).
    753     LOAD rtl_params globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) ::
     752  let f ≝ λdestr : register.λacc : list (joint_seq RTL globals).
     753    LOAD RTL globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) ::
    754754    translate_op ? Add
    755755      [tmp_addr_l ; tmp_addr_h]
     
    761761] // qed.
    762762 
    763 definition translate_store : ∀globals.?→?→?→bind_new (localsT rtl_params) ? ≝
     763definition translate_store : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝
    764764  λglobals: list ident.
    765765  λaddr : list psd_argument.
     
    768768  ν tmp_addr_l in
    769769  ν tmp_addr_h in
    770   let f ≝ λsrcr : psd_argument.λacc : list (joint_seq rtl_params globals).
    771     STORE rtl_params globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr ::
     770  let f ≝ λsrcr : psd_argument.λacc : list (joint_seq RTL globals).
     771    STORE RTL globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr ::
    772772    translate_op … Add
    773773      [tmp_addr_l ; tmp_addr_h]
     
    780780definition translate_statement : ∀globals.local_env → statement →
    781781  𝚺b :
    782   bind_seq_block rtl_params globals (joint_step rtl_params globals) +
    783   bind_seq_block rtl_params globals (joint_fin_step rtl_params).
     782  bind_seq_block RTL globals (joint_step RTL globals) +
     783  bind_seq_block RTL globals (joint_fin_step RTL).
    784784  if is_inl … b then label else unit ≝
    785785  λglobals,lenv,stmt.
     
    812812    ❬(match retr with
    813813      [ Some retr ⇒
    814         CALL_ID rtl_params ? f (rtl_args args lenv ?) (find_local_env retr lenv ?)
     814        CALL_ID RTL ? f (rtl_args args lenv ?) (find_local_env retr lenv ?)
    815815      | None ⇒
    816         CALL_ID rtl_params ? f (rtl_args args lenv ?) [ ]
     816        CALL_ID RTL ? f (rtl_args args lenv ?) [ ]
    817817      ] : bind_seq_block ???), lbl'❭
    818818  | St_call_ptr f args retr lbl' ⇒
     
    882882  let entry' ≝ f_entry def in
    883883  let exit' ≝ f_exit def in
    884   let graph' ≝ empty_map LabelTag (joint_statement rtl_params globals) in
     884  let graph' ≝ empty_map LabelTag (joint_statement RTL globals) in
    885885  let graph' ≝ add LabelTag ? graph' entry'
    886886    (GOTO … exit') in
     
    891891    b_adds_graph … (rtl_ertl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in
    892892  let res ≝
    893     mk_joint_internal_function globals rtl_params luniverse' runiverse' result' params'
     893    mk_joint_internal_function RTL globals luniverse' runiverse' result' params'
    894894     locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in
    895895    foldi … f_trans (f_graph def) res. 
  • src/joint/Joint_paolo.ma

    r2208 r2214  
    472472  (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))).
    473473
    474 record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝
     474record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
    475475{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
    476476  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
     
    489489
    490490definition joint_closed_internal_function ≝
    491   λglobals,p.
     491  λp,globals.
    492492    Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
    493493
     
    495495  λglobals: list ident.
    496496  λpars: params.
    497   λint_fun: joint_internal_function globals pars.
     497  λint_fun: joint_internal_function pars globals.
    498498  λgraph: codeT pars globals.
    499499  λentry.
    500500  λexit.
    501     mk_joint_internal_function globals pars
     501    mk_joint_internal_function pars globals
    502502      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
    503503      (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
     
    507507  λglobals.λpars : graph_params.
    508508  λgraph.
    509   λp:joint_internal_function globals pars.
     509  λp:joint_internal_function pars globals.
    510510  λentry_prf.
    511511  λexit_prf.
     
    536536definition add_graph ≝
    537537  λg_pars : graph_params.λglobals.λl:label.λstmt.
    538     λp:joint_internal_function globals g_pars.
     538    λp:joint_internal_function g_pars globals.
    539539   let code ≝ add … (joint_if_code … p) l stmt in
    540     mk_joint_internal_function ? g_pars
     540    mk_joint_internal_function
    541541     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    542542     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     
    550550
    551551definition set_locals ≝
    552   λglobals,pars.
    553   λp : joint_internal_function globals pars.
     552  λpars,globals.
     553  λp : joint_internal_function pars globals.
    554554  λlocals.
    555    mk_joint_internal_function globals pars
     555   mk_joint_internal_function pars globals
    556556    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    557557    (joint_if_params … p) locals (joint_if_stacksize … p)
     
    561561
    562562definition joint_program ≝
    563  λp:params. program (λglobals. joint_function globals p) nat.
     563 λp:params. program (joint_function p) nat.
  • src/joint/TranslateUtils_paolo.ma

    r2182 r2214  
    55(* type T is the syntactic type of the generated things *)
    66(* (sig for RTLabs registers, unit in others ) *)
    7 definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function … g pars).
     7definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function pars g).
    88
    99definition rtl_ertl_fresh_reg:
     
    3939  (globals: list ident)
    4040  (insts: list (joint_seq g_pars globals))
    41   (src : label) on insts : state_monad (joint_internal_function … g_pars) label ≝
     41  (src : label) on insts : state_monad (joint_internal_function g_pars globals) label ≝
    4242  match insts with
    4343  [ nil ⇒ return src
     
    4949  ].
    5050
     51definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with
     52  [ inl _ ⇒ true
     53  | inr _ ⇒ false
     54  ].
     55definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with
     56  [ inl _ ⇒ true
     57  | inr _ ⇒ false
     58  ].
     59
    5160definition adds_graph :
    5261  ∀g_pars : graph_params.
     
    5564       seq_block g_pars globals (joint_fin_step g_pars).
    5665  label → if is_inl … b then label else unit →
    57   joint_internal_function … g_pars → joint_internal_function … g_pars ≝
     66  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
    5867  λg_pars,globals,insts,src.
    5968  match insts return λx.if is_inl … x then ? else ? → ? → ? with
     
    6978definition insert_prologue ≝
    7079  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
    71   λdef : joint_internal_function globals g_pars.
     80  λdef : joint_internal_function g_pars globals.
    7281  let entry ≝ joint_if_entry … def in
    7382  match stmt_at … entry
     
    99108definition insert_epilogue ≝
    100109  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
    101   λdef : joint_internal_function globals g_pars.
     110  λdef : joint_internal_function g_pars globals.
    102111  let exit ≝ joint_if_exit … def in
    103112  match stmt_at … exit
     
    121130       bind_seq_block g_pars globals (joint_fin_step g_pars).
    122131  label → if is_inl … b then label else unit →
    123   joint_internal_function globals g_pars
    124   joint_internal_function globals g_pars ≝
     132  joint_internal_function g_pars globals
     133  joint_internal_function g_pars globals ≝
    125134  λg_pars,globals,fresh_r,insts,src.
    126135  match insts return λx.if is_inl … x then ? else ? → ? → ? with
     
    140149  freshT globals dst_g_pars (localsT dst_g_pars) →
    141150  (* initialized function definition with empty graph *)
    142   joint_internal_function globals dst_g_pars →
     151  joint_internal_function dst_g_pars globals →
    143152  (* functions dictating the translation *)
    144153  (label → joint_step src_g_pars globals →
     
    147156    bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
    148157  (* source function *)
    149   joint_internal_function globals src_g_pars →
     158  joint_internal_function src_g_pars globals →
    150159  (* destination function *)
    151   joint_internal_function globals dst_g_pars ≝
     160  joint_internal_function dst_g_pars globals ≝
    152161  λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
    153162  let f : label → joint_statement (src_g_pars : params) globals →
    154     joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
     163    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
    155164    λlbl,stmt,def.
    156165    match stmt with
     
    167176  ∀globals: list ident.
    168177  (* initialized function definition with empty graph *)
    169   joint_internal_function … dst_g_pars →
     178  joint_internal_function dst_g_pars globals →
    170179  (* functions dictating the translation *)
    171180  (label → joint_step src_g_pars globals →
     
    174183    seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
    175184  (* source function *)
    176   joint_internal_function … src_g_pars →
     185  joint_internal_function src_g_pars globals →
    177186  (* destination function *)
    178   joint_internal_function … dst_g_pars ≝
     187  joint_internal_function dst_g_pars globals ≝
    179188  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
    180189  let f : label → joint_statement (src_g_pars : params) globals →
    181     joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
     190    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
    182191    λlbl,stmt,def.
    183192    match stmt with
  • src/joint/blocks.ma

    r2186 r2214  
    22include "utilities/bindLists.ma".
    33
    4 inductive block_step (p : stmt_params) (globals : list ident) : Type[0] ≝
     4(* inductive block_step (p : stmt_params) (globals : list ident) : Type[0] ≝
    55  | block_seq : joint_seq p globals → block_step p globals
    66  | block_skip : label → block_step p globals.
     
    4040
    4141definition skip_block ≝ λp,globals,A.
    42   (list (block_step p globals)) × A.
     42  (list (block_step p globals)) × A.*)
    4343
    4444definition seq_block ≝ λp : stmt_params.λglobals,A.
    4545  (list (joint_seq p globals)) × A.
    4646
    47 definition seq_to_skip_block :
     47(*definition seq_to_skip_block :
    4848  ∀p,g,A.seq_block p g A → skip_block p g A
    4949 ≝ λp,g,A,b.〈\fst b, \snd b〉.
     
    5151coercion skip_from_seq_block :
    5252  ∀p,g,A.∀b : seq_block p g A.skip_block p g A ≝
    53   seq_to_skip_block on _b : seq_block ??? to skip_block ???.
     53  seq_to_skip_block on _b : seq_block ??? to skip_block ???.*)
    5454
    5555definition bind_seq_block ≝ λp : stmt_params.λglobals,A.
     
    7070bind_seq_list p g ≡ bind_new R L.
    7171
    72 definition bind_skip_block ≝ λp : stmt_params.λglobals,A.
     72(*definition bind_skip_block ≝ λp : stmt_params.λglobals,A.
    7373  bind_new (localsT p) (skip_block p globals A).
    7474unification hint 0 ≔ p : stmt_params, g, A;
     
    8484coercion bind_skip_from_seq_block :
    8585  ∀p,g,A.∀b:bind_seq_block p g A.bind_skip_block p g A ≝
    86   bind_seq_to_skip_block on _b : bind_seq_block ??? to bind_skip_block ???.
     86  bind_seq_to_skip_block on _b : bind_seq_block ??? to bind_skip_block ???.*)
    8787(*
    8888definition block_classifier ≝
  • src/joint/linearise.ma

    r2200 r2214  
    652652  ∀p : unserialized_params.
    653653  ∀globals.
    654     joint_internal_function globals (mk_graph_params p)
    655     joint_internal_function globals (mk_lin_params p)
     654    joint_internal_function (mk_graph_params p) globals
     655    joint_internal_function (mk_lin_params p) globals
    656656     (* ∃sigma : identifier_map LabelTag ℕ.
    657657        let g ≝ joint_if_code ?? (pi1 … fin) in
     
    670670                    (stmt_implicit_label … s)) (nth_opt … n c)*) ≝
    671671  λp,globals,f_in.
    672   mk_joint_internal_function globals (mk_lin_params p)
     672  mk_joint_internal_function (mk_lin_params p) globals
    673673   (joint_if_luniverse ?? f_in) (joint_if_runiverse ?? f_in)
    674674   (joint_if_result ?? f_in) (joint_if_params ?? f_in) (joint_if_locals ?? f_in)
  • src/joint/semanticsUtils_paolo.ma

    r2208 r2214  
    124124definition make_sem_graph_params :
    125125  ∀pars : graph_params.
    126   ∀g_pars : more_sem_genv_params pars.
     126  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
    127127  sem_params ≝
    128128  λpars,g_pars.
     
    163163definition make_sem_lin_params :
    164164  ∀pars : lin_params.
    165   ∀g_pars : more_sem_genv_params pars.
     165  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
    166166  sem_params ≝
    167167  λpars,g_pars.
  • src/joint/semantics_paolo.ma

    r2200 r2214  
    1212   only the head is kept (or Undef if the list is empty) ??? *)
    1313
    14 definition genv ≝ λglobals.λp:params. genv_t (joint_function globals p).
     14definition genv ≝ λp:params.λglobals.genv_t (joint_function p globals).
    1515definition cpointer ≝ Σp.ptype p = Code.
    1616definition xpointer ≝ Σp.ptype p = XData.
     
    6868 ∀pars : params.
    6969 ∀globals.
    70   genv globals pars →
     70  genv pars globals →
    7171  block →
    72   res (joint_internal_function … pars) ≝
    73   λpars,blobals,ge,b.
     72  res (joint_internal_function pars globals) ≝
     73  λpars,globals,ge,b.
    7474  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
    7575  match def with
     
    8181 ∀pars : params.
    8282 ∀globals.
    83   genv globals pars →
     83  genv pars globals →
    8484  cpointer →
    85   res (joint_internal_function … pars) ≝
     85  res (joint_internal_function pars globals) ≝
    8686 λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
    8787
    88 inductive step_flow (p : params) (globals : list ident) : possible_flows → Type[0] ≝
    89   | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p globals (Labels lbls) (* used for goto-like flow alteration *)
    90   | 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 *)
    91   | Proceed  : ∀flows.step_flow p globals flows. (* go to implicit successor *)
    92 
    93 (*
    94 definition step_flow_cons : ∀p,globals,l,lbls.
    95   step_flow p globals lbls → step_flow p globals (l :: lbls) ≝
    96   λp,globals,l1,l2,flow.match flow with
    97   [ Redirect l ⇒ Redirect … «l, ?»
    98   | Init id f args dest ⇒ Init … id f args dest
    99   | Proceed ⇒ Proceed ???
    100   ]. cases l /2 by or_intror/ qed.
    101 coercion step_flow_c : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1::l2) ≝
    102   step_flow_cons on _flow : step_flow ??? to step_flow ?? (cons ???).
    103 
    104 definition step_flow_append_l : ∀p,globals,l1,l2.
    105   step_flow p globals l1 → step_flow p globals (l1 @ l2) ≝
    106   λp,globals,l1,l2,flow.match flow with
    107   [ Redirect l ⇒ Redirect … «l, ?»
    108   | Init id f args dest ⇒ Init … id f args dest
    109   | Proceed ⇒ Proceed ???
    110   ]. cases l /2 by Exists_append_l/ qed.
    111 coercion step_flow_l : ∀p,globals,l1,l2.∀flow : step_flow p globals l1.step_flow p globals (l1@l2) ≝
    112   step_flow_append_l on _flow : step_flow ??? to step_flow ?? (append ???).
    113 
    114 definition step_flow_append_r : ∀p,globals,l1,l2.
    115   step_flow p globals l2 → step_flow p globals (l1 @ l2) ≝
    116   λp,globals,l1,l2,flow.match flow with
    117   [ Redirect l ⇒ Redirect … «l, ?»
    118   | Init id f args dest ⇒ Init … id f args dest
    119   | Proceed ⇒ Proceed ???
    120   ]. cases l /2 by Exists_append_r/ qed.
    121 coercion step_flow_r : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1@l2) ≝
    122   step_flow_append_r on _flow : step_flow ??? to step_flow ?? (append ???).
    123 *)
    124 
    125 inductive fin_step_flow (p : params) (globals : list ident) : possible_flows → Type[0] ≝
    126   | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p globals (Labels lbls)
    127   | FTailInit : Z → joint_internal_function globals p → call_args p → fin_step_flow p globals Call
    128   | FEnd1  : fin_step_flow p globals (Labels [ ]) (* end flow *)
    129   | FEnd2  : fin_step_flow p globals Call. (* end flow *)
    130 
    131 (*
    132 definition fin_step_flow_cons : ∀p,globals,l,lbls.
    133   fin_step_flow p globals lbls → fin_step_flow p globals (l :: lbls) ≝
    134   λp,globals,l1,l2,flow.match flow with
    135   [ FRedirect l ⇒ FRedirect … «l, ?»
    136   | FTailInit id f args ⇒ FTailInit … id f args
    137   | FEnd ⇒ FEnd ???
    138   ]. cases l /2 by or_intror/ qed.
    139 coercion fin_step_flow_c : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1::l2) ≝
    140   fin_step_flow_cons on _flow : fin_step_flow ??? to fin_step_flow ?? (cons ???).
    141 
    142 definition fin_step_flow_append_l : ∀p,globals,l1,l2.
    143   fin_step_flow p globals l1 → fin_step_flow p globals (l1@l2) ≝
    144   λp,globals,l1,l2,flow.match flow with
    145   [ FRedirect l ⇒ FRedirect … «l, ?»
    146   | FTailInit id f args ⇒ FTailInit … id f args
    147   | FEnd ⇒ FEnd ???
    148   ]. cases l /2 by Exists_append_l/ qed.
    149 coercion fin_step_flow_l : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l1.fin_step_flow p globals (l1@l2) ≝
    150   fin_step_flow_append_l on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???).
    151 
    152 definition fin_step_flow_append_r : ∀p,globals,l1,l2.
    153   fin_step_flow p globals l2 → fin_step_flow p globals (l1@l2) ≝
    154   λp,globals,l1,l2,flow.match flow with
    155   [ FRedirect l ⇒ FRedirect … «l, ?»
    156   | FTailInit id f args ⇒ FTailInit … id f args
    157   | FEnd ⇒ FEnd ???
    158   ]. cases l /2 by Exists_append_r/ qed.
    159 coercion fin_step_flow_r : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1@l2) ≝
    160   fin_step_flow_append_r on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???).
    161 *)
    162 
    163 record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
    164   { st_pars :> sem_state_params
     88inductive step_flow (p : step_params) (F : Type[0]) : possible_flows → Type[0] ≝
     89  | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *)
     90  | Init     : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *)
     91  | Proceed  : ∀flows.step_flow p F flows. (* go to implicit successor *)
     92
     93inductive fin_step_flow (p : step_params) (F : Type[0]) : possible_flows → Type[0] ≝
     94  | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls)
     95  | FTailInit : Z → F → call_args p → fin_step_flow p F Call
     96  | FEnd1  : fin_step_flow p F (Labels [ ]) (* end flow *)
     97  | FEnd2  : fin_step_flow p F Call. (* end flow *)
     98
     99record more_sem_unserialized_params
     100  (uns_pars : unserialized_params)
     101  (F : list ident → Type[0]) : Type[1] ≝
     102  { st_pars :> sem_state_params (* automatic coercion has issues *)
    165103  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
    166104  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
     
    181119  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
    182120  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    183   ; save_frame: cpointer → call_dest uns_pars → state st_pars → framesT st_pars
     121  ; save_frame: cpointer → call_dest uns_pars → state st_pars → res (state st_pars)
    184122   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    185123     type of arguments. To be fixed using a dependent type *)
     
    191129  ; call_args_for_main: call_args uns_pars
    192130  ; call_dest_for_main: call_dest uns_pars
    193  }.
     131
     132  (* from now on, parameters that use the type of functions *)
     133  ; read_result: ∀globals.genv_t (fundef (F globals)) → state st_pars → res (list beval)
     134  (* change of pc must be left to *_flow execution *)
     135  ; eval_ext_seq: ∀globals.genv_t (fundef (F globals)) → ext_seq uns_pars →
     136      state st_pars → IO io_out io_in (state st_pars)
     137  ; eval_ext_tailcall : ∀globals.genv_t (fundef (F globals)) → ext_tailcall uns_pars →
     138      state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
     139  ; eval_ext_call: ∀globals.genv_t (fundef (F globals)) → ∀s : ext_call uns_pars.
     140      state st_pars →
     141      IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars))
     142  ; pop_frame: ∀globals.genv_t (fundef (F globals)) → state st_pars → res (state st_pars)
     143  }.
     144
     145(*coercion msu_pars_to_ss_pars nocomposites :
     146∀p,F.∀msup : more_sem_unserialized_params p F.sem_state_params
     147 ≝ st_pars
     148on _msup : more_sem_unserialized_params ?? to sem_state_params.*)
    194149
    195150
    196151definition helper_def_retrieve :
    197   ∀X : ? → ? → Type[0].
    198   (∀up.∀p:more_sem_unserialized_params up. regsT p → X up p → res beval) →
    199   ∀up.∀p : more_sem_unserialized_params up.state p → X up p → res beval ≝
    200     λX,f,up,p,st.f ? p (regs … st).
     152  ∀X : ? → ? → ? → Type[0].
     153  (∀up,F.∀p:more_sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
     154  ∀up,F.∀p : more_sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
     155    λX,f,up,F,p,st.f ?? p (regs … st).
    201156
    202157definition helper_def_store :
    203   ∀X : ? → ? → Type[0].
    204   (∀up.∀p : more_sem_unserialized_params up.X up p → beval → regsT p → res (regsT p)) →
    205   ∀up.∀p : more_sem_unserialized_params up.X up p → beval → state p → res (state p) ≝
    206   λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return set_regs … r st.
     158  ∀X : ? → ? → ? → Type[0].
     159  (∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
     160  ∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
     161  λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st.
    207162
    208163definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
     
    219174definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
    220175definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
    221 definition pair_reg_move : ?→?→?→?→? 
    222   λup.λp : more_sem_unserialized_params up.λst : state p.λpm : pair_move up.
    223     ! r ← pair_reg_move_ ? p (regs ? st) pm;
     176definition pair_reg_move
     177  λup,F.λp : more_sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
     178    ! r ← pair_reg_move_ ?? p (regs ? st) pm;
    224179    return set_regs ? r st.
    225180
    226181 
    227182axiom BadPointer : String.
    228  
     183
    229184(* this is preamble to all calls (including tail ones). The optional argument in
    230185   input tells the function whether it has to save the frame for internal
     
    235190   serialization and on whether the call is a tail one. *)
    236191definition eval_call_block:
    237  ∀globals.∀p : params.∀p':more_sem_unserialized_params p.
    238   genv globals p → state p' → block → call_args p → call_dest p →
    239     IO io_out io_in ((step_flow p globals Call)×(state p')) ≝
    240  λglobals,p,p',ge,st,b,args,dest.
    241   ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ge b) : IO ? io_in ?);
     192 ∀p,F.∀p':more_sem_unserialized_params p F.∀globals.
     193  genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p →
     194    IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝
     195 λp,F,p',globals,ge,st,b,args,dest.
     196  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
    242197    match fd with
    243     [ Internal fn
    244       return 〈Init … (block_id b) fn args dest, st〉
     198    [ Internal fd
     199      return 〈Init ?? (block_id b) fd args dest, st〉
    245200    | External fn ⇒
    246201      ! params ← fetch_external_args … p' fn st : IO ???;
     
    289244  return 〈st'', pr〉.
    290245
    291 (* parameters that need full params to have type of functions,
    292    but are still independent of serialization *)
    293 record more_sem_genv_params (pp : params) : Type[1] ≝
    294   { msu_pars :> more_sem_unserialized_params pp
    295   ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
    296   (* change of pc must be left to *_flow execution *)
    297   ; eval_ext_seq: ∀globals.genv globals pp → ext_seq pp →
    298       state msu_pars → IO io_out io_in (state msu_pars)
    299   ; eval_ext_tailcall : ∀globals.genv globals pp → ext_tailcall pp →
    300       state msu_pars → IO io_out io_in ((fin_step_flow pp globals Call)×(state msu_pars))
    301   ; eval_ext_call: ∀globals.genv globals pp →∀s : ext_call pp.
    302       state msu_pars →
    303       IO io_out io_in ((step_flow pp globals Call)×(state msu_pars))
    304   ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
    305   }.
    306 
    307246(* parameters that are defined by serialization *)
    308247record more_sem_params (pp : params) : Type[1] ≝
    309   { msg_pars :> more_sem_genv_params pp
     248  { msu_pars :> more_sem_unserialized_params pp (joint_internal_function pp)
    310249  ; offset_of_point : code_point pp → option offset (* can overflow *)
    311250  ; point_of_offset : offset → code_point pp
     
    315254    ∀o.offset_of_point (point_of_offset o) = Some ? o
    316255  }.
     256
     257(*
     258coercion ms_pars_to_msu_pars nocomposites :
     259∀p : params.∀msp : more_sem_params p.more_sem_unserialized_params p (λglobals.joint_internal_function globals p)
     260 ≝ msu_pars
     261on _msp : more_sem_params ? to more_sem_unserialized_params ??.
     262
     263definition ss_pars_of_ms_pars ≝
     264  λp.λpp : more_sem_params p.
     265  st_pars … (msu_pars … pp).
     266coercion ms_pars_to_ss_pars nocomposites :
     267∀p : params.∀msp : more_sem_params p.sem_state_params ≝
     268ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*)
    317269
    318270axiom CodePointerOverflow : String.
     
    374326
    375327definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
    376   genv globals p → cpointer → res (joint_statement p globals) ≝
     328  genv p globals → cpointer → res (joint_statement p globals) ≝
    377329  λp,msp,globals,ge,ptr.
    378330  let pt ≝ point_of_pointer ? msp ptr in
     
    381333 
    382334definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
    383   genv globals p → cpointer → label → res cpointer ≝
     335  genv p globals → cpointer → label → res cpointer ≝
    384336  λp,msp,globals,ge,ptr,lbl.
    385337  ! fn ← fetch_function … ge ptr ;
     
    399351  }.
    400352
     353(* definition msu_pars_of_s_pars :
     354∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p))
     355≝ λp : sem_params.
     356  msu_pars … (more_sem_pars p).
     357coercion s_pars_to_msu_pars nocomposites :
     358∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝
     359msu_pars_of_s_pars
     360on p : sem_params to more_sem_unserialized_params ??.
     361
     362definition ss_pars_of_s_pars :
     363∀p : sem_params.sem_state_params
     364≝ λp : sem_params.
     365  st_pars … (msu_pars … (more_sem_pars p)).
     366coercion s_pars_to_ss_pars nocomposites :
     367∀p : sem_params.sem_state_params ≝
     368ss_pars_of_s_pars
     369on _p : sem_params to sem_state_params.
     370
     371definition ms_pars_of_s_pars :
     372∀p : sem_params.more_sem_params (spp p)
     373≝ more_sem_pars.
     374coercion s_pars_to_ms_pars nocomposites :
     375∀p : sem_params.more_sem_params (spp p) ≝
     376ms_pars_of_s_pars
     377on p : sem_params to more_sem_params ?.*)
     378
    401379(* definition address_of_label: ∀globals. ∀p:sem_params.
    402380  genv globals p → pointer → label → res address ≝
     
    405383  OK … (address_of_code_pointer newptr). *)
    406384
    407 definition goto: ∀globals. ∀p:sem_params.
    408   genv globals p → label → state p → cpointer → res (state_pc p) ≝
     385definition goto: ∀globals.∀p : sem_params.
     386  genv p globals → label → state p → cpointer → res (state_pc p) ≝
    409387 λglobals,p,ge,l,st,b.
    410388  ! newpc ← pointer_of_label ? p … ge b l ;
     
    427405
    428406definition eval_seq_no_pc :
    429  ∀globals.∀p:sem_params. genv globals p → state p →
     407 ∀globals.∀p:sem_params. genv p globals → state p →
    430408  ∀s:joint_seq p globals.
    431409  IO io_out io_in (state p) ≝
     
    433411  match seq return λx.IO ??? with
    434412  [ extension_seq c ⇒
    435     eval_ext_seq ??? ge c st
     413    eval_ext_seq ge c st
    436414  | LOAD dst addrl addrh ⇒
    437415    ! vaddrh ← dph_arg_retrieve … st addrh ;
     
    484462  | POP dst ⇒
    485463    ! 〈st',v〉 ← pop p st;
    486     acca_store p p dst v st'
     464    acca_store p dst v st'
    487465  | PUSH src ⇒
    488466    ! v ← acca_arg_retrieve … st src;
     
    495473    return st'
    496474  | extension_call s ⇒
    497     !〈flow, st'〉 ← eval_ext_call ??? ge s st ;
     475    !〈flow, st'〉 ← eval_ext_call ge s st ;
    498476    return st'
    499477  | _ ⇒ return st
     
    504482
    505483definition eval_seq_pc :
    506  ∀globals.∀p:sem_params. genv globals p → state p →
     484 ∀globals.∀p:sem_params. genv p globals → state p →
    507485  ∀s:joint_seq p globals.
    508   IO io_out io_in (step_flow p globals (step_flows … s)) ≝
     486  IO io_out io_in (step_flow p ? (step_flows … s)) ≝
    509487  λg,p,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
    510488  [ CALL_ID id args dest ⇒
     
    513491    return flow
    514492  | extension_call s ⇒
    515     !〈flow, st'〉 ← eval_ext_call ??? ge s st ;
     493    !〈flow, st'〉 ← eval_ext_call ge s st ;
    516494    return flow
    517495  | _ ⇒ return Proceed ???
     
    519497
    520498definition eval_step :
    521  ∀globals.∀p:sem_params. genv globals p → state p →
     499 ∀globals.∀p:sem_params. genv p globals → state p →
    522500  ∀s:joint_step p globals.
    523   IO io_out io_in ((step_flow p globals (step_flows … s))×(state p)) ≝
     501  IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝
    524502  λglobals,p,ge,st,s.
    525503  match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with
     
    538516  %1 % qed.
    539517
    540 definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv globals p
     518definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv p globals
    541519  state p → ∀s : joint_fin_step p.
    542520  IO io_out io_in (state p) ≝
     
    544522  match s return λx.IO ??? with
    545523    [ tailcall c ⇒
    546       !〈flow,st'〉 ← eval_ext_tailcall ??? ge c st ;
     524      !〈flow,st'〉 ← eval_ext_tailcall ge c st ;
    547525      return st'
    548526    | _ ⇒ return st
     
    550528
    551529definition eval_fin_step_pc :
    552  ∀globals.∀p:sem_params. genv globals p → state p →
     530 ∀globals.∀p:sem_params. genv p globals → state p →
    553531  ∀s:joint_fin_step p.
    554   IO io_out io_in (fin_step_flow p globals (fin_step_flows … s)) ≝
     532  IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
    555533  λg,p,ge,st,s.
    556534  match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
    557535  [ tailcall c ⇒
    558     !〈flow,st'〉 ← eval_ext_tailcall ??? ge c st ;
     536    !〈flow,st'〉 ← eval_ext_tailcall ge c st ;
    559537    return flow 
    560538  | GOTO l ⇒ return FRedirect … l
     
    562540  ]. %1 % qed.
    563541
    564 definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p
    565   state p → Z → joint_internal_function globals p → call_args p →
     542definition do_call : ∀globals: list ident.∀p:sem_params. genv p globals
     543  state p → Z → joint_internal_function p globals → call_args p →
    566544  res (state_pc p) ≝
    567545  λglobals,p,ge,st,id,fn,args.
    568546    ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
    569547              args st ;
    570     let regs ≝ foldr ?? (allocate_local p p) (regs … st) (joint_if_locals … fn) in
     548    let regs ≝ foldr ?? (allocate_local p) (regs … st) (joint_if_locals … fn) in
    571549    let l' ≝ joint_if_entry … fn in
    572550    let st' ≝ set_regs p regs st in
     
    577555(* The pointer provided is the one to the *next* instruction. *)
    578556definition eval_step_flow :
    579  ∀globals.∀p:sem_params.∀flows.genv globals p
    580  state p → cpointer → step_flow p globals flows → res (state_pc p) ≝
     557 ∀globals.∀p:sem_params.∀flows.genv p globals
     558 state p → cpointer → step_flow p ? flows → res (state_pc p) ≝
    581559 λglobals,p,flows,ge,st,nxt,cmd.
    582560 match cmd with
     
    584562    goto … ge l st nxt
    585563  | Init id fn args dest ⇒
    586     let st' ≝ set_frms … (save_frame … nxt dest st) st in
     564    ! st' ← save_frame … nxt dest st ;
    587565    do_call ?? ge st' id fn args
    588566  | Proceed _ ⇒
     
    590568  ].
    591569
    592 definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀flows. genv globals p
    593   state p → cpointer → fin_step_flow p globals flows → res (state_pc p) ≝
     570definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀flows. genv p globals
     571  state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝
    594572  λglobals,p,lbls,ge,st,curr,cmd.
    595573  match cmd with
     
    604582
    605583definition eval_statement :
    606  ∀globals.∀p:sem_params.genv globals p
     584 ∀globals.∀p:sem_params.genv p globals
    607585  state_pc p → joint_statement p globals →
    608586    IO io_out io_in (state_pc p) ≝
     
    619597 ].
    620598
    621 definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p
     599definition eval_state : ∀globals: list ident.∀p:sem_params. genv p globals
    622600  state_pc p → IO io_out io_in (state_pc p) ≝
    623601  λglobals,p,ge,st.
     
    629607  not static... *)
    630608definition is_final: ∀globals:list ident. ∀p: sem_params.
    631   genv globals p → cpointer → state_pc p → option int ≝
     609  genv p globals → cpointer → state_pc p → option int ≝
    632610 λglobals,p,ge,exit,st.res_to_opt ? (
    633611  do s ← fetch_statement ? p … ge (pc … st);
Note: See TracChangeset for help on using the changeset viewer.