CicTypeChecker.type_of_aux'
metasenv current_ctx ty CicUniv.empty_ugraph
in
+ let set = Constr.UriManagerSet.union set(Constr.constants_of ty)in
match sort with
| Cic.Sort Cic.Prop -> set, hyp::current_ctx
| _ -> Constr.UriManagerSet.union set (Constr.constants_of t),
let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
let cmatch' = Constr.cmatch'
+(* used only by te old auto *)
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 uris = List.filter nonvar (List.map snd uris) in
let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
uris
-;;
-let filter_predicate set ctx menv =
- let is_predicate t =
+let is_predicate u =
let ty, _ =
try CicTypeChecker.type_of_aux' [] []
- (CicUtil.term_of_uri t) CicUniv.empty_ugraph
+ (CicUtil.term_of_uri u) CicUniv.empty_ugraph
with CicTypeChecker.TypeCheckerFailure _ -> assert false
in
let rec check_last_pi = function
| Cic.Sort Cic.Prop -> true
| _ -> false
in
- not (check_last_pi ty)
+ 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 universe_of_goals ~(dbd:HMysql.dbd) proof goals =
+ let (_, metasenv, _, _) = proof in
+ let add_uris_for acc goal =
+ let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+ let main, sig_constants = Constr.signature_of ty in
+ let set = signature_of_hypothesis context metasenv 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
+ Constr.UriManagerSet.union all_constants_closed acc
+ in
+ let all_constants_closed =
+ List.fold_left add_uris_for Constr.UriManagerSet.empty goals in
+ (* we split predicates from the rest *)
+ let predicates, rest =
+ Constr.UriManagerSet.partition is_predicate all_constants_closed
+ in
+ prerr_endline ("FOO!1");
+ let uris =
+ Constr.UriManagerSet.fold
+ (fun u acc ->
+ let uris =
+ sigmatch ~dbd ~facts:false ~where:`Statement
+ (Some (u,[]),all_constants_closed)
+ in
+ acc @ uris)
+ predicates []
in
- Constr.UriManagerSet.filter is_predicate set
+ prerr_endline ("FOO!2");
+(*
+ 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
+ let uris = List.filter (only all_constants_closed) uris in
+ uris
+;;
+
+let filter_out_predicate set ctx menv =
+ Constr.UriManagerSet.filter (fun u -> not (is_predicate u)) set
;;
let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
-(* let to_string set =
- "{ " ^
- (String.concat ", "
+(*
+ let to_string set =
+ "{\n" ^
+ (String.concat "\n"
(Constr.UriManagerSet.fold
- (fun u l -> (UriManager.string_of_uri u)::l) set []))
- ^ " }"
- in *)
+ (fun u l -> (" "^UriManager.string_of_uri u)::l) set []))
+ ^ "\n}"
+ in
+*)
let (_, metasenv, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants =
let set = signature_of_hypothesis context metasenv in
(* Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *)
let set = Constr.UriManagerSet.union set sig_constants in
- let set = filter_predicate set context metasenv in
+ let set = filter_out_predicate set context metasenv 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 l set in
+ let set_for_sigmatch = List.fold_right Constr.UriManagerSet.remove l set in
let uris =
- sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
+ sigmatch ~dbd ~facts:false ~where:`Statement (main,set_for_sigmatch) in
let uris = List.filter nonvar (List.map snd uris) in
let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
+ let set = List.fold_right Constr.UriManagerSet.add l set in
+ let uris = List.filter (only set) uris in
uris
(* ) *)
(* else raise Goal_is_not_an_equation *)