+let is_proof_irrelevant status context ty =
+ match
+ NCicReduction.whd status ~subst:[] context
+ (NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] context ty)
+ with
+ NCic.Sort NCic.Prop -> true
+ | NCic.Sort _ -> false
+ | _ -> assert false
+;;
+
+let rec relevance_of status ?(context=[]) ty =
+ match NCicReduction.whd status ~subst:[] context ty with
+ NCic.Prod (n,s,t) ->
+ not (is_proof_irrelevant status context s) ::
+ relevance_of status ~context:((n,NCic.Decl s)::context) t
+ | _ -> []
+;;
+
+let compute_relevance status uri =
+ function
+ NCic.Constant (_,name,bo,ty,attrs) ->
+ let relevance = relevance_of status ty in
+ NCic.Constant (relevance,name,bo,ty,attrs)
+ | NCic.Fixpoint (ind,funs,attrs) ->
+ let funs =
+ List.map
+ (fun (_,name,recno,ty,bo) ->
+ let relevance = relevance_of status ty in
+ relevance,name,recno,ty,bo
+ ) funs
+ in
+ NCic.Fixpoint (ind,funs,attrs)
+ | NCic.Inductive (ind,leftno,tys,attrs) ->
+ let context =
+ List.rev_map (fun (_,name,arity,_) -> name,NCic.Decl arity) tys in
+ let tysno = List.length tys in
+ let tys =
+ List.map
+ (fun (_,name,arity,cons) ->
+ let relevance = relevance_of status arity in
+ let cons =
+ List.map
+ (fun (_,name,ty) ->
+ let dety =
+ NCicTypeChecker.debruijn status uri tysno ~subst:[] [] ty in
+ let relevance = relevance_of status ~context dety in
+ relevance,name,ty
+ ) cons
+ in
+ (relevance,name,arity,cons)
+ ) tys
+ in
+ NCic.Inductive (ind,leftno,tys,attrs)
+;;
+
+let extract_uris status uris =
+ List.fold_left
+ (fun status uri ->
+ let obj = NCicEnvironment.get_checked_obj status uri in
+ let status = eval_extract_obj status obj in
+ eval_extract_ocaml_obj status obj
+ ) status uris
+;;