Last change
on this file was
2645,
checked in by sacerdot, 7 years ago

 some broken backend 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.