New implementation of eat_prods.

In theory we expected it to be less efficient.
In pratice it is MUCH more efficient.

The old implementation is still there, but commented out.
We have to investigate the mistery a bit more.

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index bc14681263b80497477efc5294ea38f710d9b11f..06398da9a5e3dafa1fa3e89545d8e65f3d5d5f38 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -487,6 +487,69 @@ and type_of_aux' metasenv context t =
           (CicPp.ppterm t2'')))
 
  and eat_prods subst metasenv context hetype tlbody_and_type =
+ let rec mk_prod metasenv context =
+  function
+     [] ->
+       let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
+       let irl =
+        CicMkImplicit.identity_relocation_list_for_metavariable context
+       in
+        metasenv,Cic.Meta (idx, irl)
+   | (_,argty)::tl ->
+      let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
+      let irl =
+       CicMkImplicit.identity_relocation_list_for_metavariable context
+      in
+       let meta = Cic.Meta (idx,irl) in
+       let name =
+        (* The name must be fresh for context.                 *)
+        (* Nevertheless, argty is well-typed only in context.  *)
+        (* Thus I generate a name (name_hint) in context and   *)
+        (* then I generate a name --- using the hint name_hint *)
+        (* --- that is fresh in (context'@context).            *)
+        let name_hint =
+         FreshNamesGenerator.mk_fresh_name
+          (CicMetaSubst.apply_subst_metasenv subst metasenv)
+          (CicMetaSubst.apply_subst_context subst context)
+          Cic.Anonymous
+          (CicMetaSubst.apply_subst subst argty)
+        in
+         (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
+         FreshNamesGenerator.mk_fresh_name
+          [] context name_hint (Cic.Sort Cic.Prop)
+       in
+       let metasenv,target =
+        mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
+       in
+        metasenv,Cic.Prod (name,meta,target)
+ in
+  let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
+  let (subst, metasenv) =
+   CicUnification.fo_unif_subst subst context metasenv hetype hetype'
+  in
+   let rec eat_prods metasenv subst context hetype =
+      function
+         [] -> metasenv,subst,hetype
+       | (hete, hety)::tl ->
+        (match hetype with
+            Cic.Prod (n,s,t) ->
+             (try
+              let subst,metasenv =
+               CicUnification.fo_unif_subst subst context metasenv s hety
+              in
+               eat_prods metasenv subst context
+                (CicMetaSubst.subst subst hete t) tl
+             with
+              e -> raise (RefineFailure ("XXX " ^ Printexc.to_string e)))
+          | _ -> assert false
+        )
+   in
+    let metasenv,subst,t =
+     eat_prods metasenv subst context hetype' tlbody_and_type
+    in
+     t,subst,metasenv
+
+(*
   let rec aux context' args (resty,subst,metasenv) =
    function
       [] -> resty,subst,metasenv
@@ -533,6 +596,7 @@ and type_of_aux' metasenv context t =
          (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
   in
    aux [] [] (hetype,subst,metasenv) tlbody_and_type
+*)
 
  in
   let ty,subst',metasenv' =