aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/first-order/formula.ml106
-rw-r--r--contrib/first-order/formula.mli30
-rw-r--r--contrib/first-order/ground.ml412
-rw-r--r--contrib/first-order/rules.ml60
-rw-r--r--contrib/first-order/rules.mli6
-rw-r--r--contrib/first-order/sequent.ml2
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 08:39:03 +0000