aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/micromega/CheckerMaker.v3
-rw-r--r--plugins/micromega/Env.v14
-rw-r--r--plugins/micromega/VarMap.v18
-rw-r--r--plugins/micromega/certificate.ml16
-rw-r--r--plugins/micromega/g_micromega.ml45
-rw-r--r--plugins/micromega/mutils.ml85
-rw-r--r--test-suite/micromega/csdp.cachebin44878 -> 0 bytes
7 files changed, 72 insertions, 69 deletions
diff --git a/plugins/micromega/CheckerMaker.v b/plugins/micromega/CheckerMaker.v
index 93b4d213f..632280d5d 100644
--- a/plugins/micromega/CheckerMaker.v
+++ b/plugins/micromega/CheckerMaker.v
@@ -12,6 +12,8 @@
(* *)
(************************************************************************)
+(* FK: scheduled for deletion *)
+(*
Require Import Setoid.
Require Import Decidable.
Require Import List.
@@ -127,3 +129,4 @@ apply <- negate_correct. intro; now elim H3. exact (H1 H2).
Qed.
End CheckerMaker.
+*) \ No newline at end of file
diff --git a/plugins/micromega/Env.v b/plugins/micromega/Env.v
index 231004bca..119093818 100644
--- a/plugins/micromega/Env.v
+++ b/plugins/micromega/Env.v
@@ -17,27 +17,21 @@ Require Import Coq.Arith.Max.
Require Import List.
Set Implicit Arguments.
-(* I have addded a Leaf constructor to the varmap data structure (/plugins/ring/Quote.v)
- -- this is harmless and spares a lot of Empty.
- This means smaller proof-terms.
- BTW, by dropping the polymorphism, I get small (yet noticeable) speed-up.
-*)
-
Section S.
Variable D :Type.
Definition Env := positive -> D.
- Definition jump (j:positive) (e:Env) := fun x => e (Pplus x j).
+ Definition jump (j:positive) (e:Env) := fun x => e (Pplus x j).
- Definition nth (n:positive) (e : Env ) := e n.
+ Definition nth (n:positive) (e : Env ) := e n.
- Definition hd (x:D) (e: Env) := nth xH e.
+ Definition hd (x:D) (e: Env) := nth xH e.
Definition tail (e: Env) := jump xH e.
- Lemma psucc : forall p, (match p with
+ Lemma psucc : forall p, (match p with
| xI y' => xO (Psucc y')
| xO y' => xI y'
| 1%positive => 2%positive
diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
index 0a66fce35..c0bf05634 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -18,11 +18,12 @@ Require Import Coq.Arith.Max.
Require Import List.
Set Implicit Arguments.
-(* I have addded a Leaf constructor to the varmap data structure (/plugins/ring/Quote.v)
- -- this is harmless and spares a lot of Empty.
- This means smaller proof-terms.
- BTW, by dropping the polymorphism, I get small (yet noticeable) speed-up.
-*)
+(*
+ * This adds a Leaf constructor to the varmap data structure (plugins/quote/Quote.v)
+ * --- it is harmless and spares a lot of Empty.
+ * It also means smaller proof-terms.
+ * As a side note, by dropping the polymorphism, one gets small, yet noticeable, speed-up.
+ *)
Section MakeVarMap.
Variable A : Type.
@@ -33,7 +34,7 @@ Section MakeVarMap.
| Leaf : A -> t
| Node : t -> A -> t -> t .
- Fixpoint find (vm : t ) (p:positive) {struct vm} : A :=
+ Fixpoint find (vm : t) (p:positive) {struct vm} : A :=
match vm with
| Empty => default
| Leaf i => i
@@ -44,8 +45,9 @@ Section MakeVarMap.
end
end.
- (* an off_map (a map with offset) offers the same functionalites as /plugins/setoid_ring/BinList.v - it is used in EnvRing.v *)
-(*
+ (* FK: scheduled for deletion *)
+ (* an off_map (a map with offset) offers the same functionalites as /plugins/setoid_ring/BinList.v - it is used in EnvRing.v *)
+ (*
Definition off_map := (option positive *t )%type.
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 7ddcf35d3..6b18281b8 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -194,9 +194,6 @@ let q_spec = {
let r_spec = z_spec
-
-
-
let dev_form n_spec p =
let rec dev_form p =
match p with
@@ -219,7 +216,6 @@ let dev_form n_spec p =
pow n in
dev_form p
-
let monomial_to_polynomial mn =
Monomial.fold
(fun v i acc ->
@@ -252,13 +248,6 @@ let rec fixpoint f x =
if y' = x then y'
else fixpoint f y'
-
-
-
-
-
-
-
let rec_simpl_cone n_spec e =
let simpl_cone =
Mc.simpl_cone n_spec.zero n_spec.unit n_spec.mult n_spec.eqb in
@@ -271,7 +260,6 @@ let rec_simpl_cone n_spec e =
| x -> simpl_cone x in
rec_simpl_cone e
-
let simplify_cone n_spec c = fixpoint (rec_simpl_cone n_spec) c
type cone_prod =
@@ -281,8 +269,6 @@ type cone_prod =
| Other of cone
and cone = Mc.zWitness
-
-
let factorise_linear_cone c =
let rec cone_list c l =
@@ -314,8 +300,6 @@ let factorise_linear_cone c =
(rebuild_cone (List.sort Pervasives.compare (cone_list c [])) None)
-
-
(* The binding with Fourier might be a bit obsolete
-- how does it handle equalities ? *)
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 869ce84b9..da16130b3 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -8,6 +8,8 @@
(* *)
(* Micromega: A reflexive tactic using the Positivstellensatz *)
(* *)
+(* * Mappings from Coq tactics to Caml function calls *)
+(* *)
(* Frédéric Besson (Irisa/Inria) 2006-2008 *)
(* *)
(************************************************************************)
@@ -55,8 +57,6 @@ TACTIC EXTEND QOmicron
[ "psatzl_Q" ] -> [ Coq_micromega.psatzl_Q]
END
-
-
TACTIC EXTEND ROmicron
[ "psatzl_R" ] -> [ Coq_micromega.psatzl_R]
END
@@ -66,7 +66,6 @@ TACTIC EXTEND RMicromega
| [ "psatz_R" ] -> [ Coq_micromega.psatz_R (-1) ]
END
-
TACTIC EXTEND QMicromega
| [ "psatz_Q" int_or_var(i) ] -> [ Coq_micromega.psatz_Q (out_arg i) ]
| [ "psatz_Q" ] -> [ Coq_micromega.psatz_Q (-1) ]
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index ec06fa58b..3f777b5c7 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -8,6 +8,11 @@
(* *)
(* Micromega: A reflexive tactic using the Positivstellensatz *)
(* *)
+(* ** Utility functions ** *)
+(* *)
+(* - Modules CoqToCaml, CamlToCoq *)
+(* - Modules Cmp, Tag, TagSet *)
+(* *)
(* Frédéric Besson (Irisa/Inria) 2006-2008 *)
(* *)
(************************************************************************)
@@ -59,8 +64,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 +72,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"
@@ -100,7 +101,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 +125,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 +138,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 +175,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 +194,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 +219,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 +233,10 @@ struct
end
+(**
+ * MODULE: Caml to Coq data-structure mappings
+ *)
+
module CamlToCoq =
struct
open Micromega
@@ -266,8 +265,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 +307,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 +320,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 +331,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 +391,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 +403,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 *)
diff --git a/test-suite/micromega/csdp.cache b/test-suite/micromega/csdp.cache
deleted file mode 100644
index 645de69cd..000000000
--- a/test-suite/micromega/csdp.cache
+++ /dev/null
Binary files differ
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 06:30:30 +0000