From 99ad573113f5afc8bb5409649843567dee40ba40 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 16 Apr 2008 20:40:19 +0000 Subject: first-order --> firstorder (kills a warning about not being a valid id) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10805 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/extraction/CHANGES | 4 +- contrib/first-order/formula.ml | 270 --------------------------------- contrib/first-order/formula.mli | 77 ---------- contrib/first-order/g_ground.ml4 | 128 ---------------- contrib/first-order/ground.ml | 152 ------------------- contrib/first-order/ground.mli | 13 -- contrib/first-order/instances.ml | 206 -------------------------- contrib/first-order/instances.mli | 26 ---- contrib/first-order/rules.ml | 216 --------------------------- contrib/first-order/rules.mli | 54 ------- contrib/first-order/sequent.ml | 303 -------------------------------------- contrib/first-order/sequent.mli | 66 --------- contrib/first-order/unify.ml | 143 ------------------ contrib/first-order/unify.mli | 23 --- contrib/firstorder/formula.ml | 270 +++++++++++++++++++++++++++++++++ contrib/firstorder/formula.mli | 77 ++++++++++ contrib/firstorder/g_ground.ml4 | 128 ++++++++++++++++ contrib/firstorder/ground.ml | 152 +++++++++++++++++++ contrib/firstorder/ground.mli | 13 ++ contrib/firstorder/instances.ml | 206 ++++++++++++++++++++++++++ contrib/firstorder/instances.mli | 26 ++++ contrib/firstorder/rules.ml | 216 +++++++++++++++++++++++++++ contrib/firstorder/rules.mli | 54 +++++++ contrib/firstorder/sequent.ml | 303 ++++++++++++++++++++++++++++++++++++++ contrib/firstorder/sequent.mli | 66 +++++++++ contrib/firstorder/unify.ml | 143 ++++++++++++++++++ contrib/firstorder/unify.mli | 23 +++ 27 files changed, 1679 insertions(+), 1679 deletions(-) delete mode 100644 contrib/first-order/formula.ml delete mode 100644 contrib/first-order/formula.mli delete mode 100644 contrib/first-order/g_ground.ml4 delete mode 100644 contrib/first-order/ground.ml delete mode 100644 contrib/first-order/ground.mli delete mode 100644 contrib/first-order/instances.ml delete mode 100644 contrib/first-order/instances.mli delete mode 100644 contrib/first-order/rules.ml delete mode 100644 contrib/first-order/rules.mli delete mode 100644 contrib/first-order/sequent.ml delete mode 100644 contrib/first-order/sequent.mli delete mode 100644 contrib/first-order/unify.ml delete mode 100644 contrib/first-order/unify.mli create mode 100644 contrib/firstorder/formula.ml create mode 100644 contrib/firstorder/formula.mli create mode 100644 contrib/firstorder/g_ground.ml4 create mode 100644 contrib/firstorder/ground.ml create mode 100644 contrib/firstorder/ground.mli create mode 100644 contrib/firstorder/instances.ml create mode 100644 contrib/firstorder/instances.mli create mode 100644 contrib/firstorder/rules.ml create mode 100644 contrib/firstorder/rules.mli create mode 100644 contrib/firstorder/sequent.ml create mode 100644 contrib/firstorder/sequent.mli create mode 100644 contrib/firstorder/unify.ml create mode 100644 contrib/firstorder/unify.mli (limited to 'contrib') diff --git a/contrib/extraction/CHANGES b/contrib/extraction/CHANGES index 83ea4910c..acd1dbda4 100644 --- a/contrib/extraction/CHANGES +++ b/contrib/extraction/CHANGES @@ -346,8 +346,8 @@ Dyade/BDDS boolean tautology checker. Lyon/CIRCUITS multiplication via a modelization of a circuit. Lyon/FIRING-SQUAD print the states of the firing squad. Marseille/CIRCUITS compares integers via a modelization of a circuit. -Nancy/FOUnify unification of two first-orderde deux termes. -Rocq/ARITH/Chinese computation of the chinese remaindering. +Nancy/FOUnify unification of two first-order terms. +Rocq/ARITH/Chinese computation of the chinese remainder. Rocq/COC small coc typechecker. (test by B. Barras, not by me) Rocq/HIGMAN run the proof on one example. Rocq/GRAPHS linear constraints checker in Z. diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml deleted file mode 100644 index ac32f6abe..000000000 --- a/contrib/first-order/formula.ml +++ /dev/null @@ -1,270 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* metavariable - -exception Is_atom of constr - -let meta_succ m = m+1 - -let rec nb_prod_after n c= - match kind_of_term c with - | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else - 1+(nb_prod_after 0 b) - | _ -> 0 - -let construct_nhyps ind gls = - let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in - let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in - let hyp = nb_prod_after nparams in - Array.map hyp constr_types - -(* indhyps builds the array of arrays of constructor hyps for (ind largs)*) -let ind_hyps nevar ind largs gls= - let types= Inductiveops.arities_of_constructors (pf_env gls) ind in - let lp=Array.length types in - let myhyps i= - let t1=Term.prod_applist types.(i) largs in - let t2=snd (Sign.decompose_prod_n_assum nevar t1) in - fst (Sign.decompose_prod_assum t2) in - Array.init lp myhyps - -let special_nf gl= - let infos=Closure.create_clos_infos !red_flags (pf_env gl) in - (fun t -> Closure.norm_val infos (Closure.inject t)) - -let special_whd gl= - let infos=Closure.create_clos_infos !red_flags (pf_env gl) in - (fun t -> Closure.whd_val infos (Closure.inject t)) - -type kind_of_formula= - Arrow of constr*constr - | False of inductive*constr list - | And of inductive*constr list*bool - | Or of inductive*constr list*bool - | Exists of inductive*constr list - | Forall of constr*constr - | Atom of constr - -let rec kind_of_formula gl term = - let normalize=special_nf gl in - let cciterm=special_whd gl term in - match match_with_imp_term cciterm with - Some (a,b)-> Arrow(a,(pop b)) - |_-> - match match_with_forall_term cciterm with - Some (_,a,b)-> Forall(a,b) - |_-> - match match_with_nodep_ind cciterm with - Some (i,l,n)-> - let ind=destInd i in - let (mib,mip) = Global.lookup_inductive ind in - let nconstr=Array.length mip.mind_consnames in - if nconstr=0 then - False(ind,l) - else - let has_realargs=(n>0) in - let is_trivial= - let is_constant c = - nb_prod c = mib.mind_nparams in - array_exists is_constant mip.mind_nf_lc in - if Inductiveops.mis_is_recursive (ind,mib,mip) || - (has_realargs && not is_trivial) - then - Atom cciterm - else - if nconstr=1 then - And(ind,l,is_trivial) - else - Or(ind,l,is_trivial) - | _ -> - match match_with_sigma_type cciterm with - Some (i,l)-> Exists((destInd i),l) - |_-> Atom (normalize cciterm) - -type atoms = {positive:constr list;negative:constr list} - -type side = Hyp | Concl | Hint - -let no_atoms = (false,{positive=[];negative=[]}) - -let dummy_id=VarRef (id_of_string "_") (* "_" cannot be parsed *) - -let build_atoms gl metagen side cciterm = - let trivial =ref false - and positive=ref [] - and negative=ref [] in - let normalize=special_nf gl in - let rec build_rec env polarity cciterm= - match kind_of_formula gl cciterm with - False(_,_)->if not polarity then trivial:=true - | Arrow (a,b)-> - build_rec env (not polarity) a; - build_rec env polarity b - | And(i,l,b) | Or(i,l,b)-> - if b then - begin - let unsigned=normalize (substnl env 0 cciterm) in - if polarity then - positive:= unsigned :: !positive - else - negative:= unsigned :: !negative - end; - let v = ind_hyps 0 i l gl in - let g i _ (_,_,t) = - build_rec env polarity (lift i t) in - let f l = - list_fold_left_i g (1-(List.length l)) () l in - if polarity && (* we have a constant constructor *) - array_exists (function []->true|_->false) v - then trivial:=true; - Array.iter f v - | Exists(i,l)-> - let var=mkMeta (metagen true) in - let v =(ind_hyps 1 i l gl).(0) in - let g i _ (_,_,t) = - build_rec (var::env) polarity (lift i t) in - list_fold_left_i g (2-(List.length l)) () v - | Forall(_,b)-> - let var=mkMeta (metagen true) in - build_rec (var::env) polarity b - | Atom t-> - let unsigned=substnl env 0 t in - if not (isMeta unsigned) then (* discarding wildcard atoms *) - if polarity then - positive:= unsigned :: !positive - else - negative:= unsigned :: !negative in - begin - match side with - Concl -> build_rec [] true cciterm - | Hyp -> build_rec [] false cciterm - | Hint -> - let rels,head=decompose_prod cciterm in - let env=List.rev (List.map (fun _->mkMeta (metagen true)) rels) in - build_rec env false head;trivial:=false (* special for hints *) - end; - (!trivial, - {positive= !positive; - negative= !negative}) - -type right_pattern = - Rarrow - | Rand - | Ror - | Rfalse - | Rforall - | Rexists of metavariable*constr*bool - -type left_arrow_pattern= - LLatom - | LLfalse of inductive*constr list - | LLand of inductive*constr list - | LLor of inductive*constr list - | LLforall of constr - | LLexists of inductive*constr list - | LLarrow of constr*constr*constr - -type left_pattern= - Lfalse - | Land of inductive - | Lor of inductive - | Lforall of metavariable*constr*bool - | Lexists of inductive - | LA of constr*left_arrow_pattern - -type t={id:global_reference; - constr:constr; - pat:(left_pattern,right_pattern) sum; - atoms:atoms} - -let build_formula side nam typ gl metagen= - let normalize = special_nf gl in - try - let m=meta_succ(metagen false) in - let trivial,atoms= - if !qflag then - build_atoms gl metagen side typ - else no_atoms in - let pattern= - match side with - Concl -> - let pat= - match kind_of_formula gl typ with - False(_,_) -> Rfalse - | Atom a -> raise (Is_atom a) - | And(_,_,_) -> Rand - | Or(_,_,_) -> Ror - | Exists (i,l) -> - let (_,_,d)=list_last (ind_hyps 0 i l gl).(0) in - Rexists(m,d,trivial) - | Forall (_,a) -> Rforall - | Arrow (a,b) -> Rarrow in - Right pat - | _ -> - let pat= - match kind_of_formula gl typ with - False(i,_) -> Lfalse - | Atom a -> raise (Is_atom a) - | And(i,_,b) -> - if b then - let nftyp=normalize typ in raise (Is_atom nftyp) - else Land i - | Or(i,_,b) -> - if b then - let nftyp=normalize typ in raise (Is_atom nftyp) - else Lor i - | Exists (ind,_) -> Lexists ind - | Forall (d,_) -> - Lforall(m,d,trivial) - | Arrow (a,b) -> - let nfa=normalize a in - LA (nfa, - match kind_of_formula gl a with - False(i,l)-> LLfalse(i,l) - | Atom t-> LLatom - | And(i,l,_)-> LLand(i,l) - | Or(i,l,_)-> LLor(i,l) - | Arrow(a,c)-> LLarrow(a,c,b) - | Exists(i,l)->LLexists(i,l) - | Forall(_,_)->LLforall a) in - Left pat - in - Left {id=nam; - constr=normalize typ; - pat=pattern; - atoms=atoms} - with Is_atom a-> Right a (* already in nf *) - diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli deleted file mode 100644 index dca55d0bd..000000000 --- a/contrib/first-order/formula.mli +++ /dev/null @@ -1,77 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a -> int) -> ('b -> 'b -> int) -> - 'a -> 'a -> 'b -> 'b -> int - -val (==?) : ('a -> 'a -> 'b ->'b -> int) -> ('c -> 'c -> int) -> - 'a -> 'a -> 'b -> 'b -> 'c ->'c -> int - -type ('a,'b) sum = Left of 'a | Right of 'b - -type counter = bool -> metavariable - -val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array - -val ind_hyps : int -> inductive -> constr list -> - Proof_type.goal Tacmach.sigma -> Sign.rel_context array - -type atoms = {positive:constr list;negative:constr list} - -type side = Hyp | Concl | Hint - -val dummy_id: global_reference - -val build_atoms : Proof_type.goal Tacmach.sigma -> counter -> - side -> constr -> bool * atoms - -type right_pattern = - Rarrow - | Rand - | Ror - | Rfalse - | Rforall - | Rexists of metavariable*constr*bool - -type left_arrow_pattern= - LLatom - | LLfalse of inductive*constr list - | LLand of inductive*constr list - | LLor of inductive*constr list - | LLforall of constr - | LLexists of inductive*constr list - | LLarrow of constr*constr*constr - -type left_pattern= - Lfalse - | Land of inductive - | Lor of inductive - | Lforall of metavariable*constr*bool - | Lexists of inductive - | LA of constr*left_arrow_pattern - -type t={id: global_reference; - constr: constr; - pat: (left_pattern,right_pattern) sum; - atoms: atoms} - -(*exception Is_atom of constr*) - -val build_formula : side -> global_reference -> types -> - Proof_type.goal Tacmach.sigma -> counter -> (t,types) sum - diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4 deleted file mode 100644 index 3ee1db14c..000000000 --- a/contrib/first-order/g_ground.ml4 +++ /dev/null @@ -1,128 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Some !ground_depth); - optwrite= - (function - None->ground_depth:=3 - | Some i->ground_depth:=(max i 0))} - in - declare_int_option gdopt - -let congruence_depth=ref 100 - -let _= - let gdopt= - { optsync=true; - optname="Congruence Depth"; - optkey=SecondaryTable("Congruence","Depth"); - optread=(fun ()->Some !congruence_depth); - optwrite= - (function - None->congruence_depth:=0 - | Some i->congruence_depth:=(max i 0))} - in - declare_int_option gdopt - -let default_solver=(Tacinterp.interp <:tactic>) - -let fail_solver=tclFAIL 0 (Pp.str "GTauto failed") - -type external_env= - Ids of global_reference list - | Bases of Auto.hint_db_name list - | Void - -let gen_ground_tac flag taco ext gl= - let backup= !qflag in - try - qflag:=flag; - let solver= - match taco with - Some tac-> tac - | None-> default_solver in - let startseq= - match ext with - Void -> (fun gl -> empty_seq !ground_depth) - | Ids l-> create_with_ref_list l !ground_depth - | Bases l-> create_with_auto_hints l !ground_depth in - let result=ground_tac solver startseq gl in - qflag:=backup;result - with e ->qflag:=backup;raise e - -(* special for compatibility with Intuition - -let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str - -let defined_connectives=lazy - [[],EvalConstRef (destConst (constant "not")); - [],EvalConstRef (destConst (constant "iff"))] - -let normalize_evaluables= - onAllClauses - (function - None->unfold_in_concl (Lazy.force defined_connectives) - | Some id-> - unfold_in_hyp (Lazy.force defined_connectives) - (Tacexpr.InHypType id)) *) - -TACTIC EXTEND firstorder - [ "firstorder" tactic_opt(t) "using" ne_reference_list(l) ] -> - [ gen_ground_tac true (Option.map eval_tactic t) (Ids l) ] -| [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> - [ gen_ground_tac true (Option.map eval_tactic t) (Bases l) ] -| [ "firstorder" tactic_opt(t) ] -> - [ gen_ground_tac true (Option.map eval_tactic t) Void ] -END - -TACTIC EXTEND gintuition - [ "gintuition" tactic_opt(t) ] -> - [ gen_ground_tac false (Option.map eval_tactic t) Void ] -END - - -let default_declarative_automation gls = - tclORELSE - (tclORELSE (Auto.h_trivial [] None) - (Cctac.congruence_tac !congruence_depth [])) - (gen_ground_tac true - (Some (tclTHEN - default_solver - (Cctac.congruence_tac !congruence_depth []))) - Void) gls - - - -let () = - Decl_proof_instr.register_automation_tac default_declarative_automation - diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml deleted file mode 100644 index a8d5fc2ef..000000000 --- a/contrib/first-order/ground.ml +++ /dev/null @@ -1,152 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - predref:=Names.KNpred.add kn !predref - | _ ->() in - let g _ l=List.iter f l in - let h _ hdb=Auto.Hint_db.iter g hdb in - Util.Stringmap.iter h !Auto.searchtable; - red_flags:= - Closure.RedFlags.red_add_transparent - Closure.betaiotazeta (Names.Idpred.full,!predref) - end -*) - -let update_flags ()= - let predref=ref Names.Cpred.empty in - let f coe= - try - let kn=destConst (Classops.get_coercion_value coe) in - predref:=Names.Cpred.add kn !predref - with Invalid_argument "destConst"-> () in - List.iter f (Classops.coercions ()); - red_flags:= - Closure.RedFlags.red_add_transparent - Closure.betaiotazeta - (Names.Idpred.full,Names.Cpred.complement !predref) - -let ground_tac solver startseq gl= - update_flags (); - let rec toptac skipped seq gl= - if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 - then Pp.msgnl (Printer.pr_goal (sig_it gl)); - tclORELSE (axiom_tac seq.gl seq) - begin - try - let (hd,seq1)=take_formula seq - and re_add s=re_add_formula_list skipped s in - let continue=toptac [] - and backtrack gl=toptac (hd::skipped) seq1 gl in - match hd.pat with - Right rpat-> - begin - match rpat with - Rand-> - and_tac backtrack continue (re_add seq1) - | Rforall-> - let backtrack1= - if !qflag then - tclFAIL 0 (Pp.str "reversible in 1st order mode") - else - backtrack in - forall_tac backtrack1 continue (re_add seq1) - | Rarrow-> - arrow_tac backtrack continue (re_add seq1) - | Ror-> - or_tac backtrack continue (re_add seq1) - | Rfalse->backtrack - | Rexists(i,dom,triv)-> - let (lfp,seq2)=collect_quantified seq in - let backtrack2=toptac (lfp@skipped) seq2 in - if !qflag && seq.depth>0 then - quantified_tac lfp backtrack2 - continue (re_add seq) - else - backtrack2 (* need special backtracking *) - end - | Left lpat-> - begin - match lpat with - Lfalse-> - left_false_tac hd.id - | Land ind-> - left_and_tac ind backtrack - hd.id continue (re_add seq1) - | Lor ind-> - left_or_tac ind backtrack - hd.id continue (re_add seq1) - | Lforall (_,_,_)-> - let (lfp,seq2)=collect_quantified seq in - let backtrack2=toptac (lfp@skipped) seq2 in - if !qflag && seq.depth>0 then - quantified_tac lfp backtrack2 - continue (re_add seq) - else - backtrack2 (* need special backtracking *) - | Lexists ind -> - if !qflag then - left_exists_tac ind backtrack hd.id - continue (re_add seq1) - else backtrack - | LA (typ,lap)-> - let la_tac= - begin - match lap with - LLatom -> backtrack - | LLand (ind,largs) | LLor(ind,largs) - | LLfalse (ind,largs)-> - (ll_ind_tac ind largs backtrack - hd.id continue (re_add seq1)) - | LLforall p -> - if seq.depth>0 && !qflag then - (ll_forall_tac p backtrack - hd.id continue (re_add seq1)) - else backtrack - | LLexists (ind,l) -> - if !qflag then - ll_ind_tac ind l backtrack - hd.id continue (re_add seq1) - else - backtrack - | LLarrow (a,b,c) -> - (ll_arrow_tac a b c backtrack - hd.id continue (re_add seq1)) - end in - ll_atom_tac typ la_tac hd.id continue (re_add seq1) - end - with Heap.EmptyHeap->solver - end gl in - wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl - diff --git a/contrib/first-order/ground.mli b/contrib/first-order/ground.mli deleted file mode 100644 index 3c0e903fd..000000000 --- a/contrib/first-order/ground.mli +++ /dev/null @@ -1,13 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic - diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml deleted file mode 100644 index 56cea8e07..000000000 --- a/contrib/first-order/instances.ml +++ /dev/null @@ -1,206 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - (OrderedConstr.compare d1 d2) - | Real((m1,c1),n1),Real((m2,c2),n2)-> - ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n1 n2 c1 c2 - | Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1 - | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1 - -let compare_gr id1 id2= - if id1==id2 then 0 else - if id1==dummy_id then 1 - else if id2==dummy_id then -1 - else Pervasives.compare id1 id2 - -module OrderedInstance= -struct - type t=instance * Libnames.global_reference - let compare (inst1,id1) (inst2,id2)= - (compare_instance =? compare_gr) inst2 inst1 id2 id1 - (* we want a __decreasing__ total order *) -end - -module IS=Set.Make(OrderedInstance) - -let make_simple_atoms seq= - let ratoms= - match seq.glatom with - Some t->[t] - | None->[] - in {negative=seq.latoms;positive=ratoms} - -let do_sequent setref triv id seq i dom atoms= - let flag=ref true in - let phref=ref triv in - let do_atoms a1 a2 = - let do_pair t1 t2 = - match unif_atoms i dom t1 t2 with - None->() - | Some (Phantom _) ->phref:=true - | Some c ->flag:=false;setref:=IS.add (c,id) !setref in - List.iter (fun t->List.iter (do_pair t) a2.negative) a1.positive; - List.iter (fun t->List.iter (do_pair t) a2.positive) a1.negative in - HP.iter (fun lf->do_atoms atoms lf.atoms) seq.redexes; - do_atoms atoms (make_simple_atoms seq); - !flag && !phref - -let match_one_quantified_hyp setref seq lf= - match lf.pat with - Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))-> - if do_sequent setref triv lf.id seq i dom lf.atoms then - setref:=IS.add ((Phantom dom),lf.id) !setref - | _ ->anomaly "can't happen" - -let give_instances lf seq= - let setref=ref IS.empty in - List.iter (match_one_quantified_hyp setref seq) lf; - IS.elements !setref - -(* collector for the engine *) - -let rec collect_quantified seq= - try - let hd,seq1=take_formula seq in - (match hd.pat with - Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) -> - let (q,seq2)=collect_quantified seq1 in - ((hd::q),seq2) - | _->[],seq) - with Heap.EmptyHeap -> [],seq - -(* open instances processor *) - -let dummy_constr=mkMeta (-1) - -let dummy_bvid=id_of_string "x" - -let mk_open_instance id gl m t= - let env=pf_env gl in - let evmap=Refiner.project gl in - let var_id= - if id==dummy_id then dummy_bvid else - let typ=pf_type_of gl (constr_of_global id) in - (* since we know we will get a product, - reduction is not too expensive *) - let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in - match nam with - Name id -> id - | Anonymous -> dummy_bvid in - let revt=substl (list_tabulate (fun i->mkRel (m-i)) m) t in - let rec aux n avoid= - if n=0 then [] else - let nid=(fresh_id avoid var_id gl) in - (Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in - let nt=it_mkLambda_or_LetIn revt (aux m []) in - let rawt=Detyping.detype false [] [] nt in - let rec raux n t= - if n=0 then t else - match t with - RLambda(loc,name,k,_,t0)-> - let t1=raux (n-1) t0 in - RLambda(loc,name,k,RHole (dummy_loc,Evd.BinderType name),t1) - | _-> anomaly "can't happen" in - let ntt=try - Pretyping.Default.understand evmap env (raux m rawt) - with _ -> - error "Untypable instance, maybe higher-order non-prenex quantification" in - Sign.decompose_lam_n_assum m ntt - -(* tactics *) - -let left_instance_tac (inst,id) continue seq= - match inst with - Phantom dom-> - if lookup (id,None) seq then - tclFAIL 0 (Pp.str "already done") - else - tclTHENS (cut dom) - [tclTHENLIST - [introf; - (fun gls->generalize - [mkApp(constr_of_global id, - [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls); - introf; - tclSOLVE [wrap 1 false continue - (deepen (record (id,None) seq))]]; - tclTRY assumption] - | Real((m,t) as c,_)-> - if lookup (id,Some c) seq then - tclFAIL 0 (Pp.str "already done") - else - let special_generalize= - if m>0 then - fun gl-> - let (rc,ot)= mk_open_instance id gl m t in - let gt= - it_mkLambda_or_LetIn - (mkApp(constr_of_global id,[|ot|])) rc in - generalize [gt] gl - else - generalize [mkApp(constr_of_global id,[|t|])] - in - tclTHENLIST - [special_generalize; - introf; - tclSOLVE - [wrap 1 false continue (deepen (record (id,Some c) seq))]] - -let right_instance_tac inst continue seq= - match inst with - Phantom dom -> - tclTHENS (cut dom) - [tclTHENLIST - [introf; - (fun gls-> - split (Rawterm.ImplicitBindings - [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); - tclSOLVE [wrap 0 true continue (deepen seq)]]; - tclTRY assumption] - | Real ((0,t),_) -> - (tclTHEN (split (Rawterm.ImplicitBindings [t])) - (tclSOLVE [wrap 0 true continue (deepen seq)])) - | Real ((m,t),_) -> - tclFAIL 0 (Pp.str "not implemented ... yet") - -let instance_tac inst= - if (snd inst)==dummy_id then - right_instance_tac (fst inst) - else - left_instance_tac inst - -let quantified_tac lf backtrack continue seq gl= - let insts=give_instances lf seq in - tclORELSE - (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts)) - backtrack gl - - diff --git a/contrib/first-order/instances.mli b/contrib/first-order/instances.mli deleted file mode 100644 index aed2ec83d..000000000 --- a/contrib/first-order/instances.mli +++ /dev/null @@ -1,26 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Formula.t list * Sequent.t - -val give_instances : Formula.t list -> Sequent.t -> - (Unify.instance * global_reference) list - -val quantified_tac : Formula.t list -> seqtac with_backtracking - - - - diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml deleted file mode 100644 index b6112e653..000000000 --- a/contrib/first-order/rules.ml +++ /dev/null @@ -1,216 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* tactic) -> Sequent.t -> tactic - -type lseqtac= global_reference -> seqtac - -type 'a with_backtracking = tactic -> 'a - -let wrap n b continue seq gls= - check_for_interrupt (); - let nc=pf_hyps gls in - let env=pf_env gls in - let rec aux i nc ctx= - if i<=0 then seq else - match nc with - []->anomaly "Not the expected number of hyps" - | ((id,_,typ) as nd)::q-> - if occur_var env id (pf_concl gls) || - List.exists (occur_var_in_decl env id) ctx then - (aux (i-1) q (nd::ctx)) - else - add_formula Hyp (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in - let seq1=aux n nc [] in - let seq2=if b then - add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in - continue seq2 gls - -let id_of_global=function - VarRef id->id - | _->assert false - -let clear_global=function - VarRef id->clear [id] - | _->tclIDTAC - - -(* connection rules *) - -let axiom_tac t seq= - try exact_no_check (constr_of_global (find_left t seq)) - with Not_found->tclFAIL 0 (Pp.str "No axiom link") - -let ll_atom_tac a backtrack id continue seq= - tclIFTHENELSE - (try - tclTHENLIST - [generalize [mkApp(constr_of_global id, - [|constr_of_global (find_left a seq)|])]; - clear_global id; - intro] - with Not_found->tclFAIL 0 (Pp.str "No link")) - (wrap 1 false continue seq) backtrack - -(* right connectives rules *) - -let and_tac backtrack continue seq= - tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack - -let or_tac backtrack continue seq= - tclORELSE - (any_constructor false (Some (tclCOMPLETE (wrap 0 true continue seq)))) - backtrack - -let arrow_tac backtrack continue seq= - tclIFTHENELSE intro (wrap 1 true continue seq) - (tclORELSE - (tclTHEN introf (tclCOMPLETE (wrap 1 true continue seq))) - backtrack) -(* left connectives rules *) - -let left_and_tac ind backtrack id continue seq gls= - let n=(construct_nhyps ind gls).(0) in - tclIFTHENELSE - (tclTHENLIST - [simplest_elim (constr_of_global id); - clear_global id; - tclDO n intro]) - (wrap n false continue seq) - backtrack gls - -let left_or_tac ind backtrack id continue seq gls= - let v=construct_nhyps ind gls in - let f n= - tclTHENLIST - [clear_global id; - tclDO n intro; - wrap n false continue seq] in - tclIFTHENSVELSE - (simplest_elim (constr_of_global id)) - (Array.map f v) - backtrack gls - -let left_false_tac id= - simplest_elim (constr_of_global id) - -(* left arrow connective rules *) - -(* We use this function for false, and, or, exists *) - -let ll_ind_tac ind largs backtrack id continue seq gl= - let rcs=ind_hyps 0 ind largs gl in - let vargs=Array.of_list largs in - (* construire le terme H->B, le generaliser etc *) - let myterm i= - let rc=rcs.(i) in - let p=List.length rc in - let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) in - let vars=Array.init p (fun j->mkRel (p-j)) in - let capply=mkApp ((lift p cstr),vars) in - let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in - Sign.it_mkLambda_or_LetIn head rc in - let lp=Array.length rcs in - let newhyps=list_tabulate myterm lp in - tclIFTHENELSE - (tclTHENLIST - [generalize newhyps; - clear_global id; - tclDO lp intro]) - (wrap lp false continue seq) backtrack gl - -let ll_arrow_tac a b c backtrack id continue seq= - let cc=mkProd(Anonymous,a,(lift 1 b)) in - let d=mkLambda (Anonymous,b, - mkApp ((constr_of_global id), - [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in - tclORELSE - (tclTHENS (cut c) - [tclTHENLIST - [introf; - clear_global id; - wrap 1 false continue seq]; - tclTHENS (cut cc) - [exact_no_check (constr_of_global id); - tclTHENLIST - [generalize [d]; - clear_global id; - introf; - introf; - tclCOMPLETE (wrap 2 true continue seq)]]]) - backtrack - -(* quantifier rules (easy side) *) - -let forall_tac backtrack continue seq= - tclORELSE - (tclIFTHENELSE intro (wrap 0 true continue seq) - (tclORELSE - (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq))) - backtrack)) - (if !qflag then - tclFAIL 0 (Pp.str "reversible in 1st order mode") - else - backtrack) - -let left_exists_tac ind backtrack id continue seq gls= - let n=(construct_nhyps ind gls).(0) in - tclIFTHENELSE - (simplest_elim (constr_of_global id)) - (tclTHENLIST [clear_global id; - tclDO n intro; - (wrap (n-1) false continue seq)]) - backtrack - gls - -let ll_forall_tac prod backtrack id continue seq= - tclORELSE - (tclTHENS (cut prod) - [tclTHENLIST - [intro; - (fun gls-> - let id0=pf_nth_hyp_id gls 1 in - let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in - tclTHEN (generalize [term]) (clear [id0]) gls); - clear_global id; - intro; - tclCOMPLETE (wrap 1 false continue (deepen seq))]; - tclCOMPLETE (wrap 0 true continue (deepen seq))]) - backtrack - -(* rules for instantiation with unification moved to instances.ml *) - -(* special for compatibility with old Intuition *) - -let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str - -let defined_connectives=lazy - [[],EvalConstRef (destConst (constant "not")); - [],EvalConstRef (destConst (constant "iff"))] - -let normalize_evaluables= - onAllClauses - (function - None->unfold_in_concl (Lazy.force defined_connectives) - | Some ((_,id),_)-> - unfold_in_hyp (Lazy.force defined_connectives) - (([],id),Tacexpr.InHypTypeOnly)) diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli deleted file mode 100644 index 1c2c93a49..000000000 --- a/contrib/first-order/rules.mli +++ /dev/null @@ -1,54 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* tactic) -> Sequent.t -> tactic - -type lseqtac= global_reference -> seqtac - -type 'a with_backtracking = tactic -> 'a - -val wrap : int -> bool -> seqtac - -val id_of_global: global_reference -> identifier - -val clear_global: global_reference -> tactic - -val axiom_tac : constr -> Sequent.t -> tactic - -val ll_atom_tac : constr -> lseqtac with_backtracking - -val and_tac : seqtac with_backtracking - -val or_tac : seqtac with_backtracking - -val arrow_tac : seqtac with_backtracking - -val left_and_tac : inductive -> lseqtac with_backtracking - -val left_or_tac : inductive -> lseqtac with_backtracking - -val left_false_tac : global_reference -> tactic - -val ll_ind_tac : inductive -> constr list -> lseqtac with_backtracking - -val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking - -val forall_tac : seqtac with_backtracking - -val left_exists_tac : inductive -> lseqtac with_backtracking - -val ll_forall_tac : types -> lseqtac with_backtracking - -val normalize_evaluables : tactic diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml deleted file mode 100644 index fd5972fb7..000000000 --- a/contrib/first-order/sequent.ml +++ /dev/null @@ -1,303 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* if b then incr cnt;!cnt - -let priority = (* pure heuristics, <=0 for non reversible *) - function - Right rf-> - begin - match rf with - Rarrow -> 100 - | Rand -> 40 - | Ror -> -15 - | Rfalse -> -50 - | Rforall -> 100 - | Rexists (_,_,_) -> -29 - end - | Left lf -> - match lf with - Lfalse -> 999 - | Land _ -> 90 - | Lor _ -> 40 - | Lforall (_,_,_) -> -30 - | Lexists _ -> 60 - | LA(_,lap) -> - match lap with - LLatom -> 0 - | LLfalse (_,_) -> 100 - | LLand (_,_) -> 80 - | LLor (_,_) -> 70 - | LLforall _ -> -20 - | LLexists (_,_) -> 50 - | LLarrow (_,_,_) -> -10 - -let left_reversible lpat=(priority lpat)>0 - -module OrderedFormula= -struct - type t=Formula.t - let compare e1 e2= - (priority e1.pat) - (priority e2.pat) -end - -(* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare - the immediate subterms of [c1] of [c2] if needed; Cast's, - application associativity, binders name and Cases annotations are - not taken into account *) - -let rec compare_list f l1 l2= - match l1,l2 with - [],[]-> 0 - | [],_ -> -1 - | _,[] -> 1 - | (h1::q1),(h2::q2) -> (f =? (compare_list f)) h1 h2 q1 q2 - -let compare_array f v1 v2= - let l=Array.length v1 in - let c=l - Array.length v2 in - if c=0 then - let rec comp_aux i= - if i<0 then 0 - else - let ci=f v1.(i) v2.(i) in - if ci=0 then - comp_aux (i-1) - else ci - in comp_aux (l-1) - else c - -let compare_constr_int f t1 t2 = - match kind_of_term t1, kind_of_term t2 with - | Rel n1, Rel n2 -> n1 - n2 - | Meta m1, Meta m2 -> m1 - m2 - | Var id1, Var id2 -> Pervasives.compare id1 id2 - | Sort s1, Sort s2 -> Pervasives.compare s1 s2 - | Cast (c1,_,_), _ -> f c1 t2 - | _, Cast (c2,_,_) -> f t1 c2 - | Prod (_,t1,c1), Prod (_,t2,c2) - | Lambda (_,t1,c1), Lambda (_,t2,c2) -> - (f =? f) t1 t2 c1 c2 - | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> - ((f =? f) ==? f) b1 b2 t1 t2 c1 c2 - | App (_,_), App (_,_) -> - let c1,l1=decompose_app t1 - and c2,l2=decompose_app t2 in - (f =? (compare_list f)) c1 c2 l1 l2 - | Evar (e1,l1), Evar (e2,l2) -> - ((-) =? (compare_array f)) e1 e2 l1 l2 - | Const c1, Const c2 -> Pervasives.compare c1 c2 - | Ind c1, Ind c2 -> Pervasives.compare c1 c2 - | Construct c1, Construct c2 -> Pervasives.compare c1 c2 - | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> - ((f =? f) ==? (compare_array f)) p1 p2 c1 c2 bl1 bl2 - | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> - ((Pervasives.compare =? (compare_array f)) ==? (compare_array f)) - ln1 ln2 tl1 tl2 bl1 bl2 - | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> - ((Pervasives.compare =? (compare_array f)) ==? (compare_array f)) - ln1 ln2 tl1 tl2 bl1 bl2 - | _ -> Pervasives.compare t1 t2 - -let rec compare_constr m n= - compare_constr_int compare_constr m n - -module OrderedConstr= -struct - type t=constr - let compare=compare_constr -end - -type h_item = global_reference * (int*constr) option - -module Hitem= -struct - type t = h_item - let compare (id1,co1) (id2,co2)= - (Pervasives.compare - =? (fun oc1 oc2 -> - match oc1,oc2 with - Some (m1,c1),Some (m2,c2) -> - ((-) =? OrderedConstr.compare) m1 m2 c1 c2 - | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2 -end - -module CM=Map.Make(OrderedConstr) - -module History=Set.Make(Hitem) - -let cm_add typ nam cm= - try - let l=CM.find typ cm in CM.add typ (nam::l) cm - with - Not_found->CM.add typ [nam] cm - -let cm_remove typ nam cm= - try - let l=CM.find typ cm in - let l0=List.filter (fun id->id<>nam) l in - match l0 with - []->CM.remove typ cm - | _ ->CM.add typ l0 cm - with Not_found ->cm - -module HP=Heap.Functional(OrderedFormula) - -type t= - {redexes:HP.t; - context:(global_reference list) CM.t; - latoms:constr list; - gl:types; - glatom:constr option; - cnt:counter; - history:History.t; - depth:int} - -let deepen seq={seq with depth=seq.depth-1} - -let record item seq={seq with history=History.add item seq.history} - -let lookup item seq= - History.mem item seq.history || - match item with - (_,None)->false - | (id,Some ((m,t) as c))-> - let p (id2,o)= - match o with - None -> false - | Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in - History.exists p seq.history - -let rec add_formula side nam t seq gl= - match build_formula side nam t gl seq.cnt with - Left f-> - begin - match side with - Concl -> - {seq with - redexes=HP.add f seq.redexes; - gl=f.constr; - glatom=None} - | _ -> - {seq with - redexes=HP.add f seq.redexes; - context=cm_add f.constr nam seq.context} - end - | Right t-> - match side with - Concl -> - {seq with gl=t;glatom=Some t} - | _ -> - {seq with - context=cm_add t nam seq.context; - latoms=t::seq.latoms} - -let re_add_formula_list lf seq= - let do_one f cm= - if f.id == dummy_id then cm - else cm_add f.constr f.id cm in - {seq with - redexes=List.fold_right HP.add lf seq.redexes; - context=List.fold_right do_one lf seq.context} - -let find_left t seq=List.hd (CM.find t seq.context) - -(*let rev_left seq= - try - let lpat=(HP.maximum seq.redexes).pat in - left_reversible lpat - with Heap.EmptyHeap -> false -*) -let no_formula seq= - seq.redexes=HP.empty - -let rec take_formula seq= - let hd=HP.maximum seq.redexes - and hp=HP.remove seq.redexes in - if hd.id == dummy_id then - let nseq={seq with redexes=hp} in - if seq.gl==hd.constr then - hd,nseq - else - take_formula nseq (* discarding deprecated goal *) - else - hd,{seq with - redexes=hp; - context=cm_remove hd.constr hd.id seq.context} - -let empty_seq depth= - {redexes=HP.empty; - context=CM.empty; - latoms=[]; - gl=(mkMeta 1); - glatom=None; - cnt=newcnt (); - history=History.empty; - depth=depth} - -let create_with_ref_list l depth gl= - let f gr seq= - let c=constr_of_global gr in - let typ=(pf_type_of gl c) in - add_formula Hyp gr typ seq gl in - List.fold_right f l (empty_seq depth) - -open Auto - -let create_with_auto_hints l depth gl= - let seqref=ref (empty_seq depth) in - let f p_a_t = - match p_a_t.code with - Res_pf (c,_) | Give_exact c - | Res_pf_THEN_trivial_fail (c,_) -> - (try - let gr=global_of_constr c in - let typ=(pf_type_of gl c) in - seqref:=add_formula Hint gr typ !seqref gl - with Not_found->()) - | _-> () in - let g _ l=List.iter f l in - let h dbname= - let hdb= - try - searchtable_map dbname - with Not_found-> - error ("Firstorder: "^dbname^" : No such Hint database") in - Hint_db.iter g hdb in - List.iter h l; - !seqref - -let print_cmap map= - let print_entry c l s= - let xc=Constrextern.extern_constr false (Global.env ()) c in - str "| " ++ - Util.prlist Printer.pr_global l ++ - str " : " ++ - Ppconstr.pr_constr_expr xc ++ - cut () ++ - s in - msgnl (v 0 - (str "-----" ++ - cut () ++ - CM.fold print_entry map (mt ()) ++ - str "-----")) - - diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli deleted file mode 100644 index 51db9de16..000000000 --- a/contrib/first-order/sequent.mli +++ /dev/null @@ -1,66 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* global_reference -> global_reference list CM.t -> - global_reference list CM.t - -val cm_remove : constr -> global_reference -> global_reference list CM.t -> - global_reference list CM.t - -module HP: Heap.S with type elt=Formula.t - -type t = {redexes:HP.t; - context: global_reference list CM.t; - latoms:constr list; - gl:types; - glatom:constr option; - cnt:counter; - history:History.t; - depth:int} - -val deepen: t -> t - -val record: h_item -> t -> t - -val lookup: h_item -> t -> bool - -val add_formula : side -> global_reference -> constr -> t -> - Proof_type.goal sigma -> t - -val re_add_formula_list : Formula.t list -> t -> t - -val find_left : constr -> t -> global_reference - -val take_formula : t -> Formula.t * t - -val empty_seq : int -> t - -val create_with_ref_list : global_reference list -> - int -> Proof_type.goal sigma -> t - -val create_with_auto_hints : Auto.hint_db_name list -> - int -> Proof_type.goal sigma -> t - -val print_cmap: global_reference list CM.t -> unit diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml deleted file mode 100644 index 41a100c2b..000000000 --- a/contrib/first-order/unify.ml +++ /dev/null @@ -1,143 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (n,subst_meta [i,t] tn)) !sigma) in - let rec head_reduce t= - (* forbids non-sigma-normal meta in head position*) - match kind_of_term t with - Meta i-> - (try - head_reduce (List.assoc i !sigma) - with Not_found->t) - | _->t in - Queue.add (t1,t2) bige; - try while true do - let t1,t2=Queue.take bige in - let nt1=head_reduce (whd_betaiotazeta t1) - and nt2=head_reduce (whd_betaiotazeta t2) in - match (kind_of_term nt1),(kind_of_term nt2) with - Meta i,Meta j-> - if i<>j then - if i - let t=subst_meta !sigma nt2 in - if Intset.is_empty (free_rels t) && - not (occur_term (mkMeta i) t) then - bind i t else raise (UFAIL(nt1,nt2)) - | _,Meta i -> - let t=subst_meta !sigma nt1 in - if Intset.is_empty (free_rels t) && - not (occur_term (mkMeta i) t) then - bind i t else raise (UFAIL(nt1,nt2)) - | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige - | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige - | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> - Queue.add (a,c) bige;Queue.add (pop b,pop d) bige - | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> - Queue.add (pa,pb) bige; - Queue.add (ca,cb) bige; - let l=Array.length va in - if l<>(Array.length vb) then - raise (UFAIL (nt1,nt2)) - else - for i=0 to l-1 do - Queue.add (va.(i),vb.(i)) bige - done - | App(ha,va),App(hb,vb)-> - Queue.add (ha,hb) bige; - let l=Array.length va in - if l<>(Array.length vb) then - raise (UFAIL (nt1,nt2)) - else - for i=0 to l-1 do - Queue.add (va.(i),vb.(i)) bige - done - | _->if not (eq_constr nt1 nt2) then raise (UFAIL (nt1,nt2)) - done; - assert false - (* this place is unreachable but needed for the sake of typing *) - with Queue.Empty-> !sigma - -let value i t= - let add x y= - if x<0 then y else if y<0 then x else x+y in - let tref=mkMeta i in - let rec vaux term= - if term=tref then 0 else - let f v t=add v (vaux t) in - let vr=fold_constr f (-1) term in - if vr<0 then -1 else vr+1 in - vaux t - -type instance= - Real of (int*constr)*int - | Phantom of constr - -let mk_rel_inst t= - let new_rel=ref 1 in - let rel_env=ref [] in - let rec renum_rec d t= - match kind_of_term t with - Meta n-> - (try - mkRel (d+(List.assoc n !rel_env)) - with Not_found-> - let m= !new_rel in - incr new_rel; - rel_env:=(n,m) :: !rel_env; - mkRel (m+d)) - | _ -> map_constr_with_binders succ renum_rec d t - in - let nt=renum_rec 0 t in (!new_rel - 1,nt) - -let unif_atoms i dom t1 t2= - try - let t=List.assoc i (unif t1 t2) in - if isMeta t then Some (Phantom dom) - else Some (Real(mk_rel_inst t,value i t1)) - with - UFAIL(_,_) ->None - | Not_found ->Some (Phantom dom) - -let renum_metas_from k n t= (* requires n = max (free_rels t) *) - let l=list_tabulate (fun i->mkMeta (k+i)) n in - substl l t - -let more_general (m1,t1) (m2,t2)= - let mt1=renum_metas_from 0 m1 t1 - and mt2=renum_metas_from m1 m2 t2 in - try - let sigma=unif mt1 mt2 in - let p (n,t)= nfalse diff --git a/contrib/first-order/unify.mli b/contrib/first-order/unify.mli deleted file mode 100644 index d6cb3a082..000000000 --- a/contrib/first-order/unify.mli +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* constr -> (int*constr) list - -type instance= - Real of (int*constr)*int (* nb trous*terme*valeur heuristique *) - | Phantom of constr (* domaine de quantification *) - -val unif_atoms : metavariable -> constr -> constr -> constr -> instance option - -val more_general : (int*constr) -> (int*constr) -> bool diff --git a/contrib/firstorder/formula.ml b/contrib/firstorder/formula.ml new file mode 100644 index 000000000..ac32f6abe --- /dev/null +++ b/contrib/firstorder/formula.ml @@ -0,0 +1,270 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* metavariable + +exception Is_atom of constr + +let meta_succ m = m+1 + +let rec nb_prod_after n c= + match kind_of_term c with + | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else + 1+(nb_prod_after 0 b) + | _ -> 0 + +let construct_nhyps ind gls = + let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in + let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in + let hyp = nb_prod_after nparams in + Array.map hyp constr_types + +(* indhyps builds the array of arrays of constructor hyps for (ind largs)*) +let ind_hyps nevar ind largs gls= + let types= Inductiveops.arities_of_constructors (pf_env gls) ind in + let lp=Array.length types in + let myhyps i= + let t1=Term.prod_applist types.(i) largs in + let t2=snd (Sign.decompose_prod_n_assum nevar t1) in + fst (Sign.decompose_prod_assum t2) in + Array.init lp myhyps + +let special_nf gl= + let infos=Closure.create_clos_infos !red_flags (pf_env gl) in + (fun t -> Closure.norm_val infos (Closure.inject t)) + +let special_whd gl= + let infos=Closure.create_clos_infos !red_flags (pf_env gl) in + (fun t -> Closure.whd_val infos (Closure.inject t)) + +type kind_of_formula= + Arrow of constr*constr + | False of inductive*constr list + | And of inductive*constr list*bool + | Or of inductive*constr list*bool + | Exists of inductive*constr list + | Forall of constr*constr + | Atom of constr + +let rec kind_of_formula gl term = + let normalize=special_nf gl in + let cciterm=special_whd gl term in + match match_with_imp_term cciterm with + Some (a,b)-> Arrow(a,(pop b)) + |_-> + match match_with_forall_term cciterm with + Some (_,a,b)-> Forall(a,b) + |_-> + match match_with_nodep_ind cciterm with + Some (i,l,n)-> + let ind=destInd i in + let (mib,mip) = Global.lookup_inductive ind in + let nconstr=Array.length mip.mind_consnames in + if nconstr=0 then + False(ind,l) + else + let has_realargs=(n>0) in + let is_trivial= + let is_constant c = + nb_prod c = mib.mind_nparams in + array_exists is_constant mip.mind_nf_lc in + if Inductiveops.mis_is_recursive (ind,mib,mip) || + (has_realargs && not is_trivial) + then + Atom cciterm + else + if nconstr=1 then + And(ind,l,is_trivial) + else + Or(ind,l,is_trivial) + | _ -> + match match_with_sigma_type cciterm with + Some (i,l)-> Exists((destInd i),l) + |_-> Atom (normalize cciterm) + +type atoms = {positive:constr list;negative:constr list} + +type side = Hyp | Concl | Hint + +let no_atoms = (false,{positive=[];negative=[]}) + +let dummy_id=VarRef (id_of_string "_") (* "_" cannot be parsed *) + +let build_atoms gl metagen side cciterm = + let trivial =ref false + and positive=ref [] + and negative=ref [] in + let normalize=special_nf gl in + let rec build_rec env polarity cciterm= + match kind_of_formula gl cciterm with + False(_,_)->if not polarity then trivial:=true + | Arrow (a,b)-> + build_rec env (not polarity) a; + build_rec env polarity b + | And(i,l,b) | Or(i,l,b)-> + if b then + begin + let unsigned=normalize (substnl env 0 cciterm) in + if polarity then + positive:= unsigned :: !positive + else + negative:= unsigned :: !negative + end; + let v = ind_hyps 0 i l gl in + let g i _ (_,_,t) = + build_rec env polarity (lift i t) in + let f l = + list_fold_left_i g (1-(List.length l)) () l in + if polarity && (* we have a constant constructor *) + array_exists (function []->true|_->false) v + then trivial:=true; + Array.iter f v + | Exists(i,l)-> + let var=mkMeta (metagen true) in + let v =(ind_hyps 1 i l gl).(0) in + let g i _ (_,_,t) = + build_rec (var::env) polarity (lift i t) in + list_fold_left_i g (2-(List.length l)) () v + | Forall(_,b)-> + let var=mkMeta (metagen true) in + build_rec (var::env) polarity b + | Atom t-> + let unsigned=substnl env 0 t in + if not (isMeta unsigned) then (* discarding wildcard atoms *) + if polarity then + positive:= unsigned :: !positive + else + negative:= unsigned :: !negative in + begin + match side with + Concl -> build_rec [] true cciterm + | Hyp -> build_rec [] false cciterm + | Hint -> + let rels,head=decompose_prod cciterm in + let env=List.rev (List.map (fun _->mkMeta (metagen true)) rels) in + build_rec env false head;trivial:=false (* special for hints *) + end; + (!trivial, + {positive= !positive; + negative= !negative}) + +type right_pattern = + Rarrow + | Rand + | Ror + | Rfalse + | Rforall + | Rexists of metavariable*constr*bool + +type left_arrow_pattern= + LLatom + | LLfalse of inductive*constr list + | LLand of inductive*constr list + | LLor of inductive*constr list + | LLforall of constr + | LLexists of inductive*constr list + | LLarrow of constr*constr*constr + +type left_pattern= + Lfalse + | Land of inductive + | Lor of inductive + | Lforall of metavariable*constr*bool + | Lexists of inductive + | LA of constr*left_arrow_pattern + +type t={id:global_reference; + constr:constr; + pat:(left_pattern,right_pattern) sum; + atoms:atoms} + +let build_formula side nam typ gl metagen= + let normalize = special_nf gl in + try + let m=meta_succ(metagen false) in + let trivial,atoms= + if !qflag then + build_atoms gl metagen side typ + else no_atoms in + let pattern= + match side with + Concl -> + let pat= + match kind_of_formula gl typ with + False(_,_) -> Rfalse + | Atom a -> raise (Is_atom a) + | And(_,_,_) -> Rand + | Or(_,_,_) -> Ror + | Exists (i,l) -> + let (_,_,d)=list_last (ind_hyps 0 i l gl).(0) in + Rexists(m,d,trivial) + | Forall (_,a) -> Rforall + | Arrow (a,b) -> Rarrow in + Right pat + | _ -> + let pat= + match kind_of_formula gl typ with + False(i,_) -> Lfalse + | Atom a -> raise (Is_atom a) + | And(i,_,b) -> + if b then + let nftyp=normalize typ in raise (Is_atom nftyp) + else Land i + | Or(i,_,b) -> + if b then + let nftyp=normalize typ in raise (Is_atom nftyp) + else Lor i + | Exists (ind,_) -> Lexists ind + | Forall (d,_) -> + Lforall(m,d,trivial) + | Arrow (a,b) -> + let nfa=normalize a in + LA (nfa, + match kind_of_formula gl a with + False(i,l)-> LLfalse(i,l) + | Atom t-> LLatom + | And(i,l,_)-> LLand(i,l) + | Or(i,l,_)-> LLor(i,l) + | Arrow(a,c)-> LLarrow(a,c,b) + | Exists(i,l)->LLexists(i,l) + | Forall(_,_)->LLforall a) in + Left pat + in + Left {id=nam; + constr=normalize typ; + pat=pattern; + atoms=atoms} + with Is_atom a-> Right a (* already in nf *) + diff --git a/contrib/firstorder/formula.mli b/contrib/firstorder/formula.mli new file mode 100644 index 000000000..dca55d0bd --- /dev/null +++ b/contrib/firstorder/formula.mli @@ -0,0 +1,77 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a -> int) -> ('b -> 'b -> int) -> + 'a -> 'a -> 'b -> 'b -> int + +val (==?) : ('a -> 'a -> 'b ->'b -> int) -> ('c -> 'c -> int) -> + 'a -> 'a -> 'b -> 'b -> 'c ->'c -> int + +type ('a,'b) sum = Left of 'a | Right of 'b + +type counter = bool -> metavariable + +val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array + +val ind_hyps : int -> inductive -> constr list -> + Proof_type.goal Tacmach.sigma -> Sign.rel_context array + +type atoms = {positive:constr list;negative:constr list} + +type side = Hyp | Concl | Hint + +val dummy_id: global_reference + +val build_atoms : Proof_type.goal Tacmach.sigma -> counter -> + side -> constr -> bool * atoms + +type right_pattern = + Rarrow + | Rand + | Ror + | Rfalse + | Rforall + | Rexists of metavariable*constr*bool + +type left_arrow_pattern= + LLatom + | LLfalse of inductive*constr list + | LLand of inductive*constr list + | LLor of inductive*constr list + | LLforall of constr + | LLexists of inductive*constr list + | LLarrow of constr*constr*constr + +type left_pattern= + Lfalse + | Land of inductive + | Lor of inductive + | Lforall of metavariable*constr*bool + | Lexists of inductive + | LA of constr*left_arrow_pattern + +type t={id: global_reference; + constr: constr; + pat: (left_pattern,right_pattern) sum; + atoms: atoms} + +(*exception Is_atom of constr*) + +val build_formula : side -> global_reference -> types -> + Proof_type.goal Tacmach.sigma -> counter -> (t,types) sum + diff --git a/contrib/firstorder/g_ground.ml4 b/contrib/firstorder/g_ground.ml4 new file mode 100644 index 000000000..3ee1db14c --- /dev/null +++ b/contrib/firstorder/g_ground.ml4 @@ -0,0 +1,128 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Some !ground_depth); + optwrite= + (function + None->ground_depth:=3 + | Some i->ground_depth:=(max i 0))} + in + declare_int_option gdopt + +let congruence_depth=ref 100 + +let _= + let gdopt= + { optsync=true; + optname="Congruence Depth"; + optkey=SecondaryTable("Congruence","Depth"); + optread=(fun ()->Some !congruence_depth); + optwrite= + (function + None->congruence_depth:=0 + | Some i->congruence_depth:=(max i 0))} + in + declare_int_option gdopt + +let default_solver=(Tacinterp.interp <:tactic>) + +let fail_solver=tclFAIL 0 (Pp.str "GTauto failed") + +type external_env= + Ids of global_reference list + | Bases of Auto.hint_db_name list + | Void + +let gen_ground_tac flag taco ext gl= + let backup= !qflag in + try + qflag:=flag; + let solver= + match taco with + Some tac-> tac + | None-> default_solver in + let startseq= + match ext with + Void -> (fun gl -> empty_seq !ground_depth) + | Ids l-> create_with_ref_list l !ground_depth + | Bases l-> create_with_auto_hints l !ground_depth in + let result=ground_tac solver startseq gl in + qflag:=backup;result + with e ->qflag:=backup;raise e + +(* special for compatibility with Intuition + +let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str + +let defined_connectives=lazy + [[],EvalConstRef (destConst (constant "not")); + [],EvalConstRef (destConst (constant "iff"))] + +let normalize_evaluables= + onAllClauses + (function + None->unfold_in_concl (Lazy.force defined_connectives) + | Some id-> + unfold_in_hyp (Lazy.force defined_connectives) + (Tacexpr.InHypType id)) *) + +TACTIC EXTEND firstorder + [ "firstorder" tactic_opt(t) "using" ne_reference_list(l) ] -> + [ gen_ground_tac true (Option.map eval_tactic t) (Ids l) ] +| [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> + [ gen_ground_tac true (Option.map eval_tactic t) (Bases l) ] +| [ "firstorder" tactic_opt(t) ] -> + [ gen_ground_tac true (Option.map eval_tactic t) Void ] +END + +TACTIC EXTEND gintuition + [ "gintuition" tactic_opt(t) ] -> + [ gen_ground_tac false (Option.map eval_tactic t) Void ] +END + + +let default_declarative_automation gls = + tclORELSE + (tclORELSE (Auto.h_trivial [] None) + (Cctac.congruence_tac !congruence_depth [])) + (gen_ground_tac true + (Some (tclTHEN + default_solver + (Cctac.congruence_tac !congruence_depth []))) + Void) gls + + + +let () = + Decl_proof_instr.register_automation_tac default_declarative_automation + diff --git a/contrib/firstorder/ground.ml b/contrib/firstorder/ground.ml new file mode 100644 index 000000000..a8d5fc2ef --- /dev/null +++ b/contrib/firstorder/ground.ml @@ -0,0 +1,152 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + predref:=Names.KNpred.add kn !predref + | _ ->() in + let g _ l=List.iter f l in + let h _ hdb=Auto.Hint_db.iter g hdb in + Util.Stringmap.iter h !Auto.searchtable; + red_flags:= + Closure.RedFlags.red_add_transparent + Closure.betaiotazeta (Names.Idpred.full,!predref) + end +*) + +let update_flags ()= + let predref=ref Names.Cpred.empty in + let f coe= + try + let kn=destConst (Classops.get_coercion_value coe) in + predref:=Names.Cpred.add kn !predref + with Invalid_argument "destConst"-> () in + List.iter f (Classops.coercions ()); + red_flags:= + Closure.RedFlags.red_add_transparent + Closure.betaiotazeta + (Names.Idpred.full,Names.Cpred.complement !predref) + +let ground_tac solver startseq gl= + update_flags (); + let rec toptac skipped seq gl= + if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 + then Pp.msgnl (Printer.pr_goal (sig_it gl)); + tclORELSE (axiom_tac seq.gl seq) + begin + try + let (hd,seq1)=take_formula seq + and re_add s=re_add_formula_list skipped s in + let continue=toptac [] + and backtrack gl=toptac (hd::skipped) seq1 gl in + match hd.pat with + Right rpat-> + begin + match rpat with + Rand-> + and_tac backtrack continue (re_add seq1) + | Rforall-> + let backtrack1= + if !qflag then + tclFAIL 0 (Pp.str "reversible in 1st order mode") + else + backtrack in + forall_tac backtrack1 continue (re_add seq1) + | Rarrow-> + arrow_tac backtrack continue (re_add seq1) + | Ror-> + or_tac backtrack continue (re_add seq1) + | Rfalse->backtrack + | Rexists(i,dom,triv)-> + let (lfp,seq2)=collect_quantified seq in + let backtrack2=toptac (lfp@skipped) seq2 in + if !qflag && seq.depth>0 then + quantified_tac lfp backtrack2 + continue (re_add seq) + else + backtrack2 (* need special backtracking *) + end + | Left lpat-> + begin + match lpat with + Lfalse-> + left_false_tac hd.id + | Land ind-> + left_and_tac ind backtrack + hd.id continue (re_add seq1) + | Lor ind-> + left_or_tac ind backtrack + hd.id continue (re_add seq1) + | Lforall (_,_,_)-> + let (lfp,seq2)=collect_quantified seq in + let backtrack2=toptac (lfp@skipped) seq2 in + if !qflag && seq.depth>0 then + quantified_tac lfp backtrack2 + continue (re_add seq) + else + backtrack2 (* need special backtracking *) + | Lexists ind -> + if !qflag then + left_exists_tac ind backtrack hd.id + continue (re_add seq1) + else backtrack + | LA (typ,lap)-> + let la_tac= + begin + match lap with + LLatom -> backtrack + | LLand (ind,largs) | LLor(ind,largs) + | LLfalse (ind,largs)-> + (ll_ind_tac ind largs backtrack + hd.id continue (re_add seq1)) + | LLforall p -> + if seq.depth>0 && !qflag then + (ll_forall_tac p backtrack + hd.id continue (re_add seq1)) + else backtrack + | LLexists (ind,l) -> + if !qflag then + ll_ind_tac ind l backtrack + hd.id continue (re_add seq1) + else + backtrack + | LLarrow (a,b,c) -> + (ll_arrow_tac a b c backtrack + hd.id continue (re_add seq1)) + end in + ll_atom_tac typ la_tac hd.id continue (re_add seq1) + end + with Heap.EmptyHeap->solver + end gl in + wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl + diff --git a/contrib/firstorder/ground.mli b/contrib/firstorder/ground.mli new file mode 100644 index 000000000..3c0e903fd --- /dev/null +++ b/contrib/firstorder/ground.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic + diff --git a/contrib/firstorder/instances.ml b/contrib/firstorder/instances.ml new file mode 100644 index 000000000..56cea8e07 --- /dev/null +++ b/contrib/firstorder/instances.ml @@ -0,0 +1,206 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + (OrderedConstr.compare d1 d2) + | Real((m1,c1),n1),Real((m2,c2),n2)-> + ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n1 n2 c1 c2 + | Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1 + | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1 + +let compare_gr id1 id2= + if id1==id2 then 0 else + if id1==dummy_id then 1 + else if id2==dummy_id then -1 + else Pervasives.compare id1 id2 + +module OrderedInstance= +struct + type t=instance * Libnames.global_reference + let compare (inst1,id1) (inst2,id2)= + (compare_instance =? compare_gr) inst2 inst1 id2 id1 + (* we want a __decreasing__ total order *) +end + +module IS=Set.Make(OrderedInstance) + +let make_simple_atoms seq= + let ratoms= + match seq.glatom with + Some t->[t] + | None->[] + in {negative=seq.latoms;positive=ratoms} + +let do_sequent setref triv id seq i dom atoms= + let flag=ref true in + let phref=ref triv in + let do_atoms a1 a2 = + let do_pair t1 t2 = + match unif_atoms i dom t1 t2 with + None->() + | Some (Phantom _) ->phref:=true + | Some c ->flag:=false;setref:=IS.add (c,id) !setref in + List.iter (fun t->List.iter (do_pair t) a2.negative) a1.positive; + List.iter (fun t->List.iter (do_pair t) a2.positive) a1.negative in + HP.iter (fun lf->do_atoms atoms lf.atoms) seq.redexes; + do_atoms atoms (make_simple_atoms seq); + !flag && !phref + +let match_one_quantified_hyp setref seq lf= + match lf.pat with + Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))-> + if do_sequent setref triv lf.id seq i dom lf.atoms then + setref:=IS.add ((Phantom dom),lf.id) !setref + | _ ->anomaly "can't happen" + +let give_instances lf seq= + let setref=ref IS.empty in + List.iter (match_one_quantified_hyp setref seq) lf; + IS.elements !setref + +(* collector for the engine *) + +let rec collect_quantified seq= + try + let hd,seq1=take_formula seq in + (match hd.pat with + Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) -> + let (q,seq2)=collect_quantified seq1 in + ((hd::q),seq2) + | _->[],seq) + with Heap.EmptyHeap -> [],seq + +(* open instances processor *) + +let dummy_constr=mkMeta (-1) + +let dummy_bvid=id_of_string "x" + +let mk_open_instance id gl m t= + let env=pf_env gl in + let evmap=Refiner.project gl in + let var_id= + if id==dummy_id then dummy_bvid else + let typ=pf_type_of gl (constr_of_global id) in + (* since we know we will get a product, + reduction is not too expensive *) + let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in + match nam with + Name id -> id + | Anonymous -> dummy_bvid in + let revt=substl (list_tabulate (fun i->mkRel (m-i)) m) t in + let rec aux n avoid= + if n=0 then [] else + let nid=(fresh_id avoid var_id gl) in + (Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in + let nt=it_mkLambda_or_LetIn revt (aux m []) in + let rawt=Detyping.detype false [] [] nt in + let rec raux n t= + if n=0 then t else + match t with + RLambda(loc,name,k,_,t0)-> + let t1=raux (n-1) t0 in + RLambda(loc,name,k,RHole (dummy_loc,Evd.BinderType name),t1) + | _-> anomaly "can't happen" in + let ntt=try + Pretyping.Default.understand evmap env (raux m rawt) + with _ -> + error "Untypable instance, maybe higher-order non-prenex quantification" in + Sign.decompose_lam_n_assum m ntt + +(* tactics *) + +let left_instance_tac (inst,id) continue seq= + match inst with + Phantom dom-> + if lookup (id,None) seq then + tclFAIL 0 (Pp.str "already done") + else + tclTHENS (cut dom) + [tclTHENLIST + [introf; + (fun gls->generalize + [mkApp(constr_of_global id, + [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls); + introf; + tclSOLVE [wrap 1 false continue + (deepen (record (id,None) seq))]]; + tclTRY assumption] + | Real((m,t) as c,_)-> + if lookup (id,Some c) seq then + tclFAIL 0 (Pp.str "already done") + else + let special_generalize= + if m>0 then + fun gl-> + let (rc,ot)= mk_open_instance id gl m t in + let gt= + it_mkLambda_or_LetIn + (mkApp(constr_of_global id,[|ot|])) rc in + generalize [gt] gl + else + generalize [mkApp(constr_of_global id,[|t|])] + in + tclTHENLIST + [special_generalize; + introf; + tclSOLVE + [wrap 1 false continue (deepen (record (id,Some c) seq))]] + +let right_instance_tac inst continue seq= + match inst with + Phantom dom -> + tclTHENS (cut dom) + [tclTHENLIST + [introf; + (fun gls-> + split (Rawterm.ImplicitBindings + [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); + tclSOLVE [wrap 0 true continue (deepen seq)]]; + tclTRY assumption] + | Real ((0,t),_) -> + (tclTHEN (split (Rawterm.ImplicitBindings [t])) + (tclSOLVE [wrap 0 true continue (deepen seq)])) + | Real ((m,t),_) -> + tclFAIL 0 (Pp.str "not implemented ... yet") + +let instance_tac inst= + if (snd inst)==dummy_id then + right_instance_tac (fst inst) + else + left_instance_tac inst + +let quantified_tac lf backtrack continue seq gl= + let insts=give_instances lf seq in + tclORELSE + (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts)) + backtrack gl + + diff --git a/contrib/firstorder/instances.mli b/contrib/firstorder/instances.mli new file mode 100644 index 000000000..aed2ec83d --- /dev/null +++ b/contrib/firstorder/instances.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Formula.t list * Sequent.t + +val give_instances : Formula.t list -> Sequent.t -> + (Unify.instance * global_reference) list + +val quantified_tac : Formula.t list -> seqtac with_backtracking + + + + diff --git a/contrib/firstorder/rules.ml b/contrib/firstorder/rules.ml new file mode 100644 index 000000000..b6112e653 --- /dev/null +++ b/contrib/firstorder/rules.ml @@ -0,0 +1,216 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* tactic) -> Sequent.t -> tactic + +type lseqtac= global_reference -> seqtac + +type 'a with_backtracking = tactic -> 'a + +let wrap n b continue seq gls= + check_for_interrupt (); + let nc=pf_hyps gls in + let env=pf_env gls in + let rec aux i nc ctx= + if i<=0 then seq else + match nc with + []->anomaly "Not the expected number of hyps" + | ((id,_,typ) as nd)::q-> + if occur_var env id (pf_concl gls) || + List.exists (occur_var_in_decl env id) ctx then + (aux (i-1) q (nd::ctx)) + else + add_formula Hyp (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in + let seq1=aux n nc [] in + let seq2=if b then + add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in + continue seq2 gls + +let id_of_global=function + VarRef id->id + | _->assert false + +let clear_global=function + VarRef id->clear [id] + | _->tclIDTAC + + +(* connection rules *) + +let axiom_tac t seq= + try exact_no_check (constr_of_global (find_left t seq)) + with Not_found->tclFAIL 0 (Pp.str "No axiom link") + +let ll_atom_tac a backtrack id continue seq= + tclIFTHENELSE + (try + tclTHENLIST + [generalize [mkApp(constr_of_global id, + [|constr_of_global (find_left a seq)|])]; + clear_global id; + intro] + with Not_found->tclFAIL 0 (Pp.str "No link")) + (wrap 1 false continue seq) backtrack + +(* right connectives rules *) + +let and_tac backtrack continue seq= + tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack + +let or_tac backtrack continue seq= + tclORELSE + (any_constructor false (Some (tclCOMPLETE (wrap 0 true continue seq)))) + backtrack + +let arrow_tac backtrack continue seq= + tclIFTHENELSE intro (wrap 1 true continue seq) + (tclORELSE + (tclTHEN introf (tclCOMPLETE (wrap 1 true continue seq))) + backtrack) +(* left connectives rules *) + +let left_and_tac ind backtrack id continue seq gls= + let n=(construct_nhyps ind gls).(0) in + tclIFTHENELSE + (tclTHENLIST + [simplest_elim (constr_of_global id); + clear_global id; + tclDO n intro]) + (wrap n false continue seq) + backtrack gls + +let left_or_tac ind backtrack id continue seq gls= + let v=construct_nhyps ind gls in + let f n= + tclTHENLIST + [clear_global id; + tclDO n intro; + wrap n false continue seq] in + tclIFTHENSVELSE + (simplest_elim (constr_of_global id)) + (Array.map f v) + backtrack gls + +let left_false_tac id= + simplest_elim (constr_of_global id) + +(* left arrow connective rules *) + +(* We use this function for false, and, or, exists *) + +let ll_ind_tac ind largs backtrack id continue seq gl= + let rcs=ind_hyps 0 ind largs gl in + let vargs=Array.of_list largs in + (* construire le terme H->B, le generaliser etc *) + let myterm i= + let rc=rcs.(i) in + let p=List.length rc in + let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) in + let vars=Array.init p (fun j->mkRel (p-j)) in + let capply=mkApp ((lift p cstr),vars) in + let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in + Sign.it_mkLambda_or_LetIn head rc in + let lp=Array.length rcs in + let newhyps=list_tabulate myterm lp in + tclIFTHENELSE + (tclTHENLIST + [generalize newhyps; + clear_global id; + tclDO lp intro]) + (wrap lp false continue seq) backtrack gl + +let ll_arrow_tac a b c backtrack id continue seq= + let cc=mkProd(Anonymous,a,(lift 1 b)) in + let d=mkLambda (Anonymous,b, + mkApp ((constr_of_global id), + [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in + tclORELSE + (tclTHENS (cut c) + [tclTHENLIST + [introf; + clear_global id; + wrap 1 false continue seq]; + tclTHENS (cut cc) + [exact_no_check (constr_of_global id); + tclTHENLIST + [generalize [d]; + clear_global id; + introf; + introf; + tclCOMPLETE (wrap 2 true continue seq)]]]) + backtrack + +(* quantifier rules (easy side) *) + +let forall_tac backtrack continue seq= + tclORELSE + (tclIFTHENELSE intro (wrap 0 true continue seq) + (tclORELSE + (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq))) + backtrack)) + (if !qflag then + tclFAIL 0 (Pp.str "reversible in 1st order mode") + else + backtrack) + +let left_exists_tac ind backtrack id continue seq gls= + let n=(construct_nhyps ind gls).(0) in + tclIFTHENELSE + (simplest_elim (constr_of_global id)) + (tclTHENLIST [clear_global id; + tclDO n intro; + (wrap (n-1) false continue seq)]) + backtrack + gls + +let ll_forall_tac prod backtrack id continue seq= + tclORELSE + (tclTHENS (cut prod) + [tclTHENLIST + [intro; + (fun gls-> + let id0=pf_nth_hyp_id gls 1 in + let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in + tclTHEN (generalize [term]) (clear [id0]) gls); + clear_global id; + intro; + tclCOMPLETE (wrap 1 false continue (deepen seq))]; + tclCOMPLETE (wrap 0 true continue (deepen seq))]) + backtrack + +(* rules for instantiation with unification moved to instances.ml *) + +(* special for compatibility with old Intuition *) + +let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str + +let defined_connectives=lazy + [[],EvalConstRef (destConst (constant "not")); + [],EvalConstRef (destConst (constant "iff"))] + +let normalize_evaluables= + onAllClauses + (function + None->unfold_in_concl (Lazy.force defined_connectives) + | Some ((_,id),_)-> + unfold_in_hyp (Lazy.force defined_connectives) + (([],id),Tacexpr.InHypTypeOnly)) diff --git a/contrib/firstorder/rules.mli b/contrib/firstorder/rules.mli new file mode 100644 index 000000000..1c2c93a49 --- /dev/null +++ b/contrib/firstorder/rules.mli @@ -0,0 +1,54 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* tactic) -> Sequent.t -> tactic + +type lseqtac= global_reference -> seqtac + +type 'a with_backtracking = tactic -> 'a + +val wrap : int -> bool -> seqtac + +val id_of_global: global_reference -> identifier + +val clear_global: global_reference -> tactic + +val axiom_tac : constr -> Sequent.t -> tactic + +val ll_atom_tac : constr -> lseqtac with_backtracking + +val and_tac : seqtac with_backtracking + +val or_tac : seqtac with_backtracking + +val arrow_tac : seqtac with_backtracking + +val left_and_tac : inductive -> lseqtac with_backtracking + +val left_or_tac : inductive -> lseqtac with_backtracking + +val left_false_tac : global_reference -> tactic + +val ll_ind_tac : inductive -> constr list -> lseqtac with_backtracking + +val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking + +val forall_tac : seqtac with_backtracking + +val left_exists_tac : inductive -> lseqtac with_backtracking + +val ll_forall_tac : types -> lseqtac with_backtracking + +val normalize_evaluables : tactic diff --git a/contrib/firstorder/sequent.ml b/contrib/firstorder/sequent.ml new file mode 100644 index 000000000..fd5972fb7 --- /dev/null +++ b/contrib/firstorder/sequent.ml @@ -0,0 +1,303 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* if b then incr cnt;!cnt + +let priority = (* pure heuristics, <=0 for non reversible *) + function + Right rf-> + begin + match rf with + Rarrow -> 100 + | Rand -> 40 + | Ror -> -15 + | Rfalse -> -50 + | Rforall -> 100 + | Rexists (_,_,_) -> -29 + end + | Left lf -> + match lf with + Lfalse -> 999 + | Land _ -> 90 + | Lor _ -> 40 + | Lforall (_,_,_) -> -30 + | Lexists _ -> 60 + | LA(_,lap) -> + match lap with + LLatom -> 0 + | LLfalse (_,_) -> 100 + | LLand (_,_) -> 80 + | LLor (_,_) -> 70 + | LLforall _ -> -20 + | LLexists (_,_) -> 50 + | LLarrow (_,_,_) -> -10 + +let left_reversible lpat=(priority lpat)>0 + +module OrderedFormula= +struct + type t=Formula.t + let compare e1 e2= + (priority e1.pat) - (priority e2.pat) +end + +(* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare + the immediate subterms of [c1] of [c2] if needed; Cast's, + application associativity, binders name and Cases annotations are + not taken into account *) + +let rec compare_list f l1 l2= + match l1,l2 with + [],[]-> 0 + | [],_ -> -1 + | _,[] -> 1 + | (h1::q1),(h2::q2) -> (f =? (compare_list f)) h1 h2 q1 q2 + +let compare_array f v1 v2= + let l=Array.length v1 in + let c=l - Array.length v2 in + if c=0 then + let rec comp_aux i= + if i<0 then 0 + else + let ci=f v1.(i) v2.(i) in + if ci=0 then + comp_aux (i-1) + else ci + in comp_aux (l-1) + else c + +let compare_constr_int f t1 t2 = + match kind_of_term t1, kind_of_term t2 with + | Rel n1, Rel n2 -> n1 - n2 + | Meta m1, Meta m2 -> m1 - m2 + | Var id1, Var id2 -> Pervasives.compare id1 id2 + | Sort s1, Sort s2 -> Pervasives.compare s1 s2 + | Cast (c1,_,_), _ -> f c1 t2 + | _, Cast (c2,_,_) -> f t1 c2 + | Prod (_,t1,c1), Prod (_,t2,c2) + | Lambda (_,t1,c1), Lambda (_,t2,c2) -> + (f =? f) t1 t2 c1 c2 + | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> + ((f =? f) ==? f) b1 b2 t1 t2 c1 c2 + | App (_,_), App (_,_) -> + let c1,l1=decompose_app t1 + and c2,l2=decompose_app t2 in + (f =? (compare_list f)) c1 c2 l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> + ((-) =? (compare_array f)) e1 e2 l1 l2 + | Const c1, Const c2 -> Pervasives.compare c1 c2 + | Ind c1, Ind c2 -> Pervasives.compare c1 c2 + | Construct c1, Construct c2 -> Pervasives.compare c1 c2 + | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> + ((f =? f) ==? (compare_array f)) p1 p2 c1 c2 bl1 bl2 + | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> + ((Pervasives.compare =? (compare_array f)) ==? (compare_array f)) + ln1 ln2 tl1 tl2 bl1 bl2 + | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> + ((Pervasives.compare =? (compare_array f)) ==? (compare_array f)) + ln1 ln2 tl1 tl2 bl1 bl2 + | _ -> Pervasives.compare t1 t2 + +let rec compare_constr m n= + compare_constr_int compare_constr m n + +module OrderedConstr= +struct + type t=constr + let compare=compare_constr +end + +type h_item = global_reference * (int*constr) option + +module Hitem= +struct + type t = h_item + let compare (id1,co1) (id2,co2)= + (Pervasives.compare + =? (fun oc1 oc2 -> + match oc1,oc2 with + Some (m1,c1),Some (m2,c2) -> + ((-) =? OrderedConstr.compare) m1 m2 c1 c2 + | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2 +end + +module CM=Map.Make(OrderedConstr) + +module History=Set.Make(Hitem) + +let cm_add typ nam cm= + try + let l=CM.find typ cm in CM.add typ (nam::l) cm + with + Not_found->CM.add typ [nam] cm + +let cm_remove typ nam cm= + try + let l=CM.find typ cm in + let l0=List.filter (fun id->id<>nam) l in + match l0 with + []->CM.remove typ cm + | _ ->CM.add typ l0 cm + with Not_found ->cm + +module HP=Heap.Functional(OrderedFormula) + +type t= + {redexes:HP.t; + context:(global_reference list) CM.t; + latoms:constr list; + gl:types; + glatom:constr option; + cnt:counter; + history:History.t; + depth:int} + +let deepen seq={seq with depth=seq.depth-1} + +let record item seq={seq with history=History.add item seq.history} + +let lookup item seq= + History.mem item seq.history || + match item with + (_,None)->false + | (id,Some ((m,t) as c))-> + let p (id2,o)= + match o with + None -> false + | Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in + History.exists p seq.history + +let rec add_formula side nam t seq gl= + match build_formula side nam t gl seq.cnt with + Left f-> + begin + match side with + Concl -> + {seq with + redexes=HP.add f seq.redexes; + gl=f.constr; + glatom=None} + | _ -> + {seq with + redexes=HP.add f seq.redexes; + context=cm_add f.constr nam seq.context} + end + | Right t-> + match side with + Concl -> + {seq with gl=t;glatom=Some t} + | _ -> + {seq with + context=cm_add t nam seq.context; + latoms=t::seq.latoms} + +let re_add_formula_list lf seq= + let do_one f cm= + if f.id == dummy_id then cm + else cm_add f.constr f.id cm in + {seq with + redexes=List.fold_right HP.add lf seq.redexes; + context=List.fold_right do_one lf seq.context} + +let find_left t seq=List.hd (CM.find t seq.context) + +(*let rev_left seq= + try + let lpat=(HP.maximum seq.redexes).pat in + left_reversible lpat + with Heap.EmptyHeap -> false +*) +let no_formula seq= + seq.redexes=HP.empty + +let rec take_formula seq= + let hd=HP.maximum seq.redexes + and hp=HP.remove seq.redexes in + if hd.id == dummy_id then + let nseq={seq with redexes=hp} in + if seq.gl==hd.constr then + hd,nseq + else + take_formula nseq (* discarding deprecated goal *) + else + hd,{seq with + redexes=hp; + context=cm_remove hd.constr hd.id seq.context} + +let empty_seq depth= + {redexes=HP.empty; + context=CM.empty; + latoms=[]; + gl=(mkMeta 1); + glatom=None; + cnt=newcnt (); + history=History.empty; + depth=depth} + +let create_with_ref_list l depth gl= + let f gr seq= + let c=constr_of_global gr in + let typ=(pf_type_of gl c) in + add_formula Hyp gr typ seq gl in + List.fold_right f l (empty_seq depth) + +open Auto + +let create_with_auto_hints l depth gl= + let seqref=ref (empty_seq depth) in + let f p_a_t = + match p_a_t.code with + Res_pf (c,_) | Give_exact c + | Res_pf_THEN_trivial_fail (c,_) -> + (try + let gr=global_of_constr c in + let typ=(pf_type_of gl c) in + seqref:=add_formula Hint gr typ !seqref gl + with Not_found->()) + | _-> () in + let g _ l=List.iter f l in + let h dbname= + let hdb= + try + searchtable_map dbname + with Not_found-> + error ("Firstorder: "^dbname^" : No such Hint database") in + Hint_db.iter g hdb in + List.iter h l; + !seqref + +let print_cmap map= + let print_entry c l s= + let xc=Constrextern.extern_constr false (Global.env ()) c in + str "| " ++ + Util.prlist Printer.pr_global l ++ + str " : " ++ + Ppconstr.pr_constr_expr xc ++ + cut () ++ + s in + msgnl (v 0 + (str "-----" ++ + cut () ++ + CM.fold print_entry map (mt ()) ++ + str "-----")) + + diff --git a/contrib/firstorder/sequent.mli b/contrib/firstorder/sequent.mli new file mode 100644 index 000000000..51db9de16 --- /dev/null +++ b/contrib/firstorder/sequent.mli @@ -0,0 +1,66 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* global_reference -> global_reference list CM.t -> + global_reference list CM.t + +val cm_remove : constr -> global_reference -> global_reference list CM.t -> + global_reference list CM.t + +module HP: Heap.S with type elt=Formula.t + +type t = {redexes:HP.t; + context: global_reference list CM.t; + latoms:constr list; + gl:types; + glatom:constr option; + cnt:counter; + history:History.t; + depth:int} + +val deepen: t -> t + +val record: h_item -> t -> t + +val lookup: h_item -> t -> bool + +val add_formula : side -> global_reference -> constr -> t -> + Proof_type.goal sigma -> t + +val re_add_formula_list : Formula.t list -> t -> t + +val find_left : constr -> t -> global_reference + +val take_formula : t -> Formula.t * t + +val empty_seq : int -> t + +val create_with_ref_list : global_reference list -> + int -> Proof_type.goal sigma -> t + +val create_with_auto_hints : Auto.hint_db_name list -> + int -> Proof_type.goal sigma -> t + +val print_cmap: global_reference list CM.t -> unit diff --git a/contrib/firstorder/unify.ml b/contrib/firstorder/unify.ml new file mode 100644 index 000000000..41a100c2b --- /dev/null +++ b/contrib/firstorder/unify.ml @@ -0,0 +1,143 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (n,subst_meta [i,t] tn)) !sigma) in + let rec head_reduce t= + (* forbids non-sigma-normal meta in head position*) + match kind_of_term t with + Meta i-> + (try + head_reduce (List.assoc i !sigma) + with Not_found->t) + | _->t in + Queue.add (t1,t2) bige; + try while true do + let t1,t2=Queue.take bige in + let nt1=head_reduce (whd_betaiotazeta t1) + and nt2=head_reduce (whd_betaiotazeta t2) in + match (kind_of_term nt1),(kind_of_term nt2) with + Meta i,Meta j-> + if i<>j then + if i + let t=subst_meta !sigma nt2 in + if Intset.is_empty (free_rels t) && + not (occur_term (mkMeta i) t) then + bind i t else raise (UFAIL(nt1,nt2)) + | _,Meta i -> + let t=subst_meta !sigma nt1 in + if Intset.is_empty (free_rels t) && + not (occur_term (mkMeta i) t) then + bind i t else raise (UFAIL(nt1,nt2)) + | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige + | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige + | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> + Queue.add (a,c) bige;Queue.add (pop b,pop d) bige + | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> + Queue.add (pa,pb) bige; + Queue.add (ca,cb) bige; + let l=Array.length va in + if l<>(Array.length vb) then + raise (UFAIL (nt1,nt2)) + else + for i=0 to l-1 do + Queue.add (va.(i),vb.(i)) bige + done + | App(ha,va),App(hb,vb)-> + Queue.add (ha,hb) bige; + let l=Array.length va in + if l<>(Array.length vb) then + raise (UFAIL (nt1,nt2)) + else + for i=0 to l-1 do + Queue.add (va.(i),vb.(i)) bige + done + | _->if not (eq_constr nt1 nt2) then raise (UFAIL (nt1,nt2)) + done; + assert false + (* this place is unreachable but needed for the sake of typing *) + with Queue.Empty-> !sigma + +let value i t= + let add x y= + if x<0 then y else if y<0 then x else x+y in + let tref=mkMeta i in + let rec vaux term= + if term=tref then 0 else + let f v t=add v (vaux t) in + let vr=fold_constr f (-1) term in + if vr<0 then -1 else vr+1 in + vaux t + +type instance= + Real of (int*constr)*int + | Phantom of constr + +let mk_rel_inst t= + let new_rel=ref 1 in + let rel_env=ref [] in + let rec renum_rec d t= + match kind_of_term t with + Meta n-> + (try + mkRel (d+(List.assoc n !rel_env)) + with Not_found-> + let m= !new_rel in + incr new_rel; + rel_env:=(n,m) :: !rel_env; + mkRel (m+d)) + | _ -> map_constr_with_binders succ renum_rec d t + in + let nt=renum_rec 0 t in (!new_rel - 1,nt) + +let unif_atoms i dom t1 t2= + try + let t=List.assoc i (unif t1 t2) in + if isMeta t then Some (Phantom dom) + else Some (Real(mk_rel_inst t,value i t1)) + with + UFAIL(_,_) ->None + | Not_found ->Some (Phantom dom) + +let renum_metas_from k n t= (* requires n = max (free_rels t) *) + let l=list_tabulate (fun i->mkMeta (k+i)) n in + substl l t + +let more_general (m1,t1) (m2,t2)= + let mt1=renum_metas_from 0 m1 t1 + and mt2=renum_metas_from m1 m2 t2 in + try + let sigma=unif mt1 mt2 in + let p (n,t)= nfalse diff --git a/contrib/firstorder/unify.mli b/contrib/firstorder/unify.mli new file mode 100644 index 000000000..d6cb3a082 --- /dev/null +++ b/contrib/firstorder/unify.mli @@ -0,0 +1,23 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* constr -> (int*constr) list + +type instance= + Real of (int*constr)*int (* nb trous*terme*valeur heuristique *) + | Phantom of constr (* domaine de quantification *) + +val unif_atoms : metavariable -> constr -> constr -> constr -> instance option + +val more_general : (int*constr) -> (int*constr) -> bool -- cgit v1.2.3