Changeset 1077


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

ack, dependent types are scary

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1071 r1077  
    4747  ertl_if_stacksize: nat;
    4848  ertl_if_graph: ertl_statement_graph;
    49   ertl_if_entry: label;
    50   ertl_if_exit: label
     49  ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?;
     50  ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?
    5151}.
    5252
  • 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.
  • src/RTLabs/RTLAbstoRTL.ma

    r1073 r1077  
    44include "common/FrontEndOps.ma".
    55include "common/Graphs.ma".
    6 
    7 axiom graph_add_lookup:
    8   ∀g: graph rtl_statement.
    9   ∀l: label.
    10   ∀s: rtl_statement.
    11   ∀to_insert: label.
    12     lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
    136
    147definition add_graph ≝
     
    3225      [1: @LABEL
    3326      |2: cases(HYP)
    34           generalize in match (graph_add_lookup (rtl_if_graph p) LABEL stmt l);
     27          generalize in match (graph_add_lookup ? (rtl_if_graph p) LABEL stmt l);
     28          normalize nodelta;
    3529          /2/
    3630      ]
     
    3933      [1: @LABEL
    4034      |2: cases(HYP)
    41           generalize in match (graph_add_lookup (rtl_if_graph p) LABEL stmt l);
     35          generalize in match (graph_add_lookup ? (rtl_if_graph p) LABEL stmt l);
     36          normalize nodelta;
    4237          /2/
    4338      ]
     
    12221217qed.
    12231218
    1224 axiom graph_add:
    1225   ∀g: graph rtl_statement.
    1226   ∀l: label.
    1227   ∀s: rtl_statement.
    1228     lookup ? ? (add ? ? g l s) l ≠ None ?.
    1229 
    12301219(* XXX: we use a "hack" here to circumvent the proof obligations required to
    12311220   create res, an empty internal_function record.  we insert into our graph
     
    12601249    mk_rtl_internal_function luniverse' runiverse' result' params'
    12611250                         locals' stack_size' graph' ? ? in
    1262     fold ? ? ? (translate_stmt lenv) (f_graph def) res.
     1251    foldi ? ? ? (translate_stmt lenv) (f_graph def) res.
    12631252  [1: %
    12641253      [1: @entry'
    12651254      |2: normalize nodelta;
    1266           @(graph_add ? (f_entry def) ?)
    12671255          @graph_add_lookup
     1256          @graph_add
    12681257      ]
    12691258  |2: %
    12701259      [1: @exit'
    1271       |2: /2/
     1260      |2: normalize nodelta;
     1261          @graph_add
    12721262      ]
    12731263  ]
     
    12811271  ].
    12821272
     1273(* XXX: change, we need to propagate the region information, not ignore it *)
    12831274definition init_data_to_nat ≝
    12841275  λi: init_data.
  • src/common/Graphs.ma

    r746 r1077  
    1111
    1212definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag.
     13
     14axiom graph_add:
     15  ∀A: Type[0].
     16  ∀g: graph A.
     17  ∀l: label.
     18  ∀s: A.
     19    lookup ? ? (add ? ? g l s) l ≠ None ?.
     20
     21axiom graph_add_lookup:
     22  ∀A: Type[0].
     23  ∀g: graph A.
     24  ∀l: label.
     25  ∀s: A.
     26  ∀to_insert: label.
     27    lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
  • src/common/Identifiers.ma

    r1072 r1077  
    139139  ].
    140140
    141 axiom fold:
     141axiom foldi:
    142142  ∀A, B: Type[0].
    143143  ∀tag: String.
Note: See TracChangeset for help on using the changeset viewer.