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 = () (*prerr_endline s;;*)
31 (* {{{ *********** local given_clause wrapper ***********)
33 let given_clause dbd ?tables maxm auto cache subst flags smart_flag status =
34 let active,passive,bag,cache,maxmeta,goal_steps,saturation_steps,timeout =
37 (* first time, do a huge saturation *)
38 let bag, equalities, cache, maxmeta =
39 Saturation.find_equalities dbd status smart_flag auto cache
41 let passive = Saturation.make_passive equalities in
42 let active = Saturation.make_active [] in
43 let goal_steps, saturation_steps, timeout =
44 if flags.use_only_paramod then max_int,max_int,flags.timeout
47 let maxm = max maxm maxmeta in
48 active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
49 | Some (active,passive,bag,oldcache) ->
50 (* saturate a bit more if cache cahnged *)
51 let bag, equalities, cache, maxm =
52 if cache_size oldcache <> cache_size cache then
54 bag active maxm status smart_flag auto cache
58 let minsteps = List.length equalities in
59 let passive = Saturation.add_to_passive equalities passive in
60 let goal_steps, saturation_steps, timeout =
61 if flags.use_only_paramod then max_int,max_int,flags.timeout
62 else max 50 minsteps, minsteps, infinity
64 active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
66 let res,actives,passives,maxmeta =
67 Saturation.given_clause bag maxmeta status active passive
68 goal_steps saturation_steps timeout
70 res,actives,passives,bag,cache,maxmeta
73 (* }}} ****************************************************************)
75 (* {{{ **************** applyS *******************)
77 let new_metasenv_and_unify_and_t
78 dbd flags proof goal ?tables newmeta' metasenv' context term' ty termty
81 let (consthead,newmetasenv,arguments,_) =
82 ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
84 match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
86 let proof',oldmetasenv =
87 let (puri,metasenv,pbo,pty) = proof in
88 (puri,newmetasenv,pbo,pty),metasenv
90 let goal_for_paramod =
91 match LibraryObjects.eq_URI () with
93 Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
94 | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
96 let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
97 let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
98 let proof'' = let uri,_,p,ty = proof' in uri,metasenv_for_paramod,p,ty in
99 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
101 ProofEngineTypes.apply_tactic
102 (EqualityTactics.rewrite_tac ~direction:`RightToLeft
103 ~pattern:(ProofEngineTypes.conclusion_pattern None)
104 (Cic.Meta(newmeta,irl)))
107 let goal = match goals with [g] -> g | _ -> assert false in
108 let subst, (proof'''', _), _ =
109 PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal)
112 let cache = cache_empty in
113 given_clause dbd ?tables 0 None cache [] flags true (proof'''',newmeta)
115 | None, active, passive, bag,_,_ ->
116 raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
117 | Some (_,proof''''',_), active, passive,bag,_,_ ->
119 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
120 ~newmetasenv:(let _,m,_,_ = proof''''' in m), active, passive
123 let rec count_prods context ty =
124 match CicReduction.whd context ty with
125 Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
128 let apply_smart ~dbd ~term ~subst ?tables flags (proof, goal) =
129 let module T = CicTypeChecker in
130 let module R = CicReduction in
131 let module C = Cic in
132 let (_,metasenv,_,_) = proof in
133 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
134 let newmeta = CicMkImplicit.new_meta metasenv subst in
135 let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
137 C.Var (uri,exp_named_subst) ->
138 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
139 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
142 exp_named_subst_diff,newmeta',newmetasenvfragment,
143 C.Var (uri,exp_named_subst')
144 | C.Const (uri,exp_named_subst) ->
145 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
146 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
149 exp_named_subst_diff,newmeta',newmetasenvfragment,
150 C.Const (uri,exp_named_subst')
151 | C.MutInd (uri,tyno,exp_named_subst) ->
152 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
153 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
156 exp_named_subst_diff,newmeta',newmetasenvfragment,
157 C.MutInd (uri,tyno,exp_named_subst')
158 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
159 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
160 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
163 exp_named_subst_diff,newmeta',newmetasenvfragment,
164 C.MutConstruct (uri,tyno,consno,exp_named_subst')
165 | _ -> [],newmeta,[],term
167 let metasenv' = metasenv@newmetasenvfragment in
169 CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
171 let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
172 let goal_arity = count_prods context ty in
173 let subst, proof, gl, active, passive =
174 new_metasenv_and_unify_and_t dbd flags proof goal ?tables
175 newmeta' metasenv' context term' ty termty goal_arity
177 subst, proof, gl, active, passive
180 (* }}} **************** applyS **************)
182 (* {{{ ***************** AUTO ********************)
184 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
185 let ugraph = CicUniv.empty_ugraph;;
186 let typeof = CicTypeChecker.type_of_aux';;
188 let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
191 let is_in_prop context subst metasenv ty =
192 let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
193 fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
195 let assert_proof_is_valid proof metasenv context goalty =
196 let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
197 let b,_ = CicReduction.are_convertible context ty goalty u in
201 List.map (function None -> None | Some (x,_) -> Some x) context
203 prerr_endline ("PROOF:" ^ CicPp.pp proof names);
204 prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
205 prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
206 prerr_endline ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
210 let assert_subst_are_disjoint subst subst' =
212 (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
216 List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2)
219 let split_goals_in_prop metasenv subst gl =
222 let _,context,ty = CicUtil.lookup_meta g metasenv in
224 let sort,u = typeof ~subst metasenv context ty ugraph in
225 fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
227 | CicTypeChecker.AssertFailure s
228 | CicTypeChecker.TypeCheckerFailure s ->
229 debug_print (ppterm context (CicMetaSubst.apply_subst subst ty));
230 debug_print (Lazy.force s);
232 (* FIXME... they should type! *)
236 let split_goals_with_metas metasenv subst gl =
239 let _,context,ty = CicUtil.lookup_meta g metasenv in
240 let ty = CicMetaSubst.apply_subst subst ty in
241 CicUtil.is_meta_closed ty)
245 let order_new_goals metasenv subst open_goals ppterm =
246 let prop,rest = split_goals_in_prop metasenv subst open_goals in
247 let open_prop,closed_prop = split_goals_with_metas metasenv subst prop in
249 (List.map (fun x -> x,P) (closed_prop @ open_prop))
251 (List.map (fun x -> x,T) rest)
256 let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty) open_goals
258 debug_print (" OPEN: "^
260 (List.map (fun (i,t) -> string_of_int i ^":"^ppterm t) tys));
264 let is_an_equational_goal = function
265 | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
270 dbd tables maxm auto cache depth fake_proof goalno goalty subst context
273 let ppterm = ppterm context in
274 prerr_endline ("PARAMOD SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
276 prerr_endline "<CACHE>";
277 prerr_endline (cache_print context cache);
278 prerr_endline "</CACHE>";
281 given_clause dbd ?tables maxm auto cache subst flags false (fake_proof,goalno)
283 | None, active,passive, bag, cache, maxmeta ->
284 let tables = Some (active,passive,bag,cache) in
285 None, tables, cache, maxmeta
286 | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,bag,cache,maxmeta ->
287 let tables = Some (active,passive,bag,cache) in
288 assert_subst_are_disjoint subst subst';
289 let subst = subst@subst' in
290 let open_goals = order_new_goals metasenv subst open_goals ppterm in
291 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
292 Some [metasenv,subst,open_goals], tables, cache, maxmeta
296 goalty dbd tables maxm subst fake_proof goalno depth context cand
298 let ppterm = ppterm context in
300 let subst', ((_,metasenv,_,_), open_goals), maxmeta =
301 PrimitiveTactics.apply_with_subst
302 ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno)
304 debug_print (" OK: " ^ ppterm cand);
305 assert (maxmeta >= maxm);
306 (*FIXME:sicuro che posso @?*)
307 assert_subst_are_disjoint subst subst';
308 let subst = subst@subst' in
309 let open_goals = order_new_goals metasenv subst open_goals ppterm in
310 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
311 Some (metasenv,subst,open_goals), tables , maxmeta
312 with ProofEngineTypes.Fail s ->
313 (*debug_print(" KO: "^Lazy.force s);*)None,tables, maxm
317 dbd tables maxm depth subst fake_proof goalno goalty metasenv context cache
319 let candidates = get_candidates cache goalty in
320 let tables, elems, maxm =
322 (fun (tables,elems,maxm) cand ->
325 dbd tables maxm subst fake_proof goalno depth context cand
327 | None, tables,maxm -> tables,elems, maxm
328 | Some x, tables, maxm -> tables,x::elems, maxm)
329 (tables,[],maxm) candidates
331 let elems = sort_new_elems elems in
332 elems, tables, cache, maxm
335 (* Works if there is no dependency over proofs *)
336 let is_a_green_cut goalty =
337 CicUtil.is_meta_closed goalty
339 let prop = function (_,_,P) -> true | _ -> false;;
340 let calculate_timeout flags =
341 if flags.timeout = 0. then
342 (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
346 let is_equational_case goalty flags =
347 let ensure_equational t =
348 if is_an_equational_goal t then true
351 let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
352 raise (ProofEngineTypes.Fail (lazy msg))
355 (flags.use_paramod && is_an_equational_goal goalty) ||
356 (flags.use_only_paramod && ensure_equational goalty)
358 let cache_add_success sort cache k v =
359 if sort = P then cache_add_success cache k v else cache_remove_underinspection
363 let rec auto_main dbd tables maxm context flags elems cache =
364 let callback_for_paramod maxm flags proof commonctx cache l =
365 let flags = {flags with use_paramod = false;dont_cache_failures=true} in
366 let _,metasenv,_,_ = proof in
367 let oldmetasenv = metasenv in
370 dbd tables maxm cache commonctx metasenv l flags
372 | [],cache,maxm -> [],cache,maxm
373 | solutions,cache,maxm ->
376 (fun (subst,newmetasenv) ->
378 ProofEngineHelpers.compare_metasenvs ~oldmetasenv ~newmetasenv
380 if opened = [] then Some subst else None)
385 let flags = calculate_timeout flags in
386 let ppterm = ppterm context in
387 let irl = mk_irl context in
388 let rec aux tables maxm cache = function (* elems in OR *)
389 | [] -> Fail "no more steps can be done", tables, cache, maxm
391 | (metasenv,subst,[])::tl ->
392 Success (metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
393 | (metasenv,subst,goals)::tl when
394 List.length (List.filter prop goals) > flags.maxwidth ->
395 debug_print (" FAILURE(width): " ^ string_of_int (List.length goals));
396 aux tables maxm cache tl (* FAILURE (width) *)
397 | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
398 if Unix.gettimeofday() > flags.timeout then
399 Fail "timeout",tables,cache,maxm
402 let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
403 debug_print ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty);
404 if sort = T && tl <> [] then (* FIXME!!!! *)
405 (debug_print (" FAILURE(not in prop)");
406 aux tables maxm cache tl (* FAILURE (not in prop) *))
408 match aux_single tables maxm cache metasenv subst elem goalty cc with
409 | Fail s, tables, cache, maxm' ->
410 assert(maxm' >= maxm);let maxm = maxm' in
412 (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty);
414 if flags.dont_cache_failures then
415 cache_remove_underinspection cache goalty
416 else cache_add_failure cache goalty depth
418 aux tables maxm cache tl
419 | Success (metasenv,subst,others), tables, cache, maxm' ->
420 assert(maxm' >= maxm);let maxm = maxm' in
421 (* others are alternatives in OR *)
423 let goal = Cic.Meta(goalno,irl) in
424 let proof = CicMetaSubst.apply_subst subst goal in
425 debug_print ("DONE: " ^ ppterm goalty^" with: "^ppterm proof);
426 if is_a_green_cut goalty then
427 (assert_proof_is_valid proof metasenv context goalty;
428 let cache = cache_add_success sort cache goalty proof in
429 aux tables maxm cache ((metasenv,subst,gl)::tl))
431 (let goalty = CicMetaSubst.apply_subst subst goalty in
432 assert_proof_is_valid proof metasenv context goalty;
434 if is_a_green_cut goalty then
435 cache_add_success sort cache goalty proof
441 (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl))
444 aux tables maxm cache ((metasenv,subst,gl)::others@tl))
445 with CicUtil.Meta_not_found i when i = goalno ->
447 with CicUtil.Meta_not_found i when i = goalno ->
448 (* goalno was closed by sideeffect *)
449 debug_print ("Goal "^string_of_int goalno^" closed by sideeffect");
450 aux tables maxm cache ((metasenv,subst,gl)::tl)
451 and aux_single tables maxm cache metasenv subst (goalno, depth, _) goalty cc =
452 let goalty = CicMetaSubst.apply_subst subst goalty in
453 (* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
454 (* FAILURE (euristic cut) *)
455 match cache_examine cache goalty with
456 | Failed_in d when d >= depth ->
457 Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
458 tables,cache,maxm(*FAILURE(depth)*)
460 assert(List.for_all (fun (i,_) -> i <> goalno) subst);
461 let entry = goalno, (cc, t,goalty) in
462 assert_subst_are_disjoint subst [entry];
463 let subst = entry :: subst in
464 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
465 debug_print (" CACHE HIT!");
466 Success (metasenv, subst, []), tables, cache, maxm
467 | UnderInspection -> Fail "looping",tables,cache, maxm
469 | Failed_in _ when depth > 0 -> (* we have more depth now *)
470 let cache = cache_add_underinspection cache goalty depth in
471 let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
472 let elems, tables, cache, maxm =
473 if is_equational_case goalty flags then
475 equational_case dbd tables maxm
476 (Some callback_for_paramod) cache
477 depth fake_proof goalno goalty subst context flags
479 | Some elems, tables, cache, maxm ->
480 elems, tables, cache, maxm
481 | None, tables,cache,maxm ->
482 applicative_case dbd tables maxm depth subst fake_proof goalno
483 goalty metasenv context cache
485 applicative_case dbd tables maxm depth subst fake_proof goalno
486 goalty metasenv context cache
488 aux tables maxm cache elems
489 | _ -> Fail "??",tables,cache,maxm
491 aux tables maxm cache elems
494 auto_all_solutions dbd tables maxm cache context metasenv gl flags
496 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
497 let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
498 let elems = [metasenv,[],goals] in
499 let rec aux tables maxm solutions cache elems flags =
500 match auto_main dbd tables maxm context flags elems cache with
501 | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
502 | Success (metasenv,subst,others),tables,cache,maxm ->
503 if Unix.gettimeofday () > flags.timeout then
504 ((subst,metasenv)::solutions), cache, maxm
506 aux tables maxm ((subst,metasenv)::solutions) cache others flags
508 let rc = aux tables maxm [] cache elems flags in
509 prerr_endline "fine auto all solutions";
513 (* }}} ****************** AUTO ***************)
515 let auto_all_solutions dbd cache context metasenv gl flags =
516 let solutions, cache, _ =
517 auto_all_solutions dbd None 0 cache context metasenv gl flags
522 let auto dbd cache context metasenv gl flags =
523 let initial_time = Unix.gettimeofday() in
524 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
525 let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
526 let elems = [metasenv,[],goals] in
527 match auto_main dbd None 0 context flags elems cache with
528 | Success (metasenv,subst,_), tables,cache,_ ->
529 prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
530 Some (subst,metasenv), cache
531 | Fail s,tables,cache,maxm -> None,cache
534 let bool params name default =
536 let s = List.assoc name params in
537 if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
538 else if s = "0" || s = "false" || s = "no" || s= "off" then false
540 let msg = "Unrecognized value for parameter "^name^"\n" in
541 let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
542 raise (ProofEngineTypes.Fail (lazy msg))
543 with Not_found -> default
546 let string params name default =
547 try List.assoc name params with
548 | Not_found -> default
551 let int params name default =
552 try int_of_string (List.assoc name params) with
553 | Not_found -> default
555 raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
558 let flags_of_params params ?(use_only_paramod = bool params "paramodulation" false) () =
559 let int = int params in
560 let bool = bool params in
561 let use_paramod = bool "use_paramod" true in
562 let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
563 let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
564 let timeout = int "timeout" 0 in
565 { AutoTypes.maxdepth =
566 if use_only_paramod then 2 else depth;
567 AutoTypes.maxwidth = width;
570 if use_only_paramod then Unix.gettimeofday () +. 30.0
574 Unix.gettimeofday() +. (float_of_int timeout);
575 AutoTypes.use_paramod = use_paramod;
576 AutoTypes.use_only_paramod = use_only_paramod;
577 AutoTypes.dont_cache_failures = false
580 let applyS_tac ~dbd ~term ~params =
581 ProofEngineTypes.mk_tactic
584 let _, proof, gl,_,_ =
585 apply_smart ~dbd ~term ~subst:[]
586 (flags_of_params params ~use_only_paramod:true ()) status
590 | CicUnification.UnificationFailure msg
591 | CicTypeChecker.TypeCheckerFailure msg ->
592 raise (ProofEngineTypes.Fail msg))
594 let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) =
595 (* argument parsing *)
596 let string = string params in
597 let bool = bool params in
598 let use_only_paramod = bool "paramodulation" false in
599 (* hacks to debug paramod *)
600 let superposition = bool "superposition" false in
601 let target = string "target" "" in
602 let table = string "table" "" in
603 let subterms_only = bool "subterms_only" false in
604 let demod_table = string "demod_table" "" in
605 match superposition with
607 (* this is the ugly hack to debug paramod *)
608 Saturation.superposition_tac
609 ~target ~table ~subterms_only ~demod_table (proof,goal)
611 (* this is the real auto *)
612 let _, metasenv, _, _ = proof in
613 let _, context, goalty = CicUtil.lookup_meta goal metasenv in
616 AutoCache.cache_add_context context metasenv AutoCache.cache_empty
618 if use_only_paramod then (* only paramod *)
621 AutoCache.cache_add_library dbd proof [goal] cache
623 let oldmetasenv = metasenv in
624 let flags = flags_of_params params () in
625 match auto dbd cache context metasenv [goal] flags with
627 raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
628 | Some (subst,metasenv),cache ->
630 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
631 proof goal (CicMetaSubst.apply_subst subst) metasenv
634 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
635 ~newmetasenv:metasenv
640 let auto_tac ~dbd ~params = ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd);;