New tactic unfold.

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

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 8a6ef81a277658d5e7cda8055768a925b7b3e574..a9b8b55001a47c5ee3390b9556c90f1c4ec642c8 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -874,3 +874,78 @@ let simpl context =
  in
   reduceaux context []
 ;;
+
+let unfold ?what context where =
+ let first_is_the_expandable_head_of_second t1 t2 =
+  match t1,t2 with
+     Cic.Const (uri,_), Cic.Const (uri',_)
+   | Cic.Var (uri,_), Cic.Var (uri',_)
+   | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_)
+   | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
+   | Cic.Const _, _
+   | Cic.Var _, _ -> false
+   | _,_ ->
+     raise
+      (ProofEngineTypes.Fail
+        "The term to unfold is neither a constant nor a variable")
+ in
+ let appl he tl =
+  if tl = [] then he else Cic.Appl (he::tl) in
+ let cannot_delta_expand t =
+  raise
+   (ProofEngineTypes.Fail
+     ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded")) in
+ let rec hd_delta_beta context tl =
+  function
+    Cic.Rel n as t ->
+     (try
+       match List.nth context (n-1) with
+          Some (_,Cic.Decl _) -> cannot_delta_expand t
+        | Some (_,Cic.Def (bo,_)) ->
+           CicReduction.head_beta_reduce
+            (appl (CicSubstitution.lift n bo) tl)
+        | None -> raise RelToHiddenHypothesis
+      with
+         Failure _ -> assert false)
+  | Cic.Const (uri,exp_named_subst) as t ->
+     let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+      (match o with
+          Cic.Constant (_,Some body,_,_,_) ->
+           CicReduction.head_beta_reduce
+            (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
+        | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t
+        | Cic.Variable _ -> raise ReferenceToVariable
+        | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
+        | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+      )
+  | Cic.Var (uri,exp_named_subst) as t ->
+     let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+      (match o with
+          Cic.Constant _ -> raise ReferenceToConstant
+        | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
+        | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+        | Cic.Variable (_,Some body,_,_,_) ->
+           CicReduction.head_beta_reduce
+            (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
+        | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t
+      )
+   | Cic.Appl [] -> assert false
+   | Cic.Appl (he::tl) -> hd_delta_beta context tl he
+   | t -> cannot_delta_expand t
+ in
+ let context, where =
+  match what with
+     None -> context, where
+   | Some what ->
+      try
+       ProofEngineHelpers.locate_in_term
+        ~equality:first_is_the_expandable_head_of_second
+        what ~where context
+      with
+       ProofEngineHelpers.TermNotFound ->
+        raise
+         (ProofEngineTypes.Fail
+           ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))
+ in
+  hd_delta_beta context [] where
+;;