1. change_tac moved from PrimitiveTactics to ReductionTactics

[helm.git] / helm / ocaml / tactics / primitiveTactics.ml

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 8766a044a576ead6f30826bc899dcd28b1999b72..3fefc662a5bcb7915e83ffb70bb9df4ea44a3bfd 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -589,92 +589,3 @@ let elim_intros_simpl_tac ~term =
        [ReductionTactics.simpl_tac
          ~pattern:(ProofEngineTypes.conclusion_pattern None)])
 ;;
-
-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
-          let _,u =
-           CicTypeChecker.type_of_aux' metasenv context_of_t with_what
-            CicUniv.empty_ugraph in
-          let b,_ =
-           CicReduction.are_convertible ~metasenv context_of_t t with_what u in
-          if b then
-           t, with_what_in_context_of_t
-          else
-           raise NotConvertible) 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)