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 mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
31 let ugraph = CicUniv.empty_ugraph;;
32 let typeof = CicTypeChecker.type_of_aux';;
34 let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
37 let is_in_prop context subst metasenv ty =
38 let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
39 fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
41 let assert_proof_is_valid proof metasenv context goalty =
42 let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
43 let b,_ = CicReduction.are_convertible context ty goalty u in
46 prerr_endline (CicPp.ppterm proof);
47 prerr_endline (CicPp.ppterm ty);
48 prerr_endline (CicPp.ppterm goalty);
52 let assert_subst_are_disjoint subst subst' =
54 (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
58 List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2)
61 let split_goals_in_prop metasenv subst gl =
64 let _,context,ty = CicUtil.lookup_meta g metasenv in
66 let sort,u = typeof ~subst metasenv context ty ugraph in
67 fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
69 | CicTypeChecker.AssertFailure s
70 | CicTypeChecker.TypeCheckerFailure s ->
71 debug_print (ppterm context (CicMetaSubst.apply_subst subst ty));
72 debug_print (Lazy.force s);
74 (* FIXME... they should type! *)
78 let split_goals_with_metas metasenv subst gl =
81 let _,context,ty = CicUtil.lookup_meta g metasenv in
82 let ty = CicMetaSubst.apply_subst subst ty in
83 CicUtil.is_meta_closed ty)
87 let order_new_goals metasenv subst open_goals ppterm =
88 let prop,rest = split_goals_in_prop metasenv subst open_goals in
89 let open_prop,closed_prop = split_goals_with_metas metasenv subst prop in
91 (List.map (fun x -> x,P) (closed_prop @ open_prop))
93 (List.map (fun x -> x,T) rest)
98 let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty) open_goals
100 debug_print (" OPEN: "^
102 (List.map (fun (i,t) -> string_of_int i ^":"^ppterm t) tys));
106 let try_candidate subst fake_proof goalno depth context cand =
107 let ppterm = ppterm context in
109 debug_print (" PROVO: " ^ ppterm cand);
110 let subst', ((_,metasenv,_,_), open_goals) =
111 PrimitiveTactics.apply_with_subst ~term:cand ~subst (fake_proof,goalno)
113 debug_print (" OK: " ^ ppterm cand);
114 (*FIXME:sicuro che posso @?*)
115 assert_subst_are_disjoint subst subst';
116 let subst = subst@subst' in
117 let open_goals = order_new_goals metasenv subst open_goals ppterm in
118 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
119 Some (metasenv,subst,open_goals)
120 with ProofEngineTypes.Fail s -> (*debug_print(" KO: "^Lazy.force s);*)None
123 (* Works if there is no dependency over proofs *)
124 let is_a_green_cut goalty =
125 CicUtil.is_meta_closed goalty
127 let prop = function (_,_,P) -> true | _ -> false;;
129 let auto_main context flags elems cache universe =
131 if flags.timeout = 0. then
134 Unix.gettimeofday () +. flags.timeout
136 let ppterm = ppterm context in
137 let irl = mk_irl context in
138 let rec aux cache = function (* elems in OR *)
139 | [] -> Fail "no more steps can be done", cache (* COMPLETE FAILURE *)
140 | (metasenv,subst,[])::tl ->
141 Success (metasenv,subst,tl), cache (* solution::cont *)
142 | (metasenv,subst,goals)::tl when
143 List.length (List.filter prop goals) > flags.maxwidth ->
144 debug_print (" FAILURE(width): " ^ string_of_int (List.length goals));
145 aux cache tl (* FAILURE (width) *)
146 | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
147 if Unix.gettimeofday() > timeout then Fail "timeout",cache
150 let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
151 debug_print ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty);
153 (debug_print (" FAILURE(not in prop)");
154 aux cache tl (* FAILURE (not in prop) *))
156 match aux_single cache metasenv subst elem goalty cc with
158 debug_print (" FAIL: " ^string_of_int goalno^ ":"^ppterm goalty);
159 let cache = cache_add_failure cache goalty depth in
161 | Success (metasenv,subst,others), cache ->
162 (* others are alternatives in OR *)
164 let goal = Cic.Meta(goalno,irl) in
165 let proof = CicMetaSubst.apply_subst subst goal in
166 debug_print ("DONE: " ^ ppterm goalty^" with: "^ppterm proof);
167 if is_a_green_cut goalty then
168 (assert_proof_is_valid proof metasenv context goalty;
169 let cache = cache_add_success cache goalty proof in
170 aux cache ((metasenv,subst,gl)::tl))
172 (let goalty = CicMetaSubst.apply_subst subst goalty in
173 assert_proof_is_valid proof metasenv context goalty;
175 if is_a_green_cut goalty then
176 cache_add_success cache goalty proof
182 (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl))
185 aux cache ((metasenv,subst,gl)::others@tl))
186 with CicUtil.Meta_not_found i when i = goalno ->
188 with CicUtil.Meta_not_found i when i = goalno ->
189 (* goalno was closed by sideeffect *)
190 aux cache ((metasenv,subst,gl)::tl)
191 and aux_single cache metasenv subst (goalno, depth, _) goalty cc =
192 let goalty = CicMetaSubst.apply_subst subst goalty in
193 (* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
194 (* FAILURE (euristic cut) *)
195 match cache_examine cache goalty with
196 | Failed_in d when d >= depth -> Fail "depth",cache(*FAILURE(depth)*)
198 assert(List.for_all (fun (i,_) -> i <> goalno) subst);
199 let entry = goalno, (cc, t,goalty) in
200 assert_subst_are_disjoint subst [entry];
201 let subst = entry :: subst in
202 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
203 debug_print (" CACHE HIT!");
204 Success (metasenv, subst, []),cache
205 | UnderInspection -> Fail "looping",cache
207 | Failed_in _ when depth > 0 -> (* we have more depth now *)
208 let cache = cache_add_underinspection cache goalty depth in
209 let candidates = get_candidates universe goalty in
210 let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
213 (try_candidate subst fake_proof goalno depth context)
216 let elems = sort_new_elems elems in
218 | _ -> Fail "??",cache
223 let auto universe cache context metasenv gl flags =
224 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
225 let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
226 let elems = [metasenv,[],goals] in
227 match auto_main context flags elems cache universe with
228 | Fail s,cache -> prerr_endline s;None,cache
229 | Success (metasenv,subst,_), cache -> Some (subst,metasenv), cache
232 let auto_all_solutions universe cache context metasenv gl flags =
233 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
234 let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
235 let elems = [metasenv,[],goals] in
236 let bigbang = Unix.gettimeofday () in
237 let rec aux solutions cache elems flags =
238 match auto_main context flags elems cache universe with
239 | Fail s,cache ->prerr_endline s; solutions,cache
240 | Success (metasenv,subst,others), cache ->
241 let elapsed = Unix.gettimeofday () -. bigbang in
242 if elapsed > flags.timeout then
243 ((subst,metasenv)::solutions), cache
245 aux ((subst,metasenv)::solutions) cache others
246 {flags with timeout = flags.timeout -. elapsed}
248 aux [] cache elems flags