Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1369 r1515  
    125125cases (identifier_eq ? id id')
    126126[ #E >E >lookup_add_hit whd in ⊢ (% → ?) *
    127 | #NE >lookup_add_miss // @eq_identifier_elim // #E >E in NE * /2/
     127| #NE >lookup_add_miss /2/
    128128] qed.
    129129
     
    134134whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ])
    135135>lookup_add_miss
    136 [ #H @H | @eq_identifier_elim // #E >E in NE * /2/ ]
     136[ #H @H | /2/ ]
    137137qed.
    138138
     
    737737  〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'.
    738738#tmp #g #g' #vars #q
    739 whd in ⊢ (???% → ?)
    740 generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?)
    741 * #tmp' #u whd in ⊢ (???% → ?) #E
    742 destruct
     739whd in ⊢ (???% → ?) #E
    743740#id #H
     741cases (identifier_eq ? id tmp)
     742destruct #E
    744743whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]
    745 cases (identifier_eq ? id tmp')
    746 [ #E1 >E1 >lookup_add_hit @I
    747 | * #NE >lookup_add_miss [ @H | @eq_identifier_elim // #E1 cases (NE E1)
     744[ >E >lookup_add_hit @I
     745| cases E #NE >lookup_add_miss [ @H | /2/
    748746] qed.
    749747
     
    770768cases (identifier_eq ? id id')
    771769[ #E >E >lookup_add_hit @I
    772 | * #NE >lookup_add_miss [ @H | @eq_identifier_elim // #E cases (NE E)
     770| #NE >lookup_add_miss [ @H | /2/
    773771] qed.
    774772
     
    793791  〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp.
    794792#tmp #u #q #u0 #vars
    795 whd in ⊢ (???% → ?)
    796 generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?)
    797 * #tmp' #u' whd in ⊢ (???% → ?) #E
     793whd in ⊢ (???% → ?) #E
    798794destruct
    799795whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ] >lookup_add_hit
     
    997993  l0 ≠ l →
    998994  lookup_label (add … lbls l l') l0 = lookup_label lbls l0.
    999 #lbls #l #l' #l0 * #NE
     995#lbls #l #l' #l0 #NE
    1000996whd in ⊢ (??%%)
    1001997>lookup_add_miss
    1002 [ @refl | @(eq_identifier_elim ?? l0 l)
    1003   [ #E cases (NE E)
    1004   | #_ @I
    1005   ]
    1006 ]
     998[ @refl | @NE ]
    1007999qed. 
    10081000
     
    10481040  cases (identifier_eq ? i id)
    10491041  [ #E >E #H %2 whd %1 @refl
    1050   | * #NE #H cases (IH ?)
     1042  | #NE #H cases (IH ?)
    10511043    [ #H' %1 @H'
    10521044    | #H' %2 %2 @H'
    10531045    | whd in H; whd in H:(match % with [ _ ⇒ ? | _ ⇒ ? ]);
    1054       >lookup_add_miss in H; [ #H @H | @eq_identifier_elim // #E cases (NE E) ]
     1046      >lookup_add_miss in H; [ #H @H | @NE ]
    10551047    ]
    10561048  ]
Note: See TracChangeset for help on using the changeset viewer.