(* 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
CicMetaSubst.apply_subst subst where', metasenv, ugraph
in
let (subst,metasenv,ugraph,selected_context,selected_ty) =
- ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+ ProofEngineHelpers.select ~subst ~metasenv ~ugraph:CicUniv.oblivion_ugraph
~conjecture ~pattern
in
let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
Some (name,Cic.Decl ty')::context', metasenv, ugraph
| Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
let bo', metasenv, ugraph =
- change subst bo selected_bo metasenv ugraph
- in
+ change subst bo selected_bo metasenv ugraph in
let ty', metasenv, ugraph =
- match ty,selected_ty with
- None,None -> None, metasenv, ugraph
- | Some ty,Some selected_ty ->
- let ty', metasenv, ugraph =
- change subst ty selected_ty metasenv ugraph
- in
- Some ty', metasenv, ugraph
- | _,_ -> assert false
+ change subst ty selected_ty metasenv ugraph
in
(Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
| _,_ -> assert false
| _ 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 ProofEngineReduction.simpl) ~pattern)
-let reduce_tac ~pattern =
- mk_tactic (reduction_tac
- ~reduction:(const_lazy_reduction ProofEngineReduction.reduce) ~pattern)
-
let unfold_tac what ~pattern =
let reduction =
match what with
| Some lazy_term ->
(fun context metasenv ugraph ->
let what, metasenv, ugraph = lazy_term context metasenv ugraph in
- ProofEngineReduction.unfold ~what, metasenv, ugraph)
+ let unfold ctx t =
+ try
+ ProofEngineReduction.unfold ~what ctx t
+ with
+ (* Not what we would like to have; however, this is required
+ right now for the case of a definition in the context:
+ if it works only in the body (or only in the type), that should
+ be accepted *)
+ ProofEngineTypes.Fail _ -> t
+ in
+ unfold, metasenv, ugraph)
in
mk_tactic (reduction_tac ~reduction ~pattern)
~reduction:(const_lazy_reduction CicReduction.normalize) ~pattern)
let head_beta_reduce_tac ?delta ?upto ~pattern =
- begin match upto with
- | Some upto ->
- HLog.warn (Printf.sprintf "inside head_beta_reduce_tac %i" upto)
- | None -> HLog.warn (Printf.sprintf "inside head_beta_reduce_tac none")
- end;
mk_tactic (reduction_tac
~reduction:
(const_lazy_reduction
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
with_what context_of_t metasenv ugraph
in
let _,u =
- CicTypeChecker.type_of_aux' metasenv context_of_t with_what ugraph
+ CicTypeChecker.type_of_aux'
+ metasenv ~subst context_of_t with_what ugraph
in
let b,_ =
- CicReduction.are_convertible ~metasenv context_of_t t with_what u
+ CicReduction.are_convertible
+ ~metasenv ~subst context_of_t t with_what u
in
if b then
((t, with_what) :: pairs), metasenv, ugraph
CicMetaSubst.apply_subst subst where', metasenv, ugraph
in
let (subst,metasenv,ugraph,selected_context,selected_ty) =
- ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture
- ~pattern in
+ ProofEngineHelpers.select
+ ~metasenv ~subst ~ugraph:CicUniv.oblivion_ugraph ~conjecture ~pattern
+ in
let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
let context', metasenv, ugraph =
List.fold_right2
(Some (name,Cic.Decl ty')::context'), metasenv, ugraph
| Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
let bo', metasenv, ugraph =
- change subst bo selected_bo metasenv ugraph
- in
+ change subst bo selected_bo metasenv ugraph in
let ty', metasenv, ugraph =
- match ty,selected_ty with
- None,None -> None, metasenv, ugraph
- | Some ty,Some selected_ty ->
- let ty', metasenv, ugraph =
- change subst ty selected_ty metasenv ugraph
- in
- Some ty', metasenv, ugraph
- | _,_ -> assert false
+ change subst ty selected_ty metasenv ugraph
in
(Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
| _,_ -> assert false
| _ 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)
+;;
let fold_tac ~reduction ~term ~pattern =
let fold_tac ~reduction ~term ~pattern:(wanted,hyps_pat,concl_pat) status =
(change_tac ~pattern:(Some reduced_term,hyps_pat,concl_pat) term) status
in
mk_tactic (fold_tac ~reduction ~term ~pattern)
+;;
projects / helm.git / blobdiff