X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=26dc85cacebadc948661b90ae084159a7499ba78;hb=c22f39a5d5afc0ef55beb221e00e2e6703b13d90;hp=6a0406747abba552d2811eb2337b44055b79d83a;hpb=002d456397be2f0046bb50356e80816f7296647d;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 6a0406747..26dc85cac 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -14,24 +14,27 @@ exception MetaSubstFailure of string Lazy.t exception Uncertain of string Lazy.t -let newmeta = +let newmeta,maxmeta = let maxmeta = ref 0 in - fun () -> incr maxmeta; !maxmeta + (fun () -> incr maxmeta; !maxmeta), + (fun () -> !maxmeta) ;; exception NotInTheList;; -let position n (shift, lc) = +let position to_skip n (shift, lc) = match lc with + | NCic.Irl _ when to_skip > 0 -> assert false (* unclear to me *) | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList | NCic.Irl _ -> n - shift | NCic.Ctx tl -> - let rec aux k = function + let rec aux to_skip k = function | [] -> raise NotInTheList + | _ :: tl when to_skip > 0 -> aux (to_skip - 1) (k+1) tl | (NCic.Rel m)::_ when m + shift = n -> k - | _::tl -> aux (k+1) tl + | _::tl -> aux to_skip (k+1) tl in - aux 1 tl + aux to_skip 1 tl ;; let pack_lc orig = @@ -193,23 +196,96 @@ and restrict metasenv subst i restrictions = | NCicUtils.Meta_not_found _ -> assert false ;; +let rec flexible_arg subst = function + | NCic.Meta (i,_) | NCic.Appl (NCic.Meta (i,_) :: _)-> + (try + let _,_,t,_ = List.assoc i subst in + flexible_arg subst t + with Not_found -> true) + | _ -> false +;; + +let flexible subst l = List.exists (flexible_arg subst) l;; + +let in_scope_tag = "tag:in_scope" ;; +let out_scope_tag_prefix = "tag:out_scope:" +let out_scope_tag n = out_scope_tag_prefix ^ string_of_int n ;; +let is_out_scope_tag tag = + String.length tag > String.length out_scope_tag_prefix && + String.sub tag 0 (String.length out_scope_tag_prefix) = out_scope_tag_prefix +;; +let int_of_out_scope_tag tag = + int_of_string + (String.sub tag (String.length out_scope_tag_prefix) + (String.length tag - (String.length out_scope_tag_prefix))) +;; + + +exception Found;; + (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), otherwise the occur check does not make sense in case of unification of ?n with ?n *) -let delift metasenv subst context n l t = - let rec aux k (metasenv, subst as ms) = function +let delift ~unify metasenv subst context n l t = + let is_in_scope_meta subst = function + | NCic.Meta (i,_) -> + (try + let tag, _, _, _ = NCicUtils.lookup_subst i subst in + tag = Some in_scope_tag + with NCicUtils.Subst_not_found _ -> false) + | _ -> false + in + let contains_in_scope subst t = + let rec aux _ () = function + | NCic.Meta _ as t -> + if is_in_scope_meta subst t then raise Found + else () + | t -> + if is_in_scope_meta subst t then raise Found + else NCicUtils.fold (fun _ () -> ()) () aux () t + in + try aux () () t; false with Found -> true + in + let unify_list ~alpha in_scope = + match l with + | _, NCic.Irl _ -> fun _ _ _ _ _ -> None + | shift, NCic.Ctx l -> fun metasenv subst context k t -> + if flexible_arg subst t || contains_in_scope subst t then None else + let lb = List.map (fun t -> t, flexible_arg subst t) l in + HExtlib.list_findopt + (fun (li,flexible) i -> + if flexible || i < in_scope then None else + let li = NCicSubstitution.lift (k+shift) li in + if alpha then + if NCicReduction.alpha_eq metasenv subst context li t then + Some ((metasenv,subst), NCic.Rel (i+1+k)) + else + None + else + match unify metasenv subst context li t with + | Some (metasenv,subst) -> + Some ((metasenv, subst), NCic.Rel (i+1+k)) + | None -> None) + lb + in + let rec aux (context,k,in_scope) (metasenv, subst as ms) t = + match unify_list ~alpha:true in_scope metasenv subst context k t with + | Some x -> x + | None -> + try + match t with | NCic.Rel n as t when n <= k -> ms, t | NCic.Rel n -> (try match List.nth context (n-k-1) with | _,NCic.Def (bo,_) -> - (try ms, NCic.Rel ((position (n-k) l) + k) + (try ms, NCic.Rel ((position in_scope (n-k) l) + k) with NotInTheList -> (* CSC: This bit of reduction hurts performances since it is * possible to have an exponential explosion of the size of the * proof. required for nat/nth_prime.ma *) - aux k ms (NCicSubstitution.lift n bo)) - | _,NCic.Decl _ -> ms, NCic.Rel ((position (n-k) l) + k) + aux (context,k,in_scope) ms (NCicSubstitution.lift n bo)) + | _,NCic.Decl _ -> ms, NCic.Rel ((position in_scope (n-k) l) + k) with Failure _ -> assert false) (*Unbound variable found in delift*) | NCic.Meta (i,_) when i=n -> raise (MetaSubstFailure (lazy (Printf.sprintf ( @@ -219,8 +295,20 @@ let delift metasenv subst context n l t = (NCicPp.ppterm ~context ~metasenv ~subst t)))) | NCic.Meta (i,l1) as orig -> (try - let _,_,t,_ = NCicUtils.lookup_subst i subst in - aux k ms (NCicSubstitution.subst_meta l1 t) + let tag,c,t,ty = NCicUtils.lookup_subst i subst in + let in_scope, clear = + match tag with + | Some tag when tag = in_scope_tag -> 0, true + | Some tag when is_out_scope_tag tag->int_of_out_scope_tag tag,true + | _ -> in_scope, false + in + let ms = + if not clear then ms + else + metasenv, + (i,(None,c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst + in + aux (context,k,in_scope) ms (NCicSubstitution.subst_meta l1 t) with NCicUtils.Subst_not_found _ -> if snd l1 = NCic.Irl 0 || snd l1 = NCic.Ctx [] then ms, orig else @@ -289,7 +377,7 @@ let delift metasenv subst context n l t = | t::tl -> let ms, tbr, tl = deliftl tbr (j+1) ms tl in try - let ms, t = aux k ms t in + let ms, t = aux (context,k,in_scope) ms t in ms, tbr, t::tl with | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl @@ -312,9 +400,15 @@ let delift metasenv subst context n l t = 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 + | t -> + NCicUntrusted.map_term_fold_a + (fun e (c,k,s) -> (e::c,k+1,s)) (context,k,in_scope) aux ms t + with NotInTheList -> + match unify_list ~alpha:false in_scope metasenv subst context k t with + | Some x -> x + | None -> raise NotInTheList in - try aux 0 (metasenv,subst) t + try aux (context,0,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 *) @@ -331,10 +425,7 @@ let delift metasenv subst context n l t = let lc = NCicUtils.expand_local_context lc in let l = List.map (NCicSubstitution.lift shift) lc in if - List.exists - (fun t -> - NCicUntrusted.metas_of_term subst context t = []) - l + List.exists (fun t-> NCicUntrusted.metas_of_term subst context t = []) l then raise (Uncertain msg) else @@ -347,16 +438,16 @@ let mk_meta ?name metasenv context ty = | `WithType ty -> 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 + menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty | `Sort -> let ty = NCic.Implicit (`Typeof n) in mk_meta (tyof name) n metasenv [] (`WithType ty) | `Type -> - let metasenv, ty, _ = + let metasenv, _, ty, _ = mk_meta (tyof name) (newmeta ()) metasenv context `Sort in mk_meta name n metasenv context (`WithType ty) | `Term -> - let metasenv, ty, _ = + let metasenv, _, ty, _ = mk_meta (tyof name) (newmeta ()) metasenv context `Type in mk_meta name n metasenv context (`WithType ty) in @@ -366,8 +457,8 @@ let mk_meta ?name metasenv context ty = let saturate ?(delta=0) metasenv subst context ty goal_arity = assert (goal_arity >= 0); let rec aux metasenv = function - | NCic.Prod (name,s,t) -> - let metasenv1, arg,_ = + | NCic.Prod (name,s,t) as ty -> + let metasenv1, _, arg,_ = mk_meta ~name:name metasenv context (`WithType s) in let t, metasenv1, args, pno = aux metasenv1 (NCicSubstitution.subst arg t)