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
- let module C = Cic in
- let module R = CicReduction in
- let module S = CicSubstitution in
- let module PET = ProofEngineTypes in
- let module PT = PrimitiveTactics in
- let _,metasenv,_,_ = proof in
- let _,context,ty = CicUtil.lookup_meta goal metasenv in
- let rec find n = function
- [] -> []
- | hd::tl ->
- let res =
- try
- Some (PET.apply_tactic
- (PT.apply_tac ~term:(C.Rel n)) status )
- with
- PET.Fail _ -> None in
- (match res with
- Some res -> res::(find (n+1) tl)
- | None -> find (n+1) tl)
- in
- try
- find 1 context
- with Failure s ->
- []
-;;
-
-let depth = 5;;
-let width = 3;;
-
-let new_search_theorems f proof goal depth gtl sign =
- let choices = f (proof,goal)
- in
- List.map
- (function (proof, goallist) ->
- (proof,(List.map (function g -> (g,depth)) goallist)@gtl, sign))
- choices
-;;
-
-exception NoOtherChoices;;
-let rec auto dbd = function
- [] -> []
- | (proof, [], sign)::tl -> (proof, [], sign)::tl
- | (proof, (goal,0)::_, _)::tl -> auto dbd tl
- | (proof, (((goal,depth)::gtl) as allg), sign)::tl ->
- (* first we check if the metavariable has not been already
- closed as a side effect by some other application *)
- let facts = (depth = 1) in
- let name,metasenv,p,statement = proof in
- let meta_inf =
- (try
- let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
- Some (ey, ty)
- with _ -> None) in
- match meta_inf with
- Some (ey, ty) ->
- (* the goal is still there *)
- (*
- debug_print ("CURRENT GOAL = " ^ CicPp.ppterm ty);
- debug_print ("CURRENT PROOF = " ^ CicPp.ppterm p);
- debug_print ("CURRENT HYP = " ^ CicPp.ppcontext ey);
- *)
- (* if the goal contains metavariables we use the input
- signature for at_most constraints *)
- let is_meta_closed = CicUtil.is_meta_closed ty in
- let sign, new_sign =
- if is_meta_closed then
- None, Some (MetadataConstraints.signature_of ty)
- else sign,sign in (* maybe the union ? *)
- let local_choices =
- new_search_theorems
- search_theorems_in_context
- proof goal (depth-1) [] new_sign in
- let global_choices =
- new_search_theorems
- (fun status ->
- List.map snd
- (MetadataQuery.hint
- ~dbd ~facts:facts ?signature:sign status))
- proof goal (depth-1) [] new_sign in
- (* we proceed depth-first on the current goal. This is
- a MAJOR optimization, since in case of success, and
- if the goal is meta_closed, we may just drop the alternatives
- tl1, avoiding useless backtracking. *)
- let all_choices =
- local_choices@global_choices in
- (match (auto dbd all_choices)
- with
- [] -> auto dbd tl
- | (proof,[],_)::tl1 ->
- let all_choices =
- let gtl' = List.map fst gtl in
- if (gtl = [] || is_meta_closed) then
- (proof,gtl,sign)::tl
- else
- let tl2 =
- (List.map
- (function (p,l,s) -> (p,l@gtl,s)) tl1)
- in
- (proof,gtl,sign)::tl2@tl in
- auto dbd all_choices
- | _ -> assert false)
- | None -> auto dbd ((proof,gtl,sign)::tl)
-;;
-
-
-let auto_tac ?num dbd =
- let auto_tac dbh (proof,goal) =
- debug_print "Entro in Auto";
- match (auto dbd [(proof, [(goal,depth)],None)]) with
- [] -> debug_print("Auto failed");
- raise (ProofEngineTypes.Fail "No Applicable theorem")
- | (proof,[],_)::_ ->
- debug_print "AUTO_TAC HA FINITO";
- (proof,[])
- | _ -> assert false
- in
- ProofEngineTypes.mk_tactic (auto_tac dbd)
-;;
-
-
-(************************** EXPERIMENTAL VERSION ****************************)
-
(* In this versions of auto_tac we maintain an hash table of all inspected
goals. We assume that the context is invariant for application.
To this aim, it is essential to sall hint_verbose, that in turns calls
apply_verbose. *)
-
-
type exitus =
No of int
| Yes of Cic.term * int
let default_depth = 5
let default_width = 3
-let auto_tac_new ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd)
+let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd)
()
=
let auto_tac dbd (proof,goal) =
in
prop1 - prop2
-let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((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 -> (Constr.sigmatch ~dbd ~facts signature, signature)
- | None -> (Constr.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
- let types_constants =
- match main with
- | None -> Constr.UriManagerSet.empty
- | Some (main, types) ->
- List.fold_right Constr.UriManagerSet.add (main :: types)
- Constr.UriManagerSet.empty
- in
- let hyp_constants =
- Constr.UriManagerSet.diff (signature_of_hypothesis context) types_constants
- in
-(* Constr.UriManagerSet.iter debug_print hyp_constants; *)
- let other_constants = Constr.UriManagerSet.union sig_constants hyp_constants in
- let uris =
- let pow = 2 ** (Constr.UriManagerSet.cardinal other_constants) in
- if ((List.length uris < pow) or (pow <= 0))
- then begin
-(* debug_print "MetadataQuery: large sig, falling back to old method"; *)
- filter_uris_forward ~dbd (main, other_constants) uris
- end else
- filter_uris_backward ~dbd ~facts (main, other_constants) uris
- in
- let rec aux = function
- | [] -> []
- | uri :: tl ->
- (let status' =
- try
- let (proof, goal_list) =
-(* debug_print ("STO APPLICANDO " ^ uri); *)
- PET.apply_tactic
- (PrimitiveTactics.apply_tac
- ~term:(CicUtil.term_of_uri uri))
- status
- in
- let goal_list =
- List.stable_sort (compare_goal_list proof) goal_list
- in
- Some (uri, (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)
-
(* experimental_hint is a version of hint for experimental
purposes. It uses auto_tac_verbose instead of auto tac.
Auto_tac verbose also returns a substitution - for the moment
projects / helm.git / commitdiff