X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=9cc6ac67c755c16e4208413f1cd7565859c64557;hb=942ec766879070892420f6297b5c078c1582b78d;hp=1a2b5471b0cf76910eb0666c1cba0fb96a59b7bb;hpb=d174e54c365ab9df38367de9336c213a03be3c27;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 1a2b5471b..9cc6ac67c 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -14,9 +14,10 @@ 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;; @@ -71,31 +72,41 @@ 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 -> - (* 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) + let meta_chain = + try + Some (NCicUtils.lookup_subst n subst) + with + NCicUtils.Subst_not_found _ -> None 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') + (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')) | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t in aux 0 (metasenv,subst) t @@ -204,8 +215,6 @@ let rec flexible_arg subst = function | _ -> 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 ;; @@ -220,30 +229,58 @@ let int_of_out_scope_tag tag = ;; +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 ~unify metasenv subst context n l t = - let unify_list in_scope = + 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 then None else + 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 - match unify metasenv subst context li t with - | Some (metasenv,subst) -> - Some ((metasenv, subst), NCic.Rel (i+1+k)) - | None -> None) + 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 in_scope metasenv subst context k t with + 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 -> @@ -266,12 +303,18 @@ let delift ~unify metasenv subst context n l t = (NCicPp.ppterm ~context ~metasenv ~subst t)))) | NCic.Meta (i,l1) as orig -> (try - let tag,_,t,_ = NCicUtils.lookup_subst i subst in - let in_scope = + 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 - | Some tag when is_out_scope_tag tag -> int_of_out_scope_tag tag - | _ -> in_scope + | 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 _ -> @@ -368,6 +411,10 @@ let delift ~unify metasenv subst context n l 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 (context,0,0) (metasenv,subst) t with NotInTheList -> @@ -386,10 +433,7 @@ let delift ~unify 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