This test stresses automatic insertion.

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

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 8a6ef81a277658d5e7cda8055768a925b7b3e574..d04acd181ba2c7c621b00ec2f479f2089aaafebe 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -127,7 +127,7 @@ let replace ~equality ~what ~with_what ~where =
     function
        [],[] -> raise Not_found
      | what::tl1,with_what::tl2 ->
-        if equality t what then with_what else find_image_aux (tl1,tl2)
+        if equality what t then with_what else find_image_aux (tl1,tl2)
      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
    in
     find_image_aux (what,with_what)
@@ -190,7 +190,7 @@ let replace_lifting ~equality ~what ~with_what ~where =
     function
        [],[] -> raise Not_found
      | what::tl1,with_what::tl2 ->
-        if equality t what then with_what else find_image_aux (tl1,tl2)
+        if equality what t then with_what else find_image_aux (tl1,tl2)
      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
    in
     find_image_aux (what,with_what)
@@ -288,7 +288,7 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
     function
        [],[] -> raise Not_found
      | what::tl1,with_what::tl2 ->
-        if equality t what then with_what else find_image_aux (tl1,tl2)
+        if equality what t then with_what else find_image_aux (tl1,tl2)
      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
    in
     find_image_aux (what,with_what)
@@ -874,3 +874,85 @@ 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_and_matched_term_list =
+  match what with
+     None -> [context, where]
+   | Some what ->
+      let res =
+       ProofEngineHelpers.locate_in_term
+        ~equality:first_is_the_expandable_head_of_second
+        what ~where context
+      in
+       if res = [] then
+        raise
+         (ProofEngineTypes.Fail
+           ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))
+       else
+        res
+ in
+  let reduced_terms =
+   List.map
+    (function (context,where) -> hd_delta_beta context [] where)
+    context_and_matched_term_list in
+  let whats = List.map snd context_and_matched_term_list in
+   replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where
+;;