From 237e58b77eda53354d9621e3e2f684c30f7da763 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 25 Oct 2006 17:42:45 +0000 Subject: [PATCH] 1. is_meta_closed should be applied only to terms on which a substitution has already been applied. Fixed here and there. Note: it is not possible to add a subst parameter to is_meta_closed since the function is declared in cic/CicUtil and it is used where the unification is not available (e.g. in whelp and library) 2. known (but never verified before) bug fixed: delifting should fail (instead of raising Uncertain) iff the local context is not meta_closed. The test used to be "does not contain a Meta" --- components/cic_unification/cicMetaSubst.ml | 15 ++++++--------- components/cic_unification/cicRefine.ml | 2 +- 2 files changed, 7 insertions(+), 10 deletions(-) diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml index 96efe2e3c..8d53495bf 100644 --- a/components/cic_unification/cicMetaSubst.ml +++ b/components/cic_unification/cicMetaSubst.ml @@ -98,7 +98,6 @@ let rec deref subst = let lookup_subst = CicUtil.lookup_subst ;; - (* clean_up_meta take a metasenv and a term and make every local context of each occurrence of a metavariable consistent with its canonical context, with respect to the hidden hipothesis *) @@ -749,15 +748,14 @@ debug_print(lazy (sprintf l)))) in if - (*CSC: WARNING: if we are working up to reduction (I do not think so), - the following test should be replaced with "all the terms in l are - meta-closed" *) - not - (List.exists (function Some (Cic.Meta _) -> true | _ -> false ) l) + List.exists + (function + Some t -> CicUtil.is_meta_closed (apply_subst subst t) + | None -> true) l then - raise (MetaSubstFailure msg) - else raise (Uncertain msg) + else + raise (MetaSubstFailure msg) in let (metasenv, subst) = restrict subst !to_be_restricted metasenv in res, metasenv, subst @@ -914,4 +912,3 @@ let fpp_gen ppf s = let fppsubst ppf subst = fpp_gen ppf (ppsubst subst) let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term) let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv) - diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index be4014507..8ae5964c9 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -1510,7 +1510,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il in (* first we check if we are in the simple case of a meta closed term *) let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty = - if CicUtil.is_meta_closed hetype then + if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then (* this optimization is to postpone fix_arity (the most common case)*) subst,metasenv,ugraph,hetype,he,args_bo_and_ty else -- 2.39.2