diff options
Diffstat (limited to 'plugins/micromega/coq_micromega.ml')
-rw-r--r-- | plugins/micromega/coq_micromega.ml | 170 |
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) |