Changeset 1077 for src/RTLabs

Timestamp:

Jul 19, 2011, 12:23:32 PM (8 years ago)

Author:

mulligan

Message:

ack, dependent types are scary

File:

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

src/RTLabs/RTLAbstoRTL.ma

@@ -4 +4 @@
 include "common/FrontEndOps.ma".
 include "common/Graphs.ma".
-
-axiom graph_add_lookup:
-  ∀g: graph rtl_statement.
-  ∀l: label.
-  ∀s: rtl_statement.
-  ∀to_insert: label.
-    lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
 
 definition add_graph ≝
@@ -32 +25 @@
       [1: @LABEL
       |2: cases(HYP)
-          generalize in match (graph_add_lookup (rtl_if_graph p) LABEL stmt l);
+          generalize in match (graph_add_lookup ? (rtl_if_graph p) LABEL stmt l);
+          normalize nodelta;
           /2/
       ]
@@ -39 +33 @@
       [1: @LABEL
       |2: cases(HYP)
-          generalize in match (graph_add_lookup (rtl_if_graph p) LABEL stmt l);
+          generalize in match (graph_add_lookup ? (rtl_if_graph p) LABEL stmt l);
+          normalize nodelta;
           /2/
       ]
@@ -1222 +1217 @@
 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
@@ -1260 +1249 @@
     mk_rtl_internal_function luniverse' runiverse' result' params'
                          locals' stack_size' graph' ? ? in
-    fold ? ? ? (translate_stmt lenv) (f_graph def) res.
+    foldi ? ? ? (translate_stmt lenv) (f_graph def) res.
   [1: %
       [1: @entry'
       |2: normalize nodelta;
-          @(graph_add ? (f_entry def) ?)
           @graph_add_lookup
+          @graph_add
       ]
   |2: %
       [1: @exit'
-      |2: /2/
+      |2: normalize nodelta;
+          @graph_add
       ]
   ]
@@ -1281 +1271 @@
   ].
 
+(* XXX: change, we need to propagate the region information, not ignore it *)
 definition init_data_to_nat ≝
   λi: init_data.