X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=12fe977083ec04a2c9ee309c116e2cb22419929b;hb=e1ffde2ba67b8a2f7d4d97898ba28afd65d96ea7;hp=102958869817e6123245a4f299a0b3f0b91ad4c6;hpb=c14ddc094a1cfa93b5337e5aecc6831f72dfc22b;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 102958869..12fe97708 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -179,15 +179,6 @@ let pack_lc orig = ;; -let mk_restricted_irl shift len restrictions = - let rec aux n = - if n = 0 then 0 else - if List.mem (n+shift) restrictions then aux (n-1) - else 1+aux (n-1) - in - pack_lc (shift, NCic.Irl (aux len)) -;; - let mk_perforated_irl shift len restrictions = let rec aux n = @@ -208,28 +199,22 @@ let rec force_does_not_occur metasenv subst restrictions t = List.length (List.filter (fun x -> x < r - k) restrictions) in if amount > 0 then ms, NCic.Rel (r - amount) else ms, orig - | NCic.Meta (n, l) as orig -> + | NCic.Meta (n, (shift,lc as l)) as orig -> (* we ignore the subst since restrict will take care of already * instantiated/restricted metavariabels *) let (metasenv,subst as ms), restrictions_for_n, l' = - match l with - | shift, NCic.Irl len -> - let restrictions = - List.filter - (fun i -> i > shift && i <= shift + len) restrictions in - ms, restrictions, mk_restricted_irl shift len restrictions - | shift, NCic.Ctx l -> - 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) + 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') @@ -287,13 +272,23 @@ and restrict metasenv subst i restrictions = let (metasenv, subst), newbo = force_does_not_occur metasenv subst restrictions bo in let j = newmeta () in - let subst_entry_j = j, (name, newctx, newty, newbo) in + let subst_entry_j = j, (name, newctx, newbo, newty) in let reloc_irl = mk_perforated_irl 0 (List.length ctx) restrictions in let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in - metasenv, - subst_entry_j :: List.map - (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst, - j + let new_subst = + 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 with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf ("Cannot restrict the context of the metavariable ?%d over "^^ "the hypotheses %s since ?%d is already instantiated "^^ @@ -311,10 +306,6 @@ and restrict metasenv subst i restrictions = force_does_not_occur metasenv subst restrictions ty in let j = newmeta () in let metasenv_entry = j, (name, newctx, newty) in - prerr_endline ("restricting ?" ^ string_of_int i ^ " to ?" ^ - string_of_int j ^ " : " ^ NCicPp.ppterm ~metasenv ~context:newctx - ~subst newty ^" in a shorter context:\n" ^ - NCicPp.ppcontext ~metasenv ~subst newctx); 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 @@ -349,6 +340,7 @@ let delift metasenv subst context n l t = aux k ms (NCicSubstitution.lift n bo)) | _,NCic.Decl _ -> ms, NCic.Rel ((position (n-k) l) + k) with Failure _ -> assert false) (*Unbound variable found in delift*) + | NCic.Meta (_,(_,(NCic.Irl 0| NCic.Ctx []))) as orig -> ms, orig | NCic.Meta (i,l1) as orig -> (try let _,_,t,_ = NCicUtils.lookup_subst i subst in @@ -364,37 +356,78 @@ let delift metasenv subst context n l t = else let shift1,lc1 = l1 in let shift,lc = l in + let shift = shift + k in match lc, lc1 with | NCic.Irl len, NCic.Irl len1 - when shift1 < shift || len1 + shift1 > len + shift -> - let restrictions = - HExtlib.list_seq 1 (shift - shift1) @ - HExtlib.list_seq (shift+len+1) (shift1+len1) - in + 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, mk_perforated_irl shift1 len1 restrictions) + NCic.Meta (newmeta, (0,NCic.Irl (max 0 (k-shift1)))) + | NCic.Irl len, NCic.Irl len1 + when shift1 < shift || len1 + shift1 > len + shift -> + (* C. Hoare. Premature optimization is the root of all evil*) + let stop = shift + len in + let stop1 = shift1 + len1 in + let low_gap = max 0 (shift - shift1) in + let high_gap = max 0 (stop1 - stop) in + let restrictions = + HExtlib.list_seq (k+1-shift1) (low_gap + 1) @ + HExtlib.list_seq (len1 - high_gap + 1) (len1 + 1) + in + 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 newlc_len = + len1 - low_gap - high_gap + max 0 (k - shift1) in + assert (if shift1 > k then + shift1 + low_gap - shift = 0 else true); + let meta = + NCic.Meta(newmeta,(shift1 + low_gap - shift, + NCic.Irl newlc_len)) + in + let _, cctx, _ = NCicUtils.lookup_meta newmeta metasenv in + assert (List.length cctx = newlc_len); + (metasenv, subst), meta + | NCic.Irl _, NCic.Irl _ when shift = 0 -> ms, orig | NCic.Irl _, NCic.Irl _ -> - ms, NCic.Meta (i, (shift1 - shift, lc1)) - | _ -> + ms, NCic.Meta (i, (max 0 (shift1 - shift), lc1)) + | _ -> let lc1 = NCicUtils.expand_local_context lc1 in + let lc1 = List.map (NCicSubstitution.lift shift1) lc1 in let rec deliftl tbr j ms = function | [] -> ms, tbr, [] | t::tl -> let ms, tbr, tl = deliftl tbr (j+1) ms tl in try - let ms, t = aux (k-shift1) ms t in + let ms, t = aux k ms t in ms, tbr, t::tl with | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl in let (metasenv, subst), to_be_r, lc1' = deliftl [] 1 ms lc1 in +(* prerr_endline ("TO BE RESTRICTED: " ^ (String.concat "," (List.map string_of_int to_be_r))); - let l1 = pack_lc (shift, NCic.Ctx lc1') in +*) + let l1 = pack_lc (0, NCic.Ctx lc1') in +(* + prerr_endline ("newmeta:" ^ NCicPp.ppterm + ~metasenv ~subst ~context (NCic.Meta (999,l1))); +*) if to_be_r = [] then (metasenv, subst), (if lc1' = lc1 then orig else NCic.Meta (i,l1)) @@ -402,6 +435,7 @@ let delift metasenv subst context n l t = let metasenv, subst, newmeta = restrict metasenv subst i to_be_r in (metasenv, subst), NCic.Meta(newmeta,l1)) + | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t in try aux 0 (metasenv,subst) t @@ -572,15 +606,22 @@ let delift_rels subst metasenv n t = let mk_meta ?name metasenv context ty = match ty with - | None -> - let len = List.length context in + | `Typeless -> + let n = newmeta () in + let ty = NCic.Implicit (`Typeof n) in + let menv_entry = (n, (name, context, ty)) in + menv_entry :: metasenv,NCic.Meta (n, (0,NCic.Irl (List.length context))), ty + | `Type + | `Term -> + let context_for_ty = if ty = `Type then [] else context in let n = newmeta () in - let ty_menv_entry = (n, (name, context, NCic.Implicit (`Typeof n))) in + let ty_menv_entry = (n, (name,context_for_ty, NCic.Implicit (`Typeof n))) in let m = newmeta () in - let ty = NCic.Meta (n, (0,NCic.Irl len)) in + let ty = NCic.Meta (n, (0,NCic.Irl (List.length context_for_ty))) in let menv_entry = (m, (name, context, ty)) in - menv_entry :: ty_menv_entry :: metasenv, NCic.Meta (m, (0,NCic.Irl len)), ty - | Some ty -> + menv_entry :: ty_menv_entry :: metasenv, + NCic.Meta (m, (0,NCic.Irl (List.length context))), ty + | `WithType ty -> let n = newmeta () in let len = List.length context in let menv_entry = (n, (name, context, ty)) in @@ -591,7 +632,8 @@ let saturate ?(delta=0) metasenv context ty goal_arity = assert (goal_arity >= 0); let rec aux metasenv = function | NCic.Prod (name,s,t) -> - let metasenv1, arg,_ = mk_meta ~name:name metasenv context (Some s) in + let metasenv1, arg,_ = + mk_meta ~name:name metasenv context (`WithType s) in let t, metasenv1, args, pno = aux metasenv1 (NCicSubstitution.subst arg t) in