Last change
on this file since 2731 was
2717,
checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.
I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).
I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size:
988 bytes

Line  

1  open Preamble 

2  

3  open Proper 

4  

5  open PositiveMap 

6  

7  open Deqsets 

8  

9  open ErrorMessages 

10  

11  open PreIdentifiers 

12  

13  open Errors 

14  

15  open Extralib 

16  

17  open Setoids 

18  

19  open Monad 

20  

21  open Option 

22  

23  open Lists 

24  

25  open Positive 

26  

27  open Identifiers 

28  

29  open Exp 

30  

31  open Arithmetic 

32  

33  open Vector 

34  

35  open Div_and_mod 

36  

37  open Jmeq 

38  

39  open Russell 

40  

41  open List 

42  

43  open Util 

44  

45  open FoldStuff 

46  

47  open BitVector 

48  

49  open Extranat 

50  

51  open Bool 

52  

53  open Relations 

54  

55  open Nat 

56  

57  open Integers 

58  

59  open Hints_declaration 

60  

61  open Core_notation 

62  

63  open Pts 

64  

65  open Logic 

66  

67  open Types 

68  

69  open AST 

70  

71  open BitVectorTrie 

72  

73  type costlabel = PreIdentifiers.identifier 

74  

75  (** val costlabel_of_nat : Nat.nat > costlabel **) 

76  let costlabel_of_nat = 

77  Identifiers.identifier_of_nat PreIdentifiers.CostTag 

78  

79  type costlabel_map = costlabel BitVectorTrie.bitVectorTrie 

80  

81  (** val costlabel_map0 : costlabel_map **) 

82  let costlabel_map0 = 

83  BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 

84  (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 

85  Nat.O)))))))))))))))) 

86  

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