Ignore:
Timestamp:
Mar 30, 2011, 6:47:35 PM (10 years ago)
Author:
campbell
Message:

Change identifiers to Words in Clight and RTLabs semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Registers.ma

    r710 r726  
    33
    44include "basics/types.ma".
    5 include "utilities/binary/positive.ma".
    65
    7 include "common/Maps.ma".
     6include "ASM/BitVectorTrie.ma".
     7include "Clight/AST.ma".
     8include "common/Errors.ma".
    89
    9 definition register ≝ Pos.
     10definition register ≝ ident.
    1011
    11 definition register_eq : ∀x,y:register. (x=y) + (x≠y).
    12 #x #y lapply (pos_compare_to_Prop x y); cases (pos_compare x y);
    13 [ #H %2 /2/; | #H %1 //; | #H %2 /2/ ] qed.
     12definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ ident_eq.
    1413
    1514record register_generation : Type[0] ≝ { reg_next : register }.
    1615
    17 definition register_gen_new : register_generation ≝ mk_register_generation one.
     16definition register_gen_new : register_generation ≝ mk_register_generation (zero ?).
    1817
    19 definition register_new : register_generation → register × register_generation ≝
    20 λg. 〈reg_next g, mk_register_generation (succ (reg_next g))〉.
     18definition 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.
    2123
    22 definition register_env : Type[0] → Type[0] ≝ tree_t … PTree.
    23 definition register_empty : ∀T. register_env T ≝ λT. empty ? PTree T.
     24definition register_env : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16.
     25definition register_empty : ∀T. register_env T ≝ λT. Stub T 16.
    2426definition register_lookup : ∀T. register_env T → register → option T ≝
    25 λT,g,l. get … l g.
     27λT,g,l. lookup_opt T 16 l g.
    2628definition register_update : ∀T. register → T → register_env T → register_env T ≝
    27 λT,l,v,g. set … l v g.
     29λT,l,v,g. insert T 16 l v g.
Note: See TracChangeset for help on using the changeset viewer.