Lines Matching refs:depth
89 val depth = ref false;; (* Use depth not inference bound. *)
413 insts=insts' andalso (size <= size' orelse !depth))
520 fun exp_goal depth (state as ((g,_),(insts,offset,size))) cont =
521 if depth < 0 then failwith "expand_goal: too deep"
525 exp_goals (depth-1) newstate
539 exp_goals depth (gl, tup as (insts,offset,size)) cont =
542 | [g] => exp_goal depth (g,tup) (fn (g',stup) => cont([g'],stup))
549 exp_goals depth (lgoals,(insts,offset,lsize))
551 exp_goals depth (rgoals,(i,off,n + rsize))
554 exp_goals depth (rgoals,(insts,offset,lsize))
556 exp_goals depth (lgoals,(i,off,n + rsize))
563 exp_goal depth (g,tup)
565 exp_goals depth (gs,stup)
582 (* With iterative deepening of inferences or depth. *)
949 if !depth then dcutin := 100001 else ();
955 solve_goal infs rules (!depth) min max inc (1,[])