Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 0 insertions, 305 deletions

diff --git a/contrib/micromega/mutils.ml b/contrib/micromega/mutils.ml
deleted file mode 100644
index 2473608f..00000000
--- a/contrib/micromega/mutils.ml
+++ /dev/null
@@ -1,305 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-(*                                                                      *)
-(* Micromega: A reflexive tactic using the Positivstellensatz           *)
-(*                                                                      *)
-(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
-(*                                                                      *)
-(************************************************************************)
-
-let debug = false
-
-let fst' (Micromega.Pair(x,y)) = x
-let snd' (Micromega.Pair(x,y)) = y
-
-let rec try_any l x = 
- match l with
-  | [] -> None
-  | (f,s)::l -> match f x with
-     | None -> try_any l x
-     | x -> x
-
-let list_try_find f =
-  let rec try_find_f = function
-    | [] -> failwith "try_find"
-    | h::t -> try f h with Failure _ -> try_find_f t
-  in
-  try_find_f
-
-let rec list_fold_right_elements f l =
-  let rec aux = function
-    | [] -> invalid_arg "list_fold_right_elements"
-    | [x] -> x
-    | x::l -> f x (aux l) in
-  aux l
-
-let interval n m = 
-  let rec interval_n (l,m) =
-    if n > m then l else interval_n (m::l,pred m)
-  in 
-  interval_n ([],m)
-
-open Num
-open Big_int
-
-let ppcm x y = 
- let g = gcd_big_int x y in
- let x' = div_big_int x g in
- let y' = div_big_int y g in
-  mult_big_int g (mult_big_int x' y')
-
-
-let denominator = function
- | Int _ | Big_int _ -> unit_big_int
- | Ratio r -> Ratio.denominator_ratio r
-
-let numerator = function
- | Ratio r -> Ratio.numerator_ratio r
- | Int i -> Big_int.big_int_of_int i
- | Big_int i -> i
-
-let rec ppcm_list c l =
- match l with
-  | [] -> c
-  | e::l -> ppcm_list (ppcm c (denominator e)) l
-
-let rec rec_gcd_list c l  = 
- match l with
-  | [] -> c
-  | e::l -> rec_gcd_list (gcd_big_int  c (numerator e)) l
-
-let rec gcd_list l = 
- let res = rec_gcd_list zero_big_int l in
-  if compare_big_int res zero_big_int = 0 
-  then unit_big_int else res
-   
-   
-   
-let rats_to_ints l = 
- let c = ppcm_list unit_big_int l in
-  List.map (fun x ->  (div_big_int (mult_big_int (numerator x) c) 
-			(denominator x))) l
-   
-(* Nasty reordering of lists - useful to trim certificate down *)
-let mapi f l =
- let rec xmapi i l = 
-  match l with
-   | []   -> []
-   | e::l ->  (f e i)::(xmapi (i+1) l) in
-  xmapi 0 l
-
-
-let concatMapi f l = List.rev (mapi (fun e i -> (i,f e)) l)
-
-(* assoc_pos j [a0...an] = [j,a0....an,j+n],j+n+1 *)
-let assoc_pos j l = (mapi (fun e i -> e,i+j) l, j + (List.length l))
-
-let assoc_pos_assoc l = 
- let rec xpos i l =
-  match l with
-   | [] -> []
-   | (x,l) ::rst -> let (l',j) = assoc_pos i l in 
-		     (x,l')::(xpos j rst) in
-  xpos 0 l
-
-let filter_pos f l =
- (* Could sort ... take care of duplicates... *)
- let rec xfilter l =
-  match l with
-   | []  -> []
-   | (x,e)::l -> 
-      if List.exists (fun ee -> List.mem ee f) (List.map snd e)
-      then (x,e)::(xfilter l)
-      else xfilter l in
-  xfilter l
-
-let  select_pos lpos l =
- let rec xselect i lpos l =
-  match lpos with
-   | [] -> []
-   | j::rpos -> 
-      match l with
-       | []   -> failwith "select_pos"
-       | e::l -> 
-	  if i = j 
-	  then e:: (xselect (i+1) rpos l)
-	  else xselect (i+1) lpos l in
-  xselect 0 lpos l
-
-
-module CoqToCaml =
-struct
- open Micromega
-
- let rec nat = function
-  | O -> 0
-  | S n -> (nat n) + 1
-
-
- let rec positive p = 
-  match p with
-   | XH -> 1
-   | XI p -> 1+ 2*(positive p)
-   | XO p -> 2*(positive p)
-
-
- let n nt =
-  match nt with
-   | N0 -> 0
-   | Npos p -> positive p
-
-
- let rec index i = (* Swap left-right ? *)
-  match i with
-   | XH -> 1
-   | XI i -> 1+(2*(index i))
-   | XO i -> 2*(index i)
-
-
- let z x = 
-  match x with
-   | Z0 -> 0
-   | Zpos p -> (positive p)
-   | Zneg p -> - (positive p)
-
- open Big_int
-
- let rec positive_big_int p =
-  match p with
-   | XH -> unit_big_int
-   | XI p -> add_int_big_int 1 (mult_int_big_int 2 (positive_big_int p))
-   | XO p -> (mult_int_big_int 2 (positive_big_int p))
-
-
- let z_big_int x = 
-  match x with
-   | Z0 -> zero_big_int
-   | Zpos p -> (positive_big_int p)
-   | Zneg p -> minus_big_int (positive_big_int p)
-
-
- let num x = Num.Big_int (z_big_int x)
-
- let rec list elt l =
-  match l with
-   | Nil -> []
-   | Cons(e,l) -> (elt e)::(list elt l)
-
- let q_to_num {qnum = x ; qden = y} = 
-  Big_int (z_big_int x) // (Big_int (z_big_int (Zpos y)))
-  
-end
-
-
-module CamlToCoq =
-struct
- open Micromega
-
- let rec nat = function
-  | 0 -> O
-  | n -> S (nat (n-1))
-
-
- let rec positive n =
-  if n=1 then XH
-  else if n land 1 = 1 then XI (positive (n lsr 1))
-  else  XO (positive (n lsr 1))
-
- let  n nt = 
-  if nt < 0 
-  then assert false
-  else if nt = 0 then N0
-  else Npos (positive nt)
-
-
-   
-
-   
- let rec index  n =
-  if n=1 then XH
-  else if n land 1 = 1 then XI (index (n lsr 1))
-  else  XO (index (n lsr 1))
-
-
- let idx n = 
-  (*a.k.a path_of_int *)
-  (* returns the list of digits of n in reverse order with
-     initial 1 removed *)
-  let rec digits_of_int n =
-   if n=1 then [] 
-   else (n mod 2 = 1)::(digits_of_int (n lsr 1))
-  in
-   List.fold_right 
-    (fun b c -> (if b then XI c else XO c))
-    (List.rev (digits_of_int n))
-    (XH)
-
-    
-
- let z x = 
-  match compare x 0 with
-   | 0 -> Z0
-   | 1 -> Zpos (positive x)
-   | _ -> (* this should be -1 *)
-      Zneg (positive (-x)) 
-
- open Big_int
-
- let positive_big_int n = 
-  let two = big_int_of_int 2 in 
-  let rec _pos n = 
-   if eq_big_int n unit_big_int then XH
-   else
-    let (q,m) = quomod_big_int n two  in
-     if eq_big_int unit_big_int m 
-     then XI (_pos q)
-     else XO (_pos q) in
-   _pos n
-
- let bigint x = 
-  match sign_big_int x with
-   | 0 -> Z0
-   | 1 -> Zpos (positive_big_int x)
-   | _ -> Zneg (positive_big_int (minus_big_int x))
-
- let q n = 
-  {Micromega.qnum = bigint (numerator n) ; 
-   Micromega.qden = positive_big_int (denominator n)}
-
-
- let list elt l = List.fold_right (fun x l -> Cons(elt x, l)) l Nil
-
-end
-
-module Cmp =
-struct
-
- let rec compare_lexical l = 
-  match l with
-   | [] -> 0 (* Equal *)
-   | f::l -> 
-      let cmp = f () in
-       if cmp = 0 	then  compare_lexical l else cmp
-
- let rec compare_list cmp l1 l2 = 
-  match l1 , l2 with
-   | []  , [] -> 0
-   | []  , _  -> -1
-   | _   , [] -> 1
-   | e1::l1 , e2::l2 -> 
-      let c = cmp e1 e2 in
-       if c = 0 then compare_list cmp l1 l2 else c
-	
- let hash_list hash l = 
-  let rec _hash_list l h =
-   match l with
-    | []  -> h lxor (Hashtbl.hash [])
-    | e::l -> _hash_list l   ((hash e)  lxor h) in
-
-   _hash_list  l 0
-end