source: src/common/Graphs.ma @ 710

Last change on this file since 710 was 710, checked in by campbell, 9 years ago

Start of way to import RTLabs from prototype compiler.

File size: 884 bytes
Line 
1
2include "basics/logic.ma".
3
4include "utilities/binary/positive.ma".
5include "common/Maps.ma".
6
7definition label : Type[0] ≝ Pos.
8definition graph : Type[0] → Type[0] ≝ tree_t … PTree.
9definition graph_lookup : ∀T. graph T → label → option T ≝
10λT,g,l. get … l g.
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.
14
15definition 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.
18
19record label_generation : Type[0] ≝ { label_next : label }.
20
21definition label_new : label_generation → label × label_generation ≝
22λg. 〈label_next g, mk_label_generation (succ (label_next g))〉.
23
24definition label_gen_new : label_generation ≝ mk_label_generation one.
Note: See TracBrowser for help on using the repository browser.