aboutsummaryrefslogtreecommitdiff
path: root/plugins/rtauto
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/rtauto')
-rw-r--r--plugins/rtauto/Bintree.v12
-rw-r--r--plugins/rtauto/g_rtauto.mlg2
-rw-r--r--plugins/rtauto/proof_search.ml2
-rw-r--r--plugins/rtauto/refl_tauto.ml259
-rw-r--r--plugins/rtauto/refl_tauto.mli19
5 files changed, 149 insertions, 145 deletions
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 99c02995fb..c2dec264ad 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -81,10 +81,12 @@ Section Store.
Variable A:Type.
+#[universes(template)]
Inductive Poption : Type:=
PSome : A -> Poption
| PNone : Poption.
+#[universes(template)]
Inductive Tree : Type :=
Tempty : Tree
| Branch0 : Tree -> Tree -> Tree
@@ -177,6 +179,7 @@ generalize i;clear i;induction j;destruct T;simpl in H|-*;
destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence.
Qed.
+#[universes(template)]
Record Store : Type :=
mkStore {index:positive;contents:Tree}.
@@ -191,6 +194,7 @@ Lemma get_empty : forall i, get i empty = PNone.
intro i; case i; unfold empty,get; simpl;reflexivity.
Qed.
+#[universes(template)]
Inductive Full : Store -> Type:=
F_empty : Full empty
| F_push : forall a S, Full S -> Full (push a S).
@@ -290,10 +294,10 @@ Qed.
End Store.
-Arguments PNone [A].
+Arguments PNone {A}.
Arguments PSome [A] _.
-Arguments Tempty [A].
+Arguments Tempty {A}.
Arguments Branch0 [A] _ _.
Arguments Branch1 [A] _ _ _.
@@ -307,7 +311,7 @@ Arguments mkStore [A] index contents.
Arguments index [A] s.
Arguments contents [A] s.
-Arguments empty [A].
+Arguments empty {A}.
Arguments get [A] i S.
Arguments push [A] a S.
@@ -315,7 +319,7 @@ Arguments get_empty [A] i.
Arguments get_push_Full [A] i a S _.
Arguments Full [A] _.
-Arguments F_empty [A].
+Arguments F_empty {A}.
Arguments F_push [A] a S _.
Arguments In [A] x S F.
diff --git a/plugins/rtauto/g_rtauto.mlg b/plugins/rtauto/g_rtauto.mlg
index 9c9fdcfa2f..d8724eb976 100644
--- a/plugins/rtauto/g_rtauto.mlg
+++ b/plugins/rtauto/g_rtauto.mlg
@@ -17,6 +17,6 @@ open Ltac_plugin
DECLARE PLUGIN "rtauto_plugin"
TACTIC EXTEND rtauto
-| [ "rtauto" ] -> { Proofview.V82.tactic (Refl_tauto.rtauto_tac) }
+| [ "rtauto" ] -> { Refl_tauto.rtauto_tac }
END
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 3de5923968..aab1e47555 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -54,7 +54,7 @@ let opt_pruning=
optread=(fun () -> !pruning);
optwrite=(fun b -> pruning:=b)}
-let _ = declare_bool_option opt_pruning
+let () = declare_bool_option opt_pruning
type form=
Atom of int
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 79418da27c..89528fe357 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -16,7 +16,7 @@ open CErrors
open Util
open Term
open Constr
-open Tacmach
+open Context
open Proof_search
open Context.Named.Declaration
@@ -26,11 +26,11 @@ let step_count = ref 0
let node_count = ref 0
-let li_False = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type"))
-let li_and = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type"))
-let li_or = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.or.type"))
+let li_False = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type"))
+let li_and = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type"))
+let li_or = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.or.type"))
-let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n))
+let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))
let l_xI = gen_constant "num.pos.xI"
let l_xO = gen_constant "num.pos.xO"
@@ -60,12 +60,11 @@ let l_I_Or_r = gen_constant "plugins.rtauto.I_Or_r"
let l_E_Or = gen_constant "plugins.rtauto.E_Or"
let l_D_Or = gen_constant "plugins.rtauto.D_Or"
+let special_whd env sigma c =
+ Reductionops.clos_whd_flags CClosure.all env sigma c
-let special_whd gl c =
- Reductionops.clos_whd_flags CClosure.all (pf_env gl) (Tacmach.project gl) c
-
-let special_nf gl c =
- Reductionops.clos_norm_flags CClosure.betaiotazeta (pf_env gl) (Tacmach.project gl) c
+let special_nf env sigma c =
+ Reductionops.clos_norm_flags CClosure.betaiotazeta env sigma c
type atom_env=
{mutable next:int;
@@ -83,61 +82,58 @@ let make_atom atom_env term=
atom_env.next<- i + 1;
Atom i
-let rec make_form atom_env gls term =
+let rec make_form env sigma atom_env term =
let open EConstr in
let open Vars in
- let normalize=special_nf gls in
- let cciterm=special_whd gls term in
- let sigma = Tacmach.project gls in
- match EConstr.kind sigma cciterm with
- Prod(_,a,b) ->
- if noccurn sigma 1 b &&
- Retyping.get_sort_family_of
- (pf_env gls) sigma a == InProp
- then
- let fa=make_form atom_env gls a in
- let fb=make_form atom_env gls b in
- Arrow (fa,fb)
- else
- make_atom atom_env (normalize term)
- | Cast(a,_,_) ->
- make_form atom_env gls a
- | Ind (ind, _) ->
- if Names.eq_ind ind (fst (Lazy.force li_False)) then
- Bot
- else
- make_atom atom_env (normalize term)
- | App(hd,argv) when Int.equal (Array.length argv) 2 ->
- begin
- try
- let ind, _ = destInd sigma hd in
- if Names.eq_ind ind (fst (Lazy.force li_and)) then
- let fa=make_form atom_env gls argv.(0) in
- let fb=make_form atom_env gls argv.(1) in
- Conjunct (fa,fb)
- else if Names.eq_ind ind (fst (Lazy.force li_or)) then
- let fa=make_form atom_env gls argv.(0) in
- let fb=make_form atom_env gls argv.(1) in
- Disjunct (fa,fb)
- else make_atom atom_env (normalize term)
- with DestKO -> make_atom atom_env (normalize term)
- end
- | _ -> make_atom atom_env (normalize term)
-
-let rec make_hyps atom_env gls lenv = function
+ let normalize = special_nf env sigma in
+ let cciterm = special_whd env sigma term in
+ match EConstr.kind sigma cciterm with
+ Prod(_,a,b) ->
+ if noccurn sigma 1 b &&
+ Retyping.get_sort_family_of env sigma a == InProp
+ then
+ let fa = make_form env sigma atom_env a in
+ let fb = make_form env sigma atom_env b in
+ Arrow (fa,fb)
+ else
+ make_atom atom_env (normalize term)
+ | Cast(a,_,_) ->
+ make_form env sigma atom_env a
+ | Ind (ind, _) ->
+ if Names.eq_ind ind (fst (Lazy.force li_False)) then
+ Bot
+ else
+ make_atom atom_env (normalize term)
+ | App(hd,argv) when Int.equal (Array.length argv) 2 ->
+ begin
+ try
+ let ind, _ = destInd sigma hd in
+ if Names.eq_ind ind (fst (Lazy.force li_and)) then
+ let fa = make_form env sigma atom_env argv.(0) in
+ let fb = make_form env sigma atom_env argv.(1) in
+ Conjunct (fa,fb)
+ else if Names.eq_ind ind (fst (Lazy.force li_or)) then
+ let fa = make_form env sigma atom_env argv.(0) in
+ let fb = make_form env sigma atom_env argv.(1) in
+ Disjunct (fa,fb)
+ else make_atom atom_env (normalize term)
+ with DestKO -> make_atom atom_env (normalize term)
+ end
+ | _ -> make_atom atom_env (normalize term)
+
+let rec make_hyps env sigma atom_env lenv = function
[] -> []
| LocalDef (_,body,typ)::rest ->
- make_hyps atom_env gls (typ::body::lenv) rest
+ make_hyps env sigma atom_env (typ::body::lenv) rest
| LocalAssum (id,typ)::rest ->
- let hrec=
- make_hyps atom_env gls (typ::lenv) rest in
- if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id c) lenv ||
- (Retyping.get_sort_family_of
- (pf_env gls) (Tacmach.project gls) typ != InProp)
- then
- hrec
- else
- (id,make_form atom_env gls typ)::hrec
+ let hrec=
+ make_hyps env sigma atom_env (typ::lenv) rest in
+ if List.exists (fun c -> Termops.local_occur_var Evd.empty (* FIXME *) id.binder_name c) lenv ||
+ (Retyping.get_sort_family_of env sigma typ != InProp)
+ then
+ hrec
+ else
+ (id,make_form env sigma atom_env typ)::hrec
let rec build_pos n =
if n<=1 then force node_count l_xH
@@ -236,7 +232,7 @@ let opt_verbose=
optread=(fun () -> !verbose);
optwrite=(fun b -> verbose:=b)}
-let _ = declare_bool_option opt_verbose
+let () = declare_bool_option opt_verbose
let check = ref false
@@ -247,77 +243,80 @@ let opt_check=
optread=(fun () -> !check);
optwrite=(fun b -> check:=b)}
-let _ = declare_bool_option opt_check
+let () = declare_bool_option opt_check
open Pp
-let rtauto_tac gls=
- Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"];
- let gamma={next=1;env=[]} in
- let gl=pf_concl gls in
- let _=
- if Retyping.get_sort_family_of
- (pf_env gls) (Tacmach.project gls) gl != InProp
- then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in
- let glf=make_form gamma gls gl in
- let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in
- let formula=
- List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in
- let search_fun = match Tacinterp.get_debug() with
- | Tactic_debug.DebugOn 0 -> Search.debug_depth_first
- | _ -> Search.depth_first
- in
- let _ =
- begin
- reset_info ();
+let rtauto_tac =
+ Proofview.Goal.enter begin fun gl ->
+ let hyps = Proofview.Goal.hyps gl in
+ let concl = Proofview.Goal.concl gl in
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"];
+ let gamma={next=1;env=[]} in
+ let () =
+ if Retyping.get_sort_family_of env sigma concl != InProp
+ then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in
+ let glf = make_form env sigma gamma concl in
+ let hyps = make_hyps env sigma gamma [concl] hyps in
+ let formula=
+ List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in
+ let search_fun = match Tacinterp.get_debug() with
+ | Tactic_debug.DebugOn 0 -> Search.debug_depth_first
+ | _ -> Search.depth_first
+ in
+ let () =
+ begin
+ reset_info ();
+ if !verbose then
+ Feedback.msg_info (str "Starting proof-search ...");
+ end in
+ let search_start_time = System.get_time () in
+ let prf =
+ try project (search_fun (init_state [] formula))
+ with Not_found ->
+ user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in
+ let search_end_time = System.get_time () in
+ let () = if !verbose then
+ begin
+ Feedback.msg_info (str "Proof tree found in " ++
+ System.fmt_time_difference search_start_time search_end_time);
+ pp_info ();
+ Feedback.msg_info (str "Building proof term ... ")
+ end in
+ let build_start_time=System.get_time () in
+ let () = step_count := 0; node_count := 0 in
+ let main = mkApp (force node_count l_Reflect,
+ [|build_env gamma;
+ build_form formula;
+ build_proof [] 0 prf|]) in
+ let term=
+ applistc main (List.rev_map (fun (id,_) -> mkVar id.binder_name) hyps) in
+ let build_end_time=System.get_time () in
+ let () = if !verbose then
+ begin
+ Feedback.msg_info (str "Proof term built in " ++
+ System.fmt_time_difference build_start_time build_end_time ++
+ fnl () ++
+ str "Proof size : " ++ int !step_count ++
+ str " steps" ++ fnl () ++
+ str "Proof term size : " ++ int (!step_count+ !node_count) ++
+ str " nodes (constants)" ++ fnl () ++
+ str "Giving proof term to Coq ... ")
+ end in
+ let tac_start_time = System.get_time () in
+ let term = EConstr.of_constr term in
+ let result=
+ if !check then
+ Tactics.exact_check term
+ else
+ Tactics.exact_no_check term in
+ let tac_end_time = System.get_time () in
+ let () =
+ if !check then Feedback.msg_info (str "Proof term type-checking is on");
if !verbose then
- Feedback.msg_info (str "Starting proof-search ...");
- end in
- let search_start_time = System.get_time () in
- let prf =
- try project (search_fun (init_state [] formula))
- with Not_found ->
- user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in
- let search_end_time = System.get_time () in
- let _ = if !verbose then
- begin
- Feedback.msg_info (str "Proof tree found in " ++
- System.fmt_time_difference search_start_time search_end_time);
- pp_info ();
- Feedback.msg_info (str "Building proof term ... ")
- end in
- let build_start_time=System.get_time () in
- let _ = step_count := 0; node_count := 0 in
- let main = mkApp (force node_count l_Reflect,
- [|build_env gamma;
- build_form formula;
- build_proof [] 0 prf|]) in
- let term=
- applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in
- let build_end_time=System.get_time () in
- let _ = if !verbose then
- begin
- Feedback.msg_info (str "Proof term built in " ++
- System.fmt_time_difference build_start_time build_end_time ++
- fnl () ++
- str "Proof size : " ++ int !step_count ++
- str " steps" ++ fnl () ++
- str "Proof term size : " ++ int (!step_count+ !node_count) ++
- str " nodes (constants)" ++ fnl () ++
- str "Giving proof term to Coq ... ")
- end in
- let tac_start_time = System.get_time () in
- let term = EConstr.of_constr term in
- let result=
- if !check then
- Proofview.V82.of_tactic (Tactics.exact_check term) gls
- else
- Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in
- let tac_end_time = System.get_time () in
- let _ =
- if !check then Feedback.msg_info (str "Proof term type-checking is on");
- if !verbose then
- Feedback.msg_info (str "Internal tactic executed in " ++
- System.fmt_time_difference tac_start_time tac_end_time) in
+ Feedback.msg_info (str "Internal tactic executed in " ++
+ System.fmt_time_difference tac_start_time tac_end_time) in
result
-
+ end
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index a91dd666a6..3de0ba44df 100644
--- a/plugins/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
@@ -14,14 +14,15 @@ type atom_env=
{mutable next:int;
mutable env:(Constr.t*int) list}
-val make_form : atom_env ->
- Goal.goal Evd.sigma -> EConstr.types -> Proof_search.form
+val make_form
+ : Environ.env -> Evd.evar_map -> atom_env
+ -> EConstr.types -> Proof_search.form
-val make_hyps :
- atom_env ->
- Goal.goal Evd.sigma ->
- EConstr.types list ->
- EConstr.named_context ->
- (Names.Id.t * Proof_search.form) list
+val make_hyps
+ : Environ.env -> Evd.evar_map
+ -> atom_env
+ -> EConstr.types list
+ -> EConstr.named_context
+ -> (Names.Id.t Context.binder_annot * Proof_search.form) list
-val rtauto_tac : Tacmach.tactic
+val rtauto_tac : unit Proofview.tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 11:26:10 +0000