source: src/common/Graphs.ma @ 1878

Last change on this file since 1878 was 1635, checked in by tranquil, 9 years ago
  • lists with binders and monads
  • Joint.ma and other temprarily forked, awaiting feedback from Claudio
  • translation of RTLabs → RTL refactored with new tools
File size: 1.3 KB
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
22definition graph_fold ≝
23  λA, B: Type[0].
24  λf.
25  λgraph: graph A.
26  λseed: B.
27  match graph with
28  [ an_id_map map ⇒ fold A B f map seed
29  ].
30
31axiom graph_add:
32  ∀A: Type[0].
33  ∀g: graph A.
34  ∀l: label.
35  ∀s: A.
36    lookup ? ? (add ? ? g l s) l ≠ None ?.
37
38axiom graph_add_eq:
39  ∀A: Type[0].
40  ∀g: graph A.
41  ∀l: label.
42  ∀s: A.
43    lookup ? ? (add ? ? g l s) l = Some ? s.
44
45axiom graph_add_lookup:
46  ∀A: Type[0].
47  ∀g: graph A.
48  ∀l: label.
49  ∀s: A.
50  ∀to_insert: label.
51    lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
52   
53axiom graph_add_preserve :
54  ∀A: Type[0].
55  ∀g: graph A.
56  ∀l: label.
57  ∀s: A.
58  ∀to_insert: label.
59  l ≠ to_insert → lookup ? ? g l = lookup ? ? (add ? ? g to_insert s) l.
60
61axiom graph_num_nodes:
62  ∀A: Type[0].
63  ∀g: graph A.
64    nat.
Note: See TracBrowser for help on using the repository browser.