| Cic.Meta _
| Cic.Sort _
| Cic.Implicit _ -> UriManagerSet.empty
- | Cic.Var (u,exp_named_subst) -> UriManagerSet.empty
+ | Cic.Var (u,exp_named_subst) ->
+ (*CSC: TODO if the var has a body it must be processed *)
+ UriManagerSet.empty
| Cic.Const (u,exp_named_subst) ->
UriManagerSet.singleton u
| Cic.MutInd (u, t, exp_named_subst) ->
| `Conclusion -> [`InConclusion]
| `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None]
in
+ let positions =
+ if m = None then `MainConclusion None :: positions else positions in
let s' = List.map (fun (u:UriManager.uri) -> `Obj (u, positions)) s in
- `Obj (m, [`MainConclusion None]) :: s'
+ match m with
+ None -> s'
+ | Some m -> `Obj (m, [`MainConclusion None]) :: s'
let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
List.concat
(List.map
(fun (m,s) ->
- if ((m = 0) && (UriManager.eq main (UriManager.uri_of_string (HelmLibraryObjects.Logic.eq_XURI)))) then
+ let is_eq,card =
+ match main with
+ None -> false,m
+ | Some main ->
+ (m = 0 &&
+ UriManager.eq main
+ (UriManager.uri_of_string (HelmLibraryObjects.Logic.eq_XURI))),
+ m+1
+ in
+ if m = 0 && is_eq then
(if facts then myspeciallist_of_facts
else myspeciallist)
else
let res =
+ (* this gets rid of the ~750 objects of type Set/Prop/Type *)
+ if card = 0 then []
+ else
let must = must_of_prefix ~where main s in
match where with
- | `Conclusion -> at_least ~dbd ~concl_card:(Eq (m+1)) must
- | `Statement -> at_least ~dbd ~full_card:(Eq (m+1)) must
+ | `Conclusion -> at_least ~dbd ~concl_card:(Eq card) must
+ | `Statement -> at_least ~dbd ~full_card:(Eq card) must
in
- List.map (fun uri -> (m, uri)) res)
+ List.map (fun uri -> (card, uri)) res)
prefixes)
(* critical value reached, fallback to "only" constraints *)
union
(List.map
(fun (m,s) ->
+ let card = if main = None then m else m + 1 in
let must = must_of_prefix ~where main s in
(let res =
match where with
- | `Conclusion -> at_least ~dbd ~concl_card:(Gt (m+1)) must
- | `Statement -> at_least ~dbd ~full_card:(Gt (m+1)) must
+ | `Conclusion -> at_least ~dbd ~concl_card:(Gt card) must
+ | `Statement -> at_least ~dbd ~full_card:(Gt card) must
in
(* we tag the uri with m+1, for sorting purposes *)
- List.map (fun uri -> (m+1, uri)) res))
+ List.map (fun uri -> (card, uri)) res))
maximal_prefixes)
in
List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
let all_constants =
List.fold_right UriManagerSet.add types (UriManagerSet.add main constants)
in
- compute_with_only ~dbd ~facts main all_concl all_constants
+ compute_with_only ~dbd ~facts (Some main) all_concl all_constants
| _, _ -> [])
else
(* in this case we compute all prefixes, and we do not need
in
(match prefixes with
Some main, all_concl ->
- compute_exactly ~dbd ~facts ~where:`Conclusion main all_concl
-(*
- List.concat
- (List.map
- (fun (m,s) ->
- let must = must_of_prefix ~where:`Conclusion main s in
- let res = at_least ~dbd ~concl_card:(Eq (m+1)) must in
- List.map (fun uri -> (m, uri)) res)
- all_concl) *)
+ compute_exactly ~dbd ~facts ~where:`Conclusion (Some main) all_concl
| _, _ -> [])
let power_upto upto consts =
type where = [ `Conclusion | `Statement ]
-let sigmatch ~(dbd:Mysql.dbd)
- ?(facts=false) ?(where = `Conclusion) (main, constants) =
- match main with
- None -> []
- | Some (main, types) ->
- let constants_no = UriManagerSet.cardinal constants in
- if (constants_no > critical_value) then
- let subsets =
- let subsets = power_upto just_factor constants in
- let types_no = List.length types in
- List.map (function (n,l) -> (n+types_no,types@l)) subsets
- in
- let all_constants =
- List.fold_right UriManagerSet.add types (UriManagerSet.add main constants)
- in
- compute_with_only ~dbd ~where main subsets all_constants
- else
- let subsets =
- let subsets = power constants in
- let types_no = List.length types in
- if types_no > 0 then
- (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
- else subsets
- in
- compute_exactly ~dbd ~facts ~where main subsets
+let sigmatch ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion)
+ (main, constants)
+=
+ let main,types =
+ match main with
+ None -> None,[]
+ | Some (main, types) -> Some main,types
+ in
+ let constants_no = UriManagerSet.cardinal constants in
+ if (constants_no > critical_value) then
+ let subsets =
+ let subsets = power_upto just_factor constants in
+ let types_no = List.length types in
+ List.map (function (n,l) -> (n+types_no,types@l)) subsets
+ in
+ let all_constants =
+ let all = match main with None -> types | Some m -> m::types in
+ List.fold_right UriManagerSet.add all constants
+ in
+ compute_with_only ~dbd ~where main subsets all_constants
+ else
+ let subsets =
+ let subsets = power constants in
+ let types_no = List.length types in
+ if types_no > 0 then
+ (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
+ else subsets
+ in
+ compute_exactly ~dbd ~facts ~where main subsets
(* match query wrappers *)
(* let debug_print = fun _ -> () *)
-let experimental_hint =
- let profile = CicUtil.profile "experimental_hint" in
- fun ~dbd ~facts ?signature status ->
- profile (MetadataQuery.experimental_hint ~dbd ~facts ?signature) status
+let new_experimental_hint =
+ let profile = CicUtil.profile "new_experimental_hint" in
+ fun ~dbd ~facts ?signature ~universe status ->
+ profile (MetadataQuery.new_experimental_hint ~dbd ~facts ?signature ~universe) status
let search_theorems_in_context status =
let (proof, goal) = status in
with _ -> false
let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
+ universe
=
if depth = 0 then [] else
if List.mem ty already_seen_goals then [] else
new_search_theorems
(fun status ->
List.map snd
- (experimental_hint
- ~dbd ~facts:facts ?signature:sign status))
+ (new_experimental_hint
+ ~dbd ~facts:facts ?signature:sign ~universe status))
dbd proof goal (depth-1) new_sign in
let all_choices =
local_choices@global_choices in
Pervasives.compare
(List.length goals1) (List.length goals2))
all_choices in
- (match (auto_new dbd width already_seen_goals sorted_choices)
+ (match (auto_new dbd width already_seen_goals universe sorted_choices)
with
[] ->
(* no proof has been found; we update the
| _ -> assert false)
end
-and auto_new dbd width already_seen_goals = function
+and auto_new dbd width already_seen_goals universe = function
[] -> []
| (subst,(proof, goals, sign))::tl ->
let _,metasenv,_,_ = proof in
true
with _ -> false in
let goals'= List.filter is_in_metasenv goals in
- auto_new_aux dbd width already_seen_goals
+ auto_new_aux dbd width already_seen_goals universe
((subst,(proof, goals', sign))::tl)
-and auto_new_aux dbd width already_seen_goals = function
+and auto_new_aux dbd width already_seen_goals universe = function
[] -> []
| (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
| (subst,(proof, (goal,0)::_, _))::tl ->
- auto_new dbd width already_seen_goals tl
+ auto_new dbd width already_seen_goals universe tl
| (subst,(proof, goals, _))::tl when
(List.length goals) > width ->
- auto_new dbd width already_seen_goals tl
+ auto_new dbd width already_seen_goals universe tl
| (subst,(proof, (goal,depth)::gtl, sign))::tl ->
let _,metasenv,p,_ = proof in
let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
match (auto_single dbd proof goal ey ty depth
- (width - (List.length gtl)) sign already_seen_goals)
+ (width - (List.length gtl)) sign already_seen_goals) universe
with
- [] -> auto_new dbd width already_seen_goals tl
+ [] -> auto_new dbd width already_seen_goals universe tl
| (local_subst,(proof,[],sign))::tl1 ->
let new_subst f t = f (subst t) in
let is_meta_closed = CicUtil.is_meta_closed ty in
(function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1)
in
(new_subst local_subst,(proof,gtl,sign))::tl2@tl in
- auto_new dbd width already_seen_goals all_choices
+ auto_new dbd width already_seen_goals universe all_choices
| _ -> assert false
;;
()
=
let auto_tac dbd (proof,goal) =
+ let universe = MetadataQuery.signature_of_goal ~dbd (proof,goal) in
Hashtbl.clear inspected_goals;
debug_print "Entro in Auto";
let id t = t in
- match (auto_new dbd width [] [id,(proof, [(goal,depth)],None)]) with
+ match auto_new dbd width [] universe [id,(proof, [(goal,depth)],None)] with
[] -> debug_print("Auto failed");
raise (ProofEngineTypes.Fail "No Applicable theorem")
| (_,(proof,[],_))::_ ->
let inter = Constr.UriManagerSet.inter set1 set2 in
List.filter (fun s -> Constr.UriManagerSet.mem s inter) uris
+let at_most =
+ let profiler = CicUtil.profile "at_most" in
+ fun ~dbd ~where uri -> profiler (Constr.at_most ~dbd ~where) uri
+
+let sigmatch =
+ let profiler = CicUtil.profile "sigmatch" in
+ fun ~dbd ~facts ~where signature ->
+ profiler (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature
+
let filter_uris_forward ~dbd (main, constants) uris =
let main_uris =
match main with
let full_signature =
List.fold_right Constr.UriManagerSet.add main_uris constants
in
- List.filter (Constr.at_most ~dbd ~where:`Statement full_signature) uris
+ List.filter (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)
+ (sigmatch ~dbd ~facts ~where:`Statement signature)
in
intersect uris siguris
Constr.UriManagerSet.union bag (Constr.constants_of ty))
s s
+let apply_tac_verbose =
+ let profiler = CicUtil.profile "apply_tac_verbose" in
+ fun ~term status -> profiler (PrimitiveTactics.apply_tac_verbose ~term) status
+
+let sigmatch =
+ let profiler = CicUtil.profile "sigmatch" in
+ fun ~dbd ~facts ?(where=`Conclusion) signature -> profiler (Constr.sigmatch ~dbd ~facts ~where) signature
+
+let cmatch' =
+ let profiler = CicUtil.profile "cmatch'" in
+ fun ~dbd ~facts signature -> profiler (Constr.cmatch' ~dbd ~facts) signature
+
+let signature_of_goal ~(dbd:Mysql.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 experimental_hint
~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
let (_, metasenv, _, _) = proof in
let (uris, (main, sig_constants)) =
match signature with
| Some signature ->
- (Constr.sigmatch ~dbd ~facts signature, signature)
+ (sigmatch ~dbd ~facts signature, signature)
| None ->
- (Constr.cmatch' ~dbd ~facts ty, Constr.signature_of ty)
+ (cmatch' ~dbd ~facts ty, Constr.signature_of ty)
in
let uris = List.filter nonvar (List.map snd uris) in
let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
try
let (subst,(proof, goal_list)) =
(* debug_print ("STO APPLICANDO" ^ uri); *)
- PrimitiveTactics.apply_tac_verbose
+ apply_tac_verbose
+ ~term:(CicUtil.term_of_uri uri)
+ status
+ in
+ let goal_list =
+ List.stable_sort (compare_goal_list proof) goal_list
+ in
+ Some (uri, (subst,(proof, goal_list)))
+ with ProofEngineTypes.Fail _ -> None
+ in
+ match status' with
+ | None -> aux tl
+ | Some status' -> status' :: aux tl)
+ in
+ List.stable_sort
+ (fun (_,(_, (_, goals1))) (_,(_, (_, goals2))) ->
+ Pervasives.compare (List.length goals1) (List.length goals2))
+ (aux uris)
+
+let new_experimental_hint
+ ~(dbd:Mysql.dbd) ?(facts=false) ?signature ~universe
+ ((proof, goal) as status)
+=
+ let (_, metasenv, _, _) = proof in
+ let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+ let (uris, (main, sig_constants)) =
+ match signature with
+ | Some signature ->
+ (sigmatch ~dbd ~facts signature, signature)
+ | None ->
+ (cmatch' ~dbd ~facts ty, Constr.signature_of ty) in
+ let universe =
+ List.fold_left
+ (fun res u -> Constr.UriManagerSet.add u res)
+ Constr.UriManagerSet.empty universe in
+ let uris =
+ List.fold_left
+ (fun res (_,u) -> Constr.UriManagerSet.add u res)
+ Constr.UriManagerSet.empty uris in
+ let uris = Constr.UriManagerSet.inter uris universe in
+ let uris = Constr.UriManagerSet.elements uris in
+ let rec aux = function
+ | [] -> []
+ | uri :: tl ->
+ (let status' =
+ try
+ let (subst,(proof, goal_list)) =
+ (* debug_print ("STO APPLICANDO" ^ uri); *)
+ apply_tac_verbose
~term:(CicUtil.term_of_uri uri)
status
in
* false
* @param pat shell like pattern matching over object names, a string where "*"
* is interpreted as 0 or more characters and "?" as exactly one character *)
+
+val signature_of_goal:
+ dbd:Mysql.dbd -> ProofEngineTypes.status -> UriManager.uri list
+
val locate:
dbd:Mysql.dbd ->
?vars:bool -> string -> UriManager.uri list
((Cic.term -> Cic.term) *
(ProofEngineTypes.proof * ProofEngineTypes.goal list))) list
+val new_experimental_hint:
+ dbd:Mysql.dbd ->
+ ?facts:bool ->
+ ?signature:MetadataConstraints.term_signature ->
+ universe:UriManager.uri list ->
+ ProofEngineTypes.status ->
+ (UriManager.uri *
+ ((Cic.term -> Cic.term) *
+ (ProofEngineTypes.proof * ProofEngineTypes.goal list))) list
+
val match_term: dbd:Mysql.dbd -> Cic.term -> UriManager.uri list
(** @param string is an uri *)
projects / helm.git / commitdiff