From: Claudio Sacerdoti Coen Date: Wed, 20 Sep 2006 16:21:53 +0000 (+0000) Subject: 1. bug fixed: injection now performs recursion lifting correctly X-Git-Tag: 0.4.95@7852~1019 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bf1f44a7486dd498de376e58039ff668beb168c2;p=helm.git 1. bug fixed: injection now performs recursion lifting correctly 2. bug introduced: injections now behaves as id_tac when it has nothing to do --- diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml index 42da52bd6..e6682709c 100644 --- a/components/tactics/discriminationTactics.ml +++ b/components/tactics/discriminationTactics.ml @@ -27,7 +27,7 @@ let debug_print = fun _ -> () -let rec injection_tac ~term = +let rec injection_tac ~term ~liftno ~continuation = let injection_tac ~term status = let (proof, goal) = status in let module C = Cic in @@ -36,6 +36,7 @@ let rec injection_tac ~term = let module T = Tacticals in let _,metasenv,_,_ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in + let term = CicSubstitution.lift liftno term in let termty,_ = (* TASSI: FIXME *) CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in @@ -51,29 +52,25 @@ let rec injection_tac ~term = (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))) when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) -> - (* raise (ProofEngineTypes.Fail "Injection: nothing to do") ; *) T.id_tac + (* raise (ProofEngineTypes.Fail "Injection: nothing to do") ; *) continuation ~liftno | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)), (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2))) when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) -> - let rec traverse_list i liftno l1 l2 = + let rec traverse_list i l1 l2 = match l1,l2 with - [],[] -> T.id_tac + [],[] -> continuation | hd1::tl1,hd2::tl2 -> if fst (CicReduction.are_convertible ~metasenv context hd1 hd2 CicUniv.empty_ugraph) then - traverse_list (i+1) liftno tl1 tl2 + traverse_list (i+1) tl1 tl2 else - T.then_ - ~start: - (injection1_tac ~i ~liftno - ~term:(CicSubstitution.lift liftno term)) - ~continuation: - (traverse_list (i+1) (liftno+1) tl1 tl2) + injection1_tac ~i ~term + ~continuation:(traverse_list (i+1) tl1 tl2) | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???")) - in traverse_list 1 0 applist1 applist2 + in traverse_list 1 applist1 applist2 ~liftno | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)), (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))) | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)), @@ -84,16 +81,16 @@ let rec injection_tac ~term = (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_))) when (consno1 <> consno2) || (exp_named_subst1 <> exp_named_subst2) -> raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality but a discriminable one")) - | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality")) + | _ -> continuation ~liftno (*raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))*) ) - | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality")) + | _ -> continuation ~liftno (*raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))*) ) | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equation")) ) status in ProofEngineTypes.mk_tactic (injection_tac ~term) -and injection1_tac ~term ~i ~liftno = +and injection1_tac ~term ~i ~liftno ~continuation = let injection1_tac ~term ~i 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 *) @@ -102,10 +99,12 @@ and injection1_tac ~term ~i ~liftno = let module U = UriManager in let module P = PrimitiveTactics in let module T = Tacticals in + let term = CicSubstitution.lift liftno term in let _,metasenv,_,_ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty,_ = (* TASSI: FIXME *) - CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in + CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph + in match termty with (* an equality *) (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) when LibraryObjects.is_eq_URI equri -> ( @@ -151,12 +150,6 @@ and injection1_tac ~term ~i ~liftno = in C.Lambda (binder',source,(aux target (k+1))) | _ -> -if id = i_constr_id then ( -prerr_endline ("k= " ^ string_of_int k); -prerr_endline ("paramsno= " ^ string_of_int paramsno); -prerr_endline ("nr_param_constr " ^ string_of_int (k - 1 - paramsno)); -prerr_endline ("rel= " ^ string_of_int (k - i)); -); let nr_param_constr = k - 1 - paramsno in if id = i_constr_id then C.Rel (k - i) @@ -211,7 +204,8 @@ prerr_endline ("rel= " ^ string_of_int (k - i)); ~start:(P.cut_tac (C.Appl [(C.MutInd (equri,0,[])) ; tty' ; t1' ; t2'])) ~continuations:[ T.then_ - ~start:T.id_tac (*(injection_tac ~term:(C.Rel 1))*) + ~start:(injection_tac ~liftno:0 ~term:(C.Rel 1) + ~continuation:(fun ~liftno:x -> continuation ~liftno:(liftno + 1 + x))) ~continuation:T.id_tac (* !!! qui devo anche fare clear di term tranne al primo passaggio *) ; T.then_ @@ -232,30 +226,20 @@ prerr_endline ("rel= " ^ string_of_int (k - i)); (lazy "Injection: goal after cut is not correct")) in -let aaa = ProofEngineTypes.apply_tactic (ReductionTactics.change_tac ~pattern:(ProofEngineTypes.conclusion_pattern (Some new_t1')) (fun _ m u -> -let xxx = C.Appl [ C.Lambda (C.Name "x", tty, C.MutCase (turi,typeno,outtype,C.Rel 1,patterns)) ; - t1] -in -prerr_endline ("i=" ^ string_of_int i ^ "; liftno=" ^ string_of_int liftno); -prerr_endline ("XXX: " ^ CicPp.ppterm xxx); -prerr_endline ("WITH: " ^ CicPp.ppterm new_t1'); -xxx, + t1], m, u)) status -in -prerr_endline "OK"; -aaa )) ~continuation: (T.then_ @@ -275,6 +259,10 @@ aaa ProofEngineTypes.mk_tactic (injection1_tac ~term ~i) ;; +let injection_tac = + injection_tac ~liftno:0 ~continuation:(fun ~liftno -> Tacticals.id_tac) +;; + exception TwoDifferentSubtermsFound of int (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori