aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega')
-rw-r--r--plugins/micromega/EnvRing.v16
-rw-r--r--plugins/micromega/MExtraction.v17
-rw-r--r--plugins/micromega/coq_micromega.ml34
-rw-r--r--plugins/micromega/g_micromega.ml42
-rw-r--r--plugins/micromega/micromega.ml16
-rw-r--r--plugins/micromega/persistent_cache.ml4
6 files changed, 48 insertions, 41 deletions
diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index 56b3d480eb..ae4857a77c 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -56,10 +56,18 @@ Section MakeRingPol.
Infix "?=!" := ceqb. Notation "[ x ]" := (phi x).
(* Useful tactics *)
- Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed.
- Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed.
- Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed.
- Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
+ Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
+ Proof. exact (Radd_ext Reqe). Qed.
+
+ Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext.
+ Proof. exact (Rmul_ext Reqe). Qed.
+
+ Add Morphism ropp with signature (req ==> req) as ropp_ext.
+ Proof. exact (Ropp_ext Reqe). Qed.
+
+ Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext.
+ Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
+
Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index e5b5854f0a..362cc3a597 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -49,16 +49,13 @@ Extract Constant Rmult => "( * )".
Extract Constant Ropp => "fun x -> - x".
Extract Constant Rinv => "fun x -> 1 / x".
-(** We now extract to stdout, see comment in Makefile.build *)
-
-(*Extraction "plugins/micromega/micromega.ml" *)
-Recursive Extraction
- List.map simpl_cone (*map_cone indexes*)
- denorm Qpower vm_add
- n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
-
-
-
+(** In order to avoid annoying build dependencies the actual
+ extraction is only performed as a test in the test suite. *)
+(* Extraction "plugins/micromega/micromega.ml" *)
+(* Recursive Extraction *)
+(* List.map simpl_cone (*map_cone indexes*) *)
+(* denorm Qpower vm_add *)
+(* n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. *)
(* Local Variables: *)
(* coding: utf-8 *)
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index a4103634e0..cb54cac3f1 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -20,6 +20,7 @@ open Pp
open Mutils
open Goptions
open Names
+open Constr
(**
* Debug flag
@@ -580,9 +581,9 @@ struct
| Ukn
| BadStr of string
| BadNum of int
- | BadTerm of Term.constr
+ | BadTerm of constr
| Msg of string
- | Goal of (Term.constr list ) * Term.constr * parse_error
+ | Goal of (constr list ) * constr * parse_error
let string_of_error = function
| Ukn -> "ukn"
@@ -983,7 +984,9 @@ struct
let parse_expr sigma parse_constant parse_exp ops_spec env term =
if debug
- then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr term);
+ then (
+ let _, env = Pfedit.get_current_context () in
+ Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term));
(*
let constant_or_variable env term =
@@ -1102,9 +1105,10 @@ struct
| _ -> raise ParseError
- let rconstant sigma term =
+ let rconstant sigma term =
+ let _, env = Pfedit.get_current_context () in
if debug
- then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr term ++ fnl ());
+ then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ());
let res = rconstant sigma term in
if debug then
(Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ;
@@ -1144,9 +1148,9 @@ struct
let parse_arith parse_op parse_expr env cstr gl =
let sigma = gl.sigma in
- if debug
- then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ());
- match EConstr.kind sigma cstr with
+ if debug
+ then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ());
+ match EConstr.kind sigma cstr with
| Term.App(op,args) ->
let (op,lhs,rhs) = parse_op gl (op,args) in
let (e1,env) = parse_expr sigma env lhs in
@@ -1521,7 +1525,7 @@ let rec witness prover l1 l2 =
let rec apply_ids t ids =
match ids with
| [] -> t
- | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids
+ | i::ids -> apply_ids (mkApp(t,[| mkVar i |])) ids
let coq_Node =
lazy (gen_constant_in_modules "VarMap"
@@ -1907,7 +1911,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in
let ff = dump_formula formula_typ
(dump_cstr spec.typ spec.dump_coeff) ff in
- Feedback.msg_notice (Printer.pr_leconstr ff);
+ Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff);
Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
end;
@@ -1931,9 +1935,9 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
Feedback.msg_notice (Pp.str "\nAFormula\n") ;
let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
let ff' = dump_formula formula_typ
- (dump_cstr spec.typ spec.dump_coeff) ff' in
- Feedback.msg_notice (Printer.pr_leconstr ff');
- Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
+ (dump_cstr spec.typ spec.dump_coeff) ff' in
+ Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff');
+ Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
end;
(* Even if it does not work, this does not mean it is not provable
@@ -1986,7 +1990,7 @@ let micromega_gen
let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
- let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in
+ let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in
let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in
let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ;
@@ -2101,7 +2105,7 @@ let micromega_genr prover tac =
let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
- let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in
+ let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in
let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in
let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ;
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index b15dd7ae66..9f1d83f96e 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -14,8 +14,6 @@
(* *)
(************************************************************************)
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
open Ltac_plugin
open Stdarg
open Tacarg
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index 7da4a3b829..52c6ef983d 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -981,8 +981,8 @@ let rec or_cnf unsat deduce f f' =
(** val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf **)
-let and_cnf f1 f2 =
- app f1 f2
+let and_cnf =
+ app
(** val xcnf :
('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1
@@ -1204,22 +1204,22 @@ type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr }
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
-> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **)
-let norm cO cI cplus ctimes cminus copp ceqb =
- norm_aux cO cI cplus ctimes cminus copp ceqb
+let norm =
+ norm_aux
(** val psub0 :
'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1
-> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **)
-let psub0 cO cplus cminus copp ceqb =
- psub cO cplus cminus copp ceqb
+let psub0 =
+ psub
(** val padd0 :
'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol
-> 'a1 pol **)
-let padd0 cO cplus ceqb =
- padd cO cplus ceqb
+let padd0 =
+ padd
(** val xnormalise :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 49ccb468c1..387a525141 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -149,7 +149,7 @@ let open_in f =
match read_key_elem inch with
| None -> ()
| Some (key,elem) ->
- Table.add htbl key elem ;
+ Table.replace htbl key elem ;
xload () in
try
(* Locking of the (whole) file while reading *)
@@ -195,7 +195,7 @@ let add t k e =
else
let fd = descr_of_out_channel outch in
begin
- Table.add tbl k e ;
+ Table.replace tbl k e ;
do_under_lock Write fd
(fun _ ->
Marshal.to_channel outch (k,e) [Marshal.No_sharing] ;
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 06:56:34 +0000