From 64ff9332da7c8ac1ca63faeceda131362f87ea91 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 14 Oct 2009 14:38:02 +0000
Subject: [PATCH] hints were not used by reduction machines on heads

---
 .../components/ng_refiner/nCicUnification.ml  | 69 +++++++++++--------
 helm/software/matita/nlibrary/logic/pts.ma    |  2 +-
 2 files changed, 41 insertions(+), 30 deletions(-)

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index d95415d99..5a3878a2b 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -15,6 +15,9 @@ exception UnificationFailure of string Lazy.t;;
 exception Uncertain of string Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 exception KeepReducing of string Lazy.t;;
+exception KeepReducingThis of 
+  string Lazy.t * (NCicReduction.machine * bool) * 
+                  (NCicReduction.machine * bool) ;;
 
 let (===) x y = Pervasives.compare x y = 0 ;;
 
@@ -662,6 +665,29 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
         cand_iter candidates
      (*D*)  in outside true; rc with exn -> outside false; raise exn 
     in
+    let put_in_whd m1 m2 =
+      NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
+      NCicReduction.reduce_machine ~delta:max_int ~subst context m2
+    in
+    let fo_unif_w_hints test_eq_only metasenv subst (_,t1 as m1) (_,t2 as m2) =
+      try fo_unif test_eq_only metasenv subst m1 m2
+      with 
+      | UnificationFailure _ as exn -> raise exn
+      | KeepReducing _ | Uncertain _ as exn ->
+        let (t1,norm1 as tm1),(t2,norm2 as tm2) =
+         put_in_whd (0,[],t1,[]) (0,[],t2,[])
+        in
+         match 
+           try_hints metasenv subst 
+            (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
+         with
+          | Some x -> x
+          | None -> 
+              match exn with 
+              | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2))
+              | Uncertain _ as exn -> raise exn
+              | _ -> assert false
+    in
     let height_of = function
      | NCic.Const (Ref.Ref (_,Ref.Def h)) 
      | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h))) 
@@ -669,10 +695,6 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
      | _ -> 0
     in
-    let put_in_whd m1 m2 =
-      NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
-      NCicReduction.reduce_machine ~delta:max_int ~subst context m2
-    in
     let small_delta_step ~subst  
       ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
     =
@@ -723,13 +745,14 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
         let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in
         try
          let metasenv,subst =
-          fo_unif test_eq_only metasenv subst (norm1,hh1) (norm2,hh2) in
+          fo_unif_w_hints test_eq_only metasenv subst (norm1,hh1) (norm2,hh2) in
          List.fold_left
           (fun (metasenv,subst) (x1,x2,r) ->
             unif_from_stack x1 x2 r metasenv subst
           ) (metasenv,subst) todo
         with
-         | KeepReducing _ ->
+         | KeepReducing _ -> assert false
+         | KeepReducingThis _ ->
             assert (not (norm1 && norm2));
 	    unif_machines metasenv subst (small_delta_step ~subst m1 m2)
          | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
@@ -740,29 +763,17 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
            -> raise (Uncertain msg)
       (*D*)  in outside true; rc with exn -> outside false; raise exn 
      in
-     try fo_unif test_eq_only metasenv subst (false,t1) (false,t2)
-     with 
-     | UnificationFailure _ as exn -> raise exn
-     | KeepReducing _ | Uncertain _ as exn ->
-       let (t1,norm1 as tm1),(t2,norm2 as tm2) =
-        put_in_whd (0,[],t1,[]) (0,[],t2,[])
-       in
-        (match 
-          try_hints metasenv subst 
-           (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
-         with
-          | Some x -> x
-          | None ->
-             match exn with
-              | KeepReducing msg ->
-                 (try 
-                   unif_machines metasenv subst (tm1,tm2)
-                  with 
-                  | UnificationFailure _ -> raise (UnificationFailure msg)
-                  | Uncertain _ -> raise (Uncertain msg)
-                  | KeepReducing _ -> assert false)
-              | Uncertain _ -> raise exn
-              | _ -> assert false)
+     try fo_unif_w_hints test_eq_only metasenv subst (false,t1) (false,t2)
+     with
+      | KeepReducingThis (msg,tm1,tm2) ->
+         (try 
+           unif_machines metasenv subst (tm1,tm2)
+          with 
+          | UnificationFailure _ -> raise (UnificationFailure msg)
+          | Uncertain _ -> raise (Uncertain msg)
+          | KeepReducing _ -> assert false)
+      | KeepReducing _ -> assert false
+
  (*D*)  in outside true; rc with KeepReducing _ -> assert false | exn -> outside false; raise exn 
 
 and delift_type_wrt_terms rdb metasenv subst context t args =
diff --git a/helm/software/matita/nlibrary/logic/pts.ma b/helm/software/matita/nlibrary/logic/pts.ma
index e4f0815ff..8a44b8300 100644
--- a/helm/software/matita/nlibrary/logic/pts.ma
+++ b/helm/software/matita/nlibrary/logic/pts.ma
@@ -14,4 +14,4 @@
 
 universe constraint Type[0] < Type[1].
 universe constraint Type[1] < Type[2].
-
+universe constraint Type[2] < Type[3].
-- 
2.39.2