X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=a0d8eba48a6b555718c45625968ccc6ddc451666;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=a6828df113d2afa33623a74306b3c5a7297d6596;hpb=174d3dbd5779c2ad602f905d7f4321dc68a53786;p=helm.git diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index a6828df11..a0d8eba48 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -274,9 +274,6 @@ let select0_tac ~where:(wanted,hyps,where) ~job = let path = match where with None -> NCic.Implicit `Term | Some where -> where in - 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) -> @@ -299,6 +296,16 @@ let select0_tac ~where:(wanted,hyps,where) ~job = Not_found -> status, entry::ctx ) (ctx_of goalty) (status,[]) in + let status, newgoalty = + select_term status ~found ~postprocess goalty (wanted,path) in + (* WARNING: the next two lines simply change the context of newgoalty + from the old to the new one. Otherwise mk_meta will do that herself, + calling relocate that calls delift. However, newgoalty is now + ?[out_scope] and thus the delift would trigger the special unification + case, which is wrong now :-( *) + let status,newgoalty = term_of_cic_term status newgoalty (ctx_of goalty) in + let newgoalty = mk_cic_term newgoalctx newgoalty in + let status, instance = mk_meta status newgoalctx (`Decl newgoalty) in @@ -329,19 +336,42 @@ let generalize_tac ~where = select_tac ~where ~job:(`Collect l) true; print_tac true "ha selezionato?"; (fun s -> distribute_tac (fun status goal -> - if !l = [] then fail (lazy "No term to generalize"); - let goalty = get_goalty status goal in - let canon = List.hd !l in - let status = + let goalty = get_goalty status goal in + let status,canon,rest = + match !l with + [] -> + (match where with + _,_,(None,_,_) -> fail (lazy "No term to generalize") + | txt,txtlen,(Some what,_,_) -> + let status, what = + disambiguate status (txt,txtlen,what) None (ctx_of goalty) + in + status,what,[] + ) + | he::tl -> status,he,tl in + let status = List.fold_left - (fun s t -> unify s (ctx_of goalty) canon t) status (List.tl !l) - in - let status, canon = term_of_cic_term status canon (ctx_of goalty) in - instantiate status goal - (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ])) + (fun s t -> unify s (ctx_of goalty) canon t) status rest in + let status, canon = term_of_cic_term status canon (ctx_of goalty) in + instantiate status goal + (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ])) ) s) ] ;; +let reduce_tac ~reduction ~where = + let change status t = + match reduction with + | `Normalize perform_delta -> + normalize status + ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t + | `Whd perform_delta -> + whd status + ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t + in + let where = GrafiteDisambiguate.disambiguate_npattern where in + select0_tac ~where ~job:(`ChangeWith change) +;; + let change_tac ~where ~with_what = let change status t = let status, ww = disambiguate status with_what None (ctx_of t) in @@ -352,6 +382,13 @@ let change_tac ~where ~with_what = select0_tac ~where ~job:(`ChangeWith change) ;; +let letin_tac ~where ~what:(_,_,w) name = + block_tac [ + select_tac ~where ~job:(`Substexpand 1) true; + exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit)); + ] +;; + let apply_tac = exact_tac;; type indtyinfo = { @@ -464,5 +501,55 @@ let case1_tac name = cases_tac ~where:("",0,(None,[],None)) ~what:("",0,Ast.Ident (name,None)); - if name = "_clearme" then clear_tac ["_clearme"] else id_tac ] + if name = "_clearme" then clear_tac ["_clearme"] else id_tac ] +;; + +let assert0_tac (hyps,concl) = distribute_tac (fun status goal -> + let gty = get_goalty status goal in + let eq status ctx t1 t2 = + let status,t1 = disambiguate status t1 None ctx in + let status,t1 = apply_subst status ctx t1 in + let status,t1 = term_of_cic_term status t1 ctx in + let t2 = mk_cic_term ctx t2 in + let status,t2 = apply_subst status ctx t2 in + let status,t2 = term_of_cic_term status t2 ctx in + prerr_endline ("COMPARING: " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t1 ^ " vs " ^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:ctx t2); + assert (t1=t2); + status + in + let status,gty' = term_of_cic_term status gty (ctx_of gty) in + let status = eq status (ctx_of gty) concl gty' in + let status,_ = + List.fold_right2 + (fun (id1,e1) ((id2,e2) as item) (status,ctx) -> + assert (id1=id2 || (prerr_endline (id1 ^ " vs " ^ id2); false)); + match e1,e2 with + `Decl t1, NCic.Decl t2 -> + let status = eq status ctx t1 t2 in + status,item::ctx + | `Def (b1,t1), NCic.Def (b2,t2) -> + let status = eq status ctx t1 t2 in + let status = eq status ctx b1 b2 in + status,item::ctx + | _ -> assert false + ) hyps (ctx_of gty) (status,[]) + in + exec id_tac status goal) +;; + +let assert_tac seqs status = + match status.gstatus with + | [] -> assert false + | (g,_,_,_) :: s -> + assert (List.length g = List.length seqs); + (match seqs with + [] -> id_tac + | [seq] -> assert0_tac seq + | _ -> + block_tac + (branch_tac:: + HExtlib.list_concat ~sep:[shift_tac] + (List.map (fun seq -> [assert0_tac seq]) seqs)@ + [merge_tac]) + ) status ;;