-
-exception NotConvertible
-
-(* Note: this code is almost identical to ReductionTactics.reduction_tac and
-* it could be unified by making the change function a callback *)
-(* CSC: with_what is parsed in the context of the goal, but it should replace
- something that lives in a completely different context. Thus we
- perform a delift + lift phase to move it in the right context. However,
- in this way the tactic is less powerful than expected: with_what cannot
- 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 ~pattern ~with_what (proof, goal) =
- let curi,metasenv,pbo,pty = proof in
- let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
- let context_len = List.length context in
- let change context'_len where terms =
- if terms = [] then where
- else
- let terms, terms' =
- List.split
- (List.map
- (fun (context_of_t, t) ->
- let context_of_t_len = List.length context_of_t in
- let with_what_in_context' =
- if context_len > context'_len then
- begin
- let with_what,subst,metasenv' =
- CicMetaSubst.delift_rels [] metasenv
- (context_len - context'_len) with_what
- in
- assert (subst = []);
- assert (metasenv = metasenv');
- with_what
- end
- else
- with_what in
- let with_what_in_context_of_t =
- if context_of_t_len > context'_len then
- CicSubstitution.lift (context_of_t_len - context'_len)
- with_what_in_context'
- else
- with_what
- in
- t, with_what_in_context_of_t) terms)
- in
- ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
- ~where:where in
- let (selected_context,selected_ty) =
- ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
- let ty' = change context_len ty selected_ty in
- let context' =
- List.fold_right2
- (fun entry selected_entry context' ->
- let context'_len = List.length context' in
- match entry,selected_entry with
- None,None -> None::context'
- | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
- let ty' = change context'_len ty selected_ty in
- Some (name,Cic.Decl ty')::context'
- | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
- let bo' = change context'_len bo selected_bo in
- let ty' =
- match ty,selected_ty with
- None,None -> None
- | Some ty,Some selected_ty ->
- Some (change context'_len ty selected_ty)
- | _,_ -> assert false
- in
- Some (name,Cic.Def (bo',ty'))::context'
- | _,_ -> assert false
- ) context selected_context [] in
- let metasenv' =
- List.map (function
- | (n,_,_) when n = metano -> (metano,context',ty')
- | _ as t -> t
- ) metasenv
- in
- (curi,metasenv',pbo,pty), [metano]
- in
- mk_tactic (change_tac ~pattern ~with_what)