(** finds the _pointers_ to subterms that are alpha-equivalent to wanted in t *)
let find_subterms ~eq ~wanted t =
- let rec find wanted t =
- if eq wanted t then
+ let rec find w t =
+ if eq w t then
[t]
else
match t with
fun acc e ->
match e with
| None -> acc
- | Some t -> find wanted t @ acc
+ | Some t -> find w t @ acc
) [] ctx
| Cic.Lambda (_, t1, t2)
| Cic.Prod (_, t1, t2)
| Cic.LetIn (_, t1, t2) ->
- find wanted t1 @ find (CicSubstitution.lift 1 wanted) t2
+ find w t1 @ find (CicSubstitution.lift 1 w) t2
| Cic.Appl l ->
- List.fold_left (fun acc t -> find wanted t @ acc) [] l
- | Cic.Cast (t, ty) -> find wanted t @ find wanted ty
+ List.fold_left (fun acc t -> find w t @ acc) [] l
+ | Cic.Cast (t, ty) -> find w t @ find w ty
| Cic.Implicit _ -> assert false
| Cic.Const (_, esubst)
| Cic.Var (_, esubst)
| Cic.MutInd (_, _, esubst)
| Cic.MutConstruct (_, _, _, esubst) ->
- List.fold_left (fun acc (_, t) -> find wanted t @ acc) [] esubst
+ List.fold_left (fun acc (_, t) -> find w t @ acc) [] esubst
| Cic.MutCase (_, _, outty, indterm, patterns) ->
- find wanted outty @ find wanted indterm @
- List.fold_left (fun acc p -> find wanted p @ acc) [] patterns
+ find w outty @ find w indterm @
+ List.fold_left (fun acc p -> find w p @ acc) [] patterns
| Cic.Fix (_, funl) ->
List.fold_left (
- fun acc (_, _, ty, bo) -> find wanted ty @ find wanted bo @ acc
+ fun acc (_, _, ty, bo) -> find w ty @ find w bo @ acc
) [] funl
| Cic.CoFix (_, funl) ->
List.fold_left (
- fun acc (_, ty, bo) -> find wanted ty @ find wanted bo @ acc
+ fun acc (_, ty, bo) -> find w ty @ find w bo @ acc
) [] funl
in
find wanted t