+let intersect uris siguris =
+ let set1 = List.fold_right Constr.StringSet.add uris Constr.StringSet.empty in
+ let set2 =
+ List.fold_right Constr.StringSet.add siguris Constr.StringSet.empty
+ in
+ let inter = Constr.StringSet.inter set1 set2 in
+ List.filter (fun s -> Constr.StringSet.mem s inter) uris
+
+let filter_uris_forward ~dbd (main, constants) uris =
+ let main_uris =
+ match main with
+ | None -> []
+ | Some (main, types) -> main :: types
+ in
+ let full_signature =
+ List.fold_right Constr.StringSet.add main_uris constants
+ in
+ List.filter (Constr.at_most ~dbd ~where:`Statement full_signature) uris
+
+let filter_uris_backward ~dbd ~facts signature uris =
+ let siguris =
+ List.map snd
+ (MetadataConstraints.sigmatch ~dbd ~facts ~where:`Statement signature)
+ in
+ intersect uris siguris
+
+let compare_goal_list proof goal1 goal2 =
+ let _,metasenv,_,_ = proof in
+ let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
+ let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
+ let ty_sort1,_ =
+ CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph
+ in
+ let ty_sort2,_ =
+ CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.empty_ugraph
+ in
+ let prop1 =
+ let b,_ =
+ CicReduction.are_convertible
+ ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.empty_ugraph
+ in
+ if b then 0
+ else 1
+ in
+ let prop2 =
+ let b,_ =
+ CicReduction.are_convertible
+ ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.empty_ugraph
+ in
+ if b then 0
+ else 1
+ in
+ prop1 - prop2
+
+let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =