diff options
Diffstat (limited to 'src/versions/standard/Int63/Int63Native_standard.v')
| -rw-r--r-- | src/versions/standard/Int63/Int63Native_standard.v | 167 |
1 files changed, 0 insertions, 167 deletions
diff --git a/src/versions/standard/Int63/Int63Native_standard.v b/src/versions/standard/Int63/Int63Native_standard.v deleted file mode 100644 index ed9d3d0..0000000 --- a/src/versions/standard/Int63/Int63Native_standard.v +++ /dev/null @@ -1,167 +0,0 @@ -(**************************************************************************) -(* *) -(* 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. |