since the outtype is now refined correclty some types can be opmitted

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

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 087d327757babbe020e167c8babd40821bdaf3b5..fc3bfd3b8a66991101daa4dd029d07b039565171 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -601,6 +601,14 @@ exception AlreadySimplified;;
 (*CSC: It does not perform simplification in a Case *)
 
 let simpl context =
+ let mk_appl t l =
+   if l = [] then 
+     t 
+   else 
+     match t with
+     | Cic.Appl l' -> Cic.Appl (l'@l)
+     | _ -> Cic.Appl (t::l)
+ in
  (* reduceaux is equal to the reduceaux locally defined inside *)
  (* reduce, but for the const case.                            *) 
  (**** Step 1 ****)
@@ -614,8 +622,7 @@ let simpl context =
             Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
           | Some (_,C.Def (bo,_)) ->
              let lifted_bo = S.lift n bo in
-             let applied_lifted_bo =
-              if l = [] then lifted_bo else C.Appl (lifted_bo::l) in
+             let applied_lifted_bo = mk_appl lifted_bo l in
              let simplified = try_delta_expansion context l t lifted_bo in
               if simplified = applied_lifted_bo then
                if l = [] then t else C.Appl (t::l)
@@ -886,7 +893,8 @@ let simpl context =
 ;;
 
 let unfold ?what context where =
- let first_is_the_expandable_head_of_second t1 t2 =
+ let contextlen = List.length context in
+ let first_is_the_expandable_head_of_second context' t1 t2 =
   match t1,t2 with
      Cic.Const (uri,_), Cic.Const (uri',_)
    | Cic.Var (uri,_), Cic.Var (uri',_)
@@ -894,17 +902,21 @@ let unfold ?what context where =
    | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
    | Cic.Const _, _
    | Cic.Var _, _ -> false
+   | Cic.Rel n, Cic.Rel m
+   | Cic.Rel n, Cic.Appl (Cic.Rel m::_) ->
+      n + (List.length context' - contextlen) = m
+   | Cic.Rel _, _ -> false
    | _,_ ->
      raise
       (ProofEngineTypes.Fail
-        "The term to unfold is neither a constant nor a variable")
+        (lazy "The term to unfold is not a constant, a variable or a bound 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
+     (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in
  let rec hd_delta_beta context tl =
   function
     Cic.Rel n as t ->
@@ -955,7 +967,7 @@ let unfold ?what context where =
        if res = [] then
         raise
          (ProofEngineTypes.Fail
-           ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))
+           (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)))
        else
         res
  in