X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FdiscriminationTactics.ml;h=e6682709c1b75edff7bda053889a19bde01f9238;hb=92d0723eca60b8d73b1f4597551155dcceaa9ced;hp=4c7f5148d1cb5a1ff225c676c7f4ea9931011b01;hpb=08a92d276c5477968b02f31097b6ed03185f34eb;p=helm.git diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml index 4c7f5148d..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,8 +36,10 @@ 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 + CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph + in ProofEngineTypes.apply_tactic (match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) @@ -50,19 +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 l1 l2 = match l1,l2 with - [],[] -> T.id_tac + [],[] -> continuation | hd1::tl1,hd2::tl2 -> - T.then_ - ~start:(injection1_tac ~i ~term) - ~continuation:(traverse_list (i+1) tl1 tl2) + if + fst + (CicReduction.are_convertible ~metasenv + context hd1 hd2 CicUniv.empty_ugraph) + then + traverse_list (i+1) tl1 tl2 + else + 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 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)), @@ -72,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 = +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 *) @@ -91,10 +99,12 @@ and injection1_tac ~term ~i = 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 -> ( @@ -112,42 +122,90 @@ and injection1_tac ~term ~i = let tty',_ = CicTypeChecker.type_of_aux' metasenv context t1' CicUniv.empty_ugraph in - let pattern = - match fst(CicEnvironment.get_obj - CicUniv.empty_ugraph turi ) with - C.InductiveDefinition (ind_type_list,_,nr_ind_params_dx,_) -> - let _,_,_,constructor_list = (List.nth ind_type_list typeno) in - let i_constr_id,_ = List.nth constructor_list (consno - 1) in - List.map - (function (id,cty) -> - let reduced_cty = CicReduction.whd context cty in - let rec aux t k = - match t with - C.Prod (_,_,target) when (k <= nr_ind_params_dx) -> - aux target (k+1) - | C.Prod (binder,source,target) when (k > nr_ind_params_dx) -> - let binder' = - match binder with - C.Name b -> C.Name b - | C.Anonymous -> C.Name "y" - in - C.Lambda (binder',source,(aux target (k+1))) - | _ -> - let nr_param_constr = k - 1 - nr_ind_params_dx in - if (id = i_constr_id) - then C.Rel (nr_param_constr - i + 1) - else S.lift (nr_param_constr + 1) t1' (* + 1 per liftare anche il lambda agguinto esternamente al case *) - in aux reduced_cty 1 - ) - constructor_list - | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible")) + let patterns,outtype = + match + fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi) + with + C.InductiveDefinition (ind_type_list,_,paramsno,_)-> + let _,_,_,constructor_list = + 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) -> + let reduced_cty = CicReduction.whd context cty in + let rec aux t k = + match t with + C.Prod (_,_,target) when k <= paramsno -> + aux target (k+1) + | C.Prod (binder,source,target) when k > paramsno -> + let binder' = + match binder with + 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 (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 (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 + 0, _ -> te + | n, C.Prod (_,_,ta) -> skip_prods (n - 1) ta + | _, _ -> assert false + in + let abstracted_tty = + match CicSubstitution.lift (paramsno + 1) tty with + C.MutInd _ as tty' -> tty' + | C.Appl l -> + let keep,abstract = + HExtlib.split_nth (paramsno +1) l in + let rec mk_rels = + function + 0 -> [] + | n -> C.Rel n :: (mk_rels (n - 1)) + in + C.Appl (keep@mk_rels (List.length abstract)) + | _ -> assert false + in + match ind_type_list with + [] -> assert false + | (_,_,ty,_)::_ -> + to_lambdas (skip_prods paramsno ty) + (C.Lambda (C.Name "x", abstracted_tty, + S.lift (2+paramsno) tty')) + in + patterns,outtype + | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible")) in ProofEngineTypes.apply_tactic (T.thens ~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_ @@ -155,27 +213,32 @@ and injection1_tac ~term ~i = (fun status -> let (proof, goal) = status in let _,metasenv,_,_ = proof in - let _,context,gty = CicUtil.lookup_meta goal metasenv in + let _,context,gty = + CicUtil.lookup_meta goal metasenv + in let new_t1' = match gty with (C.Appl (C.MutInd (_,_,_)::arglist)) -> List.nth arglist 1 - | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: goal after cut is not correct")) + | _ -> + raise + (ProofEngineTypes.Fail + (lazy + "Injection: goal after cut is not correct")) in ProofEngineTypes.apply_tactic (ReductionTactics.change_tac ~pattern:(ProofEngineTypes.conclusion_pattern (Some new_t1')) (fun _ m u -> - C.Appl [ C.Lambda (C.Name "x", tty, - C.MutCase (turi, typeno, - (C.Lambda ((C.Name "x"), - (S.lift 1 tty), - (S.lift 2 tty'))), - (C.Rel 1), pattern - ) - ); - t1], m, u)) + C.Appl [ + C.Lambda + (C.Name "x", + tty, + C.MutCase + (turi,typeno,outtype,C.Rel 1,patterns)) ; + t1], + m, u)) status )) ~continuation: @@ -189,13 +252,17 @@ and injection1_tac ~term ~i = ) ]) status - | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: not a discriminable equality")) + | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equality over elements of an inductive type")) ) - | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: 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