From: Claudio Sacerdoti Coen Date: Thu, 5 Feb 2004 16:41:42 +0000 (+0000) Subject: - sort_of_prod now returns the second Meta (if it is a Meta) after X-Git-Tag: V_0_2_3~37 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f42507bf45ea6b50adbae7ba8117905cc9631101;p=helm.git - 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 27929645b..b64d8f4bb 100644 --- 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