diff options
Diffstat (limited to 'plugins/micromega/mutils.ml')
-rw-r--r-- | plugins/micromega/mutils.ml | 123 |
1 files changed, 83 insertions, 40 deletions
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index ef23b912..c4dbf6af 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,12 +8,23 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) +(* ** Utility functions ** *) +(* *) +(* - Modules CoqToCaml, CamlToCoq *) +(* - Modules Cmp, Tag, TagSet *) +(* *) (* Frédéric Besson (Irisa/Inria) 2006-2008 *) (* *) (************************************************************************) let debug = false +let rec pp_list f o l = + match l with + | [] -> () + | e::l -> f o e ; output_string o ";" ; pp_list f o l + + let finally f rst = try let res = f () in @@ -46,12 +57,16 @@ let iteri f l = | e::l -> f i e ; xiter (i+1) l in xiter 0 l -let mapi f l = - let rec xmap i l = - match l with - | [] -> [] - | e::l -> (f i e)::xmap (i+1) l in - xmap 0 l +let all_sym_pairs f l = + let pair_with acc e l = List.fold_left (fun acc x -> (f e x) ::acc) acc l in + + let rec xpairs acc l = + match l with + | [] -> acc + | e::l -> xpairs (pair_with acc e l) l in + xpairs [] l + + let rec map3 f l1 l2 l3 = match l1 , l2 ,l3 with @@ -59,8 +74,6 @@ let rec map3 f l1 l2 l3 = | e1::l1 , e2::l2 , e3::l3 -> (f e1 e2 e3)::(map3 f l1 l2 l3) | _ -> raise (Invalid_argument "map3") - - let rec is_sublist l1 l2 = match l1 ,l2 with | [] ,_ -> true @@ -69,8 +82,6 @@ let rec is_sublist l1 l2 = if e = e' then is_sublist l1' l2' else is_sublist l1 l2' - - let list_try_find f = let rec try_find_f = function | [] -> failwith "try_find" @@ -91,6 +102,18 @@ let interval n m = in interval_n ([],m) +let extract pred l = + List.fold_left (fun (fd,sys) e -> + match fd with + | None -> + begin + match pred e with + | None -> fd, e::sys + | Some v -> Some(v,e) , sys + end + | _ -> (fd, e::sys) + ) (None,[]) l + open Num open Big_int @@ -100,7 +123,6 @@ let ppcm x y = 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 @@ -125,8 +147,6 @@ let rec gcd_list l = 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) @@ -140,7 +160,6 @@ let mapi f l = | 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 *) @@ -178,6 +197,9 @@ let select_pos lpos l = else xselect (i+1) lpos l in xselect 0 lpos l +(** + * MODULE: Coq to Caml data-structure mappings + *) module CoqToCaml = struct @@ -194,20 +216,17 @@ struct | 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 @@ -222,14 +241,12 @@ struct | 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 q_to_num {qnum = x ; qden = y} = @@ -238,6 +255,10 @@ struct end +(** + * MODULE: Caml to Coq data-structure mappings + *) + module CamlToCoq = struct open Micromega @@ -252,7 +273,7 @@ struct else if n land 1 = 1 then XI (positive (n lsr 1)) else XO (positive (n lsr 1)) - let n nt = + let n nt = if nt < 0 then assert false else if nt = 0 then N0 @@ -266,8 +287,7 @@ struct let idx n = (*a.k.a path_of_int *) - (* returns the list of digits of n in reverse order with - initial 1 removed *) + (* 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)) @@ -309,6 +329,11 @@ struct end +(** + * MODULE: Comparisons on lists: by evaluating the elements in a single list, + * between two lists given an ordering, and using a hash computation + *) + module Cmp = struct @@ -317,7 +342,7 @@ struct | [] -> 0 (* Equal *) | f::l -> let cmp = f () in - if cmp = 0 then compare_lexical l else cmp + if cmp = 0 then compare_lexical l else cmp let rec compare_list cmp l1 l2 = match l1 , l2 with @@ -328,36 +353,59 @@ struct let c = cmp e1 e2 in if c = 0 then compare_list cmp l1 l2 else c +(** + * hash_list takes a hash function and a list, and computes an integer which + * is the hash value of the list. + *) 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 + | e::l -> _hash_list l ((hash e) lxor h) + in _hash_list l 0 - _hash_list l 0 end +(** + * MODULE: Labels for atoms in propositional formulas. + * Tags are used to identify unused atoms in CNFs, and propagate them back to + * the original formula. The translation back to Coq then ignores these + * superfluous items, which speeds the translation up a bit. + *) + module type Tag = sig + type t val from : int -> t val next : t -> t val pp : out_channel -> t -> unit val compare : t -> t -> int + end module Tag : Tag = struct + type t = int + let from i = i let next i = i + 1 let pp o i = output_string o (string_of_int i) let compare : int -> int -> int = Pervasives.compare + end +(** + * MODULE: Ordered sets of tags. + *) + module TagSet = Set.Make(Tag) +(** + * Forking routine, plumbing the appropriate pipes where needed. + *) let command exe_path args vl = (* creating pipes for stdin, stdout, stderr *) @@ -365,7 +413,6 @@ let command exe_path args vl = and (stdout_read,stdout_write) = Unix.pipe () and (stderr_read,stderr_write) = Unix.pipe () in - (* Create the process *) let pid = Unix.create_process exe_path args stdin_read stdout_write stderr_write in @@ -378,24 +425,20 @@ let command exe_path args vl = let _pid,status = Unix.waitpid [] pid in finally + (* Recover the result *) (fun () -> - (* Recover the result *) match status with | Unix.WEXITED 0 -> - let inch = Unix.in_channel_of_descr stdout_read in - begin try Marshal.from_channel inch with x -> failwith (Printf.sprintf "command \"%s\" exited %s" exe_path (Printexc.to_string x)) end - | Unix.WEXITED i -> failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i) + let inch = Unix.in_channel_of_descr stdout_read in + begin try Marshal.from_channel inch + with x -> failwith (Printf.sprintf "command \"%s\" exited %s" exe_path (Printexc.to_string x)) + end + | Unix.WEXITED i -> failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i) | Unix.WSIGNALED i -> failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i) - | Unix.WSTOPPED i -> failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i)) + | Unix.WSTOPPED i -> failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i)) + (* Cleanup *) (fun () -> - (* Cleanup *) - List.iter (fun x -> try Unix.close x with _ -> ()) [stdin_read; stdin_write; stdout_read ; stdout_write ; stderr_read; stderr_write] - ) - - - - - + List.iter (fun x -> try Unix.close x with _ -> ()) [stdin_read; stdin_write; stdout_read; stdout_write; stderr_read; stderr_write]) (* Local Variables: *) (* coding: utf-8 *) |