diff options
-rw-r--r-- | contrib/first-order/formula.ml | 106 | ||||
-rw-r--r-- | contrib/first-order/formula.mli | 30 | ||||
-rw-r--r-- | contrib/first-order/ground.ml4 | 12 | ||||
-rw-r--r-- | contrib/first-order/rules.ml | 60 | ||||
-rw-r--r-- | contrib/first-order/rules.mli | 6 | ||||
-rw-r--r-- | contrib/first-order/sequent.ml | 2 |
6 files changed, 110 insertions, 106 deletions
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml index 42611884e..3b387d73a 100644 --- a/contrib/first-order/formula.ml +++ b/contrib/first-order/formula.ml @@ -29,38 +29,12 @@ let (==?) fg h i1 i2 j1 j2 k1 k2= if c=0 then h k1 k2 else c type ('a,'b) sum = Left of 'a | Right of 'b - -type kind_of_formula= - Arrow of constr*constr - |And of inductive*constr list - |Or of inductive*constr list - |Exists of inductive*constr list - |Forall of constr*constr - |Atom of constr - |Evaluable of evaluable_global_reference*constr - |False type counter = bool -> metavariable -let constant path str () = Coqlib.gen_constant "User" ["Init";path] str - -let op2bool = function Some _->true | None->false - -let id_not=constant "Logic" "not" -let id_iff=constant "Logic" "iff" - -let defined_connectives=lazy - [[],EvalConstRef (destConst (id_not ())); - [],EvalConstRef (destConst (id_iff ()))] +exception Is_atom of constr -let match_with_evaluable t= - match kind_of_term t with - App (hd,b)-> - if (hd=id_not () && (Array.length b) = 1) || - (hd=id_iff () && (Array.length b) = 2) then - Some(destConst hd,t) - else None - | _-> None +let meta_succ m = m+1 let rec nb_prod_after n c= match kind_of_term c with @@ -75,22 +49,50 @@ let nhyps mip = let construct_nhyps ind= nhyps (snd (Global.lookup_inductive ind)) -(* builds the array of arrays of constructor hyps for (ind largs)*) - +(* indhyps builds the array of arrays of constructor hyps for (ind largs)*) let ind_hyps nevar ind largs= let (mib,mip) = Global.lookup_inductive ind in let n = mip.mind_nparams in -(* assert (n=(List.length largs));*) - let lp=Array.length mip.mind_consnames in - let types= mip.mind_nf_lc 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 kind_of_formula term = + (* assert (n=(List.length largs));*) + let lp=Array.length mip.mind_consnames in + let types= mip.mind_nf_lc 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 constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str + +let id_not=lazy (destConst (constant "not")) +let id_iff=lazy (destConst (constant "iff")) + +let match_with_evaluable gl t= + let env=pf_env gl in + match kind_of_term t with + App (hd,b)-> + (match kind_of_term hd with + Const cst-> + if (*Environ.evaluable_constant cst env*) + cst=(Lazy.force id_not) || + cst=(Lazy.force id_iff) then + Some(EvalConstRef cst,t) + else None + | _-> None) + | _-> None + +type kind_of_formula= + Arrow of constr*constr + | And of inductive*constr list + | Or of inductive*constr list + | Exists of inductive*constr list + | Forall of constr*constr + | Atom of constr + | Evaluable of evaluable_global_reference*constr + | False + +let rec kind_of_formula gl term = let cciterm=whd_betaiotazeta term in match match_with_imp_term cciterm with Some (a,b)-> Arrow(a,(pop b)) @@ -113,13 +115,13 @@ let kind_of_formula term = match match_with_sigma_type cciterm with Some (i,l)-> Exists((destInd i),l) |_-> - match match_with_evaluable cciterm with - Some (cst,t)->Evaluable ((EvalConstRef cst),t) + match match_with_evaluable gl cciterm with + Some (ec,t)->Evaluable (ec,t) | None ->Atom cciterm let build_atoms gl metagen= let rec build_rec env polarity cciterm = - match kind_of_formula cciterm with + match kind_of_formula gl cciterm with False->[] | Arrow (a,b)-> (build_rec env (not polarity) a)@ @@ -144,7 +146,7 @@ let build_atoms gl metagen= [polarity,(substnl env 0 cciterm)] | Evaluable(ec,t)-> let nt=Tacred.unfoldn [[1],ec] (pf_env gl) (Refiner.sig_sig gl) t in - build_rec env polarity nt + build_rec env polarity nt in build_rec [] type right_pattern = @@ -174,7 +176,7 @@ type left_pattern= | Land of inductive | Lor of inductive | Lforall of metavariable*constr - | Lexists + | Lexists of inductive | Levaluable of evaluable_global_reference | LA of constr*left_arrow_pattern @@ -184,23 +186,19 @@ type left_formula={id:global_reference; atoms:(bool*constr) list; internal:bool} -exception Is_atom of constr - -let meta_succ m = m+1 - let build_left_entry nam typ internal gl metagen= try let pattern= - match kind_of_formula typ with + match kind_of_formula gl typ with False -> Lfalse | Atom a -> raise (Is_atom a) | And(i,_) -> Land i | Or(i,_) -> Lor i - | Exists (_,_) -> Lexists + | Exists (ind,_) -> Lexists ind | Forall (d,_) -> let m=meta_succ(metagen false) in Lforall(m,d) | Evaluable (egc,_) ->Levaluable egc | Arrow (a,b) ->LA (a, - match kind_of_formula a with + match kind_of_formula gl a with False-> LLfalse | Atom t-> LLatom | And(i,l)-> LLand(i,l) @@ -223,7 +221,7 @@ let build_left_entry nam typ internal gl metagen= let build_right_entry typ gl metagen= try let pattern= - match kind_of_formula typ with + match kind_of_formula gl typ with False -> raise (Is_atom typ) | Atom a -> raise (Is_atom a) | And(_,_) -> Rand diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli index c31eec2b2..c71c7fce2 100644 --- a/contrib/first-order/formula.mli +++ b/contrib/first-order/formula.mli @@ -22,25 +22,27 @@ val (==?) : ('a -> 'a -> 'b ->'b -> int) -> ('c -> 'c -> int) -> type ('a,'b) sum = Left of 'a | Right of 'b -val defined_connectives: (int list * evaluable_global_reference) list lazy_t - -type kind_of_formula= - Arrow of constr*constr - |And of inductive*constr list - |Or of inductive*constr list - |Exists of inductive*constr list - |Forall of constr*constr - |Atom of constr - |Evaluable of Names.evaluable_global_reference * Term.constr - |False - type counter = bool -> metavariable val construct_nhyps : inductive -> int array val ind_hyps : int -> inductive -> constr list -> Sign.rel_context array -val kind_of_formula : constr -> kind_of_formula +val match_with_evaluable : Proof_type.goal Tacmach.sigma -> + constr -> (evaluable_global_reference * constr) option + +type kind_of_formula= + Arrow of constr*constr + | And of inductive*constr list + | Or of inductive*constr list + | Exists of inductive*constr list + | Forall of constr*constr + | Atom of constr + | Evaluable of Names.evaluable_global_reference * Term.constr + | False + +val kind_of_formula : Proof_type.goal Tacmach.sigma -> + constr -> kind_of_formula val build_atoms : Proof_type.goal Tacmach.sigma -> counter -> bool -> constr -> (bool*constr) list @@ -72,7 +74,7 @@ type left_pattern= | Land of inductive | Lor of inductive | Lforall of metavariable*constr - | Lexists + | Lexists of inductive | Levaluable of Names.evaluable_global_reference | LA of constr*left_arrow_pattern diff --git a/contrib/first-order/ground.ml4 b/contrib/first-order/ground.ml4 index 054b28a07..ce2ba22ff 100644 --- a/contrib/first-order/ground.ml4 +++ b/contrib/first-order/ground.ml4 @@ -21,6 +21,8 @@ open Libnames open Util open Goptions +(* declaring search depth as a global option *) + let ground_depth=ref 5 let _= @@ -36,12 +38,6 @@ let _= in declare_int_option gdopt - -(* - 1- keep track of the instantiations and of ninst in the Sequent.t structure - 2- ordered instantiations -*) - let ground_tac solver startseq gl= let rec toptac seq gl= if Tacinterp.get_debug()=Tactic_debug.DebugOn @@ -108,9 +104,9 @@ let ground_tac solver startseq gl= else left_forall_tac lfp toptac (re_add seq)) (left_tac seq2 (lfp@ctx)) gl - | Lexists -> + | Lexists ind -> if !qflag then - left_exists_tac hd.id toptac (re_add seq1) gl + left_exists_tac ind hd.id toptac (re_add seq1) gl else (left_tac seq1 (hd::ctx)) gl | Levaluable egr-> left_evaluable_tac egr hd.id toptac (re_add seq1) gl diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml index 73b280d0a..1af4db1bc 100644 --- a/contrib/first-order/rules.ml +++ b/contrib/first-order/rules.ml @@ -29,19 +29,21 @@ type lseqtac= global_reference -> seqtac let wrap n b tacrec seq gls= check_for_interrupt (); let nc=pf_hyps gls in - let rec aux i nc= + 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)::q-> - let gr=VarRef id in - (add_left (gr,typ) (aux (i-1) q) true gls) in - let seq1= - if b then - (change_right (pf_concl gls) (aux n nc) gls) - else - (aux n nc) in - tacrec seq1 gls + | ((id,_,typ) as nd)::q-> + if occur_var env id (pf_concl gls) then + seq + else if List.exists (occur_var_in_decl env id) ctx then + seq + else + add_left (VarRef id,typ) (aux (i-1) q (nd::ctx)) true gls in + let seq1=aux n nc [] in + let seq2=if b then change_right (pf_concl gls) seq1 gls else seq1 in + tacrec seq2 gls let id_of_global=function VarRef id->id @@ -70,14 +72,6 @@ let left_evaluable_tac ec id tacrec seq gl= unfold_in_hyp [[1],ec] (Tacexpr.InHypType nid) gls); wrap 1 false tacrec seq] gl -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)) - let and_tac tacrec seq= tclTHEN simplest_split (wrap 0 true tacrec seq) @@ -104,7 +98,7 @@ let left_or_tac ind id tacrec seq= (Array.map f v) let forall_tac tacrec seq= - tclTHEN intro (wrap 1 true tacrec seq) + tclTHEN intro (wrap 0 true tacrec seq) let rec collect_forall seq= if is_empty_left seq then ([],seq) @@ -150,7 +144,6 @@ let left_forall_tac lfp tacrec seq gl= let arrow_tac tacrec seq= tclTHEN intro (wrap 1 true tacrec seq) - let dummy_exists_tac dom tacrec seq= tclTHENS (cut dom) [tclTHENLIST @@ -169,12 +162,13 @@ let exists_tac insts tacrec seq gl= tclFIRST (List.map (fun inst -> right_instance_tac inst tacrec seq) insts) gl -let left_exists_tac id tacrec seq= - tclTHENLIST - [simplest_elim (constr_of_reference id); - clear_global id; - tclDO 2 intro; - (wrap 1 false tacrec seq)] +let left_exists_tac ind id tacrec seq= + let n=(construct_nhyps ind).(0) in + tclTHENLIST + [simplest_elim (constr_of_reference id); + clear_global id; + tclDO n intro; + (wrap (n-1) false tacrec seq)] let ll_arrow_tac a b c id tacrec seq= let cc=mkProd(Anonymous,a,(lift 1 b)) in @@ -246,3 +240,17 @@ let ll_forall_tac prod id tacrec seq= intro; tclSOLVE [wrap 1 false tacrec (deepen seq)]]; tclSOLVE [wrap 0 true tacrec (deepen seq)]] + +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)) diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli index 91fdc8cf3..f47a40180 100644 --- a/contrib/first-order/rules.mli +++ b/contrib/first-order/rules.mli @@ -27,8 +27,6 @@ val evaluable_tac : evaluable_global_reference -> seqtac val left_evaluable_tac : evaluable_global_reference -> lseqtac -val normalize_evaluables : tactic - val and_tac : seqtac val left_and_tac : inductive -> lseqtac @@ -53,7 +51,7 @@ val right_instance_tac : constr * int -> seqtac val exists_tac : (constr * int) list -> seqtac -val left_exists_tac : lseqtac +val left_exists_tac : inductive -> lseqtac val ll_arrow_tac : constr -> constr -> constr -> lseqtac @@ -66,3 +64,5 @@ val left_false_tac : global_reference -> tactic val ll_ind_tac : inductive -> constr list -> lseqtac val ll_forall_tac : types -> lseqtac + +val normalize_evaluables : tactic diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml index 690feb874..bd24d38f5 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/first-order/sequent.ml @@ -25,7 +25,7 @@ let priority = function (* pure heuristics, <=0 for non reversible *) | Land _ -> 90 | Lor _ -> 40 | Lforall (_,_) -> -30 (* must stay at lowest priority *) - | Lexists -> 60 + | Lexists _ -> 60 | Levaluable _ -> 100 | LA(_,lap) -> match lap with |