From: Ferruccio Guidi Date: Wed, 24 Oct 2007 16:10:11 +0000 (+0000) Subject: we revisited the implementation of the destruct tactic in the perspective of joining... X-Git-Tag: 0.4.95@7852~106 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fba2e2e69c7ad9ed9a8747bcdf817de23781bb71;p=helm.git we revisited the implementation of the destruct tactic in the perspective of joining the subst tactic to it --- diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml index 21b609949..27baa2b9d 100644 --- a/components/tactics/discriminationTactics.ml +++ b/components/tactics/discriminationTactics.ml @@ -35,6 +35,8 @@ module PET = ProofEngineTypes module CTC = CicTypeChecker module CU = CicUniv module S = CicSubstitution +module RT = ReductionTactics +module PEH = ProofEngineHelpers let debug = false let debug_print = @@ -81,6 +83,8 @@ let relocate_term map t = in map_term 0 t +let id n = n + (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori diversi *) @@ -222,7 +226,7 @@ let discriminate_tac ~term = ~continuation: (T.then_ ~start: - (ReductionTactics.change_tac + (RT.change_tac ~pattern:(PET.conclusion_pattern None) (fun _ m u -> C.Appl [ @@ -260,26 +264,25 @@ let pp ctx t = let names = List.map (function Some (n,_) -> Some n | None -> None) ctx in CicPp.pp t names -let rec injection_tac ~term ~i ~liftno ~continuation = +let 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) in let rec mk_rels = function | 0 -> [] | n -> C.Rel n :: (mk_rels (n - 1)) in - let injection_tac ~term ~i status = + let injection_tac status = let (proof, goal) = status in (* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma * differiscono (o potrebbero differire?) nell'i-esimo parametro * del costruttore *) - let term = S.lift liftno term in let _,metasenv,_subst,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in - debug_print (lazy ("\ninjection1 su : " ^ pp context termty)); + debug_print (lazy ("\ninjection su : " ^ pp context termty)); match termty with (* an equality *) - | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] + | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] when LibraryObjects.is_eq_URI equri -> let turi,typeno,ens,params = match tty with (* some inductive type *) @@ -387,160 +390,136 @@ let rec injection_tac ~term ~i ~liftno ~continuation = | CTC.TypeCheckerFailure _ -> false in if not go_on then - PET.apply_tactic T.id_tac status + PET.apply_tactic T.id_tac status (* FG: ??????? *) else - (debug_print (lazy ("CUT: " ^ pp context cutted)); - PET.apply_tactic + let tac term = + let tac status = + debug_print (lazy "riempio il cut"); + let (proof, goal) = status in + let _,metasenv,_subst,_,_, _ = proof in + let _,context,gty = CicUtil.lookup_meta goal metasenv in + let gty = Unshare.unshare gty in + let new_t1' = match gty with + | (C.Appl (C.MutInd (_,_,_)::_::t::_)) -> t + | _ -> raise exn_injwronggoal + in + debug_print (lazy ("metto: " ^ pp context changed)); + debug_print (lazy ("al posto di: " ^ pp context new_t1')); + debug_print (lazy ("nel goal: " ^ pp context gty)); + debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); + debug_print (lazy ("e poi rewrite con: "^pp context term)); + let tac = T.seq ~tactics:[ + RT.change_tac + ~pattern:(None, [], Some (PEH.pattern_of ~term:gty [new_t1'])) + (fun _ m u -> changed,m,u); + EqualityTactics.rewrite_simpl_tac + ~direction:`LeftToRight + ~pattern:(PET.conclusion_pattern None) + term []; + EqualityTactics.reflexivity_tac + ] in + PET.apply_tactic tac status + in + PET.mk_tactic tac + in + debug_print (lazy ("CUT: " ^ pp context cutted)); + PET.apply_tactic (T.thens ~start: (P.cut_tac cutted) - ~continuations: - [injection1_tac ~first_time:false ~liftno:0 ~term:(C.Rel 1) - ~continuation: - (fun ~liftno:x -> continuation ~liftno:(liftno+1+x)) - (* here I need to lift all the continuations by 1; - since I am setting back liftno to 0, I actually - need to lift all the continuations by liftno + 1 *) - ;T.then_ - ~start:(PET.mk_tactic - (fun status -> - debug_print (lazy "riempo il cut"); - let (proof, goal) = status in - let _,metasenv,_subst,_,_, _ = proof in - let _,context,gty =CicUtil.lookup_meta goal metasenv in - let gty = Unshare.unshare gty in - let new_t1' = - match gty with - | (C.Appl (C.MutInd (_,_,_)::_::t::_)) -> t - | _ -> raise exn_injwronggoal - in - debug_print - (lazy ("metto questo: " ^ pp context changed)); - debug_print - (lazy ("al posto di questo: " ^ pp context new_t1')); - debug_print - (lazy ("nel goal: " ^ pp context gty)); - debug_print - (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); - debug_print - (lazy ("e poi rewrite con: "^pp context term)); - let rc = - PET.apply_tactic - (ReductionTactics.change_tac - ~pattern:(None, [], - Some (ProofEngineHelpers.pattern_of - ~term:gty [new_t1'])) - (fun _ m u -> changed,m,u)) - status - in rc - )) - ~continuation: - (T.then_ - ~start: - (EqualityTactics.rewrite_simpl_tac - ~direction:`LeftToRight - ~pattern:(PET.conclusion_pattern None) - term []) - ~continuation:EqualityTactics.reflexivity_tac) - ]) - status) + ~continuations:[continuation ~map:succ; tac term] + ) status | _ -> raise exn_noneq in - PET.mk_tactic (injection_tac ~term ~i) + 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 -and injection1_tac ~first_time ~term ~liftno ~continuation = +let rec 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 - let injection1_tac ~term status = + let qnify_tac status = let (proof, goal) = status in let _,metasenv,_subst, _,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in - let term = S.lift liftno term in + let term = relocate_term map term in let termty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in - debug_print (lazy ("\ninjection su: " ^ pp context termty)); - let tac = - match termty with + debug_print (lazy ("\nqnify su: " ^ pp context termty)); + let tac = match termty with | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] when LibraryObjects.is_eq_URI equri -> begin - match (CR.whd ~delta:true context tty) with - | C.MutInd (turi,typeno,ens) - | C.Appl (C.MutInd (turi,typeno,ens)::_) -> begin - match t1,t2 with - | C.MutConstruct (uri1,typeno1,consno1,ens1), - C.MutConstruct (uri2,typeno2,consno2,ens2) - when (uri1 = uri2) && (typeno1 = typeno2) && - (consno1 = consno2) && (ens1 = ens2) -> - if first_time then raise exn_nothingtodo - else continuation ~liftno - | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::applist1), - C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::applist2) - when (uri1 = uri2) && (typeno1 = typeno2) && - (consno1 = consno2) && (ens1 = ens2) -> - let rec traverse_list i l1 l2 = - match l1,l2 with - | [],[] when first_time -> continuation - | [],[] -> begin - match term with - | C.Rel n -> begin - match List.nth context (n-1) with - | Some (C.Name id,_) -> - fun ~liftno -> - T.then_ ~start:(PST.clear ~hyps:[id]) - ~continuation:(continuation ~liftno) - | _ -> assert false - end - | _ -> assert false - end - | hd1::tl1,hd2::tl2 -> + match (CR.whd ~delta:true context tty) with + | C.MutInd _ + | C.Appl (C.MutInd _ :: _) -> + begin match t1,t2 with + | C.MutConstruct _, + C.MutConstruct _ + when t1 = t2 -> + T.then_ ~start:(clear_term first_time context term) + ~continuation:(continuation ~map:id) + | C.Appl (C.MutConstruct _ as mc1 :: applist1), + C.Appl (C.MutConstruct _ as mc2 :: applist2) + when mc1 = mc2 -> + let rec traverse_list i l1 l2 = match l1, l2 with + | [], [] -> + T.then_ ~start:(clear_term first_time context term) + ~continuation:(continuation ~map:id) + | hd1 :: tl1, hd2 :: tl2 -> if are_convertible hd1 hd2 metasenv context then - traverse_list (i+1) tl1 tl2 + traverse_list (succ i) tl1 tl2 else - injection_tac ~i ~term - ~continuation:(traverse_list (i+1) tl1 tl2) + injection_tac ~i ~term ~continuation: + (qnify_tac ~first_time:false ~term ~continuation) | _ -> assert false (* i 2 termini hanno in testa lo stesso costruttore, * ma applicato a un numero diverso di termini *) in - traverse_list 1 applist1 applist2 ~liftno - | C.MutConstruct (uri1,typeno1,consno1,ens1), - C.MutConstruct (uri2,typeno2,consno2,ens2) - | C.MutConstruct (uri1,typeno1,consno1,ens1), - C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::_) - | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::_), - C.MutConstruct (uri2,typeno2,consno2,ens2) - | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::_), - C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::_) + traverse_list 1 applist1 applist2 + | C.MutConstruct (_,_,consno1,ens1), + C.MutConstruct (_,_,consno2,ens2) + | C.MutConstruct (_,_,consno1,ens1), + C.Appl ((C.MutConstruct (_,_,consno2,ens2))::_) + | C.Appl ((C.MutConstruct (_,_,consno1,ens1))::_), + C.MutConstruct (_,_,consno2,ens2) + | C.Appl ((C.MutConstruct (_,_,consno1,ens1))::_), + C.Appl ((C.MutConstruct (_,_,consno2,ens2))::_) when (consno1 <> consno2) || (ens1 <> ens2) -> discriminate_tac ~term - | _ when not first_time -> continuation ~liftno + | _ when not first_time -> continuation ~map:id | _ (* when first_time *) -> - match term with - | Cic.Rel i -> - let name = - match List.nth context (i-1) with - | Some (Cic.Name s, Cic.Def _) -> s - | Some (Cic.Name s, Cic.Decl _) -> s - | _ -> assert false - in - T.then_ - ~start:(ReductionTactics.simpl_tac - ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None)) - ~continuation:(injection1_tac ~first_time:false ~term ~liftno - ~continuation) - | _ -> raise exn_nonproj - end - | _ when not first_time -> continuation ~liftno + T.then_ ~start:(simpl_in_term context term) + ~continuation:(qnify_tac ~first_time:false ~term ~map:id ~continuation) + end + | _ when not first_time -> continuation ~map:id | _ (* when first_time *) -> raise exn_nonproj end | _ -> raise exn_nonproj in PET.apply_tactic tac status in - PET.mk_tactic (injection1_tac ~term) + PET.mk_tactic qnify_tac (* destruct performs either injection or discriminate *) (* equivalent to Coq's "analyze equality" *) let destruct_tac = - injection1_tac - ~first_time:true ~liftno:0 ~continuation:(fun ~liftno -> T.id_tac) + qnify_tac + ~first_time:true ~map:id ~continuation:(fun ~map -> T.id_tac)