From ee2bbb5aa3f13fbea8cd758e69347d9f1f5ed6bb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 Sep 2008 16:36:32 +0000 Subject: [PATCH] snapshot, cicMsubst compiles --- .../components/ng_refiner/nCicMetaSubst.ml | 211 +++++++++++------- .../components/ng_refiner/nCicMetaSubst.mli | 2 +- 2 files changed, 128 insertions(+), 85 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 121131f4d..b5a4646ba 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -155,57 +155,86 @@ exception NotInTheList;; let position n (shift, lc) = match lc with | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList - | NCic.Itl len -> n - shift + | NCic.Irl len -> n - shift | NCic.Ctx tl -> let rec aux k = function | [] -> raise NotInTheList - | (Cic.Rel m)::_ when m + shift = n -> k + | (NCic.Rel m)::_ when m + shift = n -> k | _::tl -> aux (k+1) tl in aux 1 tl ;; +let pack_lc orig = + let rec are_contiguous k = function + | [] -> true + | (NCic.Rel j) :: tl when j = k+1 -> are_contiguous j tl + | _ -> false + in + match orig with + | _, NCic.Ctx [] -> 0, NCic.Irl 0 + | shift, NCic.Ctx (NCic.Rel k::tl as l) when are_contiguous k tl -> + shift+k-1, NCic.Irl (List.length l) + | _ -> orig +;; + +let mk_restricted_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) + in + pack_lc (shift, NCic.Ctx (List.rev (aux len))) +;; + exception Occur;; let rec force_does_not_occur metasenv subst restrictions t = - let rec aux k = function - | C.Rel r when List.mem (r - k) restrictions -> raise Occur - | C.Meta (n, l) as t -> + let rec aux k (metasenv, subst as 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 * instantiated/restricted metavariabels *) - let more_to_be_restricted = ref [] in - let l' = - let i = ref 0 in - HExtlib.map_option - (fun t -> - incr i ; - try - let (*subst, metasenv,*) t = aux k t in Some t - with Occur -> - more_to_be_restricted := !i :: !more_to_be_restricted; None) - l + 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) in - if !more_to_be_restricted = [] then - if l = l' then t else NCic.Meta (n, l') + 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 !more_to_be_restricted + restrict metasenv subst n restrictions_for_n in - (*metasenv, subst,*) NCic.Meta (newmeta, l') - | t -> NCicUtils.map (fun _ k -> k+1) k aux t + (metasenv, subst), NCic.Meta (newmeta, l') + | t -> NCicUtils.map_term_fold_a (fun _ k -> k+1) k aux ms t in - aux 0 t + aux 0 (metasenv,subst) t and force_does_not_occur_in_context metasenv subst restrictions = function | name, NCic.Decl t as orig -> - let metasenv, subst, t' = - force_does_not_occur metasenv subst restrictions t - in + let (metasenv, subst), t' = + force_does_not_occur metasenv subst restrictions t in metasenv, subst, (if t == t' then orig else (name,NCic.Decl t')) | name, NCic.Def (bo, ty) as orig -> - let metasenv, subst, bo' = + let (metasenv, subst), bo' = force_does_not_occur metasenv subst restrictions bo in - let metasenv, subst, ty' = + let (metasenv, subst), ty' = force_does_not_occur metasenv subst restrictions ty in metasenv, subst, (if bo == bo' && ty == ty' then orig else (name, NCic.Def (bo', ty'))) @@ -214,88 +243,96 @@ and erase_in_context metasenv subst pos restrictions = function | [] -> metasenv, subst, restrictions, [] | hd::tl as orig -> let metasenv, subst, restricted, tl' = - erase_in_context metasenv subst (i+1) restrictions tl in - if List.mem i restricted then + erase_in_context metasenv subst (pos+1) restrictions tl in + if List.mem pos restricted then metasenv, subst, restricted, tl' else try let metasenv, subst, hd' = - let delifted_restricted = List.map ((+) ~-i) restricted in - force_does_not_occur_in_context - metasenv susbst delifted_restricted hd + let delifted_restricted = + List.map ((+) ~-pos) (List.filter ((<=) pos) restricted) in + force_does_not_occur_in_context + metasenv subst delifted_restricted hd in metasenv, subst, restricted, (if hd' == hd && tl' == tl then orig else (hd' :: tl')) with Occur -> - metasenv, subst, (i :: restricted), tl' + metasenv, subst, (pos :: restricted), tl' and restrict metasenv subst i restrictions = assert (restrictions <> []); try let name, ctx, bo, ty = NCicUtils.lookup_subst i subst in try - let name, ctx, ty = NCicUtils.lookup_meta i metasenv in let metasenv, subst, restrictions, newctx = - erase_in_context metasenv subst 1 restrictions in - let metasenv, subst, _ = + erase_in_context metasenv subst 1 restrictions ctx in + let (metasenv, subst), newty = force_does_not_occur metasenv subst restrictions ty in - let metasenv, subst, _ = + let (metasenv, subst), newbo = force_does_not_occur metasenv subst restrictions bo in - (* we don't care newly generated bo/tys since up to subst they are - * convertible (only metas are substituted for metas *) - metasenv, subst, ? + 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 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, + 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 "^^ "with %s and at least one of the hypotheses occurs in "^^ - "the substituted term" i (String.concat ", " + "the substituted term") i (String.concat ", " (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)) i - (NCicPp.ppterm ~metasenv ~subst ~context:ctx bo))))) + (NCicPp.ppterm ~metasenv ~subst ~context:ctx bo)))) with NCicUtils.Subst_not_found _ -> try let name, ctx, ty = NCicUtils.lookup_meta i metasenv in - let metasenv, subst, restrictions, newctx = - erase_in_context metasenv subst 1 restrictions in - let metasenv, subst, newty = - force_does_not_occur metasenv subst restrictions ty in - let j = newmeta () in - let metasenv_entry = j, (name, newctx, newty) in - let subst_entry = i,(name,ctx, NCic.Meta (j, irl - restrictions), ty) in - List.map - (fun (n,x) as orig -> if i = n then metasenv_entry else orig) metasenv, - subst_entry :: subst, j + try + let metasenv, subst, restrictions, newctx = + erase_in_context metasenv subst 1 restrictions ctx in + let (metasenv, subst), newty = + 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 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) + metasenv, + subst_entry :: subst, j + with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf + ("Cannot restrict the context of the metavariable ?%d "^^ + "over the hypotheses %s since metavariable's type depends "^^ + "on at least one of them") i (String.concat ", " + (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions))))) with | NCicUtils.Meta_not_found _ -> assert false - | Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf - ("Cannot restrict the context of the metavariable ?%d "^^ - "over the hypotheses %s since metavariable's type depends "^^ - "on at least one of them" i (String.concat ", " - (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)))))) +;; (* 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 to_be_restricted = ref [] in - let rec aux k = function - | NCic.Rel n as t when n <= k -> t + let rec aux k (metasenv, subst as ms) = function + | 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 C.Rel ((position (n-k) l) + k) + (try ms, NCic.Rel ((position (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 (NCicSubstitution.lift n bo)) - | _,NCic.Decl _ -> NCic.Rel ((position (n-k) l) + k) + 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 (i,l1) as orig -> (try - let _,_,t,_ = NCicUtil.lookup_subst i subst in - aux k (NCicSubstitution.subst_meta l1 t) - with NCicUtil.Subst_not_found _ -> + let _,_,t,_ = NCicUtils.lookup_subst i subst in + aux k ms (NCicSubstitution.subst_meta l1 t) + with NCicUtils.Subst_not_found _ -> (* see the top level invariant *) if (i = n) then raise (MetaSubstFailure (lazy (Printf.sprintf ( @@ -313,33 +350,39 @@ let delift metasenv subst context n l t = HExtlib.list_seq 1 (shift - shift1) @ HExtlib.list_seq (shift+len+1) (shift1+len1) in - let subst, metasenv, newmeta = + let metasenv, subst, newmeta = restrict metasenv subst i restrictions in - (* return that meta *) - assert false - | NCic.Irl len, NCic.Irl len1 when shift = 0 -> orig + (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.Meta (i, (shift1 - shift, lc1)) + ms, NCic.Meta (i, (shift1 - shift, lc1)) | _ -> + let to_be_restricted = ref [] in let lc1 = NCicUtils.expand_local_context lc1 in - let rec deliftl j = function - | [] -> [] + let rec deliftl tbr j ms = function + | [] -> ms, tbr, [] | t::tl -> - let tl = deliftl (j+1) tl in - try (aux (k+shift1) t)::tl + let ms, tbr, tl = deliftl tbr (j+1) ms tl in + try + let ms, t = aux (k-shift1) ms t in + ms, tbr, t::tl with - | NotInTheList | MetaSubstFailure _ -> - to_be_restricted := (i,j)::!to_be_restricted; - tl + | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl in - let l1 = deliftl 1 l1 in - C.Meta(i,l1)) (* or another ?k and possibly compress l1 *) - | t -> NCicUtils.map (fun _ k -> k+1) k aux t + let (metasenv, subst), to_be_r, lc1' = deliftl [] 1 ms lc1 in + let l1 = pack_lc (shift, NCic.Ctx lc1') in + if to_be_r = [] then + (metasenv, subst), + (if lc1' = lc1 then orig else NCic.Meta (i,l1)) + else + 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 in - let t = aux 0 t in - let metasenv, subst = restrict subst !to_be_restricted metasenv in - metasenv, subst, t + aux 0 (metasenv,subst) t ;; (* diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli index 322330488..8f03ccb11 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.mli +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -45,5 +45,5 @@ val restrict : val delift : NCic.metasenv -> NCic.substitution -> NCic.context -> int -> NCic.local_context -> NCic.term -> - Cic.metasenv * Cic.substitution * Cic.term + (NCic.metasenv * NCic.substitution) * NCic.term -- 2.39.2