aboutsummaryrefslogtreecommitdiff
path: root/plugins/rtauto
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/rtauto')
-rw-r--r--plugins/rtauto/g_rtauto.ml44
-rw-r--r--plugins/rtauto/proof_search.ml20
-rw-r--r--plugins/rtauto/refl_tauto.ml60
-rw-r--r--plugins/rtauto/refl_tauto.mli10
-rw-r--r--plugins/rtauto/vo.itarget2
5 files changed, 52 insertions, 44 deletions
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index d27b04834e..565308f72e 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -6,8 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
+
(*i camlp4deps: "grammar/grammar.cma" i*)
+open Ltac_plugin
+
DECLARE PLUGIN "rtauto_plugin"
TACTIC EXTEND rtauto
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 8b92611136..8dd7a5e469 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
open CErrors
open Util
open Goptions
@@ -46,8 +47,7 @@ let reset_info () =
let pruning = ref true
let opt_pruning=
- {optsync=true;
- optdepr=false;
+ {optdepr=false;
optname="Rtauto Pruning";
optkey=["Rtauto";"Pruning"];
optread=(fun () -> !pruning);
@@ -146,7 +146,7 @@ let add_step s sub =
| SI_Or_r,[p] -> I_Or_r p
| SE_Or i,[p1;p2] -> E_Or(i,p1,p2)
| SD_Or i,[p] -> D_Or(i,p)
- | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity")
+ | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity.")
type 'a with_deps =
{dep_it:'a;
@@ -168,7 +168,7 @@ type state =
let project = function
Complete prf -> prf
- | Incomplete (_,_) -> anomaly (Pp.str "not a successful state")
+ | Incomplete (_,_) -> anomaly (Pp.str "not a successful state.")
let pop n prf =
let nprf=
@@ -362,7 +362,7 @@ let search_norev seq=
(Arrow(f2,f3)))
f1;
add_hyp (embed nseq) f3]):: !goals
- | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen") in
+ | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen.") in
Int.Map.iter add_one seq.norev_hyps;
List.rev !goals
@@ -387,7 +387,7 @@ let search_in_rev_hyps seq=
| Arrow (Disjunct (f1,f2),f0) ->
[make_step (SD_Or(i)),
[add_hyp (add_hyp (embed nseq) (Arrow(f1,f0))) (Arrow (f2,f0))]]
- | _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen")
+ | _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen.")
with
Not_found -> search_norev seq
@@ -465,7 +465,7 @@ let branching = function
| _::next ->
s_info.nd_branching<-s_info.nd_branching+List.length next in
List.map (append stack) successors
- | Complete prf -> anomaly (Pp.str "already succeeded")
+ | Complete prf -> anomaly (Pp.str "already succeeded.")
open Pp
@@ -505,12 +505,12 @@ let pp_mapint map =
pp_form obj ++ str " => " ++
pp_list (fun (i,f) -> pp_form f) l ++
cut ()) ) map;
- str "{ " ++ vb 0 ++ (!pp) ++ str " }" ++ close ()
+ str "{ " ++ hv 0 (!pp ++ str " }")
let pp_connect (i,j,f1,f2) = pp_form f1 ++ str " => " ++ pp_form f2
let pp_gl gl= cut () ++
- str "{ " ++ vb 0 ++
+ str "{ " ++ hv 0 (
begin
match gl.abs with
None -> str ""
@@ -520,7 +520,7 @@ let pp_gl gl= cut () ++
str "norev =" ++ pp_intmap gl.norev_hyps ++ cut () ++
str "arrows=" ++ pp_mapint gl.right ++ cut () ++
str "cnx =" ++ pp_list pp_connect gl.cnx ++ cut () ++
- str "goal =" ++ pp_form gl.gl ++ str " }" ++ close ()
+ str "goal =" ++ pp_form gl.gl ++ str " }")
let pp =
function
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 4ed9079517..f84eebadce 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -6,8 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
+
module Search = Explore.Make(Proof_search)
+open Ltac_plugin
open CErrors
open Util
open Term
@@ -21,28 +24,28 @@ let step_count = ref 0
let node_count = ref 0
-let logic_constant =
- Coqlib.gen_constant "refl_tauto" ["Init";"Logic"]
+let logic_constant s = Universes.constr_of_global @@
+ Coqlib.coq_reference "refl_tauto" ["Init";"Logic"] s
let li_False = lazy (destInd (logic_constant "False"))
-let li_and = lazy (destInd (logic_constant "and"))
-let li_or = lazy (destInd (logic_constant "or"))
+let li_and = lazy (destInd (logic_constant "and"))
+let li_or = lazy (destInd (logic_constant "or"))
-let pos_constant =
- Coqlib.gen_constant "refl_tauto" ["Numbers";"BinNums"]
+let pos_constant s = Universes.constr_of_global @@
+ Coqlib.coq_reference "refl_tauto" ["Numbers";"BinNums"] s
let l_xI = lazy (pos_constant "xI")
let l_xO = lazy (pos_constant "xO")
let l_xH = lazy (pos_constant "xH")
-let store_constant =
- Coqlib.gen_constant "refl_tauto" ["rtauto";"Bintree"]
+let store_constant s = Universes.constr_of_global @@
+ Coqlib.coq_reference "refl_tauto" ["rtauto";"Bintree"] s
let l_empty = lazy (store_constant "empty")
let l_push = lazy (store_constant "push")
-let constant=
- Coqlib.gen_constant "refl_tauto" ["rtauto";"Rtauto"]
+let constant s = Universes.constr_of_global @@
+ Coqlib.coq_reference "refl_tauto" ["rtauto";"Rtauto"] s
let l_Reflect = lazy (constant "Reflect")
@@ -66,19 +69,18 @@ let l_E_Or = lazy (constant "E_Or")
let l_D_Or = lazy (constant "D_Or")
-let special_whd gl=
- let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in
- (fun t -> CClosure.whd_val infos (CClosure.inject t))
+let special_whd gl c =
+ Reductionops.clos_whd_flags CClosure.all (pf_env gl) (Tacmach.project gl) c
-let special_nf gl=
- let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in
- (fun t -> CClosure.norm_val infos (CClosure.inject t))
+let special_nf gl c =
+ Reductionops.clos_norm_flags CClosure.betaiotazeta (pf_env gl) (Tacmach.project gl) c
type atom_env=
{mutable next:int;
mutable env:(constr*int) list}
let make_atom atom_env term=
+ let term = EConstr.Unsafe.to_constr term in
try
let (_,i)=
List.find (fun (t,_)-> eq_constr term t) atom_env.env
@@ -90,13 +92,16 @@ let make_atom atom_env term=
Atom i
let rec make_form atom_env gls term =
+ let open EConstr in
+ let open Vars in
let normalize=special_nf gls in
let cciterm=special_whd gls term in
- match kind_of_term cciterm with
+ let sigma = Tacmach.project gls in
+ match EConstr.kind sigma cciterm with
Prod(_,a,b) ->
- if not (Termops.dependent (mkRel 1) b) &&
+ if noccurn sigma 1 b &&
Retyping.get_sort_family_of
- (pf_env gls) (Tacmach.project gls) a == InProp
+ (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
@@ -113,7 +118,7 @@ let rec make_form atom_env gls term =
| App(hd,argv) when Int.equal (Array.length argv) 2 ->
begin
try
- let ind, _ = destInd hd in
+ 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
@@ -134,7 +139,7 @@ let rec make_hyps atom_env gls lenv = function
| LocalAssum (id,typ)::rest ->
let hrec=
make_hyps atom_env gls (typ::lenv) rest in
- if List.exists (Termops.dependent (mkVar id)) lenv ||
+ 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
@@ -233,8 +238,7 @@ open Goptions
let verbose = ref false
let opt_verbose=
- {optsync=true;
- optdepr=false;
+ {optdepr=false;
optname="Rtauto Verbose";
optkey=["Rtauto";"Verbose"];
optread=(fun () -> !verbose);
@@ -245,8 +249,7 @@ let _ = declare_bool_option opt_verbose
let check = ref false
let opt_check=
- {optsync=true;
- optdepr=false;
+ {optdepr=false;
optname="Rtauto Check";
optkey=["Rtauto";"Check"];
optread=(fun () -> !check);
@@ -263,7 +266,7 @@ let rtauto_tac gls=
let _=
if Retyping.get_sort_family_of
(pf_env gls) (Tacmach.project gls) gl != InProp
- then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in
+ 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=
@@ -282,7 +285,7 @@ let rtauto_tac gls=
let prf =
try project (search_fun (init_state [] formula))
with Not_found ->
- errorlabstrm "rtauto" (Pp.str "rtauto couldn't find any proof") in
+ 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
@@ -298,7 +301,7 @@ let rtauto_tac gls=
build_form formula;
build_proof [] 0 prf|]) in
let term=
- applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in
+ applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in
let build_end_time=System.get_time () in
let _ = if !verbose then
begin
@@ -312,6 +315,7 @@ let rtauto_tac gls=
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
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index 9a14ac6c79..ac260e51ac 100644
--- a/plugins/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
@@ -7,18 +7,20 @@
(************************************************************************)
(* raises Not_found if no proof is found *)
+open API
+
type atom_env=
{mutable next:int;
mutable env:(Term.constr*int) list}
val make_form : atom_env ->
- Proof_type.goal Tacmach.sigma -> Term.types -> Proof_search.form
+ Proof_type.goal Evd.sigma -> EConstr.types -> Proof_search.form
val make_hyps :
atom_env ->
- Proof_type.goal Tacmach.sigma ->
- Term.types list ->
- Context.Named.t ->
+ Proof_type.goal Evd.sigma ->
+ EConstr.types list ->
+ EConstr.named_context ->
(Names.Id.t * Proof_search.form) list
val rtauto_tac : Proof_type.tactic
diff --git a/plugins/rtauto/vo.itarget b/plugins/rtauto/vo.itarget
deleted file mode 100644
index 4c9364ad72..0000000000
--- a/plugins/rtauto/vo.itarget
+++ /dev/null
@@ -1,2 +0,0 @@
-Bintree.vo
-Rtauto.vo
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 11:40:56 +0000