* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
(******************** THE FOURIER TACTIC ***********************)
*)
let fails f a =
try
- let tmp = (f a) in
- false
+ ignore (f a);
+ false
with
_-> true
;;
apply_tactic (PrimitiveTactics.apply_tac ~term:_Rnot_lt0) status
else
apply_tactic (Tacticals.then_
- ~start:( mk_tactic (fun status ->
- let (proof, goal) = status in
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt) status))
+ ~start:(mk_tactic (apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt)))
~continuation:(tac_zero_infeq_pos gl (-n,d)))
status
in
apply_tactic
(Tacticals.then_
~start:
- (ReductionTactics.fold_tac ~reduction:CicReduction.whd
- ~pattern:
- (ProofEngineTypes.conclusion_pattern
- (Some
- (Cic.Appl
- [_Rle ; _R0 ;
- Cic.Appl
- [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
- ]
- )))
- )
+ (ReductionTactics.fold_tac
+ ~reduction:(const_lazy_reduction CicReduction.whd)
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)
+ ~term:
+ (const_lazy_term
+ (Cic.Appl
+ [_Rle ; _R0 ;
+ Cic.Appl
+ [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]])))
~continuation:
(Tacticals.then_
~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
- ~continuation:(tac_zero_inf_pos (-n,d))))
+ ~continuation:(tac_zero_inf_pos (-n,d))))
status
in
mk_tactic (tac_zero_infeq_false gl (n,d))
let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
let (proof,goals) = apply_tactic
- (EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) ())
+ (EqualityTactics.rewrite_simpl_tac
+ ~direction:`LeftToRight
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)
+ (C.Meta (fresh_meta,irl)))
((curi,metasenv',pbo,pty),goal)
in
let new_goals = fresh_meta::goals in
let tcl_fail a (proof,goal) =
match a with
- 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
+ 1 -> raise (ProofEngineTypes.Fail (lazy "fail-tactical"))
| _ -> (proof,[goal])
;;
)
context
in
- Tacticals.try_tactics ~tactics:tac_list (proof,goal)
+ Tacticals.first ~tactics:tac_list (proof,goal)
;;
*)
(* Galla: moved in negationTactics.ml
debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n");
debug_pcontext s_context;
- let fhyp = String.copy "new_hyp_for_fourier" in
-
(* here we need to negate the thesis, but to do this we need to apply the
right theoreme,so let's parse our thesis *)
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
apply_tactic
- (PrimitiveTactics.change_tac
+ (ReductionTactics.change_tac
~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
- (Cic.Appl [ _not; ineq]))
+ (const_lazy_term (Cic.Appl [ _not; ineq])))
status))
~continuation:(Tacticals.then_
~start:(PrimitiveTactics.apply_tac ~term:
r))
~continuations:
[PrimitiveTactics.apply_tac ~term:_Rinv_R1;
- Tacticals.try_tactics
+ Tacticals.first
~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac]
])
;(*Tacticals.id_tac*)
|_ -> assert false)
in
let r = apply_tactic
- (PrimitiveTactics.change_tac
+ (ReductionTactics.change_tac
~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
- w1) status
+ (const_lazy_term w1)) status
in
debug("fine MY_CHNGE\n");
r))