| NCic.Meta (n, (shift,lc as l)) as orig ->
(try
let _,_,bo,_ = NCicUtils.lookup_subst n subst in
| NCic.Meta (n, (shift,lc as l)) as orig ->
(try
let _,_,bo,_ = NCicUtils.lookup_subst n subst in
with
NCicUtils.Subst_not_found _ ->
(* we ignore the subst since restrict will take care of already
* instantiated/restricted metavariabels *)
let l = NCicUtils.expand_local_context lc in
with
NCicUtils.Subst_not_found _ ->
(* we ignore the subst since restrict will take care of already
* instantiated/restricted metavariabels *)
let l = NCicUtils.expand_local_context lc in
let (metasenv,subst as ms), _, restrictions_for_n, l' =
List.fold_right
(fun t (ms, i, restrictions_for_n, l) ->
try
(*pp (lazy ("L'ORLO DELLA FOSSA: k= " ^ string_of_int k ^ " shift=" ^
let (metasenv,subst as ms), _, restrictions_for_n, l' =
List.fold_right
(fun t (ms, i, restrictions_for_n, l) ->
try
(*pp (lazy ("L'ORLO DELLA FOSSA: k= " ^ string_of_int k ^ " shift=" ^
ms, i-1, restrictions_for_n, t::l
with Occur ->
ms, i-1, i::restrictions_for_n, l)
ms, i-1, restrictions_for_n, t::l
with Occur ->
ms, i-1, i::restrictions_for_n, l)
in
if restrictions_for_n = [] then
ms, if sl = l' then orig else (
in
if restrictions_for_n = [] then
ms, if sl = l' then orig else (
~context:[] (NCic.Meta (n,pack_lc (0, NCic.Ctx l')))));*)
NCic.Meta (n, pack_lc (0, NCic.Ctx l'))
)
~context:[] (NCic.Meta (n,pack_lc (0, NCic.Ctx l')))));*)
NCic.Meta (n, pack_lc (0, NCic.Ctx l'))
)
let l' = pack_lc (0, NCic.Ctx l') in
let _ = pp (lazy ("restrictions for n are:" ^ String.concat "," (List.map string_of_int restrictions_for_n))) in
let metasenv, subst, newmeta, more_restricted =
let l' = pack_lc (0, NCic.Ctx l') in
let _ = pp (lazy ("restrictions for n are:" ^ String.concat "," (List.map string_of_int restrictions_for_n))) in
let metasenv, subst, newmeta, more_restricted =
let _ = pp (lazy ("more restricted: " ^String.concat "," (List.map string_of_int more_restricted))) in
let l' = purge_restricted restrictions more_restricted l' in
(metasenv, subst), NCic.Meta (newmeta, l'))
let _ = pp (lazy ("more restricted: " ^String.concat "," (List.map string_of_int more_restricted))) in
let l' = purge_restricted restrictions more_restricted l' in
(metasenv, subst), NCic.Meta (newmeta, l'))
"\nCCC: restrictions are:" ^ String.concat "," (List.map string_of_int restrictions)));*)
let (metasenv, subst), t' =
"\nCCC: restrictions are:" ^ String.concat "," (List.map string_of_int restrictions)));*)
let (metasenv, subst), t' =
metasenv, subst, (if t == t' then orig else (name,NCic.Decl t'))
| name, NCic.Def (bo, ty) as orig ->
let (metasenv, subst), bo' =
metasenv, subst, (if t == t' then orig else (name,NCic.Decl t'))
| name, NCic.Def (bo, ty) as orig ->
let (metasenv, subst), bo' =
| [] -> metasenv, subst, restrictions, []
| hd::tl as orig ->
let metasenv, subst, restricted, tl' =
| [] -> metasenv, subst, restrictions, []
| hd::tl as orig ->
let metasenv, subst, restricted, tl' =
if List.mem pos restricted then
metasenv, subst, restricted, tl'
else
if List.mem pos restricted then
metasenv, subst, restricted, tl'
else
let delifted_restricted =
List.map ((+) ~-pos) (List.filter ((<=) pos) restricted) in
force_does_not_occur_in_context
let delifted_restricted =
List.map ((+) ~-pos) (List.filter ((<=) pos) restricted) in
force_does_not_occur_in_context
in
metasenv, subst, restricted,
(if hd' == hd && tl' == tl then orig else (hd' :: tl'))
with Occur ->
metasenv, subst, (pos :: restricted), tl'
in
metasenv, subst, restricted,
(if hd' == hd && tl' == tl then orig else (hd' :: tl'))
with Occur ->
metasenv, subst, (pos :: restricted), tl'
assert (restrictions <> []);
try
let name, ctx, bo, ty = NCicUtils.lookup_subst i subst in
try
let metasenv, subst, restrictions, newctx =
assert (restrictions <> []);
try
let name, ctx, bo, ty = NCicUtils.lookup_subst i subst in
try
let metasenv, subst, restrictions, newctx =
let j = newmeta () in
let subst_entry_j = j, (name, newctx, newbo, newty) in
let reloc_irl = mk_perforated_irl 0 (List.length ctx) restrictions in
let j = newmeta () in
let subst_entry_j = j, (name, newctx, newbo, newty) in
let reloc_irl = mk_perforated_irl 0 (List.length ctx) restrictions in
"with %s and at least one of the hypotheses occurs in "^^
"the substituted term") i (String.concat ", "
(List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)) i
"with %s and at least one of the hypotheses occurs in "^^
"the substituted term") i (String.concat ", "
(List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)) i
with NCicUtils.Subst_not_found _ ->
try
let name, ctx, ty = NCicUtils.lookup_meta i metasenv in
try
let metasenv, subst, restrictions, newctx =
with NCicUtils.Subst_not_found _ ->
try
let name, ctx, ty = NCicUtils.lookup_meta i metasenv in
try
let metasenv, subst, restrictions, newctx =
let j = newmeta () in
let metasenv_entry = j, (name, newctx, newty) in
let reloc_irl =
let j = newmeta () in
let metasenv_entry = j, (name, newctx, newty) in
let reloc_irl =
| NCic.Meta (i,_) ->
(try
let _,_,t,_ = List.assoc i subst in
| NCic.Meta (i,_) ->
(try
let _,_,t,_ = List.assoc i subst in
with Not_found -> true)
| NCic.Appl (NCic.Meta (i,_) :: args)->
(try
let _,_,t,_ = List.assoc i subst in
with Not_found -> true)
| NCic.Appl (NCic.Meta (i,_) :: args)->
(try
let _,_,t,_ = List.assoc i subst in
(* 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 *)
(* 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 *)
match l with
| _, NCic.Irl _ -> fun _ _ _ _ _ -> None
| shift, NCic.Ctx l -> fun metasenv subst context k t ->
match l with
| _, NCic.Irl _ -> fun _ _ _ _ _ -> None
| shift, NCic.Ctx l -> fun metasenv subst context k t ->
- let t = NCicSubstitution.lift (k+shift) t in
- t, is_flexible context ~subst t)
+ let t = NCicSubstitution.lift status (k+shift) t in
+ t, is_flexible status context ~subst t)
(* 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 *)
(* 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 *)
| _,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 ->
| _,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 ->
"Cannot unify the metavariable ?%d with a term that has "^^
"as subterm %s in which the same metavariable "^^
"occurs (occur check)") i
"Cannot unify the metavariable ?%d with a term that has "^^
"as subterm %s in which the same metavariable "^^
"occurs (occur check)") i
| NCic.Meta (i,l1) as orig ->
(try
let tag,c,t,ty = NCicUtils.lookup_subst i subst in
| NCic.Meta (i,l1) as orig ->
(try
let tag,c,t,ty = NCicUtils.lookup_subst i subst in
metasenv,
(i,([],c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst
in
metasenv,
(i,([],c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst
in
with NCicUtils.Subst_not_found _ ->
if snd l1 = NCic.Irl 0 || snd l1 = NCic.Ctx [] then ms, orig
else
with NCicUtils.Subst_not_found _ ->
if snd l1 = NCic.Irl 0 || snd l1 = NCic.Ctx [] then ms, orig
else
when shift1 + len1 < shift || shift1 > shift + len ->
let restrictions = HExtlib.list_seq 1 (len1 + 1) in
let metasenv, subst, newmeta, more_restricted =
when shift1 + len1 < shift || shift1 > shift + len ->
let restrictions = HExtlib.list_seq 1 (len1 + 1) in
let metasenv, subst, newmeta, more_restricted =
let l' = (0,NCic.Irl (max 0 (k-shift1))) in
let l' = purge_restricted restrictions more_restricted l' in
(metasenv, subst),NCic.Meta (newmeta,l')
let l' = (0,NCic.Irl (max 0 (k-shift1))) in
let l' = purge_restricted restrictions more_restricted l' in
(metasenv, subst),NCic.Meta (newmeta,l')
else ms, NCic.Meta (i, (new_shift, lc1))
else
let metasenv, subst, newmeta, more_restricted =
else ms, NCic.Meta (i, (new_shift, lc1))
else
let metasenv, subst, newmeta, more_restricted =
let newlc_len = len1 - List.length restrictions in
let l' = new_shift, NCic.Irl newlc_len in
let l' = purge_restricted restrictions more_restricted l' in
let newlc_len = len1 - List.length restrictions in
let l' = new_shift, NCic.Irl newlc_len in
let l' = purge_restricted restrictions more_restricted l' in
pp (lazy ("TO BE RESTRICTED: " ^
(String.concat "," (List.map string_of_int to_be_r))));
let l1 = pack_lc (0, NCic.Ctx lc1') in
pp (lazy ("TO BE RESTRICTED: " ^
(String.concat "," (List.map string_of_int to_be_r))));
let l1 = pack_lc (0, 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, more_restricted =
if to_be_r = [] then
(metasenv, subst),
(if lc1' = lc1 then orig else NCic.Meta (i,l1))
else
let metasenv, subst, newmeta, more_restricted =
let l1 = purge_restricted to_be_r more_restricted l1 in
(metasenv, subst), NCic.Meta(newmeta,l1))
| t ->
let l1 = purge_restricted to_be_r more_restricted l1 in
(metasenv, subst), NCic.Meta(newmeta,l1))
| t ->
(fun e (c,k,s) -> (e::c,k+1,s)) (context,k,in_scope) aux ms t
in
(*
(fun e (c,k,s) -> (e::c,k+1,s)) (context,k,in_scope) aux ms t
in
(*
(* related to the delift function. *)
let msg = (lazy (Printf.sprintf
("Error trying to abstract %s over [%s]: the algorithm only tried to "^^
(* related to the delift function. *)
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
+ "abstract over bound variables") (status#ppterm ~metasenv ~subst
+ ~context t) (String.concat "; " (List.map (status#ppterm ~metasenv
assert (goal_arity >= 0);
let rec aux metasenv = function
| NCic.Prod (name,s,t) as ty ->
let metasenv1, _, arg,_ =
mk_meta ~attrs:[`Name name] metasenv context ~with_type:s `IsTerm in
let t, metasenv1, args, pno =
assert (goal_arity >= 0);
let rec aux metasenv = function
| NCic.Prod (name,s,t) as ty ->
let metasenv1, _, arg,_ =
mk_meta ~attrs:[`Name name] metasenv context ~with_type:s `IsTerm in
let t, metasenv1, args, pno =
in
if pno + 1 = goal_arity then
ty, metasenv, [], goal_arity+1
else
t, metasenv1, arg::args, pno+1
| ty ->
in
if pno + 1 = goal_arity then
ty, metasenv, [], goal_arity+1
else
t, metasenv1, arg::args, pno+1
| ty ->
| NCic.Prod _ as ty -> aux metasenv ty
| ty -> ty, metasenv, [], 0
in
| NCic.Prod _ as ty -> aux metasenv ty
| ty -> ty, metasenv, [], 0
in