-(* get_context_of_meta meta term *)
-(* returns the context of the occurrence of [meta] in [term]. *)
-(* Warning: if [meta] occurs not linearly in [term], the context *)
-(* of one "random" occurrence is returned. *)
-let get_context_of_meta meta term =
- let module C = Cic in
- let rec aux ctx =
- function
- C.Rel _
- | C.Var _ -> ()
- | C.Meta i when meta = i -> raise (Found ctx)
- | C.Meta _
- | C.Sort _
- | C.Implicit -> ()
- | C.Cast (te,ty) -> aux ctx te ; aux ctx ty
- | C.Prod (n,s,t) -> aux ctx s ; aux ((n, C.Decl s)::ctx) t
- | C.Lambda (n,s,t) -> aux ctx s ; aux ((n, C.Decl s)::ctx) t
- | C.LetIn (n,s,t) -> aux ctx s ; aux ((n, C.Def s)::ctx) t
- | C.Appl l -> List.iter (aux ctx) l
- | C.Const _ -> ()
- | C.Abst _ -> assert false
- | C.MutInd _
- | C.MutConstruct _ -> ()
- | C.MutCase (_,_,_,outt,t,pl) ->
- aux ctx outt ; aux ctx t; List.iter (aux ctx) pl
- | C.Fix (_,ifl) ->
- let counter = ref 0 in
- let ctx' =
- List.rev_map
- (function (name,_,ty,bo) ->
- let res = (C.Name name, C.Def (C.Fix (!counter,ifl))) in
- incr counter ;
- res
- ) ifl
- @ ctx
- in
- List.iter (function (_,_,ty,bo) -> aux ctx ty ; aux ctx' bo) ifl
- | C.CoFix (_,ifl) ->
- let counter = ref 0 in
- let ctx' =
- List.rev_map
- (function (name,ty,bo) ->
- let res = (C.Name name, C.Def (C.CoFix (!counter,ifl))) in
- incr counter ;
- res
- ) ifl
- @ ctx
- in
- List.iter (function (_,ty,bo) -> aux ctx ty ; aux ctx' bo) ifl
- in
- try
- aux [] term ;
- assert false (* No occurrences found. *)
- with
- Found context -> context
-;;
-