113 |
113 |
114 (*The empty list here indicates that the constant is being ignored*) |
114 (*The empty list here indicates that the constant is being ignored*) |
115 fun add_standard_const (s,tab) = Symtab.update (s,[]) tab; |
115 fun add_standard_const (s,tab) = Symtab.update (s,[]) tab; |
116 |
116 |
117 val null_const_tab : const_typ list list Symtab.table = |
117 val null_const_tab : const_typ list list Symtab.table = |
118 foldl add_standard_const Symtab.empty standard_consts; |
118 List.foldl add_standard_const Symtab.empty standard_consts; |
119 |
119 |
120 fun get_goal_consts_typs thy = foldl (add_term_consts_typs_rm thy) null_const_tab; |
120 fun get_goal_consts_typs thy = List.foldl (add_term_consts_typs_rm thy) null_const_tab; |
121 |
121 |
122 (*Inserts a dummy "constant" referring to the theory name, so that relevance |
122 (*Inserts a dummy "constant" referring to the theory name, so that relevance |
123 takes the given theory into account.*) |
123 takes the given theory into account.*) |
124 fun const_prop_of theory_const th = |
124 fun const_prop_of theory_const th = |
125 if theory_const then |
125 if theory_const then |
188 in |
188 in |
189 rel_weight / (rel_weight + real (length consts_typs - length rel)) |
189 rel_weight / (rel_weight + real (length consts_typs - length rel)) |
190 end; |
190 end; |
191 |
191 |
192 (*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*) |
192 (*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*) |
193 fun add_expand_pairs (x,ys) xys = foldl (fn (y,acc) => (x,y)::acc) xys ys; |
193 fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys; |
194 |
194 |
195 fun consts_typs_of_term thy t = |
195 fun consts_typs_of_term thy t = |
196 let val tab = add_term_consts_typs_rm thy (t, null_const_tab) |
196 let val tab = add_term_consts_typs_rm thy (t, null_const_tab) |
197 in Symtab.fold add_expand_pairs tab [] end; |
197 in Symtab.fold add_expand_pairs tab [] end; |
198 |
198 |
248 fun relevant_clauses max_new thy ctab p rel_consts = |
248 fun relevant_clauses max_new thy ctab p rel_consts = |
249 let fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*) |
249 let fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*) |
250 | relevant (newpairs,rejects) [] = |
250 | relevant (newpairs,rejects) [] = |
251 let val (newrels,more_rejects) = take_best max_new newpairs |
251 let val (newrels,more_rejects) = take_best max_new newpairs |
252 val new_consts = List.concat (map #2 newrels) |
252 val new_consts = List.concat (map #2 newrels) |
253 val rel_consts' = foldl add_const_typ_table rel_consts new_consts |
253 val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts |
254 val newp = p + (1.0-p) / convergence |
254 val newp = p + (1.0-p) / convergence |
255 in |
255 in |
256 Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels))); |
256 Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels))); |
257 (map #1 newrels) @ |
257 (map #1 newrels) @ |
258 (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects)) |
258 (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects)) |
374 fun multi_name a (th, (n,pairs)) = |
374 fun multi_name a (th, (n,pairs)) = |
375 (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs) |
375 (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs) |
376 |
376 |
377 fun add_single_names ((a, []), pairs) = pairs |
377 fun add_single_names ((a, []), pairs) = pairs |
378 | add_single_names ((a, [th]), pairs) = (a,th)::pairs |
378 | add_single_names ((a, [th]), pairs) = (a,th)::pairs |
379 | add_single_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths); |
379 | add_single_names ((a, ths), pairs) = #2 (List.foldl (multi_name a) (1,pairs) ths); |
380 |
380 |
381 (*Ignore blacklisted basenames*) |
381 (*Ignore blacklisted basenames*) |
382 fun add_multi_names ((a, ths), pairs) = |
382 fun add_multi_names ((a, ths), pairs) = |
383 if (Sign.base_name a) mem_string ResAxioms.multi_base_blacklist then pairs |
383 if (Sign.base_name a) mem_string ResAxioms.multi_base_blacklist then pairs |
384 else add_single_names ((a, ths), pairs); |
384 else add_single_names ((a, ths), pairs); |
391 val ht = mk_clause_table 900 (*ht for blacklisted theorems*) |
391 val ht = mk_clause_table 900 (*ht for blacklisted theorems*) |
392 fun blacklisted x = run_blacklist_filter andalso isSome (Polyhash.peek ht x) |
392 fun blacklisted x = run_blacklist_filter andalso isSome (Polyhash.peek ht x) |
393 in |
393 in |
394 app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt); |
394 app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt); |
395 filter (not o blacklisted o #2) |
395 filter (not o blacklisted o #2) |
396 (foldl add_single_names (foldl add_multi_names [] mults) singles) |
396 (List.foldl add_single_names (List.foldl add_multi_names [] mults) singles) |
397 end; |
397 end; |
398 |
398 |
399 fun check_named ("",th) = (warning ("No name for theorem " ^ Display.string_of_thm th); false) |
399 fun check_named ("",th) = (warning ("No name for theorem " ^ Display.string_of_thm th); false) |
400 | check_named (_,th) = true; |
400 | check_named (_,th) = true; |
401 |
401 |
429 |
429 |
430 (***************************************************************) |
430 (***************************************************************) |
431 (* Type Classes Present in the Axiom or Conjecture Clauses *) |
431 (* Type Classes Present in the Axiom or Conjecture Clauses *) |
432 (***************************************************************) |
432 (***************************************************************) |
433 |
433 |
434 fun add_classes (sorts, cset) = foldl setinsert cset (List.concat sorts); |
434 fun add_classes (sorts, cset) = List.foldl setinsert cset (List.concat sorts); |
435 |
435 |
436 (*Remove this trivial type class*) |
436 (*Remove this trivial type class*) |
437 fun delete_type cset = Symtab.delete_safe "HOL.type" cset; |
437 fun delete_type cset = Symtab.delete_safe "HOL.type" cset; |
438 |
438 |
439 fun tvar_classes_of_terms ts = |
439 fun tvar_classes_of_terms ts = |
440 let val sorts_list = map (map #2 o OldTerm.term_tvars) ts |
440 let val sorts_list = map (map #2 o OldTerm.term_tvars) ts |
441 in Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list)) end; |
441 in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; |
442 |
442 |
443 fun tfree_classes_of_terms ts = |
443 fun tfree_classes_of_terms ts = |
444 let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts |
444 let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts |
445 in Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list)) end; |
445 in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; |
446 |
446 |
447 (*fold type constructors*) |
447 (*fold type constructors*) |
448 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) |
448 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) |
449 | fold_type_consts f T x = x; |
449 | fold_type_consts f T x = x; |
450 |
450 |