|
Last change
on this file since 2768 was
2645,
checked in by sacerdot, 8 years ago
|
- some broken back-end files repaires, several still to go
- the string datatype has been refined into three different data
types: string (for backend comments); identifierTag; ErrorMessage?
- all axioms of type String have been turned into constructors of one of the
three datatypes. In this way we do not have axioms to be implemented in
the extracted files
|
|
File size:
1.6 KB
|
| Line | |
|---|
| 1 | include "basics/types.ma". |
|---|
| 2 | |
|---|
| 3 | include "ASM/BitVectorTrie.ma". |
|---|
| 4 | include "common/Identifiers.ma". |
|---|
| 5 | include "common/AST.ma". |
|---|
| 6 | |
|---|
| 7 | definition label ≝ identifier LabelTag. |
|---|
| 8 | |
|---|
| 9 | (* o'caml compiler doesn't make distinction between idents and labels *) |
|---|
| 10 | definition label_to_ident: label → ident ≝ |
|---|
| 11 | λl. |
|---|
| 12 | match l with |
|---|
| 13 | [ an_identifier l ⇒ an_identifier SymbolTag l |
|---|
| 14 | ]. |
|---|
| 15 | |
|---|
| 16 | definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?. |
|---|
| 17 | |
|---|
| 18 | definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag. |
|---|
| 19 | |
|---|
| 20 | definition graph_fold ≝ |
|---|
| 21 | λA, B: Type[0]. |
|---|
| 22 | λf. |
|---|
| 23 | λgraph: graph A. |
|---|
| 24 | λseed: B. |
|---|
| 25 | match graph with |
|---|
| 26 | [ an_id_map map ⇒ fold A B f map seed |
|---|
| 27 | ]. |
|---|
| 28 | |
|---|
| 29 | axiom graph_add: |
|---|
| 30 | ∀A: Type[0]. |
|---|
| 31 | ∀g: graph A. |
|---|
| 32 | ∀l: label. |
|---|
| 33 | ∀s: A. |
|---|
| 34 | lookup ? ? (add ? ? g l s) l ≠ None ?. |
|---|
| 35 | |
|---|
| 36 | axiom graph_add_eq: |
|---|
| 37 | ∀A: Type[0]. |
|---|
| 38 | ∀g: graph A. |
|---|
| 39 | ∀l: label. |
|---|
| 40 | ∀s: A. |
|---|
| 41 | lookup ? ? (add ? ? g l s) l = Some ? s. |
|---|
| 42 | |
|---|
| 43 | axiom graph_add_lookup: |
|---|
| 44 | ∀A: Type[0]. |
|---|
| 45 | ∀g: graph A. |
|---|
| 46 | ∀l: label. |
|---|
| 47 | ∀s: A. |
|---|
| 48 | ∀to_insert: label. |
|---|
| 49 | lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?. |
|---|
| 50 | |
|---|
| 51 | axiom graph_add_preserve : |
|---|
| 52 | ∀A: Type[0]. |
|---|
| 53 | ∀g: graph A. |
|---|
| 54 | ∀l: label. |
|---|
| 55 | ∀s: A. |
|---|
| 56 | ∀to_insert: label. |
|---|
| 57 | l ≠ to_insert → lookup ? ? g l = lookup ? ? (add ? ? g to_insert s) l. |
|---|
| 58 | |
|---|
| 59 | definition graph_num_nodes: |
|---|
| 60 | ∀A: Type[0].graph A → ℕ ≝ λA,g.|g|. |
|---|
| 61 | |
|---|
| 62 | lemma graph_num_ind : ∀A : Type[0].∀P : graph A → Prop. |
|---|
| 63 | (∀g.(∀g'.|g'|<|g| → P g') → P g) → ∀g.P g. |
|---|
| 64 | #A#P#H#g |
|---|
| 65 | lapply (refl ? (|g|)) |
|---|
| 66 | generalize in ⊢(???%→?); |
|---|
| 67 | #n lapply g -g |
|---|
| 68 | @(nat_elim1 … n) |
|---|
| 69 | #m #G #g #EQs @H >EQs #g' #DEQ @(G ? DEQ g' (refl …)) |
|---|
| 70 | qed. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
