+ check_last_pi ty
+;;
+
+let only constants uri =
+ prerr_endline (UriManager.string_of_uri uri);
+ let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *)
+ let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+ let consts = Constr.constants_of ty in
+(*
+ prerr_endline ("XXX " ^ UriManager.string_of_uri uri);
+ Constr.UriManagerSet.iter (fun u -> prerr_endline (" - " ^
+ UriManager.string_of_uri u)) consts;
+ Constr.UriManagerSet.iter (fun u -> prerr_endline (" + " ^
+ UriManager.string_of_uri u)) constants;*)
+ Constr.UriManagerSet.subset consts constants
+;;
+
+let rec types_of_equality = function
+ | Cic.Appl [Cic.MutInd (uri, _, _); ty; _; _]
+ when (LibraryObjects.is_eq_URI uri) ->
+ let uri_set = Constr.constants_of ty in
+ if Constr.UriManagerSet.equal uri_set Constr.UriManagerSet.empty then
+ Constr.SetSet.empty
+ else Constr.SetSet.singleton uri_set
+ | Cic.Prod (_, s, t) ->
+ Constr.SetSet.union (types_of_equality s) (types_of_equality t)
+ | _ -> Constr.SetSet.empty
+;;
+
+let types_for_equality metasenv goal =
+ let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+ let all = types_of_equality ty in
+ let _, all =
+ List.fold_left
+ (fun (i,acc) _ ->
+ let ty, _ =
+ CicTypeChecker.type_of_aux'
+ metasenv context (Cic.Rel i) CicUniv.empty_ugraph in
+ let newty = types_of_equality ty in
+ (i+1,Constr.SetSet.union newty acc))
+ (1,all) context
+ in all
+;;
+
+let signature_of metasenv goal =
+ let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+ let ty_set = Constr.constants_of ty in
+ let hyp_set = signature_of_hypothesis context metasenv in
+ let set = Constr.UriManagerSet.union ty_set hyp_set in
+ close_with_types set metasenv context
+
+
+let universe_of_goal ~(dbd:HSql.dbd) apply_only metasenv goal =
+ let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+ let ty_set = Constr.constants_of ty in
+ let hyp_set = signature_of_hypothesis context metasenv in
+ let set = Constr.UriManagerSet.union ty_set hyp_set in
+ let all_constants_closed = close_with_types set metasenv context in
+ (* we split predicates from the rest *)
+ let predicates, rest =
+ Constr.UriManagerSet.partition is_predicate all_constants_closed
+ in
+ let uris =
+ Constr.UriManagerSet.fold
+ (fun u acc ->
+ prerr_endline ("processing "^(UriManager.string_of_uri u));
+ let set_for_sigmatch =
+ Constr.UriManagerSet.remove u all_constants_closed in
+ if LibraryObjects.is_eq_URI (UriManager.strip_xpointer u) then
+ (* equality has a special treatment *)
+ (prerr_endline "special treatment";
+ let tfe =
+ Constr.SetSet.elements (types_for_equality metasenv goal)
+ in
+ List.fold_left
+ (fun acc l ->
+ let tyl = Constr.UriManagerSet.elements l in
+ prerr_endline ("tyl: "^(String.concat "\n"
+ (List.map UriManager.string_of_uri tyl)));
+ let set_for_sigmatch =
+ Constr.UriManagerSet.diff set_for_sigmatch l in
+ let uris =
+ sigmatch ~dbd ~facts:false ~where:`Statement
+ (Some (u,tyl),set_for_sigmatch) in
+ acc @ uris)
+ acc tfe)
+ else
+ (prerr_endline "normal treatment";
+ let uris =
+ sigmatch ~dbd ~facts:false ~where:`Statement
+ (Some (u,[]),set_for_sigmatch)
+ in
+ acc @ uris))
+ predicates []