- let rec aux steps next visited goal =
- if steps = 0 then visited, None else
- let goalproof,menv,_,_,left,right = open_goal goal in
- if (List.mem (left,right,next) visited || List.mem (right,left,next) visited)
- then visited, None else
- let do_step t =
- demodulation_all_aux menv context ugraph table 0 t
+ (pr@pl@proof, m, Cic.Appl [eq;ty;l;r])
+;;
+
+let demodulation_all_goal bag env table goal maxnf =
+ let proof,menv,eq,ty,left,right = open_goal goal in
+ let v1, bag, l_demod = demod_all maxnf bag env table ([],menv,left) in
+ let v2, bag, r_demod = demod_all maxnf bag env table ([],menv,right) in
+ let l_demod = if l_demod = [] then [ [], menv, left ] else l_demod in
+ let r_demod = if r_demod = [] then [ [], menv, right ] else r_demod in
+ List.fold_left
+ (fun acc (_,_,l as ld) ->
+ List.fold_left
+ (fun acc (_,_,r as rd) ->
+ combine_demodulation_proofs bag env goal ld rd :: acc)
+ acc r_demod)
+ [] l_demod
+;;
+
+let solve_demodulating bag env table initgoal steps =
+ let proof,menv,eq,ty,left,right = open_goal initgoal in
+ let uri =
+ match eq with
+ | Cic.MutInd (u,_,_) -> u
+ | _ -> assert false
+ in
+ let _, context, ugraph = env in
+ let v1, bag, l_demod = demod_all steps bag env table ([],menv,left) in
+ let v2, bag, r_demod = demod_all steps bag env table ([],menv,right) in
+ let is_solved left right ml mr =
+ let m = ml @ (List.filter
+ (fun (x,_,_) -> not (List.exists (fun (y,_,_) -> x=y)ml)) mr)