various updates, removed proofs for now because they are the real bottleneck!!

[helm.git] / helm / ocaml / tactics / discriminationTactics.ml

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index cfed56c95b94fbf6d8a390189d8e34a3dd66a135..24ab511f05d71c77f08e83e186b8be41f67f27d2 100644 (file)
--- 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
@@ -163,6 +165,7 @@ and injection1_tac ~term ~i =
                             ProofEngineTypes.apply_tactic 
                             (P.change_tac
                                ~what:new_t1'
+                               ~pattern:([],None)
                                ~with_what:
                                  (C.Appl [
                                    C.Lambda (
@@ -182,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
                        )
                    ])     
@@ -298,6 +301,7 @@ let discriminate'_tac ~term =
                              ~start:
                               (P.change_tac 
                                ~what:gty' 
+                               ~pattern:([],None)
                                ~with_what:
                                 (C.Appl [
                                   C.Lambda (
@@ -314,7 +318,8 @@ let discriminate'_tac ~term =
                              ~continuation:
                               (
                                  T.then_
-                                   ~start:(EqualityTactics.rewrite_back_simpl_tac ~term)
+                                   ~start:(EqualityTactics.rewrite_back_simpl_tac
+                                   ~term ())
                                    ~continuation:(IntroductionTactics.constructor_tac ~n:1) 
                               ))
                              (proof',goal')
@@ -427,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)))
@@ -458,7 +463,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 +473,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 +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)