Changeset 1515 for src/Clight/toCminor.ma

Timestamp:

Nov 18, 2011, 1:03:14 PM (8 years ago)

Author:

campbell

Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

• fix interpretation for - on positives
• move eq_nat_dec to a more appropriate place
• split out costs from other identifiers in ASM
• use identifier abstractions in back-end

File:

• src/Clight/toCminor.ma (modified) (7 diffs)

src/Clight/toCminor.ma

@@ -125 +125 @@
 cases (identifier_eq ? id id')
 [ #E >E >lookup_add_hit whd in ⊢ (% → ?) *
-| #NE >lookup_add_miss // @eq_identifier_elim // #E >E in NE * /2/
+| #NE >lookup_add_miss /2/
 ] qed.
 
@@ -134 +134 @@
 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ])
 >lookup_add_miss
-[ #H @H | @eq_identifier_elim // #E >E in NE * /2/ ]
+[ #H @H | /2/ ]
 qed.
 
@@ -737 +737 @@
   〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'.
 #tmp #g #g' #vars #q
-whd in ⊢ (???% → ?)
-generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?)
-* #tmp' #u whd in ⊢ (???% → ?) #E
-destruct
+whd in ⊢ (???% → ?) #E
 #id #H
+cases (identifier_eq ? id tmp)
+destruct #E
 whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]
-cases (identifier_eq ? id tmp')
-[ #E1 >E1 >lookup_add_hit @I
-| * #NE >lookup_add_miss [ @H | @eq_identifier_elim // #E1 cases (NE E1)
+[ >E >lookup_add_hit @I
+| cases E #NE >lookup_add_miss [ @H | /2/
 ] qed.
 
@@ -770 +768 @@
 cases (identifier_eq ? id id')
 [ #E >E >lookup_add_hit @I
-| * #NE >lookup_add_miss [ @H | @eq_identifier_elim // #E cases (NE E)
+| #NE >lookup_add_miss [ @H | /2/ 
 ] qed.
 
@@ -793 +791 @@
   〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp.
 #tmp #u #q #u0 #vars
-whd in ⊢ (???% → ?)
-generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?)
-* #tmp' #u' whd in ⊢ (???% → ?) #E
+whd in ⊢ (???% → ?) #E
 destruct
 whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ] >lookup_add_hit
@@ -997 +993 @@
   l0 ≠ l →
   lookup_label (add … lbls l l') l0 = lookup_label lbls l0.
-#lbls #l #l' #l0 * #NE
+#lbls #l #l' #l0 #NE
 whd in ⊢ (??%%)
 >lookup_add_miss
-[ @refl | @(eq_identifier_elim ?? l0 l)
-  [ #E cases (NE E)
-  | #_ @I
-  ]
-]
+[ @refl | @NE ]
 qed.  
 
@@ -1048 +1040 @@
   cases (identifier_eq ? i id)
   [ #E >E #H %2 whd %1 @refl
-  | * #NE #H cases (IH ?)
+  | #NE #H cases (IH ?)
     [ #H' %1 @H'
     | #H' %2 %2 @H'
     | whd in H; whd in H:(match % with [ _ ⇒ ? | _ ⇒ ? ]);
-      >lookup_add_miss in H; [ #H @H | @eq_identifier_elim // #E cases (NE E) ]
+      >lookup_add_miss in H; [ #H @H | @NE ]
     ]
   ]