ocaml 3.09 transition

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

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 1a05bce1bed6d95c207704e4d23806891c30877d..c9feaaee68da093fd97a49df693886a463fc5931 100644 (file)
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -59,7 +59,7 @@ let rec injection_tac ~term =
                              T.then_ 
                               ~start:(injection1_tac ~i ~term)
                               ~continuation:(traverse_list (i+1) tl1 tl2)
-                          | _ -> raise (ProofEngineTypes.Fail "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???") ; T.id_tac
+                          | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???")) ; T.id_tac
                        in traverse_list 1 applist1 applist2
                     | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
                        (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
@@ -73,9 +73,9 @@ let rec injection_tac ~term =
                        (* 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 "Injection: not a projectable equality")
+            | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))
            )
-        | _ -> raise (ProofEngineTypes.Fail "Injection: not an equation")
+        | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equation"))
       ) status
  in 
   ProofEngineTypes.mk_tactic (injection_tac ~term)
@@ -138,7 +138,7 @@ and injection1_tac ~term ~i =
                                 in aux reduced_cty 1
                              )
                              constructor_list
-                       | _ -> raise (ProofEngineTypes.Fail "Discriminate: object is not an Inductive Definition: it's imposible")
+                       | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible"))
                 in
                 ProofEngineTypes.apply_tactic   
                  (T.thens 
@@ -158,7 +158,7 @@ and injection1_tac ~term ~i =
                             match gty with 
                                (C.Appl (C.MutInd (_,_,_)::arglist)) -> 
                                 List.nth arglist 1
-                             | _ -> raise (ProofEngineTypes.Fail "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
@@ -187,9 +187,9 @@ and injection1_tac ~term ~i =
                        )
                    ])     
                   status
-            | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")
+            | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: not a discriminable equality"))
            )
-        | _ -> raise (ProofEngineTypes.Fail "Discriminate: not an equality")
+        | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: not an equality"))
  in
   ProofEngineTypes.mk_tactic (injection1_tac ~term ~i)
 ;;
@@ -204,7 +204,7 @@ let discriminate'_tac ~term =
  let module U = UriManager in
  let module P = PrimitiveTactics in
  let module T = Tacticals in
- let fail msg = raise (ProofEngineTypes.Fail ("Discriminate: " ^ msg)) in
+ let fail msg = raise (ProofEngineTypes.Fail (lazy ("Discriminate: " ^ msg))) in
  let find_discriminating_consno t1 t2 =
    let rec aux t1 t2 =
      match t1, t2 with
@@ -423,8 +423,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 =
-debug_print ("XXXX t1 " ^ CicPp.ppterm t1) ;
-debug_print ("XXXX t2 " ^ CicPp.ppterm t2) ;
+debug_print (lazy ("XXXX t1 " ^ CicPp.ppterm t1)) ;
+debug_print (lazy ("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)))
@@ -454,7 +454,7 @@ debug_print ("XXXX t2 " ^ CicPp.ppterm t2) ;
                   in traverse t1 t2
                  with (TwoDifferentSubtermsFound (t1,t2,consno2)) -> (t1,t2,consno2)
                 in
-debug_print ("XXXX consno2' " ^ (string_of_int consno2')) ;
+debug_print (lazy ("XXXX consno2' " ^ (string_of_int consno2'))) ;
                  if consno2' = 0 
                   then raise (ProofEngineTypes.Fail "Discriminate: Discriminating terms are structurally equal")
                   else
@@ -464,11 +464,11 @@ debug_print ("XXXX consno2' " ^ (string_of_int consno2')) ;
                      match fst(CicEnvironment.get_obj turi 
                                  CicUniv.empty_ugraph) with
                         C.InductiveDefinition (ind_type_list,_,nr_ind_params)  ->
-debug_print ("XXXX nth " ^ (string_of_int (List.length ind_type_list)) ^ " " ^ (string_of_int typeno)) ;
+debug_print (lazy ("XXXX nth " ^ (string_of_int (List.length ind_type_list)) ^ " " ^ (string_of_int typeno))) ;
                          let _,_,_,constructor_list = (List.nth ind_type_list typeno) in 
-debug_print ("XXXX nth " ^ (string_of_int (List.length constructor_list)) ^ " " ^ (string_of_int consno2')) ;
+debug_print (lazy ("XXXX nth " ^ (string_of_int (List.length constructor_list)) ^ " " ^ (string_of_int consno2'))) ;
                           let false_constr_id,_ = List.nth constructor_list (consno2' - 1) in
-debug_print ("XXXX nth funzionano ") ;
+debug_print (lazy "XXXX nth funzionano ") ;
                            List.map 
                             (function (id,cty) ->
                               let red_ty = CicReduction.whd context cty in (* dubbio: e' corretto ridurre in questo context ??? *)
@@ -518,22 +518,22 @@ debug_print ("XXXX nth funzionano ") ;
                               )
                              ~continuation:
                               (
-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')) ;
+debug_print (lazy ("XXXX rewrite<-: " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2']))));
+debug_print (lazy ("XXXX rewrite<-: " ^ CicPp.ppterm (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2']))) ;
+debug_print (lazy ("XXXX equri: " ^ U.string_of_uri equri)) ;
+debug_print (lazy ("XXXX tty : " ^ CicPp.ppterm tty)) ;
+debug_print (lazy ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1'))) ;
+debug_print (lazy ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2'))) ;
+if (CicTypeChecker.type_of_aux' metasenv' context' t1') <> tty then debug_print (lazy ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1'))) ;
+if (CicTypeChecker.type_of_aux' metasenv' context' t2') <> tty then debug_print (lazy ("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 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')) ;
+ then debug_print (lazy ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux'
+ metasenv' context' t1'))) ; debug_print (lazy ("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
 
-debug_print ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' term));
+debug_print (lazy ("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)