Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: .project Sprache: Unknown

Original von: Coq^©

(************************************************************************)
(*         *   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.3 Sekunden (vorverarbeitet) ¤

vermutete Sprache: Sekunden
vermutete Sprache: sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.