diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-22 14:24:47 +0200 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-22 15:26:59 +0200 |
commit | a8808e8d3935430f4dc24b68a828620a9e9f12a4 (patch) | |
tree | 98ce72284c49a64e001adc1642922542990c0398 | |
parent | f1e08dd28903513b71909326d60dc77366dca0fa (diff) |
romega: add a tactic named unsafe_romega (for debugging, or bold users)
In this variant, the proof term produced by romega isn't verified at
the tactic run-time (no vm_compute). In theory, [unsafe_romega] should
behave exactly as [romega], but faster. Now, if there's a bug in romega,
we'll be notified only at the following Qed. This could be interesting
for debugging purpose : you could inspect the produced buggish term
via a Show Proof.
-rw-r--r-- | plugins/romega/g_romega.ml4 | 12 | ||||
-rw-r--r-- | plugins/romega/refl_omega.ml | 20 |
2 files changed, 16 insertions, 16 deletions
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index df7e5cb99..c2d7d5050 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -21,7 +21,7 @@ let eval_tactic name = let tac = Tacenv.interp_ltac kn in Tacinterp.eval_tactic tac -let romega_tactic l = +let romega_tactic unsafe l = let tacs = List.map (function | "nat" -> eval_tactic "zify_nat" @@ -38,15 +38,15 @@ let romega_tactic l = we'd better leave as little as possible in the conclusion, for an easier decidability argument. *) (Tactics.intros) - (total_reflexive_omega_tactic)) - + (total_reflexive_omega_tactic unsafe)) TACTIC EXTEND romega -| [ "romega" ] -> [ romega_tactic [] ] +| [ "romega" ] -> [ romega_tactic false [] ] +| [ "unsafe_romega" ] -> [ romega_tactic true [] ] END TACTIC EXTEND romega' | [ "romega" "with" ne_ident_list(l) ] -> - [ romega_tactic (List.map Names.Id.to_string l) ] -| [ "romega" "with" "*" ] -> [ romega_tactic ["nat";"positive";"N";"Z"] ] + [ romega_tactic false (List.map Names.Id.to_string l) ] +| [ "romega" "with" "*" ] -> [ romega_tactic false ["nat";"positive";"N";"Z"] ] END diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 7b63d5503..7a48b9788 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -974,7 +974,7 @@ l'extraction d'un ensemble minimal de solutions permettant la résolution globale du système et enfin construit la trace qui permet de faire rejouer cette solution par la tactique réflexive. *) -let resolution env (reified_concl,reified_hyps) systems_list = +let resolution unsafe env (reified_concl,reified_hyps) systems_list = let num = ref 0 in let solve_system list_eq = let index = !num in @@ -1070,16 +1070,16 @@ let resolution env (reified_concl,reified_hyps) systems_list = Tactics.change_concl (EConstr.of_constr reified) >> Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic|])) >> show_goal >> - 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: - Tactics.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >> - i*) + (if unsafe then + (* Trust the produced term. Faster, but might fail later at Qed. + Also handy when debugging, e.g. via a Show Proof after romega. *) + Tactics.convert_concl_no_check + (EConstr.of_constr (Lazy.force coq_True)) Term.VMcast + else + Tactics.normalise_vm_in_concl) >> Tactics.apply (EConstr.of_constr (Lazy.force coq_I)) -let total_reflexive_omega_tactic = +let total_reflexive_omega_tactic unsafe = Proofview.Goal.nf_enter { enter = begin fun gl -> Coqlib.check_required_library ["Coq";"romega";"ROmega"]; rst_omega_eq (); @@ -1090,7 +1090,7 @@ let total_reflexive_omega_tactic = let full_reified_goal = (id_concl,Pnot concl) :: hyps in let systems_list = destructurate_hyps full_reified_goal in if !debug then display_systems systems_list; - resolution env reified_goal systems_list + resolution unsafe env reified_goal systems_list with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system" end } |