-(*CSC: this restriction function is utterly wrong, since it does not check *)
-(*CSC: that the variable that is going to be restricted does not occur free *)
-(*CSC: in a part of the sequent that is not going to be restricted. *)
-(*CSC: In particular, the whole approach is wrong; if restriction can fail *)
-(*CSC: (as indeed it is the case), we can not collect all the restrictions *)
-(*CSC: and restrict everything at the end ;-( *)
-let restrict to_be_restricted =
- let rec erase i n =
- function
- [] -> []
- | _::tl when List.mem (n,i) to_be_restricted ->
- None::(erase (i+1) n tl)
- | he::tl -> he::(erase (i+1) n tl) in
- let rec aux =
- function
- [] -> []
- | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
- aux
+let rec restrict subst to_be_restricted metasenv =
+ let names_of_context_indexes context indexes =
+ String.concat ", "
+ (List.map
+ (fun i ->
+ try
+ match List.nth context i with
+ | None -> assert false
+ | Some (n, _) -> CicPp.ppname n
+ with
+ Failure _ -> assert false
+ ) indexes)
+ in
+ let force_does_not_occur_in_context to_be_restricted = function
+ | None -> [], None
+ | Some (name, Cic.Decl t) ->
+ let (more_to_be_restricted, t') =
+ force_does_not_occur subst to_be_restricted t
+ in
+ more_to_be_restricted, Some (name, Cic.Decl t')
+ | Some (name, Cic.Def (bo, ty)) ->
+ let (more_to_be_restricted, bo') =
+ force_does_not_occur subst to_be_restricted bo
+ in
+ let more_to_be_restricted, ty' =
+ match ty with
+ | None -> more_to_be_restricted, None
+ | Some ty ->
+ let more_to_be_restricted', ty' =
+ force_does_not_occur subst to_be_restricted ty
+ in
+ more_to_be_restricted @ more_to_be_restricted',
+ Some ty'
+ in
+ more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
+ in
+ let rec erase i to_be_restricted n = function
+ | [] -> [], to_be_restricted, []
+ | hd::tl ->
+ let more_to_be_restricted,restricted,tl' =
+ erase (i+1) to_be_restricted n tl
+ in
+ let restrict_me = List.mem i restricted in
+ if restrict_me then
+ more_to_be_restricted, restricted, None:: tl'
+ else
+ (try
+ let more_to_be_restricted', hd' =
+ let delifted_restricted =
+ let rec aux =
+ function
+ [] -> []
+ | j::tl when j > i -> (j - i)::aux tl
+ | _::tl -> aux tl
+ in
+ aux restricted
+ in
+ force_does_not_occur_in_context delifted_restricted hd
+ in
+ more_to_be_restricted @ more_to_be_restricted',
+ restricted, hd' :: tl'
+ with Occur ->
+ more_to_be_restricted, (i :: restricted), None :: tl')
+ in
+ let (more_to_be_restricted, metasenv, subst) =
+ List.fold_right
+ (fun (n, context, t) (more, metasenv, subst) ->
+ let to_be_restricted =
+ List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
+ in
+ 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
+ try
+ let more_to_be_restricted', t' =
+ force_does_not_occur subst restricted t
+ in
+ let metasenv' = (n, context', t') :: metasenv in
+ (try
+ let s = List.assoc n subst in
+ try
+ let more_to_be_restricted'', s' =
+ force_does_not_occur subst restricted s
+ in
+ let subst' = (n, s') :: (List.remove_assoc n subst) in
+ let more =
+ more @ more_to_be_restricted @ more_to_be_restricted' @
+ more_to_be_restricted''
+ in
+ (more, metasenv', subst')
+ with Occur ->
+ raise (MetaSubstFailure (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
+ (CicPp.ppterm s)))
+ with Not_found -> (more @ more_to_be_restricted @ more_to_be_restricted', metasenv', subst))
+ with Occur ->
+ raise (MetaSubstFailure (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 ([], [], subst)
+ in
+ match more_to_be_restricted with
+ | [] -> (metasenv, subst)
+ | _ -> restrict subst more_to_be_restricted metasenv