From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 20 Jul 2007 14:48:36 +0000 (+0000)
Subject: acic_procedural: bug fix:
X-Git-Tag: make_still_working~6145
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=58c0db9bcf83591115445a538bee028d3260fdf7;p=helm.git

acic_procedural: bug fix:
                 sometimes whd is not enough, we need normalize ...
---

diff --git a/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml
index 489feb4b6..4c0014d2e 100644
--- a/helm/software/components/acic_procedural/proceduralClassify.ml
+++ b/helm/software/components/acic_procedural/proceduralClassify.ml
@@ -78,7 +78,7 @@ let classify_conclusion vs =
  
 let classify c t =
 try   
-   let vs, h = PEH.split_with_whd (c, t) in
+   let vs, h = PEH.split_with_normalize (c, t) in
    let rc = classify_conclusion vs in
    let map (b, h) (c, v) = 
       let _, argsno = PEH.split_with_whd (c, v) in
diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml
index 85dba95ea..ec2e1919c 100644
--- a/helm/software/components/tactics/proofEngineHelpers.ml
+++ b/helm/software/components/tactics/proofEngineHelpers.ml
@@ -652,6 +652,13 @@ let split_with_whd (c, t) =
     in
     aux false [] 0 c t
 
+let split_with_normalize (c, t) =
+   let add s v c = Some (s, Cic.Decl v) :: c in
+   let rec aux a n c = function
+      | Cic.Prod (s, v, t)  -> aux ((c, v) :: a) (succ n) (add s v c) t
+      | v                   -> (c, v) :: a, n
+    in
+    aux [] 0 c (CicReduction.normalize c t)
 
   (* menv sorting *)
 module OT = 
diff --git a/helm/software/components/tactics/proofEngineHelpers.mli b/helm/software/components/tactics/proofEngineHelpers.mli
index 1eeb0aca3..39fb69b0d 100644
--- a/helm/software/components/tactics/proofEngineHelpers.mli
+++ b/helm/software/components/tactics/proofEngineHelpers.mli
@@ -121,6 +121,10 @@ val get_rel: Cic.context -> string -> Cic.term option
    t and t_i is the premise of t accessed by Rel i in t_0. 
    Performes a whd on the conclusion before giving up.
    Each t_i is returned with a context c_i in wich it is typed
+   split_with_normalize (c, t) normalizes t before operating the split
+   whd is useless here
 *)
 val split_with_whd: Cic.context * Cic.term -> 
                     (Cic.context * Cic.term) list * int
+val split_with_normalize: Cic.context * Cic.term -> 
+                          (Cic.context * Cic.term) list * int