change code moved to change_tac (functional version defined in primitiveTactics)

diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml
index 75f421cede4ec24c666700a69a1316d56fbdd818..bf65d1a7b2257e3c8da526e6492e410b8a1f276d 100644 (file)
--- a/helm/gTopLevel/primitiveTactics.ml
+++ b/helm/gTopLevel/primitiveTactics.ml
@@ -477,3 +477,41 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*)
                     in
                      (newproof,
                       List.map (function (i,_,_) -> i) new_uninstantiatedmetas)
+
+
+exception NotConvertible
+
+(*CSC: Bug (or feature?). [with_what] is parsed in the context of the goal,  *)
+(*CSC: while [what] can have a richer context (because of binders)           *)
+(*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *)
+(*CSC: Is that evident? Is that right? Or should it be changed?              *)
+let change_tac ~what ~with_what ~status:(proof, goal) =
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  (* are_convertible works only on well-typed terms *)
+  ignore (CicTypeChecker.type_of_aux' metasenv context with_what) ;
+  if CicReduction.are_convertible context what with_what then
+   begin
+    let replace =
+     ProofEngineReduction.replace ~equality:(==) ~what ~with_what
+    in
+    let ty' = replace ty in
+    let context' =
+     List.map
+      (function
+          Some (name,Cic.Def  t) -> Some (name,Cic.Def  (replace t))
+        | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
+        | None -> None
+      ) context
+    in
+     let metasenv' = 
+      List.map
+       (function
+           (n,_,_) when n = metano -> (metano,context',ty')
+         | _ as t -> t
+       ) metasenv
+     in
+      (curi,metasenv',pbo,pty), [metano]
+   end
+  else
+   raise (ProofEngineTypes.Fail "Not convertible")

diff --git a/helm/gTopLevel/primitiveTactics.mli b/helm/gTopLevel/primitiveTactics.mli
index 123b3859df099adad8c26ce7ca1af9286c442edd..93db3ea10f8c95bc15fa5f320499bb11ab7904d7 100644 (file)
--- a/helm/gTopLevel/primitiveTactics.mli
+++ b/helm/gTopLevel/primitiveTactics.mli
@@ -1,3 +1,28 @@
+(* Copyright (C) 2002, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
 val apply_tac:
   term: Cic.term -> ProofEngineTypes.tactic
 val exact_tac:
@@ -11,3 +36,6 @@ val letin_tac:
 
 val elim_intros_simpl_tac:
   term: Cic.term -> ProofEngineTypes.tactic 
+
+val change_tac:
+  what: Cic.term -> with_what: Cic.term -> ProofEngineTypes.tactic 

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 69e8062eeddd17f10c667c7634c60f26c31b78bb..0e4de4f3bc1d639cadd821eaff0b535f5a1add99 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -246,53 +246,6 @@ let fold term =
       proof := Some (curi,metasenv',pbo,pty) ;
       goal := Some metano
 
-exception NotConvertible
-
-(*CSC: Bug (or feature?). [input] is parsed in the context of the goal,  *)
-(*CSC: while [goal_input] can have a richer context (because of binders) *)
-(*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
-(*CSC: Is that evident? Is that right? Or should it be changed?          *)
-let change ~goal_input ~input =
- let curi,metasenv,pbo,pty =
-  match !proof with
-     None -> assert false
-   | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
- let metano,context,ty =
-  match !goal with
-     None -> assert false
-   | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
-  (* are_convertible works only on well-typed terms *)
-  ignore (CicTypeChecker.type_of_aux' metasenv context input) ;
-  if CicReduction.are_convertible context goal_input input then
-   begin
-    let replace =
-     ProofEngineReduction.replace
-      ~equality:(==) ~what:goal_input ~with_what:input
-    in
-    let ty' = replace ty in
-    let context' =
-     List.map
-      (function
-          Some (name,Cic.Def  t) -> Some (name,Cic.Def  (replace t))
-        | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
-        | None -> None
-      ) context
-    in
-     let metasenv' = 
-      List.map
-       (function
-           (n,_,_) when n = metano -> (metano,context',ty')
-         | _ as t -> t
-       ) metasenv
-     in
-      proof := Some (curi,metasenv',pbo,pty) ;
-      goal := Some metano
-   end
-  else
-   raise NotConvertible
-
 (************************************************************)
 (*              Tactics defined elsewhere                   *)
 (************************************************************)
@@ -307,6 +260,8 @@ let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term)
 let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)
 let elim_intros_simpl term =
   apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term)
+let change ~goal_input:what ~input:with_what =
+  apply_tactic (PrimitiveTactics.change_tac ~what ~with_what)
 
   (* structural tactics *)
 

diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli
index f9233ea05a83a2f1b2b4100999098cc94b058285..fed8d04ad7598a6689625c3acf740a0f3373c55b 100644 (file)
--- a/helm/gTopLevel/proofEngine.mli
+++ b/helm/gTopLevel/proofEngine.mli
@@ -23,8 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception NotConvertible
-
   (* proof engine status *)
 val proof : ProofEngineTypes.proof option ref
 val goal : ProofEngineTypes.goal option ref
@@ -37,7 +35,6 @@ val whd : Cic.term -> unit
 val reduce : Cic.term -> unit
 val simpl : Cic.term -> unit
 val fold : Cic.term -> unit
-val change : goal_input:Cic.term -> input:Cic.term -> unit
 
   (* scratch area reduction tactics *)
 val whd_in_scratch : Cic.term -> Cic.term -> Cic.term
@@ -51,6 +48,7 @@ val cut : Cic.term -> unit
 val letin : Cic.term -> unit
 val exact : Cic.term -> unit
 val elim_intros_simpl : Cic.term -> unit
+val change : goal_input:Cic.term -> input:Cic.term -> unit
 
   (* structural tactics *)
 val clearbody : Cic.hypothesis -> unit