-(* 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',
- (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 =
+ 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