X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=188d4dc207ff4bf8e4f47d4bf28d8407b12be214;hb=b0b6b600e029435bfce53f41cd267c669a1f8dc2;hp=b5a4646baba5160bbe940c44d84c38ca8e194b4f;hpb=ee2bbb5aa3f13fbea8cd758e69347d9f1f5ed6bb;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index b5a4646ba..188d4dc20 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 @@ -190,7 +190,7 @@ 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.Meta (n, l) as orig -> (* we ignore the subst since restrict will take care of already @@ -222,7 +222,7 @@ let rec force_does_not_occur metasenv subst restrictions t = restrict metasenv subst n restrictions_for_n in (metasenv, subst), NCic.Meta (newmeta, l') - | t -> NCicUtils.map_term_fold_a (fun _ k -> k+1) k aux ms t + | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t in aux 0 (metasenv,subst) t @@ -276,7 +276,7 @@ and restrict metasenv subst i restrictions = 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 "^^ @@ -298,7 +298,7 @@ and restrict metasenv subst i restrictions = let reloc_irl = mk_restricted_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 @@ -355,11 +355,10 @@ let delift metasenv subst context n l t = 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 -> + | 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, [] @@ -380,52 +379,33 @@ 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 -> NCicUtils.map_term_fold_a (fun _ k -> k+1) k aux ms t + | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t in - aux 0 (metasenv,subst) t -;; - -(* - in - let res = - try - deliftaux 0 t - with - NotInTheList -> + try aux 0 (metasenv,subst) t + with NotInTheList -> (* This is the case where we fail even first order unification. *) (* The reason is that our delift function is weaker than first *) (* order (in the sense of alpha-conversion). See comment above *) (* related to the delift function. *) -(* debug_print (lazy "First Order UnificationFailure during delift") ; -debug_print(lazy (sprintf - "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" - (ppterm subst t) - (String.concat "; " - (List.map - (function Some t -> ppterm subst t | None -> "_") l - )))); *) - let msg = (lazy (sprintf - "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" - (ppterm ~metasenv subst t) - (String.concat "; " - (List.map - (function Some t -> ppterm ~metasenv subst t | None -> "_") - l)))) + let msg = (lazy (Printf.sprintf + ("Error trying to abstract %s over [%s]: the algorithm only tried to "^^ + "abstract over bound variables") (NCicPp.ppterm ~metasenv ~subst + ~context t) (String.concat "; " (List.map (NCicPp.ppterm ~metasenv + ~subst ~context) (let shift, lc = l in List.map (NCicSubstitution.lift + shift) (NCicUtils.expand_local_context lc)))))) in + let shift, lc = l in + let lc = NCicUtils.expand_local_context lc in + let l = List.map (NCicSubstitution.lift shift) lc in if List.exists - (function - Some t -> CicUtil.is_meta_closed (apply_subst subst t) - | None -> true) l + (fun t -> NCicUntrusted.metas_of_term subst context t = []) + l then raise (Uncertain msg) else raise (MetaSubstFailure msg) - in - let (metasenv, subst) = restrict subst !to_be_restricted metasenv in - res, metasenv, subst ;; -*) (* (* delifts a term t of n levels strating from k, that is changes (Rel m) @@ -567,3 +547,30 @@ let delift_rels subst metasenv n t = delift_rels_from subst metasenv 1 n t *) +let mk_meta ?name metasenv context 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)) +;; + +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 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 +;;