source: src/common/Graphs.ma @ 1082

Last change on this file since 1082 was 1082, checked in by mulligan, 9 years ago

work from today on ertl -> ltl pass

File size: 908 bytes
Line 
1include "basics/types.ma".
2
3include "ASM/BitVectorTrie.ma".
4include "common/Identifiers.ma".
5include "common/AST.ma".
6
7axiom LabelTag : String.
8
9definition label ≝ identifier LabelTag.
10
11(* o'caml compiler doesn't make distinction between idents and labels *)
12definition label_to_ident: label → ident ≝
13  λl.
14  match l with
15  [ an_identifier l ⇒ an_identifier SymbolTag l
16  ].
17
18definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?.
19
20definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag.
21
22axiom graph_add:
23  ∀A: Type[0].
24  ∀g: graph A.
25  ∀l: label.
26  ∀s: A.
27    lookup ? ? (add ? ? g l s) l ≠ None ?.
28
29axiom graph_add_lookup:
30  ∀A: Type[0].
31  ∀g: graph A.
32  ∀l: label.
33  ∀s: A.
34  ∀to_insert: label.
35    lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
36
37axiom graph_num_nodes:
38  ∀A: Type[0].
39  ∀g: graph A.
40    nat.
Note: See TracBrowser for help on using the repository browser.