source: src/common/Graphs.ma @ 1515

Last change on this file since 1515 was 1515, checked in by campbell, 8 years ago

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File size: 1.0 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_lookup:
39  ∀A: Type[0].
40  ∀g: graph A.
41  ∀l: label.
42  ∀s: A.
43  ∀to_insert: label.
44    lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
45
46axiom graph_num_nodes:
47  ∀A: Type[0].
48  ∀g: graph A.
49    nat.
Note: See TracBrowser for help on using the repository browser.