Changeset 1643 for src/RTLabs


Ignore:
Timestamp:
Jan 13, 2012, 12:23:30 PM (8 years ago)
Author:
tranquil
Message:
  • some changes in everything
  • separated extensions in sequential and final, to accomodate tailcalls
  • finished RTL's semantics
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r1640 r1643  
    816816axiom fake_label: label.
    817817
    818 definition stmt_not_return ≝ λstmt.match stmt with
     818definition stmt_not_final ≝ λstmt.match stmt with
    819819  [ St_return ⇒ False
     820  | St_tailcall_id _ _ ⇒ False
     821  | St_tailcall_ptr _ _ ⇒ False
    820822  | _ ⇒ True ].
    821823
     
    824826        tailcall_* instructions. *)
    825827definition translate_inst : ∀globals.?→?→?→
    826   Prod (bind_list register unit (rtl_instruction globals)) label ≝
     828  (bind_list register unit (rtl_instruction globals)) × label ≝
    827829  λglobals: list ident.
    828830  λlenv: local_env.
    829831  λstmt.
    830   λstmt_prf : stmt_not_return stmt.
     832  λstmt_prf : stmt_not_final stmt.
    831833  match stmt return λx.stmt = x →
    832834    (bind_list register unit (rtl_instruction globals)) × label with
     
    873875        extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])
    874876      ]) [ ], lbl'〉
    875   | St_tailcall_id f args ⇒ λ_.
    876     〈[extension rtl_params globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))], fake_label〉
    877   | St_tailcall_ptr f args ⇒ λ_.
    878     let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    879     〈bcons … (extension rtl_params globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) [ ], fake_label〉
    880877  | St_cond r lbl_true lbl_false ⇒ λ_.
    881878    〈translate_cond globals (find_local_env r lenv) lbl_true, lbl_false〉
    882879  | St_jumptable r l ⇒  λ_.? (* assert false: not implemented yet *)
    883   | St_return ⇒ λeq_stmt.⊥
     880  | _ ⇒ λeq_stmt.⊥
    884881  ] (refl …).
    885   [11: cases not_implemented (* jtable case *)
    886   |12: >eq_stmt in stmt_prf; normalize //
     882  [12: cases not_implemented (* jtable case *)
     883  |10,11,13: >eq_stmt in stmt_prf; normalize //
    887884  |*: cases daemon
    888885  (* TODO: proofs regarding lengths of lists, examine! *)
     
    895892  match stmt return λx.stmt = x → rtl_internal_function globals with
    896893  [ St_return ⇒ λ_.add_graph rtl_params globals lbl (RETURN …) def
     894  | St_tailcall_id f args ⇒ λ_.
     895    add_graph rtl_params globals lbl
     896      (extension_fin rtl_params globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) def
     897  | St_tailcall_ptr f args ⇒ λ_.
     898    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
     899    add_graph rtl_params globals lbl
     900      (extension_fin rtl_params globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) def
    897901  | _ ⇒ λstmt_eq.
    898902    let 〈translation, lbl'〉 ≝ translate_inst globals lenv stmt ? in
    899903    rtl_adds_graph globals translation lbl lbl' def
    900904  ] (refl …).
    901 >stmt_eq normalize % qed.
     905[10: cases daemon (* length of address lookup *)
     906|*: >stmt_eq normalize %] qed.
    902907 
    903908 
Note: See TracChangeset for help on using the changeset viewer.