Changeset 2674 for src/RTLabs


Ignore:
Timestamp:
Feb 18, 2013, 5:48:19 PM (7 years ago)
Author:
tranquil
Message:
  • another change in block definition
  • RTLabs -> RTL and ERTL -> ERTLptr passes fixed, others stil broken
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r2640 r2674  
    362362@IH qed.
    363363
    364 lemma last_last_ne : ∀A,l.last A (pi1 … l) = Some ? (last_ne … l).
    365 #A * @list_elim_left [*] #hd #tl #_ #prf
    366 whd in match last_ne; normalize nodelta
    367 >split_on_last_ne_def @last_def qed.
    368 
    369364lemma last_not_empty : ∀A,l.not_empty A l →
    370365  match last A l with
    371366  [ None ⇒ False
    372367  | _ ⇒ True ].
    373 #A #l #prf >(last_last_ne … «l, prf») % qed.
     368#A @list_elim_left [*] #pref #last #_ #_ >last_def % qed.
    374369
    375370definition translate_op_asym_signed :
     
    858853  | cons srcr srcrs' ⇒
    859854    ν tmpr in
    860     let f : register → joint_seq RTL globals ≝
    861       λr. tmpr ← tmpr .Or. r in
    862     bret … ((MOVE RTL globals 〈tmpr,srcr〉 ::
    863     map ?? f srcrs' : list (joint_step ??)) @ [COND … tmpr lbl_true])
     855    let f : register → label → joint_seq RTL globals ≝
     856      λr.λ_. tmpr ← tmpr .Or. r in
     857    bret …
     858    〈(λ_.MOVE RTL globals 〈tmpr,srcr〉) ::
     859     map ?? f srcrs',
     860     λ_.COND … tmpr lbl_true, [ ]〉
    864861  ].
    865862
     
    940937qed.
    941938
     939(* TODO: move it *)
    942940definition ensure_bind_step_block : ∀p : params.∀g.
    943   bind_new register (list (joint_step p g)) → bind_step_block p g ≝
    944   λp,g,b.! l ← b; bret ? (step_block p g) l.
    945 
    946 definition ensure_bind_step_block_from_seq : ∀p : params.∀g.
    947941  bind_new register (list (joint_seq p g)) → bind_step_block p g ≝
    948942  λp,g,b.! l ← b; bret ? (step_block p g) l.
     
    950944coercion bind_step_block_from_bind_list nocomposites :
    951945  ∀p : params.∀g.
    952   ∀b : bind_new register (list (joint_step p g)).bind_step_block p g ≝
    953   ensure_bind_step_block on _b : bind_new register (list (joint_step ??)) to
    954   bind_step_block ??.
    955 
    956 coercion bind_step_block_from_bind_seq_list nocomposites :
    957   ∀p : params.∀g.
    958946  ∀b : bind_new register (list (joint_seq p g)).bind_step_block p g ≝
    959   ensure_bind_step_block_from_seq on _b : bind_new register (list (joint_seq ??)) to
     947  ensure_bind_step_block on _b : bind_new register (list (joint_seq ??)) to
    960948  bind_step_block ??.
    961949
     
    993981      (find_local_env_arg srcr lenv ?)), lbl'❭
    994982  | St_call_id f args retr lbl' ⇒ λstmt_typed.
    995     ❬inl ?? (bret ?? [CALL RTL ? (inl … f) (rtl_args args lenv ?)
    996       (match retr with
    997       [ Some retr ⇒ find_local_env retr lenv ?
    998       | None ⇒ [ ]
    999       ])]), lbl'❭
     983    ❬inl … (bret …
     984      〈[ ],λ_.CALL RTL ? (inl ?? f) (rtl_args args lenv ?)
     985        (match retr with
     986         [ Some retr ⇒
     987           find_local_env retr lenv ?
     988         | None ⇒ [ ]
     989         ]), [ ]〉), lbl'❭
    1000990  | St_call_ptr f args retr lbl' ⇒ λstmt_typed.
    1001991    let fs ≝ find_and_addr_arg f lenv ?? in
    1002     ❬inl … (bret … [CALL RTL ? (inr ?? fs) (rtl_args args lenv ?)
    1003       (match retr with
    1004        [ Some retr ⇒
    1005          find_local_env retr lenv ?
    1006        | None ⇒ [ ]
    1007        ])]), lbl'❭
     992    ❬inl … (bret …
     993      〈[ ],λ_.CALL RTL ? (inr ?? fs) (rtl_args args lenv ?)
     994        (match retr with
     995         [ Some retr ⇒
     996           find_local_env retr lenv ?
     997         | None ⇒ [ ]
     998         ]), [ ]〉), lbl'❭
    1008999  | St_cond r lbl_true lbl_false ⇒ λstmt_typed.
    10091000    ❬inl … (translate_cond globals (find_local_env r lenv ?) lbl_true), lbl_false❭
     
    10411032  let stack_size' ≝ f_stacksize def in
    10421033  let entry' ≝ f_entry def in
    1043   let init ≝ init_graph_if RTL globals luniverse' runiverse' [ ]
    1044      [ ] stack_size' (pi1 … entry') in
     1034  let init ≝ mk_joint_internal_function RTL globals
     1035    luniverse' runiverse' [ ] [ ] stack_size'
     1036    (add … (empty_map ? (joint_statement ??)) entry' (RETURN …)) (pi1 … entry') in
    10451037  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
    10461038    (f_locals def) (f_params def) (f_result def) init in
     
    10531045    | inr instrs ⇒ λ_.b_fin_adds_graph … instrs lbl def
    10541046    ] (dpi2 … pr) in
    1055   foldi … f_trans (f_graph def) init'. (* TODO *) cases daemon
     1047  foldi … f_trans (f_graph def) init'.
     1048[4: >graph_code_has_point @mem_set_add_id ] 
     1049(* TODO *) cases daemon
    10561050qed.
    10571051
Note: See TracChangeset for help on using the changeset viewer.