Changeset 1073

Timestamp:

Jul 15, 2011, 5:38:37 PM (9 years ago)

Author:

mulligan

Message:

more changes from today

File:

• src/RTLabs/RTLAbstoRTL.ma (modified) (3 diffs)

src/RTLabs/RTLAbstoRTL.ma

@@ -29 +29 @@
                              rtl_if_stacksize' rtl_if_graph' ? ?.
   [1: cases(rtl_if_entry')
-      #LABEL #HYP
-      %
+      #LABEL #HYP %
       [1: @LABEL
       |2: cases(HYP)
-          #STMT
-          #FRST_PRF
-          %
-          [1: @STMT
-          |2: <FRST_PRF @(graph_add_lookup (rtl_if_graph p) LABEL stmt)
-          ]
+          generalize in match (graph_add_lookup (rtl_if_graph p) LABEL stmt l);
+          /2/
       ]
-  
+  |2: cases(rtl_if_exit')
+      #LABEL #HYP %
+      [1: @LABEL
+      |2: cases(HYP)
+          generalize in match (graph_add_lookup (rtl_if_graph p) LABEL stmt l);
+          /2/
+      ]
+  ]
+qed.
       
 definition fresh_label: rtl_internal_function → rtl_internal_function × label ≝
@@ -1219 +1222 @@
 qed.
 
+axiom graph_add:
+  ∀g: graph rtl_statement.
+  ∀l: label.
+  ∀s: rtl_statement.
+    lookup ? ? (add ? ? g l s) l ≠ None ?.
+
+(* XXX: we use a "hack" here to circumvent the proof obligations required to
+   create res, an empty internal_function record.  we insert into our graph
+   the start and end nodes to ensure that they are in, and place dummy
+   skip instructions at these nodes. *)
 definition translate_internal ≝
   λdef.
@@ -1240 +1253 @@
   let locals' ≝ locals in
   let stack_size' ≝ f_stacksize def in
-  let graph' ≝ empty_map ? ? in
   let entry' ≝ f_entry def in
   let exit' ≝ f_exit def in
+  let graph' ≝ add ? ? (empty_map ? ?) entry' (rtl_st_skip entry') in
+  let graph' ≝ add ? ? graph' exit' (rtl_st_skip exit') in
   let res ≝
     mk_rtl_internal_function luniverse' runiverse' result' params'
-                         locals' stack_size' graph' entry' exit' in
+                         locals' stack_size' graph' ? ? in
     fold ? ? ? (translate_stmt lenv) (f_graph def) res.
+  [1: %
+      [1: @entry'
+      |2: normalize nodelta;
+          @(graph_add ? (f_entry def) ?)
+          @graph_add_lookup
+      ]
+  |2: %
+      [1: @exit'
+      |2: /2/
+      ]
+  ]
+qed.
 
 definition translate_fun_def ≝