Lines Matching refs:depth
1201 | meson depth res
1204 else meson depth (f :: res) others
1205 | meson depth res
1211 trace "meson: (depth, state, length others)"
1212 (fn () => printVal ((depth, state, length others)))
1215 val _ = assert (depth > 0) (CUT "hit bottom")
1227 prune_subfacts_wrt (snd lit) (meson (depth - 1) [] subgoals)
1242 meson depth res (newgoals @ others)
1244 handle CUT _ => meson depth res others
1246 fn depth => fn f => meson depth [] [([], (empty_subst, f))]
1251 fun meson_refute_reduce_depth_fact reduce depth =
1255 meson_frule_reduce_depth reduce depth
1270 fun meson_refute_reduce_depth db reduce depth =
1272 val _ = trace "meson_refute_reduce_depth: depth" (fn () => printVal depth)
1274 val f = meson_refute_reduce_depth_fact reduce depth
1291 fun deepen 0 depth =
1292 raise ERR "meson_refute_deepen" "no solutions up to max depth"
1293 | deepen n depth = (refute orelsef (deepen (n - 1) o plus step)) depth
1310 fun meson_prove_reduce_depth db reduce depth (vars, goal) =
1321 meson_frule_reduce_depth reduce depth