-(* let names = U.names_of_context context in *)
-(* Printf.printf "MATCH FOUND: %s, %s\n" *)
-(* (CicPp.pp term names) (CicPp.pp (S.lift lift_amount c) names); *)
- Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
- (candidate, eq_URI))
-(* (proof, ty, c, other, eq_URI)) *)
- in
- let c, other, eq_URI =
- if pos = 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
-(* print_endline "SONO QUI!"; *)
- let res = do_match c other eq_URI in
-(* print_endline "RITORNO RES"; *)
- res
- with e ->
-(* Printf.printf "ERRORE!: %s\n" (Printexc.to_string e); *)
- find_matches unif_fun metasenv context ugraph lift_amount term tl
- else
- let res = try do_match c other eq_URI with e -> None in
- match res with
- | Some (_, 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
-(* Printf.printf "c': %s\nother': %s\norder: %s\n\n" *)
-(* (CicPp.pp c' names) (CicPp.pp other' names) *)
-(* (U.string_of_comparison order); *)
-(* if cmp (M.apply_subst s c) (M.apply_subst s other) = U.Gt then *)
- if order = U.Gt then
- res
- else
- find_matches unif_fun metasenv context ugraph
+ 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
+ do_match c other eq_URI
+ with Inference.MatchingFailure ->
+ find_matches metasenv context ugraph lift_amount term tl
+ else
+ let res =
+ try do_match c other eq_URI
+ with Inference.MatchingFailure -> None
+ in
+ match res with
+ | Some (_, 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.Gt then
+ res
+ else
+ find_matches metasenv context ugraph lift_amount term tl
+ | None ->
+ 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
+ let termty, ugraph =
+ CicTypeChecker.type_of_aux' metasenv context term ugraph
+ in
+ function
+ | [] -> []
+ | candidate::tl ->
+ let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
+ if not (fst (CicReduction.are_convertible
+ ~metasenv context termty ty ugraph)) then (
+ debug_print (
+ Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found"
+ (CicPp.pp termty names) (CicPp.pp ty names));
+ find_all_matches ~unif_fun metasenv context ugraph
+ lift_amount term tl
+ ) else
+ 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
+ | Inference.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ as 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
+ | Inference.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ 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
+ | Inference.MatchingFailure
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ find_all_matches ~unif_fun metasenv context ugraph