From da11c92be86c24285ef1a4d0ddfe1e074a6b322a Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 26 Feb 2004 16:14:58 +0000
Subject: [PATCH] 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.
---
 helm/ocaml/cic_unification/cicRefine.ml | 64 +++++++++++++++++++++++++
 1 file changed, 64 insertions(+)

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index bc1468126..06398da9a 100644
--- 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' =
-- 
2.39.2