+let rec compute_var pos uri =
+ let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ match o with
+ | Cic.Variable (_, Some _, _, _, _) -> S.empty
+ | Cic.Variable (_, None, ty, params, _) ->
+ let var_metadata =
+ List.fold_left
+ (fun metadata uri ->
+ S.union metadata (compute_var (next_pos pos) uri))
+ S.empty
+ params
+ in
+ (match pos with
+ | `MainHypothesis (Some (Eq 0)) ->
+ let pos = `MainHypothesis (Some (Eq (depth_offset params))) in
+ let ty_metadata = compute_term pos ty in
+ S.union ty_metadata var_metadata
+ | `InHypothesis ->
+ let ty_metadata = compute_term pos ty in
+ S.union ty_metadata var_metadata
+ | _ -> assert false)
+ | _ -> assert false
+
+let compute_obj uri =
+ let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ match o with
+ | Cic.Variable (_, body, ty, params, _)
+ | Cic.Constant (_, body, ty, params, _) ->
+ let pos = `MainConclusion (Some (Eq (depth_offset params))) in
+ let metadata = compute pos ~body ~ty in
+ let var_metadata =
+ List.fold_left
+ (fun metadata uri ->
+ S.union metadata (compute_var (`MainHypothesis (Some (Eq 0))) uri))
+ S.empty
+ params
+ in
+ [ uri,
+ UriManager.name_of_uri uri,
+ S.union metadata var_metadata ]
+ | Cic.InductiveDefinition (types, params, _, _) ->
+ let pos = `MainConclusion(Some (Eq (depth_offset params))) in
+ let metadata = compute_ind pos ~uri ~types in
+ let var_metadata =
+ List.fold_left
+ (fun metadata uri ->
+ S.union metadata (compute_var (`MainHypothesis (Some (Eq 0))) uri))
+ S.empty params
+ in
+ List.fold_left
+ (fun acc m ->
+ (List.map (fun (uri,name,md) -> (uri,name,S.union md var_metadata)) m)
+ @ acc)
+ [] metadata
+ | Cic.CurrentProof _ -> assert false
+
+let compute_obj uri =
+ List.map (fun (u, n, md) -> (u, n, S.elements md)) (compute_obj uri)
+
+let compute ~body ~ty =
+ S.elements (compute (`MainConclusion (Some (Eq 0))) ~body ~ty)