From f3d3702d9dae5012484ec7b9afe35c56be73ca5d Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 16 Apr 2002 09:34:07 +0000
Subject: [PATCH] * Bug fixed: applications of MutCase that are not
 iota-redexes were reduced   just to their head. * More debugging enabled (to
 be removed when code becomes stable)

---
 .../cic_proof_checking/cicReductionNaif.ml    | 30 +++++++++++--------
 1 file changed, 17 insertions(+), 13 deletions(-)

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index e0ad91f59..b4296f1c1 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -88,7 +88,7 @@ let whd =
     | C.Abst _ as t -> t (*CSC l should be empty ????? *)
     | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
-    | C.MutCase (mutind,cookingsno,i,_,term,pl) as t ->
+    | C.MutCase (mutind,cookingsno,i,_,term,pl) as t->
        let decofix =
         function
            C.CoFix (i,fl) as t ->
@@ -142,7 +142,7 @@ let whd =
                whdaux (ts@l) (List.nth pl (j-1))
          | C.Abst _| C.Cast _ | C.Implicit ->
             raise (Impossible 2) (* we don't trust our whd ;-) *)
-         | _ -> t
+         | _ -> if l = [] then t else C.Appl (t::l)
        )
     | C.Fix (i,fl) as t ->
        let (_,recindex,_,body) = List.nth fl i in
@@ -188,10 +188,10 @@ let whd =
 ;;
 
 (* t1, t2 must be well-typed *)
-let are_convertible t1 t2 =
+let are_convertible =
  let module U = UriManager in
  let rec aux t1 t2 =
-  debug t1 [t2] "PREWHD";
+ let aux2 t1 t2 =
   (* this trivial euristic cuts down the total time of about five times ;-) *)
   (* this because most of the time t1 and t2 are "sintactically" the same   *)
   if t1 = t2 then
@@ -199,11 +199,7 @@ let are_convertible t1 t2 =
   else
    begin
     let module C = Cic in
-     let t1' = whd t1 
-     and t2' = whd t2 in
-     debug t1' [t2'] "POSTWHD";
-     (*if !fdebug = 0 then ignore(Unix.system "read" );*)
-      match (t1',t2') with
+      match (t1,t2) with
          (C.Rel n1, C.Rel n2) -> n1 = n2
        | (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2
        | (C.Meta n1, C.Meta n2) -> n1 = n2
@@ -259,10 +255,18 @@ let are_convertible t1 t2 =
        | (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _)
        | (C.Implicit, _) | (_, C.Implicit) ->
           raise (Impossible 3) (* we don't trust our whd ;-) *)
-       | (_,_) ->
-          debug t1' [t2'] "NOT-CONVERTIBLE" ;
-          false
+       | (_,_) -> false
+   end
+ in
+  if aux2 t1 t2 then true
+  else
+   begin
+    debug t1 [t2] "PREWHD";
+    let t1' = whd t1 
+    and t2' = whd t2 in
+     debug t1' [t2'] "POSTWHD";
+     aux2 t1' t2'
    end
  in
-  aux t1 t2
+  aux
 ;;
-- 
2.39.2