Changeset 1644 for src/RTLabs


Ignore:
Timestamp:
Jan 13, 2012, 3:08:55 PM (8 years ago)
Author:
tranquil
Message:

minor changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r1643 r1644  
    196196  | _ ⇒ True
    197197  ].
    198 
    199198definition translate_cst :
    200199  ∀globals: list ident.
     
    219218    | Oaddrstack offset ⇒ λeqcst.
    220219      let 〈r1, r2〉 ≝ make_addr … destrs ? in
    221       [extension rtl_params globals (rtl_st_ext_stack_address r1 r2)]
     220      [(rtl_st_ext_stack_address r1 r2 : rtl_instruction globals)]
    222221    ] (refl …)
    223222  ] (refl …).
     
    822821  | _ ⇒ True ].
    823822
    824 (* XXX: following conversation with CSC about the mix up in extension statements
    825         and extension instructions in RTL, use fake_label in calls to
    826         tailcall_* instructions. *)
    827823definition translate_inst : ∀globals.?→?→?→
    828824  (bind_list register unit (rtl_instruction globals)) × label ≝
     
    869865    (* Paolo: no notation to avoid ambiguity *)
    870866    〈bcons … (
    871       match retr with
     867      match retr return λ_.rtl_instruction globals with
    872868      [ Some retr ⇒
    873         extension rtl_params globals (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv))
     869        rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv)
    874870      | None ⇒
    875         extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])
     871        rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ]
    876872      ]) [ ], lbl'〉
    877873  | St_cond r lbl_true lbl_false ⇒ λ_.
     
    894890  | St_tailcall_id f args ⇒ λ_.
    895891    add_graph rtl_params globals lbl
    896       (extension_fin rtl_params globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) def
     892      (extension_fin (rtl_st_ext_tailcall_id f (rtl_args args lenv))) def
    897893  | St_tailcall_ptr f args ⇒ λ_.
    898894    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    899895    add_graph rtl_params globals lbl
    900       (extension_fin rtl_params globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) def
     896      (extension_fin (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) def
    901897  | _ ⇒ λstmt_eq.
    902898    let 〈translation, lbl'〉 ≝ translate_inst globals lenv stmt ? in
     
    935931  let entry' ≝ f_entry def in
    936932  let exit' ≝ f_exit def in
    937   let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry'
    938     (GOTO (rtl_params : params) globals entry') in
     933  let graph' ≝ empty_map LabelTag ? in
     934  let graph' ≝ add LabelTag ? graph' entry'
     935    (GOTO … exit') in
    939936  let graph' ≝ add LabelTag ? graph' exit'
    940     (RETURN (rtl_params : params) globals) in
     937    (RETURN ) in
    941938  let res ≝
    942939    mk_joint_internal_function globals rtl_params luniverse' runiverse' result' params'
    943940     locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in
    944941    foldi … (translate_stmt globals … lenv) (f_graph def) res.
    945 [ @graph_add_lookup @graph_add
    946 | @graph_add ]
     942[ @graph_add_lookup ] @graph_add
    947943qed.
    948944
Note: See TracChangeset for help on using the changeset viewer.