4 exception NotMetaConvertible;;
6 let meta_convertibility_aux table t1 t2 =
8 let rec aux table t1 t2 =
10 | t1, t2 when t1 = t2 -> table
11 | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
12 let m1_binding, m2_binding, table =
14 try List.assoc m1 table, table
15 with Not_found -> m2, (m1, m2)::table
18 try List.assoc m2 table, table
19 with Not_found -> m1, (m2, m1)::table
23 if m1_binding <> m2 || m2_binding <> m1 then
24 raise NotMetaConvertible
30 | None, Some _ | Some _, None -> raise NotMetaConvertible
32 | Some t1, Some t2 -> (aux res t1 t2))
34 with Invalid_argument _ ->
35 raise NotMetaConvertible
37 | C.Var (u1, ens1), C.Var (u2, ens2)
38 | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
39 aux_ens table ens1 ens2
40 | C.Cast (s1, t1), C.Cast (s2, t2)
41 | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
42 | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
43 | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
44 let table = aux table s1 s2 in
46 | C.Appl l1, C.Appl l2 -> (
47 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
48 with Invalid_argument _ -> raise NotMetaConvertible
50 | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
51 when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
52 | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
53 when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
54 aux_ens table ens1 ens2
55 | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
56 when (UriManager.eq u1 u2) && i1 = i2 ->
57 let table = aux table s1 s2 in
58 let table = aux table t1 t2 in (
59 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
60 with Invalid_argument _ -> raise NotMetaConvertible
62 | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
65 (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
66 if i1 <> i2 then raise NotMetaConvertible
68 let res = (aux res s1 s2) in aux res t1 t2)
70 with Invalid_argument _ -> raise NotMetaConvertible
72 | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
75 (fun res (n1, s1, t1) (n2, s2, t2) ->
76 let res = aux res s1 s2 in aux res t1 t2)
78 with Invalid_argument _ -> raise NotMetaConvertible
80 | _, _ -> raise NotMetaConvertible
82 and aux_ens table ens1 ens2 =
83 let cmp (u1, t1) (u2, t2) =
84 compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
86 let ens1 = List.sort cmp ens1
87 and ens2 = List.sort cmp ens2 in
90 (fun res (u1, t1) (u2, t2) ->
91 if not (UriManager.eq u1 u2) then raise NotMetaConvertible
94 with Invalid_argument _ -> raise NotMetaConvertible
100 let meta_convertibility_eq eq1 eq2 =
101 let _, (ty, left, right), _, _ = eq1
102 and _, (ty', left', right'), _, _ = eq2 in
106 let print_table t w =
107 Printf.printf "table %s is:\n" w;
109 (fun (k, v) -> Printf.printf "?%d: ?%d\n" k v)
114 let table = meta_convertibility_aux [] left left' in
115 let _ = meta_convertibility_aux table right right' in
116 (* Printf.printf "meta_convertibility_eq, ok:\n%s\n%s\n" *)
117 (* (string_of_equality eq1) (string_of_equality eq2); *)
118 (* print_newline (); *)
120 with NotMetaConvertible ->
122 let table = meta_convertibility_aux [] left right' in
123 let _ = meta_convertibility_aux table right left' in
124 (* Printf.printf "meta_convertibility_eq, ok:\n%s\n%s\n" *)
125 (* (string_of_equality eq1) (string_of_equality eq2); *)
126 (* print_newline (); *)
128 with NotMetaConvertible ->
133 let meta_convertibility t1 t2 =
135 let _ = meta_convertibility_aux [] t1 t2 in
137 with NotMetaConvertible ->
142 let beta_expand ?(metas_ok=true) ?(match_only=false)
143 what type_of_what where context metasenv ugraph =
144 let module S = CicSubstitution in
145 let module C = Cic in
147 (* let names = names_of_context context in *)
148 (* Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
149 (* (CicPp.pp what names) (CicPp.ppterm what) *)
150 (* (CicPp.pp where names) (CicPp.ppterm where); *)
151 (* print_newline (); *)
155 ((list of all possible beta expansions, subst, metasenv, ugraph),
158 let rec aux lift_amount term context metasenv subst ugraph =
159 (* Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
160 let res, lifted_term =
163 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
165 | C.Var (uri, exp_named_subst) ->
166 let ens', lifted_ens =
167 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
171 (fun (e, s, m, ug) ->
172 (C.Var (uri, e), s, m, ug)) ens'
174 expansions, C.Var (uri, lifted_ens)
179 (fun arg (res, lifted_tl) ->
182 let arg_res, lifted_arg =
183 aux lift_amount arg context metasenv subst ugraph in
186 (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
191 (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
193 (Some lifted_arg)::lifted_tl)
196 (fun (r, s, m, ug) -> None::r, s, m, ug)
203 (fun (l, s, m, ug) ->
204 (C.Meta (i, l), s, m, ug)) l'
206 e, C.Meta (i, lifted_l)
209 | C.Implicit _ as t -> [], t
213 aux lift_amount s context metasenv subst ugraph in
215 aux lift_amount t context metasenv subst ugraph
219 (fun (t, s, m, ug) ->
220 C.Cast (t, lifted_t), s, m, ug) l1 in
223 (fun (t, s, m, ug) ->
224 C.Cast (lifted_s, t), s, m, ug) l2 in
225 l1'@l2', C.Cast (lifted_s, lifted_t)
227 | C.Prod (nn, s, t) ->
229 aux lift_amount s context metasenv subst ugraph in
231 aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
232 metasenv subst ugraph
236 (fun (t, s, m, ug) ->
237 C.Prod (nn, t, lifted_t), s, m, ug) l1 in
240 (fun (t, s, m, ug) ->
241 C.Prod (nn, lifted_s, t), s, m, ug) l2 in
242 l1'@l2', C.Prod (nn, lifted_s, lifted_t)
244 | C.Lambda (nn, s, t) ->
246 aux lift_amount s context metasenv subst ugraph in
248 aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
249 metasenv subst ugraph
253 (fun (t, s, m, ug) ->
254 C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
257 (fun (t, s, m, ug) ->
258 C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
259 l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
261 | C.LetIn (nn, s, t) ->
263 aux lift_amount s context metasenv subst ugraph in
265 aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
266 metasenv subst ugraph
270 (fun (t, s, m, ug) ->
271 C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
274 (fun (t, s, m, ug) ->
275 C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
276 l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
280 aux_list lift_amount l context metasenv subst ugraph
282 (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
285 | C.Const (uri, exp_named_subst) ->
286 let ens', lifted_ens =
287 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
291 (fun (e, s, m, ug) ->
292 (C.Const (uri, e), s, m, ug)) ens'
294 (expansions, C.Const (uri, lifted_ens))
296 | C.MutInd (uri, i ,exp_named_subst) ->
297 let ens', lifted_ens =
298 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
302 (fun (e, s, m, ug) ->
303 (C.MutInd (uri, i, e), s, m, ug)) ens'
305 (expansions, C.MutInd (uri, i, lifted_ens))
307 | C.MutConstruct (uri, i, j, exp_named_subst) ->
308 let ens', lifted_ens =
309 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
313 (fun (e, s, m, ug) ->
314 (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
316 (expansions, C.MutConstruct (uri, i, j, lifted_ens))
318 | C.MutCase (sp, i, outt, t, pl) ->
319 let pl_res, lifted_pl =
320 aux_list lift_amount pl context metasenv subst ugraph
322 let l1, lifted_outt =
323 aux lift_amount outt context metasenv subst ugraph in
325 aux lift_amount t context metasenv subst ugraph in
329 (fun (outt, s, m, ug) ->
330 C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
333 (fun (t, s, m, ug) ->
334 C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
337 (fun (pl, s, m, ug) ->
338 C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
340 (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
343 let len = List.length fl in
346 (fun (nm, idx, ty, bo) (res, lifted_tl) ->
347 let lifted_ty = S.lift lift_amount ty in
348 let bo_res, lifted_bo =
349 aux (lift_amount+len) bo context metasenv subst ugraph in
352 (fun (a, s, m, ug) ->
353 (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
358 (fun (r, s, m, ug) ->
359 (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
360 (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
364 (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
365 C.Fix (i, lifted_fl))
368 let len = List.length fl in
371 (fun (nm, ty, bo) (res, lifted_tl) ->
372 let lifted_ty = S.lift lift_amount ty in
373 let bo_res, lifted_bo =
374 aux (lift_amount+len) bo context metasenv subst ugraph in
377 (fun (a, s, m, ug) ->
378 (nm, lifted_ty, a)::lifted_tl, s, m, ug)
383 (fun (r, s, m, ug) ->
384 (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
385 (nm, lifted_ty, lifted_bo)::lifted_tl)
389 (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
390 C.CoFix (i, lifted_fl))
394 | C.Meta _ when (not metas_ok) ->
398 let subst', metasenv', ugraph' =
399 (* Printf.printf "provo a unificare %s e %s\n" *)
400 (* (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
401 CicUnification.fo_unif metasenv context
402 (S.lift lift_amount what) term ugraph
404 (* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
405 (* (CicPp.ppterm (S.lift lift_amount what)); *)
406 (* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
407 (* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
408 (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
410 let t' = CicMetaSubst.apply_subst subst' term in
411 if not (meta_convertibility term t') then (
412 let names = names_of_context context in
413 (* Printf.printf "\nbeta_expand: term e t' sono diversi!:\n%s\n%s\n\n" *)
414 (* (CicPp.pp term names) (CicPp.pp t' names); *)
418 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
421 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
424 (* print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e)); *)
427 (* Printf.printf "exit aux\n"; *)
430 and aux_list lift_amount l context metasenv subst ugraph =
432 (fun arg (res, lifted_tl) ->
433 let arg_res, lifted_arg =
434 aux lift_amount arg context metasenv subst ugraph in
436 (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
439 (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
440 lifted_arg::lifted_tl)
443 and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
445 (fun (u, arg) (res, lifted_tl) ->
446 let arg_res, lifted_arg =
447 aux lift_amount arg context metasenv subst ugraph in
450 (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
452 (l1 @ (List.map (fun (r, s, m, ug) ->
453 (u, lifted_arg)::r, s, m, ug) res),
454 (u, lifted_arg)::lifted_tl)
455 ) exp_named_subst ([], [])
458 let expansions, _ = aux 0 where context metasenv [] ugraph in
460 (fun (term, subst, metasenv, ugraph) ->
461 let term' = C.Lambda (C.Anonymous, type_of_what, term) in
462 (* Printf.printf "term is: %s\nsubst is:\n%s\n\n" *)
463 (* (CicPp.ppterm term') (print_subst subst); *)
464 (term', subst, metasenv, ugraph))
470 Cic.term * (* proof *)
471 (Cic.term * (* type *)
472 Cic.term * (* left side *)
473 Cic.term) * (* right side *)
474 Cic.metasenv * (* environment for metas *)
475 Cic.term list (* arguments *)
479 let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
480 let module C = Cic in
481 let module S = CicSubstitution in
482 let module T = CicTypeChecker in
483 let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
484 let rec aux index newmeta = function
486 | (Some (_, C.Decl (term)))::tl ->
487 let do_find context term =
489 | C.Prod (name, s, t) ->
490 (* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
491 let (head, newmetas, args, _) =
492 PrimitiveTactics.new_metasenv_for_apply newmeta proof
493 context (S.lift index term)
499 | C.Meta (i, _) -> (max maxm i)
504 if List.length args = 0 then
507 C.Appl ((C.Rel index)::args)
510 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
511 Printf.printf "OK: %s\n" (CicPp.ppterm term);
512 Some (p, (ty, t1, t2), newmetas, args), (newmeta+1)
515 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
517 (ty, S.lift index t1, S.lift index t2), [], []), (newmeta+1)
520 match do_find context term with
522 let tl, newmeta' = (aux (index+1) newmeta tl) in
523 p::tl, max newmeta newmeta'
525 aux (index+1) newmeta tl
528 aux (index+1) newmeta tl
530 aux 1 newmeta context
534 let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) =
535 let table = Hashtbl.create (List.length args) in
538 (fun t (newargs, index) ->
541 Hashtbl.add table i index;
542 ((Cic.Meta (index, l))::newargs, index+1)
547 ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
552 (fun (i, context, term) menv ->
554 let index = Hashtbl.find table i in
555 (index, context, term)::menv
557 (i, context, term)::menv)
560 (newmeta + (List.length newargs) + 1,
561 (repl proof, (repl ty, repl left, repl right), menv', newargs))
565 exception TermIsNotAnEquality;;
567 let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
568 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
569 (proof, (ty, t1, t2), [], [])
571 raise TermIsNotAnEquality
575 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
578 let superposition_left (metasenv, context, ugraph) target source =
579 let module C = Cic in
580 let module S = CicSubstitution in
581 let module M = CicMetaSubst in
582 let module HL = HelmLibraryObjects in
583 let module CR = CicReduction in
584 (* we assume that target is ground (does not contain metavariables): this
585 * should always be the case (I hope, at least) *)
586 let proof, (eq_ty, left, right), _, _ = target in
587 let eqproof, (ty, t1, t2), newmetas, args = source in
589 (* ALB: TODO check that ty and eq_ty are indeed equal... *)
590 (* assert (eq_ty = ty); *)
596 match nonrec_kbo left right with
600 Printf.printf "????????? %s = %s" (CicPp.ppterm left)
601 (CicPp.ppterm right);
603 assert false (* again, for ground terms this shouldn't happen... *)
606 let metasenv' = newmetas @ metasenv in
609 (fun (t, s, m, ug) ->
610 nonrec_kbo (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
611 (beta_expand t1 ty where context metasenv' ugraph)
614 (fun (t, s, m, ug) ->
615 nonrec_kbo (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
616 (beta_expand t2 ty where context metasenv' ugraph)
618 (* let what, other = *)
619 (* if is_left then left, right *)
620 (* else right, left *)
622 let build_new what other eq_URI (t, s, m, ug) =
623 let newgoal, newgoalproof =
625 | C.Lambda (nn, ty, bo) ->
626 let bo' = S.subst (M.apply_subst s other) bo in
629 [C.MutInd (HL.Logic.eq_URI, 0, []);
631 if is_left then [bo'; S.lift 1 right]
632 else [S.lift 1 left; bo'])
634 let t' = C.Lambda (nn, ty, bo'') in
635 S.subst (M.apply_subst s other) bo,
637 (C.Appl [C.Const (eq_URI, []); ty; what; t';
638 proof; other; eqproof])
642 if is_left then (eq_ty, newgoal, right)
643 else (eq_ty, left, newgoal)
645 (eqproof, equation, [], [])
647 let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
648 and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
653 let superposition_right newmeta (metasenv, context, ugraph) target source =
654 let module C = Cic in
655 let module S = CicSubstitution in
656 let module M = CicMetaSubst in
657 let module HL = HelmLibraryObjects in
658 let module CR = CicReduction in
659 let eqproof, (eq_ty, left, right), newmetas, args = target in
660 let eqp', (ty', t1, t2), newm', args' = source in
661 let maxmeta = ref newmeta in
663 (* TODO check if ty and ty' are equal... *)
664 (* assert (eq_ty = ty'); *)
669 (* let ok term subst other other_eq_side ugraph = *)
670 (* match term with *)
671 (* | C.Lambda (nn, ty, bo) -> *)
672 (* let bo' = S.subst (M.apply_subst subst other) bo in *)
673 (* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
675 (* | _ -> assert false *)
677 let condition left right what other (t, s, m, ug) =
678 let subst = M.apply_subst s in
679 let cmp1 = nonrec_kbo (subst what) (subst other) in
680 let cmp2 = nonrec_kbo (subst left) (subst right) in
681 (* cmp1 = Gt && cmp2 = Gt *)
682 cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
683 (* && (ok t s other right ug) *)
685 let metasenv' = metasenv @ newmetas @ newm' in
686 let beta_expand = beta_expand ~metas_ok:false in
689 (condition left right t1 t2)
690 (beta_expand t1 eq_ty left context metasenv' ugraph)
693 (condition left right t2 t1)
694 (beta_expand t2 eq_ty left context metasenv' ugraph)
697 (condition right left t1 t2)
698 (beta_expand t1 eq_ty right context metasenv' ugraph)
701 (condition right left t2 t1)
702 (beta_expand t2 eq_ty right context metasenv' ugraph)
704 let newmetas = newmetas @ newm' in
705 let newargs = args @ args' in
706 let build_new what other is_left eq_URI (t, s, m, ug) =
707 (* let what, other = *)
708 (* if is_left then left, right *)
709 (* else right, left *)
711 let newterm, neweqproof =
713 | C.Lambda (nn, ty, bo) ->
714 let bo' = M.apply_subst s (S.subst other bo) in
717 [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
718 if is_left then [bo'; S.lift 1 right]
719 else [S.lift 1 left; bo'])
721 let t' = C.Lambda (nn, ty, bo'') in
724 (C.Appl [C.Const (eq_URI, []); ty; what; t';
725 eqproof; other; eqp'])
728 let newmeta, newequality =
730 if is_left then (newterm, M.apply_subst s right)
731 else (M.apply_subst s left, newterm) in
733 (neweqproof, (eq_ty, left, right), newmetas, newargs)
738 let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
739 and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
740 and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
741 and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
743 | _, (_, left, right), _, _ ->
744 not (fst (CR.are_convertible context left right ugraph))
746 !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4))
750 let is_identity ((_, context, ugraph) as env) = function
751 | ((_, (ty, left, right), _, _) as equality) ->
754 (fst (CicReduction.are_convertible context left right ugraph)))
757 (* Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
758 (* print_newline (); *)
764 let demodulation newmeta (metasenv, context, ugraph) target source =
765 let module C = Cic in
766 let module S = CicSubstitution in
767 let module M = CicMetaSubst in
768 let module HL = HelmLibraryObjects in
769 let module CR = CicReduction in
771 let proof, (eq_ty, left, right), metas, args = target
772 and proof', (ty, t1, t2), metas', args' = source in
776 let get_params step =
778 | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
779 | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
780 | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
781 | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
784 let rec demodulate newmeta step metasenv target =
785 let proof, (eq_ty, left, right), metas, args = target in
786 let is_left, what, other, eq_URI = get_params step in
788 let env = metasenv, context, ugraph in
789 let names = names_of_context context in
791 (* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
792 (* (string_of_equality ~env target) (CicPp.pp what names) *)
793 (* (CicPp.pp other names) (string_of_bool is_left); *)
794 (* Printf.printf "step: %d" step; *)
795 (* print_newline (); *)
797 let ok (t, s, m, ug) =
798 nonrec_kbo (M.apply_subst s what) (M.apply_subst s other) = Gt
801 let r = (beta_expand ~metas_ok:false ~match_only:true
802 what ty (if is_left then left else right)
803 context (metasenv @ metas) ugraph)
805 (* print_endline "res:"; *)
806 (* List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
807 (* print_newline (); *)
808 (* Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
809 (* print_newline (); *)
814 if step = 0 then newmeta, target
815 else demodulate newmeta (step-1) metasenv target
816 | (t, s, m, ug)::_ ->
817 let newterm, newproof =
819 | C.Lambda (nn, ty, bo) ->
820 let bo' = M.apply_subst s (S.subst other bo) in
823 [C.MutInd (HL.Logic.eq_URI, 0, []);
825 if is_left then [bo'; S.lift 1 right]
826 else [S.lift 1 left; bo'])
828 let t' = C.Lambda (nn, ty, bo'') in
829 M.apply_subst s (S.subst other bo),
831 (C.Appl [C.Const (eq_URI, []); ty; what; t';
832 proof; other; proof'])
835 let newmeta, newtarget =
837 if is_left then (newterm, M.apply_subst s right)
838 else (M.apply_subst s left, newterm) in
839 let newmetasenv = metasenv @ metas in
840 let newargs = args @ args' in
842 (newproof, (eq_ty, left, right), newmetasenv, newargs)
845 "demodulate, newtarget: %s\ntarget was: %s\n"
846 (string_of_equality ~env newtarget)
847 (string_of_equality ~env target);
849 if is_identity env newtarget then
852 demodulate newmeta step metasenv newtarget
854 demodulate newmeta 3 (metasenv @ metas') target
859 let demodulation newmeta env target source =