X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FdiscriminationTactics.ml;h=e6682709c1b75edff7bda053889a19bde01f9238;hb=92d0723eca60b8d73b1f4597551155dcceaa9ced;hp=9ec2d76221e19ffd3dc48f44374c7c1c085517fb;hpb=3a0c3a4275ba88babc9d5717a019fe277d947fa6;p=helm.git diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml index 9ec2d7622..e6682709c 100644 --- a/helm/software/components/tactics/discriminationTactics.ml +++ b/helm/software/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)), @@ -83,17 +80,17 @@ let rec injection_tac ~term = | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::_)), (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_))) when (consno1 <> consno2) || (exp_named_subst1 <> exp_named_subst2) -> - (* raise (ProofEngineTypes.Fail "Injection: not a projectable equality but a discriminable one") ; *) T.id_tac - | _ -> (* raise (ProofEngineTypes.Fail "Injection: not a projectable equality") ; *) T.id_tac + raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality but a discriminable one")) + | _ -> 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 -> ( @@ -132,6 +131,7 @@ and injection1_tac ~term ~i ~liftno = List.nth ind_type_list typeno in let i_constr_id,_ = List.nth constructor_list (consno - 1) in + let seed = ref 0 in let patterns = List.map (function (id,cty) -> @@ -143,22 +143,31 @@ and injection1_tac ~term ~i ~liftno = | C.Prod (binder,source,target) when k > paramsno -> let binder' = match binder with - C.Name b -> C.Name b - | C.Anonymous -> C.Name "y" + C.Name _ -> binder + | C.Anonymous -> + C.Name + (incr seed; "y" ^ string_of_int !seed) in C.Lambda (binder',source,(aux target (k+1))) | _ -> let nr_param_constr = k - 1 - paramsno in if id = i_constr_id - then C.Rel (nr_param_constr - liftno) + then C.Rel (k - i) else S.lift (nr_param_constr + 1) t1' (* + 1 per liftare anche il lambda aggiunto esternamente al case *) in aux reduced_cty 1 ) constructor_list in let outtype = + let seed = ref 0 in let rec to_lambdas te head = match CicReduction.whd context te with - | C.Prod (name,so,ta) -> - C.Lambda (name,so,to_lambdas ta head) + | C.Prod (binder,so,ta) -> + let binder' = + match binder with + C.Name _ -> binder + | C.Anonymous -> + C.Name (incr seed; "d" ^ string_of_int !seed) + in + C.Lambda (binder',so,to_lambdas ta head) | _ -> head in let rec skip_prods n te = match n, CicReduction.whd context te with @@ -195,7 +204,8 @@ and injection1_tac ~term ~i ~liftno = ~start:(P.cut_tac (C.Appl [(C.MutInd (equri,0,[])) ; tty' ; t1' ; t2'])) ~continuations:[ T.then_ - ~start:(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_ @@ -216,29 +226,20 @@ and injection1_tac ~term ~i ~liftno = (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 ("XXX: " ^ CicPp.ppterm xxx); -prerr_endline ("WITH: " ^ CicPp.ppterm new_t1'); -xxx, + t1], m, u)) status -in -prerr_endline "OK"; -aaa )) ~continuation: (T.then_ @@ -253,11 +254,15 @@ aaa status | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equality over elements of an inductive type")) ) - | _ -> ProofEngineTypes.apply_tactic T.id_tac status (*XXXraise (ProofEngineTypes.Fail (lazy "Injection: not an equality"))*) + | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equality")) in 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