+let debug_print = Utils.debug_print;;
+
+
type retrieval_mode = Matching | Unification;;
Discrimination_tree.PosEqSet.elements s
in
(* print_candidates mode term res; *)
+(* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
+(* print_newline (); *)
let t2 = Unix.gettimeofday () in
indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
res
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
| [] -> None
| 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 =
- Inference.matching (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
+ 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_matches 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 =
+ Inference.matching (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 as e ->
+ let t2 = Unix.gettimeofday () in
+ match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
+ raise e
+ in
Some (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
- do_match c other eq_URI
- with e ->
- find_matches 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
- if order = U.Gt then
- res
- else
- find_matches metasenv context ugraph lift_amount term tl
- | None ->
+ 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
+ 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 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
- 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
+ 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
- (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 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
+ lift_amount term tl
;;
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
r
- with e ->
+ with Inference.MatchingFailure as e ->
let t2 = Unix.gettimeofday () in
match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
raise e
in
samesubst subst subst'
- with e ->
+ with Inference.MatchingFailure ->
false
in
let r = List.exists (ok right) leftr in
projects / helm.git / blobdiff