let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))
-let signature_of_hypothesis context =
- List.fold_left
- (fun set hyp ->
- match hyp with
- | None -> set
- | Some (_, Cic.Decl t)
- | Some (_, Cic.Def (t, _)) ->
- Constr.UriManagerSet.union set (Constr.constants_of t))
- Constr.UriManagerSet.empty context
+let signature_of_hypothesis context metasenv =
+ let set, _ =
+ List.fold_right
+ (fun hyp (set,current_ctx) ->
+ match hyp with
+ | None -> set, hyp::current_ctx
+ | Some (_, Cic.Decl t) ->
+ Constr.UriManagerSet.union set (Constr.constants_of t),
+ hyp::current_ctx
+ | Some (_, Cic.Def (t, _)) ->
+ try
+ let ty,_ =
+ CicTypeChecker.type_of_aux'
+ metasenv current_ctx t CicUniv.empty_ugraph
+ in
+ let sort,_ =
+ 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),
+ hyp::current_ctx
+ with
+ | CicTypeChecker.TypeCheckerFailure _ -> set, hyp::current_ctx)
+ context (Constr.UriManagerSet.empty,[])
+ in
+ set
+;;
let intersect uris siguris =
let set1 = List.fold_right Constr.UriManagerSet.add uris Constr.UriManagerSet.empty in
*)
let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
let cmatch' = Constr.cmatch'
+
+let is_predicate u =
+ let ty, _ =
+ try CicTypeChecker.type_of_aux' [] []
+ (CicUtil.term_of_uri u) CicUniv.empty_ugraph
+ with CicTypeChecker.TypeCheckerFailure _ -> assert false
+ in
+ let rec check_last_pi = function
+ | Cic.Prod (_,_,tgt) -> check_last_pi tgt
+ | Cic.Sort Cic.Prop -> true
+ | _ -> false
+ in
+ check_last_pi ty
+;;
-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 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
+ 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
+(*
+ 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 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 ", "
in *)
let (_, metasenv, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
- let main, sig_constants = Constr.signature_of ty in
+ let main, sig_constants =
+ match signature with
+ | None -> Constr.signature_of ty
+ | Some s -> s
+ in
(* Printf.printf "\nsig_constants: %s\n\n" (to_string sig_constants); *)
(* match main with *)
(* None -> raise Goal_is_not_an_equation *)
in
match eq_URI,main with
| Some eq_URI, Some (m, l) when UriManager.eq m eq_URI -> m::l
- | _,_ -> []
+ | _ -> []
in
- Printf.printf "\nSome (m, l): %s, [%s]\n\n"
+ (*Printf.printf "\nSome (m, l): %s, [%s]\n\n"
(UriManager.string_of_uri (List.hd l))
(String.concat "; " (List.map UriManager.string_of_uri (List.tl l)));
+ *)
(* if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *)
- let set = signature_of_hypothesis context in
+ 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_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
let all_constants =
let hyp_and_sug =
Constr.UriManagerSet.union
- (signature_of_hypothesis context)
+ (signature_of_hypothesis context metasenv)
sig_constants
in
let main =
projects / helm.git / blobdiff