Last change
on this file since 2500 was
1882,
checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

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  axiom LabelTag : String. 

8  

9  definition label ≝ identifier LabelTag. 

10  

11  (* o'caml compiler doesn't make distinction between idents and labels *) 

12  definition label_to_ident: label → ident ≝ 

13  λl. 

14  match l with 

15  [ an_identifier l ⇒ an_identifier SymbolTag l 

16  ]. 

17  

18  definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?. 

19  

20  definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag. 

21  

22  definition 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  

31  axiom 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  

38  axiom 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  

45  axiom 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  

53  axiom 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  

61  definition graph_num_nodes: 

62  ∀A: Type[0].graph A → ℕ ≝ λA,g.g. 

63  

64  lemma graph_num_ind : ∀A : Type[0].∀P : graph A → Prop. 

65  (∀g.(∀g'.g'<g → P g') → P g) → ∀g.P g. 

66  #A#P#H#g 

67  lapply (refl ? (g)) 

68  generalize in ⊢(???%→?); 

69  #n lapply g g 

70  @(nat_elim1 … n) 

71  #m #G #g #EQs @H >EQs #g' #DEQ @(G ? DEQ g' (refl …)) 

72  qed. 

Note: See
TracBrowser
for help on using the repository browser.