in
subst,metasenv,ugraph,context_terms, ty_terms
-let locate_in_term what ~where =
+(** 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 _
| Cic.Prod (name, s, t)
| Cic.Lambda (name, s, t) ->
aux context s @ aux (add_ctx context name (Cic.Decl s)) t
+ | Cic.LetIn (name, s, t) ->
+ aux context s @ aux (add_ctx context name (Cic.Def (s,None))) t
| Cic.Appl tl -> auxs context tl
-(*
- | Cic.LetIn (Cic.Anonymous, s1, t1), Cic.LetIn (name, s2, t2) ->
- aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2
- | Cic.LetIn (Cic.Name n1, s1, t1),
- Cic.LetIn ((Cic.Name n2) as name, s2, t2) when n1 = n2->
- aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2
- | Cic.LetIn (name1, s1, t1), Cic.LetIn (name2, s2, t2) -> []
- | Cic.MutCase (_, _, out1, t1, pat1), Cic.MutCase (_ , _, out2, t2, pat2) ->
- aux context out1 out2 @ aux context t1 t2 @ auxs context pat1 pat2
- | Cic.Fix (_, funs1), Cic.Fix (_, funs2) ->
+ | Cic.MutCase (_, _, out, t, pat) ->
+ aux context out @ aux context t @ auxs context pat
+ | Cic.Fix (_, funs) ->
let tys =
- List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2
+ List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
in
List.concat
- (List.map2
- (fun (_, _, ty1, bo1) (_, _, ty2, bo2) ->
- aux context ty1 ty2 @ aux (tys @ context) bo1 bo2)
- funs1 funs2)
- | Cic.CoFix (_, funs1), Cic.CoFix (_, funs2) ->
+ (List.map
+ (fun (_, _, ty, bo) ->
+ aux context ty @ aux (tys @ context) bo)
+ funs)
+ | Cic.CoFix (_, funs) ->
let tys =
- List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2
+ List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
in
List.concat
- (List.map2
- (fun (_, ty1, bo1) (_, ty2, bo2) ->
- aux context ty1 ty2 @ aux (tys @ context) bo1 bo2)
- funs1 funs2)
- | x,y ->
- raise (Bad_pattern
- (Printf.sprintf "Pattern %s versus term %s"
- (CicPp.ppterm x)
- (CicPp.ppterm y)))
-*)
+ (List.map
+ (fun (_, ty, bo) ->
+ aux context ty @ aux (tys @ context) bo)
+ funs)
and auxs context tl = (* as aux for list of terms *)
List.concat (List.map (fun t -> aux context t) tl)
in
- aux [] where
+ aux context where
+(** 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) ->
+ match entry with
+ None -> entry::context, res
+ | Some (_, Cic.Decl ty) ->
+ let res = res @ locate_in_term what ~where:ty context in
+ let context' = entry::context in
+ context',res
+ | Some (_, Cic.Def (bo,ty)) ->
+ let res = res @ locate_in_term what ~where:bo context in
+ let res =
+ match ty with
+ None -> res
+ | 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 *)