X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fring.ml;h=1d7cc10e6bfad0a0a16fe9b7ad2b74bc0dc6d078;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=298a87f3c8df8361fc4bcaee9f9cbaa5dc12c5d9;hpb=c792b3d48316f63cd1066b5901cf859496d71052;p=helm.git
diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index 298a87f3c..1d7cc10e6 100644
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -35,9 +35,7 @@ let debug = false
let debug_print = fun _ -> ()
(** debugging print *)
-let warn s =
- if debug then
- debug_print ("RING WARNING: " ^ s)
+let warn s = debug_print (lazy ("RING WARNING: " ^ (Lazy.force s)))
(** CIC URIS *)
@@ -199,10 +197,10 @@ let ringable =
in
function
| Cic.Appl (app::set::_::_::[]) when (is_equality app && is_real set) ->
- warn "Goal Ringable!";
+ warn (lazy "Goal Ringable!");
true
| _ ->
- warn "Goal Not Ringable :-((";
+ warn (lazy "Goal Not Ringable :-((");
false
(**
@@ -214,8 +212,8 @@ let ringable =
*)
let split_eq = function
| (Cic.Appl (_::_::t1::t2::[])) as term when ringable term ->
- warn ("" ^ (CicPp.ppterm t1) ^ "");
- warn ("" ^ (CicPp.ppterm t2) ^ "");
+ warn (lazy ("" ^ (CicPp.ppterm t1) ^ ""));
+ warn (lazy ("" ^ (CicPp.ppterm t2) ^ ""));
(t1, t2)
| _ -> raise GoalUnringable
@@ -368,7 +366,7 @@ let status_of_single_goal_tactic_result =
function
proof,[goal] -> proof,goal
| _ ->
- raise (Fail "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal")
+ raise (Fail (lazy "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal"))
(* Galla: spostata in variousTactics.ml
(**
@@ -377,7 +375,7 @@ let status_of_single_goal_tactic_result =
@param term term to cut
*)
let elim_type_tac ~term status =
- warn "in Ring.elim_type_tac";
+ warn (lazy "in Ring.elim_type_tac");
Tacticals.thens ~start:(cut_tac ~term)
~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] status
*)
@@ -388,12 +386,13 @@ let elim_type_tac ~term status =
@param term term to cut
@param proof term used to prove second subgoal generated by elim_type
*)
+(* FG: METTERE I NOMI ANCHE QUI? *)
let elim_type2_tac ~term ~proof =
let elim_type2_tac ~term ~proof status =
let module E = EliminationTactics in
- warn "in Ring.elim_type2";
+ warn (lazy "in Ring.elim_type2");
ProofEngineTypes.apply_tactic
- (Tacticals.thens ~start:(E.elim_type_tac ~term)
+ (Tacticals.thens ~start:(E.elim_type_tac term)
~continuations:[Tacticals.id_tac ; exact_tac ~term:proof]) status
in
ProofEngineTypes.mk_tactic (elim_type2_tac ~term ~proof)
@@ -406,7 +405,7 @@ let elim_type2_tac ~term ~proof =
@param status current proof engine status
*)
let reflexivity_tac (proof, goal) =
- warn "in Ring.reflexivity_tac";
+ warn (lazy "in Ring.reflexivity_tac");
let refl_eqt = mkCtor ~uri:refl_eqt_uri ~exp_named_subst:[] in
try
apply_tac (proof, goal) ~term:refl_eqt
@@ -463,7 +462,7 @@ let purge_hyps_tac ~count =
let ring_tac status =
let (proof, goal) = status in
- warn "in Ring tactic";
+ warn (lazy "in Ring tactic");
let eqt = mkMutInd (HelmLibraryObjects.Logic.eq_URI, 0) [] in
let r = HelmLibraryObjects.Reals.r in
let metasenv = metasenv_of_status status in
@@ -471,9 +470,10 @@ let ring_tac status =
let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
match (build_segments ~terms:[t1; t2]) with
| (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin
+ if debug then
List.iter (* debugging, feel free to remove *)
(fun (descr, term) ->
- warn (descr ^ " " ^ (CicPp.ppterm term)))
+ warn (lazy (descr ^ " " ^ (CicPp.ppterm term))))
(List.combine
["t1"; "t1'"; "t1''"; "t1'_eq_t1''";
"t2"; "t2'"; "t2''"; "t2'_eq_t2''"]
@@ -482,7 +482,7 @@ let ring_tac status =
try
let new_hyps = ref 0 in (* number of new hypotheses created *)
ProofEngineTypes.apply_tactic
- (Tacticals.try_tactics
+ (Tacticals.first
~tactics:[
"reflexivity", EqualityTactics.reflexivity_tac ;
"exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
@@ -503,7 +503,7 @@ let ring_tac status =
let b,_ = (*TASSI : FIXME*)
are_convertible context t1'' t1 CicUniv.empty_ugraph in
if not b then begin
- warn "t1'' and t1 are NOT CONVERTIBLE";
+ warn (lazy "t1'' and t1 are NOT CONVERTIBLE");
let newstatus =
ProofEngineTypes.apply_tactic
(elim_type2_tac (* 1st elim_type use *)
@@ -516,7 +516,7 @@ let ring_tac status =
(proof,[goal]) -> proof,goal
| _ -> assert false
end else begin
- warn "t1'' and t1 are CONVERTIBLE";
+ warn (lazy "t1'' and t1 are CONVERTIBLE");
status
end
in
@@ -525,7 +525,7 @@ let ring_tac status =
in
let status'' =
ProofEngineTypes.apply_tactic
- (Tacticals.try_tactics (* try to solve 1st subgoal *)
+ (Tacticals.first (* try to solve 1st subgoal *)
~tactics:[
"exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
"exact sym_eqt su t2 ...",
@@ -547,7 +547,7 @@ let ring_tac status =
are_convertible context t2'' t2 CicUniv.empty_ugraph
in
if not b then begin
- warn "t2'' and t2 are NOT CONVERTIBLE";
+ warn (lazy "t2'' and t2 are NOT CONVERTIBLE");
let newstatus =
ProofEngineTypes.apply_tactic
(elim_type2_tac (* 2nd elim_type use *)
@@ -560,16 +560,16 @@ let ring_tac status =
(proof,[goal]) -> proof,goal
| _ -> assert false
end else begin
- warn "t2'' and t2 are CONVERTIBLE";
+ warn (lazy "t2'' and t2 are CONVERTIBLE");
status
end
in
try (* try to solve main goal *)
- warn "trying reflexivity ....";
+ warn (lazy "trying reflexivity ....");
ProofEngineTypes.apply_tactic
EqualityTactics.reflexivity_tac status'
with (Fail _) -> (* leave conclusion to the user *)
- warn "reflexivity failed, solution's left as an ex :-)";
+ warn (lazy "reflexivity failed, solution's left as an ex :-)");
ProofEngineTypes.apply_tactic
(purge_hyps_tac ~count:!new_hyps) status')])
status'
@@ -577,7 +577,7 @@ let ring_tac status =
status'')])
status
with (Fail s) ->
- raise (Fail ("Ring failure: " ^ s))
+ raise (Fail (lazy ("Ring failure: " ^ Lazy.force s)))
end
| _ -> (* impossible: we are applying ring exacty to 2 terms *)
assert false
@@ -588,7 +588,7 @@ let ring_tac status =
try
ring_tac status
with GoalUnringable ->
- raise (Fail "goal unringable")
+ raise (Fail (lazy "goal unringable"))
let ring_tac = ProofEngineTypes.mk_tactic ring_tac