Changeset 1515 for src/RTLabs


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/RTLabs/RTLabsToRTL.ma

    r1408 r1515  
    5959  | register_ptr: register → register → register_type.
    6060
    61 definition local_env ≝ BitVectorTrie (list register) 16.
     61definition local_env ≝ identifier_map RegisterTag (list register).
    6262
    6363definition mem_local_env : register → local_env → bool ≝
    64   λr. member … (word_of_identifier … r).
     64  λr,e. member … e r.
    6565
    6666definition add_local_env : register → list register → local_env → local_env ≝
    67   λr. insert … (word_of_identifier … r).
     67  λr,v,e. add … e r v.
    6868
    6969definition find_local_env : register → local_env → list register ≝
    70   λr: register.λbvt. lookup … (word_of_identifier … r) bvt [].
     70  λr: register.λenv. lookup_def … env r [].
    7171
    7272definition initialize_local_env_internal ≝
     
    8989    ]
    9090  in
    91     foldl … initialize_local_env_internal 〈Stub …,runiverse〉 registers.
     91    foldl … initialize_local_env_internal 〈empty_map …,runiverse〉 registers.
    9292
    9393definition map_list_local_env_internal ≝
Note: See TracChangeset for help on using the changeset viewer.