Ignore:
Timestamp:
Apr 4, 2011, 5:13:08 PM (9 years ago)
Author:
campbell
Message:

Extra type safety for identifiers.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Registers.ma

    r726 r736  
    55
    66include "ASM/BitVectorTrie.ma".
    7 include "Clight/AST.ma".
    8 include "common/Errors.ma".
     7include "common/Identifiers.ma".
    98
    10 definition register ≝ ident.
     9axiom RegisterTag : String.
    1110
    12 definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ ident_eq.
     11definition register ≝ Identifier RegisterTag.
    1312
    14 record register_generation : Type[0] ≝ { reg_next : register }.
     13definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ identifier_eq ?.
    1514
    16 definition register_gen_new : register_generation ≝ mk_register_generation (zero ?).
    17 
    18 definition register_new : register_generation → res (register × register_generation) ≝
    19 λg. let 〈gen, carries〉 ≝ add_with_carries ? (reg_next g) (zero ?) true in
    20     if get_index_v ?? carries 0 ? then Error ? else
    21       OK ? 〈reg_next g, mk_register_generation gen〉.
    22 // qed.
    23 
    24 definition register_env : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16.
    25 definition register_empty : ∀T. register_env T ≝ λT. Stub T 16.
    26 definition register_lookup : ∀T. register_env T → register → option T ≝
    27 λT,g,l. lookup_opt T 16 l g.
    28 definition register_update : ∀T. register → T → register_env T → register_env T ≝
    29 λT,l,v,g. insert T 16 l v g.
     15definition register_env ≝ IdentifierMap RegisterTag.
Note: See TracChangeset for help on using the changeset viewer.