Last change
on this file since 2717 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:
892 bytes

Line  

1  open Preamble 

2  

3  open Proper 

4  

5  open PositiveMap 

6  

7  open Deqsets 

8  

9  open Extralib 

10  

11  open Lists 

12  

13  open Identifiers 

14  

15  open Integers 

16  

17  open AST 

18  

19  open Division 

20  

21  open Exp 

22  

23  open Arithmetic 

24  

25  open Extranat 

26  

27  open Vector 

28  

29  open FoldStuff 

30  

31  open BitVector 

32  

33  open Z 

34  

35  open BitVectorZ 

36  

37  open Pointers 

38  

39  open ErrorMessages 

40  

41  open Option 

42  

43  open Setoids 

44  

45  open Monad 

46  

47  open Positive 

48  

49  open PreIdentifiers 

50  

51  open Errors 

52  

53  open Div_and_mod 

54  

55  open Jmeq 

56  

57  open Russell 

58  

59  open Util 

60  

61  open Bool 

62  

63  open Relations 

64  

65  open Nat 

66  

67  open List 

68  

69  open Hints_declaration 

70  

71  open Core_notation 

72  

73  open Pts 

74  

75  open Logic 

76  

77  open Types 

78  

79  open Coqlib 

80  

81  open Values 

82  

83  (** val truncate : 

84  Nat.nat > Nat.nat > BitVector.bitVector > BitVector.bitVector **) 

85  let truncate m n x = 

86  (Vector.vsplit m n x).Types.snd 

87  

88  (** val sign : 

89  Nat.nat > Nat.nat > BitVector.bitVector > BitVector.bitVector **) 

90  let sign m n v = 

91  Vector.pad_vector (Arithmetic.sign_bit m v) n m v 

92  

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