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 table = 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'); *)
120 let meta_convertibility t1 t2 =
122 let _ = meta_convertibility_aux [] t1 t2 in
124 with NotMetaConvertible ->
129 let beta_expand ?(metas_ok=true) ?(match_only=false)
130 what type_of_what where context metasenv ugraph =
131 let module S = CicSubstitution in
132 let module C = Cic in
135 ((list of all possible beta expansions, subst, metasenv, ugraph),
138 let rec aux lift_amount term context metasenv subst ugraph =
139 (* Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
140 let res, lifted_term =
143 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
145 | C.Var (uri, exp_named_subst) ->
146 let ens', lifted_ens =
147 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
151 (fun (e, s, m, ug) ->
152 (C.Var (uri, e), s, m, ug)) ens'
154 expansions, C.Var (uri, lifted_ens)
159 (fun arg (res, lifted_tl) ->
162 let arg_res, lifted_arg =
163 aux lift_amount arg context metasenv subst ugraph in
166 (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
171 (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
173 (Some lifted_arg)::lifted_tl)
176 (fun (r, s, m, ug) -> None::r, s, m, ug)
183 (fun (l, s, m, ug) ->
184 (C.Meta (i, l), s, m, ug)) l'
186 e, C.Meta (i, lifted_l)
189 | C.Implicit _ as t -> [], t
193 aux lift_amount s context metasenv subst ugraph in
195 aux lift_amount t context metasenv subst ugraph
199 (fun (t, s, m, ug) ->
200 C.Cast (t, lifted_t), s, m, ug) l1 in
203 (fun (t, s, m, ug) ->
204 C.Cast (lifted_s, t), s, m, ug) l2 in
205 l1'@l2', C.Cast (lifted_s, lifted_t)
207 | C.Prod (nn, s, t) ->
209 aux lift_amount s context metasenv subst ugraph in
211 aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
212 metasenv subst ugraph
216 (fun (t, s, m, ug) ->
217 C.Prod (nn, t, lifted_t), s, m, ug) l1 in
220 (fun (t, s, m, ug) ->
221 C.Prod (nn, lifted_s, t), s, m, ug) l2 in
222 l1'@l2', C.Prod (nn, lifted_s, lifted_t)
224 | C.Lambda (nn, s, t) ->
226 aux lift_amount s context metasenv subst ugraph in
228 aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
229 metasenv subst ugraph
233 (fun (t, s, m, ug) ->
234 C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
237 (fun (t, s, m, ug) ->
238 C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
239 l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
241 | C.LetIn (nn, s, t) ->
243 aux lift_amount s context metasenv subst ugraph in
245 aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
246 metasenv subst ugraph
250 (fun (t, s, m, ug) ->
251 C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
254 (fun (t, s, m, ug) ->
255 C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
256 l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
260 aux_list lift_amount l context metasenv subst ugraph
262 (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
265 | C.Const (uri, exp_named_subst) ->
266 let ens', lifted_ens =
267 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
271 (fun (e, s, m, ug) ->
272 (C.Const (uri, e), s, m, ug)) ens'
274 (expansions, C.Const (uri, lifted_ens))
276 | C.MutInd (uri, i ,exp_named_subst) ->
277 let ens', lifted_ens =
278 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
282 (fun (e, s, m, ug) ->
283 (C.MutInd (uri, i, e), s, m, ug)) ens'
285 (expansions, C.MutInd (uri, i, lifted_ens))
287 | C.MutConstruct (uri, i, j, exp_named_subst) ->
288 let ens', lifted_ens =
289 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
293 (fun (e, s, m, ug) ->
294 (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
296 (expansions, C.MutConstruct (uri, i, j, lifted_ens))
298 | C.MutCase (sp, i, outt, t, pl) ->
299 let pl_res, lifted_pl =
300 aux_list lift_amount pl context metasenv subst ugraph
302 let l1, lifted_outt =
303 aux lift_amount outt context metasenv subst ugraph in
305 aux lift_amount t context metasenv subst ugraph in
309 (fun (outt, s, m, ug) ->
310 C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
313 (fun (t, s, m, ug) ->
314 C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
317 (fun (pl, s, m, ug) ->
318 C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
320 (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
323 let len = List.length fl in
326 (fun (nm, idx, ty, bo) (res, lifted_tl) ->
327 let lifted_ty = S.lift lift_amount ty in
328 let bo_res, lifted_bo =
329 aux (lift_amount+len) bo context metasenv subst ugraph in
332 (fun (a, s, m, ug) ->
333 (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
338 (fun (r, s, m, ug) ->
339 (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
340 (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
344 (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
345 C.Fix (i, lifted_fl))
348 let len = List.length fl in
351 (fun (nm, ty, bo) (res, lifted_tl) ->
352 let lifted_ty = S.lift lift_amount ty in
353 let bo_res, lifted_bo =
354 aux (lift_amount+len) bo context metasenv subst ugraph in
357 (fun (a, s, m, ug) ->
358 (nm, lifted_ty, a)::lifted_tl, s, m, ug)
363 (fun (r, s, m, ug) ->
364 (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
365 (nm, lifted_ty, lifted_bo)::lifted_tl)
369 (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
370 C.CoFix (i, lifted_fl))
374 | C.Meta _ when (not metas_ok) ->
378 let subst', metasenv', ugraph' =
379 CicUnification.fo_unif metasenv context
380 (S.lift lift_amount what) term ugraph
382 (* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
383 (* (CicPp.ppterm (S.lift lift_amount what)); *)
384 (* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
385 (* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
386 (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
387 let term' = CicMetaSubst.apply_subst subst' term in (
388 if match_only && not (meta_convertibility term term') then (
389 (* Printf.printf "term e term' sono diversi!:\n%s\n%s\n\n" *)
390 (* (CicPp.ppterm term) (CicPp.ppterm term'); *)
395 (* if match_only then *)
396 (* Printf.printf "OK, trovato match con %s\n" *)
397 (* (CicPp.ppterm term) *)
399 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
405 (* Printf.printf "exit aux\n"; *)
408 and aux_list lift_amount l context metasenv subst ugraph =
410 (fun arg (res, lifted_tl) ->
411 let arg_res, lifted_arg =
412 aux lift_amount arg context metasenv subst ugraph in
414 (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
417 (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
418 lifted_arg::lifted_tl)
421 and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
423 (fun (u, arg) (res, lifted_tl) ->
424 let arg_res, lifted_arg =
425 aux lift_amount arg context metasenv subst ugraph in
428 (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
430 (l1 @ (List.map (fun (r, s, m, ug) ->
431 (u, lifted_arg)::r, s, m, ug) res),
432 (u, lifted_arg)::lifted_tl)
433 ) exp_named_subst ([], [])
436 let expansions, _ = aux 0 where context metasenv [] ugraph in
438 (fun (term, subst, metasenv, ugraph) ->
439 let term' = C.Lambda (C.Anonymous, type_of_what, term) in
440 (* Printf.printf "term is: %s\nsubst is:\n%s\n\n" *)
441 (* (CicPp.ppterm term') (print_subst subst); *)
442 (term', subst, metasenv, ugraph))
448 Cic.term * (* proof *)
449 (Cic.term * (* type *)
450 Cic.term * (* left side *)
451 Cic.term) * (* right side *)
452 Cic.metasenv * (* environment for metas *)
453 Cic.term list (* arguments *)
457 let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
458 let module C = Cic in
459 let module S = CicSubstitution in
460 let module T = CicTypeChecker in
461 let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
462 let rec aux index newmeta = function
464 | (Some (_, C.Decl (term)))::tl ->
465 let do_find context term =
467 | C.Prod (name, s, t) ->
468 (* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
469 let (head, newmetas, args, _) =
470 PrimitiveTactics.new_metasenv_for_apply newmeta proof
471 context (S.lift index term)
477 | C.Meta (i, _) -> (max maxm i)
482 if List.length args = 0 then
485 C.Appl ((C.Rel index)::args)
488 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
489 Printf.printf "OK: %s\n" (CicPp.ppterm term);
490 Some (p, (ty, t1, t2), newmetas, args), (newmeta+1)
493 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
495 (ty, S.lift index t1, S.lift index t2), [], []), (newmeta+1)
498 match do_find context term with
500 let tl, newmeta' = (aux (index+1) newmeta tl) in
501 p::tl, max newmeta newmeta'
503 aux (index+1) newmeta tl
506 aux (index+1) newmeta tl
508 aux 1 newmeta context
512 let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) =
515 (fun t (newargs, index) ->
517 | Cic.Meta (i, l) -> ((Cic.Meta (index, l))::newargs, index+1)
522 ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
527 (fun (i, context, term) (menv, index) ->
528 ((index, context, term)::menv, index+1))
531 (newmeta + (List.length newargs) + 1,
532 (repl proof, (repl ty, repl left, repl right), menv', newargs))
536 exception TermIsNotAnEquality;;
538 let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
539 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
540 (proof, (ty, t1, t2), [], [])
542 raise TermIsNotAnEquality
546 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
549 let superposition_left (metasenv, context, ugraph) target source =
550 let module C = Cic in
551 let module S = CicSubstitution in
552 let module M = CicMetaSubst in
553 let module HL = HelmLibraryObjects in
554 let module CR = CicReduction in
555 (* we assume that target is ground (does not contain metavariables): this
556 * should always be the case (I hope, at least) *)
557 let proof, (eq_ty, left, right), _, _ = target in
558 let eqproof, (ty, t1, t2), newmetas, args = source in
560 (* ALB: TODO check that ty and eq_ty are indeed equal... *)
564 match nonrec_kbo left right with
568 Printf.printf "????????? %s = %s" (CicPp.ppterm left)
569 (CicPp.ppterm right);
571 assert false (* again, for ground terms this shouldn't happen... *)
574 let metasenv' = newmetas @ metasenv in
577 (fun (t, s, m, ug) ->
578 nonrec_kbo (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
579 (beta_expand t1 ty where context metasenv' ugraph)
582 (fun (t, s, m, ug) ->
583 nonrec_kbo (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
584 (beta_expand t2 ty where context metasenv' ugraph)
586 (* let what, other = *)
587 (* if is_left then left, right *)
588 (* else right, left *)
590 let build_new what other eq_URI (t, s, m, ug) =
591 let newgoal, newgoalproof =
593 | C.Lambda (nn, ty, bo) ->
594 let bo' = S.subst (M.apply_subst s other) bo in
597 [C.MutInd (HL.Logic.eq_URI, 0, []);
599 if is_left then [bo'; S.lift 1 right] else [S.lift 1 left; bo'])
601 let t' = C.Lambda (nn, ty, bo'') in
602 S.subst (M.apply_subst s other) bo,
604 (C.Appl [C.Const (eq_URI, []); ty; what; t';
605 proof; other; eqproof])
609 if is_left then (eq_ty, newgoal, right)
610 else (eq_ty, left, newgoal)
612 (eqproof, equation, [], [])
614 let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
615 and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
620 let superposition_right newmeta (metasenv, context, ugraph) target source =
621 let module C = Cic in
622 let module S = CicSubstitution in
623 let module M = CicMetaSubst in
624 let module HL = HelmLibraryObjects in
625 let module CR = CicReduction in
626 let eqproof, (eq_ty, left, right), newmetas, args = target in
627 let eqp', (ty', t1, t2), newm', args' = source in
628 let maxmeta = ref newmeta in
630 (* TODO check if ty and ty' are equal... *)
631 assert (eq_ty = ty');
633 (* let ok term subst other other_eq_side ugraph = *)
634 (* match term with *)
635 (* | C.Lambda (nn, ty, bo) -> *)
636 (* let bo' = S.subst (M.apply_subst subst other) bo in *)
637 (* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
639 (* | _ -> assert false *)
641 let condition left right what other (t, s, m, ug) =
642 let subst = M.apply_subst s in
643 let cmp1 = nonrec_kbo (subst what) (subst other) in
644 let cmp2 = nonrec_kbo (subst left) (subst right) in
645 (* cmp1 = Gt && cmp2 = Gt *)
646 cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
647 (* && (ok t s other right ug) *)
649 let metasenv' = metasenv @ newmetas @ newm' in
650 let beta_expand = beta_expand ~metas_ok:false in
653 (condition left right t1 t2)
654 (beta_expand t1 eq_ty left context metasenv' ugraph)
657 (condition left right t2 t1)
658 (beta_expand t2 eq_ty left context metasenv' ugraph)
661 (condition right left t1 t2)
662 (beta_expand t1 eq_ty right context metasenv' ugraph)
665 (condition right left t2 t1)
666 (beta_expand t2 eq_ty right context metasenv' ugraph)
668 let newmetas = newmetas @ newm' in
669 let newargs = args @ args' in
670 let build_new what other is_left eq_URI (t, s, m, ug) =
671 (* let what, other = *)
672 (* if is_left then left, right *)
673 (* else right, left *)
675 let newterm, neweqproof =
677 | C.Lambda (nn, ty, bo) ->
678 let bo' = M.apply_subst s (S.subst other bo) in
681 [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
682 if is_left then [bo'; S.lift 1 right] else [S.lift 1 left; bo'])
684 let t' = C.Lambda (nn, ty, bo'') in
687 (C.Appl [C.Const (eq_URI, []); ty; what; t'; eqproof; other; eqp'])
690 let newmeta, newequality =
692 if is_left then (newterm, M.apply_subst s right)
693 else (M.apply_subst s left, newterm) in
695 (neweqproof, (eq_ty, left, right), newmetas, newargs)
700 let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
701 and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
702 and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
703 and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
705 | _, (_, left, right), _, _ ->
706 not (fst (CR.are_convertible context left right ugraph))
708 !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4))
712 let demodulation newmeta (metasenv, context, ugraph) target source =
713 let module C = Cic in
714 let module S = CicSubstitution in
715 let module M = CicMetaSubst in
716 let module HL = HelmLibraryObjects in
717 let module CR = CicReduction in
719 let proof, (eq_ty, left, right), metas, args = target
720 and proof', (ty, t1, t2), metas', args' = source in
724 let get_params step =
726 | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
727 | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
728 | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
729 | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
732 let rec demodulate newmeta step metasenv target =
733 let proof, (eq_ty, left, right), metas, args = target in
734 let is_left, what, other, eq_URI = get_params step in
736 (* "demodulate\ntarget: %s = %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
737 (* (CicPp.ppterm left) (CicPp.ppterm right) (CicPp.ppterm what) *)
738 (* (CicPp.ppterm other) (string_of_bool is_left); *)
739 (* Printf.printf "step: %d\n" step; *)
740 (* print_newline (); *)
741 let ok (t, s, m, ug) =
742 nonrec_kbo (M.apply_subst s what) (M.apply_subst s other) = Gt
746 (beta_expand ~metas_ok:false ~match_only:true
747 what ty left context (metasenv @ metas) ugraph)
751 if step = 0 then newmeta, target
752 else demodulate newmeta (step-1) metasenv target
753 | (t, s, m, ug)::_ ->
754 let newterm, newproof =
756 | C.Lambda (nn, ty, bo) ->
757 let bo' = M.apply_subst s (S.subst other bo) in
760 [C.MutInd (HL.Logic.eq_URI, 0, []);
762 if is_left then [bo'; S.lift 1 right]
763 else [S.lift 1 left; bo'])
765 let t' = C.Lambda (nn, ty, bo'') in
766 M.apply_subst s (S.subst other bo),
768 (C.Appl [C.Const (eq_URI, []); ty; what; t';
769 proof; other; proof'])
772 let newmeta, newtarget =
774 if is_left then (newterm, M.apply_subst s right)
775 else (M.apply_subst s left, newterm) in
776 let newmetasenv = metasenv @ metas in
777 let newargs = args @ args' in
779 (newproof, (eq_ty, left, right), newmetasenv, newargs)
781 let _, (_, left, right), _, _ = newtarget
782 and _, (_, oldleft, oldright), _, _ = target in
784 (* "demodulate, newtarget: %s = %s\ntarget was: %s = %s\n" *)
785 (* (CicPp.ppterm left) (CicPp.ppterm right) *)
786 (* (CicPp.ppterm oldleft) (CicPp.ppterm oldright); *)
787 (* print_newline (); *)
788 demodulate newmeta step metasenv newtarget
790 demodulate newmeta 3 (metasenv @ metas') target
795 let demodulation newmeta env target source =