blob: 1d2b177dfb9234a5569fae5099dd3a8bb28e9a00 (
plain)
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
|
Require Export Int31.
Require Import NMake.
Require Import ZnZ.
Open Scope int31_scope.
Definition int31_op : znz_op int31.
split.
(* Conversion functions with Z *)
exact (31%positive). (* number of digits *)
exact (31). (* number of digits *)
exact (phi). (* conversion to Z *)
exact (positive_to_int31). (* positive -> N*int31 : p => N,i where p = N*2^31+phi i *)
exact head031. (* number of head 0 *)
(* Basic constructors *)
exact 0. (* 0 *)
exact 1. (* 1 *)
exact Tn. (* 2^31 - 1 *)
(* A function which given two int31 i and j, returns a double word
which is worth i*2^31+j *)
exact (fun i j => match (match i ?= 0 with | Eq => j ?= 0 | not0 => not0 end) with | Eq => W0 | _ => WW i j end).
(* two special cases where i and j are respectively taken equal to 0 *)
exact (fun i => match i ?= 0 with | Eq => W0 | _ => WW i 0 end).
exact (fun j => match j ?= 0 with | Eq => W0 | _ => WW 0 j end).
(* Comparison *)
exact compare31.
exact (fun i => match i ?= 0 with | Eq => true | _ => false end).
(* Basic arithmetic operations *)
(* opposite functions *)
exact (fun i => 0 -c i).
exact (fun i => 0 - i).
exact (fun i => 0-i-1). (* the carry is always -1*)
(* successor and addition functions *)
exact (fun i => i +c 1).
exact add31c.
exact add31carryc.
exact (fun i => i + 1).
exact add31.
exact (fun i j => i + j + 1).
(* predecessor and subtraction functions *)
exact (fun i => i -c 1).
exact sub31c.
exact sub31carryc.
exact (fun i => i - 1).
exact sub31.
exact (fun i j => i - j - 1).
(* multiplication functions *)
exact mul31c.
exact mul31.
exact (fun x => x *c x).
(* special (euclidian) division operations *)
exact div3121.
exact div31. (* this is supposed to be the special case of division a/b where a > b *)
exact div31.
(* euclidian division remainder *)
(* again special case for a > b *)
exact (fun i j => let (_,r) := i/j in r).
exact (fun i j => let (_,r) := i/j in r).
(* gcd functions *)
exact gcd31. (*gcd_gt*)
exact gcd31. (*gcd*)
(* shift operations *)
exact addmuldiv31. (*add_mul_div *)
(*modulo 2^p *)
exact (fun p i =>
match compare31 p 32 with
| Lt => addmuldiv31 p 0 (addmuldiv31 (31-p) i 0)
| _ => i
end).
(* is i even ? *)
exact (fun i => let (_,r) := i/2 in
match r ?= 0 with
| Eq => true
| _ => false
end).
(* square root operations *)
exact sqrt312. (* sqrt2 *)
exact sqrt31. (* sqr *)
Defined.
Definition int31_spec : znz_spec int31_op.
Admitted.
Module Int31_words <: W0Type.
Definition w := int31.
Definition w_op := int31_op.
Definition w_spec := int31_spec.
End Int31_words.
Module BigN := NMake.Make Int31_words.
Definition bigN := BigN.t.
Delimit Scope bigN_scope with bigN.
Bind Scope bigN_scope with bigN.
Bind Scope bigN_scope with BigN.t.
Bind Scope bigN_scope with BigN.t_.
Notation " i + j " := (BigN.add i j) : bigN_scope.
Notation " i - j " := (BigN.sub i j) : bigN_scope.
Notation " i * j " := (BigN.mul i j) : bigN_scope.
Notation " i / j " := (BigN.div i j) : bigN_scope.
Notation " i ?= j " := (BigN.compare i j) : bigN_scope.
|