+let equations_blacklist =
+ List.fold_left
+ (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
+ UriManager.UriSet.empty [
+ "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
+ "cic:/Coq/Init/Logic/trans_eq.con";
+ "cic:/Coq/Init/Logic/f_equal.con";
+ "cic:/Coq/Init/Logic/f_equal2.con";
+ "cic:/Coq/Init/Logic/f_equal3.con";
+ "cic:/Coq/Init/Logic/sym_eq.con";
+(* "cic:/Coq/Logic/Eqdep/UIP_refl.con"; *)
+(* "cic:/Coq/Init/Peano/mult_n_Sm.con"; *)
+
+ (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
+ perche' questo cacchio di teorema rompe le scatole :'( *)
+ "cic:/Rocq/SUBST/comparith/mult_n_2.con";
+ ]
+ ;;
+
+let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module T = CicTypeChecker in
+ let candidates =
+ List.fold_left
+ (fun l uri ->
+ let suri = UriManager.string_of_uri uri in
+ if UriManager.UriSet.mem uri equations_blacklist then
+ l
+ else
+ let t = CicUtil.term_of_uri uri in
+ let ty, _ =
+ CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
+ in
+ (t, ty)::l)
+ []
+ (MetadataQuery.equations_for_goal ~dbd status)
+ in
+ let eq_uri1 = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI
+ and eq_uri2 = HelmLibraryObjects.Logic.eq_URI in
+ let iseq uri =
+ (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
+ in
+ let ok_types ty menv =
+ List.for_all (fun (_, _, mt) -> mt = ty) menv
+ in
+ let rec aux newmeta = function
+ | [] -> [], newmeta
+ | (term, termty)::tl ->
+ debug_print (lazy (
+ Printf.sprintf "Examining: %s (%s)"
+ (UriManager.string_of_uri (CicUtil.uri_of_term term))(* (CicPp.ppterm term) *) (CicPp.ppterm termty)));
+ let res, newmeta =
+ match termty with
+ | C.Prod (name, s, t) ->
+ let head, newmetas, args, newmeta =
+ ProofEngineHelpers.saturate_term newmeta [] context termty 0
+ in
+ let p =
+ if List.length args = 0 then
+ term
+ else
+ C.Appl (term::args)
+ in (
+ match head with
+ | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+ when (iseq uri) && (ok_types ty newmetas) ->
+ debug_print (lazy (
+ Printf.sprintf "OK: %s" (CicPp.ppterm term)));
+ let o = !Utils.compare_terms t1 t2 in
+ let w = compute_equality_weight ty t1 t2 in
+ let proof = BasicProof p in
+ let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
+ Some e, (newmeta+1)
+ | _ -> None, newmeta
+ )
+ | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
+ let o = !Utils.compare_terms t1 t2 in
+ let w = compute_equality_weight ty t1 t2 in
+ let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in
+ Some e, (newmeta+1)
+ | _ -> None, newmeta
+ in
+ match res with
+ | Some e ->
+ let tl, newmeta' = aux newmeta tl in
+ e::tl, max newmeta newmeta'
+ | None ->
+ aux newmeta tl
+ in
+ let found, maxm = aux maxmeta candidates in
+ (List.fold_left
+ (fun l e ->
+ if List.exists (meta_convertibility_eq e) l then (
+ debug_print (lazy (
+ Printf.sprintf "NO!! %s already there!" (string_of_equality e)));
+ l
+ )
+ else e::l)
+ [] found), maxm
+;;
+
+
+let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
+(* print_endline ("fix_metas " ^ (string_of_int newmeta)); *)