@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
(**
@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 =
| (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
let proof',goal' = aux count context status in
assert (goal = goal') ;
proof',[goal']
+ in
+ ProofEngineTypes.mk_tactic (purge_hyps_tac ~count)
(** THE TACTIC! *)
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";
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'' ;
] ;
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
+ 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";
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
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 ...",
] ;
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
+ let b,_ = (* TASSI:FIXME *)
+ are_convertible context t2'' t2 CicUniv.empty_ugraph
+ in
+ if not b 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
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
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
+