diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-16 00:53:17 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-16 00:53:17 +0000 |
commit | 18e543106f358272138a87bf331c4d1964a385f5 (patch) | |
tree | 5714692f140688b634eb789f3897e8dc1860b3c4 /theories/Numbers/Natural/BigN/BigN.v | |
parent | 49a7bb129b8a7f9d5a9175b7a340112c20e95d96 (diff) |
More BigNum cleanup:
* View of Int31 as a Z/nZ moved to file Z31Z.v (TO FINISH: specs are still admitted!)
* Modular specification of Z/nZ moved to ZnZ and renamed CyclicType
* More isolation between Cyclic/Abstract and Cyclic/DoubleCyclic
* A few comments
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10936 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/BigN/BigN.v')
-rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 95 |
1 files changed, 1 insertions, 94 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index ecb4578eb..db4cd8965 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -15,105 +15,12 @@ Author: Arnaud Spiwack *) Require Export Int31. +Require Import Z31Z. 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 *) - exact tail031. (* number of tail 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. |