summaryrefslogtreecommitdiff
path: root/contrib/micromega/mutils.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/micromega/mutils.ml')
-rw-r--r--contrib/micromega/mutils.ml305
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 00:07:44 +0000