From 9d33fd0863f207cee7f882ae28c83e1944d2a0f1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 4 Nov 2009 16:47:11 +0000 Subject: [PATCH] Bug fixed: restrict used to take the list of positions to be restricted, but it did not return the (potentially bigger) set of actually restricted positions. Thus, it was possible to create a local context longer then the canonical one. --- .../components/ng_refiner/nCicMetaSubst.ml | 86 +++++++++---------- .../components/ng_refiner/nCicMetaSubst.mli | 7 +- .../components/ng_refiner/nCicRefiner.ml | 6 +- .../components/ng_refiner/nCicUnification.ml | 2 +- .../components/ng_tactics/nTactics.ml | 2 +- 5 files changed, 54 insertions(+), 49 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index f63aa9a30..ce0021d3d 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -96,6 +96,27 @@ let mk_perforated_irl shift len restrictions = exception Occur;; +let purge_restricted restrictions more_restrictions l = + if more_restrictions = [] then l + else + begin + pp (lazy ("TO BE RESTRICTED: " ^ + (String.concat "," (List.map string_of_int restrictions)))); + pp (lazy ("MORE RESTRICTIONS: " ^ + (String.concat "," (List.map string_of_int more_restrictions)))); + let shift,lc = l in + let lc = NCicUtils.expand_local_context lc in + let rec aux n lc = + match lc with + [] -> [] + | _ when List.mem n restrictions -> aux (n+1) lc + | _::tl when List.mem n more_restrictions -> aux (n+1) tl + | he::tl -> he::aux (n+1) tl + in + pack_lc (shift, NCic.Ctx (aux 1 lc)) + end +;; + let rec force_does_not_occur metasenv subst restrictions t = let rec aux k ms = function | NCic.Rel r when List.mem (r - k) restrictions -> raise Occur @@ -131,9 +152,9 @@ let rec force_does_not_occur metasenv subst restrictions t = if restrictions_for_n = [] then ms, if l = l' then orig else NCic.Meta (n, l') else - let metasenv, subst, newmeta = - restrict metasenv subst n restrictions_for_n - in + let metasenv, subst, newmeta, more_restricted = + restrict metasenv subst n restrictions_for_n in + let l' = purge_restricted restrictions more_restricted l' in (metasenv, subst), NCic.Meta (newmeta, l')) | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t in @@ -172,7 +193,7 @@ and erase_in_context metasenv subst pos restrictions = function with Occur -> metasenv, subst, (pos :: restricted), tl' -and restrict metasenv subst i restrictions = +and restrict metasenv subst i (restrictions as orig) = assert (restrictions <> []); try let name, ctx, bo, ty = NCicUtils.lookup_subst i subst in @@ -191,16 +212,8 @@ and restrict metasenv subst i restrictions = subst_entry_j :: List.map (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst in -(* - prerr_endline ("restringo nella subst: " ^string_of_int i ^ " -> " ^ - string_of_int j ^ "\n" ^ - NCicPp.ppsubst ~metasenv [subst_entry_j] ^ "\n\n" ^ - NCicPp.ppsubst ~metasenv [subst_entry_i] ^ "\n" ^ - NCicPp.ppterm ~metasenv ~subst ~context:ctx bo ^ " ---- " ^ - NCicPp.ppterm ~metasenv ~subst ~context:newctx newbo - ); -*) - metasenv, new_subst, j + let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in + metasenv, new_subst, j, diff with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf ("Cannot restrict the context of the metavariable ?%d over "^^ "the hypotheses %s since ?%d is already instantiated "^^ @@ -221,10 +234,11 @@ and restrict metasenv subst i restrictions = let reloc_irl = mk_perforated_irl 0 (List.length ctx) restrictions in let subst_entry = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in + let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in List.map (fun (n,_) as orig -> if i = n then metasenv_entry else orig) metasenv, - subst_entry :: subst, j + subst_entry :: subst, j, diff with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf ("Cannot restrict the context of the metavariable ?%d "^^ "over the hypotheses %s since metavariable's type depends "^^ @@ -372,11 +386,11 @@ let delift ~unify metasenv subst context n l t = | NCic.Irl len, NCic.Irl len1 when shift1 + len1 < shift || shift1 > shift + len -> let restrictions = HExtlib.list_seq 1 (len1 + 1) in - let metasenv, subst, newmeta = - restrict metasenv subst i restrictions - in - (metasenv, subst), - NCic.Meta (newmeta, (0,NCic.Irl (max 0 (k-shift1)))) + let metasenv, subst, newmeta, more_restricted = + restrict metasenv subst i restrictions in + let l' = (0,NCic.Irl (max 0 (k-shift1))) in + let l' = purge_restricted restrictions more_restricted l' in + (metasenv, subst),NCic.Meta (newmeta,l') | NCic.Irl len, NCic.Irl len1 -> let low_restrictions, new_shift = if k <= shift1 && shift1 < shift then @@ -400,27 +414,12 @@ let delift ~unify metasenv subst context n l t = if shift = k then ms, orig else ms, NCic.Meta (i, (new_shift, lc1)) else - let metasenv, subst, newmeta = - restrict metasenv subst i restrictions - in -(* {{{ - prerr_endline ("RESTRICTIONS FOR: " ^ - NCicPp.ppterm ~metasenv ~subst ~context:[] - (NCic.Meta (i,l1))^" that was part of a term unified with " - ^ NCicPp.ppterm ~metasenv ~subst ~context:[] (NCic.Meta - (n,l)) ^ " ====> " ^ String.concat "," (List.map - string_of_int restrictions) ^ "\nMENV:\n" ^ - NCicPp.ppmetasenv ~subst metasenv ^ "\nSUBST:\n" ^ - NCicPp.ppsubst subst ~metasenv); -}}} *) + let metasenv, subst, newmeta, more_restricted = + restrict metasenv subst i restrictions in let newlc_len = len1 - List.length restrictions in - let meta = - NCic.Meta(newmeta,(new_shift, NCic.Irl newlc_len)) - in - assert ( - let _, cctx, _ = NCicUtils.lookup_meta newmeta metasenv in - List.length cctx = newlc_len); - (metasenv, subst), meta + let l' = new_shift, NCic.Irl newlc_len in + let l' = purge_restricted restrictions more_restricted l' in + (metasenv, subst),NCic.Meta(newmeta,l') | _ -> let lc1 = NCicUtils.expand_local_context lc1 in @@ -446,9 +445,10 @@ let delift ~unify metasenv subst context n l t = (metasenv, subst), (if lc1' = lc1 then orig else NCic.Meta (i,l1)) else - let metasenv, subst, newmeta = - restrict metasenv subst i to_be_r in - (metasenv, subst), NCic.Meta(newmeta,l1)) + let metasenv, subst, newmeta, more_restricted = + restrict metasenv subst i to_be_r in + let l1 = purge_restricted to_be_r more_restricted l1 in + (metasenv, subst), NCic.Meta(newmeta,l1)) | t -> NCicUntrusted.map_term_fold_a diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli index 94a77f287..fd101414d 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.mli +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -41,10 +41,15 @@ val delift : int -> NCic.local_context -> NCic.term -> (NCic.metasenv * NCic.substitution) * NCic.term +(* restrict metasenv subst n l + returns metasenv, subst, created meta and l' where l' is the list of + additional (i.e. l' does not intersects l) positions whose restriction was + forced because of type dependencies *) val restrict: NCic.metasenv -> NCic.substitution -> - int -> int list -> NCic.metasenv * NCic.substitution * int + int -> int list -> + NCic.metasenv * NCic.substitution * int * int list (* bool = true if the type of the new meta is closed *) val mk_meta: diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index fdb9c2137..d75fd6ab0 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -457,10 +457,10 @@ and force_to_sort rdb metasenv subst context t orig_t localise ty = metasenv, subst, t, C.Meta(i,(0,C.Irl 0)) *) | C.Meta (i,(_,lc)) -> let len = match lc with C.Irl len->len | C.Ctx l->List.length l in - let metasenv, subst, newmeta = + let metasenv, subst, newmeta, _ = if len > 0 then - NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1)) - else metasenv, subst, i + NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1)) + else metasenv, subst, i, [] in metasenv, subst, t, C.Meta (newmeta,(0,C.Irl 0)) | C.Sort _ as ty -> metasenv, subst, t, ty diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 1a667770b..0f73dbc5c 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -453,7 +453,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = l1 l2 (metasenv, subst, [], List.length l1) in if to_restrict <> [] then - let metasenv, subst, _ = + let metasenv, subst, _, _ = NCicMetaSubst.restrict metasenv subst n1 to_restrict in metasenv, subst diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index a4a72a180..6011d912d 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -314,7 +314,7 @@ let clear_tac names = names in let n,h,metasenv,subst,o = status#obj in - let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in + let metasenv,subst,_,_ = NCicMetaSubst.restrict metasenv subst goal js in status#set_obj (n,h,metasenv,subst,o)) ;; -- 2.39.2