From: Enrico Tassi Date: Thu, 9 Apr 2009 15:05:29 +0000 (+0000) Subject: - change implemented in 4 lines X-Git-Tag: make_still_working~4096 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=174d3dbd5779c2ad602f905d7f4321dc68a53786;p=helm.git - change implemented in 4 lines - select0 runs on hypothesis - relocate honors conversion (but clearbody is not implemented) --- diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 545e5603b..86487e20d 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -45,24 +45,41 @@ let ctx_of (_,c,_) = c ;; let relocate status destination (name,source,t as orig) = if source == destination then status, orig else - let rec lcp j i = function - | (n1, t1)::cl1, (n2, t2)::cl2 -> - if n1 = n2 && t1 = t2 then - NCic.Rel i :: lcp (j-1) (i-1) (cl1,cl2) + let u, d, metasenv, subst, o = status.pstatus in + let rec lcp ctx j i = function + | (n1, NCic.Decl t1 as e)::cl1, (n2, NCic.Decl t2)::cl2 -> + if n1 = n2 && + NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then + NCic.Rel i :: lcp (e::ctx)(j-1) (i-1) (cl1,cl2) else HExtlib.mk_list (NCic.Appl [NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) j + | (n1, NCic.Def (b1,t1) as e)::cl1, (n2, NCic.Def (b2,t2))::cl2 -> + if n1 = n2 && + NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 && + NCicReduction.are_convertible ctx ~subst ~metasenv b1 b2 then + NCic.Rel i :: lcp (e::ctx)(j-1) (i-1) (cl1,cl2) + else + HExtlib.mk_list (NCic.Appl + [NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) j + | (n1, NCic.Def (b1,t1) as e)::cl1, (n2, NCic.Decl t2)::cl2 -> + if n1 = n2 && + NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then + NCic.Rel i :: lcp (e::ctx)(j-1) (i-1) (cl1,cl2) + else + HExtlib.mk_list (NCic.Appl + [NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) j + | (n1, NCic.Decl _)::cl1, (n2, NCic.Def _)::cl2 -> assert false | _::_, [] -> HExtlib.mk_list (NCic.Appl [NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) j | _ -> [] in let lc = - lcp (List.length destination) (List.length source) + lcp [] (List.length destination) (List.length source) (List.rev destination, List.rev source) in let lc = (0,NCic.Ctx (List.rev lc)) in - let u, d, metasenv, subst, o = status.pstatus in let db = NCicUnifHint.db () in (* XXX fixme *) let (metasenv, subst), t = NCicMetaSubst.delift @@ -82,10 +99,7 @@ let term_of_cic_term s t c = s, t ;; -type ast_term = string * int * CicNotationPt.term - -let disambiguate (status : lowtac_status) (t : ast_term) - (ty : cic_term option) context = +let disambiguate status t ty context = let status, expty = match ty with | None -> status, None diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index 3963f2500..81436f53d 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -37,9 +37,8 @@ val term_of_cic_term : lowtac_status -> cic_term -> NCic.context -> lowtac_status * NCic.term val mk_cic_term : NCic.context -> NCic.term -> cic_term -type ast_term = string * int * CicNotationPt.term val disambiguate: - lowtac_status -> ast_term -> cic_term option -> NCic.context -> + lowtac_status -> tactic_term -> cic_term option -> NCic.context -> lowtac_status * cic_term (* * cic_term XXX *) val analyse_indty: @@ -69,7 +68,7 @@ val select_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 -> + cic_term -> tactic_term option * NCic.term -> lowtac_status * cic_term val mk_in_scope: lowtac_status -> cic_term -> lowtac_status * cic_term diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index e1fed4deb..a6828df11 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -262,11 +262,12 @@ let generalize0_tac args = else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args)) ;; -let select0_tac ~where:(wanted,_,where) ~job = +let select0_tac ~where:(wanted,hyps,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 + | `ChangeWith f -> f,(fun s t -> s, t) in distribute_tac (fun status goal -> let goalty = get_goalty status goal in @@ -276,8 +277,30 @@ let select0_tac ~where:(wanted,_,where) ~job = let status, newgoalty = select_term status ~found ~postprocess goalty (wanted,path) in + let status, newgoalctx = + List.fold_right + (fun (name,d as entry) (status,ctx) -> + try + let path = List.assoc name hyps in + match d with + NCic.Decl ty -> + let status,ty = + select_term status ~found ~postprocess (mk_cic_term ctx ty) + (wanted,path) in + let status,ty = term_of_cic_term status ty ctx in + status,(name,NCic.Decl ty)::ctx + | NCic.Def (bo,ty) -> + let status,bo = + select_term status ~found ~postprocess (mk_cic_term ctx bo) + (wanted,path) in + let status,bo = term_of_cic_term status bo ctx in + status,(name,NCic.Def (bo,ty))::ctx + with + Not_found -> status, entry::ctx + ) (ctx_of goalty) (status,[]) + in let status, instance = - mk_meta status (ctx_of newgoalty) (`Decl newgoalty) + mk_meta status newgoalctx (`Decl newgoalty) in instantiate status goal instance) ;; @@ -319,55 +342,15 @@ let generalize_tac ~where = ) s) ] ;; - -let reopen status = - let n,h,metasenv,subst,o = status.pstatus in - let subst, newm = - List.partition - (function (_,(Some tag,_,_,_)) -> - tag <> NCicMetaSubst.in_scope_tag && - not (NCicMetaSubst.is_out_scope_tag tag) - | _ -> true) - subst - in - let in_m, out_m = - List.partition - (function (_,(Some tag,_,_,_)) -> - tag = NCicMetaSubst.in_scope_tag | _ -> assert false) - newm - in - let metasenv = List.map (fun (i,(_,c,_,t)) -> i,(None,c,t)) in_m @ metasenv in - let in_m = List.map fst in_m in - let out_m = match out_m with [i] -> i | _ -> assert false in - { status with pstatus = n,h,metasenv,subst,o }, in_m, out_m -;; - -let change ~where ~with_what status goal = -assert false; (* - let goalty = get_goalty status goal in - let (wanted,_,where) = GrafiteDisambiguate.disambiguate_npattern where in - let path = - match where with None -> NCic.Implicit `Term | Some where -> where - 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 - - let j,(n,cctx,bo,_) = out_scope in - let _ = typeof status (ctx_of goalty) (Obj.magic (n,cctx,bo)) in - - let n,h,metasenv,subst,o = status.pstatus in - let subst = out_scope :: subst in - let status = { status with pstatus = n,h,metasenv,subst,o } in - - let status, instance = - mk_meta status (ctx_of newgoalty) (`Decl newgoalty) - in - instantiate status goal instance -*) +let change_tac ~where ~with_what = + let change status t = + let status, ww = disambiguate status with_what None (ctx_of t) in + let status = unify status (ctx_of t) t ww in + status, ww + in + let where = GrafiteDisambiguate.disambiguate_npattern where in + select0_tac ~where ~job:(`ChangeWith change) ;; -let change_tac ~where ~with_what = distribute_tac (change ~where ~with_what) ;; let apply_tac = exact_tac;;