From: Ferruccio Guidi Date: Wed, 24 Oct 2007 17:24:18 +0000 (+0000) Subject: bug fix in injection: we have to recur on the generated premises X-Git-Tag: 0.4.95@7852~105 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=681ef7c2760a6c628ed4fa96b2f9b5690ac5e1c8;p=helm.git bug fix in injection: we have to recur on the generated premises --- diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml index 27baa2b9d..f12e4b3f5 100644 --- a/components/tactics/discriminationTactics.ml +++ b/components/tactics/discriminationTactics.ml @@ -81,10 +81,12 @@ let relocate_term map t = | C.Fix (i, fs) -> C.Fix (i, map_fs (List.length fs) k fs) | C.CoFix (i, cfs) -> C.CoFix (i, map_cfs (List.length cfs) k cfs) in - map_term 0 t + map_term 1 t let id n = n +let comp f g n = f (g n) + (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori diversi *) @@ -264,7 +266,30 @@ let pp ctx t = let names = List.map (function Some (n,_) -> Some n | None -> None) ctx in CicPp.pp t names -let injection_tac ~term ~i ~continuation = +let clear_term first_time context term = + let g () = if first_time then raise exn_nothingtodo else T.id_tac in + match term with + | C.Rel n -> + begin match List.nth context (pred n) with + | Some (C.Name id, _) -> PST.clear ~hyps:[id] + | _ -> assert false + end + | _ -> g () + +let simpl_in_term context = function + | Cic.Rel i -> + let name = match List.nth context (pred i) with + | Some (Cic.Name s, Cic.Def _) -> s + | Some (Cic.Name s, Cic.Decl _) -> s + | _ -> assert false + in + RT.simpl_tac ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None) + | _ -> raise exn_nonproj + +(* ~term vive nel contesto della tattica + * ~continuation riceve la mappa relativa + *) +let rec injection_tac ~term ~i ~continuation = let give_name seed = function | C.Name _ as name -> name | C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed) @@ -423,35 +448,22 @@ let injection_tac ~term ~i ~continuation = PET.mk_tactic tac in debug_print (lazy ("CUT: " ^ pp context cutted)); + let continuation ~map = continuation ~map:(comp succ map) in PET.apply_tactic (T.thens ~start: (P.cut_tac cutted) - ~continuations:[continuation ~map:succ; tac term] + ~continuations:[ + (qnify_tac ~first_time:false ~term:(C.Rel 1) ~map:id + ~continuation); + tac term] ) status | _ -> raise exn_noneq in PET.mk_tactic injection_tac -let clear_term first_time context term = - let g () = if first_time then raise exn_nothingtodo else T.id_tac in - match term with - | C.Rel n -> - begin match List.nth context (pred n) with - | Some (C.Name id, _) -> PST.clear ~hyps:[id] - | _ -> assert false - end - | _ -> g () - -let simpl_in_term context = function - | Cic.Rel i -> - let name = match List.nth context (pred i) with - | Some (Cic.Name s, Cic.Def _) -> s - | Some (Cic.Name s, Cic.Decl _) -> s - | _ -> assert false - in - RT.simpl_tac ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None) - | _ -> raise exn_nonproj - -let rec qnify_tac ~first_time ~map ~term ~continuation = +(* ~term vive nel contesto della tattica una volta ~mappato + * ~continuation riceve la mappa relativa + *) +and qnify_tac ~first_time ~map ~term ~continuation = let are_convertible hd1 hd2 metasenv context = fst (CR.are_convertible ~metasenv context hd1 hd2 CicUniv.empty_ugraph) in