diff options
Diffstat (limited to 'contrib/micromega/mutils.ml')
-rw-r--r-- | contrib/micromega/mutils.ml | 305 |
1 files changed, 305 insertions, 0 deletions
diff --git a/contrib/micromega/mutils.ml b/contrib/micromega/mutils.ml new file mode 100644 index 00000000..2473608f --- /dev/null +++ b/contrib/micromega/mutils.ml @@ -0,0 +1,305 @@ +(************************************************************************) +(* 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 |