diff options
Diffstat (limited to 'plugins/firstorder/formula.ml')
| -rw-r--r-- | plugins/firstorder/formula.ml | 276 |
1 files changed, 276 insertions, 0 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml new file mode 100644 index 0000000000..a60a966cec --- /dev/null +++ b/plugins/firstorder/formula.ml @@ -0,0 +1,276 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Hipattern +open Names +open Constr +open EConstr +open Vars +open Termops +open Util +open Declarations +open Globnames + +module RelDecl = Context.Rel.Declaration + +let qflag=ref true + +let red_flags=ref CClosure.betaiotazeta + +let (=?) f g i1 i2 j1 j2= + let c=f i1 i2 in + if Int.equal c 0 then g j1 j2 else c + +let (==?) fg h i1 i2 j1 j2 k1 k2= + let c=fg i1 i2 j1 j2 in + if Int.equal c 0 then h k1 k2 else c + +type ('a,'b) sum = Left of 'a | Right of 'b + +type counter = bool -> metavariable + +exception Is_atom of constr + +let meta_succ m = m+1 + +let rec nb_prod_after n c= + match Constr.kind 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 env ind = + let nparams = (fst (Global.lookup_inductive (fst ind))).mind_nparams in + let constr_types = Inductiveops.arities_of_constructors env 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 env sigma nevar ind largs = + let types= Inductiveops.arities_of_constructors env ind in + let myhyps t = + let t = EConstr.of_constr t in + let nparam_decls = Context.Rel.length (fst (Global.lookup_inductive (fst ind))).mind_params_ctxt in + let t1=Termops.prod_applist_assum sigma nparam_decls t largs in + let t2=snd (decompose_prod_n_assum sigma nevar t1) in + fst (decompose_prod_assum sigma t2) in + Array.map myhyps types + +let special_nf env sigma t = + Reductionops.clos_norm_flags !red_flags env sigma t + +let special_whd env sigma t = + Reductionops.clos_whd_flags !red_flags env sigma t + +type kind_of_formula= + Arrow of constr*constr + | False of pinductive*constr list + | And of pinductive*constr list*bool + | Or of pinductive*constr list*bool + | Exists of pinductive*constr list + | Forall of constr*constr + | Atom of constr + +let pop t = Vars.lift (-1) t + +let kind_of_formula env sigma term = + let normalize = special_nf env sigma in + let cciterm = special_whd env sigma term in + match match_with_imp_term sigma cciterm with + Some (a,b)-> Arrow (a, pop b) + |_-> + match match_with_forall_term sigma cciterm with + Some (_,a,b)-> Forall (a, b) + |_-> + match match_with_nodep_ind sigma cciterm with + Some (i,l,n)-> + let ind,u=EConstr.destInd sigma i in + let u = EConstr.EInstance.kind sigma u in + let (mib,mip) = Global.lookup_inductive ind in + let nconstr=Array.length mip.mind_consnames in + if Int.equal nconstr 0 then + False((ind,u),l) + else + let has_realargs=(n>0) in + let is_trivial= + let is_constant c = + Int.equal (nb_prod sigma (EConstr.of_constr 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 Int.equal nconstr 1 then + And((ind,u),l,is_trivial) + else + Or((ind,u),l,is_trivial) + | _ -> + match match_with_sigma_type sigma cciterm with + Some (i,l)-> + let (ind, u) = EConstr.destInd sigma i in + let u = EConstr.EInstance.kind sigma u in + Exists((ind, u), 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 env sigma metagen side cciterm = + let trivial =ref false + and positive=ref [] + and negative=ref [] in + let normalize=special_nf env sigma in + let rec build_rec subst polarity cciterm= + match kind_of_formula env sigma cciterm with + False(_,_)->if not polarity then trivial:=true + | Arrow (a,b)-> + build_rec subst (not polarity) a; + build_rec subst polarity b + | And(i,l,b) | Or(i,l,b)-> + if b then + begin + let unsigned=normalize (substnl subst 0 cciterm) in + if polarity then + positive:= unsigned :: !positive + else + negative:= unsigned :: !negative + end; + let v = ind_hyps env sigma 0 i l in + let g i _ decl = + build_rec subst polarity (lift i (RelDecl.get_type decl)) 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 env sigma 1 i l).(0) in + let g i _ decl = + build_rec (var::subst) polarity (lift i (RelDecl.get_type decl)) in + List.fold_left_i g (2-(List.length l)) () v + | Forall(_,b)-> + let var=mkMeta (metagen true) in + build_rec (var::subst) polarity b + | Atom t-> + let unsigned=substnl subst 0 t in + if not (isMeta sigma 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 sigma cciterm in + let subst=List.rev_map (fun _->mkMeta (metagen true)) rels in + build_rec subst 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 pinductive*constr list + | LLand of pinductive*constr list + | LLor of pinductive*constr list + | LLforall of constr + | LLexists of pinductive*constr list + | LLarrow of constr*constr*constr + +type left_pattern= + Lfalse + | Land of pinductive + | Lor of pinductive + | Lforall of metavariable*constr*bool + | Lexists of pinductive + | LA of constr*left_arrow_pattern + +type t={id:GlobRef.t; + constr:constr; + pat:(left_pattern,right_pattern) sum; + atoms:atoms} + +let build_formula env sigma side nam typ metagen= + let normalize = special_nf env sigma in + try + let m=meta_succ(metagen false) in + let trivial,atoms= + if !qflag then + build_atoms env sigma metagen side typ + else no_atoms in + let pattern= + match side with + Concl -> + let pat= + match kind_of_formula env sigma typ with + False(_,_) -> Rfalse + | Atom a -> raise (Is_atom a) + | And(_,_,_) -> Rand + | Or(_,_,_) -> Ror + | Exists (i,l) -> + let d = RelDecl.get_type (List.last (ind_hyps env sigma 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 env sigma 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 env sigma 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 *) + |