- sort_of_prod now returns the second Meta (if it is a Meta) after

  unifying it with a fresh Meta whose context is empty
- the name generated by eat_prods where not always fresh. Fixed.

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 27929645b8cfa8caa17b9fbf19f107f9a723a9d6..b64d8f4bb8b2236793b5be72d911e038e946b227 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -188,8 +188,7 @@ and type_of_aux' metasenv context t =
        let sort2,subst'',metasenv'' =
         type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
        in
-        sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2),
-         subst'',metasenv''
+        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
        let type2,subst'',metasenv'' =
@@ -199,10 +198,10 @@ and type_of_aux' metasenv context t =
          type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
         in
          (* only to check if the product is well-typed *)
-         let _ =
+         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
@@ -472,18 +471,24 @@ and type_of_aux' metasenv context t =
     match (t1'', t2'') with
        (C.Sort s1, C.Sort s2)
          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
-          C.Sort s2
+          C.Sort s2,subst,metasenv
      | (C.Sort s1, C.Sort s2) ->
          (*CSC manca la gestione degli universi!!! *)
-         C.Sort C.Type
-     | (C.Meta _,_) | (_,C.Meta _) ->
+         C.Sort C.Type,subst,metasenv
+     | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
+     | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
          (* TODO how can we force the meta to become a sort? If we don't we
           * brake the invariant that refine produce only well typed terms *)
          (* TODO if we check the non meta term and if it is a sort then we are
           * likely to know the exact value of the result e.g. if the rhs is a
           * Sort (Prop | Set | CProp) then the result is the rhs *)
-         (C.Sort C.Type)
-(*           t2'' *)
+         let (metasenv,idx) =
+          CicMkImplicit.mk_implicit metasenv [] in
+         let (subst, metasenv) =
+          CicUnification.fo_unif_subst subst context metasenv
+           (C.Meta (idx,[])) t2''
+         in
+          t2'',subst,metasenv
      | (_,_) ->
          raise (NotRefinable (sprintf
           "Two types were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
@@ -503,11 +508,22 @@ and type_of_aux' metasenv context t =
          ) args in
        let argty' = CicMetaSubst.lift subst (List.length args) argty in
        let name =
-        FreshNamesGenerator.mk_fresh_name
-         (CicMetaSubst.apply_subst_metasenv subst metasenv)
-         (CicMetaSubst.apply_subst_context subst context)
-         Cic.Anonymous
-         (CicMetaSubst.apply_subst subst argty) in
+        (* The name must be fresh for (context'@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'@context) name_hint (Cic.Sort Cic.Prop)
+       in
        let context'' = Some (name, Cic.Decl argty') :: context' in
        let (metasenv, idx) =
         CicMkImplicit.mk_implicit metasenv (context'' @ context) in