-let rec force_does_not_occur subst to_be_restricted t =
- let module C = Cic in
- let more_to_be_restricted = ref [] in
- let rec aux k = function
- C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur
- | C.Rel _
- | C.Sort _ as t -> t
- | C.Implicit _ -> assert false
- | C.Meta (n, l) ->
- (* we do not retrieve the term associated to ?n in subst since *)
- (* in this way we can restrict if something goes wrong *)
- let l' =
- let i = ref 0 in
- List.map
- (function t ->
- incr i ;
- match t with
- None -> None
- | Some t ->
- try
- Some (aux k t)
- with Occur ->
- more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
- None)
- l
- in
- C.Meta (n, l')
- | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
- | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
- | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
- | C.LetIn (name,so,ty,dest) ->
- C.LetIn (name, aux k so, aux k ty, aux (k+1) dest)
- | C.Appl l -> C.Appl (List.map (aux k) l)
- | C.Var (uri,exp_named_subst) ->
- let exp_named_subst' =
- List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
- in
- C.Var (uri, exp_named_subst')
- | C.Const (uri, exp_named_subst) ->
- let exp_named_subst' =
- List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
- in
- C.Const (uri, exp_named_subst')
- | C.MutInd (uri,tyno,exp_named_subst) ->
- let exp_named_subst' =
- List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
- in
- C.MutInd (uri, tyno, exp_named_subst')
- | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
- let exp_named_subst' =
- List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
- in
- C.MutConstruct (uri, tyno, consno, exp_named_subst')
- | C.MutCase (uri,tyno,out,te,pl) ->
- C.MutCase (uri, tyno, aux k out, aux k te, List.map (aux k) pl)
- | C.Fix (i,fl) ->
- let len = List.length fl in
- let k_plus_len = k + len in
- let fl' =
- List.map
- (fun (name,j,ty,bo) -> (name, j, aux k ty, aux k_plus_len bo)) fl
- in
- C.Fix (i, fl')
- | C.CoFix (i,fl) ->
- let len = List.length fl in
- let k_plus_len = k + len in
- let fl' =
- List.map
- (fun (name,ty,bo) -> (name, aux k ty, aux k_plus_len bo)) fl
- in
- C.CoFix (i, fl')
- in
- let res = aux 0 t in
- (!more_to_be_restricted, res)
-
-let rec restrict subst to_be_restricted metasenv =
- match to_be_restricted with
- | [] -> metasenv, subst
- | _ ->
- let names_of_context_indexes context indexes =
- String.concat ", "
- (List.map
- (fun i ->
- try
- match List.nth context (i-1) 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' =
- let more_to_be_restricted', ty' =
- force_does_not_occur subst to_be_restricted ty
- in
- more_to_be_restricted @ more_to_be_restricted',
- 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) = (* restrict metasenv *)
- List.fold_right
- (fun (n, context, t) (more, metasenv) ->
- 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
- (more @ more_to_be_restricted @ more_to_be_restricted',
- metasenv')
- with Occur ->
- 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 ([], [])