Changeset 726 for src/common


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

Change identifiers to Words in Clight and RTLabs semantics.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Graphs.ma

    r710 r726  
     1include "basics/types.ma".
    12
    2 include "basics/logic.ma".
     3include "ASM/BitVectorTrie.ma".
     4include "Clight/AST.ma".
     5include "common/Errors.ma".
    36
    4 include "utilities/binary/positive.ma".
    5 include "common/Maps.ma".
     7definition label ≝ ident.
    68
    7 definition label : Type[0] ≝ Pos.
    8 definition graph : Type[0] → Type[0] ≝ tree_t … PTree.
     9definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ ident_eq.
     10
     11record label_generation : Type[0] ≝ { lab_next : label }.
     12
     13definition label_gen_new : label_generation ≝ mk_label_generation (zero ?).
     14
     15definition label_new : label_generation → res (label × label_generation) ≝
     16λg. let 〈gen, carries〉 ≝ add_with_carries ? (lab_next g) (zero ?) true in
     17    if get_index_v ?? carries 0 ? then Error ? else
     18      OK ? 〈lab_next g, mk_label_generation gen〉.
     19// qed.
     20
     21definition graph : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16.
     22definition empty_graph : ∀T. graph T ≝ λT. Stub T 16.
    923definition graph_lookup : ∀T. graph T → label → option T ≝
    10 λT,g,l. get … l g.
     24λT,g,l. lookup_opt T 16 l g.
    1125definition graph_add : ∀T. graph T → label → T → graph T ≝
    12 λT,g,l,t. set … l t g.
    13 definition empty_graph : ∀T. graph T ≝ λT. empty ? PTree T.
     26λT,g,l,v. insert T 16 l v g.
    1427
    15 definition label_eq : ∀x,y:label. (x=y) + (x≠y).
    16 #x #y lapply (pos_compare_to_Prop x y); cases (pos_compare x y);
    17 [ #H %2 /2/; | #H %1 //; | #H %2 /2/ ] qed.
    1828
    19 record label_generation : Type[0] ≝ { label_next : label }.
    20 
    21 definition label_new : label_generation → label × label_generation ≝
    22 λg. 〈label_next g, mk_label_generation (succ (label_next g))〉.
    23 
    24 definition label_gen_new : label_generation ≝ mk_label_generation one.
  • 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.