From fc8f251f8a471249ac6a296c079ccfeb0b535862 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 19 Jul 2007 17:54:40 +0000
Subject: [PATCH] Convertibility now converts machines in place of terms.
 Actually, the heads of the machines (i.e. everything but the stack) are still
 unwinded and converted as terms. Thus there is much space for improvement.

---
 components/cic_proof_checking/cicReduction.ml | 40 ++++++++++++++++++-
 1 file changed, 39 insertions(+), 1 deletion(-)

diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml
index af5564d07..7f1ec5835 100644
--- a/components/cic_proof_checking/cicReduction.ml
+++ b/components/cic_proof_checking/cicReduction.ml
@@ -796,9 +796,10 @@ module R = Reduction
 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
 *)
 (*module R = Reduction(CallByValueByNameForUnwind);;*)
-module R = Reduction(CallByValueByNameForUnwind');;
+module RS = CallByValueByNameForUnwind';;
 (*module R = Reduction(CallByNameStrategy);;*)
 (*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*)
+module R = Reduction(RS);;
 module U = UriManager;;
 
 let whd = R.whd
@@ -1067,11 +1068,48 @@ begin
    (* heuristic := false; *)
    debug t1 [t2] "PREWHD";
 (*prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);*)
+(*
+prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);
    let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in
    let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
     debug t1' [t2'] "POSTWHD";
+*)
+let rec convert_machines ugraph =
+ function
+    [] -> true,ugraph
+  | ((k1,env1,ens1,h1,s1),(k2,env2,ens2,h2,s2))::tl ->
+     let (b,ugraph) as res =
+      aux2 test_equality_only
+       (R.unwind (k1,env1,ens1,h1,[])) (R.unwind (k2,env2,ens2,h2,[])) ugraph
+     in
+      if b then
+       let problems =
+        try
+         Some
+          (List.combine
+            (List.map
+              (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si))
+              s1)
+            (List.map
+              (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si))
+              s2)
+          @ tl)
+        with
+         Invalid_argument _ -> None
+       in
+        match problems with
+           None -> false,ugraph
+         | Some problems -> convert_machines ugraph problems
+      else
+       res
+in
+ convert_machines ugraph
+  [R.reduce ~delta:true ~subst context (0,[],[],t1,[]),
+   R.reduce ~delta:true ~subst context (0,[],[],t2,[])]
 (*prerr_endline ("POSTWH: " ^ CicPp.ppterm t1' ^ " <===> " ^ CicPp.ppterm t2');*)
+(*
     aux2 test_equality_only t1' t2' ugraph
+*)
 end
  in
   aux false (*c t1 t2 ugraph *)
-- 
2.39.2