X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=cbcd8153cc2db8741da71c1715cd8e264244b9a8;hb=1ee5193677b8e2a80d4f068ee79ecac335de1196;hp=5267796efda2ec43ee8bd9e920ad49f1d035b650;hpb=b68325537e9e42c5da370c9f053fa99dba8a55cd;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 5267796ef..cbcd8153c 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -155,7 +155,7 @@ exception NotInTheList;; let position n (shift, lc) = match lc with | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList - | NCic.Irl len -> n - shift + | NCic.Irl _ -> n - shift | NCic.Ctx tl -> let rec aux k = function | [] -> raise NotInTheList @@ -178,11 +178,22 @@ let pack_lc orig = | _ -> 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 = if n = 0 then [] else - if List.mem (n+shift) restrictions then aux (n-1) - else (NCic.Rel n)::aux (n-1) + if List.mem (n+shift) restrictions then aux (n-1) + else (NCic.Rel n) :: aux (n-1) in pack_lc (shift, NCic.Ctx (List.rev (aux len))) ;; @@ -190,8 +201,13 @@ let mk_restricted_irl shift len restrictions = exception Occur;; let rec force_does_not_occur metasenv subst restrictions t = - let rec aux k (metasenv, subst as ms) = function + let rec aux k ms = function | NCic.Rel r when List.mem (r - k) restrictions -> raise Occur + | NCic.Rel r as orig -> + let amount = + 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 -> (* we ignore the subst since restrict will take care of already * instantiated/restricted metavariabels *) @@ -272,11 +288,11 @@ and restrict metasenv subst i restrictions = force_does_not_occur metasenv subst restrictions bo in let j = newmeta () in let subst_entry_j = j, (name, newctx, newty, newbo) in - let reloc_irl = mk_restricted_irl 0 (List.length ctx) restrictions 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,x) as orig -> if i = n then subst_entry_i else orig) subst, + (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst, j with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf ("Cannot restrict the context of the metavariable ?%d over "^^ @@ -295,10 +311,11 @@ 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 - let reloc_irl = mk_restricted_irl 0 (List.length ctx) restrictions in + 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 List.map - (fun (n,x) as orig -> if i = n then metasenv_entry else orig) + (fun (n,_) as orig -> if i = n then metasenv_entry else orig) metasenv, subst_entry :: subst, j with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf @@ -345,21 +362,34 @@ let delift metasenv subst context n l t = let shift,lc = l in match lc, lc1 with | NCic.Irl len, NCic.Irl len1 - when shift1 < shift || len1 + shift1 > len + shift -> + when shift1 - k < shift || len1 + shift1 - k > len + shift -> + let low_gap = max 0 (shift - (shift1 - k)) in + let high_gap = max 0 (shift1 + len1 - k - (shift + len)) in let restrictions = - HExtlib.list_seq 1 (shift - shift1) @ - HExtlib.list_seq (shift+len+1) (shift1+len1) + HExtlib.list_seq 1 (low_gap+1) @ + HExtlib.list_seq (len1-high_gap) len1 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)); +*) let metasenv, subst, newmeta = restrict metasenv subst i restrictions in - (metasenv, subst), - NCic.Meta(newmeta, mk_restricted_irl shift1 len1 restrictions) - | NCic.Irl len, NCic.Irl len1 when shift = 0 -> ms, orig - | NCic.Irl len, NCic.Irl len1 -> + let meta = + NCic.Meta(newmeta,(k,NCic.Irl (len - low_gap - high_gap))) + in + (metasenv, subst), meta + + | NCic.Irl _, NCic.Irl _ when shift = 0 -> ms, orig + | NCic.Irl _, NCic.Irl _ -> ms, NCic.Meta (i, (shift1 - shift, lc1)) | _ -> - let to_be_restricted = ref [] in let lc1 = NCicUtils.expand_local_context lc1 in let rec deliftl tbr j ms = function | [] -> ms, tbr, [] @@ -372,6 +402,10 @@ let delift metasenv subst context n l t = | 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 if to_be_r = [] then (metasenv, subst), @@ -548,3 +582,48 @@ let delift_rels subst metasenv n t = delift_rels_from subst metasenv 1 n t *) +let mk_meta ?name metasenv context ty = + match ty with + | `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_for_ty, NCic.Implicit (`Typeof n))) in + let m = newmeta () 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 (List.length context))), ty + | `WithType ty -> + let n = newmeta () in + let len = List.length context in + let menv_entry = (n, (name, context, ty)) in + menv_entry :: metasenv, NCic.Meta (n, (0,NCic.Irl len)), ty +;; + +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 (`WithType s) in + let t, metasenv1, args, pno = + aux metasenv1 (NCicSubstitution.subst arg t) + in + if pno + 1 = goal_arity then + ty, metasenv, [], goal_arity+1 + else + t, metasenv1, arg::args, pno+1 + | ty -> + match NCicReduction.whd context ty ~delta with + | NCic.Prod _ as ty -> aux metasenv ty + | ty -> ty, metasenv, [], 0 + in + let res, newmetasenv, arguments, _ = aux metasenv ty in + res, newmetasenv, arguments +;;