1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2015 *)
(* *)
(* Chantal Keller *)
(* *)
(* from the Int63 library of native-coq *)
(* by Benjamin Gregoire and Laurent Thery *)
(* *)
(* Inria - École Polytechnique - MSR-Inria Joint Lab *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
(* Add LoadPath "." as SMTCoq.Int63.standard.versions. *)
Require Export DoubleType.
Require Import Int31 Cyclic31 Ring31.
Require Import ZArith.
Require Import Bool.
Definition size := size.
Notation int := int31.
Delimit Scope int63_scope with int.
Bind Scope int63_scope with int.
(* Some constants *)
Notation "0" := 0%int31 : int63_scope.
Notation "1" := 1%int31 : int63_scope.
Notation "2" := 2%int31 : int63_scope.
Notation "3" := 3%int31 : int63_scope.
(* Logical operations *)
Definition lsl : int -> int -> int :=
fun i j => nshiftl (N.to_nat (Z.to_N (phi j))) i.
Infix "<<" := lsl (at level 30, no associativity) : int63_scope.
Definition lsr : int -> int -> int :=
fun i j => nshiftr (N.to_nat (Z.to_N (phi j))) i.
Infix ">>" := lsr (at level 30, no associativity) : int63_scope.
(* For the bitwise operations, I add a useless pattern matching to avoid
too much unfolding of their definitions at Qed (since Qed bypasses
the Opaque declaration) *)
Definition land : int -> int -> int :=
fun i => match i with
| 0%int31 | _ => fun j =>
recrbis _ j (fun d _ acc =>
let r := acc in
let d' := firstl r in
let dr := match d, d' with | D1, D1 => D1 | _, _ => D0 end in
sneakl dr r
) i
end.
Global Arguments land i j : simpl never.
Global Opaque land.
Infix "land" := land (at level 40, left associativity) : int63_scope.
Definition lor : int -> int -> int :=
fun i => match i with
| 0%int31 | _ => fun j =>
recrbis _ j (fun d _ acc =>
let r := acc in
let d' := firstl r in
let dr := match d, d' with | D0, D0 => D0 | _, _ => D1 end in
sneakl dr r
) i
end.
Global Arguments lor i j : simpl never.
Global Opaque lor.
Infix "lor" := lor (at level 40, left associativity) : int63_scope.
Definition lxor : int -> int -> int :=
fun i => match i with
| 0%int31 | _ => fun j =>
recrbis _ j (fun d _ acc =>
let r := acc in
let d' := firstl r in
let dr := match d, d' with | D0, D0 | D1, D1 => D0 | _, _ => D1 end in
sneakl dr r
) i
end.
Global Arguments lxor i j : simpl never.
Global Opaque lxor.
Infix "lxor" := lxor (at level 40, left associativity) : int63_scope.
(* Arithmetic modulo operations *)
(* Definition add : int -> int -> int := add63. *)
(* Notation "n + m" := (add n m) : int63_scope. *)
Notation "n + m" := (add31 n m) : int63_scope.
(* Definition sub : int -> int -> int := sub63. *)
(* Notation "n - m" := (sub n m) : int63_scope. *)
Notation "n - m" := (sub31 n m) : int63_scope.
(* Definition mul : int -> int -> int := mul63. *)
(* Notation "n * m" := (mul n m) : int63_scope. *)
Notation "n * m" := (mul31 n m) : int63_scope.
Definition mulc : int -> int -> int * int :=
fun i j => match mul31c i j with
| W0 => (0%int, 0%int)
| WW h l => (h, l)
end.
Definition div : int -> int -> int :=
fun i j => let (q,_) := div31 i j in q.
Notation "n / m" := (div n m) : int63_scope.
Definition modulo : int -> int -> int :=
fun i j => let (_,r) := div31 i j in r.
Notation "n '\%' m" := (modulo n m) (at level 40, left associativity) : int63_scope.
(* Comparisons *)
Definition eqb := eqb31.
Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope.
Definition ltb : int -> int -> bool :=
fun i j => match compare31 i j with | Lt => true | _ => false end.
Notation "m < n" := (ltb m n) : int63_scope.
Definition leb : int -> int -> bool :=
fun i j => match compare31 i j with | Gt => false | _ => true end.
Notation "m <= n" := (leb m n) : int63_scope.
(* TODO: fill this proof (should be in the stdlib) *)
Lemma eqb_correct : forall i j, (i==j)%int = true -> i = j.
Admitted.
(* Iterators *)
Definition foldi_cont
{A B : Type}
(f : int -> (A -> B) -> A -> B)
(from to : int)
(cont : A -> B) : A -> B :=
if ltb to from then
cont
else
let (_,r) := iter_int31 (to - from) _ (fun (jy: (int * (A -> B))%type) =>
let (j,y) := jy in ((j-1)%int, f j y)
) (to, cont) in
f from r.
Definition foldi_down_cont
{A B : Type}
(f : int -> (A -> B) -> A -> B)
(from downto : int)
(cont : A -> B) : A -> B :=
if ltb from downto then
cont
else
let (_,r) := iter_int31 (from - downto) _ (fun (jy: (int * (A -> B))%type) =>
let (j,y) := jy in ((j+1)%int, f j y)
) (downto, cont) in
f from r.
(* Fake print *)
Definition print_int : int -> int := fun i => i.
|
