(* Note: this code is almost identical to change_tac and
* it could be unified by making the change function a callback *)
let reduction_tac ~reduction ~pattern (proof,goal) =
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let change subst where terms metasenv ugraph =
if terms = [] then where, metasenv, ugraph
| _ as t -> t
) metasenv
in
- (curi,metasenv',pbo,pty, attrs), [metano]
+ (curi,metasenv',_subst,pbo,pty, attrs), [metano]
;;
let simpl_tac ~pattern =
mk_tactic (reduction_tac
~reduction:(const_lazy_reduction CicReduction.normalize) ~pattern)
+let head_beta_reduce_tac ?delta ?upto ~pattern =
+ mk_tactic (reduction_tac
+ ~reduction:
+ (const_lazy_reduction
+ (fun _context -> CicReduction.head_beta_reduce ?delta ?upto)) ~pattern)
+
exception NotConvertible
(* Note: this code is almost identical to reduction_tac and
reference variables that are local to the term that is going to be
replaced. To fix this we should parse with_what in the context of the
term(s) to be replaced. *)
-let change_tac ~pattern with_what =
+let change_tac ?(with_cast=false) ~pattern with_what =
let change_tac ~pattern ~with_what (proof, goal) =
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let change subst where terms metasenv ugraph =
if terms = [] then where, metasenv, ugraph
| _ as t -> t)
metasenv
in
- (curi,metasenv',pbo,pty, attrs), [metano]
+ let proof,goal = (curi,metasenv',_subst,pbo,pty, attrs), metano in
+ if with_cast then
+ let metano' = ProofEngineHelpers.new_meta_of_proof ~proof in
+ let (newproof,_) =
+ let irl= CicMkImplicit.identity_relocation_list_for_metavariable context'
+ in
+ ProofEngineHelpers.subst_meta_in_proof
+ proof metano
+ (Cic.Cast (Cic.Meta(metano',irl),ty')) [metano',context',ty']
+ in
+ newproof, [metano']
+ else
+ proof,[goal]
in
mk_tactic (change_tac ~pattern ~with_what)