aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/standard/mutils_full.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/versions/standard/mutils_full.ml')
-rw-r--r--src/versions/standard/mutils_full.ml358
1 files changed, 0 insertions, 358 deletions
diff --git a/src/versions/standard/mutils_full.ml b/src/versions/standard/mutils_full.ml
deleted file mode 100644
index efa2e4d..0000000
--- a/src/versions/standard/mutils_full.ml
+++ /dev/null
@@ -1,358 +0,0 @@
-(*** This file is taken from Coq-8.9.0 to solve a compilation issue due
- to a wrong order in dependencies.
- See https://github.com/coq/coq/issues/9768 . ***)
-
-
-(************************************************************************)
-(* * 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 Micromega = Micromega_plugin.Micromega
-
-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
- 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_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 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
-
-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 gcd_list l =
- let res = rec_gcd_list zero_big_int l in
- if Int.equal (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
-
-(* assoc_pos j [a0...an] = [j,a0....an,j+n],j+n+1 *)
-(**
- * 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
-
-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 = Int.compare
-
-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: *)
generated by cgit (git 2.34.1) at 2024-06-18 02:34:39 +0000