Changeset 1071 for src/RTLabs

Timestamp:

Jul 15, 2011, 2:40:40 PM (10 years ago)

Author:

mulligan

Message:

changes the specific form that the added proofs take to use None, not Some, hence removing the exitential

Location:

src/RTLabs

Files:

• RTLAbstoRTL.ma (modified) (7 diffs)
• syntax.ma (modified) (1 diff)

src/RTLabs/RTLAbstoRTL.ma

@@ -2 +2 @@
 include "RTL/RTL.ma".
 include "common/AssocList.ma".
+include "common/FrontEndOps.ma".
 include "common/Graphs.ma".
-include "common/FrontEndOps.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 ≝
@@ -20 +27 @@
     mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse'
                              rtl_if_params' rtl_if_params' rtl_if_locals'
-                             rtl_if_stacksize' rtl_if_graph' rtl_if_entry'
-                             rtl_if_exit'.
+                             rtl_if_stacksize' rtl_if_graph' ? ?.
+  [1: cases(rtl_if_entry')
+      #LABEL #HYP
+      %
+      [1: @LABEL
+      |2: cases(HYP)
+          #STMT
+          #FRST_PRF
+          %
+          [1: @STMT
+          |2: <FRST_PRF @(graph_add_lookup (rtl_if_graph p) LABEL stmt)
+          ]
+      ]
+  
       
 definition fresh_label: rtl_internal_function → rtl_internal_function × label ≝
@@ -316 +335 @@
   λsrcrs: list register.
   λstart_lbl: label.
-    match reduce_strong register destrs srcrs with
+    match reduce_strong register register destrs srcrs with
     [ dp crl_crr len_proof ⇒
       let commonl ≝ \fst (\fst crl_crr) in
@@ -399 +418 @@
       translate_move destrs srcrs
     else
-      match reduce_strong ? destrs srcrs with
+      match reduce_strong register register destrs srcrs with
       [ dp crl len_proof ⇒
         let commonl ≝ \fst (\fst crl) in
@@ -510 +529 @@
   λdest_lbl.
   λdef.
-  match reduce_strong ? srcrs1 srcrs2 with
+  match reduce_strong register register srcrs1 srcrs2 with
   [ dp reduced first_reduced_proof ⇒
     let srcrsl_common ≝ \fst (\fst reduced) in
@@ -517 +536 @@
     let srcrsr_rest ≝ \snd (\snd reduced) in
     let srcrs_rest ≝ choose_rest ? srcrsl_rest srcrsr_rest ? ? in
-    match reduce_strong ? destrs srcrsl_common with
+    match reduce_strong register register destrs srcrsl_common with
     [ dp reduced second_reduced_proof ⇒
       let destrs_common ≝ \fst (\fst reduced) in
       let destrs_rest ≝ \snd (\fst reduced) in
-      match reduce_strong ? destrs_rest srcrs_rest with
+      match reduce_strong register register destrs_rest srcrs_rest with
       [ dp reduced third_reduced_proof ⇒
         let destrs_cted ≝ \fst (\fst reduced) in
@@ -704 +723 @@
     let 〈def, tmp_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
     let save_srcrs2 ≝ translate_move tmp_srcrs2 srcrs2 in
-    match reduce_strong ? tmp_srcrs1 tmp_srcrs2 with
+    match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with
     [ dp crl their_proof ⇒
       let commonl ≝ \fst (\fst crl) in

src/RTLabs/syntax.ma

@@ -35 +35 @@
 ; f_stacksize : nat
 ; f_graph     : graph statement
-; f_entry     : Σl:label. ∃s. lookup ?? f_graph l = Some ? s
-; f_exit      : Σl:label. ∃s. lookup ?? f_graph l = Some ? s
+; f_entry     : Σl:label. lookup ?? f_graph l ≠ None ?
+; f_exit      : Σl:label. lookup ?? f_graph l ≠ None ?
 }.