summaryrefslogtreecommitdiff
path: root/plugins/rtauto/refl_tauto.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/rtauto/refl_tauto.ml')
-rw-r--r--plugins/rtauto/refl_tauto.ml72
1 files changed, 39 insertions, 33 deletions
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 4ed90795..946b6dff 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -1,16 +1,21 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+
module Search = Explore.Make(Proof_search)
+open Ltac_plugin
open CErrors
open Util
open Term
+open Constr
open Tacmach
open Proof_search
open Context.Named.Declaration
@@ -21,28 +26,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,22 +71,21 @@ 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
+ List.find (fun (t,_)-> Constr.equal term t) atom_env.env
in Atom i
with Not_found ->
let i=atom_env.next in
@@ -90,13 +94,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 +120,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 +141,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 +240,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 +251,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 +268,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 +287,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 +303,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 +317,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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-08 02:23:02 +0000