diff options
| -rw-r--r-- | contrib/first-order/formula.ml | 109 | ||||
| -rw-r--r-- | contrib/first-order/formula.mli | 20 | ||||
| -rw-r--r-- | contrib/first-order/rules.ml | 4 | ||||
| -rw-r--r-- | contrib/first-order/sequent.ml | 40 | ||||
| -rw-r--r-- | contrib/first-order/sequent.mli | 2 | ||||
| -rw-r--r-- | contrib/first-order/unify.ml | 19 |
6 files changed, 98 insertions, 96 deletions
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml index 7901e0d40c..96f6930cad 100644 --- a/contrib/first-order/formula.ml +++ b/contrib/first-order/formula.ml @@ -126,11 +126,13 @@ let rec kind_of_formula gl term = 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 "") -let build_atoms gl metagen polarity cciterm = +let build_atoms gl metagen side cciterm = let trivial =ref false and positive=ref [] and negative=ref [] in @@ -170,12 +172,20 @@ let build_atoms gl metagen polarity cciterm = build_rec (var::env) polarity b | Atom t-> let unsigned=substnl env 0 t in - if polarity then - positive:= unsigned :: !positive - else - negative:= unsigned :: !negative - in - build_rec [] polarity cciterm; + 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 + end; (!trivial, {positive= !positive; negative= !negative}) @@ -219,51 +229,52 @@ let build_formula side nam typ gl metagen= build_atoms gl metagen side typ else no_atoms in let pattern= - if side then - 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).(0) in - Rexists(m,d,trivial) - | Forall (_,a) -> Rforall - | Arrow (a,b) -> Rarrow in - Right pat - else - 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 + 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).(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 index 35ae80f592..140358523f 100644 --- a/contrib/first-order/formula.mli +++ b/contrib/first-order/formula.mli @@ -30,25 +30,15 @@ val ind_hyps : int -> inductive -> constr list -> Sign.rel_context array val match_with_evaluable : Proof_type.goal Tacmach.sigma -> constr -> (evaluable_global_reference * constr) option -(* -type kind_of_formula = - Arrow of constr*constr - | False of inductive*constr list - | And of inductive*constr list - | Or of inductive*constr list - | Exists of inductive*constr list - | Forall of constr*constr - | Atom of constr - -val kind_of_formula : Proof_type.goal Tacmach.sigma -> - constr -> kind_of_formula -*) + 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 -> - bool -> constr -> bool * atoms + side -> constr -> bool * atoms type right_pattern = Rarrow @@ -82,6 +72,6 @@ type t={id: global_reference; (*exception Is_atom of constr*) -val build_formula : bool -> global_reference -> types -> +val build_formula : side -> global_reference -> types -> Proof_type.goal Tacmach.sigma -> counter -> (t,types) sum diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml index ad36bc4d70..bd69262906 100644 --- a/contrib/first-order/rules.ml +++ b/contrib/first-order/rules.ml @@ -39,10 +39,10 @@ let wrap n b continue seq gls= List.exists (occur_var_in_decl env id) ctx then (aux (i-1) q (nd::ctx)) else - add_formula false (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in + 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 true dummy_id (pf_concl gls) seq1 gls else seq1 in + add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in continue seq2 gls let id_of_global=function diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml index a91b4956c8..c30c109c27 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/first-order/sequent.ml @@ -189,23 +189,27 @@ let lookup item seq= let rec add_formula side nam t seq gl= match build_formula side nam t gl seq.cnt with Left f-> - if side then - {seq with - redexes=HP.add f seq.redexes; - gl=f.constr; - glatom=None} - else - {seq with - redexes=HP.add f seq.redexes; - context=cm_add f.constr nam seq.context} + 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-> - if side then - {seq with gl=t;glatom=Some t} - else - {seq with - context=cm_add t nam seq.context; - latoms=t::seq.latoms} - + 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 @@ -253,7 +257,7 @@ let create_with_ref_list l depth gl= let f gr seq= let c=constr_of_reference gr in let typ=(pf_type_of gl c) in - add_formula false gr typ seq gl in + add_formula Hyp gr typ seq gl in List.fold_right f l (empty_seq depth) open Auto @@ -267,7 +271,7 @@ let create_with_auto_hints l depth gl= (try let gr=reference_of_constr c in let typ=(pf_type_of gl c) in - seqref:=add_formula false gr typ !seqref gl + seqref:=add_formula Hint gr typ !seqref gl with Not_found->()) | _-> () in let g _ l=List.iter f l in diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli index b126bf638e..d6cc8a5a2f 100644 --- a/contrib/first-order/sequent.mli +++ b/contrib/first-order/sequent.mli @@ -46,7 +46,7 @@ val record: h_item -> t -> t val lookup: h_item -> t -> bool -val add_formula : bool -> global_reference -> constr -> t -> +val add_formula : side -> global_reference -> constr -> t -> Proof_type.goal sigma -> t val re_add_formula_list : Formula.t list -> t -> t diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml index ffe0070409..03d01f2dfd 100644 --- a/contrib/first-order/unify.ml +++ b/contrib/first-order/unify.ml @@ -88,8 +88,6 @@ let unif t1 t2= (* this place is unreachable but needed for the sake of typing *) with Queue.Empty-> !sigma -let is_head_meta t=match kind_of_term t with Meta _->true | _ ->false - let value i t= let add x y= if x<0 then y else if y<0 then x else x+y in @@ -123,14 +121,13 @@ let mk_rel_inst t= let nt=renum_rec 0 t in (!new_rel - 1,nt) let unif_atoms i dom t1 t2= - if is_head_meta t1 || is_head_meta t2 then None else - try - let t=List.assoc i (unif t1 t2) in - if is_head_meta t then Some (Phantom dom) - else Some (Real(mk_rel_inst t,value i t1)) - with - UFAIL(_,_) ->None - | Not_found ->Some (Phantom dom) + 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 @@ -141,6 +138,6 @@ let more_general (m1,t1) (m2,t2)= and mt2=renum_metas_from m1 m2 t2 in try let sigma=unif mt1 mt2 in - let p (n,t)= n<m1 || is_head_meta t in + let p (n,t)= n<m1 || isMeta t in List.for_all p sigma with UFAIL(_,_)->false |