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, (proof, (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.;;
380 let rec demodulation newmeta env table target =
381 let module C = Cic in
382 let module S = CicSubstitution in
383 let module M = CicMetaSubst in
384 let module HL = HelmLibraryObjects in
385 let metasenv, context, ugraph = env in
386 let proof, (eq_ty, left, right, order), metas, args = target in
387 let metasenv' = metasenv @ metas in
388 let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
389 let time1 = Unix.gettimeofday () in
391 let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
392 let what, other = if pos = Utils.Left then what, other else other, what in
393 let newterm, newproof =
394 let bo = (* M. *)apply_subst subst (S.subst other t) in
396 C.Appl ([C.MutInd (HL.Logic.eq_URI, 0, []);
398 if is_left then [bo; S.lift 1 right] else [S.lift 1 left; bo])
400 let t' = C.Lambda (C.Anonymous, ty, bo'') in
402 Inference.ProofBlock (subst, eq_URI, t', eq_found, target)
403 (* (\* M. *\)apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
404 (* proof; other; proof']) *)
406 let left, right = if is_left then newterm, right else left, newterm in
408 (Inference.metas_of_term left) @ (Inference.metas_of_term right)
410 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
413 (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
416 let ordering = !Utils.compare_terms left right in
418 let time2 = Unix.gettimeofday () in
419 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
422 let w = Utils.compute_equality_weight eq_ty left right in
423 (w, (eq_ty, left, right, ordering), newmetasenv, newargs)
425 Inference.store_proof res newproof;
428 (* let build_newtarget = *)
429 (* let profile = CicUtil.profile "Indexing.demodulation.build_newtarget" in *)
430 (* (fun a b -> profile (build_newtarget a) b) *)
432 let res = demodulate_term metasenv' context ugraph table 0 left in
433 let build_identity (p, (t, l, r, o), m, a) =
435 | Utils.Gt -> (p, (t, r, r, Utils.Eq), m, a)
436 | _ -> (p, (t, l, l, Utils.Eq), m, a)
440 let newmeta, newtarget = build_newtarget true t in
441 if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
442 (Inference.meta_convertibility_eq target newtarget) then
445 (* if subsumption env table newtarget then *)
446 (* newmeta, build_identity newtarget *)
448 demodulation newmeta env table newtarget
450 let res = demodulate_term metasenv' context ugraph table 0 right in
453 let newmeta, newtarget = build_newtarget false 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
467 let rec betaexpand_term metasenv context ugraph table lift_amount term =
468 let module C = Cic in
469 let module S = CicSubstitution in
470 let module M = CicMetaSubst in
471 let module HL = HelmLibraryObjects in
472 let candidates = get_candidates Unification table term in
473 let res, lifted_term =
478 (fun arg (res, lifted_tl) ->
481 let arg_res, lifted_arg =
482 betaexpand_term metasenv context ugraph table
486 (fun (t, s, m, ug, eq_found) ->
487 (Some t)::lifted_tl, s, m, ug, eq_found)
492 (fun (l, s, m, ug, eq_found) ->
493 (Some lifted_arg)::l, s, m, ug, eq_found)
495 (Some lifted_arg)::lifted_tl)
498 (fun (r, s, m, ug, eq_found) ->
499 None::r, s, m, ug, eq_found) res,
505 (fun (l, s, m, ug, eq_found) ->
506 (C.Meta (i, l), s, m, ug, eq_found)) l'
508 e, C.Meta (i, lifted_l)
511 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
513 | C.Prod (nn, s, t) ->
515 betaexpand_term metasenv context ugraph table lift_amount s in
517 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
518 table (lift_amount+1) t in
521 (fun (t, s, m, ug, eq_found) ->
522 C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
525 (fun (t, s, m, ug, eq_found) ->
526 C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
527 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
532 (fun arg (res, lifted_tl) ->
533 let arg_res, lifted_arg =
534 betaexpand_term metasenv context ugraph table lift_amount arg
538 (fun (a, s, m, ug, eq_found) ->
539 a::lifted_tl, s, m, ug, eq_found)
544 (fun (r, s, m, ug, eq_found) ->
545 lifted_arg::r, s, m, ug, eq_found)
547 lifted_arg::lifted_tl)
551 (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
554 | t -> [], (S.lift lift_amount t)
557 | C.Meta _ -> res, lifted_term
560 find_all_matches metasenv context ugraph lift_amount term candidates
566 let superposition_left (metasenv, context, ugraph) table target =
567 let module C = Cic in
568 let module S = CicSubstitution in
569 let module M = CicMetaSubst in
570 let module HL = HelmLibraryObjects in
571 let module CR = CicReduction in
572 let module U = Utils in
573 let proof, (eq_ty, left, right, ordering), _, _ = target in
575 let term = if ordering = U.Gt then left else right in
576 betaexpand_term metasenv context ugraph table 0 term
578 let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
579 let time1 = Unix.gettimeofday () in
581 let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
582 let what, other = if pos = Utils.Left then what, other else other, what in
583 let newgoal, newproof =
584 let bo' = (* M. *)apply_subst s (S.subst other bo) in
587 [C.MutInd (HL.Logic.eq_URI, 0, []);
589 if ordering = U.Gt then [bo'; S.lift 1 right]
590 else [S.lift 1 left; bo'])
592 let t' = C.Lambda (C.Anonymous, ty, bo'') in
594 Inference.ProofBlock (s, eq_URI, t', eq_found, target)
595 (* (\* M. *\)apply_subst s *)
596 (* (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
597 (* proof; other; proof']) *)
600 if ordering = U.Gt then newgoal, right else left, newgoal in
601 let neworder = !Utils.compare_terms left right in
603 let time2 = Unix.gettimeofday () in
604 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
607 let w = Utils.compute_equality_weight eq_ty left right in
608 (w, (eq_ty, left, right, neworder), [], [])
610 Inference.store_proof res newproof;
613 (* let build_new = *)
614 (* let profile = CicUtil.profile "Inference.superposition_left.build_new" in *)
615 (* (fun e -> profile build_new e) *)
617 List.map build_new expansions
621 let superposition_right newmeta (metasenv, context, ugraph) table target =
622 let module C = Cic in
623 let module S = CicSubstitution in
624 let module M = CicMetaSubst in
625 let module HL = HelmLibraryObjects in
626 let module CR = CicReduction in
627 let module U = Utils in
628 let eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
629 let metasenv' = metasenv @ newmetas in
630 let maxmeta = ref newmeta in
633 | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
634 | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
638 (fun (_, subst, _, _, _) ->
639 let subst = (* M. *)apply_subst subst in
640 let o = !Utils.compare_terms (subst l) (subst r) in
641 o <> U.Lt && o <> U.Le)
642 (fst (betaexpand_term metasenv' context ugraph table 0 l))
644 (res left right), (res right left)
646 let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
648 let time1 = Unix.gettimeofday () in
650 let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
651 let what, other = if pos = Utils.Left then what, other else other, what in
652 let newgoal, newproof =
653 let bo' = (* M. *)apply_subst s (S.subst other bo) in
656 [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
657 if ordering = U.Gt then [bo'; S.lift 1 right]
658 else [S.lift 1 left; bo'])
660 let t' = C.Lambda (C.Anonymous, ty, bo'') in
662 Inference.ProofBlock (s, eq_URI, t', eq_found, target)
663 (* (\* M. *\)apply_subst s *)
664 (* (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
665 (* eqproof; other; proof']) *)
667 let newmeta, newequality =
669 if ordering = U.Gt then newgoal, (* M. *)apply_subst s right
670 else (* M. *)apply_subst s left, newgoal in
671 let neworder = !Utils.compare_terms left right
672 and newmenv = newmetas @ menv'
673 and newargs = args @ args' in
675 let w = Utils.compute_equality_weight eq_ty left right in
676 (w, (eq_ty, left, right, neworder), newmenv, newargs)
677 and env = (metasenv, context, ugraph) in
678 let newm, eq' = Inference.fix_metas !maxmeta eq' in
683 let time2 = Unix.gettimeofday () in
684 build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
686 Inference.store_proof newequality newproof;
690 (* let build_new = *)
691 (* let profile = CicUtil.profile "Indexing.superposition_right.build_new" in *)
692 (* (fun o e -> profile (build_new o) e) *)
695 let new1 = List.map (build_new U.Gt) res1
696 and new2 = List.map (build_new U.Lt) res2 in
698 | _, (_, left, right, _), _, _ ->
699 not (fst (CR.are_convertible context left right ugraph))
702 (List.filter ok (new1 @ new2)))