source: src/common/Graphs.ma @ 1713

Last change on this file since 1713 was 1635, checked in by tranquil, 8 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
RevLine 
[726]1include "basics/types.ma".
[639]2
[726]3include "ASM/BitVectorTrie.ma".
[736]4include "common/Identifiers.ma".
[1082]5include "common/AST.ma".
[639]6
[736]7axiom LabelTag : String.
[639]8
[738]9definition label ≝ identifier LabelTag.
[726]10
[1082]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
[736]18definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?.
[726]19
[738]20definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag.
[1077]21
[1253]22definition graph_fold ≝
23  λA, B: Type[0].
24  λf.
25  λgraph: graph A.
26  λseed: B.
27  match graph with
[1515]28  [ an_id_map map ⇒ fold A B f map seed
[1253]29  ].
30
[1077]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
[1635]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
[1077]45axiom graph_add_lookup:
46  ∀A: Type[0].
47  ∀g: graph A.
48  ∀l: label.
49  ∀s: A.
50  ∀to_insert: label.
[1080]51    lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
[1635]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.
[1080]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.