package coq-core

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file mutils.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \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                             *)
(*                                                                      *)
(************************************************************************)

open NumCompat
module Z_ = NumCompat.Z

module Int = struct
  type t = int

  let compare : int -> int -> int = 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 -> (
        match pred e with None -> (fd, e :: sys) | Some v -> (Some (v, e), sys)
        )
      | _ -> (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_option pred l =
  match l with
  | [] -> raise Not_found
  | e :: l -> ( match pred e with Some r -> r | None -> find_option pred l )

let find_some pred l = try Some (find_option pred l) with Not_found -> None

let extract_all pred l =
  List.fold_left
    (fun (s1, s2) e ->
      match pred e with None -> (s1, e :: s2) | Some v -> (v :: 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 ->
    Printexc.print_backtrace stdout;
    raise x

let saturate_bin (type a) (module Set : Set.S with type elt = a)
    (f : a -> a -> a option) (l : a list) =
  let rec map_with (acc : Set.t) e l =
    match l with
    | [] -> acc
    | e' :: l -> (
      match f e e' with
      | None -> map_with acc e l
      | Some r -> map_with (Set.add r acc) e l )
  in
  let map2_with acc l' = Set.fold (fun e' acc -> map_with acc e' l) l' acc in
  let rec iterate acc l' =
    let res = map2_with Set.empty l' in
    if Set.is_empty res then Set.union l' acc
    else iterate (Set.union l' acc) res
  in
  let s0 = List.fold_left (fun acc e -> Set.add e acc) Set.empty l in
  Set.elements (Set.diff (iterate Set.empty s0) s0)

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

  let rec positive_big_int p =
    match p with
    | XH -> Z_.one
    | XI p -> Z_.add Z_.one (Z_.mul Z_.two (positive_big_int p))
    | XO p -> Z_.mul Z_.two (positive_big_int p)

  let z_big_int x =
    match x with
    | Z0 -> Z_.zero
    | Zpos p -> positive_big_int p
    | Zneg p -> Z_.neg (positive_big_int p)

  let z x = match x with Z0 -> 0 | Zpos p -> index p | Zneg p -> -index p

  let q_to_num {qnum = x; qden = y} =
    let open Q.Notations in
    Q.of_bigint (z_big_int x) // Q.of_bigint (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))

  let positive_big_int n =
    let rec _pos n =
      if Z_.equal n Z_.one then XH
      else
        let q, m = Z_.quomod n Z_.two in
        if Z_.equal Z_.one m then XI (_pos q) else XO (_pos q)
    in
    _pos n

  let bigint x =
    match Z_.sign x with
    | 0 -> Z0
    | 1 -> Zpos (positive_big_int x)
    | _ -> Zneg (positive_big_int (Z_.neg x))

  let q n =
    { Micromega.qnum = bigint (Q.num n)
    ; Micromega.qden = positive_big_int (Q.den 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 = int

  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 = 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 = struct
  include Set.Make (Tag)
end

module McPrinter = struct
  module Mc = Micromega

  let pp_nat o n = Printf.fprintf o "%i" (CoqToCaml.nat n)

  let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x)

  let pp_z o x =
  Printf.fprintf o "%s" (NumCompat.Z.to_string (CoqToCaml.z_big_int x))

  let pp_pol pp_c o e =
    let rec pp_pol o e =
    match e with
    | Mc.Pc n -> Printf.fprintf o "Pc %a" pp_c n
    | Mc.Pinj (p, pol) ->
      Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol
    | Mc.PX (pol1, p, pol2) ->
      Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2
  in
  pp_pol o e

  let pp_psatz pp_z o e =
  let rec pp_cone o e =
    match e with
    | Mc.PsatzLet (e1, e2) ->
      Printf.fprintf o "(Let %a %a)%%nat" pp_cone e1 pp_cone e2
    | Mc.PsatzIn n -> Printf.fprintf o "(In %a)%%nat" pp_nat n
    | Mc.PsatzMulC (e, c) ->
      Printf.fprintf o "( %a [*] %a)" (pp_pol pp_z) e pp_cone c
    | Mc.PsatzSquare e -> Printf.fprintf o "(%a^2)" (pp_pol pp_z) e
    | Mc.PsatzAdd (e1, e2) ->
      Printf.fprintf o "(%a [+] %a)" pp_cone e1 pp_cone e2
    | Mc.PsatzMulE (e1, e2) ->
      Printf.fprintf o "(%a [*] %a)" pp_cone e1 pp_cone e2
    | Mc.PsatzC p -> Printf.fprintf o "(%a)%%positive" pp_z p
    | Mc.PsatzZ -> Printf.fprintf o "0"
  in
  pp_cone o e

let rec pp_proof_term o = function
  | Micromega.DoneProof -> Printf.fprintf o "D"
  | Micromega.RatProof (cone, rst) ->
    Printf.fprintf o "R[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst
  | Micromega.CutProof (cone, rst) ->
    Printf.fprintf o "C[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst
  | Micromega.SplitProof (p, p1, p2) ->
    Printf.fprintf o "S[%a,%a,%a]" (pp_pol pp_z) p pp_proof_term p1
      pp_proof_term p2
  | Micromega.EnumProof (c1, c2, rst) ->
    Printf.fprintf o "EP[%a,%a,%a]" (pp_psatz pp_z) c1 (pp_psatz pp_z) c2
      (pp_list "," pp_proof_term)
      rst
  | Micromega.ExProof (p, prf) ->
    Printf.fprintf o "Ex[%a,%a]" pp_positive p pp_proof_term prf

end


(** 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
        try Marshal.from_channel inch
        with any ->
          failwith
            (Printf.sprintf "command \"%s\" exited %s" exe_path
               (Printexc.to_string any)) )
      | 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 ])

(** Hashing utilities *)

module Hash = struct
  module Mc = Micromega
  open Hashset.Combine

  let int_of_eq_op1 =
    Mc.(function Equal -> 0 | NonEqual -> 1 | Strict -> 2 | NonStrict -> 3)

  let int_of_eq_op2 =
    Mc.(
      function
      | OpEq -> 0 | OpNEq -> 1 | OpLe -> 2 | OpGe -> 3 | OpLt -> 4 | OpGt -> 5)

  let eq_op1 o1 o2 = Int.equal (int_of_eq_op1 o1) (int_of_eq_op1 o2)
  let eq_op2 o1 o2 = Int.equal (int_of_eq_op2 o1) (int_of_eq_op2 o2)
  let hash_op1 h o = combine h (int_of_eq_op1 o)

  let rec eq_positive p1 p2 =
    match (p1, p2) with
    | Mc.XH, Mc.XH -> true
    | Mc.XI p1, Mc.XI p2 -> eq_positive p1 p2
    | Mc.XO p1, Mc.XO p2 -> eq_positive p1 p2
    | _, _ -> false

  let eq_z z1 z2 =
    match (z1, z2) with
    | Mc.Z0, Mc.Z0 -> true
    | Mc.Zpos p1, Mc.Zpos p2 | Mc.Zneg p1, Mc.Zneg p2 -> eq_positive p1 p2
    | _, _ -> false

  let eq_q {Mc.qnum = qn1; Mc.qden = qd1} {Mc.qnum = qn2; Mc.qden = qd2} =
    eq_z qn1 qn2 && eq_positive qd1 qd2

  let rec eq_pol eq p1 p2 =
    match (p1, p2) with
    | Mc.Pc c1, Mc.Pc c2 -> eq c1 c2
    | Mc.Pinj (i1, p1), Mc.Pinj (i2, p2) -> eq_positive i1 i2 && eq_pol eq p1 p2
    | Mc.PX (p1, i1, p1'), Mc.PX (p2, i2, p2') ->
      eq_pol eq p1 p2 && eq_positive i1 i2 && eq_pol eq p1' p2'
    | _, _ -> false

  let eq_pair eq1 eq2 (x1, y1) (x2, y2) = eq1 x1 x2 && eq2 y1 y2

  let hash_pol helt =
    let rec hash acc = function
      | Mc.Pc c -> helt (combine acc 1) c
      | Mc.Pinj (p, c) -> hash (combine (combine acc 1) (CoqToCaml.index p)) c
      | Mc.PX (p1, i, p2) ->
        hash (hash (combine (combine acc 2) (CoqToCaml.index i)) p1) p2
    in
    hash

  let hash_pair h1 h2 h (e1, e2) = h2 (h1 h e1) e2
  let hash_elt f h e = combine h (f e)
  let hash_string h (e : string) = hash_elt Hashtbl.hash h e
  let hash_z = hash_elt CoqToCaml.z
  let hash_q = hash_elt (fun q -> Hashtbl.hash (CoqToCaml.q_to_num q))
end

(* Local Variables: *)
(* coding: utf-8 *)
(* End: *)
OCaml

Innovation. Community. Security.