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/.
28 let debug_print s = () (* prerr_endline s;; *)
30 let given_clause dbd ?tables maxm ?auto cache subst flags status =
31 prerr_endline ("given_clause " ^ string_of_int maxm);
32 let active, passive, bag, cache, maxmeta, goal_steps, saturation_steps, timeout =
35 let bag, equalities, cache, maxmeta =
36 Saturation.find_equalities dbd status ?auto true cache
38 let passive = Saturation.make_passive equalities in
39 let active = Saturation.make_active [] in
40 let goal_steps, saturation_steps, timeout =
41 if flags.use_only_paramod then max_int,max_int,flags.timeout
44 let maxm = max maxm maxmeta in
45 active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
46 | Some (active,passive,bag,oldcache) ->
47 let bag, equalities, cache, maxm =
48 if cache_size oldcache <> cache_size cache then
49 Saturation.saturate_more bag active maxm status true ?auto cache
53 let minsteps = List.length equalities in
54 let passive = Saturation.add_to_passive equalities passive in
55 let goal_steps, saturation_steps, timeout =
56 if flags.use_only_paramod then max_int,max_int,flags.timeout
57 else max 30 minsteps, minsteps, infinity
59 active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
61 let res,a,p, maxmeta =
62 Saturation.given_clause bag maxmeta status active passive
63 goal_steps saturation_steps timeout
65 res,a,p,bag,cache,maxmeta
68 (* {{{ **************** applyS *******************)
70 let new_metasenv_and_unify_and_t
71 dbd proof goal ?tables newmeta' metasenv' context term' ty termty goal_arity
73 let (consthead,newmetasenv,arguments,_) =
74 ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
76 match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
78 let proof',oldmetasenv =
79 let (puri,metasenv,pbo,pty) = proof in
80 (puri,newmetasenv,pbo,pty),metasenv
82 let goal_for_paramod =
83 match LibraryObjects.eq_URI () with
85 Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
86 | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
88 let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
89 let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
90 let proof'' = let uri,_,p,ty = proof' in uri,metasenv_for_paramod,p,ty in
91 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
93 ProofEngineTypes.apply_tactic
94 (EqualityTactics.rewrite_tac ~direction:`RightToLeft
95 ~pattern:(ProofEngineTypes.conclusion_pattern None)
96 (Cic.Meta(newmeta,irl)))
99 let goal = match goals with [g] -> g | _ -> assert false in
100 let subst, (proof'''', _), _ =
101 PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal)
104 let cache, flags = AutoTypes.cache_empty, AutoTypes.default_flags() in
106 {flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0}
108 given_clause dbd ?tables 0 cache [] flags (proof'''',newmeta)
110 | None, active, passive, bag,_,_ ->
111 raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
112 | Some (_,proof''''',_), active, passive,bag,_,_ ->
114 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
115 ~newmetasenv:(let _,m,_,_ = proof''''' in m), active, passive
118 let rec count_prods context ty =
119 match CicReduction.whd context ty with
120 Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
123 let apply_smart ~dbd ~term ~subst ?tables (proof, goal) =
124 let module T = CicTypeChecker in
125 let module R = CicReduction in
126 let module C = Cic in
127 let (_,metasenv,_,_) = proof in
128 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
129 let newmeta = CicMkImplicit.new_meta metasenv subst in
130 let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
132 C.Var (uri,exp_named_subst) ->
133 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
134 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
137 exp_named_subst_diff,newmeta',newmetasenvfragment,
138 C.Var (uri,exp_named_subst')
139 | C.Const (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.Const (uri,exp_named_subst')
146 | C.MutInd (uri,tyno,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.MutInd (uri,tyno,exp_named_subst')
153 | C.MutConstruct (uri,tyno,consno,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.MutConstruct (uri,tyno,consno,exp_named_subst')
160 | _ -> [],newmeta,[],term
162 let metasenv' = metasenv@newmetasenvfragment in
164 CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
166 let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
167 let goal_arity = count_prods context ty in
168 let subst, proof, gl, active, passive =
169 new_metasenv_and_unify_and_t dbd proof goal ?tables
170 newmeta' metasenv' context term' ty termty goal_arity
172 subst, proof, gl, active, passive
175 (* }}} **************** applyS **************)
177 (* {{{ ***************** AUTO ********************)
179 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
180 let ugraph = CicUniv.empty_ugraph;;
181 let typeof = CicTypeChecker.type_of_aux';;
183 let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
186 let is_in_prop context subst metasenv ty =
187 let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
188 fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
190 let assert_proof_is_valid proof metasenv context goalty =
191 let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
192 let b,_ = CicReduction.are_convertible context ty goalty u in
196 List.map (function None -> None | Some (x,_) -> Some x) context
198 prerr_endline ("PROOF:" ^ CicPp.pp proof names);
199 prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
200 prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
201 prerr_endline ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
205 let assert_subst_are_disjoint subst subst' =
207 (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
211 List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2)
214 let split_goals_in_prop metasenv subst gl =
217 let _,context,ty = CicUtil.lookup_meta g metasenv in
219 let sort,u = typeof ~subst metasenv context ty ugraph in
220 fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
222 | CicTypeChecker.AssertFailure s
223 | CicTypeChecker.TypeCheckerFailure s ->
224 debug_print (ppterm context (CicMetaSubst.apply_subst subst ty));
225 debug_print (Lazy.force s);
227 (* FIXME... they should type! *)
231 let split_goals_with_metas metasenv subst gl =
234 let _,context,ty = CicUtil.lookup_meta g metasenv in
235 let ty = CicMetaSubst.apply_subst subst ty in
236 CicUtil.is_meta_closed ty)
240 let order_new_goals metasenv subst open_goals ppterm =
241 let prop,rest = split_goals_in_prop metasenv subst open_goals in
242 let open_prop,closed_prop = split_goals_with_metas metasenv subst prop in
244 (List.map (fun x -> x,P) (closed_prop @ open_prop))
246 (List.map (fun x -> x,T) rest)
251 let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty) open_goals
253 debug_print (" OPEN: "^
255 (List.map (fun (i,t) -> string_of_int i ^":"^ppterm t) tys));
259 let is_an_equational_goal = function
260 | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
265 dbd tables maxm ?auto cache depth fake_proof goalno goalty subst context
268 let ppterm = ppterm context in
269 prerr_endline ("PARAMOD SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
270 prerr_endline "<CACHE>";
271 prerr_endline (cache_print context cache);
272 prerr_endline "</CACHE>";
274 given_clause dbd ?tables maxm ?auto cache subst flags (fake_proof,goalno)
276 | None, active,passive, bag, cache, maxmeta ->
277 let tables = Some (active,passive,bag,cache) in
278 None, tables, cache, maxmeta
279 | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,bag,cache,maxmeta ->
280 let tables = Some (active,passive,bag,cache) in
281 assert_subst_are_disjoint subst subst';
282 let subst = subst@subst' in
283 let open_goals = order_new_goals metasenv subst open_goals ppterm in
284 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
285 Some [metasenv,subst,open_goals], tables, cache, maxmeta
289 goalty dbd tables maxm subst fake_proof goalno depth context cand
291 let ppterm = ppterm context in
293 let subst', ((_,metasenv,_,_), open_goals), maxmeta =
294 PrimitiveTactics.apply_with_subst
295 ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno)
297 debug_print (" OK: " ^ ppterm cand);
298 assert (maxmeta >= maxm);
299 (*FIXME:sicuro che posso @?*)
300 assert_subst_are_disjoint subst subst';
301 let subst = subst@subst' in
302 let open_goals = order_new_goals metasenv subst open_goals ppterm in
303 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
304 Some (metasenv,subst,open_goals), tables , maxmeta
305 with ProofEngineTypes.Fail s ->
306 (*debug_print(" KO: "^Lazy.force s);*)None,tables, maxm
310 dbd tables maxm depth subst fake_proof goalno goalty metasenv context universe
312 let candidates = get_candidates universe goalty in
313 let tables, elems, maxm =
315 (fun (tables,elems,maxm) cand ->
318 dbd tables maxm subst fake_proof goalno depth context cand
320 | None, tables,maxm -> tables,elems, maxm
321 | Some x, tables, maxm -> tables,x::elems, maxm)
322 (tables,[],maxm) candidates
324 let elems = sort_new_elems elems in
328 (* Works if there is no dependency over proofs *)
329 let is_a_green_cut goalty =
330 CicUtil.is_meta_closed goalty
332 let prop = function (_,_,P) -> true | _ -> false;;
333 let calculate_timeout flags =
334 if flags.timeout = 0. then
335 (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
339 let is_equational_case goalty flags =
340 let ensure_equational t =
341 if is_an_equational_goal t then true
343 let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
344 raise (ProofEngineTypes.Fail (lazy msg))
346 (flags.use_paramod && is_an_equational_goal goalty) ||
347 (flags.use_only_paramod && ensure_equational goalty)
349 let cache_add_success sort cache k v =
350 if sort = P then cache_add_success cache k v else cache
353 let rec auto_main dbd tables maxm context flags elems cache universe =
354 let callback_for_paramod maxm flags proof commonctx cache l =
355 let flags = {flags with use_paramod = false} in
356 let _,metasenv,_,_ = proof in
357 let oldmetasenv = metasenv in
360 dbd tables maxm universe cache commonctx metasenv l flags
362 | [],cache,maxm -> [],cache,maxm
363 | solutions,cache,maxm ->
366 (fun (subst,newmetasenv) ->
368 ProofEngineHelpers.compare_metasenvs ~oldmetasenv ~newmetasenv
370 if opened = [] then Some subst else None)
375 let flags = calculate_timeout flags in
376 let ppterm = ppterm context in
377 let irl = mk_irl context in
378 let rec aux tables maxm cache = function (* elems in OR *)
379 | [] -> Fail "no more steps can be done", tables, cache, maxm
381 | (metasenv,subst,[])::tl ->
382 Success (metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
383 | (metasenv,subst,goals)::tl when
384 List.length (List.filter prop goals) > flags.maxwidth ->
385 debug_print (" FAILURE(width): " ^ string_of_int (List.length goals));
386 aux tables maxm cache tl (* FAILURE (width) *)
387 | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
388 if Unix.gettimeofday() > flags.timeout then
389 Fail "timeout",tables,cache,maxm
392 let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
393 debug_print ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty);
394 if sort = T && tl <> [] then (* FIXME!!!! *)
395 (debug_print (" FAILURE(not in prop)");
396 aux tables maxm cache tl (* FAILURE (not in prop) *))
398 match aux_single tables maxm cache metasenv subst elem goalty cc with
399 | Fail _, tables, cache, maxm' ->
400 assert(maxm' >= maxm);let maxm = maxm' in
401 debug_print (" FAIL: " ^string_of_int goalno^ ":"^ppterm goalty);
402 let cache = cache_add_failure cache goalty depth in
403 aux tables maxm cache tl
404 | Success (metasenv,subst,others), tables, cache, maxm' ->
405 assert(maxm' >= maxm);let maxm = maxm' in
406 (* others are alternatives in OR *)
408 let goal = Cic.Meta(goalno,irl) in
409 let proof = CicMetaSubst.apply_subst subst goal in
410 debug_print ("DONE: " ^ ppterm goalty^" with: "^ppterm proof);
411 if is_a_green_cut goalty then
412 (assert_proof_is_valid proof metasenv context goalty;
413 let cache = cache_add_success sort cache goalty proof in
414 aux tables maxm cache ((metasenv,subst,gl)::tl))
416 (let goalty = CicMetaSubst.apply_subst subst goalty in
417 assert_proof_is_valid proof metasenv context goalty;
419 if is_a_green_cut goalty then
420 cache_add_success sort cache goalty proof
426 (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl))
429 aux tables maxm cache ((metasenv,subst,gl)::others@tl))
430 with CicUtil.Meta_not_found i when i = goalno ->
432 with CicUtil.Meta_not_found i when i = goalno ->
433 (* goalno was closed by sideeffect *)
434 debug_print ("Goal "^string_of_int goalno^" closed by sideeffect");
435 aux tables maxm cache ((metasenv,subst,gl)::tl)
436 and aux_single tables maxm cache metasenv subst (goalno, depth, _) goalty cc =
437 let goalty = CicMetaSubst.apply_subst subst goalty in
438 (* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
439 (* FAILURE (euristic cut) *)
440 match cache_examine cache goalty with
441 | Failed_in d when d >= depth ->
442 Fail "depth",tables,cache,maxm(*FAILURE(depth)*)
444 assert(List.for_all (fun (i,_) -> i <> goalno) subst);
445 let entry = goalno, (cc, t,goalty) in
446 assert_subst_are_disjoint subst [entry];
447 let subst = entry :: subst in
448 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
449 debug_print (" CACHE HIT!");
450 Success (metasenv, subst, []), tables, cache, maxm
451 | UnderInspection -> Fail "looping",tables,cache, maxm
453 | Failed_in _ when depth > 0 -> (* we have more depth now *)
454 let cache = cache_add_underinspection cache goalty depth in
455 let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
456 let elems, tables, cache, maxm =
457 if is_equational_case goalty flags then
459 equational_case dbd tables maxm
460 ~auto:callback_for_paramod cache
461 depth fake_proof goalno goalty subst context flags
463 | Some elems, tables, cache, maxm ->
464 elems, tables, cache, maxm (* manca cache *)
465 | None, tables,cache,maxm ->
466 let elems, tables, maxm =
467 applicative_case dbd tables maxm depth subst fake_proof goalno
468 goalty metasenv context universe
469 in elems, tables, cache, maxm
471 let elems, tables, maxm =
472 applicative_case dbd tables maxm depth subst fake_proof goalno
473 goalty metasenv context universe
474 in elems, tables, cache, maxm
476 aux tables maxm cache elems
477 | _ -> Fail "??",tables,cache,maxm
479 aux tables maxm cache elems
482 auto_all_solutions dbd tables maxm universe cache context metasenv gl flags
484 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
485 let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
486 let elems = [metasenv,[],goals] in
487 let rec aux tables maxm solutions cache elems flags =
488 match auto_main dbd tables maxm context flags elems cache universe with
489 | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
490 | Success (metasenv,subst,others),tables,cache,maxm ->
491 if Unix.gettimeofday () > flags.timeout then
492 ((subst,metasenv)::solutions), cache, maxm
494 aux tables maxm ((subst,metasenv)::solutions) cache others flags
496 let rc = aux tables maxm [] cache elems flags in
497 prerr_endline "fine auto all solutions";
501 (* }}} ****************** AUTO ***************)
503 let auto_all_solutions dbd universe cache context metasenv gl flags =
504 let solutions, cache, _ =
505 auto_all_solutions dbd None 0 universe cache context metasenv gl flags
510 let auto dbd universe cache context metasenv gl flags =
511 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
512 let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
513 let elems = [metasenv,[],goals] in
514 match auto_main dbd None 0 context flags elems cache universe with
515 | Success (metasenv,subst,_), tables,cache,_ -> Some (subst,metasenv), cache
516 | Fail s,tables,cache,maxm ->
517 let cache = cache_clean cache in
518 match auto_main dbd tables maxm context flags elems cache universe with
519 | Success (metasenv,subst,_), tables,cache,_ ->
520 Some (subst,metasenv), cache
521 | Fail s,tables,cache,maxm -> prerr_endline s;None,cache
524 let applyS_tac ~dbd ~term =
525 ProofEngineTypes.mk_tactic
528 let _, proof, gl,_,_ = apply_smart ~dbd ~term ~subst:[] status in
531 | CicUnification.UnificationFailure msg
532 | CicTypeChecker.TypeCheckerFailure msg ->
533 raise (ProofEngineTypes.Fail msg))