-
-(*
- let proof, goalno = status in
- let _, metasenv,_,_ = proof in
- let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
- let eq_uri = eq_of_goal type_of_goal in
- let env = (metasenv, context, CicUniv.empty_ugraph) in
- let eq_indexes, equalities, maxm, cache =
- Equality_retrieval.find_context_equalities maxmeta bag auto context proof cache
- in
- prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
- string_of_int maxm);
- List.iter
- (fun e -> prerr_endline (Equality.string_of_equality ~env e))
- equalities;
- prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
- let equalities =
- HExtlib.filter_map
- (fun e -> forward_simplify bag eq_uri env e active)
- equalities
- in
- prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>";
- List.iter
- (fun e -> prerr_endline (Equality.string_of_equality ~env e)) equalities;
- prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm);
- bag, equalities, cache, maxm
-*)
+;;
+
+let only signature context t =
+ try
+ let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in
+ let consts = MetadataConstraints.constants_of ty in
+ let b = MetadataConstraints.UriManagerSet.subset consts signature in
+ if b then b
+ else
+ try
+ let ty' = unfold context ty in
+ let consts' = MetadataConstraints.constants_of ty' in
+ MetadataConstraints.UriManagerSet.subset consts' signature
+ with _-> false
+ with _ -> false
+;;
+
+let not_default_eq_term t =
+ try
+ let uri = CicUtil.uri_of_term t in
+ not (LibraryObjects.in_eq_URIs uri)
+ with Invalid_argument _ -> true
+
+let retrieve_equations signature universe cache context=
+ match LibraryObjects.eq_URI() with
+ | None -> []
+ | Some eq_uri ->
+ let eq_uri = UriManager.strip_xpointer eq_uri in
+ let fake= Cic.Meta(-1,[]) in
+ let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
+ let candidates = get_candidates universe cache fake_eq in
+ (* defaults eq uris are built-in in auto *)
+ let candidates = List.filter not_default_eq_term candidates in
+ let candidates = List.filter (only signature context) candidates in
+ List.iter (fun t -> prerr_endline (CicPp.ppterm t)) candidates;
+ candidates