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')))
| [] -> 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 (
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
;;
(*
projects / helm.git / commitdiff