From a484672e530900bb3b3aa02f9fff5fedd9fb06a4 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 Mar 2006 16:26:32 +0000
Subject: [PATCH] Huge speed-up in conversion: the old conversion strategy is
 set back.  1. try to "convert" the two terms recursively without performing
 reduction  2. if it fails, do a whd and try again The overall result on the
 library of Coq is really remarkable.

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

diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml
index 0bc05674b..bd8d07b8d 100644
--- a/components/cic_proof_checking/cicReduction.ml
+++ b/components/cic_proof_checking/cicReduction.ml
@@ -107,6 +107,7 @@ module CallByValueByNameForUnwind =
 ;;
 
 
+(* Old Machine
 module CallByNameStrategy =
  struct
   type stack_term = Cic.term
@@ -126,6 +127,28 @@ module CallByNameStrategy =
   let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
  end
 ;;
+*)
+
+module CallByNameStrategy =
+ struct
+  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
+  and stack_term = config
+  and env_term = config
+  and ens_term = config
+
+  let to_env c = c
+  let to_ens c = c
+  let from_stack config = config
+  let from_stack_list_for_unwind ~unwind l = List.map unwind l
+  let from_env c = c
+  let from_ens c = c
+  let from_env_for_unwind ~unwind c = unwind c
+  let from_ens_for_unwind ~unwind c = unwind c
+  let stack_to_env ~reduce ~unwind config = 0,[],[],unwind config,[]
+  let compute_to_env ~reduce ~unwind k e ens t = k,e,ens,t,[]
+  let compute_to_stack ~reduce ~unwind config = config
+ end
+;;
 
 module CallByValueStrategy =
  struct
@@ -747,6 +770,7 @@ module R = Reduction
 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
 *)
 module R = Reduction(CallByValueByNameForUnwind);;
+(*module R = Reduction(CallByNameStrategy);;*)
 (*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*)
 module U = UriManager;;
 
@@ -766,6 +790,7 @@ let (===) x y =
 
 (* t1, t2 must be well-typed *)
 let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
+ let heuristic = ref true in
  let rec aux test_equality_only context t1 t2 ugraph =
   let aux2 test_equality_only t1 t2 ugraph =
 
@@ -811,6 +836,26 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
                 if b2 then true,ugraph1 else false,ugraph 
             else
               false,ugraph
+        | C.Meta (n1,l1), _ ->
+           (try 
+              let _,term,_ = CicUtil.lookup_subst n1 subst in
+              let term' = CicSubstitution.subst_meta l1 term in
+(*
+prerr_endline ("%?: " ^ CicPp.ppterm t1 ^ " <==> " ^ CicPp.ppterm t2);
+prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t2);
+*)
+               aux test_equality_only context term' t2 ugraph
+            with  CicUtil.Subst_not_found _ -> false,ugraph)
+        | _, C.Meta (n2,l2) ->
+           (try 
+              let _,term,_ = CicUtil.lookup_subst n2 subst in
+              let term' = CicSubstitution.subst_meta l2 term in
+(*
+prerr_endline ("%?: " ^ CicPp.ppterm t1 ^ " <==> " ^ CicPp.ppterm t2);
+prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
+*)
+               aux test_equality_only context t1 term' ugraph
+            with  CicUtil.Subst_not_found _ -> false,ugraph)
           (* TASSI: CONSTRAINTS *)
         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
             true,(CicUniv.add_eq t2 t1 ugraph)
@@ -968,11 +1013,26 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
         | (_,_) -> false,ugraph
     end
   in
+   let res =
+    if !heuristic then
+     aux2 test_equality_only t1 t2 ugraph
+    else
+     false,ugraph
+   in
+    if fst res = true then
+     res
+    else
+begin
+(*if !heuristic then prerr_endline ("NON FACILE: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);*)
+   (* heuristic := false; *)
    debug t1 [t2] "PREWHD";
+(*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";
+(*prerr_endline ("POSTWH: " ^ CicPp.ppterm t1' ^ " <===> " ^ CicPp.ppterm t2');*)
     aux2 test_equality_only t1' t2' ugraph
+end
  in
   aux false (*c t1 t2 ugraph *)
 ;;
@@ -1073,7 +1133,7 @@ let rec head_beta_reduce =
   | Cic.Cast (te,_) -> head_beta_reduce te
   | t -> t
 
-(*Debugging code
+(*
 let are_convertible ?subst ?metasenv context t1 t2 ugraph =
  let before = Unix.gettimeofday () in
  let res = are_convertible ?subst ?metasenv context t1 t2 ugraph in
-- 
2.39.2