Great optimization for eat_prods: if the type of the head of the application is meta_...

the construction of the spine of Prods and relative unification is skipped.

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 1f92a5fa881b95396c1eaf06fd2a06fdcc0fc1fc..e99ce5cd70285fe94680b80fdab6a20442b860c7 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -35,6 +35,30 @@ let insert_coercions = ref true
 
 let debug_print = fun _ -> ()
 
+let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
+
+let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
+  try
+let foo () =
+    CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
+in profiler_eat_prods2.HExtlib.profile foo ()
+  with
+      (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
+    | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
+;;
+
+let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
+
+let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
+  try
+let foo () =
+    CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
+in profiler_eat_prods.HExtlib.profile foo ()
+  with
+      (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
+    | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
+;;
+
 let profiler = HExtlib.profile "CicRefine.fo_unif"
 
 let fo_unif_subst subst context metasenv t1 t2 ugraph =
@@ -1150,21 +1174,24 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
             in
               metasenv,Cic.Prod (name,meta,target)
     in
-    let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
-    let (subst, metasenv,ugraph1) =
-      try
-        fo_unif_subst subst context metasenv hetype hetype' ugraph
-      with exn ->
-       enrich localization_tbl he
-        ~f:(fun _ ->
-          (lazy ("The term " ^
-            CicMetaSubst.ppterm_in_context subst he
-             context ^ " (that has type " ^
-            CicMetaSubst.ppterm_in_context subst hetype
-             context ^ ") is here applied to " ^
-            string_of_int (List.length tlbody_and_type) ^
-            " arguments that are more than expected"
-             (* "\nReason: " ^ Lazy.force exn*)))) exn
+    let ((subst,metasenv,ugraph1),hetype') =
+     if CicUtil.is_meta_closed hetype then
+      (subst,metasenv,ugraph),hetype
+     else
+      let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
+       try
+         fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph, hetype'
+       with exn ->
+        enrich localization_tbl he
+         ~f:(fun _ ->
+           (lazy ("The term " ^
+             CicMetaSubst.ppterm_in_context subst he
+              context ^ " (that has type " ^
+             CicMetaSubst.ppterm_in_context subst hetype
+              context ^ ") is here applied to " ^
+             string_of_int (List.length tlbody_and_type) ^
+             " arguments that are more than expected"
+              (* "\nReason: " ^ Lazy.force exn*)))) exn
     in
     let rec eat_prods metasenv subst context hetype ugraph =
       function
@@ -1175,7 +1202,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                    let arg,subst,metasenv,ugraph1 =
                      try
                        let subst,metasenv,ugraph1 = 
-                         fo_unif_subst subst context metasenv hety s ugraph
+                         fo_unif_subst_eat_prods2 subst context metasenv hety s ugraph
                        in
                          hete,subst,metasenv,ugraph1
                      with exn when allow_coercions && !insert_coercions ->
@@ -1250,8 +1277,15 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                        (CicSubstitution.subst arg t) ugraph1 tl
                    in
                      arg::coerced_args,metasenv',subst',t',ugraph2
-               | _ -> assert false
-            )
+               | _ ->
+                 raise (RefineFailure
+                  (lazy ("The term " ^
+                    CicMetaSubst.ppterm_in_context subst he
+                     context ^ " (that has type " ^
+                    CicMetaSubst.ppterm_in_context subst hetype'
+                     context ^ ") is here applied to " ^
+                    string_of_int (List.length tlbody_and_type) ^
+                    " arguments that are more than expected"))))
     in
     let coerced_args,metasenv,subst,t,ugraph2 =
       eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type 
@@ -1306,12 +1340,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) 
 ;;
 
-let type_of_aux' ?localization_tbl metasenv context term ugraph =
-  try 
-    type_of_aux' ?localization_tbl metasenv context term ugraph
-  with 
-    CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
-
 let undebrujin uri typesno tys t =
   snd
    (List.fold_right