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.ml337
1 files changed, 337 insertions, 0 deletions
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
new file mode 100644
index 00000000..23cb0705
--- /dev/null
+++ b/plugins/rtauto/refl_tauto.ml
@@ -0,0 +1,337 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id$ *)
+
+module Search = Explore.Make(Proof_search)
+
+open Util
+open Term
+open Termops
+open Names
+open Evd
+open Tacmach
+open Proof_search
+
+let force count lazc = incr count;Lazy.force lazc
+
+let step_count = ref 0
+
+let node_count = ref 0
+
+let logic_constant =
+ Coqlib.gen_constant "refl_tauto" ["Init";"Logic"]
+
+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 data_constant =
+ Coqlib.gen_constant "refl_tauto" ["Init";"Datatypes"]
+
+let l_true_equals_true =
+ lazy (mkApp(logic_constant "refl_equal",
+ [|data_constant "bool";data_constant "true"|]))
+
+let pos_constant =
+ Coqlib.gen_constant "refl_tauto" ["NArith";"BinPos"]
+
+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 l_empty = lazy (store_constant "empty")
+let l_push = lazy (store_constant "push")
+
+let constant=
+ Coqlib.gen_constant "refl_tauto" ["rtauto";"Rtauto"]
+
+let l_Reflect = lazy (constant "Reflect")
+
+let l_Atom = lazy (constant "Atom")
+let l_Arrow = lazy (constant "Arrow")
+let l_Bot = lazy (constant "Bot")
+let l_Conjunct = lazy (constant "Conjunct")
+let l_Disjunct = lazy (constant "Disjunct")
+
+let l_Ax = lazy (constant "Ax")
+let l_I_Arrow = lazy (constant "I_Arrow")
+let l_E_Arrow = lazy (constant "E_Arrow")
+let l_D_Arrow = lazy (constant "D_Arrow")
+let l_E_False = lazy (constant "E_False")
+let l_I_And = lazy (constant "I_And")
+let l_E_And = lazy (constant "E_And")
+let l_D_And = lazy (constant "D_And")
+let l_I_Or_l = lazy (constant "I_Or_l")
+let l_I_Or_r = lazy (constant "I_Or_r")
+let l_E_Or = lazy (constant "E_Or")
+let l_D_Or = lazy (constant "D_Or")
+
+
+let special_whd gl=
+ let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in
+ (fun t -> Closure.whd_val infos (Closure.inject t))
+
+let special_nf gl=
+ let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in
+ (fun t -> Closure.norm_val infos (Closure.inject t))
+
+type atom_env=
+ {mutable next:int;
+ mutable env:(constr*int) list}
+
+let make_atom atom_env term=
+ try
+ let (_,i)=
+ List.find (fun (t,_)-> eq_constr term t) atom_env.env
+ in Atom i
+ with Not_found ->
+ let i=atom_env.next in
+ atom_env.env <- (term,i)::atom_env.env;
+ atom_env.next<- i + 1;
+ Atom i
+
+let rec make_form atom_env gls term =
+ let normalize=special_nf gls in
+ let cciterm=special_whd gls term in
+ match kind_of_term cciterm with
+ Prod(_,a,b) ->
+ if not (dependent (mkRel 1) b) &&
+ Retyping.get_sort_family_of
+ (pf_env gls) (Tacmach.project gls) 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 ind = Lazy.force li_False then
+ Bot
+ else
+ make_atom atom_env (normalize term)
+ | App(hd,argv) when Array.length argv = 2 ->
+ begin
+ try
+ let ind = destInd hd in
+ if ind = 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 ind = 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 Invalid_argument _ -> make_atom atom_env (normalize term)
+ end
+ | _ -> make_atom atom_env (normalize term)
+
+let rec make_hyps atom_env gls lenv = function
+ [] -> []
+ | (_,Some body,typ)::rest ->
+ make_hyps atom_env gls (typ::body::lenv) rest
+ | (id,None,typ)::rest ->
+ let hrec=
+ make_hyps atom_env gls (typ::lenv) rest in
+ if List.exists (dependent (mkVar id)) 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 rec build_pos n =
+ if n<=1 then force node_count l_xH
+ else if n land 1 = 0 then
+ mkApp (force node_count l_xO,[|build_pos (n asr 1)|])
+ else
+ mkApp (force node_count l_xI,[|build_pos (n asr 1)|])
+
+let rec build_form = function
+ Atom n -> mkApp (force node_count l_Atom,[|build_pos n|])
+ | Arrow (f1,f2) ->
+ mkApp (force node_count l_Arrow,[|build_form f1;build_form f2|])
+ | Bot -> force node_count l_Bot
+ | Conjunct (f1,f2) ->
+ mkApp (force node_count l_Conjunct,[|build_form f1;build_form f2|])
+ | Disjunct (f1,f2) ->
+ mkApp (force node_count l_Disjunct,[|build_form f1;build_form f2|])
+
+let rec decal k = function
+ [] -> k
+ | (start,delta)::rest ->
+ if k>start then
+ k - delta
+ else
+ decal k rest
+
+let add_pop size d pops=
+ match pops with
+ [] -> [size+d,d]
+ | (_,sum)::_ -> (size+sum,sum+d)::pops
+
+let rec build_proof pops size =
+ function
+ Ax i ->
+ mkApp (force step_count l_Ax,
+ [|build_pos (decal i pops)|])
+ | I_Arrow p ->
+ mkApp (force step_count l_I_Arrow,
+ [|build_proof pops (size + 1) p|])
+ | E_Arrow(i,j,p) ->
+ mkApp (force step_count l_E_Arrow,
+ [|build_pos (decal i pops);
+ build_pos (decal j pops);
+ build_proof pops (size + 1) p|])
+ | D_Arrow(i,p1,p2) ->
+ mkApp (force step_count l_D_Arrow,
+ [|build_pos (decal i pops);
+ build_proof pops (size + 2) p1;
+ build_proof pops (size + 1) p2|])
+ | E_False i ->
+ mkApp (force step_count l_E_False,
+ [|build_pos (decal i pops)|])
+ | I_And(p1,p2) ->
+ mkApp (force step_count l_I_And,
+ [|build_proof pops size p1;
+ build_proof pops size p2|])
+ | E_And(i,p) ->
+ mkApp (force step_count l_E_And,
+ [|build_pos (decal i pops);
+ build_proof pops (size + 2) p|])
+ | D_And(i,p) ->
+ mkApp (force step_count l_D_And,
+ [|build_pos (decal i pops);
+ build_proof pops (size + 1) p|])
+ | I_Or_l(p) ->
+ mkApp (force step_count l_I_Or_l,
+ [|build_proof pops size p|])
+ | I_Or_r(p) ->
+ mkApp (force step_count l_I_Or_r,
+ [|build_proof pops size p|])
+ | E_Or(i,p1,p2) ->
+ mkApp (force step_count l_E_Or,
+ [|build_pos (decal i pops);
+ build_proof pops (size + 1) p1;
+ build_proof pops (size + 1) p2|])
+ | D_Or(i,p) ->
+ mkApp (force step_count l_D_Or,
+ [|build_pos (decal i pops);
+ build_proof pops (size + 2) p|])
+ | Pop(d,p) ->
+ build_proof (add_pop size d pops) size p
+
+let build_env gamma=
+ List.fold_right (fun (p,_) e ->
+ mkApp(force node_count l_push,[|mkProp;p;e|]))
+ gamma.env (mkApp (force node_count l_empty,[|mkProp|]))
+
+open Goptions
+
+let verbose = ref false
+
+let opt_verbose=
+ {optsync=true;
+ optname="Rtauto Verbose";
+ optkey=["Rtauto";"Verbose"];
+ optread=(fun () -> !verbose);
+ optwrite=(fun b -> verbose:=b)}
+
+let _ = declare_bool_option opt_verbose
+
+let check = ref false
+
+let opt_check=
+ {optsync=true;
+ optname="Rtauto Check";
+ optkey=["Rtauto";"Check"];
+ optread=(fun () -> !check);
+ optwrite=(fun b -> check:=b)}
+
+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=gls.it.evar_concl in
+ 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
+ let glf=make_form gamma gls gl in
+ let hyps=make_hyps gamma gls [gl]
+ (Environ.named_context_of_val gls.it.evar_hyps) in
+ let formula=
+ List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in
+ let search_fun =
+ if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 then
+ Search.debug_depth_first
+ else
+ Search.depth_first in
+ let _ =
+ begin
+ reset_info ();
+ if !verbose then
+ msgnl (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 ->
+ errorlabstrm "rtauto" (Pp.str "rtauto couldn't find any proof") in
+ let search_end_time = System.get_time () in
+ let _ = if !verbose then
+ begin
+ msgnl (str "Proof tree found in " ++
+ System.fmt_time_difference search_start_time search_end_time);
+ pp_info ();
+ msgnl (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=
+ Term.applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in
+ let build_end_time=System.get_time () in
+ let _ = if !verbose then
+ begin
+ msgnl (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 result=
+ if !check then
+ Tactics.exact_check term gls
+ else
+ Tactics.exact_no_check term gls in
+ let tac_end_time = System.get_time () in
+ let _ =
+ if !check then msgnl (str "Proof term type-checking is on");
+ if !verbose then
+ msgnl (str "Internal tactic executed in " ++
+ System.fmt_time_difference tac_start_time tac_end_time) in
+ result
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 21:00:24 +0000