diff options
Diffstat (limited to 'contrib/rtauto/refl_tauto.ml')
| -rw-r--r-- | contrib/rtauto/refl_tauto.ml | 337 |
1 files changed, 0 insertions, 337 deletions
diff --git a/contrib/rtauto/refl_tauto.ml b/contrib/rtauto/refl_tauto.ml deleted file mode 100644 index 81256f4a..00000000 --- a/contrib/rtauto/refl_tauto.ml +++ /dev/null @@ -1,337 +0,0 @@ -(************************************************************************) -(* 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: refl_tauto.ml 10478 2008-01-29 10:31:39Z notin $ *) - -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=SecondaryTable("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=SecondaryTable("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 - |