diff options
Diffstat (limited to 'contrib/first-order')
-rw-r--r-- | contrib/first-order/formula.ml | 95 | ||||
-rw-r--r-- | contrib/first-order/formula.mli | 4 | ||||
-rw-r--r-- | contrib/first-order/g_ground.ml4 | 96 | ||||
-rw-r--r-- | contrib/first-order/ground.ml (renamed from contrib/first-order/ground.ml4) | 84 | ||||
-rw-r--r-- | contrib/first-order/ground.mli | 13 | ||||
-rw-r--r-- | contrib/first-order/instances.ml | 26 | ||||
-rw-r--r-- | contrib/first-order/rules.ml | 40 | ||||
-rw-r--r-- | contrib/first-order/rules.mli | 4 | ||||
-rw-r--r-- | contrib/first-order/sequent.ml | 3 |
9 files changed, 173 insertions, 192 deletions
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml index 3cf099773..bce1ef24e 100644 --- a/contrib/first-order/formula.ml +++ b/contrib/first-order/formula.ml @@ -63,25 +63,19 @@ let ind_hyps nevar ind largs= 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 + let hd= 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) + App (head,_) -> head + | _ -> t in + match kind_of_term hd with + Const cst-> + if Environ.evaluable_constant cst env + then Some (EvalConstRef cst,t) + else None | _-> None - + type kind_of_formula= Arrow of constr*constr | False of inductive*constr list @@ -90,7 +84,6 @@ type kind_of_formula= | Exists of inductive*constr list | Forall of constr*constr | Atom of constr - | Evaluable of evaluable_global_reference*constr let rec kind_of_formula gl term = let cciterm=whd_betaiotazeta term in @@ -116,8 +109,14 @@ let rec kind_of_formula gl term = Some (i,l)-> Exists((destInd i),l) |_-> match match_with_evaluable gl cciterm with - Some (ec,t)->Evaluable (ec,t) - | None ->Atom cciterm + Some (ec,t)-> + let nt=Tacred.unfoldn [[1],ec] + (pf_env gl) + (Refiner.sig_sig gl) t in + kind_of_formula gl nt + | None ->Atom (nf_betadeltaiota + (pf_env gl) + (Refiner.sig_sig gl) cciterm) type atoms = {positive:constr list;negative:constr list} @@ -161,10 +160,6 @@ let build_atoms gl metagen polarity cciterm = positive:= unsigned :: !positive else negative:= unsigned :: !negative - | Evaluable(ec,t)-> - let nt=Tacred.unfoldn [[1],ec] (Lazy.force pfenv) - (Refiner.sig_sig gl) t in - build_rec env polarity nt in build_rec [] polarity cciterm; (!trivial, @@ -179,7 +174,6 @@ type right_pattern = | Rfalse | Rforall | Rexists of metavariable*constr*bool - | Revaluable of evaluable_global_reference type left_arrow_pattern= LLatom @@ -189,7 +183,6 @@ type left_arrow_pattern= | LLforall of constr | LLexists of inductive*constr list | LLarrow of constr*constr*constr - | LLevaluable of evaluable_global_reference type left_pattern= Lfalse @@ -197,7 +190,6 @@ type left_pattern= | Lor of inductive | Lforall of metavariable*constr*bool | Lexists of inductive - | Levaluable of evaluable_global_reference | LA of constr*left_arrow_pattern type t={id:global_reference; @@ -224,8 +216,7 @@ let build_formula side nam typ gl metagen= let (_,_,d)=list_last (ind_hyps 0 i l).(0) in Rexists(m,d,trivial) | Forall (_,a) -> Rforall - | Arrow (a,b) -> Rarrow - | Evaluable (egc,_)->Revaluable egc in + | Arrow (a,b) -> Rarrow in Right pat else let pat= @@ -237,44 +228,22 @@ let build_formula side nam typ gl metagen= | Exists (ind,_) -> Lexists ind | Forall (d,_) -> Lforall(m,d,trivial) - | Evaluable (egc,_) ->Levaluable egc - | Arrow (a,b) ->LA (a, - 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 - | Evaluable (egc,_)-> LLevaluable egc) in + | Arrow (a,b) -> + let nfa=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) 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=typ; + constr=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) typ; pat=pattern; atoms=atoms} - with Is_atom a-> Right a -(* -let build_right_entry typ gl metagen= - try - let m=meta_succ(metagen false) in - let trivial,atoms= - if !qflag then - build_atoms gl metagen true typ - else no_atoms in - let pattern= - match kind_of_formula gl typ with - False(_,_) -> raise (Is_atom typ) - | Atom a -> raise (Is_atom a) - | And(_,_) -> Rand - | Or(_,_) -> Ror - | Exists (i,l) -> - let (_,_,d)=list_last (ind_hyps 0 i l).(0) in - Rexists(m,d,trivial) - | Forall (_,a) -> Rforall - | Arrow (a,b) -> Rarrow - | Evaluable (egc,_)->Revaluable egc in - Complex(pattern,typ,atoms) - with Is_atom a-> Atomic a -*) + with Is_atom a-> Right a (* already in nf *) + diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli index 815657f54..cbf3dc152 100644 --- a/contrib/first-order/formula.mli +++ b/contrib/first-order/formula.mli @@ -39,7 +39,6 @@ type kind_of_formula = | Exists of inductive*constr list | Forall of constr*constr | Atom of constr - | Evaluable of Names.evaluable_global_reference * Term.constr val kind_of_formula : Proof_type.goal Tacmach.sigma -> constr -> kind_of_formula @@ -58,7 +57,6 @@ type right_pattern = | Rfalse | Rforall | Rexists of metavariable*constr*bool - | Revaluable of Names.evaluable_global_reference type left_arrow_pattern= LLatom @@ -68,7 +66,6 @@ type left_arrow_pattern= | LLforall of constr | LLexists of inductive*constr list | LLarrow of constr*constr*constr - | LLevaluable of Names.evaluable_global_reference type left_pattern= Lfalse @@ -76,7 +73,6 @@ type left_pattern= | Lor of inductive | Lforall of metavariable*constr*bool | Lexists of inductive - | Levaluable of Names.evaluable_global_reference | LA of constr*left_arrow_pattern type t={id: global_reference; diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4 new file mode 100644 index 000000000..059ca69a6 --- /dev/null +++ b/contrib/first-order/g_ground.ml4 @@ -0,0 +1,96 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(* $Id$ *) + +open Formula +open Sequent +open Ground +open Goptions +open Tactics +open Tacticals +open Term +open Names + +(* declaring search depth as a global option *) + +let ground_depth=ref 5 + +let _= + let gdopt= + { optsync=false; + optname="ground_depth"; + optkey=SecondaryTable("Ground","Depth"); + optread=(fun ()->Some !ground_depth); + optwrite= + (function + None->ground_depth:=5 + | Some i->ground_depth:=(max i 0))} + in + declare_int_option gdopt + +let default_solver=(Tacinterp.interp <:tactic<Auto with *>>) + +let fail_solver=tclFAIL 0 "GTauto failed" + +let gen_ground_tac flag taco l gl= + let backup= !qflag in + try + qflag:=flag; + let solver= + match taco with + Some tac->tac + | None-> default_solver in + let startseq=create_with_ref_list 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 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) + (Tacexpr.InHypType id)) + +TACTIC EXTEND Ground + | [ "Ground" tactic(t) "with" ne_reference_list(l) ] -> + [ gen_ground_tac true (Some (snd t)) l ] + | [ "Ground" tactic(t) ] -> + [ gen_ground_tac true (Some (snd t)) [] ] + | [ "Ground" "with" ne_reference_list(l) ] -> + [ gen_ground_tac true None l ] + | [ "Ground" ] -> + [ gen_ground_tac true None [] ] +END + +TACTIC EXTEND GTauto + [ "GTauto" ] -> + [ gen_ground_tac false (Some fail_solver) [] ] +END + +TACTIC EXTEND GIntuition + ["GIntuition" tactic(t)] -> + [ gen_ground_tac false + (Some(tclTHEN normalize_evaluables (snd t))) [] ] +| [ "GIntuition" ] -> + [ gen_ground_tac false + (Some (tclTHEN normalize_evaluables default_solver)) [] ] +END + diff --git a/contrib/first-order/ground.ml4 b/contrib/first-order/ground.ml index 69f70d590..cc63b4afc 100644 --- a/contrib/first-order/ground.ml4 +++ b/contrib/first-order/ground.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) - (* $Id$ *) open Formula @@ -18,40 +16,18 @@ open Term open Tacmach open Tactics open Tacticals -open Libnames -open Util -open Goptions - -(* declaring search depth as a global option *) - -let ground_depth=ref 5 - -let set_qflag b= qflag:=b - -let _= - let gdopt= - { optsync=false; - optname="ground_depth"; - optkey=SecondaryTable("Ground","Depth"); - optread=(fun ()->Some !ground_depth); - optwrite= - (function - None->ground_depth:=5 - | Some i->ground_depth:=(max i 0))} - in - declare_int_option gdopt let ground_tac solver startseq gl= - let rec toptac ctx seq gl= + let rec toptac skipped seq gl= if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 then Pp.msgnl (Proof_trees.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 ctx s in + and re_add s=re_add_formula_list skipped s in let continue=toptac [] - and backtrack=toptac (hd::ctx) seq1 in + and backtrack=toptac (hd::skipped) seq1 in match hd.pat with Right rpat-> begin @@ -62,8 +38,6 @@ let ground_tac solver startseq gl= forall_tac continue (re_add seq1) | Rarrow-> arrow_tac continue (re_add seq1) - | Revaluable egr-> - evaluable_tac egr continue (re_add seq1) | Ror-> tclORELSE (or_tac continue (re_add seq1)) @@ -71,7 +45,7 @@ let ground_tac solver startseq gl= | Rfalse->backtrack | Rexists(i,dom,triv)-> let (lfp,seq2)=collect_quantified seq in - let backtrack2=toptac (lfp@ctx) seq2 in + let backtrack2=toptac (lfp@skipped) seq2 in tclORELSE (if seq.depth<=0 || not !qflag then tclFAIL 0 "max depth" @@ -90,7 +64,7 @@ let ground_tac solver startseq gl= left_or_tac ind hd.id continue (re_add seq1) | Lforall (_,_,_)-> let (lfp,seq2)=collect_quantified seq in - let backtrack2=toptac (lfp@ctx) seq2 in + let backtrack2=toptac (lfp@skipped) seq2 in tclORELSE (if seq.depth<=0 || not !qflag then tclFAIL 0 "max depth" @@ -101,8 +75,6 @@ let ground_tac solver startseq gl= if !qflag then left_exists_tac ind hd.id continue (re_add seq1) else backtrack - | Levaluable egr-> - left_evaluable_tac egr hd.id continue (re_add seq1) | LA (typ,lap)-> tclORELSE (ll_atom_tac typ hd.id continue (re_add seq1)) @@ -132,54 +104,8 @@ let ground_tac solver startseq gl= (ll_arrow_tac a b c hd.id continue (re_add seq1)) backtrack - | LLevaluable egr-> - left_evaluable_tac egr hd.id continue - (re_add seq1) end end with Heap.EmptyHeap->solver end gl in wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl - -let default_solver=(Tacinterp.interp <:tactic<Auto with *>>) - -let fail_solver=tclFAIL 0 "GroundTauto failed" - -let gen_ground_tac flag taco l gl= - let backup= !qflag in - try - set_qflag flag; - let solver= - match taco with - Some tac->tac - | None-> default_solver in - let startseq=create_with_ref_list l !ground_depth in - let result=ground_tac solver startseq gl in - set_qflag backup;result - with e -> set_qflag backup;raise e - -TACTIC EXTEND Ground - | [ "Ground" tactic(t) "with" ne_reference_list(l) ] -> - [ gen_ground_tac true (Some (snd t)) l ] - | [ "Ground" tactic(t) ] -> - [ gen_ground_tac true (Some (snd t)) [] ] - | [ "Ground" "with" ne_reference_list(l) ] -> - [ gen_ground_tac true None l ] - | [ "Ground" ] -> - [ gen_ground_tac true None [] ] -END - -TACTIC EXTEND GTauto - [ "GTauto" ] -> - [ gen_ground_tac false (Some fail_solver) [] ] -END - -TACTIC EXTEND GIntuition - ["GIntuition" tactic(t)] -> - [ gen_ground_tac false - (Some(tclTHEN normalize_evaluables (snd t))) [] ] -| [ "GIntuition" ] -> - [ gen_ground_tac false - (Some (tclTHEN normalize_evaluables default_solver)) [] ] -END - diff --git a/contrib/first-order/ground.mli b/contrib/first-order/ground.mli new file mode 100644 index 000000000..fff45816a --- /dev/null +++ b/contrib/first-order/ground.mli @@ -0,0 +1,13 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +val ground_tac: Tacmach.tactic -> + (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic + diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml index 41a4078cc..e75ee8fb8 100644 --- a/contrib/first-order/instances.ml +++ b/contrib/first-order/instances.ml @@ -115,41 +115,47 @@ let left_instance_tac (inst,id) tacrec seq= else tclTHENS (cut dom) [tclTHENLIST - [intro; + [introf; (fun gls->generalize [mkApp(constr_of_reference id, [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls); - intro; + introf; tclSOLVE [wrap 1 false tacrec (deepen (record (id,None) seq))]]; tclTRY assumption] - | Real((m,t) as c,_)-> - if lookup (id,Some c) seq || m>0 then + | Real((0,t) as c,_)-> + if lookup (id,Some c) seq then tclFAIL 0 "already done" else tclTHENLIST [generalize [mkApp(constr_of_reference id,[|t|])]; - intro; + introf; tclSOLVE [wrap 1 false tacrec (deepen (record (id,Some c) seq))]] + | Real((m,t) as c,_)-> + if lookup (id,Some c) seq then + tclFAIL 0 "already done" + else + tclFAIL 0 "not implemented ... yet" + let right_instance_tac inst tacrec seq= match inst with Phantom dom -> tclTHENS (cut dom) [tclTHENLIST - [intro; + [introf; (fun gls-> split (Rawterm.ImplicitBindings [mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls); tclSOLVE [wrap 0 false tacrec (deepen seq)]]; tclTRY assumption] + | Real ((0,t),_) -> + (tclTHEN (split (Rawterm.ImplicitBindings [t])) + (tclSOLVE [wrap 0 true tacrec (deepen seq)])) | Real ((m,t),_) -> - if m>0 then tclFAIL 0 "not implemented ... yes" - else - tclTHEN (split (Rawterm.ImplicitBindings [t])) - (tclSOLVE [wrap 0 true tacrec (deepen seq)]) + tclFAIL 0 "not implemented ... yet" let instance_tac inst= if (snd inst)==dummy_id then diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml index e7b71f54f..3ee0871de 100644 --- a/contrib/first-order/rules.ml +++ b/contrib/first-order/rules.ml @@ -15,7 +15,6 @@ open Tacmach open Tactics open Tacticals open Termops -open Reductionops open Declarations open Formula open Sequent @@ -65,27 +64,10 @@ let ll_atom_tac a id tacrec seq= [generalize [mkApp(constr_of_reference id, [|constr_of_reference (find_left a seq)|])]; clear_global id; - intro; + introf; wrap 1 false tacrec seq] with Not_found->tclFAIL 0 "No link" -(* evaluation rules *) - -let evaluable_tac ec tacrec seq gl= - tclTHEN - (unfold_in_concl [[1],ec]) - (wrap 0 true tacrec seq) gl - -let left_evaluable_tac ec id tacrec seq gl= - tclTHENLIST - [generalize [constr_of_reference id]; - clear_global id; - intro; - (fun gls-> - let nid=(Tacmach.pf_nth_hyp_id gls 1) in - unfold_in_hyp [[1],ec] (Tacexpr.InHypType nid) gls); - wrap 1 false tacrec seq] gl - (* right connectives rules *) let and_tac tacrec seq= @@ -95,7 +77,7 @@ let or_tac tacrec seq= any_constructor (Some (tclSOLVE [wrap 0 true tacrec seq])) let arrow_tac tacrec seq= - tclTHEN intro (wrap 1 true tacrec seq) + tclTHEN introf (wrap 1 true tacrec seq) (* left connectives rules *) @@ -104,7 +86,7 @@ let left_and_tac ind id tacrec seq= tclTHENLIST [simplest_elim (constr_of_reference id); clear_global id; - tclDO n intro; + tclDO n introf; wrap n false tacrec seq] let left_or_tac ind id tacrec seq= @@ -112,7 +94,7 @@ let left_or_tac ind id tacrec seq= let f n= tclTHENLIST [clear_global id; - tclDO n intro; + tclDO n introf; wrap n false tacrec seq] in tclTHENSV (simplest_elim (constr_of_reference id)) @@ -143,7 +125,7 @@ let ll_ind_tac ind largs id tacrec seq gl= tclTHENLIST [generalize newhyps; clear_global id; - tclDO lp intro; + tclDO lp introf; wrap lp false tacrec seq] with Invalid_argument _ ->tclFAIL 0 "") gl @@ -154,40 +136,40 @@ let ll_arrow_tac a b c id tacrec seq= [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in tclTHENS (cut c) [tclTHENLIST - [intro; + [introf; clear_global id; wrap 1 false tacrec seq]; tclTHENS (cut cc) [exact_no_check (constr_of_reference id); tclTHENLIST [generalize [d]; - intro; + introf; clear_global id; tclSOLVE [wrap 1 true tacrec seq]]]] (* quantifier rules (easy side) *) let forall_tac tacrec seq= - tclTHEN intro (wrap 0 true tacrec seq) + tclTHEN introf (wrap 0 true 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; + tclDO n introf; (wrap (n-1) false tacrec seq)] let ll_forall_tac prod id tacrec seq= tclTHENS (cut prod) [tclTHENLIST - [intro; + [introf; (fun gls-> let id0=pf_nth_hyp_id gls 1 in let term=mkApp((constr_of_reference id),[|mkVar(id0)|]) in tclTHEN (generalize [term]) (clear [id0]) gls); clear_global id; - intro; + introf; tclSOLVE [wrap 1 false tacrec (deepen seq)]]; tclSOLVE [wrap 0 true tacrec (deepen seq)]] diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli index 10ffe863d..afccfcd1b 100644 --- a/contrib/first-order/rules.mli +++ b/contrib/first-order/rules.mli @@ -27,10 +27,6 @@ val axiom_tac : constr -> Sequent.t -> tactic val ll_atom_tac : constr -> lseqtac -val evaluable_tac : evaluable_global_reference -> seqtac - -val left_evaluable_tac : evaluable_global_reference -> lseqtac - val and_tac : seqtac val or_tac : seqtac diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml index 4942503c6..4c18090b9 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/first-order/sequent.ml @@ -31,7 +31,6 @@ let priority = (* pure heuristics, <=0 for non reversible *) | Ror -> -15 | Rfalse -> -50 (* dead end for sure *) | Rforall -> 100 - | Revaluable _ -> 100 | Rexists (_,_,_) -> -30 end | Left lf -> @@ -41,7 +40,6 @@ let priority = (* pure heuristics, <=0 for non reversible *) | Lor _ -> 40 | Lforall (_,_,_) -> -30 (* must stay at lowest priority *) | Lexists _ -> 60 - | Levaluable _ -> 100 | LA(_,lap) -> match lap with LLatom -> 0 @@ -51,7 +49,6 @@ let priority = (* pure heuristics, <=0 for non reversible *) | LLforall _ -> -20 | LLexists (_,_) -> 50 | LLarrow (_,_,_) -> -10 - | LLevaluable _ -> 100 let left_reversible lpat=(priority lpat)>0 |