Last change
on this file since 1783 was
1635,
checked in by tranquil, 8 years ago

 lists with binders and monads
 Joint.ma and other temprarily forked, awaiting feedback from Claudio
 translation of RTLabs → RTL refactored with new tools

File size:
1.3 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  axiom graph_num_nodes: 

62  ∀A: Type[0]. 

63  ∀g: graph A. 

64  nat. 

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