+let close_with_constructors s metasenv context =
+ Constr.UriManagerSet.fold
+ (fun e bag ->
+ let t = CicUtil.term_of_uri e in
+ match t with
+ Cic.MutInd (uri,_,_)
+ | Cic.MutConstruct (uri,_,_,_) ->
+ (match fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ Cic.InductiveDefinition(tl,_,_,_) ->
+ snd
+ (List.fold_left
+ (fun (i,s) (_,_,_,cl) ->
+ let _,s =
+ List.fold_left
+ (fun (j,s) _ ->
+ let curi = UriManager.uri_of_uriref uri i (Some j) in
+ j+1,Constr.UriManagerSet.add curi s) (1,s) cl in
+ (i+1,s)) (0,bag) tl)
+ | _ -> assert false)
+ | _ -> bag)
+ s s
+
+(* Profiling code
+let apply_tac_verbose =
+ let profiler = CicUtil.profile "apply_tac_verbose" in
+ fun ~term status -> profiler.profile (PrimitiveTactics.apply_tac_verbose ~term) status
+
+let sigmatch =
+ let profiler = CicUtil.profile "sigmatch" in
+ fun ~dbd ~facts ?(where=`Conclusion) signature -> profiler.profile (Constr.sigmatch ~dbd ~facts ~where) signature
+
+let cmatch' =
+ let profiler = CicUtil.profile "cmatch'" in
+ fun ~dbd ~facts signature -> profiler.profile (Constr.cmatch' ~dbd ~facts) signature
+*)
+let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
+let cmatch' = Constr.cmatch'
+
+let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
+ let (_, metasenv, _, _) = proof in
+ let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+ let main, sig_constants = Constr.signature_of ty in
+ let set = signature_of_hypothesis context in
+ let set =
+ match main with
+ None -> set
+ | Some (main,l) ->
+ List.fold_right Constr.UriManagerSet.add (main::l) set in
+ let set = Constr.UriManagerSet.union set sig_constants in
+ let all_constants_closed = close_with_types set metasenv context in
+ let uris =
+ sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) in
+ let uris = List.filter nonvar (List.map snd uris) in
+ let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
+ uris
+
+let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
+(* let to_string set =
+ "{ " ^
+ (String.concat ", "
+ (Constr.UriManagerSet.fold
+ (fun u l -> (UriManager.string_of_uri u)::l) set []))
+ ^ " }"
+ in *)
+ let (_, metasenv, _, _) = proof in
+ let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+ let main, sig_constants = Constr.signature_of ty in
+(* Printf.printf "\nsig_constants: %s\n\n" (to_string sig_constants); *)
+(* match main with *)
+(* None -> raise Goal_is_not_an_equation *)
+(* | Some (m,l) -> *)
+ let m, l =
+ let eq_URI =
+ let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
+ UriManager.uri_of_string (us ^ "#xpointer(1/1)")
+ in
+ match main with
+ | None -> eq_URI, []
+ | Some (m, l) when UriManager.eq m eq_URI -> m, l
+ | Some (m, l) -> eq_URI, []
+ in
+ Printf.printf "\nSome (m, l): %s, [%s]\n\n"
+ (UriManager.string_of_uri m)
+ (String.concat "; " (List.map UriManager.string_of_uri l));
+ (* if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *)
+ let set = signature_of_hypothesis context in
+ (* Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *)
+ let set = Constr.UriManagerSet.union set sig_constants in
+ let set = close_with_types set metasenv context in
+ (* Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *)
+ let set = close_with_constructors set metasenv context in
+ (* Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *)
+ let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in
+ let uris =
+ sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
+ let uris = List.filter nonvar (List.map snd uris) in
+ let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
+ uris
+ (* ) *)
+ (* else raise Goal_is_not_an_equation *)
+