better precedence handling, should remove useless parens

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

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index a9b8b55001a47c5ee3390b9556c90f1c4ec642c8..f8782b7aec13db70083d025a44258d1416d0cf21 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)
@@ -583,8 +583,11 @@ exception AlreadySimplified;;
 
 (* Takes a well-typed term and                                               *)
 (*  1) Performs beta-iota-zeta reduction until delta reduction is needed     *)
+(*     Zeta-reduction is performed if and only if the simplified form of its *)
+(*     definiendum (applied to the actual arguments) is different from the   *)
+(*      non-simplified form.                                                 *)
 (*  2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted  *)
-(*     w.r.t. zero or more variables and if the Fix can be reductaed, than it  *)
+(*     w.r.t. zero or more variables and if the Fix can be reductaed, than it*)
 (*     is reduced, the delta-reduction is succesfull and the whole algorithm *)
 (*     is applied again to the new redex; Step 3) is applied to the result   *)
 (*     of the recursive simplification. Otherwise, if the Fix can not be     *)
@@ -598,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 ****)
@@ -610,7 +621,13 @@ let simpl context =
          match List.nth context (n-1) with
             Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
           | Some (_,C.Def (bo,_)) ->
-             try_delta_expansion context l t (S.lift n bo)
+             let lifted_bo = S.lift n bo 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)
+              else
+               simplified
          | None -> raise RelToHiddenHypothesis
         with
          Failure _ -> assert false)
@@ -714,7 +731,7 @@ let simpl context =
                 reduceaux context tl body'
          | t -> t
        in
-        (match decofix (reduceaux context [] term) with
+        (match decofix (CicReduction.whd context term) with
             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
              let (arity, r) =
@@ -876,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',_)
@@ -884,10 +902,14 @@ 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")
+        "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
@@ -933,19 +955,26 @@ let unfold ?what context where =
    | Cic.Appl (he::tl) -> hd_delta_beta context tl he
    | t -> cannot_delta_expand t
  in
- let context, where =
+ let context_and_matched_term_list =
   match what with
-     None -> context, where
+     None -> [context, where]
    | Some what ->
-      try
+      let res =
        ProofEngineHelpers.locate_in_term
         ~equality:first_is_the_expandable_head_of_second
         what ~where context
-      with
-       ProofEngineHelpers.TermNotFound ->
+      in
+       if res = [] then
         raise
          (ProofEngineTypes.Fail
            ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))
+       else
+        res
  in
-  hd_delta_beta context [] where
+  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
 ;;