- raise (MetaSubstFailure (lazy (sprintf
- "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
- n (names_of_context_indexes context to_be_restricted)))))
- metasenv ([], [])
- in
- let (more_to_be_restricted', subst) = (* restrict subst *)
- List.fold_right
- (* TODO: cambiare dopo l'aggiunta del ty *)
- (fun (n, (context, term,ty)) (more, subst') ->
- let to_be_restricted =
- List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
- in
- (try
- let (more_to_be_restricted, restricted, context') =
- (* just an optimization *)
- if to_be_restricted = [] then
- [], [], context
- else
- erase 1 to_be_restricted n context
- in
- let more_to_be_restricted', term' =
- force_does_not_occur subst restricted term
- in
- let more_to_be_restricted'', ty' =
- force_does_not_occur subst restricted ty in
- let subst' = (n, (context', term',ty')) :: subst' in
- let more =
- more @ more_to_be_restricted
- @ more_to_be_restricted'@more_to_be_restricted'' in
- (more, subst')
- with Occur ->
- let error_msg = lazy (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"
- n (names_of_context_indexes context to_be_restricted) n
- (ppterm ~metasenv subst term))
- in
- (* DEBUG
- debug_print (lazy error_msg);
- debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst)));
- debug_print (lazy ("subst = \n" ^ (ppsubst subst)));
- debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *)
- raise (MetaSubstFailure error_msg)))
- subst ([], [])
- in
- restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv
+ 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 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 (metasenv, subst), newbo =
+ force_does_not_occur metasenv subst restrictions bo in
+ 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,_) 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 ", "
+ (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)) i
+ (NCicPp.ppterm ~metasenv ~subst ~context:ctx bo))))
+ with NCicUtils.Subst_not_found _ ->
+ try
+ let name, ctx, ty = NCicUtils.lookup_meta i metasenv in
+ 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,_) 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