X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=21fc2b33c1f60aa1d1ded2a76fa812a4992ea97e;hb=b8ac0d11d5cd4083838a3848fce68683a518b54a;hp=cfed56c95b94fbf6d8a390189d8e34a3dd66a135;hpb=883bfac8ffa054608e4923d185405dbcb0a06f0f;p=helm.git diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index cfed56c95..21fc2b33c 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -open HelmLibraryObjects +let debug_print = fun _ -> () let rec injection_tac ~term = let injection_tac ~term status = @@ -39,7 +39,7 @@ let rec injection_tac ~term = ProofEngineTypes.apply_tactic (match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri Logic.eq_URI) -> ( + when LibraryObjects.is_eq_URI equri -> ( match tty with (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> ( @@ -95,7 +95,7 @@ and injection1_tac ~term ~i = 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 (U.eq equri Logic.eq_URI) -> ( + when LibraryObjects.is_eq_URI equri -> ( match tty with (* some inductive type *) (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> @@ -161,28 +161,31 @@ and injection1_tac ~term ~i = | _ -> raise (ProofEngineTypes.Fail "Injection: goal after cut is not correct") in ProofEngineTypes.apply_tactic - (P.change_tac - ~what:new_t1' - ~with_what: - (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] - )) + (ReductionTactics.change_tac + ~pattern:(ProofEngineTypes.conclusion_pattern (Some new_t1')) + (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] + )) status )) ~continuation: (T.then_ - ~start:(EqualityTactics.rewrite_simpl_tac ~term) + ~start: + (EqualityTactics.rewrite_simpl_tac + ~direction:`LeftToRight + ~pattern:(ProofEngineTypes.conclusion_pattern None) + term) ~continuation:EqualityTactics.reflexivity_tac ) ]) @@ -214,7 +217,7 @@ let discriminate'_tac ~term = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri Logic.eq_URI) -> ( + when LibraryObjects.is_eq_URI equri -> ( match tty with (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> @@ -273,8 +276,8 @@ let discriminate'_tac ~term = C.Lambda (binder,source,(aux target (k+1))) | _ -> if (id = false_constr_id) - then (C.MutInd(Logic.false_URI,0,[])) - else (C.MutInd(Logic.true_URI,0,[])) + then (C.MutInd(LibraryObjects.false_URI,0,[])) + else (C.MutInd(LibraryObjects.true_URI,0,[])) in aux red_ty 1 ) constructor_list @@ -284,7 +287,7 @@ let discriminate'_tac ~term = let (proof',goals') = ProofEngineTypes.apply_tactic (EliminationTactics.elim_type_tac - ~term:(C.MutInd(Logic.false_URI,0,[]))) + ~term:(C.MutInd(LibraryObjects.false_URI,0,[]))) status in (match goals' with @@ -296,25 +299,28 @@ let discriminate'_tac ~term = ProofEngineTypes.apply_tactic (T.then_ ~start: - (P.change_tac - ~what:gty' - ~with_what: - (C.Appl [ - C.Lambda ( - C.Name "x", tty, - C.MutCase ( - turi, typeno, - (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))), - (C.Rel 1), pattern - ) - ); - t2] - ) + (ReductionTactics.change_tac + ~pattern:(ProofEngineTypes.conclusion_pattern (Some gty')) + (C.Appl [ + C.Lambda ( + C.Name "x", tty, + C.MutCase ( + turi, typeno, + (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))), + (C.Rel 1), pattern + ) + ); + t2] + ) ) ~continuation: ( T.then_ - ~start:(EqualityTactics.rewrite_back_simpl_tac ~term) + ~start: + (EqualityTactics.rewrite_simpl_tac + ~direction:`RightToLeft + ~pattern:(ProofEngineTypes.conclusion_pattern None) + term) ~continuation:(IntroductionTactics.constructor_tac ~n:1) )) (proof',goal') @@ -427,8 +433,8 @@ let discriminate_tac ~term status = let (t1',t2',consno2') = (* bruuutto: uso un eccezione per terminare con successo! buuu!! :-/ *) try let rec traverse t1 t2 = -prerr_endline ("XXXX t1 " ^ CicPp.ppterm t1) ; -prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ; +debug_print ("XXXX t1 " ^ CicPp.ppterm t1) ; +debug_print ("XXXX t2 " ^ CicPp.ppterm t2) ; match t1,t2 with ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)), (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))) @@ -458,7 +464,7 @@ prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ; in traverse t1 t2 with (TwoDifferentSubtermsFound (t1,t2,consno2)) -> (t1,t2,consno2) in -prerr_endline ("XXXX consno2' " ^ (string_of_int consno2')) ; +debug_print ("XXXX consno2' " ^ (string_of_int consno2')) ; if consno2' = 0 then raise (ProofEngineTypes.Fail "Discriminate: Discriminating terms are structurally equal") else @@ -468,11 +474,11 @@ prerr_endline ("XXXX consno2' " ^ (string_of_int consno2')) ; match fst(CicEnvironment.get_obj turi CicUniv.empty_ugraph) with C.InductiveDefinition (ind_type_list,_,nr_ind_params) -> -prerr_endline ("XXXX nth " ^ (string_of_int (List.length ind_type_list)) ^ " " ^ (string_of_int typeno)) ; +debug_print ("XXXX nth " ^ (string_of_int (List.length ind_type_list)) ^ " " ^ (string_of_int typeno)) ; let _,_,_,constructor_list = (List.nth ind_type_list typeno) in -prerr_endline ("XXXX nth " ^ (string_of_int (List.length constructor_list)) ^ " " ^ (string_of_int consno2')) ; +debug_print ("XXXX nth " ^ (string_of_int (List.length constructor_list)) ^ " " ^ (string_of_int consno2')) ; let false_constr_id,_ = List.nth constructor_list (consno2' - 1) in -prerr_endline ("XXXX nth funzionano ") ; +debug_print ("XXXX nth funzionano ") ; List.map (function (id,cty) -> let red_ty = CicReduction.whd context cty in (* dubbio: e' corretto ridurre in questo context ??? *) @@ -522,21 +528,22 @@ prerr_endline ("XXXX nth funzionano ") ; ) ~continuation: ( -prerr_endline ("XXXX rewrite<-: " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2']))); -prerr_endline ("XXXX rewrite<-: " ^ CicPp.ppterm (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2'])) ; -prerr_endline ("XXXX equri: " ^ U.string_of_uri equri) ; -prerr_endline ("XXXX tty : " ^ CicPp.ppterm tty) ; -prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1')) ; -prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2')) ; -if (CicTypeChecker.type_of_aux' metasenv' context' t1') <> tty then prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1')) ; -if (CicTypeChecker.type_of_aux' metasenv' context' t2') <> tty then prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2')) ; +debug_print ("XXXX rewrite<-: " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2']))); +debug_print ("XXXX rewrite<-: " ^ CicPp.ppterm (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2'])) ; +debug_print ("XXXX equri: " ^ U.string_of_uri equri) ; +debug_print ("XXXX tty : " ^ CicPp.ppterm tty) ; +debug_print ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1')) ; +debug_print ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2')) ; +if (CicTypeChecker.type_of_aux' metasenv' context' t1') <> tty then debug_print ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1')) ; +if (CicTypeChecker.type_of_aux' metasenv' context' t2') <> tty then debug_print ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2')) ; if (CicTypeChecker.type_of_aux' metasenv' context' t1') <> (CicTypeChecker.type_of_aux' metasenv' context' t2') - then prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1')) ; prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2')) ; + then debug_print ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' + metasenv' context' t1')) ; debug_print ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2')) ; let termty' = ProofEngineReduction.replace_lifting ~equality:(==) ~what:t1 ~with_what:t1' ~where:termty in let termty'' = ProofEngineReduction.replace_lifting ~equality:(==) ~what:t2 ~with_what:t2' ~where:termty' in -prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' term)); +debug_print ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' term)); T.then_ ~start:(EqualityTactics.rewrite_back_simpl_tac ~term:term) ~continuation:(IntroductionTactics.constructor_tac ~n:1)