From: Enrico Tassi Date: Wed, 8 Apr 2009 14:18:33 +0000 (+0000) Subject: generalized is half-implemented (still broken) X-Git-Tag: make_still_working~4105 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b438322c4140e3d2395d693e9c5f0e96934436a0;p=helm.git generalized is half-implemented (still broken) --- diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index a83023140..b69ff18f4 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -58,6 +58,7 @@ type ntactic = | NId of loc | NIntro of loc * string | NRewrite of loc * direction * CicNotationPt.term * npattern + | NGeneralize of loc * npattern type ('term, 'lazy_term, 'reduction, 'ident) tactic = (* Higher order tactics (i.e. tacticals) *) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index a41415fe7..7be93328e 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -598,6 +598,8 @@ let eval_ng_tac (text, prefix_len, tac) = NTactics.elim_tac ~what:(text,prefix_len,what) ~where:(text,prefix_len,where) + | GrafiteAst.NGeneralize (_loc, where) -> + NTactics.generalize_tac ~where:(text,prefix_len,where) | GrafiteAst.NId _ -> (fun x -> x) | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n | GrafiteAst.NRewrite (_loc,dir,what,where) -> diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 2316c04ca..5fc3a7fad 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -188,6 +188,8 @@ EXTEND GrafiteAst.NChange (loc, what, with_what) | IDENT "nelim"; what = tactic_term ; where = pattern_spec -> GrafiteAst.NElim (loc, what, where) + | IDENT "ngeneralize"; p=pattern_spec -> + GrafiteAst.NGeneralize (loc, p) | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec -> GrafiteAst.NRewrite (loc, dir, what, where) | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n) diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 9fc008efa..4bc751f3a 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -162,15 +162,28 @@ let mk_meta status ?name ctx bo_or_ty = status, (None,ctx,instance) ;; +let mk_in_scope status t = + mk_meta status ~name:NCicMetaSubst.in_scope_tag (ctx_of t) (`Def t) +;; + +let mk_out_scope n status t = + mk_meta status ~name:(NCicMetaSubst.out_scope_tag n) (ctx_of t) (`Def t) +;; + (* the following unification problem will be driven by - * select s argsno t pattern + * select s ~found:mk_in_scope ~postprocess:(mk_out_scope argsno) t pattern * * ? args = t * * where argsn = length args and the pattern matches t + * + * found is called on every selected term to map them + * postprocess is called on the entire term after selection *) -let select_term low_status argsno (name,context,term) (wanted,path) = - let found status ctx t wanted = +let select_term + low_status ~found ~postprocess (name,context,term) (wanted,path) += + let is_found status ctx t wanted = (* we could lift wanted step-by-step *) try true, unify status ctx (None, ctx, t) wanted with @@ -179,14 +192,19 @@ let select_term low_status argsno (name,context,term) (wanted,path) = in let match_term status ctx (wanted : cic_term) t = let rec aux ctx status t = - let b, status = found status ctx t wanted in - if b then - let status, (_,_,t) = - mk_meta status ~name:NCicMetaSubst.in_scope_tag - ctx (`Def (None, ctx, t)) - in - status, t - else NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t + let b, status = is_found status ctx t wanted in + if b then + let status , (_,_,t) = found status (None, ctx, t) in + status, t + else + let _,_,_,subst,_ = status.pstatus in + match t with + | NCic.Meta (i,lc) when List.mem_assoc i subst -> + let _,_,t,_ = NCicUtils.lookup_subst i subst in + aux ctx status t + | NCic.Meta _ -> status, t + | _ -> + NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t in aux ctx status t in @@ -249,7 +267,7 @@ let select_term low_status argsno (name,context,term) (wanted,path) = in let status, term = select low_status context path term in let term = (name, context, term) in - mk_meta status ~name:(NCicMetaSubst.out_scope_tag argsno) context (`Def term) + postprocess status term ;; let analyse_indty status ty = diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index 2a065bc5f..df862f223 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -61,9 +61,15 @@ val mk_meta: val instantiate: lowtac_status -> int -> cic_term -> lowtac_status val select_term: - lowtac_status -> int -> cic_term -> ast_term option * NCic.term -> + lowtac_status -> + found: (lowtac_status -> cic_term -> lowtac_status * cic_term) -> + postprocess: (lowtac_status -> cic_term -> lowtac_status * cic_term) -> + cic_term -> ast_term option * NCic.term -> lowtac_status * cic_term +val mk_in_scope: lowtac_status -> cic_term -> lowtac_status * cic_term +val mk_out_scope: int -> lowtac_status -> cic_term -> lowtac_status * cic_term + val pp_tac_status: tac_status -> unit (* end *) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index b34a3a34d..b64ef34f2 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -257,6 +257,8 @@ let clear names status goal = { status with pstatus = n,h,metasenv,subst,o } ;; +let force f s = Lazy.force f s;; + let clear_tac names = if names = [] then id_tac else distribute_tac (clear names) ;; @@ -266,25 +268,32 @@ let generalize0_tac args = else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args)) ;; -let select0_tac ~where:(wanted,_,where) ~argsno = +let select0_tac ~where:(wanted,_,where) ~job = + let found, postprocess = + match job with + | `Substexpand argsno -> mk_in_scope, mk_out_scope argsno + | `Collect l -> (fun s t -> l := t::!l; mk_in_scope s t), mk_out_scope 1 + in distribute_tac (fun status goal -> let goalty = get_goalty status goal in let path = match where with None -> NCic.Implicit `Term | Some where -> where in - let status, newgoalty = select_term status argsno goalty (wanted,path) in + let status, newgoalty = + select_term status ~found ~postprocess goalty (wanted,path) + in let status, instance = mk_meta status (ctx_of newgoalty) (`Decl newgoalty) in instantiate status goal instance) ;; -let select_tac ~where ~argsno move_down_hyps = +let select_tac ~where ~job move_down_hyps = let (wanted,hyps,where) = GrafiteDisambiguate.disambiguate_npattern where in let path = match where with None -> NCic.Implicit `Term | Some where -> where in if not move_down_hyps then - select0_tac ~where:(wanted,hyps,Some path) ~argsno + select0_tac ~where:(wanted,hyps,Some path) ~job else let path = List.fold_left @@ -293,15 +302,22 @@ let select_tac ~where ~argsno move_down_hyps = in block_tac [ generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps); - select0_tac ~where:(wanted,[],Some path) ~argsno; + select0_tac ~where:(wanted,[],Some path) ~job; clear_tac (List.map fst hyps) ] ;; -(* let generalize_tac ~where = - block_tac [ select_tac ~where true ; generalize0_tac ???? ] + let l = ref [] in + block_tac [ + select_tac ~where ~job:(`Collect l) true; + force (lazy (distribute_tac (fun status goal -> + let goalty = get_goalty status goal in + (* unift (ctx_of goal) t s *) + instantiate status goal + (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; + term_of_cic_term (List.hd !l) (ctx_of goalty) ])) + ))) ] ;; -*) let reopen status = @@ -332,7 +348,8 @@ let change ~where ~with_what status goal = let path = match where with None -> NCic.Implicit `Term | Some where -> where in - let status, newgoalty = select_term status 1 goalty (wanted,path) in + let status, newgoalty = assert false (* + select_term status 1 goalty (wanted,path)*) in let status, in_scope, out_scope = reopen status in let status = List.fold_left (exact with_what) status in_scope in @@ -379,8 +396,6 @@ let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal -> exec id_tac status goal) ;; -let force f s = Lazy.force f s;; - let elim_tac ~what ~where = let indtyinfo = ref None in let sort = ref None in @@ -394,7 +409,7 @@ let elim_tac ~what ~where = atomic_tac (block_tac [ analyze_indty_tac ~what indtyinfo; force (lazy (select_tac - ~where ~argsno:((HExtlib.unopt !indtyinfo).rightno+1) true)); + ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true)); print_tac "CIAO"; compute_goal_sort_tac; print_tac "CIAO2"; @@ -422,7 +437,7 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where = match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq_ind" in block_tac - [ select_tac ~where ~argsno:2 true; + [ select_tac ~where ~job:(`Substexpand 2) true; exact_tac ("",0, Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @ @@ -456,7 +471,8 @@ let cases_tac ~what ~where = atomic_tac (block_tac [ analyze_indty_tac ~what indtyinfo; - select_tac ~where ~argsno:((HExtlib.unopt !indtyinfo).rightno+1) true; + force (lazy (select_tac + ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true)); distribute_tac (cases ~what) ]) ;; diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index 0b805d22b..cc79e05b9 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -40,3 +40,4 @@ val rewrite_tac: dir:[ `LeftToRight | `RightToLeft ] -> what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> NTacStatus.tactic +val generalize_tac : where:NTacStatus.tactic_pattern -> NTacStatus.tactic