Changeset 1073


Ignore:
Timestamp:
Jul 15, 2011, 5:38:37 PM (8 years ago)
Author:
mulligan
Message:

more changes from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1071 r1073  
    2929                             rtl_if_stacksize' rtl_if_graph' ? ?.
    3030  [1: cases(rtl_if_entry')
    31       #LABEL #HYP
    32       %
     31      #LABEL #HYP %
    3332      [1: @LABEL
    3433      |2: cases(HYP)
    35           #STMT
    36           #FRST_PRF
    37           %
    38           [1: @STMT
    39           |2: <FRST_PRF @(graph_add_lookup (rtl_if_graph p) LABEL stmt)
    40           ]
     34          generalize in match (graph_add_lookup (rtl_if_graph p) LABEL stmt l);
     35          /2/
    4136      ]
    42  
     37  |2: cases(rtl_if_exit')
     38      #LABEL #HYP %
     39      [1: @LABEL
     40      |2: cases(HYP)
     41          generalize in match (graph_add_lookup (rtl_if_graph p) LABEL stmt l);
     42          /2/
     43      ]
     44  ]
     45qed.
    4346     
    4447definition fresh_label: rtl_internal_function → rtl_internal_function × label ≝
     
    12191222qed.
    12201223
     1224axiom graph_add:
     1225  ∀g: graph rtl_statement.
     1226  ∀l: label.
     1227  ∀s: rtl_statement.
     1228    lookup ? ? (add ? ? g l s) l ≠ None ?.
     1229
     1230(* XXX: we use a "hack" here to circumvent the proof obligations required to
     1231   create res, an empty internal_function record.  we insert into our graph
     1232   the start and end nodes to ensure that they are in, and place dummy
     1233   skip instructions at these nodes. *)
    12211234definition translate_internal ≝
    12221235  λdef.
     
    12401253  let locals' ≝ locals in
    12411254  let stack_size' ≝ f_stacksize def in
    1242   let graph' ≝ empty_map ? ? in
    12431255  let entry' ≝ f_entry def in
    12441256  let exit' ≝ f_exit def in
     1257  let graph' ≝ add ? ? (empty_map ? ?) entry' (rtl_st_skip entry') in
     1258  let graph' ≝ add ? ? graph' exit' (rtl_st_skip exit') in
    12451259  let res ≝
    12461260    mk_rtl_internal_function luniverse' runiverse' result' params'
    1247                          locals' stack_size' graph' entry' exit' in
     1261                         locals' stack_size' graph' ? ? in
    12481262    fold ? ? ? (translate_stmt lenv) (f_graph def) res.
     1263  [1: %
     1264      [1: @entry'
     1265      |2: normalize nodelta;
     1266          @(graph_add ? (f_entry def) ?)
     1267          @graph_add_lookup
     1268      ]
     1269  |2: %
     1270      [1: @exit'
     1271      |2: /2/
     1272      ]
     1273  ]
     1274qed.
    12491275
    12501276definition translate_fun_def ≝
Note: See TracChangeset for help on using the changeset viewer.