Changeset 726 for src/common/Graphs.ma


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

Change identifiers to Words in Clight and RTLabs semantics.

File:
1 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.
Note: See TracChangeset for help on using the changeset viewer.