source: extracted/integers.mli @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 2.9 KB
Line 
1open Preamble
2
3open Bool
4
5open Hints_declaration
6
7open Core_notation
8
9open Pts
10
11open Logic
12
13open Relations
14
15open Nat
16
17open Types
18
19open Extranat
20
21open Char
22
23open String
24
25open Vector
26
27open Div_and_mod
28
29open Jmeq
30
31open Russell
32
33open List
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Arithmetic
42
43type comparison =
44| Ceq
45| Cne
46| Clt
47| Cle
48| Cgt
49| Cge
50
51val comparison_rect_Type4 :
52  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
53
54val comparison_rect_Type5 :
55  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
56
57val comparison_rect_Type3 :
58  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
59
60val comparison_rect_Type2 :
61  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
62
63val comparison_rect_Type1 :
64  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
65
66val comparison_rect_Type0 :
67  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
68
69val comparison_inv_rect_Type4 :
70  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
71  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
72
73val comparison_inv_rect_Type3 :
74  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
75  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
76
77val comparison_inv_rect_Type2 :
78  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
79  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
80
81val comparison_inv_rect_Type1 :
82  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
83  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
84
85val comparison_inv_rect_Type0 :
86  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
87  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
88
89val comparison_discr : comparison -> comparison -> __
90
91val comparison_jmdiscr : comparison -> comparison -> __
92
93val negate_comparison : comparison -> comparison
94
95val swap_comparison : comparison -> comparison
96
97val wordsize : Nat.nat
98
99type int = BitVector.bitVector
100
101val repr : Nat.nat -> int
102
103val zero0 : int
104
105val one : int
106
107val mone : BitVector.bitVector
108
109val iwordsize : int
110
111val eq_dec : int -> int -> (__, __) Types.sum
112
113val eq : int -> int -> Bool.bool
114
115val lt : int -> int -> Bool.bool
116
117val ltu : int -> int -> Bool.bool
118
119val neg : int -> int
120
121val mul :
122  BitVector.bitVector -> BitVector.bitVector -> Bool.bool Vector.vector
123
124val zero_ext_n :
125  Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
126
127val zero_ext0 : Nat.nat -> int -> int
128
129val sign_ext_n :
130  Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
131
132val sign_ext0 : Nat.nat -> int -> int
133
134val i_and : int -> int -> int
135
136val or0 : int -> int -> int
137
138val xor : int -> int -> int
139
140val not : int -> int
141
142val shl : int -> int -> int
143
144val shru : int -> int -> int
145
146val shr : int -> int -> int
147
148val shrx : int -> int -> int
149
150val shr_carry : int -> int -> BitVector.bitVector
151
152val rol : int -> int -> int
153
154val ror : int -> int -> int
155
156val rolm : int -> int -> int -> int
157
158val cmp : comparison -> int -> int -> Bool.bool
159
160val cmpu : comparison -> int -> int -> Bool.bool
161
162val notbool : int -> int
163
Note: See TracBrowser for help on using the repository browser.