* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let debug_print = fun _ -> ()
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???"))
in traverse_list 1 applist1 applist2
| ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
(C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
(* 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)
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
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
)
])
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)
;;
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
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)))
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
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 ??? *)
)
~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)