Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (9 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/joint/SemanticUtils.ma

    r1452 r1515  
    2525 λoldpc,l.
    2626  mk_pointer Code
    27    (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (nat_of_bitvector ? (word_of_identifier … l))).
     27   (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))).
    2828// qed.
    2929
     
    3434
    3535definition graph_label_of_pointer: pointer → res label ≝
    36  λp. OK … (an_identifier ? (bitvector_of_nat … (abs (offv (poff p))))).
     36 λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).
    3737
    3838(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
Note: See TracChangeset for help on using the changeset viewer.