New implementation of eat_prods.

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 8935d867c570628f4f80d70eac72e9c30ce564cd..06398da9a5e3dafa1fa3e89545d8e65f3d5d5f38 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -185,17 +185,19 @@ and type_of_aux' metasenv context t =
         sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
    | C.Lambda (n,s,t) ->
        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
+       (match CicMetaSubst.whd subst' context sort1 with
+           C.Meta _
+         | C.Sort _ -> ()
+         | _ ->
+           raise (NotRefinable (sprintf
+            "Not well-typed lambda-abstraction: the source %s should be a type;
+             instead it is a term of type %s" (CicPp.ppterm s)
+            (CicPp.ppterm sort1)))
+       ) ;
        let type2,subst'',metasenv'' =
         type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
        in
-        let sort2,subst''',metasenv''' =
-         type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
-        in
-         (* only to check if the product is well-typed *)
-         let _,subst'''',metasenv'''' =
-          sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
-         in
-          C.Prod (n,s,type2),subst'''',metasenv''''
+          C.Prod (n,s,type2),subst'',metasenv''
    | C.LetIn (n,s,t) ->
       (* only to check if s is well-typed *)
       let ty,subst',metasenv' = type_of_aux subst metasenv context s in
@@ -485,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
@@ -531,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' =