Changeset 736 for src/common/Graphs.ma


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/Graphs.ma

    r728 r736  
    22
    33include "ASM/BitVectorTrie.ma".
    4 include "Clight/AST.ma".
    5 include "common/Errors.ma".
     4include "common/Identifiers.ma".
    65
    7 definition label ≝ ident.
     6axiom LabelTag : String.
    87
    9 definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ ident_eq.
     8definition label ≝ Identifier LabelTag.
    109
    11 record label_generation : Type[0] ≝ { lab_next : label }.
     10definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?.
    1211
    13 definition label_gen_new : label_generation ≝ mk_label_generation (zero ?).
    1412
    15 definition 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 
    21 definition graph : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16.
    22 definition empty_graph : ∀T. graph T ≝ λT. Stub T 16.
    23 definition graph_lookup : ∀T. graph T → label → option T ≝
    24 λT,g,l. lookup_opt T 16 l g.
    25 definition graph_add : ∀T. graph T → label → T → graph T ≝
    26 λT,g,l,v. insert T 16 l v g.
     13definition graph : Type[0] → Type[0] ≝ IdentifierMap LabelTag.
Note: See TracChangeset for help on using the changeset viewer.