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:
704 bytes

Line  

1  open Preamble 

2  

3  open Types 

4  

5  open Bool 

6  

7  open Relations 

8  

9  open Nat 

10  

11  open Hints_declaration 

12  

13  open Core_notation 

14  

15  open Pts 

16  

17  open Logic 

18  

19  open Positive 

20  

21  open Z 

22  

23  open Extranat 

24  

25  open Vector 

26  

27  open Div_and_mod 

28  

29  open Jmeq 

30  

31  open Russell 

32  

33  open List 

34  

35  open Util 

36  

37  open FoldStuff 

38  

39  open BitVector 

40  

41  open Exp 

42  

43  open Arithmetic 

44  

45  open Division 

46  

47  val z_of_unsigned_bitvector : Nat.nat > BitVector.bitVector > Z.z 

48  

49  val z_of_signed_bitvector : Nat.nat > BitVector.bitVector > Z.z 

50  

51  val bits_of_pos : Positive.pos > Bool.bool List.list 

52  

53  val zeroext_reversed : 

54  Nat.nat > Nat.nat > BitVector.bitVector > BitVector.bitVector 

55  

56  val bitvector_of_Z : Nat.nat > Z.z > BitVector.bitVector 

57  

58  val pos_length : Positive.pos > Nat.nat 

59  

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