From 4469d300334ff00a22eab15d763fc96521c92906 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 3 Feb 2004 15:11:07 +0000 Subject: [PATCH] sort_of_prod changed to not generate a new metavariable in the case Meta vs Sort. Reason: the new metavariable is not constrained in any way and, at the end, we find it in the final metasenv. --- helm/ocaml/cic_unification/cicRefine.ml | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 60b6129b1..ee5916e0c 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -188,7 +188,8 @@ 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) + sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2), + subst'',metasenv'' | C.Lambda (n,s,t) -> let sort1,subst',metasenv' = type_of_aux subst metasenv context s in let type2,subst'',metasenv'' = @@ -198,10 +199,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 _,subst'''',metasenv'''' = + let _ = 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 @@ -466,21 +467,17 @@ 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,subst,metasenv + C.Sort s2 | (C.Sort s1, C.Sort s2) -> (*CSC manca la gestione degli universi!!! *) - C.Sort C.Type,subst,metasenv + C.Sort C.Type | (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 *) - let (metasenv, idx) = CicMkImplicit.mk_implicit metasenv context in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in - C.Meta (idx, irl), subst, metasenv + t2'' | (_,_) -> raise (NotRefinable (sprintf "Two types were expected, found %s (that reduces to %s) and %s (that reducecs to %s)" -- 2.39.2