2 type retrieval_mode = Matching | Unification;;
5 let print_candidates mode term res =
9 Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
11 Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
17 Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
18 (Inference.string_of_equality e))
24 let indexing_retrieval_time = ref 0.;;
27 (* let my_apply_subst subst term = *)
28 (* let module C = Cic in *)
29 (* let lookup lift_amount meta = *)
31 (* | C.Meta (i, _) -> ( *)
33 (* let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in *)
34 (* (\* CicSubstitution.lift lift_amount *\)t *)
35 (* with Not_found -> meta *)
37 (* | _ -> assert false *)
39 (* let rec apply_aux lift_amount = function *)
40 (* | C.Meta (i, l) as t -> lookup lift_amount t *)
41 (* | C.Appl l -> C.Appl (List.map (apply_aux lift_amount) l) *)
42 (* | C.Prod (nn, s, t) -> *)
43 (* C.Prod (nn, apply_aux lift_amount s, apply_aux (lift_amount+1) t) *)
44 (* | C.Lambda (nn, s, t) -> *)
45 (* C.Lambda (nn, apply_aux lift_amount s, apply_aux (lift_amount+1) t) *)
48 (* apply_aux 0 term *)
52 (* let apply_subst subst term = *)
53 (* Printf.printf "| apply_subst:\n| subst: %s\n| term: %s\n" *)
54 (* (Utils.print_subst ~prefix:" ; " subst) (CicPp.ppterm term); *)
55 (* let res = my_apply_subst subst term in *)
56 (* (\* let res = CicMetaSubst.apply_subst subst term in *\) *)
57 (* Printf.printf "| res: %s\n" (CicPp.ppterm res); *)
58 (* print_endline "|"; *)
62 (* let apply_subst = my_apply_subst *)
63 let apply_subst = CicMetaSubst.apply_subst
67 let profile = CicUtil.profile "apply_subst" in
68 (fun s a -> profile (apply_subst s) a)
74 Path_indexing.PSTrie.empty
77 let index = Path_indexing.index
78 and remove_index = Path_indexing.remove_index
79 and in_index = Path_indexing.in_index;;
81 let get_candidates mode trie term =
82 let t1 = Unix.gettimeofday () in
86 | Matching -> Path_indexing.retrieve_generalizations trie term
87 | Unification -> Path_indexing.retrieve_unifiables trie term
88 (* Path_indexing.retrieve_all trie term *)
90 Path_indexing.PosEqSet.elements s
92 (* print_candidates mode term res; *)
93 let t2 = Unix.gettimeofday () in
94 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
101 Discrimination_tree.DiscriminationTree.empty
104 let index = Discrimination_tree.index
105 and remove_index = Discrimination_tree.remove_index
106 and in_index = Discrimination_tree.in_index;;
108 let get_candidates mode tree term =
109 let t1 = Unix.gettimeofday () in
113 | Matching -> Discrimination_tree.retrieve_generalizations tree term
114 | Unification -> Discrimination_tree.retrieve_unifiables tree term
116 Discrimination_tree.PosEqSet.elements s
118 (* print_candidates mode term res; *)
119 let t2 = Unix.gettimeofday () in
120 indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
125 (* let get_candidates = *)
126 (* let profile = CicUtil.profile "Indexing.get_candidates" in *)
127 (* (fun mode tree term -> profile (get_candidates mode tree) term) *)
131 let match_unif_time_ok = ref 0.;;
132 let match_unif_time_no = ref 0.;;
135 let rec find_matches metasenv context ugraph lift_amount term =
136 let module C = Cic in
137 let module U = Utils in
138 let module S = CicSubstitution in
139 let module M = CicMetaSubst in
140 let module HL = HelmLibraryObjects in
141 let cmp = !Utils.compare_terms in
142 let names = Utils.names_of_context context in
146 let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
147 let do_match c other eq_URI =
148 let subst', metasenv', ugraph' =
149 let t1 = Unix.gettimeofday () in
152 Inference.matching (metasenv @ metas) context
153 term (S.lift lift_amount c) ugraph in
154 let t2 = Unix.gettimeofday () in
155 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
158 let t2 = Unix.gettimeofday () in
159 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
162 Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
165 let c, other, eq_URI =
166 if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
167 else right, left, HL.Logic.eq_ind_r_URI
169 if o <> U.Incomparable then
171 do_match c other eq_URI
173 find_matches metasenv context ugraph lift_amount term tl
175 let res = try do_match c other eq_URI with e -> None in
177 | Some (_, s, _, _, _) ->
178 let c' = (* M. *)apply_subst s c
179 and other' = (* M. *)apply_subst s other in
180 let order = cmp c' other' in
181 let names = U.names_of_context context in
185 find_matches metasenv context ugraph lift_amount term tl
187 find_matches metasenv context ugraph lift_amount term tl
191 let rec find_all_matches ?(unif_fun=Inference.unification)
192 metasenv context ugraph lift_amount term =
193 let module C = Cic in
194 let module U = Utils in
195 let module S = CicSubstitution in
196 let module M = CicMetaSubst in
197 let module HL = HelmLibraryObjects in
198 let cmp = !Utils.compare_terms in
199 let names = Utils.names_of_context context in
203 let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
204 let do_match c other eq_URI =
205 let subst', metasenv', ugraph' =
206 let t1 = Unix.gettimeofday () in
209 unif_fun (metasenv @ metas) context
210 term (S.lift lift_amount c) ugraph in
211 let t2 = Unix.gettimeofday () in
212 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
215 let t2 = Unix.gettimeofday () in
216 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
219 (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
222 let c, other, eq_URI =
223 if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
224 else right, left, HL.Logic.eq_ind_r_URI
226 if o <> U.Incomparable then
228 let res = do_match c other eq_URI in
229 res::(find_all_matches ~unif_fun metasenv context ugraph
232 find_all_matches ~unif_fun metasenv context ugraph
236 let res = do_match c other eq_URI in
239 let c' = (* M. *)apply_subst s c
240 and other' = (* M. *)apply_subst s other in
241 let order = cmp c' other' in
242 let names = U.names_of_context context in
243 if order <> U.Lt && order <> U.Le then
244 res::(find_all_matches ~unif_fun metasenv context ugraph
247 find_all_matches ~unif_fun metasenv context ugraph
250 find_all_matches ~unif_fun metasenv context ugraph
255 let subsumption env table target =
256 let _, (ty, left, right, _), tmetas, _ = target in
257 let metasenv, context, ugraph = env in
258 let metasenv = metasenv @ tmetas in
259 let samesubst subst subst' =
260 let tbl = Hashtbl.create (List.length subst) in
261 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
263 (fun (m, (c, t1, t2)) ->
265 let c', t1', t2' = Hashtbl.find tbl m in
266 if (c = c') && (t1 = t1') && (t2 = t2') then true
276 let leftc = get_candidates Matching table left in
277 find_all_matches ~unif_fun:Inference.matching
278 metasenv context ugraph 0 left leftc
280 let ok what (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _)) =
282 let other = if pos = Utils.Left then r else l in
283 let subst', menv', ug' =
284 let t1 = Unix.gettimeofday () in
287 Inference.matching metasenv context what other ugraph in
288 let t2 = Unix.gettimeofday () in
289 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
292 let t2 = Unix.gettimeofday () in
293 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
296 samesubst subst subst'
300 let r = List.exists (ok right) leftr in
308 let rightc = get_candidates Matching table right in
309 find_all_matches ~unif_fun:Inference.matching
310 metasenv context ugraph 0 right rightc
312 List.exists (ok left) rightr
316 let rec demodulate_term metasenv context ugraph table lift_amount term =
317 let module C = Cic in
318 let module S = CicSubstitution in
319 let module M = CicMetaSubst in
320 let module HL = HelmLibraryObjects in
321 let candidates = get_candidates Matching table term in
326 find_matches metasenv context ugraph lift_amount term candidates
337 (res, tl @ [S.lift 1 t])
340 demodulate_term metasenv context ugraph table
344 | None -> (None, tl @ [S.lift 1 t])
345 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
350 | Some (_, subst, menv, ug, eq_found) ->
351 Some (C.Appl ll, subst, menv, ug, eq_found)
353 | C.Prod (nn, s, t) ->
355 demodulate_term metasenv context ugraph table lift_amount s in (
359 demodulate_term metasenv
360 ((Some (nn, C.Decl s))::context) ugraph
361 table (lift_amount+1) t
365 | Some (t', subst, menv, ug, eq_found) ->
366 Some (C.Prod (nn, (S.lift 1 s), t'),
367 subst, menv, ug, eq_found)
369 | Some (s', subst, menv, ug, eq_found) ->
370 Some (C.Prod (nn, s', (S.lift 1 t)),
371 subst, menv, ug, eq_found)
378 let build_newtarget_time = ref 0.;;
381 let demod_counter = ref 1;;
383 let rec demodulation newmeta env table target =
384 let module C = Cic in
385 let module S = CicSubstitution in
386 let module M = CicMetaSubst in
387 let module HL = HelmLibraryObjects in
388 let metasenv, context, ugraph = env in
389 let _, proof, (eq_ty, left, right, order), metas, args = target in
390 let metasenv' = metasenv @ metas in
391 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
392 let time1 = Unix.gettimeofday () in
394 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
395 let what, other = if pos = Utils.Left then what, other else other, what in
396 let newterm, newproof =
397 let bo = (* M. *)apply_subst subst (S.subst other t) in
399 let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
401 let l, r = if is_left then bo, right else left, bo in
402 (name, ty, eq_ty, l, r)
405 (* C.Appl ([C.MutInd (HL.Logic.eq_URI, 0, []); *)
406 (* S.lift 1 eq_ty] @ *)
407 (* if is_left then [S.lift 1 bo; S.lift 1 right] *)
408 (* else [S.lift 1 left; S.lift 1 bo]) *)
411 (* let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in *)
412 (* incr demod_counter; *)
413 (* C.Lambda (name, ty, bo'') *)
416 Inference.ProofBlock (subst, eq_URI, t', eq_found, target)
417 (* (\* M. *\)apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
418 (* proof; other; proof']) *)
420 let left, right = if is_left then newterm, right else left, newterm in
422 (Inference.metas_of_term left) @ (Inference.metas_of_term right)
424 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
427 (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
430 let ordering = !Utils.compare_terms left right in
432 let time2 = Unix.gettimeofday () in
433 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
436 let w = Utils.compute_equality_weight eq_ty left right in
437 (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
441 (* let build_newtarget = *)
442 (* let profile = CicUtil.profile "Indexing.demodulation.build_newtarget" in *)
443 (* (fun a b -> profile (build_newtarget a) b) *)
445 let res = demodulate_term metasenv' context ugraph table 0 left in
446 (* let build_identity (w, p, (t, l, r, o), m, a) = *)
448 (* | Utils.Gt -> (w, p, (t, r, r, Utils.Eq), m, a) *)
449 (* | _ -> (w, p, (t, l, l, Utils.Eq), m, a) *)
453 let newmeta, newtarget = build_newtarget true t in
454 if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
455 (Inference.meta_convertibility_eq target newtarget) then
458 (* if subsumption env table newtarget then *)
459 (* newmeta, build_identity newtarget *)
461 demodulation newmeta env table newtarget
463 let res = demodulate_term metasenv' context ugraph table 0 right in
466 let newmeta, newtarget = build_newtarget false t in
467 if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
468 (Inference.meta_convertibility_eq target newtarget) then
471 (* if subsumption env table newtarget then *)
472 (* newmeta, build_identity newtarget *)
474 demodulation newmeta env table newtarget
480 let rec betaexpand_term metasenv context ugraph table lift_amount term =
481 let module C = Cic in
482 let module S = CicSubstitution in
483 let module M = CicMetaSubst in
484 let module HL = HelmLibraryObjects in
485 let candidates = get_candidates Unification table term in
486 let res, lifted_term =
491 (fun arg (res, lifted_tl) ->
494 let arg_res, lifted_arg =
495 betaexpand_term metasenv context ugraph table
499 (fun (t, s, m, ug, eq_found) ->
500 (Some t)::lifted_tl, s, m, ug, eq_found)
505 (fun (l, s, m, ug, eq_found) ->
506 (Some lifted_arg)::l, s, m, ug, eq_found)
508 (Some lifted_arg)::lifted_tl)
511 (fun (r, s, m, ug, eq_found) ->
512 None::r, s, m, ug, eq_found) res,
518 (fun (l, s, m, ug, eq_found) ->
519 (C.Meta (i, l), s, m, ug, eq_found)) l'
521 e, C.Meta (i, lifted_l)
524 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
526 | C.Prod (nn, s, t) ->
528 betaexpand_term metasenv context ugraph table lift_amount s in
530 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
531 table (lift_amount+1) t in
534 (fun (t, s, m, ug, eq_found) ->
535 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
538 (fun (t, s, m, ug, eq_found) ->
539 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
540 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
545 (fun arg (res, lifted_tl) ->
546 let arg_res, lifted_arg =
547 betaexpand_term metasenv context ugraph table lift_amount arg
551 (fun (a, s, m, ug, eq_found) ->
552 a::lifted_tl, s, m, ug, eq_found)
557 (fun (r, s, m, ug, eq_found) ->
558 lifted_arg::r, s, m, ug, eq_found)
560 lifted_arg::lifted_tl)
564 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
567 | t -> [], (S.lift lift_amount t)
570 | C.Meta _ -> res, lifted_term
573 find_all_matches metasenv context ugraph lift_amount term candidates
579 let sup_l_counter = ref 1;;
581 let superposition_left (metasenv, context, ugraph) table target =
582 let module C = Cic in
583 let module S = CicSubstitution in
584 let module M = CicMetaSubst in
585 let module HL = HelmLibraryObjects in
586 let module CR = CicReduction in
587 let module U = Utils in
588 let _, proof, (eq_ty, left, right, ordering), _, _ = target in
590 let term = if ordering = U.Gt then left else right in
591 betaexpand_term metasenv context ugraph table 0 term
593 let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
594 let time1 = Unix.gettimeofday () in
596 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
597 let what, other = if pos = Utils.Left then what, other else other, what in
598 let newgoal, newproof =
599 let bo' = (* M. *)apply_subst s (S.subst other bo) in
601 let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
603 let l, r = if ordering = U.Gt then bo', right else left, bo' in
604 (name, ty, eq_ty, l, r)
608 (* [C.MutInd (HL.Logic.eq_URI, 0, []); *)
609 (* S.lift 1 eq_ty] @ *)
610 (* if ordering = U.Gt then [S.lift 1 bo'; S.lift 1 right] *)
611 (* else [S.lift 1 left; S.lift 1 bo']) *)
614 (* let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in *)
615 (* incr sup_l_counter; *)
616 (* C.Lambda (name, ty, bo'') *)
619 Inference.ProofBlock (s, eq_URI, t', eq_found, target)
620 (* (\* M. *\)apply_subst s *)
621 (* (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
622 (* proof; other; proof']) *)
625 if ordering = U.Gt then newgoal, right else left, newgoal in
626 let neworder = !Utils.compare_terms left right in
628 let time2 = Unix.gettimeofday () in
629 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
632 let w = Utils.compute_equality_weight eq_ty left right in
633 (w, newproof, (eq_ty, left, right, neworder), [], [])
637 (* let build_new = *)
638 (* let profile = CicUtil.profile "Inference.superposition_left.build_new" in *)
639 (* (fun e -> profile build_new e) *)
641 List.map build_new expansions
645 let sup_r_counter = ref 1;;
647 let superposition_right newmeta (metasenv, context, ugraph) table target =
648 let module C = Cic in
649 let module S = CicSubstitution in
650 let module M = CicMetaSubst in
651 let module HL = HelmLibraryObjects in
652 let module CR = CicReduction in
653 let module U = Utils in
654 let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
655 let metasenv' = metasenv @ newmetas in
656 let maxmeta = ref newmeta in
659 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
660 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
664 (fun (_, subst, _, _, _) ->
665 let subst = (* M. *)apply_subst subst in
666 let o = !Utils.compare_terms (subst l) (subst r) in
667 o <> U.Lt && o <> U.Le)
668 (fst (betaexpand_term metasenv' context ugraph table 0 l))
670 (res left right), (res right left)
672 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
674 let time1 = Unix.gettimeofday () in
676 let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
677 let what, other = if pos = Utils.Left then what, other else other, what in
678 let newgoal, newproof =
679 let bo' = (* M. *)apply_subst s (S.subst other bo) in
681 let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
683 let l, r = if ordering = U.Gt then bo', right else left, bo' in
684 (name, ty, eq_ty, l, r)
688 (* [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @ *)
689 (* if ordering = U.Gt then [S.lift 1 bo'; S.lift 1 right] *)
690 (* else [S.lift 1 left; S.lift 1 bo']) *)
693 (* let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in *)
694 (* incr sup_r_counter; *)
695 (* C.Lambda (name, ty, bo'') *)
698 Inference.ProofBlock (s, eq_URI, t', eq_found, target)
699 (* (\* M. *\)apply_subst s *)
700 (* (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
701 (* eqproof; other; proof']) *)
703 let newmeta, newequality =
705 if ordering = U.Gt then newgoal, (* M. *)apply_subst s right
706 else (* M. *)apply_subst s left, newgoal in
707 let neworder = !Utils.compare_terms left right
708 and newmenv = newmetas @ menv'
709 and newargs = args @ args' in
711 let w = Utils.compute_equality_weight eq_ty left right in
712 (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
713 and env = (metasenv, context, ugraph) in
714 let newm, eq' = Inference.fix_metas !maxmeta eq' in
719 let time2 = Unix.gettimeofday () in
720 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
725 (* let build_new = *)
726 (* let profile = CicUtil.profile "Indexing.superposition_right.build_new" in *)
727 (* (fun o e -> profile (build_new o) e) *)
730 let new1 = List.map (build_new U.Gt) res1
731 and new2 = List.map (build_new U.Lt) res2 in
733 | _, _, (_, left, right, _), _, _ ->
734 not (fst (CR.are_convertible context left right ugraph))
737 (List.filter ok (new1 @ new2)))