Changeset 710


Ignore:
Timestamp:
Mar 25, 2011, 6:37:49 PM (9 years ago)
Author:
campbell
Message:

Start of way to import RTLabs from prototype compiler.

Location:
src
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Graphs.ma

    r702 r710  
    99definition graph_lookup : ∀T. graph T → label → option T ≝
    1010λT,g,l. get … l g.
    11 
     11definition graph_add : ∀T. graph T → label → T → graph T ≝
     12λT,g,l,t. set … l t g.
     13definition empty_graph : ∀T. graph T ≝ λT. empty ? PTree T.
    1214
    1315definition label_eq : ∀x,y:label. (x=y) + (x≠y).
     
    1921definition label_new : label_generation → label × label_generation ≝
    2022λg. 〈label_next g, mk_label_generation (succ (label_next g))〉.
     23
     24definition label_gen_new : label_generation ≝ mk_label_generation one.
  • src/common/Registers.ma

    r702 r710  
    1515record register_generation : Type[0] ≝ { reg_next : register }.
    1616
     17definition register_gen_new : register_generation ≝ mk_register_generation one.
     18
    1719definition register_new : register_generation → register × register_generation ≝
    1820λg. 〈reg_next g, mk_register_generation (succ (reg_next g))〉.
Note: See TracChangeset for help on using the changeset viewer.