X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fring.ml;fp=helm%2Focaml%2Ftactics%2Fring.ml;h=cf6950c4be9776a7d4de1ad309c1a29d4da8b6e2;hb=655906d74521fa49de332f54ec34bfc9d9744151;hp=e2de0459193e91339b562f4f3a27075781585d78;hpb=87ad71faeb3f544a3a21b2b57a589fc55543bae6;p=helm.git diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml index e2de04591..cf6950c4b 100644 --- a/helm/ocaml/tactics/ring.ml +++ b/helm/ocaml/tactics/ring.ml @@ -389,11 +389,15 @@ let elim_type_tac ~term status = @param term term to cut @param proof term used to prove second subgoal generated by elim_type *) -let elim_type2_tac ~term ~proof status = +let elim_type2_tac ~term ~proof = + let elim_type2_tac ~term ~proof status = let module E = EliminationTactics in warn "in Ring.elim_type2"; - Tacticals.thens ~start:(E.elim_type_tac ~term) - ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] status + ProofEngineTypes.apply_tactic + (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) (* Galla: spostata in variousTactics.ml (** @@ -423,7 +427,8 @@ let lift ~n (a,b,c,d,e,f,g,h) = @param count number of hypotheses to remove @param status current proof engine status *) -let purge_hyps_tac ~count status = +let purge_hyps_tac ~count = + let purge_hyps_tac ~count status = let module S = ProofEngineStructuralRules in let (proof, goal) = status in let rec aux n context status = @@ -432,7 +437,8 @@ let purge_hyps_tac ~count status = | (0, _) -> status | (n, hd::tl) -> aux (n-1) tl - (status_of_single_goal_tactic_result (S.clear ~hyp:hd status)) + (status_of_single_goal_tactic_result + (ProofEngineTypes.apply_tactic (S.clear ~hyp:hd) status)) | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left" in let (_, metasenv, _, _) = proof in @@ -440,6 +446,8 @@ let purge_hyps_tac ~count status = let proof',goal' = aux count context status in assert (goal = goal') ; proof',[goal'] + in + ProofEngineTypes.mk_tactic (purge_hyps_tac ~count) (** THE TACTIC! *) @@ -447,6 +455,7 @@ let purge_hyps_tac ~count status = Ring tactic, does associative and commutative rewritings in Reals ring @param status current proof engine status *) + let ring_tac status = let (proof, goal) = status in warn "in Ring tactic"; @@ -467,8 +476,8 @@ let ring_tac status = t2; t2'; t2''; t2'_eq_t2'']); try let new_hyps = ref 0 in (* number of new hypotheses created *) - Tacticals.try_tactics - status + ProofEngineTypes.apply_tactic + (Tacticals.try_tactics ~tactics:[ "reflexivity", EqualityTactics.reflexivity_tac ; "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ; @@ -483,15 +492,17 @@ let ring_tac status = ] ; t1'_eq_t1'' ]) ; - "elim_type eqt su t1 ...", (fun status -> + "elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status -> let status' = (* status after 1st elim_type use *) let context = context_of_status status in if not (are_convertible context t1'' t1) then begin warn "t1'' and t1 are NOT CONVERTIBLE"; let newstatus = - elim_type2_tac (* 1st elim_type use *) - status ~proof:t1'_eq_t1'' - ~term:(Cic.Appl [eqt; r; t1''; t1]) + ProofEngineTypes.apply_tactic + (elim_type2_tac (* 1st elim_type use *) + ~proof:t1'_eq_t1'' + ~term:(Cic.Appl [eqt; r; t1''; t1])) + status in incr new_hyps; (* elim_type add an hyp *) match newstatus with @@ -506,8 +517,8 @@ let ring_tac status = lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'') in let status'' = - Tacticals.try_tactics (* try to solve 1st subgoal *) - status' + ProofEngineTypes.apply_tactic + (Tacticals.try_tactics (* try to solve 1st subgoal *) ~tactics:[ "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2''; "exact sym_eqt su t2 ...", @@ -521,15 +532,18 @@ let ring_tac status = ] ; t2'_eq_t2'' ]) ; - "elim_type eqt su t2 ...", (fun status -> + "elim_type eqt su t2 ...", + ProofEngineTypes.mk_tactic (fun status -> let status' = let context = context_of_status status in if not (are_convertible context t2'' t2) then begin warn "t2'' and t2 are NOT CONVERTIBLE"; let newstatus = - elim_type2_tac (* 2nd elim_type use *) - status ~proof:t2'_eq_t2'' - ~term:(Cic.Appl [eqt; r; t2''; t2]) + ProofEngineTypes.apply_tactic + (elim_type2_tac (* 2nd elim_type use *) + ~proof:t2'_eq_t2'' + ~term:(Cic.Appl [eqt; r; t2''; t2])) + status in incr new_hyps; (* elim_type add an hyp *) match newstatus with @@ -542,12 +556,16 @@ let ring_tac status = in try (* try to solve main goal *) warn "trying reflexivity ...."; - EqualityTactics.reflexivity_tac status' + ProofEngineTypes.apply_tactic + EqualityTactics.reflexivity_tac status' with (Fail _) -> (* leave conclusion to the user *) warn "reflexivity failed, solution's left as an ex :-)"; - purge_hyps_tac ~count:!new_hyps status')] + ProofEngineTypes.apply_tactic + (purge_hyps_tac ~count:!new_hyps) status')]) + status' in - status'')] + status'')]) + status with (Fail s) -> raise (Fail ("Ring failure: " ^ s)) end @@ -555,9 +573,12 @@ let ring_tac status = assert false (* wrap ring_tac catching GoalUnringable and raising Fail *) + let ring_tac status = try ring_tac status with GoalUnringable -> raise (Fail "goal unringable") +let ring_tac = ProofEngineTypes.mk_tactic ring_tac +