From 7d220f8b61649646692983872626d6a8042446a9 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 20 Mar 2009 01:22:58 +0000 Subject: Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/firstorder/formula.ml | 270 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 270 insertions(+) create mode 100644 plugins/firstorder/formula.ml (limited to 'plugins/firstorder/formula.ml') diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml new file mode 100644 index 000000000..0be3a4b39 --- /dev/null +++ b/plugins/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 (decompose_prod_n_assum nevar t1) in + fst (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 *) + -- cgit v1.2.3