4 let string_of_equality ?env =
8 | _, (ty, left, right), _, _ ->
9 Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty)
10 (CicPp.ppterm left) (CicPp.ppterm right)
12 | Some (_, context, _) -> (
13 let names = names_of_context context in
15 | _, (ty, left, right), _, _ ->
16 Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names)
17 (CicPp.pp left names) (CicPp.pp right names)
22 let rec metas_of_term = function
23 | Cic.Meta (i, c) -> [i]
26 | Cic.MutInd (_, _, ens)
27 | Cic.MutConstruct (_, _, _, ens) ->
28 List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
31 | Cic.Lambda (_, s, t)
32 | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
33 | Cic.Appl l -> List.flatten (List.map metas_of_term l)
34 | Cic.MutCase (uri, i, s, t, l) ->
35 (metas_of_term s) @ (metas_of_term t) @
36 (List.flatten (List.map metas_of_term l))
39 (List.map (fun (s, i, t1, t2) ->
40 (metas_of_term t1) @ (metas_of_term t2)) il)
41 | Cic.CoFix (i, il) ->
43 (List.map (fun (s, t1, t2) ->
44 (metas_of_term t1) @ (metas_of_term t2)) il)
49 exception NotMetaConvertible;;
51 let meta_convertibility_aux table t1 t2 =
56 (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
58 let rec aux ((table_l, table_r) as table) t1 t2 =
59 (* Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *)
60 (* (CicPp.ppterm t1) (CicPp.ppterm t2) *)
61 (* (print_table table_l) (print_table table_r); *)
63 | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
64 let m1_binding, table_l =
65 try List.assoc m1 table_l, table_l
66 with Not_found -> m2, (m1, m2)::table_l
67 and m2_binding, table_r =
68 try List.assoc m2 table_r, table_r
69 with Not_found -> m1, (m2, m1)::table_r
71 (* let m1_binding, m2_binding, table = *)
72 (* let m1b, table = *)
73 (* try List.assoc m1 table, table *)
74 (* with Not_found -> m2, (m1, m2)::table *)
76 (* let m2b, table = *)
77 (* try List.assoc m2 table, table *)
78 (* with Not_found -> m1, (m2, m1)::table *)
82 (* Printf.printf "table_l: %s\ntable_r: %s\n\n" *)
83 (* (print_table table_l) (print_table table_r); *)
84 if (m1_binding <> m2) || (m2_binding <> m1) then
85 raise NotMetaConvertible
91 | None, Some _ | Some _, None -> raise NotMetaConvertible
93 | Some t1, Some t2 -> (aux res t1 t2))
94 (table_l, table_r) tl1 tl2
95 with Invalid_argument _ ->
96 raise NotMetaConvertible
98 | C.Var (u1, ens1), C.Var (u2, ens2)
99 | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
100 aux_ens table ens1 ens2
101 | C.Cast (s1, t1), C.Cast (s2, t2)
102 | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
103 | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
104 | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
105 let table = aux table s1 s2 in
107 | C.Appl l1, C.Appl l2 -> (
108 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
109 with Invalid_argument _ -> raise NotMetaConvertible
111 | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
112 when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
113 | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
114 when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
115 aux_ens table ens1 ens2
116 | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
117 when (UriManager.eq u1 u2) && i1 = i2 ->
118 let table = aux table s1 s2 in
119 let table = aux table t1 t2 in (
120 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
121 with Invalid_argument _ -> raise NotMetaConvertible
123 | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
126 (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
127 if i1 <> i2 then raise NotMetaConvertible
129 let res = (aux res s1 s2) in aux res t1 t2)
131 with Invalid_argument _ -> raise NotMetaConvertible
133 | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
136 (fun res (n1, s1, t1) (n2, s2, t2) ->
137 let res = aux res s1 s2 in aux res t1 t2)
139 with Invalid_argument _ -> raise NotMetaConvertible
141 | t1, t2 when t1 = t2 -> table
142 | _, _ -> raise NotMetaConvertible
144 and aux_ens table ens1 ens2 =
145 let cmp (u1, t1) (u2, t2) =
146 compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
148 let ens1 = List.sort cmp ens1
149 and ens2 = List.sort cmp ens2 in
152 (fun res (u1, t1) (u2, t2) ->
153 if not (UriManager.eq u1 u2) then raise NotMetaConvertible
156 with Invalid_argument _ -> raise NotMetaConvertible
162 let meta_convertibility_eq eq1 eq2 =
163 let _, (ty, left, right), _, _ = eq1
164 and _, (ty', left', right'), _, _ = eq2 in
167 else if (left = left') && (right = right') then
169 else if (left = right') && (right = left') then
173 let table = meta_convertibility_aux ([], []) left left' in
174 let _ = meta_convertibility_aux table right right' in
176 with NotMetaConvertible ->
178 let table = meta_convertibility_aux ([], []) left right' in
179 let _ = meta_convertibility_aux table right left' in
181 with NotMetaConvertible ->
186 let meta_convertibility t1 t2 =
190 (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
196 let l, r = meta_convertibility_aux ([], []) t1 t2 in
197 (* Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *)
199 with NotMetaConvertible ->
204 let replace_metas (* context *) term =
205 let module C = Cic in
206 let rec aux = function
209 (* CicMkImplicit.identity_relocation_list_for_metavariable context *)
211 (* if c = irl then *)
212 (* C.Implicit (Some (`MetaIndex i)) *)
214 (* Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *)
215 (* (String.concat "\n" *)
217 (* (function None -> "" | Some t -> CicPp.ppterm t) c)); *)
220 C.Implicit (Some (`MetaInfo (i, c)))
221 | C.Var (u, ens) -> C.Var (u, aux_ens ens)
222 | C.Const (u, ens) -> C.Const (u, aux_ens ens)
223 | C.Cast (s, t) -> C.Cast (aux s, aux t)
224 | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
225 | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
226 | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
227 | C.Appl l -> C.Appl (List.map aux l)
228 | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
229 | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
230 | C.MutCase (uri, i, s, t, l) ->
231 C.MutCase (uri, i, aux s, aux t, List.map aux l)
234 List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
238 List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
242 List.map (fun (u, t) -> (u, aux t)) ens
248 let restore_metas (* context *) term =
249 let module C = Cic in
250 let rec aux = function
251 | C.Implicit (Some (`MetaInfo (i, c))) ->
253 (* CicMkImplicit.identity_relocation_list_for_metavariable context *)
256 (* let local_context:(C.term option) list = *)
257 (* Marshal.from_string mc 0 *)
259 (* C.Meta (i, local_context) *)
261 | C.Var (u, ens) -> C.Var (u, aux_ens ens)
262 | C.Const (u, ens) -> C.Const (u, aux_ens ens)
263 | C.Cast (s, t) -> C.Cast (aux s, aux t)
264 | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
265 | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
266 | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
267 | C.Appl l -> C.Appl (List.map aux l)
268 | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
269 | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
270 | C.MutCase (uri, i, s, t, l) ->
271 C.MutCase (uri, i, aux s, aux t, List.map aux l)
274 List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
278 List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
282 List.map (fun (u, t) -> (u, aux t)) ens
288 let rec restore_subst (* context *) subst =
290 (fun (i, (c, t, ty)) ->
291 i, (c, restore_metas (* context *) t, ty))
296 exception MatchingFailure;;
298 let matching metasenv context t1 t2 ugraph =
300 let subst, metasenv, ugraph =
301 CicUnification.fo_unif metasenv context t1 t2 ugraph
303 let t' = CicMetaSubst.apply_subst subst t1 in
304 if not (meta_convertibility t1 t') then
305 raise MatchingFailure
307 let metas = metas_of_term t1 in
308 let fix_subst = function
309 | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
310 (j, (c, Cic.Meta (i, lc), ty))
313 let subst = List.map fix_subst subst in
314 subst, metasenv, ugraph
316 raise MatchingFailure
320 let beta_expand ?(metas_ok=true) ?(match_only=false)
321 what type_of_what where context metasenv ugraph =
322 let module S = CicSubstitution in
323 let module C = Cic in
325 let print_info = false in
328 (* let names = names_of_context context in *)
329 (* Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
330 (* (CicPp.pp what names) (CicPp.ppterm what) *)
331 (* (CicPp.pp where names) (CicPp.ppterm where); *)
332 (* print_newline (); *)
336 ((list of all possible beta expansions, subst, metasenv, ugraph),
339 let rec aux lift_amount term context metasenv subst ugraph =
340 (* Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
341 let res, lifted_term =
344 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
346 | C.Var (uri, exp_named_subst) ->
347 let ens', lifted_ens =
348 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
352 (fun (e, s, m, ug) ->
353 (C.Var (uri, e), s, m, ug)) ens'
355 expansions, C.Var (uri, lifted_ens)
360 (fun arg (res, lifted_tl) ->
363 let arg_res, lifted_arg =
364 aux lift_amount arg context metasenv subst ugraph in
367 (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
372 (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
374 (Some lifted_arg)::lifted_tl)
377 (fun (r, s, m, ug) -> None::r, s, m, ug)
384 (fun (l, s, m, ug) ->
385 (C.Meta (i, l), s, m, ug)) l'
387 e, C.Meta (i, lifted_l)
390 | C.Implicit _ as t -> [], t
394 aux lift_amount s context metasenv subst ugraph in
396 aux lift_amount t context metasenv subst ugraph
400 (fun (t, s, m, ug) ->
401 C.Cast (t, lifted_t), s, m, ug) l1 in
404 (fun (t, s, m, ug) ->
405 C.Cast (lifted_s, t), s, m, ug) l2 in
406 l1'@l2', C.Cast (lifted_s, lifted_t)
408 | C.Prod (nn, s, t) ->
410 aux lift_amount s context metasenv subst ugraph in
412 aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
413 metasenv subst ugraph
417 (fun (t, s, m, ug) ->
418 C.Prod (nn, t, lifted_t), s, m, ug) l1 in
421 (fun (t, s, m, ug) ->
422 C.Prod (nn, lifted_s, t), s, m, ug) l2 in
423 l1'@l2', C.Prod (nn, lifted_s, lifted_t)
425 | C.Lambda (nn, s, t) ->
427 aux lift_amount s context metasenv subst ugraph in
429 aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
430 metasenv subst ugraph
434 (fun (t, s, m, ug) ->
435 C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
438 (fun (t, s, m, ug) ->
439 C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
440 l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
442 | C.LetIn (nn, s, t) ->
444 aux lift_amount s context metasenv subst ugraph in
446 aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
447 metasenv subst ugraph
451 (fun (t, s, m, ug) ->
452 C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
455 (fun (t, s, m, ug) ->
456 C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
457 l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
461 aux_list lift_amount l context metasenv subst ugraph
463 (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
466 | C.Const (uri, exp_named_subst) ->
467 let ens', lifted_ens =
468 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
472 (fun (e, s, m, ug) ->
473 (C.Const (uri, e), s, m, ug)) ens'
475 (expansions, C.Const (uri, lifted_ens))
477 | C.MutInd (uri, i ,exp_named_subst) ->
478 let ens', lifted_ens =
479 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
483 (fun (e, s, m, ug) ->
484 (C.MutInd (uri, i, e), s, m, ug)) ens'
486 (expansions, C.MutInd (uri, i, lifted_ens))
488 | C.MutConstruct (uri, i, j, exp_named_subst) ->
489 let ens', lifted_ens =
490 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
494 (fun (e, s, m, ug) ->
495 (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
497 (expansions, C.MutConstruct (uri, i, j, lifted_ens))
499 | C.MutCase (sp, i, outt, t, pl) ->
500 let pl_res, lifted_pl =
501 aux_list lift_amount pl context metasenv subst ugraph
503 let l1, lifted_outt =
504 aux lift_amount outt context metasenv subst ugraph in
506 aux lift_amount t context metasenv subst ugraph in
510 (fun (outt, s, m, ug) ->
511 C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
514 (fun (t, s, m, ug) ->
515 C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
518 (fun (pl, s, m, ug) ->
519 C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
521 (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
524 let len = List.length fl in
527 (fun (nm, idx, ty, bo) (res, lifted_tl) ->
528 let lifted_ty = S.lift lift_amount ty in
529 let bo_res, lifted_bo =
530 aux (lift_amount+len) bo context metasenv subst ugraph in
533 (fun (a, s, m, ug) ->
534 (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
539 (fun (r, s, m, ug) ->
540 (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
541 (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
545 (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
546 C.Fix (i, lifted_fl))
549 let len = List.length fl in
552 (fun (nm, ty, bo) (res, lifted_tl) ->
553 let lifted_ty = S.lift lift_amount ty in
554 let bo_res, lifted_bo =
555 aux (lift_amount+len) bo context metasenv subst ugraph in
558 (fun (a, s, m, ug) ->
559 (nm, lifted_ty, a)::lifted_tl, s, m, ug)
564 (fun (r, s, m, ug) ->
565 (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
566 (nm, lifted_ty, lifted_bo)::lifted_tl)
570 (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
571 C.CoFix (i, lifted_fl))
575 | C.Meta _ when (not metas_ok) ->
579 (* if match_only then replace_metas context term *)
583 let subst', metasenv', ugraph' =
584 (* Printf.printf "provo a unificare %s e %s\n" *)
585 (* (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
587 matching metasenv context term (S.lift lift_amount what)ugraph
589 CicUnification.fo_unif metasenv context
590 (S.lift lift_amount what) term ugraph
592 (* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
593 (* (CicPp.ppterm (S.lift lift_amount what)); *)
594 (* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
595 (* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
596 (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
597 (* if match_only then *)
598 (* let t' = CicMetaSubst.apply_subst subst' term in *)
599 (* if not (meta_convertibility term t') then ( *)
600 (* res, lifted_term *)
602 (* let metas = metas_of_term term in *)
603 (* let fix_subst = function *)
604 (* | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
605 (* (j, (c, C.Meta (i, lc), ty)) *)
608 (* let subst' = List.map fix_subst subst' in *)
609 (* ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
613 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
617 print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e));
621 (* Printf.printf "exit aux\n"; *)
624 and aux_list lift_amount l context metasenv subst ugraph =
626 (fun arg (res, lifted_tl) ->
627 let arg_res, lifted_arg =
628 aux lift_amount arg context metasenv subst ugraph in
630 (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
633 (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
634 lifted_arg::lifted_tl)
637 and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
639 (fun (u, arg) (res, lifted_tl) ->
640 let arg_res, lifted_arg =
641 aux lift_amount arg context metasenv subst ugraph in
644 (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
646 (l1 @ (List.map (fun (r, s, m, ug) ->
647 (u, lifted_arg)::r, s, m, ug) res),
648 (u, lifted_arg)::lifted_tl)
649 ) exp_named_subst ([], [])
654 (* if match_only then replace_metas (\* context *\) where *)
658 Printf.printf "searching %s inside %s\n"
659 (CicPp.ppterm what) (CicPp.ppterm where);
661 aux 0 where context metasenv [] ugraph
664 (* if match_only then *)
665 (* (fun (term, subst, metasenv, ugraph) -> *)
667 (* C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
668 (* and subst = restore_subst subst in *)
669 (* (term', subst, metasenv, ugraph)) *)
671 (fun (term, subst, metasenv, ugraph) ->
672 let term' = C.Lambda (C.Anonymous, type_of_what, term) in
673 (term', subst, metasenv, ugraph))
675 List.map mapfun expansions
680 Cic.term * (* proof *)
681 (Cic.term * (* type *)
682 Cic.term * (* left side *)
683 Cic.term) * (* right side *)
684 Cic.metasenv * (* environment for metas *)
685 Cic.term list (* arguments *)
689 let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
690 let module C = Cic in
691 let module S = CicSubstitution in
692 let module T = CicTypeChecker in
693 let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
694 let rec aux index newmeta = function
696 | (Some (_, C.Decl (term)))::tl ->
697 let do_find context term =
699 | C.Prod (name, s, t) ->
700 (* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
701 let (head, newmetas, args, _) =
702 PrimitiveTactics.new_metasenv_for_apply newmeta proof
703 context (S.lift index term)
709 | C.Meta (i, _) -> (max maxm i)
714 if List.length args = 0 then
717 C.Appl ((C.Rel index)::args)
720 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
721 Printf.printf "OK: %s\n" (CicPp.ppterm term);
722 Some (p, (ty, t1, t2), newmetas, args), (newmeta+1)
725 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
727 (ty, S.lift index t1, S.lift index t2), [], []), (newmeta+1)
730 match do_find context term with
732 let tl, newmeta' = (aux (index+1) newmeta tl) in
733 p::tl, max newmeta newmeta'
735 aux (index+1) newmeta tl
738 aux (index+1) newmeta tl
740 aux 1 newmeta context
744 let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) =
745 let table = Hashtbl.create (List.length args) in
748 (fun t (newargs, index) ->
751 Hashtbl.add table i index;
752 ((Cic.Meta (index, l))::newargs, index+1)
757 ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
762 (fun (i, context, term) menv ->
764 let index = Hashtbl.find table i in
765 (index, context, term)::menv
767 (i, context, term)::menv)
772 and right = repl right in
773 let metas = (metas_of_term left) @ (metas_of_term right) in
774 let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv'
777 (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
779 (newmeta + (List.length newargs) + 1,
780 (repl proof, (ty, left, right), menv', newargs))
784 exception TermIsNotAnEquality;;
786 let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
787 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
788 (proof, (ty, t1, t2), [], [])
790 raise TermIsNotAnEquality
794 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
797 let superposition_left (metasenv, context, ugraph) target source =
798 let module C = Cic in
799 let module S = CicSubstitution in
800 let module M = CicMetaSubst in
801 let module HL = HelmLibraryObjects in
802 let module CR = CicReduction in
803 (* we assume that target is ground (does not contain metavariables): this
804 * should always be the case (I hope, at least) *)
805 let proof, (eq_ty, left, right), _, _ = target in
806 let eqproof, (ty, t1, t2), newmetas, args = source in
808 let compare_terms = !Utils.compare_terms in
814 match compare_terms left right with
818 Printf.printf "????????? %s = %s" (CicPp.ppterm left)
819 (CicPp.ppterm right);
821 assert false (* again, for ground terms this shouldn't happen... *)
824 let metasenv' = newmetas @ metasenv in
825 let result = compare_terms t1 t2 in
828 | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
829 | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
833 (fun (t, s, m, ug) ->
834 compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
835 (beta_expand t1 ty where context metasenv' ugraph)
838 (fun (t, s, m, ug) ->
839 compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
840 (beta_expand t2 ty where context metasenv' ugraph)
844 (* let what, other = *)
845 (* if is_left then left, right *)
846 (* else right, left *)
848 let build_new what other eq_URI (t, s, m, ug) =
849 let newgoal, newgoalproof =
851 | C.Lambda (nn, ty, bo) ->
852 let bo' = S.subst (M.apply_subst s other) bo in
855 [C.MutInd (HL.Logic.eq_URI, 0, []);
857 if is_left then [bo'; S.lift 1 right]
858 else [S.lift 1 left; bo'])
860 let t' = C.Lambda (nn, ty, bo'') in
861 S.subst (M.apply_subst s other) bo,
863 (C.Appl [C.Const (eq_URI, []); ty; what; t';
864 proof; other; eqproof])
868 if is_left then (eq_ty, newgoal, right)
869 else (eq_ty, left, newgoal)
871 (eqproof, equation, [], [])
873 let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
874 and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
879 let superposition_right newmeta (metasenv, context, ugraph) target source =
880 let module C = Cic in
881 let module S = CicSubstitution in
882 let module M = CicMetaSubst in
883 let module HL = HelmLibraryObjects in
884 let module CR = CicReduction in
885 let eqproof, (eq_ty, left, right), newmetas, args = target in
886 let eqp', (ty', t1, t2), newm', args' = source in
887 let maxmeta = ref newmeta in
889 let compare_terms = !Utils.compare_terms in
894 (* let ok term subst other other_eq_side ugraph = *)
895 (* match term with *)
896 (* | C.Lambda (nn, ty, bo) -> *)
897 (* let bo' = S.subst (M.apply_subst subst other) bo in *)
898 (* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
900 (* | _ -> assert false *)
902 let condition left right what other (t, s, m, ug) =
903 let subst = M.apply_subst s in
904 let cmp1 = compare_terms (subst what) (subst other) in
905 let cmp2 = compare_terms (subst left) (subst right) in
906 (* cmp1 = Gt && cmp2 = Gt *)
907 cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
908 (* && (ok t s other right ug) *)
910 let metasenv' = metasenv @ newmetas @ newm' in
911 let beta_expand = beta_expand ~metas_ok:false in
912 let cmp1 = compare_terms left right
913 and cmp2 = compare_terms t1 t2 in
914 let res1, res2, res3, res4 =
918 (beta_expand s eq_ty l context metasenv' ugraph)
920 match cmp1, cmp2 with
922 (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
924 [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
926 [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
928 [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
930 let res1 = res left right t1 t2
931 and res2 = res left right t2 t1 in
934 let res3 = res right left t1 t2
935 and res4 = res right left t2 t1 in
938 let res1 = res left right t1 t2
939 and res3 = res right left t1 t2 in
942 let res2 = res left right t2 t1
943 and res4 = res right left t2 t1 in
946 let res1 = res left right t1 t2
947 and res2 = res left right t2 t1
948 and res3 = res right left t1 t2
949 and res4 = res right left t2 t1 in
950 res1, res2, res3, res4
952 let newmetas = newmetas @ newm' in
953 let newargs = args @ args' in
954 let build_new what other is_left eq_URI (t, s, m, ug) =
955 (* let what, other = *)
956 (* if is_left then left, right *)
957 (* else right, left *)
959 let newterm, neweqproof =
961 | C.Lambda (nn, ty, bo) ->
962 let bo' = M.apply_subst s (S.subst other bo) in
965 [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
966 if is_left then [bo'; S.lift 1 right]
967 else [S.lift 1 left; bo'])
969 let t' = C.Lambda (nn, ty, bo'') in
972 (C.Appl [C.Const (eq_URI, []); ty; what; t';
973 eqproof; other; eqp'])
976 let newmeta, newequality =
978 if is_left then (newterm, M.apply_subst s right)
979 else (M.apply_subst s left, newterm) in
981 (neweqproof, (eq_ty, left, right), newmetas, newargs)
986 let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
987 and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
988 and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
989 and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
991 | _, (_, left, right), _, _ ->
992 not (fst (CR.are_convertible context left right ugraph))
994 !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4))
998 let is_identity ((_, context, ugraph) as env) = function
999 | ((_, (ty, left, right), _, _) as equality) ->
1002 (fst (CicReduction.are_convertible context left right ugraph)))
1005 (* Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
1006 (* print_newline (); *)
1012 let demodulation newmeta (metasenv, context, ugraph) target source =
1013 let module C = Cic in
1014 let module S = CicSubstitution in
1015 let module M = CicMetaSubst in
1016 let module HL = HelmLibraryObjects in
1017 let module CR = CicReduction in
1019 let proof, (eq_ty, left, right), metas, args = target
1020 and proof', (ty, t1, t2), metas', args' = source in
1022 let compare_terms = !Utils.compare_terms in
1027 let first_step, get_params =
1028 match compare_terms t1 t2 with
1029 | Gt -> 1, (function
1030 | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
1031 | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
1032 | _ -> assert false)
1033 | Lt -> 1, (function
1034 | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1035 | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1036 | _ -> assert false)
1038 let first_step = 3 in
1039 let get_params step =
1041 | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
1042 | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
1043 | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1044 | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1047 first_step, get_params
1049 let rec demodulate newmeta step metasenv target =
1050 let proof, (eq_ty, left, right), metas, args = target in
1051 let is_left, what, other, eq_URI = get_params step in
1053 let env = metasenv, context, ugraph in
1054 let names = names_of_context context in
1056 (* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1057 (* (string_of_equality ~env target) (CicPp.pp what names) *)
1058 (* (CicPp.pp other names) (string_of_bool is_left); *)
1059 (* Printf.printf "step: %d" step; *)
1060 (* print_newline (); *)
1062 let ok (t, s, m, ug) =
1063 compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
1066 let r = (beta_expand ~metas_ok:false ~match_only:true
1067 what ty (if is_left then left else right)
1068 context (metasenv @ metas) ugraph)
1070 (* let m' = metas_of_term what *)
1071 (* and m'' = metas_of_term (if is_left then left else right) in *)
1072 (* if (List.mem 527 m'') && (List.mem 6 m') then ( *)
1074 (* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1075 (* (string_of_equality ~env target) (CicPp.pp what names) *)
1076 (* (CicPp.pp other names) (string_of_bool is_left); *)
1077 (* Printf.printf "step: %d" step; *)
1078 (* print_newline (); *)
1079 (* print_endline "res:"; *)
1080 (* List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
1081 (* print_newline (); *)
1082 (* Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
1083 (* print_newline (); *)
1089 if step = 0 then newmeta, target
1090 else demodulate newmeta (step-1) metasenv target
1091 | (t, s, m, ug)::_ ->
1092 let newterm, newproof =
1094 | C.Lambda (nn, ty, bo) ->
1095 (* let bo' = M.apply_subst s (S.subst other bo) in *)
1096 let bo' = S.subst (M.apply_subst s other) bo in
1099 [C.MutInd (HL.Logic.eq_URI, 0, []);
1101 if is_left then [bo'; S.lift 1 right]
1102 else [S.lift 1 left; bo'])
1104 let t' = C.Lambda (nn, ty, bo'') in
1105 (* M.apply_subst s (S.subst other bo), *)
1108 (C.Appl [C.Const (eq_URI, []); ty; what; t';
1109 proof; other; proof'])
1112 let newmeta, newtarget =
1114 (* if is_left then (newterm, M.apply_subst s right) *)
1115 (* else (M.apply_subst s left, newterm) in *)
1116 if is_left then newterm, right
1119 (* let newmetasenv = metasenv @ metas in *)
1120 (* let newargs = args @ args' in *)
1121 (* fix_metas newmeta *)
1122 (* (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
1123 let m = (metas_of_term left) @ (metas_of_term right) in
1124 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
1127 (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
1130 newmeta, (newproof, (eq_ty, left, right), newmetasenv, newargs)
1133 (* "demodulate, newtarget: %s\ntarget was: %s\n" *)
1134 (* (string_of_equality ~env newtarget) *)
1135 (* (string_of_equality ~env target); *)
1136 (* (\* let _, _, newm, newa = newtarget in *\) *)
1137 (* (\* Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
1138 (* (\* (print_metasenv newm) *\) *)
1139 (* (\* (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
1140 (* print_newline (); *)
1141 if is_identity env newtarget then
1144 demodulate newmeta first_step metasenv newtarget
1146 demodulate newmeta first_step (metasenv @ metas') target
1151 let demodulation newmeta env target source =
1157 let subsumption env target source =
1158 let _, (ty, tl, tr), tmetas, _ = target
1159 and _, (ty', sl, sr), smetas, _ = source in
1163 let metasenv, context, ugraph = env in
1164 let metasenv = metasenv @ tmetas @ smetas in
1165 let names = names_of_context context in
1166 let samesubst subst subst' =
1167 (* Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
1168 (* (print_subst subst) (print_subst subst'); *)
1169 (* print_newline (); *)
1170 let tbl = Hashtbl.create (List.length subst) in
1171 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
1173 (fun (m, (c, t1, t2)) ->
1175 let c', t1', t2' = Hashtbl.find tbl m in
1176 if (c = c') && (t1 = t1') && (t2 = t2') then true
1182 let subsaux left right left' right' =
1184 let subst, menv, ug = matching metasenv context left left' ugraph
1185 and subst', menv', ug' = matching metasenv context right right' ugraph
1187 (* Printf.printf "left = right: %s = %s\n" *)
1188 (* (CicPp.pp left names) (CicPp.pp right names); *)
1189 (* Printf.printf "left' = right': %s = %s\n" *)
1190 (* (CicPp.pp left' names) (CicPp.pp right' names); *)
1191 samesubst subst subst'
1193 (* print_endline (Printexc.to_string e); *)
1197 if subsaux tl tr sl sr then true
1198 else subsaux tl tr sr sl
1201 Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
1202 (string_of_equality ~env target) (string_of_equality ~env source);