(*
returns true if target is subsumed by some equality in table
*)
-let subsumption env table target =
+let subsumption env table target =
+ (*
+ let print_res l =
+ prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
+ ((pos,equation),_)) -> Inference.string_of_equality equation)l))
+ in
+ *)
let _, _, (ty, left, right, _), tmetas = target in
let metasenv, context, ugraph = env in
let metasenv = tmetas in
find_all_matches ~unif_fun:Inference.matching
metasenv context ugraph 0 left ty leftc
in
+(* print_res leftr;*)
let rec ok what = function
- | [] -> false, []
- | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m)), _))::tl ->
+ | [] -> None
+ | (_, subst, menv, ug, ((pos,equation),_))::tl ->
+ let _, _, (_, l, r, o), m = equation in
try
let other = if pos = Utils.Left then r else l in
let subst', menv', ug' =
let t1 = Unix.gettimeofday () in
try
let r =
- Inference.matching metasenv menv context what other ugraph
+ Inference.matching metasenv m context what other ugraph
in
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
in
(match merge_if_possible subst subst' with
| None -> ok what tl
- | Some s -> true, s)
+ | Some s -> Some (s, equation))
with Inference.MatchingFailure ->
ok what tl
in
- let r, subst = ok right leftr in
- let r, s =
- if r then
- true, subst
- else
+ match ok right leftr with
+ | Some _ as res -> res
+ | None ->
let rightr =
match right with
| Cic.Meta _ -> []
find_all_matches ~unif_fun:Inference.matching
metasenv context ugraph 0 right ty rightc
in
+(* print_res rightr;*)
ok left rightr
- in
(* (if r then *)
(* debug_print *)
(* (lazy *)
(* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
(* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
- r, s
;;
let rec demodulation_aux ?from ?(typecheck=false)
prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
prerr_endline ("+++++++++++++subst: " ^ (Inference.ppsubst subst));
+ prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
+ newmenv));
raise exc;
else ()
in