X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=24ab511f05d71c77f08e83e186b8be41f67f27d2;hb=bbe7741f3bbaacb93f2876c018dace82f5e929b8;hp=ceaccdcefaed715d9a636da8c34f222a1099447f;hpb=655906d74521fa49de332f54ec34bfc9d9744151;p=helm.git diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index ceaccdcef..24ab511f0 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -25,6 +25,8 @@ open HelmLibraryObjects +let debug_print = fun _ -> () + let rec injection_tac ~term = let injection_tac ~term status = let (proof, goal) = status in @@ -32,10 +34,11 @@ let rec injection_tac ~term = let module U = UriManager in let module P = PrimitiveTactics in let module T = Tacticals in - let _,metasenv,_,_ = proof in - let _,context,_ = CicUtil.lookup_meta goal metasenv in - let termty = (CicTypeChecker.type_of_aux' metasenv context term) in - ProofEngineTypes.apply_tactic + 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 + ProofEngineTypes.apply_tactic (match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) when (U.eq equri Logic.eq_URI) -> ( @@ -88,36 +91,31 @@ and injection1_tac ~term ~i = let module U = UriManager in let module P = PrimitiveTactics in let module T = Tacticals in - let _,metasenv,_,_ = proof in - let _,context,_ = CicUtil.lookup_meta goal metasenv in - let termty = (CicTypeChecker.type_of_aux' metasenv context term) in - match termty with (* an equality *) - (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) + 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 + match termty with (* an equality *) + (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) when (U.eq equri Logic.eq_URI) -> ( match tty with (* some inductive type *) (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> - prerr_endline ("XXXX term " ^ CicPp.ppterm term) ; - prerr_endline ("XXXX termty " ^ CicPp.ppterm termty) ; - prerr_endline ("XXXX t1 " ^ CicPp.ppterm t1) ; - prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ; - prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ; let t1',t2',consno = (* sono i due sottotermini che differiscono *) match t1,t2 with ((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) -> (* controllo ridondante *) (List.nth applist1 (i-1)),(List.nth applist2 (i-1)),consno2 - | _ -> raise (ProofEngineTypes.Fail "Injection: qui non dovrei capitarci mai") + | _ -> assert false in - let tty' = (CicTypeChecker.type_of_aux' metasenv context t1') in - prerr_endline ("XXXX tty' " ^ CicPp.ppterm tty') ; - prerr_endline ("XXXX t1' " ^ CicPp.ppterm t1') ; - prerr_endline ("XXXX t2' " ^ CicPp.ppterm t2') ; - prerr_endline ("XXXX consno " ^ string_of_int consno) ; + let tty',_ = + CicTypeChecker.type_of_aux' metasenv context t1' + CicUniv.empty_ugraph in let pattern = - match (CicEnvironment.get_obj turi) with - C.InductiveDefinition (ind_type_list,_,nr_ind_params_dx) -> + 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 @@ -144,7 +142,6 @@ and injection1_tac ~term ~i = constructor_list | _ -> raise (ProofEngineTypes.Fail "Discriminate: object is not an Inductive Definition: it's imposible") in - prerr_endline ("XXXX cominciamo!") ; ProofEngineTypes.apply_tactic (T.thens ~start:(P.cut_tac (C.Appl [(C.MutInd (equri,0,[])) ; tty' ; t1' ; t2'])) @@ -159,20 +156,16 @@ and injection1_tac ~term ~i = let (proof, goal) = status in let _,metasenv,_,_ = proof in let _,context,gty = CicUtil.lookup_meta goal metasenv in - prerr_endline ("XXXX goal " ^ string_of_int goal) ; - prerr_endline ("XXXX gty " ^ CicPp.ppterm gty) ; - prerr_endline ("XXXX old t1' " ^ CicPp.ppterm t1') ; - prerr_endline ("XXXX change " ^ CicPp.ppterm (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])) ; let new_t1' = match gty with (C.Appl (C.MutInd (_,_,_)::arglist)) -> List.nth arglist 1 | _ -> raise (ProofEngineTypes.Fail "Injection: goal after cut is not correct") in - prerr_endline ("XXXX new t1' " ^ CicPp.ppterm new_t1') ; ProofEngineTypes.apply_tactic (P.change_tac ~what:new_t1' + ~pattern:([],None) ~with_what: (C.Appl [ C.Lambda ( @@ -192,7 +185,7 @@ and injection1_tac ~term ~i = )) ~continuation: (T.then_ - ~start:(EqualityTactics.rewrite_simpl_tac ~term) + ~start:(EqualityTactics.rewrite_simpl_tac ~term ()) ~continuation:EqualityTactics.reflexivity_tac ) ]) @@ -218,9 +211,10 @@ let discriminate'_tac ~term = let module U = UriManager in let module P = PrimitiveTactics in let module T = Tacticals in - let _,metasenv,_,_ = proof in - let _,context,_ = CicUtil.lookup_meta goal metasenv in - let termty = (CicTypeChecker.type_of_aux' metasenv context term) in + let _,metasenv,_,_ = proof in + let _,context,_ = CicUtil.lookup_meta goal metasenv in + let termty,_ = + 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) -> ( @@ -231,8 +225,6 @@ let discriminate'_tac ~term = let 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) ; match t1,t2 with ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)), (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))) @@ -262,20 +254,17 @@ prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ; in traverse t1 t2 with (TwoDifferentSubtermsFound consno2) -> consno2 in -prerr_endline ("XXXX consno2 " ^ (string_of_int consno2)) ; if consno2 = 0 then raise (ProofEngineTypes.Fail "Discriminate: Discriminating terms are structurally equal") else let pattern = (* a list of "True" except for the element in position consno2 which is "False" *) - match (CicEnvironment.get_obj turi) 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)) ; + match fst(CicEnvironment.get_obj + CicUniv.empty_ugraph turi) with + C.InductiveDefinition (ind_type_list,_,nr_ind_params,_) -> 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)) ; let false_constr_id,_ = List.nth constructor_list (consno2 - 1) in -prerr_endline ("XXXX nth funzionano ") ; List.map (function (id,cty) -> let red_ty = CicReduction.whd context cty in (* dubbio: e' corretto ridurre in questo context ??? *) @@ -312,6 +301,7 @@ prerr_endline ("XXXX nth funzionano ") ; ~start: (P.change_tac ~what:gty' + ~pattern:([],None) ~with_what: (C.Appl [ C.Lambda ( @@ -327,19 +317,9 @@ 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)) ; -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)) ; -prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' term)); T.then_ - ~start:(EqualityTactics.rewrite_back_simpl_tac ~term) + ~start:(EqualityTactics.rewrite_back_simpl_tac + ~term ()) ~continuation:(IntroductionTactics.constructor_tac ~n:1) )) (proof',goal') @@ -452,8 +432,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))) @@ -483,20 +463,21 @@ 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 let pattern = (* a list of "True" except for the element in position consno2' which is "False" *) - match (CicEnvironment.get_obj turi) with + 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 ??? *) @@ -546,21 +527,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)