+ find_matches metasenv context ugraph lift_amount term tl
+;;
+
+
+let rec find_all_matches ?(unif_fun=Inference.unification)
+ metasenv context ugraph lift_amount term =
+ let module C = Cic in
+ let module U = Utils in
+ let module S = CicSubstitution in
+ let module M = CicMetaSubst in
+ let module HL = HelmLibraryObjects in
+ let cmp = !Utils.compare_terms in
+ let names = Utils.names_of_context context in
+ function
+ | [] -> []
+ | candidate::tl ->
+ let pos, (proof, (ty, left, right, o), metas, args) = candidate in
+ let do_match c other eq_URI =
+ let subst', metasenv', ugraph' =
+ let t1 = Unix.gettimeofday () in
+ try
+ let r =
+ unif_fun (metasenv @ metas) context
+ term (S.lift lift_amount c) ugraph in
+ let t2 = Unix.gettimeofday () in
+ match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
+ r
+ with e ->
+ let t2 = Unix.gettimeofday () in
+ match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
+ raise e
+ in
+ (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
+ (candidate, eq_URI))
+ in
+ let c, other, eq_URI =
+ if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
+ else right, left, HL.Logic.eq_ind_r_URI
+ in
+ if o <> U.Incomparable then
+ try
+ let res = do_match c other eq_URI in
+ res::(find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term tl)
+ with e ->
+ find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term tl
+ else
+ try
+ let res = do_match c other eq_URI in
+ match res with
+ | _, s, _, _, _ ->
+ let c' = (* M. *)apply_subst s c
+ and other' = (* M. *)apply_subst s other in
+ let order = cmp c' other' in
+ let names = U.names_of_context context in
+ if order <> U.Lt && order <> U.Le then
+ res::(find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term tl)
+ else
+ find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term tl
+ with e ->
+ find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term tl
+;;
+
+
+let subsumption env table target =
+ let _, (ty, left, right, _), tmetas, _ = target in
+ let metasenv, context, ugraph = env in
+ let metasenv = metasenv @ tmetas in
+ let samesubst subst subst' =
+ let tbl = Hashtbl.create (List.length subst) in
+ List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
+ List.for_all
+ (fun (m, (c, t1, t2)) ->
+ try
+ let c', t1', t2' = Hashtbl.find tbl m in
+ if (c = c') && (t1 = t1') && (t2 = t2') then true
+ else false
+ with Not_found ->
+ true)
+ subst'
+ in
+ let leftr =
+ match left with
+ | Cic.Meta _ -> []
+ | _ ->
+ let leftc = get_candidates Matching table left in
+ find_all_matches ~unif_fun:Inference.matching
+ metasenv context ugraph 0 left leftc
+ in
+ let ok what (_, subst, menv, ug, ((pos, (_, (_, l, r, o), _, _)), _)) =
+ 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 context what other ugraph in
+ let t2 = Unix.gettimeofday () in
+ match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
+ r
+ with e ->
+ let t2 = Unix.gettimeofday () in
+ match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
+ raise e
+ in
+ samesubst subst subst'
+ with e ->
+ false
+ in
+ let r = List.exists (ok right) leftr in
+ if r then
+ true
+ else
+ let rightr =
+ match right with
+ | Cic.Meta _ -> []
+ | _ ->
+ let rightc = get_candidates Matching table right in
+ find_all_matches ~unif_fun:Inference.matching
+ metasenv context ugraph 0 right rightc
+ in
+ List.exists (ok left) rightr