1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273
(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) 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 t1=Termops.prod_applist sigma 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:global_reference; 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 *)