Changeset 1882 for src/RTL


Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (9 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL_paolo.ma

    r1644 r1882  
    1616  on _n : nat to rtl_argument.
    1717
    18 (*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
    19   are not sequential. Thus there is a dummy label at the moment in the code.
    20   To be fixed once we understand exactly what to do with tail calls. *)
    21 inductive rtl_instruction_extension: Type[0] ≝
    22   | rtl_st_ext_stack_address: register → register → rtl_instruction_extension
    23   | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_instruction_extension.
     18inductive rtl_step_extension: Type[0] ≝
     19  | rtl_st_ext_stack_address: register → register → rtl_step_extension
     20  | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_step_extension.
    2421
    2522inductive rtl_statement_extension : Type[0] ≝
     
    2825
    2926definition rtl_uns_params ≝ mk_unserialized_params
    30   (mk_inst_params
     27  (mk_step_params
    3128    (* acc_a_reg ≝ *) register
    3229    (* acc_b_reg ≝ *) register
     
    4138    (* call_args ≝ *) (list rtl_argument)
    4239    (* call_dest ≝ *) (list register)
    43     (* ext_instruction ≝ *) rtl_instruction_extension
    44     (* ext_forall_labels ≝ *) (λP.λes.True)
    45     (* ext_fin_instruction ≝ *) rtl_statement_extension
    46     (* ext_fin_forall_labels ≝ *) (λP.λes.True))
     40    (* ext_step ≝ *) rtl_step_extension
     41    (* ext_step_labels ≝ *) (λes.[ ])
     42    (* ext_fin_stmt ≝ *) rtl_statement_extension
     43    (* ext_fin_stmt_labels ≝ *) (λes.[ ]))
    4744  (mk_local_params
    4845    (mk_funct_params
     
    5350definition rtl_params ≝ mk_graph_params rtl_uns_params.
    5451definition lin_rtl_params ≝ mk_lin_params rtl_uns_params.
     52definition rtl_internal_function ≝
     53  λglobals. joint_internal_function globals rtl_params.
     54definition rtl_program ≝ joint_program rtl_params.
     55definition rtl_step ≝ joint_step rtl_params.
     56definition rtl_statement ≝ joint_statement rtl_params.
    5557
    56 interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ?? r a)).
     58
     59interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ? rtl_argument r a)).
    5760
    5861(* aid unification *)
     
    9598call_dest (u_inst_pars (g_u_pars rtl_params)) ≡ list register.
    9699
    97 
    98 definition rtl_instruction ≝ joint_instruction rtl_params.
    99100unification hint 0 ≔
    100101(*---------------*) ⊢
    101 ext_instruction (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_instruction_extension.
     102ext_step (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_step_extension.
    102103unification hint 0 ≔ globals
    103104(*---------------*) ⊢
    104 joint_instruction (u_inst_pars (g_u_pars rtl_params)) globals ≡ rtl_instruction globals.
     105joint_step (u_inst_pars (g_u_pars rtl_params)) globals ≡ rtl_step globals.
    105106
    106 definition rtl_statement ≝ joint_statement rtl_params.
    107107unification hint 0 ≔
    108108(*---------------*) ⊢
    109 ext_fin_instruction (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_statement_extension.
     109ext_fin_stmt (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_statement_extension.
    110110unification hint 0 ≔ globals
    111111(*---------------*) ⊢
    112112joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
    113 
    114 definition rtl_internal_function ≝
    115   λglobals. joint_internal_function globals rtl_params.
    116 
    117 definition rtl_program ≝ joint_program rtl_params.
    118113
    119114(************ Same without tail calls ****************)
     
    124119
    125120definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
    126   (mk_inst_params
     121  (mk_step_params
    127122    (* acc_a_reg ≝ *) register
    128123    (* acc_b_reg ≝ *) register
     
    138133    (* call_dest ≝ *) (list register)
    139134    (* extend_statements ≝ *) rtlntc_statement_extension
    140     (* ext_forall_labels ≝ *) (λP.λes.True)
    141     void (λP,es.True))
     135    (* ext_forall_labels ≝ *) (λes.[ ])
     136    void (λes.[ ]))
    142137  (mk_local_params
    143138    (mk_funct_params
Note: See TracChangeset for help on using the changeset viewer.