X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=549f06f85b57845c97737b609855b5b95fd016cc;hb=e62111335574a6ec78e5a4367a540e0529a00404;hp=f63aa9a30759d4a36acae98f99f892738e444dfd;hpb=57a360d659425ce1ee9a69516b66a4d3c7b8eb62;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index f63aa9a30..549f06f85 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 @@ -112,28 +133,34 @@ let rec force_does_not_occur metasenv subst restrictions t = NCicUtils.Subst_not_found _ -> (* we ignore the subst since restrict will take care of already * instantiated/restricted metavariabels *) - let (metasenv,subst as ms), restrictions_for_n, l' = - let l = NCicUtils.expand_local_context lc in - - let ms, _, restrictions_for_n, l = + let l = NCicUtils.expand_local_context lc in + let sl = List.map (NCicSubstitution.lift shift) l in + let (metasenv,subst as ms), _, restrictions_for_n, l' = List.fold_right (fun t (ms, i, restrictions_for_n, l) -> try - let ms, t = aux (k-shift) ms t in + (*pp (lazy ("L'ORLO DELLA FOSSA: k= " ^ string_of_int k ^ " shift=" ^ + string_of_int shift ^ " t=" ^ NCicPp.ppterm ~metasenv ~subst ~context:[] t));*) + let ms, t = aux k ms t in + (*pp (lazy ("LA FOSSA: " ^ NCicPp.ppterm ~metasenv ~subst ~context:[] t));*) ms, i-1, restrictions_for_n, t::l with Occur -> ms, i-1, i::restrictions_for_n, l) - l (ms, List.length l, [], []) - in - - ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l) + sl (ms, List.length l, [], []) in if restrictions_for_n = [] then - ms, if l = l' then orig else NCic.Meta (n, l') + ms, if sl = l' then orig else ( + (*pp (lazy ("FINITO: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] + ~context:[] (NCic.Meta (n,pack_lc (0, NCic.Ctx l')))));*) + NCic.Meta (n, pack_lc (0, NCic.Ctx l')) + ) else - let metasenv, subst, newmeta = - restrict metasenv subst n restrictions_for_n - in + let l' = pack_lc (0, NCic.Ctx l') in + let _ = pp (lazy ("restrictions for n are:" ^ String.concat "," (List.map string_of_int restrictions_for_n))) in + let metasenv, subst, newmeta, more_restricted = + restrict metasenv subst n restrictions_for_n in + let _ = pp (lazy ("more restricted: " ^String.concat "," (List.map string_of_int more_restricted))) 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 @@ -141,6 +168,8 @@ let rec force_does_not_occur metasenv subst restrictions t = and force_does_not_occur_in_context metasenv subst restrictions = function | name, NCic.Decl t as orig -> + (* pp (lazy ("CCC: hd is" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t ^ + "\nCCC: restrictions are:" ^ String.concat "," (List.map string_of_int restrictions)));*) let (metasenv, subst), t' = force_does_not_occur metasenv subst restrictions t in metasenv, subst, (if t == t' then orig else (name,NCic.Decl t')) @@ -172,7 +201,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 +220,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 +242,14 @@ 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 + (* pp (lazy ("BBB: dopo1 \n" ^ NCicPp.ppsubst ~metasenv [subst_entry])); + pp (lazy ("BBB: dopo2 \n" ^ NCicPp.ppsubst ~metasenv (subst_entry::subst))); + pp (lazy ("BBB: dopo metasenv\n" ^ NCicPp.ppmetasenv ~subst [metasenv_entry]));*) + 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 +397,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 +425,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 +456,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