+let rec compute_var pos uri =
+ let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ match o with
+ | Cic.Variable (_, body, ty, params, _) ->
+ let metadata_of_vars =
+ List.flatten
+ (List.map (compute_var (next_pos pos)) params) in
+ (match pos with
+ | `MainHypothesis (Some 0) ->
+ let pos = `MainHypothesis(Some (List.length params)) in
+ (compute pos ~body ~ty)@metadata_of_vars
+ | `InHypothesis ->
+ (compute pos ~body ~ty)@metadata_of_vars
+ | _ -> 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 (List.length params)) in
+ let metadata = compute pos ~body ~ty
+ in
+ let metadata_of_vars =
+ List.flatten
+ (List.map (compute_var (`MainHypothesis (Some 0))) params)
+ in
+ [UriManager.string_of_uri uri,
+ UriManager.name_of_uri uri,metadata @ metadata_of_vars]
+ | Cic.InductiveDefinition (types, params, _, _) ->
+ let pos = `MainConclusion(Some (List.length params)) in
+ let metadata_of_vars =
+ List.flatten
+ (List.map (compute_var (`MainHypothesis (Some 0))) params) in
+ let metadata = compute_ind pos ~uri ~types in
+ List.map (fun (uri,name,md) -> (uri,name,md@metadata_of_vars)) metadata
+ | Cic.CurrentProof _ -> assert false
+
+
+let compute ~body ~ty = compute (`MainConclusion (Some 0)) ~body ~ty