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 proof goal ?tables newmeta' metasenv' context term' ty termty goal_arity
80 let (consthead,newmetasenv,arguments,_) =
81 ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
83 match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
85 let proof',oldmetasenv =
86 let (puri,metasenv,pbo,pty) = proof in
87 (puri,newmetasenv,pbo,pty),metasenv
89 let goal_for_paramod =
90 match LibraryObjects.eq_URI () with
92 Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
93 | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
95 let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
96 let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
97 let proof'' = let uri,_,p,ty = proof' in uri,metasenv_for_paramod,p,ty in
98 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
100 ProofEngineTypes.apply_tactic
101 (EqualityTactics.rewrite_tac ~direction:`RightToLeft
102 ~pattern:(ProofEngineTypes.conclusion_pattern None)
103 (Cic.Meta(newmeta,irl)))
106 let goal = match goals with [g] -> g | _ -> assert false in
107 let subst, (proof'''', _), _ =
108 PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal)
111 let cache, flags = cache_empty, default_flags() in
113 {flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0}
115 given_clause dbd ?tables 0 None cache [] flags true (proof'''',newmeta)
117 | None, active, passive, bag,_,_ ->
118 raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
119 | Some (_,proof''''',_), active, passive,bag,_,_ ->
121 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
122 ~newmetasenv:(let _,m,_,_ = proof''''' in m), active, passive
125 let rec count_prods context ty =
126 match CicReduction.whd context ty with
127 Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
130 let apply_smart ~dbd ~term ~subst ?tables (proof, goal) =
131 let module T = CicTypeChecker in
132 let module R = CicReduction in
133 let module C = Cic in
134 let (_,metasenv,_,_) = proof in
135 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
136 let newmeta = CicMkImplicit.new_meta metasenv subst in
137 let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
139 C.Var (uri,exp_named_subst) ->
140 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
141 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
144 exp_named_subst_diff,newmeta',newmetasenvfragment,
145 C.Var (uri,exp_named_subst')
146 | C.Const (uri,exp_named_subst) ->
147 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
148 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
151 exp_named_subst_diff,newmeta',newmetasenvfragment,
152 C.Const (uri,exp_named_subst')
153 | C.MutInd (uri,tyno,exp_named_subst) ->
154 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
155 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
158 exp_named_subst_diff,newmeta',newmetasenvfragment,
159 C.MutInd (uri,tyno,exp_named_subst')
160 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
161 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
162 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
165 exp_named_subst_diff,newmeta',newmetasenvfragment,
166 C.MutConstruct (uri,tyno,consno,exp_named_subst')
167 | _ -> [],newmeta,[],term
169 let metasenv' = metasenv@newmetasenvfragment in
171 CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
173 let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
174 let goal_arity = count_prods context ty in
175 let subst, proof, gl, active, passive =
176 new_metasenv_and_unify_and_t dbd proof goal ?tables
177 newmeta' metasenv' context term' ty termty goal_arity
179 subst, proof, gl, active, passive
182 (* }}} **************** applyS **************)
184 (* {{{ ***************** AUTO ********************)
186 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
187 let ugraph = CicUniv.empty_ugraph;;
188 let typeof = CicTypeChecker.type_of_aux';;
190 let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
193 let is_in_prop context subst metasenv ty =
194 let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
195 fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
197 let assert_proof_is_valid proof metasenv context goalty =
198 let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
199 let b,_ = CicReduction.are_convertible context ty goalty u in
203 List.map (function None -> None | Some (x,_) -> Some x) context
205 prerr_endline ("PROOF:" ^ CicPp.pp proof names);
206 prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
207 prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
208 prerr_endline ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
212 let assert_subst_are_disjoint subst subst' =
214 (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
218 List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2)
221 let split_goals_in_prop metasenv subst gl =
224 let _,context,ty = CicUtil.lookup_meta g metasenv in
226 let sort,u = typeof ~subst metasenv context ty ugraph in
227 fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
229 | CicTypeChecker.AssertFailure s
230 | CicTypeChecker.TypeCheckerFailure s ->
231 debug_print (ppterm context (CicMetaSubst.apply_subst subst ty));
232 debug_print (Lazy.force s);
234 (* FIXME... they should type! *)
238 let split_goals_with_metas metasenv subst gl =
241 let _,context,ty = CicUtil.lookup_meta g metasenv in
242 let ty = CicMetaSubst.apply_subst subst ty in
243 CicUtil.is_meta_closed ty)
247 let order_new_goals metasenv subst open_goals ppterm =
248 let prop,rest = split_goals_in_prop metasenv subst open_goals in
249 let open_prop,closed_prop = split_goals_with_metas metasenv subst prop in
251 (List.map (fun x -> x,P) (closed_prop @ open_prop))
253 (List.map (fun x -> x,T) rest)
258 let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty) open_goals
260 debug_print (" OPEN: "^
262 (List.map (fun (i,t) -> string_of_int i ^":"^ppterm t) tys));
266 let is_an_equational_goal = function
267 | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
272 dbd tables maxm auto cache depth fake_proof goalno goalty subst context
275 let ppterm = ppterm context in
276 prerr_endline ("PARAMOD SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
278 prerr_endline "<CACHE>";
279 prerr_endline (cache_print context cache);
280 prerr_endline "</CACHE>";
283 given_clause dbd ?tables maxm auto cache subst flags false (fake_proof,goalno)
285 | None, active,passive, bag, cache, maxmeta ->
286 let tables = Some (active,passive,bag,cache) in
287 None, tables, cache, maxmeta
288 | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,bag,cache,maxmeta ->
289 let tables = Some (active,passive,bag,cache) in
290 assert_subst_are_disjoint subst subst';
291 let subst = subst@subst' in
292 let open_goals = order_new_goals metasenv subst open_goals ppterm in
293 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
294 Some [metasenv,subst,open_goals], tables, cache, maxmeta
298 goalty dbd tables maxm subst fake_proof goalno depth context cand
300 let ppterm = ppterm context in
302 let subst', ((_,metasenv,_,_), open_goals), maxmeta =
303 PrimitiveTactics.apply_with_subst
304 ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno)
306 debug_print (" OK: " ^ ppterm cand);
307 assert (maxmeta >= maxm);
308 (*FIXME:sicuro che posso @?*)
309 assert_subst_are_disjoint subst subst';
310 let subst = subst@subst' in
311 let open_goals = order_new_goals metasenv subst open_goals ppterm in
312 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
313 Some (metasenv,subst,open_goals), tables , maxmeta
314 with ProofEngineTypes.Fail s ->
315 (*debug_print(" KO: "^Lazy.force s);*)None,tables, maxm
319 dbd tables maxm depth subst fake_proof goalno goalty metasenv context cache
321 let candidates = get_candidates cache goalty in
322 let tables, elems, maxm =
324 (fun (tables,elems,maxm) cand ->
327 dbd tables maxm subst fake_proof goalno depth context cand
329 | None, tables,maxm -> tables,elems, maxm
330 | Some x, tables, maxm -> tables,x::elems, maxm)
331 (tables,[],maxm) candidates
333 let elems = sort_new_elems elems in
334 elems, tables, cache, maxm
337 (* Works if there is no dependency over proofs *)
338 let is_a_green_cut goalty =
339 CicUtil.is_meta_closed goalty
341 let prop = function (_,_,P) -> true | _ -> false;;
342 let calculate_timeout flags =
343 if flags.timeout = 0. then
344 (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
348 let is_equational_case goalty flags =
349 let ensure_equational t =
350 if is_an_equational_goal t then true
353 let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
354 raise (ProofEngineTypes.Fail (lazy msg))
357 (flags.use_paramod && is_an_equational_goal goalty) ||
358 (flags.use_only_paramod && ensure_equational goalty)
360 let cache_add_success sort cache k v =
361 if sort = P then cache_add_success cache k v else cache_remove_underinspection
365 let rec auto_main dbd tables maxm context flags elems cache =
366 let callback_for_paramod maxm flags proof commonctx cache l =
367 let flags = {flags with use_paramod = false;dont_cache_failures=true} in
368 let _,metasenv,_,_ = proof in
369 let oldmetasenv = metasenv in
372 dbd tables maxm cache commonctx metasenv l flags
374 | [],cache,maxm -> [],cache,maxm
375 | solutions,cache,maxm ->
378 (fun (subst,newmetasenv) ->
380 ProofEngineHelpers.compare_metasenvs ~oldmetasenv ~newmetasenv
382 if opened = [] then Some subst else None)
387 let flags = calculate_timeout flags in
388 let ppterm = ppterm context in
389 let irl = mk_irl context in
390 let rec aux tables maxm cache = function (* elems in OR *)
391 | [] -> Fail "no more steps can be done", tables, cache, maxm
393 | (metasenv,subst,[])::tl ->
394 Success (metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
395 | (metasenv,subst,goals)::tl when
396 List.length (List.filter prop goals) > flags.maxwidth ->
397 debug_print (" FAILURE(width): " ^ string_of_int (List.length goals));
398 aux tables maxm cache tl (* FAILURE (width) *)
399 | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
400 if Unix.gettimeofday() > flags.timeout then
401 Fail "timeout",tables,cache,maxm
404 let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
405 debug_print ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty);
406 if sort = T && tl <> [] then (* FIXME!!!! *)
407 (debug_print (" FAILURE(not in prop)");
408 aux tables maxm cache tl (* FAILURE (not in prop) *))
410 match aux_single tables maxm cache metasenv subst elem goalty cc with
411 | Fail s, tables, cache, maxm' ->
412 assert(maxm' >= maxm);let maxm = maxm' in
414 (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty);
416 if flags.dont_cache_failures then
417 cache_remove_underinspection cache goalty
418 else cache_add_failure cache goalty depth
420 aux tables maxm cache tl
421 | Success (metasenv,subst,others), tables, cache, maxm' ->
422 assert(maxm' >= maxm);let maxm = maxm' in
423 (* others are alternatives in OR *)
425 let goal = Cic.Meta(goalno,irl) in
426 let proof = CicMetaSubst.apply_subst subst goal in
427 debug_print ("DONE: " ^ ppterm goalty^" with: "^ppterm proof);
428 if is_a_green_cut goalty then
429 (assert_proof_is_valid proof metasenv context goalty;
430 let cache = cache_add_success sort cache goalty proof in
431 aux tables maxm cache ((metasenv,subst,gl)::tl))
433 (let goalty = CicMetaSubst.apply_subst subst goalty in
434 assert_proof_is_valid proof metasenv context goalty;
436 if is_a_green_cut goalty then
437 cache_add_success sort cache goalty proof
443 (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl))
446 aux tables maxm cache ((metasenv,subst,gl)::others@tl))
447 with CicUtil.Meta_not_found i when i = goalno ->
449 with CicUtil.Meta_not_found i when i = goalno ->
450 (* goalno was closed by sideeffect *)
451 debug_print ("Goal "^string_of_int goalno^" closed by sideeffect");
452 aux tables maxm cache ((metasenv,subst,gl)::tl)
453 and aux_single tables maxm cache metasenv subst (goalno, depth, _) goalty cc =
454 let goalty = CicMetaSubst.apply_subst subst goalty in
455 (* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
456 (* FAILURE (euristic cut) *)
457 match cache_examine cache goalty with
458 | Failed_in d when d >= depth ->
459 Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
460 tables,cache,maxm(*FAILURE(depth)*)
462 assert(List.for_all (fun (i,_) -> i <> goalno) subst);
463 let entry = goalno, (cc, t,goalty) in
464 assert_subst_are_disjoint subst [entry];
465 let subst = entry :: subst in
466 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
467 debug_print (" CACHE HIT!");
468 Success (metasenv, subst, []), tables, cache, maxm
469 | UnderInspection -> Fail "looping",tables,cache, maxm
471 | Failed_in _ when depth > 0 -> (* we have more depth now *)
472 let cache = cache_add_underinspection cache goalty depth in
473 let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
474 let elems, tables, cache, maxm =
475 if is_equational_case goalty flags then
477 equational_case dbd tables maxm
478 (Some callback_for_paramod) cache
479 depth fake_proof goalno goalty subst context flags
481 | Some elems, tables, cache, maxm ->
482 elems, tables, cache, maxm
483 | None, tables,cache,maxm ->
484 applicative_case dbd tables maxm depth subst fake_proof goalno
485 goalty metasenv context cache
487 applicative_case dbd tables maxm depth subst fake_proof goalno
488 goalty metasenv context cache
490 aux tables maxm cache elems
491 | _ -> Fail "??",tables,cache,maxm
493 aux tables maxm cache elems
496 auto_all_solutions dbd tables maxm cache context metasenv gl flags
498 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
499 let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
500 let elems = [metasenv,[],goals] in
501 let rec aux tables maxm solutions cache elems flags =
502 match auto_main dbd tables maxm context flags elems cache with
503 | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
504 | Success (metasenv,subst,others),tables,cache,maxm ->
505 if Unix.gettimeofday () > flags.timeout then
506 ((subst,metasenv)::solutions), cache, maxm
508 aux tables maxm ((subst,metasenv)::solutions) cache others flags
510 let rc = aux tables maxm [] cache elems flags in
511 prerr_endline "fine auto all solutions";
515 (* }}} ****************** AUTO ***************)
517 let auto_all_solutions dbd cache context metasenv gl flags =
518 let solutions, cache, _ =
519 auto_all_solutions dbd None 0 cache context metasenv gl flags
524 let auto dbd cache context metasenv gl flags =
525 let initial_time = Unix.gettimeofday() in
526 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
527 let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
528 let elems = [metasenv,[],goals] in
529 match auto_main dbd None 0 context flags elems cache with
530 | Success (metasenv,subst,_), tables,cache,_ ->
531 prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
532 Some (subst,metasenv), cache
533 | Fail s,tables,cache,maxm -> None,cache
536 let applyS_tac ~dbd ~term =
537 ProofEngineTypes.mk_tactic
540 let _, proof, gl,_,_ = apply_smart ~dbd ~term ~subst:[] status in
543 | CicUnification.UnificationFailure msg
544 | CicTypeChecker.TypeCheckerFailure msg ->
545 raise (ProofEngineTypes.Fail msg))