diff options
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/const_omega.ml | 6 | ||||
| -rw-r--r-- | plugins/romega/const_omega.mli | 2 | ||||
| -rw-r--r-- | plugins/romega/g_romega.ml4 | 3 | ||||
| -rw-r--r-- | plugins/romega/refl_omega.ml | 34 |
4 files changed, 26 insertions, 19 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 4935fe4bbc..8d7ae51fc0 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -285,7 +285,7 @@ module type Int = sig val mk : Bigint.bigint -> Term.constr val parse_term : Term.constr -> parse_term - val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel + val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel (* check whether t is built only with numbers and + * - *) val is_scalar : Term.constr -> bool end @@ -350,10 +350,12 @@ let parse_term t = | _ -> Tother with e when Logic.catchable_exception e -> Tother +let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c + let parse_rel gl t = try match destructurate t with | Kapp("eq",[typ;t1;t2]) - when destructurate (Tacmach.pf_nf gl typ) = Kapp("Z",[]) -> Req (t1,t2) + when destructurate (EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr typ))) = Kapp("Z",[]) -> Req (t1,t2) | Kapp("Zne",[t1;t2]) -> Rne (t1,t2) | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2) | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2) diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index af50ea0fff..ee7ff451a9 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -168,7 +168,7 @@ module type Int = (* parsing a term (one level, except if a number is found) *) val parse_term : Term.constr -> parse_term (* parsing a relation expression, including = < <= >= > *) - val parse_rel : Proof_type.goal Tacmach.sigma -> Term.constr -> parse_rel + val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel (* Is a particular term only made of numbers and + * - ? *) val is_scalar : Term.constr -> bool end diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 2f38688d1f..df7e5cb99e 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -10,6 +10,7 @@ DECLARE PLUGIN "romega_plugin" +open Ltac_plugin open Names open Refl_omega open Stdarg @@ -37,7 +38,7 @@ let romega_tactic l = we'd better leave as little as possible in the conclusion, for an easier decidability argument. *) (Tactics.intros) - (Proofview.V82.tactic total_reflexive_omega_tactic)) + (total_reflexive_omega_tactic)) TACTIC EXTEND romega diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index ba882e39a2..a20589fb46 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -8,6 +8,7 @@ open Pp open Util +open Proofview.Notations open Const_omega module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -16,13 +17,12 @@ open OmegaSolver (* Especially useful debugging functions *) let debug = ref false -let show_goal gl = - if !debug then (); Tacticals.tclIDTAC gl +let show_goal = Tacticals.New.tclIDTAC let pp i = print_int i; print_newline (); flush stdout (* More readable than the prefix notation *) -let (>>) = Tacticals.tclTHEN +let (>>) = Tacticals.New.tclTHEN let mkApp = Term.mkApp @@ -739,7 +739,8 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = (* Destructuration des hypothèses et de la conclusion *) let reify_gl env gl = - let concl = Tacmach.pf_concl gl in + let concl = Tacmach.New.pf_concl gl in + let concl = EConstr.Unsafe.to_constr concl in let t_concl = Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in if !debug then begin @@ -748,6 +749,7 @@ let reify_gl env gl = end; let rec loop = function (i,t) :: lhyps -> + let t = EConstr.Unsafe.to_constr t in let t' = oproposition_of_constr env (false,[],i,[]) gl t in if !debug then begin Printf.printf " %s: " (Names.Id.to_string i); @@ -758,7 +760,7 @@ let reify_gl env gl = | [] -> if !debug then print_env_reification env; [] in - let t_lhyps = loop (Tacmach.pf_hyps_types gl) in + let t_lhyps = loop (Tacmach.New.pf_hyps_types gl) in (id_concl,t_concl) :: t_lhyps let rec destructurate_pos_hyp orig list_equations list_depends = function @@ -1222,7 +1224,7 @@ let resolution env full_reified_goal systems_list = (* variables a introduire *) let to_introduce = add_stated_equations env solution_tree in let stated_vars = List.map (fun (v,_,_,_) -> v) to_introduce in - let l_generalize_arg = List.map (fun (_,t,_,_) -> t) to_introduce in + let l_generalize_arg = List.map (fun (_,t,_,_) -> EConstr.of_constr t) to_introduce in let hyp_stated_vars = List.map (fun (_,_,_,id) -> CCEqua id) to_introduce in (* L'environnement de base se construit en deux morceaux : - les variables des équations utiles (et de la conclusion) @@ -1258,6 +1260,7 @@ let resolution env full_reified_goal systems_list = let reified = app coq_interp_sequent [| reified_concl;env_props_reified;env_terms_reified;reified_goal|] in + let reified = EConstr.of_constr reified in let normalize_equation e = let rec loop = function [] -> app (if e.e_negated then coq_p_invert else coq_p_step) @@ -1280,21 +1283,22 @@ let resolution env full_reified_goal systems_list = CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in let decompose_tactic = decompose_tree env context solution_tree in - Proofview.V82.of_tactic (Tactics.generalize - (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps))) >> - Proofview.V82.of_tactic (Tactics.change_concl reified) >> - Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >> + Tactics.generalize + (l_generalize_arg @ List.map EConstr.mkVar (List.tl l_hyps)) >> + Tactics.change_concl reified >> + Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic; normalization_trace|])) >> show_goal >> - Proofview.V82.of_tactic (Tactics.normalise_vm_in_concl) >> + Tactics.normalise_vm_in_concl >> (*i Alternatives to the previous line: - Normalisation without VM: Tactics.normalise_in_concl - Skip the conversion check and rely directly on the QED: Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >> i*) - Proofview.V82.of_tactic (Tactics.apply (Lazy.force coq_I)) + Tactics.apply (EConstr.of_constr (Lazy.force coq_I)) -let total_reflexive_omega_tactic gl = +let total_reflexive_omega_tactic = + Proofview.Goal.nf_enter { enter = begin fun gl -> Coqlib.check_required_library ["Coq";"romega";"ROmega"]; rst_omega_eq (); rst_omega_var (); @@ -1303,9 +1307,9 @@ let total_reflexive_omega_tactic gl = let full_reified_goal = reify_gl env gl in let systems_list = destructurate_hyps full_reified_goal in if !debug then display_systems systems_list; - resolution env full_reified_goal systems_list gl + resolution env full_reified_goal systems_list with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system" - + end } (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*) |