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, table =
13 try List.assoc m1 table, table
14 with Not_found -> m2, (m1, m2)::table
16 if m1_binding <> m2 then
17 raise NotMetaConvertible
23 | None, Some _ | Some _, None -> raise NotMetaConvertible
25 | Some t1, Some t2 -> (aux res t1 t2))
27 with Invalid_argument _ ->
28 raise NotMetaConvertible
30 | C.Var (u1, ens1), C.Var (u2, ens2)
31 | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
32 aux_ens table ens1 ens2
33 | C.Cast (s1, t1), C.Cast (s2, t2)
34 | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
35 | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
36 | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
37 let table = aux table s1 s2 in
39 | C.Appl l1, C.Appl l2 -> (
40 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
41 with Invalid_argument _ -> raise NotMetaConvertible
43 | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
44 when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
45 | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
46 when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
47 aux_ens table ens1 ens2
48 | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
49 when (UriManager.eq u1 u2) && i1 = i2 ->
50 let table = aux table s1 s2 in
51 let table = aux table t1 t2 in (
52 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
53 with Invalid_argument _ -> raise NotMetaConvertible
55 | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
58 (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
59 if i1 <> i2 then raise NotMetaConvertible
61 let res = (aux res s1 s2) in aux res t1 t2)
63 with Invalid_argument _ -> raise NotMetaConvertible
65 | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
68 (fun res (n1, s1, t1) (n2, s2, t2) ->
69 let res = aux res s1 s2 in aux res t1 t2)
71 with Invalid_argument _ -> raise NotMetaConvertible
73 | _, _ -> raise NotMetaConvertible
75 and aux_ens table ens1 ens2 =
76 let cmp (u1, t1) (u2, t2) =
77 compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
79 let ens1 = List.sort cmp ens1
80 and ens2 = List.sort cmp ens2 in
83 (fun res (u1, t1) (u2, t2) ->
84 if not (UriManager.eq u1 u2) then raise NotMetaConvertible
87 with Invalid_argument _ -> raise NotMetaConvertible
93 let meta_convertibility_eq eq1 eq2 =
94 let _, (ty, left, right), _, _ = eq1
95 and _, (ty', left', right'), _, _ = eq2 in
100 Printf.printf "table %s is:\n" w;
102 (fun (k, v) -> Printf.printf "?%d: ?%d\n" k v)
107 let table = meta_convertibility_aux [] left left' in
108 (* print_table table "before"; *)
109 let _ = meta_convertibility_aux table right right' in
110 (* print_table table "after"; *)
112 with NotMetaConvertible ->
113 (* Printf.printf "NotMetaConvertible:\n%s = %s\n%s = %s\n\n" *)
114 (* (CicPp.ppterm left) (CicPp.ppterm right) *)
115 (* (CicPp.ppterm left') (CicPp.ppterm right'); *)
117 let table = meta_convertibility_aux [] left right' in
118 let _ = meta_convertibility_aux table right left' in
120 with NotMetaConvertible ->
125 let meta_convertibility t1 t2 =
127 let _ = meta_convertibility_aux [] t1 t2 in
129 with NotMetaConvertible ->
134 let beta_expand ?(metas_ok=true) ?(match_only=false)
135 what type_of_what where context metasenv ugraph =
136 let module S = CicSubstitution in
137 let module C = Cic in
140 ((list of all possible beta expansions, subst, metasenv, ugraph),
143 let rec aux lift_amount term context metasenv subst ugraph =
144 (* Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
145 let res, lifted_term =
148 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
150 | C.Var (uri, exp_named_subst) ->
151 let ens', lifted_ens =
152 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
156 (fun (e, s, m, ug) ->
157 (C.Var (uri, e), s, m, ug)) ens'
159 expansions, C.Var (uri, lifted_ens)
164 (fun arg (res, lifted_tl) ->
167 let arg_res, lifted_arg =
168 aux lift_amount arg context metasenv subst ugraph in
171 (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
176 (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
178 (Some lifted_arg)::lifted_tl)
181 (fun (r, s, m, ug) -> None::r, s, m, ug)
188 (fun (l, s, m, ug) ->
189 (C.Meta (i, l), s, m, ug)) l'
191 e, C.Meta (i, lifted_l)
194 | C.Implicit _ as t -> [], t
198 aux lift_amount s context metasenv subst ugraph in
200 aux lift_amount t context metasenv subst ugraph
204 (fun (t, s, m, ug) ->
205 C.Cast (t, lifted_t), s, m, ug) l1 in
208 (fun (t, s, m, ug) ->
209 C.Cast (lifted_s, t), s, m, ug) l2 in
210 l1'@l2', C.Cast (lifted_s, lifted_t)
212 | C.Prod (nn, s, t) ->
214 aux lift_amount s context metasenv subst ugraph in
216 aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
217 metasenv subst ugraph
221 (fun (t, s, m, ug) ->
222 C.Prod (nn, t, lifted_t), s, m, ug) l1 in
225 (fun (t, s, m, ug) ->
226 C.Prod (nn, lifted_s, t), s, m, ug) l2 in
227 l1'@l2', C.Prod (nn, lifted_s, lifted_t)
229 | C.Lambda (nn, s, t) ->
231 aux lift_amount s context metasenv subst ugraph in
233 aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
234 metasenv subst ugraph
238 (fun (t, s, m, ug) ->
239 C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
242 (fun (t, s, m, ug) ->
243 C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
244 l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
246 | C.LetIn (nn, s, t) ->
248 aux lift_amount s context metasenv subst ugraph in
250 aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
251 metasenv subst ugraph
255 (fun (t, s, m, ug) ->
256 C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
259 (fun (t, s, m, ug) ->
260 C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
261 l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
265 aux_list lift_amount l context metasenv subst ugraph
267 (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
270 | C.Const (uri, exp_named_subst) ->
271 let ens', lifted_ens =
272 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
276 (fun (e, s, m, ug) ->
277 (C.Const (uri, e), s, m, ug)) ens'
279 (expansions, C.Const (uri, lifted_ens))
281 | C.MutInd (uri, i ,exp_named_subst) ->
282 let ens', lifted_ens =
283 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
287 (fun (e, s, m, ug) ->
288 (C.MutInd (uri, i, e), s, m, ug)) ens'
290 (expansions, C.MutInd (uri, i, lifted_ens))
292 | C.MutConstruct (uri, i, j, exp_named_subst) ->
293 let ens', lifted_ens =
294 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
298 (fun (e, s, m, ug) ->
299 (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
301 (expansions, C.MutConstruct (uri, i, j, lifted_ens))
303 | C.MutCase (sp, i, outt, t, pl) ->
304 let pl_res, lifted_pl =
305 aux_list lift_amount pl context metasenv subst ugraph
307 let l1, lifted_outt =
308 aux lift_amount outt context metasenv subst ugraph in
310 aux lift_amount t context metasenv subst ugraph in
314 (fun (outt, s, m, ug) ->
315 C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
318 (fun (t, s, m, ug) ->
319 C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
322 (fun (pl, s, m, ug) ->
323 C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
325 (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
328 let len = List.length fl in
331 (fun (nm, idx, ty, bo) (res, lifted_tl) ->
332 let lifted_ty = S.lift lift_amount ty in
333 let bo_res, lifted_bo =
334 aux (lift_amount+len) bo context metasenv subst ugraph in
337 (fun (a, s, m, ug) ->
338 (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
343 (fun (r, s, m, ug) ->
344 (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
345 (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
349 (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
350 C.Fix (i, lifted_fl))
353 let len = List.length fl in
356 (fun (nm, ty, bo) (res, lifted_tl) ->
357 let lifted_ty = S.lift lift_amount ty in
358 let bo_res, lifted_bo =
359 aux (lift_amount+len) bo context metasenv subst ugraph in
362 (fun (a, s, m, ug) ->
363 (nm, lifted_ty, a)::lifted_tl, s, m, ug)
368 (fun (r, s, m, ug) ->
369 (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
370 (nm, lifted_ty, lifted_bo)::lifted_tl)
374 (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
375 C.CoFix (i, lifted_fl))
379 | C.Meta _ when (not metas_ok) ->
383 let subst', metasenv', ugraph' =
384 CicUnification.fo_unif metasenv context
385 (S.lift lift_amount what) term ugraph
387 (* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
388 (* (CicPp.ppterm (S.lift lift_amount what)); *)
389 (* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
390 (* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
391 (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
393 let term' = CicMetaSubst.apply_subst subst' term in
394 if not (meta_convertibility term term') then (
395 (* let names = names_of_context context in *)
396 (* Printf.printf "\nterm e term' sono diversi!:\n%s\n%s\n\n" *)
397 (* (CicPp.pp term names) (CicPp.pp term' names); *)
401 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
404 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
409 (* Printf.printf "exit aux\n"; *)
412 and aux_list lift_amount l context metasenv subst ugraph =
414 (fun arg (res, lifted_tl) ->
415 let arg_res, lifted_arg =
416 aux lift_amount arg context metasenv subst ugraph in
418 (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
421 (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
422 lifted_arg::lifted_tl)
425 and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
427 (fun (u, arg) (res, lifted_tl) ->
428 let arg_res, lifted_arg =
429 aux lift_amount arg context metasenv subst ugraph in
432 (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
434 (l1 @ (List.map (fun (r, s, m, ug) ->
435 (u, lifted_arg)::r, s, m, ug) res),
436 (u, lifted_arg)::lifted_tl)
437 ) exp_named_subst ([], [])
440 let expansions, _ = aux 0 where context metasenv [] ugraph in
442 (fun (term, subst, metasenv, ugraph) ->
443 let term' = C.Lambda (C.Anonymous, type_of_what, term) in
444 (* Printf.printf "term is: %s\nsubst is:\n%s\n\n" *)
445 (* (CicPp.ppterm term') (print_subst subst); *)
446 (term', subst, metasenv, ugraph))
452 Cic.term * (* proof *)
453 (Cic.term * (* type *)
454 Cic.term * (* left side *)
455 Cic.term) * (* right side *)
456 Cic.metasenv * (* environment for metas *)
457 Cic.term list (* arguments *)
461 let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
462 let module C = Cic in
463 let module S = CicSubstitution in
464 let module T = CicTypeChecker in
465 let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
466 let rec aux index newmeta = function
468 | (Some (_, C.Decl (term)))::tl ->
469 let do_find context term =
471 | C.Prod (name, s, t) ->
472 (* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
473 let (head, newmetas, args, _) =
474 PrimitiveTactics.new_metasenv_for_apply newmeta proof
475 context (S.lift index term)
481 | C.Meta (i, _) -> (max maxm i)
486 if List.length args = 0 then
489 C.Appl ((C.Rel index)::args)
492 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
493 Printf.printf "OK: %s\n" (CicPp.ppterm term);
494 Some (p, (ty, t1, t2), newmetas, args), (newmeta+1)
497 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
499 (ty, S.lift index t1, S.lift index t2), [], []), (newmeta+1)
502 match do_find context term with
504 let tl, newmeta' = (aux (index+1) newmeta tl) in
505 p::tl, max newmeta newmeta'
507 aux (index+1) newmeta tl
510 aux (index+1) newmeta tl
512 aux 1 newmeta context
516 let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) =
519 (fun t (newargs, index) ->
521 | Cic.Meta (i, l) -> ((Cic.Meta (index, l))::newargs, index+1)
526 ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
531 (fun (i, context, term) (menv, index) ->
532 ((index, context, term)::menv, index+1))
535 (newmeta + (List.length newargs) + 1,
536 (repl proof, (repl ty, repl left, repl right), menv', newargs))
540 exception TermIsNotAnEquality;;
542 let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
543 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
544 (proof, (ty, t1, t2), [], [])
546 raise TermIsNotAnEquality
550 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
553 let superposition_left (metasenv, context, ugraph) target source =
554 let module C = Cic in
555 let module S = CicSubstitution in
556 let module M = CicMetaSubst in
557 let module HL = HelmLibraryObjects in
558 let module CR = CicReduction in
559 (* we assume that target is ground (does not contain metavariables): this
560 * should always be the case (I hope, at least) *)
561 let proof, (eq_ty, left, right), _, _ = target in
562 let eqproof, (ty, t1, t2), newmetas, args = source in
564 (* ALB: TODO check that ty and eq_ty are indeed equal... *)
568 match nonrec_kbo left right with
572 Printf.printf "????????? %s = %s" (CicPp.ppterm left)
573 (CicPp.ppterm right);
575 assert false (* again, for ground terms this shouldn't happen... *)
578 let metasenv' = newmetas @ metasenv in
581 (fun (t, s, m, ug) ->
582 nonrec_kbo (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
583 (beta_expand t1 ty where context metasenv' ugraph)
586 (fun (t, s, m, ug) ->
587 nonrec_kbo (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
588 (beta_expand t2 ty where context metasenv' ugraph)
590 (* let what, other = *)
591 (* if is_left then left, right *)
592 (* else right, left *)
594 let build_new what other eq_URI (t, s, m, ug) =
595 let newgoal, newgoalproof =
597 | C.Lambda (nn, ty, bo) ->
598 let bo' = S.subst (M.apply_subst s other) bo in
601 [C.MutInd (HL.Logic.eq_URI, 0, []);
603 if is_left then [bo'; S.lift 1 right] else [S.lift 1 left; bo'])
605 let t' = C.Lambda (nn, ty, bo'') in
606 S.subst (M.apply_subst s other) bo,
608 (C.Appl [C.Const (eq_URI, []); ty; what; t';
609 proof; other; eqproof])
613 if is_left then (eq_ty, newgoal, right)
614 else (eq_ty, left, newgoal)
616 (eqproof, equation, [], [])
618 let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
619 and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
624 let superposition_right newmeta (metasenv, context, ugraph) target source =
625 let module C = Cic in
626 let module S = CicSubstitution in
627 let module M = CicMetaSubst in
628 let module HL = HelmLibraryObjects in
629 let module CR = CicReduction in
630 let eqproof, (eq_ty, left, right), newmetas, args = target in
631 let eqp', (ty', t1, t2), newm', args' = source in
632 let maxmeta = ref newmeta in
634 (* TODO check if ty and ty' are equal... *)
635 assert (eq_ty = ty');
637 (* let ok term subst other other_eq_side ugraph = *)
638 (* match term with *)
639 (* | C.Lambda (nn, ty, bo) -> *)
640 (* let bo' = S.subst (M.apply_subst subst other) bo in *)
641 (* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
643 (* | _ -> assert false *)
645 let condition left right what other (t, s, m, ug) =
646 let subst = M.apply_subst s in
647 let cmp1 = nonrec_kbo (subst what) (subst other) in
648 let cmp2 = nonrec_kbo (subst left) (subst right) in
649 (* cmp1 = Gt && cmp2 = Gt *)
650 cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
651 (* && (ok t s other right ug) *)
653 let metasenv' = metasenv @ newmetas @ newm' in
654 let beta_expand = beta_expand ~metas_ok:false in
657 (condition left right t1 t2)
658 (beta_expand t1 eq_ty left context metasenv' ugraph)
661 (condition left right t2 t1)
662 (beta_expand t2 eq_ty left context metasenv' ugraph)
665 (condition right left t1 t2)
666 (beta_expand t1 eq_ty right context metasenv' ugraph)
669 (condition right left t2 t1)
670 (beta_expand t2 eq_ty right context metasenv' ugraph)
672 let newmetas = newmetas @ newm' in
673 let newargs = args @ args' in
674 let build_new what other is_left eq_URI (t, s, m, ug) =
675 (* let what, other = *)
676 (* if is_left then left, right *)
677 (* else right, left *)
679 let newterm, neweqproof =
681 | C.Lambda (nn, ty, bo) ->
682 let bo' = M.apply_subst s (S.subst other bo) in
685 [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
686 if is_left then [bo'; S.lift 1 right] else [S.lift 1 left; bo'])
688 let t' = C.Lambda (nn, ty, bo'') in
691 (C.Appl [C.Const (eq_URI, []); ty; what; t'; eqproof; other; eqp'])
694 let newmeta, newequality =
696 if is_left then (newterm, M.apply_subst s right)
697 else (M.apply_subst s left, newterm) in
699 (neweqproof, (eq_ty, left, right), newmetas, newargs)
704 let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
705 and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
706 and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
707 and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
709 | _, (_, left, right), _, _ ->
710 not (fst (CR.are_convertible context left right ugraph))
712 !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4))
716 let demodulation newmeta (metasenv, context, ugraph) target source =
717 let module C = Cic in
718 let module S = CicSubstitution in
719 let module M = CicMetaSubst in
720 let module HL = HelmLibraryObjects in
721 let module CR = CicReduction in
723 let proof, (eq_ty, left, right), metas, args = target
724 and proof', (ty, t1, t2), metas', args' = source in
728 let get_params step =
730 | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
731 | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
732 | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
733 | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
736 let rec demodulate newmeta step metasenv target =
737 let proof, (eq_ty, left, right), metas, args = target in
738 let is_left, what, other, eq_URI = get_params step in
740 let env = metasenv, context, ugraph in
741 let names = names_of_context context in
743 (* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
744 (* (string_of_equality ~env target) (CicPp.pp what names) *)
745 (* (CicPp.pp other names) (string_of_bool is_left); *)
746 (* Printf.printf "step: %d\n" step; *)
747 (* print_newline (); *)
749 let ok (t, s, m, ug) =
750 nonrec_kbo (M.apply_subst s what) (M.apply_subst s other) = Gt
753 let r = (beta_expand ~metas_ok:false ~match_only:true
754 what ty (if is_left then left else right)
755 context (metasenv @ metas) ugraph)
757 (* print_endline "res:"; *)
758 (* List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
763 if step = 0 then newmeta, target
764 else demodulate newmeta (step-1) metasenv target
765 | (t, s, m, ug)::_ ->
766 let newterm, newproof =
768 | C.Lambda (nn, ty, bo) ->
769 let bo' = M.apply_subst s (S.subst other bo) in
772 [C.MutInd (HL.Logic.eq_URI, 0, []);
774 if is_left then [bo'; S.lift 1 right]
775 else [S.lift 1 left; bo'])
777 let t' = C.Lambda (nn, ty, bo'') in
778 M.apply_subst s (S.subst other bo),
780 (C.Appl [C.Const (eq_URI, []); ty; what; t';
781 proof; other; proof'])
784 let newmeta, newtarget =
786 if is_left then (newterm, M.apply_subst s right)
787 else (M.apply_subst s left, newterm) in
788 let newmetasenv = metasenv @ metas in
789 let newargs = args @ args' in
791 (newproof, (eq_ty, left, right), newmetasenv, newargs)
794 (* "demodulate, newtarget: %s\ntarget was: %s\n" *)
795 (* (string_of_equality ~env newtarget) *)
796 (* (string_of_equality ~env target); *)
797 (* print_newline (); *)
798 demodulate newmeta step metasenv newtarget
800 demodulate newmeta 3 (metasenv @ metas') target
805 let demodulation newmeta env target source =