source: src/common/Graphs.ma @ 1562

Last change on this file since 1562 was 1515, checked in by campbell, 10 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
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
38axiom graph_add_lookup:
39  ∀A: Type[0].
40  ∀g: graph A.
41  ∀l: label.
42  ∀s: A.
43  ∀to_insert: label.
[1080]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.