Initial revision

[helm.git] / helm / gTopLevel / primitiveTactics.ml

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")