summaryrefslogtreecommitdiff
path: root/plugins/micromega/coq_micromega.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/coq_micromega.ml')
-rw-r--r--plugins/micromega/coq_micromega.ml170
1 files changed, 86 insertions, 84 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 7e10464a..2812e36e 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -16,6 +16,7 @@
(* *)
(************************************************************************)
+open Pp
open Mutils
(**
@@ -44,7 +45,7 @@ type tag = Tag.t
(**
* An atom is of the form:
- * pExpr1 {<,>,=,<>,<=,>=} pExpr2
+ * pExpr1 \{<,>,=,<>,<=,>=\} pExpr2
* where pExpr1, pExpr2 are polynomial expressions (see Micromega). pExprs are
* parametrized by 'cst, which is used as the type of constants.
*)
@@ -65,7 +66,7 @@ type 'cst formula =
| C of 'cst formula * 'cst formula
| D of 'cst formula * 'cst formula
| N of 'cst formula
- | I of 'cst formula * Names.identifier option * 'cst formula
+ | I of 'cst formula * Names.Id.t option * 'cst formula
(**
* Formula pretty-printer.
@@ -82,7 +83,7 @@ let rec pp_formula o f =
| I(f1,n,f2) -> Printf.fprintf o "I(%a%s,%a)"
pp_formula f1
(match n with
- | Some id -> Names.string_of_id id
+ | Some id -> Names.Id.to_string id
| None -> "") pp_formula f2
| N(f) -> Printf.fprintf o "N(%a)" pp_formula f
@@ -111,7 +112,7 @@ let rec ids_of_formula f =
(**
* A clause is a list of (tagged) nFormulas.
* nFormulas are normalized formulas, i.e., of the form:
- * cPol {=,<>,>,>=} 0
+ * cPol \{=,<>,>,>=\} 0
* with cPol compact polynomials (see the Pol inductive type in EnvRing.v).
*)
@@ -242,10 +243,10 @@ let rec add_term t0 = function
* MODULE: Ordered set of integers.
*)
-module ISet = Set.Make(struct type t = int let compare : int -> int -> int = Pervasives.compare end)
+module ISet = Set.Make(Int)
(**
- * Given a set of integers s={i0,...,iN} and a list m, return the list of
+ * Given a set of integers s=\{i0,...,iN\} and a list m, return the list of
* elements of m that are at position i0,...,iN.
*)
@@ -535,10 +536,10 @@ struct
let get_left_construct term =
match Term.kind_of_term term with
- | Term.Construct(_,i) -> (i,[| |])
+ | Term.Construct((_,i),_) -> (i,[| |])
| Term.App(l,rst) ->
(match Term.kind_of_term l with
- | Term.Construct(_,i) -> (i,rst)
+ | Term.Construct((_,i),_) -> (i,rst)
| _ -> raise ParseError
)
| _ -> raise ParseError
@@ -577,7 +578,7 @@ struct
let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x)
- let rec dump_n x =
+ let dump_n x =
match x with
| Mc.N0 -> Lazy.force coq_N0
| Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p|])
@@ -590,12 +591,12 @@ struct
let pp_index o x = Printf.fprintf o "%i" (CoqToCaml.index x)
- let rec pp_n o x = output_string o (string_of_int (CoqToCaml.n x))
+ let pp_n o x = output_string o (string_of_int (CoqToCaml.n x))
let dump_pair t1 t2 dump_t1 dump_t2 (x,y) =
Term.mkApp(Lazy.force coq_pair,[| t1 ; t2 ; dump_t1 x ; dump_t2 y|])
- let rec parse_z term =
+ let parse_z term =
let (i,c) = get_left_construct term in
match i with
| 1 -> Mc.Z0
@@ -622,7 +623,7 @@ struct
let parse_q term =
match Term.kind_of_term term with
- | Term.App(c, args) -> if c = Lazy.force coq_Qmake then
+ | Term.App(c, args) -> if Constr.equal c (Lazy.force coq_Qmake) then
{Mc.qnum = parse_z args.(0) ; Mc.qden = parse_positive args.(1) }
else raise ParseError
| _ -> raise ParseError
@@ -780,7 +781,7 @@ struct
Printf.fprintf o "0" in
pp_cone o e
- let rec dump_op = function
+ let dump_op = function
| Mc.OpEq-> Lazy.force coq_OpEq
| Mc.OpNEq-> Lazy.force coq_OpNEq
| Mc.OpLe -> Lazy.force coq_OpLe
@@ -808,7 +809,7 @@ struct
let assoc_const x l =
try
- snd (List.find (fun (x',y) -> x = Lazy.force x') l)
+ snd (List.find (fun (x',y) -> Constr.equal x (Lazy.force x')) l)
with
Not_found -> raise ParseError
@@ -830,25 +831,33 @@ struct
coq_Qeq, Mc.OpEq
]
- let parse_zop (op,args) =
+ let has_typ gl t1 typ =
+ let ty = Retyping.get_type_of (Tacmach.pf_env gl) (Tacmach.project gl) t1 in
+ Constr.equal ty typ
+
+
+ let is_convertible gl t1 t2 =
+ Reductionops.is_conv (Tacmach.pf_env gl) (Tacmach.project gl) t1 t2
+
+ let parse_zop gl (op,args) =
match kind_of_term op with
- | Const x -> (assoc_const op zop_table, args.(0) , args.(1))
- | Ind(n,0) ->
- if op = Lazy.force coq_Eq && args.(0) = Lazy.force coq_Z
+ | Const (x,_) -> (assoc_const op zop_table, args.(0) , args.(1))
+ | Ind((n,0),_) ->
+ if Constr.equal op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_Z)
then (Mc.OpEq, args.(1), args.(2))
else raise ParseError
| _ -> failwith "parse_zop"
- let parse_rop (op,args) =
+ let parse_rop gl (op,args) =
match kind_of_term op with
- | Const x -> (assoc_const op rop_table, args.(0) , args.(1))
- | Ind(n,0) ->
- if op = Lazy.force coq_Eq && args.(0) = Lazy.force coq_R
+ | Const (x,_) -> (assoc_const op rop_table, args.(0) , args.(1))
+ | Ind((n,0),_) ->
+ if Constr.equal op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_R)
then (Mc.OpEq, args.(1), args.(2))
else raise ParseError
| _ -> failwith "parse_zop"
- let parse_qop (op,args) =
+ let parse_qop gl (op,args) =
(assoc_const op qop_table, args.(0) , args.(1))
let is_constant t = (* This is an approx *)
@@ -864,7 +873,7 @@ struct
let assoc_ops x l =
try
- snd (List.find (fun (x',y) -> x = Lazy.force x') l)
+ snd (List.find (fun (x',y) -> Constr.equal x (Lazy.force x')) l)
with
Not_found -> Ukn "Oups"
@@ -901,10 +910,7 @@ struct
let parse_expr parse_constant parse_exp ops_spec env term =
if debug
- then (Pp.pp (Pp.str "parse_expr: ");
- Pp.pp (Printer.prterm term);
- Pp.pp (Pp.str "\n");
- Pp.pp_flush ());
+ then Pp.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term);
(*
let constant_or_variable env term =
@@ -941,7 +947,7 @@ struct
let (expr,env) = parse_expr env args.(0) in
let power = (parse_exp expr args.(1)) in
(power , env)
- with e when e <> Sys.Break ->
+ with e when Errors.noncritical e ->
(* if the exponent is a variable *)
let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env)
end
@@ -994,9 +1000,9 @@ struct
let rec rconstant term =
match Term.kind_of_term term with
| Const x ->
- if term = Lazy.force coq_R0
+ if Constr.equal term (Lazy.force coq_R0)
then Mc.C0
- else if term = Lazy.force coq_R1
+ else if Constr.equal term (Lazy.force coq_R1)
then Mc.C1
else raise ParseError
| App(op,args) ->
@@ -1010,8 +1016,8 @@ struct
with
ParseError ->
match op with
- | op when op = Lazy.force coq_Rinv -> Mc.CInv(rconstant args.(0))
- | op when op = Lazy.force coq_IQR -> Mc.CQ (parse_q args.(0))
+ | op when Constr.equal op (Lazy.force coq_Rinv) -> Mc.CInv(rconstant args.(0))
+ | op when Constr.equal op (Lazy.force coq_IQR) -> Mc.CQ (parse_q args.(0))
(* | op when op = Lazy.force coq_IZR -> Mc.CZ (parse_z args.(0))*)
| _ -> raise ParseError
end
@@ -1021,11 +1027,7 @@ struct
let rconstant term =
if debug
- then (Pp.pp_flush ();
- Pp.pp (Pp.str "rconstant: ");
- Pp.pp (Printer.prterm term);
- Pp.pp (Pp.str "\n");
- Pp.pp_flush ());
+ then Pp.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ());
let res = rconstant term in
if debug then
(Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ;
@@ -1063,26 +1065,22 @@ struct
Mc.PEpow(expr,exp))
rop_spec
- let parse_arith parse_op parse_expr env cstr =
+ let parse_arith parse_op parse_expr env cstr gl =
if debug
- then (Pp.pp_flush ();
- Pp.pp (Pp.str "parse_arith: ");
- Pp.pp (Printer.prterm cstr);
- Pp.pp (Pp.str "\n");
- Pp.pp_flush ());
+ then Pp.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm cstr ++ fnl ());
match kind_of_term cstr with
| App(op,args) ->
- let (op,lhs,rhs) = parse_op (op,args) in
+ let (op,lhs,rhs) = parse_op gl (op,args) in
let (e1,env) = parse_expr env lhs in
let (e2,env) = parse_expr env rhs in
({Mc.flhs = e1; Mc.fop = op;Mc.frhs = e2},env)
| _ -> failwith "error : parse_arith(2)"
- let parse_zarith = parse_arith parse_zop parse_zexpr
+ let parse_zarith = parse_arith parse_zop parse_zexpr
- let parse_qarith = parse_arith parse_qop parse_qexpr
+ let parse_qarith = parse_arith parse_qop parse_qexpr
- let parse_rarith = parse_arith parse_rop parse_rexpr
+ let parse_rarith = parse_arith parse_rop parse_rexpr
(* generic parsing of arithmetic expressions *)
@@ -1115,14 +1113,13 @@ struct
* This is the big generic function for formula parsers.
*)
- let parse_formula parse_atom env tg term =
+ let parse_formula gl parse_atom env tg term =
let parse_atom env tg t =
try
- let (at,env) = parse_atom env t in
+ let (at,env) = parse_atom env t gl in
(A(at,tg,t), env,Tag.next tg)
- with e when e <> Sys.Break -> (X(t),env,tg)
- in
+ with e when Errors.noncritical e -> (X(t),env,tg) in
let rec xparse_formula env tg term =
match kind_of_term term with
@@ -1177,7 +1174,7 @@ struct
| (e::l) ->
let (name,expr,typ) = e in
xset (Term.mkNamedLetIn
- (Names.id_of_string name)
+ (Names.Id.of_string name)
expr typ acc) l in
xset concl l
@@ -1199,13 +1196,13 @@ let same_proof sg cl1 cl2 =
match sg with
| [] -> true
| n::sg ->
- (try List.nth cl1 n = List.nth cl2 n with e when e <> Sys.Break -> false)
+ (try Int.equal (List.nth cl1 n) (List.nth cl2 n) with Invalid_argument _ -> false)
&& (xsame_proof sg ) in
xsame_proof sg
let tags_of_clause tgs wit clause =
let rec xtags tgs = function
- | Mc.PsatzIn n -> Names.Idset.union tgs
+ | Mc.PsatzIn n -> Names.Id.Set.union tgs
(snd (List.nth clause (CoqToCaml.nat n) ))
| Mc.PsatzMulC(e,w) -> xtags tgs w
| Mc.PsatzMulE (w1,w2) | Mc.PsatzAdd(w1,w2) -> xtags (xtags tgs w1) w2
@@ -1214,7 +1211,7 @@ let tags_of_clause tgs wit clause =
(*let tags_of_cnf wits cnf =
List.fold_left2 (fun acc w cl -> tags_of_clause acc w cl)
- Names.Idset.empty wits cnf *)
+ Names.Id.Set.empty wits cnf *)
let find_witness prover polys1 = try_any prover polys1
@@ -1263,7 +1260,7 @@ let btree_of_array typ a =
let btree_of_array typ a =
try
btree_of_array typ a
- with x when x <> Sys.Break ->
+ with x when Errors.noncritical x ->
failwith (Printf.sprintf "btree of array : %s" (Printexc.to_string x))
let dump_varmap typ env =
@@ -1324,24 +1321,24 @@ let rec pp_proof_term o = function
(pp_psatz pp_z) c1 (pp_psatz pp_z) c2
(pp_list "[" "]" pp_proof_term) rst
-let rec parse_hyps parse_arith env tg hyps =
+let rec parse_hyps gl parse_arith env tg hyps =
match hyps with
| [] -> ([],env,tg)
| (i,t)::l ->
- let (lhyps,env,tg) = parse_hyps parse_arith env tg l in
+ let (lhyps,env,tg) = parse_hyps gl parse_arith env tg l in
try
- let (c,env,tg) = parse_formula parse_arith env tg t in
+ let (c,env,tg) = parse_formula gl parse_arith env tg t in
((i,c)::lhyps, env,tg)
- with e when e <> Sys.Break -> (lhyps,env,tg)
+ with e when Errors.noncritical e -> (lhyps,env,tg)
(*(if debug then Printf.printf "parse_arith : %s\n" x);*)
(*exception ParseError*)
-let parse_goal parse_arith env hyps term =
+let parse_goal gl parse_arith env hyps term =
(* try*)
- let (f,env,tg) = parse_formula parse_arith env (Tag.from 0) term in
- let (lhyps,env,tg) = parse_hyps parse_arith env tg hyps in
+ let (f,env,tg) = parse_formula gl parse_arith env (Tag.from 0) term in
+ let (lhyps,env,tg) = parse_hyps gl parse_arith env tg hyps in
(lhyps,f,env)
(* with Failure x -> raise ParseError*)
@@ -1385,22 +1382,31 @@ let rcst_domain_spec = lazy {
* witness.
*)
-let micromega_order_change spec cert cert_typ env ff gl =
+
+
+let micromega_order_change spec cert cert_typ env ff : Tacmach.tactic =
+ let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__z"^(string_of_int i)))) 0 env in
let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in
- let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
+ let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
let vm = dump_varmap (spec.typ) env in
- Tactics.change_in_concl None
+ (* todo : directly generate the proof term - or generalize befor conversion? *)
+ Tacticals.tclTHENSEQ [
+ (fun gl ->
+ Proofview.V82.of_tactic (Tactics.change_concl
(set
[
("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
("__varmap", vm, Term.mkApp
(Coqlib.gen_constant_in_modules "VarMap"
- [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|]));
+ [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|]));
("__wit", cert, cert_typ)
]
- (Tacmach.pf_concl gl)
- )
- gl
+ (Tacmach.pf_concl gl))) gl);
+ Tactics.generalize env ;
+ Tacticals.tclTHENSEQ (List.map (fun id -> Proofview.V82.of_tactic (Tactics.introduction id)) ids) ;
+ ]
+
+
(**
* The datastructures that aggregate prover attributes.
@@ -1476,7 +1482,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
(pp_ml_list prover.pp_f) (List.map fst new_cl) ;
flush stdout
end ; *)
- let res = try prover.compact prf remap with x when x <> Sys.Break ->
+ let res = try prover.compact prf remap with x when Errors.noncritical x ->
if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ;
(* This should not happen -- this is the recovery plan... *)
match prover.prover (List.map fst new_cl) with
@@ -1494,7 +1500,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
let is_proof_compatible (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) =
let hyps_idx = prover.hyps prf in
let hyps = selecti hyps_idx old_cl in
- is_sublist hyps new_cl in
+ is_sublist Pervasives.(=) hyps new_cl in
let cnf_res = List.combine cnf_ff res in (* we get pairs clause * proof *)
@@ -1644,7 +1650,7 @@ let micromega_gen
let concl = Tacmach.pf_concl gl in
let hyps = Tacmach.pf_hyps_types gl in
try
- let (hyps,concl,env) = parse_goal parse_arith Env.empty hyps concl in
+ let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
let env = Env.elements env in
let spec = Lazy.force spec in
@@ -1658,8 +1664,6 @@ let micromega_gen
(Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff'
]) gl
with
-(* | Failure x -> flush stdout ; Pp.pp_flush () ;
- Tacticals.tclFAIL 0 (Pp.str x) gl *)
| ParseError -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl
| CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
Tacticals.tclFAIL 0 (Pp.str
@@ -1679,7 +1683,7 @@ let micromega_order_changer cert env ff gl =
let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
let vm = dump_varmap (typ) env in
- Tactics.change_in_concl None
+ Proofview.V82.of_tactic (Tactics.change_concl
(set
[
("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
@@ -1689,7 +1693,7 @@ let micromega_order_changer cert env ff gl =
("__wit", cert, cert_typ)
]
(Tacmach.pf_concl gl)
- )
+ ))
gl
@@ -1710,7 +1714,7 @@ let micromega_genr prover gl =
let concl = Tacmach.pf_concl gl in
let hyps = Tacmach.pf_hyps_types gl in
try
- let (hyps,concl,env) = parse_goal parse_arith Env.empty hyps concl in
+ let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
let env = Env.elements env in
let spec = Lazy.force spec in
@@ -1729,8 +1733,6 @@ let micromega_genr prover gl =
micromega_order_changer res' env (abstract_wrt_formula ff' ff)
]) gl
with
-(* | Failure x -> flush stdout ; Pp.pp_flush () ;
- Tacticals.tclFAIL 0 (Pp.str x) gl *)
| ParseError -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl
| CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
Tacticals.tclFAIL 0 (Pp.str
@@ -1760,7 +1762,7 @@ open Persistent_cache
module Cache = PHashtable(struct
type t = (provername * micromega_polys)
- let equal = (=)
+ let equal = Pervasives.(=)
let hash = Hashtbl.hash
end)
@@ -1954,7 +1956,7 @@ let non_linear_prover_Z str o = {
module CacheZ = PHashtable(struct
type t = (Mc.z Mc.pol * Mc.op1) list
- let equal = (=)
+ let equal = Pervasives.(=)
let hash = Hashtbl.hash
end)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 10:03:24 +0000