X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=b18364509db79f282b7d18372bee0d2cd189f87c;hb=a0b7db9844126ebcdf4b5dbb586514854cef5d93;hp=b69984f3d5c2c15a0e6d761529c2cd69fe935c04;hpb=fb2fabf6c94d6a2f930b7a84673c90af32c48803;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index b69984f3d..b18364509 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 @@ -105,47 +126,50 @@ let rec force_does_not_occur metasenv subst restrictions t = in if amount > 0 then ms, NCic.Rel (r - amount) else ms, orig | NCic.Meta (n, (shift,lc as l)) as orig -> - let meta_chain = - try - Some (NCicUtils.lookup_subst n subst) + (try + let _,_,bo,_ = NCicUtils.lookup_subst n subst in + aux k ms (NCicSubstitution.subst_meta l bo) with - NCicUtils.Subst_not_found _ -> None - in - (match meta_chain with - Some (_,_,bo,_) -> - aux k ms (NCicSubstitution.subst_meta l bo) - | None -> - (* 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 = - List.fold_right - (fun t (ms, i, restrictions_for_n, l) -> - try - let ms, t = aux (k-shift) ms t in - 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) - in - 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 - (metasenv, subst), NCic.Meta (newmeta, l')) + NCicUtils.Subst_not_found _ -> + (* we ignore the subst since restrict will take care of already + * instantiated/restricted metavariabels *) + 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 + (*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) + sl (ms, List.length l, [], []) + in + if restrictions_for_n = [] then + 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 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 aux 0 (metasenv,subst) 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')) @@ -177,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 @@ -196,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 "^^ @@ -226,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 "^^ @@ -239,16 +259,16 @@ and restrict metasenv subst i restrictions = | NCicUtils.Meta_not_found _ -> assert false ;; -let rec flexible_arg context subst = function +let rec is_flexible context ~subst = function | NCic.Meta (i,_) -> (try let _,_,t,_ = List.assoc i subst in - flexible_arg context subst t + is_flexible context ~subst t with Not_found -> true) | NCic.Appl (NCic.Meta (i,_) :: args)-> (try let _,_,t,_ = List.assoc i subst in - flexible_arg context subst + is_flexible context ~subst (NCicReduction.head_beta_reduce ~delta:max_int (NCic.Appl (t :: args))) with Not_found -> true) @@ -263,7 +283,7 @@ let rec flexible_arg context subst = function match List.nth context (i-1) with | _,NCic.Def (bo,_) -> - flexible_arg context subst + is_flexible context ~subst (NCicSubstitution.lift i bo) | _ -> false with @@ -312,11 +332,11 @@ let delift ~unify metasenv subst context n l t = match l with | _, NCic.Irl _ -> fun _ _ _ _ _ -> None | shift, NCic.Ctx l -> fun metasenv subst context k t -> - if flexible_arg context subst t || contains_in_scope subst t then None else + if is_flexible context ~subst t || contains_in_scope subst t then None else let lb = List.map (fun t -> let t = NCicSubstitution.lift (k+shift) t in - t, flexible_arg context subst t) + t, is_flexible context ~subst t) l in HExtlib.list_findopt @@ -377,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 @@ -405,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 @@ -451,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