X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=c9feaaee68da093fd97a49df693886a463fc5931;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=1a05bce1bed6d95c207704e4d23806891c30877d;hpb=66496e0c92e31547de2bd84defe0d83bc8bf49ea;p=helm.git diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 1a05bce1b..c9feaaee6 100644 --- 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)