in
subst,metasenv,ugraph,context_terms, ty_terms
-(** locate_in_term what where
-* [what] must be a physical pointer to a subterm of [where]
-* It returns the context of [what] in [where] *)
-let locate_in_term what ~where context =
+(** locate_in_term equality what where context
+* [what] must match a subterm of [where] according to [equality]
+* It returns the matched terms together with their contexts in [where]
+* [equality] defaults to physical equality
+* [context] must be the context of [where]
+*)
+let locate_in_term ?(equality=(==))what ~where context =
let add_ctx context name entry =
- (Some (name, entry)) :: context
- in
+ (Some (name, entry)) :: context in
let rec aux context where =
- if what == where then context
+ if equality what where then [context,where]
else
match where with
| Cic.Implicit _
in
aux context where
-(** locate_in_conjecture what where
-* [what] must be a physical pointer to a subterm of [where]
-* It returns the context of [what] in [where] *)
-let locate_in_conjecture what (_,context,ty) =
+(** locate_in_term equality what where context
+* [what] must match a subterm of [where] according to [equality]
+* It returns the matched terms together with their contexts in [where]
+* [equality] defaults to physical equality
+* [context] must be the context of [where]
+*)
+let locate_in_conjecture ?(equality=(==)) what (_,context,ty) =
let context,res =
List.fold_right
(fun entry (context,res) ->
let res =
match ty with
None -> res
- | Some ty -> res @ locate_in_term what ~where:ty context in
+ | Some ty ->
+ res @ locate_in_term what ~where:ty context in
let context' = entry::context in
context',res
) context ([],[])
in
res @ locate_in_term what ~where:ty context
-
(* saturate_term newmeta metasenv context ty *)
(* Given a type [ty] (a backbone), it returns its head and a new metasenv in *)
(* which there is new a META for each hypothesis, a list of arguments for the *)