eat_prods reimplemented to generalize the output type of the application

a bit more (when it is a metavariable).

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index a6506d5cacb057c13c0f7de4813364c813922d68..60b6129b1c2db4ca806e4460872e95db635f525d 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -25,6 +25,8 @@
 
 open Printf
 
+exception RefineFailure of string;;
+
 exception Impossible of int;;
 exception NotRefinable of string;;
 exception Uncertain of string;;
@@ -33,7 +35,6 @@ exception WrongUriToVariable of string;;
 exception ListTooShort;;
 exception WrongUriToMutualInductiveDefinitions of string;;
 exception RelToHiddenHypothesis;;
-exception MetasenvInconsistency;;
 exception WrongArgumentNumber;;
 
 let fdebug = ref 0;;
@@ -416,7 +417,7 @@ and type_of_aux' metasenv context t =
          | Some t,Some (_,C.Def (ct,_)) ->
             (try
               CicUnification.fo_unif_subst subst context metasenv t ct
-             with _ -> raise MetasenvInconsistency)
+             with _ -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct))))
          | Some t,Some (_,C.Decl ct) ->
             let inferredty,subst',metasenv' =
              type_of_aux subst metasenv context t
@@ -424,9 +425,9 @@ and type_of_aux' metasenv context t =
              (try
                CicUnification.fo_unif_subst
                 subst' context metasenv' inferredty ct
-             with _ -> raise MetasenvInconsistency)
-         | _, _  ->
-             raise MetasenvInconsistency
+             with _ -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct))))
+         | None, Some _  ->
+             raise (NotRefinable "The local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context")
       ) (subst,metasenv) l lifted_canonical_context 
 
  and check_exp_named_subst metasubst metasenv context =
@@ -482,41 +483,46 @@ and type_of_aux' metasenv context t =
          C.Meta (idx, irl), subst, metasenv
      | (_,_) ->
          raise (NotRefinable (sprintf
-          "Two types were expected, found %s of type %s and %s of type %s"
+          "Two types were expected, found %s (that reduces to %s) and %s (that reducecs to %s)"
           (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
           (CicPp.ppterm t2'')))
 
  and eat_prods subst metasenv context hetype tlbody_and_type =
-   (* TODO to be reviewed *)
-  List.fold_left
-    (fun (resty, subst, metasenv) (arg, argty) ->
-      let context' = Some (Cic.Anonymous, Cic.Decl argty) :: context in
-      let (metasenv, idx) = CicMkImplicit.mk_implicit metasenv context' in
-      let irl =
-        CicMkImplicit.identity_relocation_list_for_metavariable context'
-      in
-      let newmeta = Cic.Meta (idx, irl) in
-      let prod = Cic.Prod (Cic.Anonymous, argty, newmeta) in
-      let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
-      let (subst, metasenv) =
-        CicUnification.fo_unif_subst subst context metasenv resty prod
-      in
-      (CicMetaSubst.subst subst arg newmeta, subst, metasenv))
-    (hetype, subst, metasenv) tlbody_and_type
+  let rec aux context' args (resty,subst,metasenv) =
+   function
+      [] -> resty,subst,metasenv
+    | (arg,argty)::tl ->
+       let args' =
+        List.map
+         (function
+             None -> assert false
+           | Some t -> Some (CicMetaSubst.lift subst 1 t)
+         ) args in
+       let argty' = CicMetaSubst.lift subst (List.length args) argty in
+       let context'' = Some (Cic.Anonymous, Cic.Decl argty') :: context' in
+       let (metasenv, idx) =
+        CicMkImplicit.mk_implicit metasenv (context'' @ context) in
+       let irl =
+         (Some (Cic.Rel 1))::args'@(CicMkImplicit.identity_relocation_list_for_metavariable ~start:2 context)
+       in
+       let newmeta = Cic.Meta (idx, irl) in
+       let prod = Cic.Prod (Cic.Anonymous, argty, newmeta) in
+       let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
+       let (subst, metasenv) =
+         CicUnification.fo_unif_subst subst context metasenv resty prod
+       in
+        aux context'' (Some arg :: args)
+         (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
+  in
+   aux [] [] (hetype,subst,metasenv) tlbody_and_type
 
  in
   let ty,subst',metasenv' =
    type_of_aux [] metasenv context t
   in
-   (* we get rid of the metavariables that have been instantiated *)
-   let metasenv'' =
-    List.filter
-     (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst'))
-     metasenv'
-   in
    (CicMetaSubst.apply_subst subst' t,
     CicMetaSubst.apply_subst subst' ty,
-    CicMetaSubst.apply_subst_metasenv subst' metasenv'')
+    CicMetaSubst.apply_subst_metasenv subst' metasenv')
 ;;
 
 (* DEBUGGING ONLY *)