-let equational_case
- tables cache depth fake_proof goalno goalty subst context
- flags
-=
- let active,passive,bag = tables in
- let ppterm = ppterm context in
- let status = (fake_proof,goalno) in
- if flags.use_only_paramod then
- begin
- debug_print (lazy ("PARAMODULATION SU: " ^
- string_of_int goalno ^ " " ^ ppterm goalty ));
- let goal_steps, saturation_steps, timeout =
- max_int,max_int,flags.timeout
- in
- match
- Saturation.given_clause bag status active passive
- goal_steps saturation_steps timeout
- with
- | None, active, passive, bag ->
- [], (active,passive,bag), cache, flags
- | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
- passive,bag ->
- assert_subst_are_disjoint subst subst';
- let subst = subst@subst' in
- let open_goals =
- order_new_goals metasenv subst open_goals ppterm
- in
- let open_goals =
- List.map (fun (x,sort) -> x,depth-1,sort) open_goals
- in
- incr candidate_no;
- [(!candidate_no,proof),metasenv,subst,open_goals],
- (active,passive,bag), cache, flags
- end
- else
- begin
- debug_print (lazy ("NARROWING DEL GOAL: " ^
- string_of_int goalno ^ " " ^ ppterm goalty ));
- let goal_steps, saturation_steps, timeout =
- 1,0,flags.timeout
- in
- match
- Saturation.solve_narrowing bag status active passive goal_steps
- with
- | None, active, passive, bag ->
- [], (active,passive,bag), cache, flags
- | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
- passive,bag ->
- assert_subst_are_disjoint subst subst';
- let subst = subst@subst' in
- let open_goals =
- order_new_goals metasenv subst open_goals ppterm
- in
- let open_goals =
- List.map (fun (x,sort) -> x,depth-1,sort) open_goals
- in
- incr candidate_no;
- [(!candidate_no,proof),metasenv,subst,open_goals],
- (active,passive,bag), cache, flags
- end