|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* *)
(* Micromega: A reflexive tactic using the Positivstellensatz *)
(* *)
(* ** Utility functions ** *)
(* *)
(* - Modules CoqToCaml, CamlToCoq *)
(* - Modules Cmp, Tag, TagSet *)
(* *)
(* Frédéric Besson (Irisa/Inria) 2006-2008 *)
(* *)
(************************************************************************)
module Int = struct
type t = int
let compare : int -> int -> int = Pervasives.compare
let equal : int -> int -> bool = (=)
end
module ISet =
struct
include Set.Make(Int)
let pp o s = iter (fun i -> Printf.fprintf o "%i " i) s
end
module IMap =
struct
include Map.Make(Int)
let from k m =
let (_,_,r) = split (k-1) m in
r
end
let rec pp_list s f o l =
match l with
| [] -> ()
| [e] -> f o e
| e::l -> f o e ; output_string o s ; pp_list s f o l
let finally f rst =
try
let res = f () in
rst () ; res
with reraise ->
(try rst ()
with any -> raise reraise
); raise reraise
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 all_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::lx -> xpairs (pair_with acc e l) lx in
xpairs [] l
let rec is_sublist f l1 l2 =
match l1 ,l2 with
| [] ,_ -> true
| e::l1', [] -> false
| e::l1' , e'::l2' ->
if f e e' then is_sublist f l1' l2'
else is_sublist f l1 l2'
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
let extract_best red lt l =
let rec extractb c e rst l =
match l with
[] -> Some (c,e) , rst
| e'::l' -> match red e' with
| None -> extractb c e (e'::rst) l'
| Some c' -> if lt c' c
then extractb c' e' (e::rst) l'
else extractb c e (e'::rst) l' in
match extract red l with
| None , _ -> None,l
| Some(c,e), rst -> extractb c e [] rst
let rec find_some pred l =
match l with
| [] -> None
| e::l -> match pred e with
| Some r -> Some r
| None -> find_some pred l
let extract_all pred l =
List.fold_left (fun (s1,s2) e ->
match pred e with
| None -> s1,e::s2
| Some v -> (v,e)::s1 , s2) ([],[]) l
let simplify f sys =
let (sys',b) =
List.fold_left (fun (sys',b) c ->
match f c with
| None -> (c::sys',b)
| Some c' ->
(c'::sys',true)
) ([],false) sys in
if b then Some sys' else None
let generate_acc f acc sys =
List.fold_left (fun sys' c -> match f c with
| None -> sys'
| Some c' -> c'::sys'
) acc sys
let generate f sys = generate_acc f [] sys
let saturate p f sys =
let rec sat acc l =
match extract p l with
| None,_ -> acc
| Some r,l' ->
let n = generate (f r) (l'@acc) in
sat (n@acc) l' in
try sat [] sys with
x ->
begin
Printexc.print_backtrace stdout ;
raise x
end
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 iterate_until_stable f x =
let rec iter x =
match f x with
| None -> x
| Some x' -> iter x' in
iter x
let rec app_funs l x =
match l with
| [] -> None
| f::fl ->
match f x with
| None -> app_funs fl x
| Some x' -> Some x'
(**
* MODULE: Coq to Caml data-structure mappings
*)
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)
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 q_to_num {qnum = x ; qden = y} =
Big_int (z_big_int x) // (Big_int (z_big_int (Zpos y)))
end
(**
* MODULE: Caml to Coq data-structure mappings
*)
module CamlToCoq =
struct
open Micromega
let rec nat = function
| 0 -> O
| n -> S (nat (n-1))
let rec positive n =
if Int.equal n 1 then XH
else if Int.equal (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 Int.equal nt 0 then N0
else Npos (positive nt)
let rec index n =
if Int.equal n 1 then XH
else if Int.equal (n land 1) 1 then XI (index (n lsr 1))
else XO (index (n lsr 1))
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)}
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
let rec compare_lexical l =
match l with
| [] -> 0 (* Equal *)
| f::l ->
let cmp = f () in
if Int.equal 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 Int.equal c 0 then compare_list cmp l1 l2 else c
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
val max : t -> t -> t
val to_int : t -> int
end
module Tag : Tag =
struct
type t = int
let from i = i
let next i = i + 1
let max : int -> int -> int = Pervasives.max
let pp o i = output_string o (string_of_int i)
let compare : int -> int -> int = Int.compare
let to_int x = x
end
(**
* MODULE: Ordered sets of tags.
*)
module TagSet = Set.Make(Tag)
(** As for Unix.close_process, our Unix.waipid will ignore all EINTR *)
let rec waitpid_non_intr pid =
try snd (Unix.waitpid [] pid)
with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_non_intr pid
(**
* Forking routine, plumbing the appropriate pipes where needed.
*)
let command exe_path args vl =
(* creating pipes for stdin, stdout, stderr *)
let (stdin_read,stdin_write) = Unix.pipe ()
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
(* Write the data on the stdin of the created process *)
let outch = Unix.out_channel_of_descr stdin_write in
output_value outch vl ;
flush outch ;
(* Wait for its completion *)
let status = waitpid_non_intr pid in
finally
(* Recover the result *)
(fun () ->
match status with
| Unix.WEXITED 0 ->
let inch = Unix.in_channel_of_descr stdout_read in
begin
try Marshal.from_channel inch
with any ->
failwith
(Printf.sprintf "command \"%s\" exited %s" exe_path
(Printexc.to_string any))
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))
(* Cleanup *)
(fun () ->
List.iter (fun x -> try Unix.close x with any -> ())
[stdin_read; stdin_write;
stdout_read; stdout_write;
stderr_read; stderr_write])
(* Local Variables: *)
(* coding: utf-8 *)
(* End: *)
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
