Changeset 1077 for src/RTL/RTLtoERTL.ma


Ignore:
Timestamp:
Jul 19, 2011, 12:23:32 PM (9 years ago)
Author:
mulligan
Message:

ack, dependent types are scary

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r1076 r1077  
    77  λl: label.
    88  λp: ertl_internal_function.
     9  λprf: lookup ? ? (ertl_if_graph p) l ≠ None ?.
    910  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
    1011  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
     
    1819                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    1920                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
     21  @prf
     22qed.
    2023
    2124definition change_entry_label ≝
    2225  λl: label.
    2326  λp: ertl_internal_function.
     27  λprf: lookup ? ? (ertl_if_graph p) l ≠ None ?.
    2428  let ertl_if_luniverse' ≝ ertl_if_luniverse p in
    2529  let ertl_if_runiverse' ≝ ertl_if_runiverse p in
     
    3337                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    3438                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
     39  @prf
     40qed.
    3541                             
    3642definition add_graph ≝
     
    4854    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
    4955                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    50                               ertl_if_graph' ertl_if_entry' ertl_if_exit'.
     56                              ertl_if_graph' ? ?.
     57  normalize nodelta;
     58  [1: generalize in match ertl_if_entry';
     59      #HYP
     60      cases HYP
     61      #LBL #LBL_PRF
     62      %
     63      [1: @LBL
     64      |2: @graph_add_lookup
     65          @LBL_PRF
     66      ]
     67  |2: generalize in match ertl_if_exit';
     68      #HYP
     69      cases HYP
     70      #LBL #LBL_PRF
     71      %
     72      [1: @LBL
     73      |2: @graph_add_lookup
     74          @LBL_PRF
     75      ]
     76  ]
     77qed.
    5178                             
    5279definition fresh_label ≝
     
    325352    in
    326353    let def ≝ add_graph tmp_lbl last_stmt def in
    327       change_exit_label tmp_lbl def
     354      change_exit_label tmp_lbl def ?
    328355  ] ?.
    329   cases not_implemented (* dep types here *)
     356  cases not_implemented (* dep types here, bug in matita too! *)
    330357qed.
    331358 
     
    471498      ertl_st_get_hdw r2 RegisterSPH lbl
    472499    ] lbl lbl' def
    473   | rtl_st_int r i lbl' ⇒ add_graph lbl (ertl_st_int r i lbl') def
     500  | rtl_st_int r i lbl' ⇒  add_graph lbl (ertl_st_int r i lbl') def
    474501  | rtl_st_move r1 r2 lbl' ⇒ add_graph lbl (ertl_st_move r1 r2 lbl') def
    475502  | rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒
     
    506533  let added_stacksize ≝ max 0 (nb_params - |parameters|) in
    507534  let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in
     535  let entry' ≝ rtl_if_entry def in
     536  let exit' ≝ rtl_if_exit def in
    508537  let def' ≝
    509538    mk_ertl_internal_function
    510539      (rtl_if_luniverse def) (rtl_if_runiverse def)
    511540      nb_params new_locals ((rtl_if_stacksize def) + added_stacksize)
    512       (empty_map ? ?) (rtl_if_entry def) (rtl_if_exit def) in
    513   let def' ≝ fold ? ? translate_stmt (rtl_if_graph def) def' in
     541      (empty_map ? ?) ? ? in
     542  let def' ≝ foldi ? ? ? translate_stmt (rtl_if_graph def) def' in
    514543  let def' ≝ add_pro_and_epilogue (rtl_if_params def) (rtl_if_result def) def' in
    515544    def'.
     545  [1: cases entry'
     546      #LBL #LBL_PRF
     547      %
     548      [1: @LBL
     549      |2: @LBL_PRF
    516550   
    517551definition translate_funct ≝
     
    520554  let def' ≝
    521555    match def with
    522     [ rtl_f_internal def ⇒ ertl_f_internal (translate_funct_internal def)
    523     | rtl_f_external def ⇒ ertl_f_external def
     556    [ Internal def ⇒ Internal ? (translate_funct_internal def)
     557    | External def ⇒ External ? def
    524558    ] in
    525559  〈id, def'〉.
    526    
    527    
     560
     561definition generate ≝
     562  λstmt.
     563  λdef.
     564  let 〈entry, nuniv〉 ≝ fresh_label def in
     565  let graph ≝ add ? ? (ertl_if_graph def) entry stmt in
     566    mk_ertl_internal_function
     567      nuniv (ertl_if_runiverse def) (ertl_if_params def)
     568      (ertl_if_locals def) (ertl_if_stacksize def) graph
     569      entry (ertl_if_exit def).
     570   
     571let generate stmt def =
     572  let entry = Label.Gen.fresh def.ERTL.f_luniverse in
     573  let def =
     574    { def with ERTL.f_graph = Label.Map.add entry stmt def.ERTL.f_graph } in
     575  { def with ERTL.f_entry = entry }
     576
     577
    528578definition save_return_internal ≝
    529579  λr.
Note: See TracChangeset for help on using the changeset viewer.