X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=e55df286b87b5a0d6f069bb4f7de9228cc3f00e4;hb=145583de619b9d2fcc4abe3f4d68d01538f9f394;hp=4d7b8ce4e9d8494da2fcf79cae1f383929beb289;hpb=a14adba81c00c9dcb9996d7af39e4803214606f1;p=helm.git diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 4d7b8ce4e..e55df286b 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -530,74 +530,67 @@ let record_index_obj = end ;; -let compute_keys uri height kind = - let mk_item orig_ty spec = - let ty,_,_ = NCicMetaSubst.saturate ~delta:max_int [] [] [] orig_ty 0 in - let keys = - match ty with - | NCic.Const (NReference.Ref (_,NReference.Def h)) - | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Def h))::_) - when h > 0 -> - let ty',_,_= - NCicMetaSubst.saturate ~delta:(h-1) [] [] [] orig_ty 0 in - [ty;ty'] - | _ -> [ty] - in - keys,NCic.Const(NReference.reference_of_spec uri spec) - in - let data = - match kind with - | NCic.Fixpoint (ind,ifl,_) -> - HExtlib.list_mapi - (fun (_,_,rno,ty,_) i -> - if ind then mk_item ty (NReference.Fix (i,rno,height)) - else mk_item ty (NReference.CoFix height)) ifl - | NCic.Inductive (b,lno,itl,_) -> - HExtlib.list_mapi - (fun (_,_,ty,_) i -> mk_item ty (NReference.Ind (b,i,lno))) itl - @ - List.map - (fun ((_,_,ty),i,j) -> - mk_item ty (NReference.Con (i,j+1,lno))) - (List.flatten - (HExtlib.list_mapi - (fun (_,_,_,cl) i -> HExtlib.list_mapi (fun x j-> x,i,j) cl) - itl)) - | NCic.Constant (_,_,Some _, ty, _) -> - [ mk_item ty (NReference.Def height) ] - | NCic.Constant (_,_,None, ty, _) -> - [ mk_item ty NReference.Decl ] - in - let data = HExtlib.filter_map - (fun (keys, t) -> - let keys = List.filter - (function - | (NCic.Meta _) - | (NCic.Appl (NCic.Meta _::_)) -> false - | _ -> true) - keys - in - if keys <> [] then - begin - HLog.debug ("Indexing:" ^ - NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t); - HLog.debug ("With keys:" ^ String.concat "\n" (List.map (fun t -> - NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t) keys)); - Some (keys,t) - end - else - begin - HLog.debug ("Not indexing:" ^ - NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t); - None - end) +let compute_keys status uri height kind = + let mk_item ty spec = + let orig_ty = NTacStatus.mk_cic_term [] ty in + let status,keys = NnAuto.keys_of_type status orig_ty in + let keys = + List.map + (fun t -> + snd (NTacStatus.term_of_cic_term status t (NTacStatus.ctx_of t))) + keys + in + keys,NCic.Const(NReference.reference_of_spec uri spec) + in + let data = + match kind with + | NCic.Fixpoint (ind,ifl,_) -> + HExtlib.list_mapi + (fun (_,_,rno,ty,_) i -> + if ind then mk_item ty (NReference.Fix (i,rno,height)) + else mk_item ty (NReference.CoFix height)) ifl + | NCic.Inductive (b,lno,itl,_) -> + HExtlib.list_mapi + (fun (_,_,ty,_) i -> mk_item ty (NReference.Ind (b,i,lno))) itl + @ + List.map (fun ((_,_,ty),i,j) -> mk_item ty (NReference.Con (i,j+1,lno))) + (List.flatten (HExtlib.list_mapi + (fun (_,_,_,cl) i -> HExtlib.list_mapi (fun x j-> x,i,j) cl) + itl)) + | NCic.Constant (_,_,Some _, ty, _) -> + [ mk_item ty (NReference.Def height) ] + | NCic.Constant (_,_,None, ty, _) -> + [ mk_item ty NReference.Decl ] + in + HExtlib.filter_map + (fun (keys, t) -> + let keys = List.filter + (function + | (NCic.Meta _) + | (NCic.Appl (NCic.Meta _::_)) -> false + | _ -> true) + keys + in + if keys <> [] then + begin + HLog.debug ("Indexing:" ^ + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t); + HLog.debug ("With keys:" ^ String.concat "\n" (List.map (fun t -> + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t) keys)); + Some (keys,t) + end + else + begin + HLog.debug ("Not indexing:" ^ + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t); + None + end) data - in data ;; let index_obj_for_auto status (uri, height, _, _, kind) = (*prerr_endline (string_of_int height);*) - let data = compute_keys uri height kind in + let data = compute_keys status uri height kind in let status = basic_index_obj data status in let dump = record_index_obj data :: status#dump in status#set_dump dump @@ -784,10 +777,11 @@ let eval_ng_tac tac = ) hyps, (text,prefix_len,concl)) ) seqs) - | GrafiteAst.NAuto (_loc, (None,a)) -> NAuto.auto_tac ~params:(None,a) + | GrafiteAst.NAuto (_loc, (None,a)) -> + NAuto.auto_tac ~params:(None,a) ?trace_ref:None | GrafiteAst.NAuto (_loc, (Some l,a)) -> NAuto.auto_tac - ~params:(Some List.map (fun x -> "",0,x) l,a) + ~params:(Some List.map (fun x -> "",0,x) l,a) ?trace_ref:None | GrafiteAst.NBranch _ -> NTactics.branch_tac ~force:false | GrafiteAst.NCases (_loc, what, where) -> NTactics.cases_tac @@ -814,6 +808,7 @@ let eval_ng_tac tac = NTactics.generalize_tac ~where:(text,prefix_len,where) | GrafiteAst.NId _ -> (fun x -> x) | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n + | GrafiteAst.NIntros (_loc,ns) -> NTactics.intros_tac ns | GrafiteAst.NInversion (_loc, what, where) -> NTactics.inversion_tac ~what:(text,prefix_len,what) @@ -940,35 +935,36 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = in if nstatus#ng_mode <> `CommandMode then begin - HLog.error "error in generating projection/eliminator"; - prerr_endline (NCicPp.ppobj nstatus#obj); - nstatus, uris + (*HLog.warn "error in generating projection/eliminator";*) + status, uris end else nstatus, concat_nuris uris nuris with - | MultiPassDisambiguator.DisambiguationError _ + | MultiPassDisambiguator.DisambiguationError _ | NCicTypeChecker.TypeCheckerFailure _ -> - HLog.warn "error in generating projection/eliminator"; + (*HLog.warn "error in generating projection/eliminator";*) status,uris ) (status,`New [] (* uris *)) boxml in let _,_,_,_,nobj = obj in let status = match nobj with - NCic.Inductive (true,leftno,[it],_) -> + NCic.Inductive (is_ind,leftno,[it],_) -> let _,ind_name,ty,cl = it in List.fold_left (fun status outsort -> let status = status#set_ng_mode `ProofMode in try - (let status,invobj = NInversion.mk_inverter - (ind_name ^ "_inv_" ^ (snd (NCicElim.ast_of_sort outsort))) - it leftno outsort status status#baseuri in + (let status,invobj = + NInversion.mk_inverter + (ind_name ^ "_inv_" ^ + (snd (NCicElim.ast_of_sort outsort))) + is_ind it leftno outsort status status#baseuri in let _,_,menv,_,_ = invobj in fst (match menv with [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) | _ -> status,`New [])) (* XXX *) - with _ -> HLog.warn "error in generating inversion principle"; + with _ -> (*HLog.warn "error in generating inversion principle"; *) let status = status#set_ng_mode `CommandMode in status) status (NCic.Prop:: @@ -1099,7 +1095,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = indtyno, NCicEnvironment.get_checked_indtys r | _ -> prerr_endline ("engine: indty =" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] indty) ; assert false in let it = List.nth tys indtyno in - let status,obj = NInversion.mk_inverter name it leftno ?selection sort + let status,obj = NInversion.mk_inverter name true it leftno ?selection sort status status#baseuri in let _,_,menv,_,_ = obj in (match menv with