1 (* Copyright (C) 2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
29 let debug_print s = if debug then prerr_endline (Lazy.force s)
31 (* let debug_print = fun _ -> () *)
34 let new_experimental_hint =
35 let profile = CicUtil.profile "new_experimental_hint" in
36 fun ~dbd ~facts ?signature ~universe status ->
37 profile.profile (MetadataQuery.new_experimental_hint ~dbd ~facts ?signature ~universe) status
38 *) let new_experimental_hint = MetadataQuery.new_experimental_hint
40 (* In this versions of auto_tac we maintain an hash table of all inspected
41 goals. We assume that the context is invariant for application.
42 To this aim, it is essential to sall hint_verbose, that in turns calls
47 | Yes of Cic.term * int
50 let inspected_goals = Hashtbl.create 503;;
52 let search_theorems_in_context status =
53 let (proof, goal) = status in
55 let module R = CicReduction in
56 let module S = CicSubstitution in
57 let module PET = ProofEngineTypes in
58 let module PT = PrimitiveTactics in
59 let _,metasenv,_,_ = proof in
60 let _,context,ty = CicUtil.lookup_meta goal metasenv in
61 let rec find n = function
65 (* we should check that the hypothesys has not been cleared *)
66 if List.nth context (n-1) = None then
70 let (subst,(proof, goal_list)) =
71 PT.apply_tac_verbose ~term:(C.Rel n) status
75 List.stable_sort (compare_goal_list proof) goal_list in
77 Some (subst,(proof, goal_list))
82 | Some res -> res::(find (n+1) tl)
83 | None -> find (n+1) tl)
91 let compare_goals proof goal1 goal2 =
92 let _,metasenv,_,_ = proof in
93 let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
94 let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
95 let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1
96 CicUniv.empty_ugraph in
97 let ty_sort2,_ = CicTypeChecker.type_of_aux' metasenv ey2 ty2
98 CicUniv.empty_ugraph in
100 let b,_ = CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1
101 CicUniv.empty_ugraph in
105 let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2
106 CicUniv.empty_ugraph in
112 let new_search_theorems f dbd proof goal depth sign =
113 let choices = f (proof,goal)
116 (function (subst,(proof, goallist)) ->
117 (* let goallist = reorder_goals dbd sign proof goallist in *)
118 let goallist = List.sort (compare_goals proof) goallist in
119 (subst,(proof,(List.map (function g -> (g,depth)) goallist), sign)))
123 exception NoOtherChoices;;
125 let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
128 if depth = 0 then [] else
129 if List.mem ty already_seen_goals then [] else
130 let already_seen_goals = ty::already_seen_goals in
131 let facts = (depth = 1) in
132 let _,metasenv,p,_ = proof in
133 (* first of all we check if the goal has been already
135 assert (CicUtil.exists_meta goal metasenv);
137 try Hashtbl.find inspected_goals ty
138 with Not_found -> NotYetInspected in
139 let is_meta_closed = CicUtil.is_meta_closed ty in
144 debug_print (lazy "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
145 debug_print (lazy (CicPp.ppterm ty));
148 (* if we just apply the subtitution, the type
149 is irrelevant: we may use Implicit, since it will
151 CicMetaSubst.apply_subst
152 [(goal,(ey, bo, Cic.Implicit None))] in
154 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
155 proof goal subst_in metasenv in
156 [(subst_in,(proof,[],sign))]
157 | No d when (d >= depth) ->
158 (* debug_print (lazy "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); *)
159 [] (* the empty list means no choices, i.e. failure *)
162 debug_print (lazy ("CURRENT GOAL = " ^ CicPp.ppterm ty));
163 debug_print (lazy ("CURRENT PROOF = " ^ CicPp.ppterm p));
164 debug_print (lazy ("CURRENT HYP = " ^ CicPp.ppcontext ey));
166 if is_meta_closed then
167 None, Some (MetadataConstraints.signature_of ty)
168 else sign,sign in (* maybe the union ? *)
171 search_theorems_in_context dbd
172 proof goal (depth-1) new_sign in
177 (new_experimental_hint
178 ~dbd ~facts:facts ?signature:sign ~universe status))
179 dbd proof goal (depth-1) new_sign in
181 local_choices@global_choices in
184 (fun (_, (_, goals1, _)) (_, (_, goals2, _)) ->
186 (List.length goals1) (List.length goals2))
188 (match (auto_new dbd width already_seen_goals universe sorted_choices)
191 (* no proof has been found; we update the
193 (* if is_meta_closed then *)
194 Hashtbl.add inspected_goals ty (No depth);
196 | (subst,(proof,[],sign))::tl1 ->
197 (* a proof for goal has been found:
198 in order to get the proof we apply subst to
200 if is_meta_closed then
203 CicMkImplicit.identity_relocation_list_for_metavariable ey in
205 subst (Cic.Meta(goal,irl)) in
206 Hashtbl.add inspected_goals
207 ty (Yes (meta_proof,depth));
211 CicTypeChecker.type_of_aux' metasenv ey meta_proof CicUniv.empty_ugraph
213 if not (cty = ty) then
215 debug_print (lazy ("ty = "^CicPp.ppterm ty));
216 debug_print (lazy ("cty = "^CicPp.ppterm cty));
219 Hashtbl.add inspected_goals
220 ty (Yes (meta_proof,depth));
224 (subst,(proof,[],sign))::tl1
228 and auto_new dbd width already_seen_goals universe = function
230 | (subst,(proof, goals, sign))::tl ->
231 let _,metasenv,_,_ = proof in
233 List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals
236 width already_seen_goals universe ((subst,(proof, goals', sign))::tl)
238 and auto_new_aux dbd width already_seen_goals universe = function
240 | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
241 | (subst,(proof, (goal,0)::_, _))::tl ->
242 auto_new dbd width already_seen_goals universe tl
243 | (subst,(proof, goals, _))::tl when
244 (List.length goals) > width ->
245 auto_new dbd width already_seen_goals universe tl
246 | (subst,(proof, (goal,depth)::gtl, sign))::tl ->
247 let _,metasenv,p,_ = proof in
248 let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
249 match (auto_single dbd proof goal ey ty depth
250 (width - (List.length gtl)) sign already_seen_goals) universe
252 [] -> auto_new dbd width already_seen_goals universe tl
253 | (local_subst,(proof,[],sign))::tl1 ->
254 let new_subst f t = f (subst t) in
255 let is_meta_closed = CicUtil.is_meta_closed ty in
257 if is_meta_closed then
258 (new_subst local_subst,(proof,gtl,sign))::tl
262 (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1)
264 (new_subst local_subst,(proof,gtl,sign))::tl2@tl in
265 auto_new dbd width already_seen_goals universe all_choices
269 let bool params name default =
271 let s = List.assoc name params in
272 if s = "" || s = "1" || s = "true" || s = "yes" then true
273 else if s = "0" || s = "false" || s = "no" then false
275 let msg = "Unrecognized value for parameter "^name^"\n" in
276 let msg = msg ^ "Accepted values are 1,true,yes and 0,false,no" in
277 raise (ProofEngineTypes.Fail (lazy msg))
278 with Not_found -> default
281 let string params name default =
282 try List.assoc name params with
283 | Not_found -> default
286 let int params name default =
287 try int_of_string (List.assoc name params) with
288 | Not_found -> default
290 raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
293 let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
294 (* argument parsing *)
296 and string = string params
297 and bool = bool params in
298 let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
299 let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
300 let timeout = int "timeout" 0 in
301 let use_paramod = bool "use_paramod" true in
302 let use_only_paramod = bool "paramodulation" false in
303 (* hacks to debug paramod *)
304 let superposition = bool "superposition" false in
305 let target = string "target" "" in
306 let table = string "table" "" in
307 let subterms_only = bool "subterms_only" false in
308 let demod_table = string "demod_table" "" in
309 match superposition with
311 (* this is the ugly hack to debug paramod *)
312 Saturation.superposition_tac
313 ~target ~table ~subterms_only ~demod_table (proof,goal)
315 (* this is the real auto *)
316 let _, metasenv, _, _ = proof in
317 let _, context, goalty = CicUtil.lookup_meta goal metasenv in
319 AutoTypes.universe_of_goals dbd proof [goal] AutoTypes.empty_universe
321 let universe = AutoTypes.universe_of_context context metasenv universe in
322 let oldmetasenv = metasenv in
324 AutoTypes.maxdepth = depth;
325 AutoTypes.maxwidth = width;
327 if timeout = 0 then float_of_int timeout
328 else Unix.gettimeofday() +. (float_of_int timeout);
329 AutoTypes.use_paramod = use_paramod;
330 AutoTypes.use_only_paramod = use_only_paramod}
332 let cache = AutoTypes.cache_empty in
333 match Auto.auto dbd universe cache context metasenv [goal] flags with
335 raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
336 | Some (subst,metasenv),cache ->
338 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
339 proof goal (CicMetaSubst.apply_subst subst) metasenv
342 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
343 ~newmetasenv:metasenv
348 let auto_tac ~params ~dbd =
349 ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd)
352 let pp_proofterm = Equality.pp_proofterm;;