equal
deleted
inserted
replaced
61 fun clear_grounds grounds = Symtab.map (K (K [])) grounds |
61 fun clear_grounds grounds = Symtab.map (K (K [])) grounds |
62 |
62 |
63 |
63 |
64 (* configuration options *) |
64 (* configuration options *) |
65 |
65 |
66 val max_rounds = Attrib.setup_config_int @{binding monomorph_max_rounds} (K 5) |
66 val max_rounds = Attrib.setup_config_int \<^binding>\<open>monomorph_max_rounds\<close> (K 5) |
67 |
67 |
68 val max_new_instances = |
68 val max_new_instances = |
69 Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 500) |
69 Attrib.setup_config_int \<^binding>\<open>monomorph_max_new_instances\<close> (K 500) |
70 |
70 |
71 val max_thm_instances = |
71 val max_thm_instances = |
72 Attrib.setup_config_int @{binding monomorph_max_thm_instances} (K 20) |
72 Attrib.setup_config_int \<^binding>\<open>monomorph_max_thm_instances\<close> (K 20) |
73 |
73 |
74 val max_new_const_instances_per_round = |
74 val max_new_const_instances_per_round = |
75 Attrib.setup_config_int @{binding monomorph_max_new_const_instances_per_round} (K 5) |
75 Attrib.setup_config_int \<^binding>\<open>monomorph_max_new_const_instances_per_round\<close> (K 5) |
76 |
76 |
77 fun limit_rounds ctxt f = |
77 fun limit_rounds ctxt f = |
78 let |
78 let |
79 val max = Config.get ctxt max_rounds |
79 val max = Config.get ctxt max_rounds |
80 fun round i x = if i > max then x else round (i + 1) (f ctxt i x) |
80 fun round i x = if i > max then x else round (i + 1) (f ctxt i x) |