8 Cic.term * (* left side *)
9 Cic.term * (* right side *)
10 Utils.comparison) * (* ordering *)
11 Cic.metasenv * (* environment for metas *)
12 Cic.term list (* arguments *)
16 | BasicProof of Cic.term
18 Cic.substitution * UriManager.uri *
19 (Cic.name * Cic.term) * Cic.term *
20 (* name, ty, eq_ty, left, right *)
21 (* (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * *)
22 (Utils.pos * equality) * proof
23 | ProofGoalBlock of proof * proof (* equality *)
24 | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof
25 | SubProof of Cic.term * int * proof
29 let string_of_equality ?env =
33 | w, _, (ty, left, right, o), _, _ ->
34 Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty)
35 (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
37 | Some (_, context, _) -> (
38 let names = names_of_context context in
40 | w, _, (ty, left, right, o), _, _ ->
41 Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names)
42 (CicPp.pp left names) (string_of_comparison o)
43 (CicPp.pp right names)
48 let build_proof_term proof =
49 let rec do_build_proof proof =
52 Printf.fprintf stderr "WARNING: no proof!\n";
54 | BasicProof term -> term
55 | ProofGoalBlock (proofbit, proof) ->
56 print_endline "found ProofGoalBlock, going up...";
57 do_build_goal_proof proofbit proof
58 | ProofSymBlock (ens, proof) ->
59 let proof = do_build_proof proof in
61 Cic.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens); (* symmetry *)
64 | ProofBlock (subst, eq_URI, (name, ty), bo(* t' *), (pos, eq), eqproof) ->
65 let t' = Cic.Lambda (name, ty, bo) in
67 let _, proof', _, _, _ = eq in
70 let eqproof = do_build_proof eqproof in
71 let _, _, (ty, what, other, _), menv', args' = eq in
73 if pos = Utils.Left then what, other else other, what
75 CicMetaSubst.apply_subst subst
76 (Cic.Appl [Cic.Const (eq_URI, []); ty;
77 what; t'; eqproof; other; proof'])
78 | SubProof (term, meta_index, proof) ->
79 let proof = do_build_proof proof in
81 | Cic.Meta (j, _) -> i = j
84 ProofEngineReduction.replace
85 ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
87 and do_build_goal_proof proofbit proof =
88 (* match proofbit with *)
89 (* | BasicProof _ -> do_build_proof proof *)
92 | ProofGoalBlock (pb, p(* eq *)) ->
93 do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p(* eq *)))
94 (* let _, proof, _, _, _ = eq in *)
95 (* let newproof = replace_proof proofbit proof in *)
96 (* do_build_proof newproof *)
98 (* | ProofBlock (subst, eq_URI, t', poseq, eqproof) -> *)
99 (* let eqproof' = replace_proof proofbit eqproof in *)
100 (* do_build_proof (ProofBlock (subst, eq_URI, t', poseq, eqproof')) *)
101 | _ -> do_build_proof (replace_proof proofbit proof) (* assert false *)
103 and replace_proof newproof = function
104 | ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof) ->
105 let eqproof' = replace_proof newproof eqproof in
106 ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof')
107 | ProofGoalBlock (pb, p(* equality *)) ->
108 let pb' = replace_proof newproof pb in
109 ProofGoalBlock (pb', p(* equality *))
110 (* let w, proof, t, menv, args = equality in *)
111 (* let proof' = replace_proof newproof proof in *)
112 (* ProofGoalBlock (pb, (w, proof', t, menv, args)) *)
113 | BasicProof _ -> newproof
114 | SubProof (term, meta_index, p) ->
115 SubProof (term, meta_index, replace_proof newproof p)
118 (* let _, proof, _, _, _ = equality in *)
123 let rec metas_of_term = function
124 | Cic.Meta (i, c) -> [i]
127 | Cic.MutInd (_, _, ens)
128 | Cic.MutConstruct (_, _, _, ens) ->
129 List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
132 | Cic.Lambda (_, s, t)
133 | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
134 | Cic.Appl l -> List.flatten (List.map metas_of_term l)
135 | Cic.MutCase (uri, i, s, t, l) ->
136 (metas_of_term s) @ (metas_of_term t) @
137 (List.flatten (List.map metas_of_term l))
140 (List.map (fun (s, i, t1, t2) ->
141 (metas_of_term t1) @ (metas_of_term t2)) il)
142 | Cic.CoFix (i, il) ->
144 (List.map (fun (s, t1, t2) ->
145 (metas_of_term t1) @ (metas_of_term t2)) il)
150 exception NotMetaConvertible;;
152 let meta_convertibility_aux table t1 t2 =
153 let module C = Cic in
157 (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
159 let rec aux ((table_l, table_r) as table) t1 t2 =
160 (* Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *)
161 (* (CicPp.ppterm t1) (CicPp.ppterm t2) *)
162 (* (print_table table_l) (print_table table_r); *)
164 | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
165 let m1_binding, table_l =
166 try List.assoc m1 table_l, table_l
167 with Not_found -> m2, (m1, m2)::table_l
168 and m2_binding, table_r =
169 try List.assoc m2 table_r, table_r
170 with Not_found -> m1, (m2, m1)::table_r
172 (* let m1_binding, m2_binding, table = *)
173 (* let m1b, table = *)
174 (* try List.assoc m1 table, table *)
175 (* with Not_found -> m2, (m1, m2)::table *)
177 (* let m2b, table = *)
178 (* try List.assoc m2 table, table *)
179 (* with Not_found -> m1, (m2, m1)::table *)
181 (* m1b, m2b, table *)
183 (* Printf.printf "table_l: %s\ntable_r: %s\n\n" *)
184 (* (print_table table_l) (print_table table_r); *)
185 if (m1_binding <> m2) || (m2_binding <> m1) then
186 raise NotMetaConvertible
192 | None, Some _ | Some _, None -> raise NotMetaConvertible
194 | Some t1, Some t2 -> (aux res t1 t2))
195 (table_l, table_r) tl1 tl2
196 with Invalid_argument _ ->
197 raise NotMetaConvertible
199 | C.Var (u1, ens1), C.Var (u2, ens2)
200 | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
201 aux_ens table ens1 ens2
202 | C.Cast (s1, t1), C.Cast (s2, t2)
203 | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
204 | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
205 | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
206 let table = aux table s1 s2 in
208 | C.Appl l1, C.Appl l2 -> (
209 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
210 with Invalid_argument _ -> raise NotMetaConvertible
212 | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
213 when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
214 | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
215 when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
216 aux_ens table ens1 ens2
217 | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
218 when (UriManager.eq u1 u2) && i1 = i2 ->
219 let table = aux table s1 s2 in
220 let table = aux table t1 t2 in (
221 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
222 with Invalid_argument _ -> raise NotMetaConvertible
224 | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
227 (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
228 if i1 <> i2 then raise NotMetaConvertible
230 let res = (aux res s1 s2) in aux res t1 t2)
232 with Invalid_argument _ -> raise NotMetaConvertible
234 | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
237 (fun res (n1, s1, t1) (n2, s2, t2) ->
238 let res = aux res s1 s2 in aux res t1 t2)
240 with Invalid_argument _ -> raise NotMetaConvertible
242 | t1, t2 when t1 = t2 -> table
243 | _, _ -> raise NotMetaConvertible
245 and aux_ens table ens1 ens2 =
246 let cmp (u1, t1) (u2, t2) =
247 compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
249 let ens1 = List.sort cmp ens1
250 and ens2 = List.sort cmp ens2 in
253 (fun res (u1, t1) (u2, t2) ->
254 if not (UriManager.eq u1 u2) then raise NotMetaConvertible
257 with Invalid_argument _ -> raise NotMetaConvertible
263 let meta_convertibility_eq eq1 eq2 =
264 let _, _, (ty, left, right, _), _, _ = eq1
265 and _, _, (ty', left', right', _), _, _ = eq2 in
268 else if (left = left') && (right = right') then
270 else if (left = right') && (right = left') then
274 let table = meta_convertibility_aux ([], []) left left' in
275 let _ = meta_convertibility_aux table right right' in
277 with NotMetaConvertible ->
279 let table = meta_convertibility_aux ([], []) left right' in
280 let _ = meta_convertibility_aux table right left' in
282 with NotMetaConvertible ->
287 let meta_convertibility t1 t2 =
291 (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
297 let l, r = meta_convertibility_aux ([], []) t1 t2 in
298 (* Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *)
300 with NotMetaConvertible ->
306 let replace_metas (* context *) term =
307 let module C = Cic in
308 let rec aux = function
311 (* CicMkImplicit.identity_relocation_list_for_metavariable context *)
313 (* if c = irl then *)
314 (* C.Implicit (Some (`MetaIndex i)) *)
316 (* Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *)
317 (* (String.concat "\n" *)
319 (* (function None -> "" | Some t -> CicPp.ppterm t) c)); *)
322 C.Implicit (Some (`MetaInfo (i, c)))
323 | C.Var (u, ens) -> C.Var (u, aux_ens ens)
324 | C.Const (u, ens) -> C.Const (u, aux_ens ens)
325 | C.Cast (s, t) -> C.Cast (aux s, aux t)
326 | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
327 | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
328 | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
329 | C.Appl l -> C.Appl (List.map aux l)
330 | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
331 | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
332 | C.MutCase (uri, i, s, t, l) ->
333 C.MutCase (uri, i, aux s, aux t, List.map aux l)
336 List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
340 List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
344 List.map (fun (u, t) -> (u, aux t)) ens
352 let restore_metas (* context *) term =
353 let module C = Cic in
354 let rec aux = function
355 | C.Implicit (Some (`MetaInfo (i, c))) ->
357 (* CicMkImplicit.identity_relocation_list_for_metavariable context *)
360 (* let local_context:(C.term option) list = *)
361 (* Marshal.from_string mc 0 *)
363 (* C.Meta (i, local_context) *)
365 | C.Var (u, ens) -> C.Var (u, aux_ens ens)
366 | C.Const (u, ens) -> C.Const (u, aux_ens ens)
367 | C.Cast (s, t) -> C.Cast (aux s, aux t)
368 | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
369 | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
370 | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
371 | C.Appl l -> C.Appl (List.map aux l)
372 | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
373 | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
374 | C.MutCase (uri, i, s, t, l) ->
375 C.MutCase (uri, i, aux s, aux t, List.map aux l)
378 List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
382 List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
386 List.map (fun (u, t) -> (u, aux t)) ens
393 let rec restore_subst (* context *) subst =
395 (fun (i, (c, t, ty)) ->
396 i, (c, restore_metas (* context *) t, ty))
402 let rec check_irl start = function
404 | None::tl -> check_irl (start+1) tl
405 | (Some (Cic.Rel x))::tl ->
406 if x = start then check_irl (start+1) tl else false
410 let rec is_simple_term = function
411 | Cic.Appl ((Cic.Meta _)::_) -> false
412 | Cic.Appl l -> List.for_all is_simple_term l
413 | Cic.Meta (i, l) -> check_irl 1 l
415 | Cic.Const _ -> true
416 | Cic.MutInd (_, _, []) -> true
417 | Cic.MutConstruct (_, _, _, []) -> true
422 let lookup_subst meta subst =
424 | Cic.Meta (i, _) -> (
425 try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
426 with Not_found -> meta
432 let unification_simple metasenv context t1 t2 ugraph =
433 let module C = Cic in
434 let module M = CicMetaSubst in
435 let module U = CicUnification in
436 let lookup = lookup_subst in
437 let rec occurs_check subst what where =
439 | t when what = t -> true
440 | C.Appl l -> List.exists (occurs_check subst what) l
442 let t = lookup where subst in
443 if t <> where then occurs_check subst what t else false
446 let rec unif subst menv s t =
447 let s = match s with C.Meta _ -> lookup s subst | _ -> s
448 and t = match t with C.Meta _ -> lookup t subst | _ -> t
451 | s, t when s = t -> subst, menv
452 | C.Meta (i, _), C.Meta (j, _) when i > j ->
454 | C.Meta _, t when occurs_check subst s t ->
456 (U.UnificationFailure
457 (U.failure_msg_of_string "Inference.unification.unif"))
458 | C.Meta (i, l), t -> (
460 let _, _, ty = CicUtil.lookup_meta i menv in
462 if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
465 let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
467 with CicUtil.Meta_not_found m ->
468 let names = names_of_context context in
471 (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
472 (CicPp.pp t1 names) (CicPp.pp t2 names)
473 (print_metasenv menv) (print_metasenv metasenv)));
476 | _, C.Meta _ -> unif subst menv t s
477 | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
478 raise (U.UnificationFailure
479 (U.failure_msg_of_string "Inference.unification.unif"))
480 | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
483 (fun (subst', menv) s t -> unif subst' menv s t)
484 (subst, menv) tls tlt
485 with Invalid_argument _ ->
486 raise (U.UnificationFailure
487 (U.failure_msg_of_string "Inference.unification.unif"))
490 raise (U.UnificationFailure
491 (U.failure_msg_of_string "Inference.unification.unif"))
493 let subst, menv = unif [] metasenv t1 t2 in
497 try let _ = List.find (fun (i, _) -> m = i) subst in false
498 with Not_found -> true)
501 List.rev subst, menv, ugraph
505 let unification metasenv context t1 t2 ugraph =
506 (* Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
507 let subst, menv, ug =
508 if not (is_simple_term t1) || not (is_simple_term t2) then (
511 (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
512 (CicPp.ppterm t1) (CicPp.ppterm t2)));
513 CicUnification.fo_unif metasenv context t1 t2 ugraph
515 unification_simple metasenv context t1 t2 ugraph
517 let rec fix_term = function
518 | (Cic.Meta (i, l) as t) ->
519 let t' = lookup_subst t subst in
520 if t <> t' then fix_term t' else t
521 | Cic.Appl l -> Cic.Appl (List.map fix_term l)
524 let rec fix_subst = function
526 | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
528 (* Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
529 (* print_endline "|"; *)
530 fix_subst subst, menv, ug
534 (* let unification = CicUnification.fo_unif;; *)
536 exception MatchingFailure;;
539 let matching_simple metasenv context t1 t2 ugraph =
540 let module C = Cic in
541 let module M = CicMetaSubst in
542 let module U = CicUnification in
543 let lookup meta subst =
546 try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
547 with Not_found -> meta
551 let rec do_match subst menv s t =
552 (* Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
553 (* (print_subst subst); *)
554 (* print_newline (); *)
555 (* let s = match s with C.Meta _ -> lookup s subst | _ -> s *)
556 (* let t = match t with C.Meta _ -> lookup t subst | _ -> t in *)
557 (* Printf.printf "after apply_subst: %s %s\n%s" *)
558 (* (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
559 (* print_newline (); *)
561 | s, t when s = t -> subst, menv
562 (* | C.Meta (i, _), C.Meta (j, _) when i > j -> *)
563 (* do_match subst menv t s *)
564 (* | C.Meta _, t when occurs_check subst s t -> *)
565 (* raise MatchingFailure *)
566 (* | s, C.Meta _ when occurs_check subst t s -> *)
567 (* raise MatchingFailure *)
568 | s, C.Meta (i, l) ->
569 let filter_menv i menv =
570 List.filter (fun (m, _, _) -> i <> m) menv
573 let value = lookup t subst in
575 (* | C.Meta (i', l') when Hashtbl.mem table i' -> *)
576 (* (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *)
577 | value when value = t ->
578 let _, _, ty = CicUtil.lookup_meta i menv in
579 (i, (context, s, ty))::subst, filter_menv i menv
580 | value when value <> s ->
581 raise MatchingFailure
582 | value -> do_match subst menv s value
585 (* else if value <> s then *)
586 (* raise MatchingFailure *)
588 (* if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst *)
591 (* let menv = List.filter (fun (m, _, _) -> i <> m) menv in *)
593 (* | _, C.Meta _ -> do_match subst menv t s *)
594 (* | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *)
595 (* raise MatchingFailure *)
596 | C.Appl ls, C.Appl lt -> (
599 (fun (subst, menv) s t -> do_match subst menv s t)
601 with Invalid_argument _ ->
602 (* print_endline (Printexc.to_string e); *)
603 (* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
604 (* print_newline (); *)
605 raise MatchingFailure
608 (* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
609 (* print_newline (); *)
610 raise MatchingFailure
612 let subst, menv = do_match [] metasenv t1 t2 in
613 (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
614 (* print_newline (); *)
619 let matching metasenv context t1 t2 ugraph =
620 (* if (is_simple_term t1) && (is_simple_term t2) then *)
621 (* let subst, menv, ug = *)
622 (* matching_simple metasenv context t1 t2 ugraph in *)
623 (* (\* Printf.printf "matching %s %s:\n%s\n" *\) *)
624 (* (\* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *)
625 (* (\* print_newline (); *\) *)
626 (* subst, menv, ug *)
629 (* (Printf.sprintf "matching %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2)); *)
630 (* print_newline (); *)
632 let subst, metasenv, ugraph =
633 (* CicUnification.fo_unif metasenv context t1 t2 ugraph *)
634 unification metasenv context t1 t2 ugraph
636 let t' = CicMetaSubst.apply_subst subst t1 in
637 if not (meta_convertibility t1 t') then
638 raise MatchingFailure
640 let metas = metas_of_term t1 in
641 let fix_subst = function
642 | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
643 (j, (c, Cic.Meta (i, lc), ty))
646 let subst = List.map fix_subst subst in
648 (* Printf.printf "matching %s %s:\n%s\n" *)
649 (* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *)
650 (* print_newline (); *)
652 subst, metasenv, ugraph
654 | CicUnification.UnificationFailure _
655 | CicUnification.Uncertain _ ->
656 (* Printf.printf "failed to match %s %s\n" *)
657 (* (CicPp.ppterm t1) (CicPp.ppterm t2); *)
658 (* print_endline (Printexc.to_string e); *)
659 raise MatchingFailure
663 (* let profile = CicUtil.profile "Inference.matching" in *)
664 (* (fun metasenv context t1 t2 ugraph -> *)
665 (* profile (matching metasenv context t1 t2) ugraph) *)
669 let beta_expand ?(metas_ok=true) ?(match_only=false)
670 what type_of_what where context metasenv ugraph =
671 let module S = CicSubstitution in
672 let module C = Cic in
675 (* let names = names_of_context context in *)
676 (* Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
677 (* (CicPp.pp what names) (CicPp.ppterm what) *)
678 (* (CicPp.pp where names) (CicPp.ppterm where); *)
679 (* print_newline (); *)
683 ((list of all possible beta expansions, subst, metasenv, ugraph),
686 let rec aux lift_amount term context metasenv subst ugraph =
687 (* Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
688 let res, lifted_term =
691 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
693 | C.Var (uri, exp_named_subst) ->
694 let ens', lifted_ens =
695 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
699 (fun (e, s, m, ug) ->
700 (C.Var (uri, e), s, m, ug)) ens'
702 expansions, C.Var (uri, lifted_ens)
707 (fun arg (res, lifted_tl) ->
710 let arg_res, lifted_arg =
711 aux lift_amount arg context metasenv subst ugraph in
714 (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
719 (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
721 (Some lifted_arg)::lifted_tl)
724 (fun (r, s, m, ug) -> None::r, s, m, ug)
731 (fun (l, s, m, ug) ->
732 (C.Meta (i, l), s, m, ug)) l'
734 e, C.Meta (i, lifted_l)
737 | C.Implicit _ as t -> [], t
741 aux lift_amount s context metasenv subst ugraph in
743 aux lift_amount t context metasenv subst ugraph
747 (fun (t, s, m, ug) ->
748 C.Cast (t, lifted_t), s, m, ug) l1 in
751 (fun (t, s, m, ug) ->
752 C.Cast (lifted_s, t), s, m, ug) l2 in
753 l1'@l2', C.Cast (lifted_s, lifted_t)
755 | C.Prod (nn, s, t) ->
757 aux lift_amount s context metasenv subst ugraph in
759 aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
760 metasenv subst ugraph
764 (fun (t, s, m, ug) ->
765 C.Prod (nn, t, lifted_t), s, m, ug) l1 in
768 (fun (t, s, m, ug) ->
769 C.Prod (nn, lifted_s, t), s, m, ug) l2 in
770 l1'@l2', C.Prod (nn, lifted_s, lifted_t)
772 | C.Lambda (nn, s, t) ->
774 aux lift_amount s context metasenv subst ugraph in
776 aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
777 metasenv subst ugraph
781 (fun (t, s, m, ug) ->
782 C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
785 (fun (t, s, m, ug) ->
786 C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
787 l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
789 | C.LetIn (nn, s, t) ->
791 aux lift_amount s context metasenv subst ugraph in
793 aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
794 metasenv subst ugraph
798 (fun (t, s, m, ug) ->
799 C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
802 (fun (t, s, m, ug) ->
803 C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
804 l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
808 aux_list lift_amount l context metasenv subst ugraph
810 (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
813 | C.Const (uri, exp_named_subst) ->
814 let ens', lifted_ens =
815 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
819 (fun (e, s, m, ug) ->
820 (C.Const (uri, e), s, m, ug)) ens'
822 (expansions, C.Const (uri, lifted_ens))
824 | C.MutInd (uri, i ,exp_named_subst) ->
825 let ens', lifted_ens =
826 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
830 (fun (e, s, m, ug) ->
831 (C.MutInd (uri, i, e), s, m, ug)) ens'
833 (expansions, C.MutInd (uri, i, lifted_ens))
835 | C.MutConstruct (uri, i, j, exp_named_subst) ->
836 let ens', lifted_ens =
837 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
841 (fun (e, s, m, ug) ->
842 (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
844 (expansions, C.MutConstruct (uri, i, j, lifted_ens))
846 | C.MutCase (sp, i, outt, t, pl) ->
847 let pl_res, lifted_pl =
848 aux_list lift_amount pl context metasenv subst ugraph
850 let l1, lifted_outt =
851 aux lift_amount outt context metasenv subst ugraph in
853 aux lift_amount t context metasenv subst ugraph in
857 (fun (outt, s, m, ug) ->
858 C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
861 (fun (t, s, m, ug) ->
862 C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
865 (fun (pl, s, m, ug) ->
866 C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
868 (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
871 let len = List.length fl in
874 (fun (nm, idx, ty, bo) (res, lifted_tl) ->
875 let lifted_ty = S.lift lift_amount ty in
876 let bo_res, lifted_bo =
877 aux (lift_amount+len) bo context metasenv subst ugraph in
880 (fun (a, s, m, ug) ->
881 (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
886 (fun (r, s, m, ug) ->
887 (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
888 (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
892 (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
893 C.Fix (i, lifted_fl))
896 let len = List.length fl in
899 (fun (nm, ty, bo) (res, lifted_tl) ->
900 let lifted_ty = S.lift lift_amount ty in
901 let bo_res, lifted_bo =
902 aux (lift_amount+len) bo context metasenv subst ugraph in
905 (fun (a, s, m, ug) ->
906 (nm, lifted_ty, a)::lifted_tl, s, m, ug)
911 (fun (r, s, m, ug) ->
912 (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
913 (nm, lifted_ty, lifted_bo)::lifted_tl)
917 (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
918 C.CoFix (i, lifted_fl))
922 | C.Meta _ when (not metas_ok) ->
926 (* if match_only then replace_metas context term *)
930 let subst', metasenv', ugraph' =
931 (* Printf.printf "provo a unificare %s e %s\n" *)
932 (* (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
934 matching metasenv context term (S.lift lift_amount what) ugraph
936 CicUnification.fo_unif metasenv context
937 (S.lift lift_amount what) term ugraph
939 (* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
940 (* (CicPp.ppterm (S.lift lift_amount what)); *)
941 (* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
942 (* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
943 (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
944 (* if match_only then *)
945 (* let t' = CicMetaSubst.apply_subst subst' term in *)
946 (* if not (meta_convertibility term t') then ( *)
947 (* res, lifted_term *)
949 (* let metas = metas_of_term term in *)
950 (* let fix_subst = function *)
951 (* | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
952 (* (j, (c, C.Meta (i, lc), ty)) *)
955 (* let subst' = List.map fix_subst subst' in *)
956 (* ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
960 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
964 | CicUnification.UnificationFailure _
965 | CicUnification.Uncertain _ ->
968 (* Printf.printf "exit aux\n"; *)
971 and aux_list lift_amount l context metasenv subst ugraph =
973 (fun arg (res, lifted_tl) ->
974 let arg_res, lifted_arg =
975 aux lift_amount arg context metasenv subst ugraph in
977 (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
980 (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
981 lifted_arg::lifted_tl)
984 and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
986 (fun (u, arg) (res, lifted_tl) ->
987 let arg_res, lifted_arg =
988 aux lift_amount arg context metasenv subst ugraph in
991 (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
993 (l1 @ (List.map (fun (r, s, m, ug) ->
994 (u, lifted_arg)::r, s, m, ug) res),
995 (u, lifted_arg)::lifted_tl)
996 ) exp_named_subst ([], [])
1001 (* if match_only then replace_metas (\* context *\) where *)
1004 aux 0 where context metasenv [] ugraph
1007 (* if match_only then *)
1008 (* (fun (term, subst, metasenv, ugraph) -> *)
1010 (* C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
1011 (* and subst = restore_subst subst in *)
1012 (* (term', subst, metasenv, ugraph)) *)
1014 (fun (term, subst, metasenv, ugraph) ->
1015 let term' = C.Lambda (C.Anonymous, type_of_what, term) in
1016 (term', subst, metasenv, ugraph))
1018 List.map mapfun expansions
1022 let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
1023 let module C = Cic in
1024 let module S = CicSubstitution in
1025 let module T = CicTypeChecker in
1026 let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
1027 let ok_types ty menv =
1028 List.for_all (fun (_, _, mt) -> mt = ty) menv
1030 let rec aux index newmeta = function
1032 | (Some (_, C.Decl (term)))::tl ->
1033 let do_find context term =
1035 | C.Prod (name, s, t) ->
1036 (* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
1037 let (head, newmetas, args, newmeta) =
1038 ProofEngineHelpers.saturate_term newmeta []
1039 context (S.lift index term) 0
1042 if List.length args = 0 then
1045 C.Appl ((C.Rel index)::args)
1048 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
1049 when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
1052 (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
1054 (* Printf.sprintf "args: %s\n" *)
1055 (* (String.concat ", " (List.map CicPp.ppterm args)))); *)
1056 (* debug_print (lazy ( *)
1057 (* Printf.sprintf "newmetas:\n%s\n" *)
1058 (* (print_metasenv newmetas))); *)
1059 let o = !Utils.compare_terms t1 t2 in
1060 let w = compute_equality_weight ty t1 t2 in
1061 let proof = BasicProof p in
1062 let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
1064 | _ -> None, newmeta
1066 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
1067 when UriManager.eq uri eq_uri ->
1068 let t1 = S.lift index t1
1069 and t2 = S.lift index t2 in
1070 let o = !Utils.compare_terms t1 t2 in
1071 let w = compute_equality_weight ty t1 t2 in
1072 let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in
1074 | _ -> None, newmeta
1076 match do_find context term with
1077 | Some p, newmeta ->
1078 let tl, newmeta' = (aux (index+1) newmeta tl) in
1079 (index, p)::tl, max newmeta newmeta'
1081 aux (index+1) newmeta tl
1084 aux (index+1) newmeta tl
1086 let il, maxm = aux 1 newmeta context in
1087 let indexes, equalities = List.split il in
1088 indexes, equalities, maxm
1092 let equations_blacklist =
1094 (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
1095 UriManager.UriSet.empty [
1096 "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
1097 "cic:/Coq/Init/Logic/trans_eq.con";
1098 "cic:/Coq/Init/Logic/f_equal.con";
1099 "cic:/Coq/Init/Logic/f_equal2.con";
1100 "cic:/Coq/Init/Logic/f_equal3.con";
1101 "cic:/Coq/Init/Logic/f_equal4.con";
1102 "cic:/Coq/Init/Logic/f_equal5.con";
1103 "cic:/Coq/Init/Logic/sym_eq.con";
1104 "cic:/Coq/Init/Logic/eq_ind.con";
1105 "cic:/Coq/Init/Logic/eq_ind_r.con";
1106 "cic:/Coq/Init/Logic/eq_rec.con";
1107 "cic:/Coq/Init/Logic/eq_rec_r.con";
1108 "cic:/Coq/Init/Logic/eq_rect.con";
1109 "cic:/Coq/Init/Logic/eq_rect_r.con";
1110 "cic:/Coq/Logic/Eqdep/UIP.con";
1111 "cic:/Coq/Logic/Eqdep/UIP_refl.con";
1112 "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
1113 "cic:/Coq/ZArith/Zcompare/rename.con";
1114 (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
1115 perche' questo cacchio di teorema rompe le scatole :'( *)
1116 "cic:/Rocq/SUBST/comparith/mult_n_2.con";
1120 let find_library_equalities dbd context status maxmeta =
1121 let module C = Cic in
1122 let module S = CicSubstitution in
1123 let module T = CicTypeChecker in
1127 let suri = UriManager.string_of_uri uri in
1128 if UriManager.UriSet.mem uri equations_blacklist then
1131 let t = CicUtil.term_of_uri uri in
1133 CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
1137 (MetadataQuery.equations_for_goal ~dbd status)
1139 let eq_uri1 = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI
1140 and eq_uri2 = HelmLibraryObjects.Logic.eq_URI in
1142 (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
1144 let ok_types ty menv =
1145 List.for_all (fun (_, _, mt) -> mt = ty) menv
1147 let rec aux newmeta = function
1149 | (uri, term, termty)::tl ->
1152 (Printf.sprintf "Examining: %s (%s)"
1153 (CicPp.ppterm term) (CicPp.ppterm termty)));
1156 | C.Prod (name, s, t) ->
1157 let head, newmetas, args, newmeta =
1158 ProofEngineHelpers.saturate_term newmeta [] context termty 0
1161 if List.length args = 0 then
1167 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
1168 when (iseq uri) && (ok_types ty newmetas) ->
1171 (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
1172 let o = !Utils.compare_terms t1 t2 in
1173 let w = compute_equality_weight ty t1 t2 in
1174 let proof = BasicProof p in
1175 let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
1177 | _ -> None, newmeta
1179 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
1180 let o = !Utils.compare_terms t1 t2 in
1181 let w = compute_equality_weight ty t1 t2 in
1182 let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in
1184 | _ -> None, newmeta
1188 let tl, newmeta' = aux newmeta tl in
1189 (uri, e)::tl, max newmeta newmeta'
1193 let found, maxm = aux maxmeta candidates in
1194 let uriset, eqlist =
1196 (fun (s, l) (u, e) ->
1197 if List.exists (meta_convertibility_eq e) l then (
1200 (Printf.sprintf "NO!! %s already there!"
1201 (string_of_equality e)));
1202 (UriManager.UriSet.add u s, l)
1203 ) else (UriManager.UriSet.add u s, e::l))
1204 (UriManager.UriSet.empty, []) found)
1206 uriset, eqlist, maxm
1210 let find_library_theorems dbd env status equalities_uris =
1211 let module C = Cic in
1212 let module S = CicSubstitution in
1213 let module T = CicTypeChecker in
1216 UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in
1217 UriManager.UriSet.remove refl_equal
1218 (UriManager.UriSet.union equalities_uris equations_blacklist)
1220 let metasenv, context, ugraph = env in
1224 if UriManager.UriSet.mem uri blacklist then l
1226 let t = CicUtil.term_of_uri uri in
1227 let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
1229 [] (MetadataQuery.signature_of_goal ~dbd status)
1235 let find_context_hypotheses env equalities_indexes =
1236 let metasenv, context, ugraph = env in
1239 (fun (n, l) entry ->
1243 if List.mem n equalities_indexes then
1246 let t = Cic.Rel n in
1248 CicTypeChecker.type_of_aux' metasenv context t ugraph in
1249 (n+1, (t, ty, [])::l))
1256 let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
1257 (* print_endline ("fix_metas " ^ (string_of_int newmeta)); *)
1258 let table = Hashtbl.create (List.length args) in
1259 let is_this_case = ref false in
1260 let newargs, newmeta =
1262 (fun t (newargs, index) ->
1264 | Cic.Meta (i, l) ->
1265 if Hashtbl.mem table i then
1266 let idx = Hashtbl.find table i in
1267 ((Cic.Meta (idx, l))::newargs, index+1)
1269 let _ = Hashtbl.add table i index in
1270 ((Cic.Meta (index, l))::newargs, index+1)
1271 | _ -> assert false)
1272 args ([], newmeta+1)
1275 ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
1280 (fun (i, context, term) menv ->
1282 let index = Hashtbl.find table i in
1283 (index, context, term)::menv
1285 (i, context, term)::menv)
1289 and left = repl left
1290 and right = repl right in
1291 let metas = (metas_of_term left) @ (metas_of_term right) in
1292 let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
1295 (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
1298 if List.length metas > 0 then
1299 let first = List.hd metas in
1303 (function Cic.Meta (i, _) -> i = v | _ -> assert false)
1305 Hashtbl.replace table k first)
1306 (Hashtbl.copy table)
1308 let rec fix_proof = function
1309 | NoProof -> NoProof
1310 | BasicProof term -> BasicProof (repl term)
1311 | ProofBlock (subst, eq_URI, namety, bo(* t' *), (pos, eq), p) ->
1313 (* Printf.printf "fix_proof of equality %s, subst is:\n%s\n" *)
1314 (* (string_of_equality equality) (print_subst subst); *)
1316 (* debug_print "table is:"; *)
1318 (* (fun k v -> debug_print (Printf.sprintf "%d: %d" k v)) *)
1324 | Cic.Meta (i, l) -> (
1326 let j = Hashtbl.find table i in
1327 if List.mem_assoc i subst then
1330 let _, context, ty = CicUtil.lookup_meta i menv in
1331 (i, (context, Cic.Meta (j, l), ty))::s
1333 (* debug_print ("Not_found meta ?" ^ (string_of_int i)); *)
1336 | _ -> assert false)
1340 (* Printf.printf "subst' is:\n%s\n" (print_subst subst'); *)
1341 (* print_newline (); *)
1343 ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p)
1346 let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
1347 (newmeta + 1, neweq)
1351 let term_is_equality ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) term =
1352 let iseq uri = UriManager.eq uri eq_uri in
1354 | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
1359 exception TermIsNotAnEquality;;
1361 let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof term =
1362 let iseq uri = UriManager.eq uri eq_uri in
1364 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
1365 let o = !Utils.compare_terms t1 t2 in
1366 let w = compute_equality_weight ty t1 t2 in
1367 let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
1369 (* (proof, (ty, t1, t2, o), [], []) *)
1371 raise TermIsNotAnEquality
1375 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
1379 let superposition_left (metasenv, context, ugraph) target source =
1380 let module C = Cic in
1381 let module S = CicSubstitution in
1382 let module M = CicMetaSubst in
1383 let module HL = HelmLibraryObjects in
1384 let module CR = CicReduction in
1385 (* we assume that target is ground (does not contain metavariables): this
1386 * should always be the case (I hope, at least) *)
1387 let proof, (eq_ty, left, right, t_order), _, _ = target in
1388 let eqproof, (ty, t1, t2, s_order), newmetas, args = source in
1390 let compare_terms = !Utils.compare_terms in
1395 let where, is_left =
1396 match t_order (* compare_terms left right *) with
1397 | Lt -> right, false
1400 Printf.printf "????????? %s = %s" (CicPp.ppterm left)
1401 (CicPp.ppterm right);
1403 assert false (* again, for ground terms this shouldn't happen... *)
1406 let metasenv' = newmetas @ metasenv in
1407 let result = s_order (* compare_terms t1 t2 *) in
1410 | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
1411 | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
1415 (fun (t, s, m, ug) ->
1416 compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
1417 (beta_expand t1 ty where context metasenv' ugraph)
1420 (fun (t, s, m, ug) ->
1421 compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
1422 (beta_expand t2 ty where context metasenv' ugraph)
1426 (* let what, other = *)
1427 (* if is_left then left, right *)
1428 (* else right, left *)
1430 let build_new what other eq_URI (t, s, m, ug) =
1431 let newgoal, newgoalproof =
1433 | C.Lambda (nn, ty, bo) ->
1434 let bo' = S.subst (M.apply_subst s other) bo in
1437 [C.MutInd (HL.Logic.eq_URI, 0, []);
1439 if is_left then [bo'; S.lift 1 right]
1440 else [S.lift 1 left; bo'])
1442 let t' = C.Lambda (nn, ty, bo'') in
1443 S.subst (M.apply_subst s other) bo,
1445 (C.Appl [C.Const (eq_URI, []); ty; what; t';
1446 proof; other; eqproof])
1450 if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
1451 else (eq_ty, left, newgoal, compare_terms left newgoal)
1453 (newgoalproof (* eqproof *), equation, [], [])
1455 let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
1456 and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
1461 let superposition_right newmeta (metasenv, context, ugraph) target source =
1462 let module C = Cic in
1463 let module S = CicSubstitution in
1464 let module M = CicMetaSubst in
1465 let module HL = HelmLibraryObjects in
1466 let module CR = CicReduction in
1467 let eqproof, (eq_ty, left, right, t_order), newmetas, args = target in
1468 let eqp', (ty', t1, t2, s_order), newm', args' = source in
1469 let maxmeta = ref newmeta in
1471 let compare_terms = !Utils.compare_terms in
1473 if eq_ty <> ty' then
1476 (* let ok term subst other other_eq_side ugraph = *)
1477 (* match term with *)
1478 (* | C.Lambda (nn, ty, bo) -> *)
1479 (* let bo' = S.subst (M.apply_subst subst other) bo in *)
1480 (* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
1482 (* | _ -> assert false *)
1484 let condition left right what other (t, s, m, ug) =
1485 let subst = M.apply_subst s in
1486 let cmp1 = compare_terms (subst what) (subst other) in
1487 let cmp2 = compare_terms (subst left) (subst right) in
1488 (* cmp1 = Gt && cmp2 = Gt *)
1489 cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
1490 (* && (ok t s other right ug) *)
1492 let metasenv' = metasenv @ newmetas @ newm' in
1493 let beta_expand = beta_expand ~metas_ok:false in
1494 let cmp1 = t_order (* compare_terms left right *)
1495 and cmp2 = s_order (* compare_terms t1 t2 *) in
1496 let res1, res2, res3, res4 =
1500 (beta_expand s eq_ty l context metasenv' ugraph)
1502 match cmp1, cmp2 with
1504 (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
1506 [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
1508 [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
1510 [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
1512 let res1 = res left right t1 t2
1513 and res2 = res left right t2 t1 in
1516 let res3 = res right left t1 t2
1517 and res4 = res right left t2 t1 in
1520 let res1 = res left right t1 t2
1521 and res3 = res right left t1 t2 in
1524 let res2 = res left right t2 t1
1525 and res4 = res right left t2 t1 in
1528 let res1 = res left right t1 t2
1529 and res2 = res left right t2 t1
1530 and res3 = res right left t1 t2
1531 and res4 = res right left t2 t1 in
1532 res1, res2, res3, res4
1534 let newmetas = newmetas @ newm' in
1535 let newargs = args @ args' in
1536 let build_new what other is_left eq_URI (t, s, m, ug) =
1537 (* let what, other = *)
1538 (* if is_left then left, right *)
1539 (* else right, left *)
1541 let newterm, neweqproof =
1543 | C.Lambda (nn, ty, bo) ->
1544 let bo' = M.apply_subst s (S.subst other bo) in
1547 [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
1548 if is_left then [bo'; S.lift 1 right]
1549 else [S.lift 1 left; bo'])
1551 let t' = C.Lambda (nn, ty, bo'') in
1554 (C.Appl [C.Const (eq_URI, []); ty; what; t';
1555 eqproof; other; eqp'])
1558 let newmeta, newequality =
1560 if is_left then (newterm, M.apply_subst s right)
1561 else (M.apply_subst s left, newterm) in
1562 let neworder = compare_terms left right in
1564 (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
1569 let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
1570 and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
1571 and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
1572 and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
1574 | _, (_, left, right, _), _, _ ->
1575 not (fst (CR.are_convertible context left right ugraph))
1578 (List.filter ok (new1 @ new2 @ new3 @ new4)))
1583 let is_identity ((_, context, ugraph) as env) = function
1584 | ((_, _, (ty, left, right, _), _, _) as equality) ->
1586 (meta_convertibility left right) ||
1587 (fst (CicReduction.are_convertible context left right ugraph)))
1592 let demodulation newmeta (metasenv, context, ugraph) target source =
1593 let module C = Cic in
1594 let module S = CicSubstitution in
1595 let module M = CicMetaSubst in
1596 let module HL = HelmLibraryObjects in
1597 let module CR = CicReduction in
1599 let proof, (eq_ty, left, right, t_order), metas, args = target
1600 and proof', (ty, t1, t2, s_order), metas', args' = source in
1602 let compare_terms = !Utils.compare_terms in
1607 let first_step, get_params =
1608 match s_order (* compare_terms t1 t2 *) with
1609 | Gt -> 1, (function
1610 | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
1611 | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
1612 | _ -> assert false)
1613 | Lt -> 1, (function
1614 | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1615 | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1616 | _ -> assert false)
1618 let first_step = 3 in
1619 let get_params step =
1621 | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
1622 | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
1623 | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1624 | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1627 first_step, get_params
1629 let rec demodulate newmeta step metasenv target =
1630 let proof, (eq_ty, left, right, t_order), metas, args = target in
1631 let is_left, what, other, eq_URI = get_params step in
1633 let env = metasenv, context, ugraph in
1634 let names = names_of_context context in
1636 (* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1637 (* (string_of_equality ~env target) (CicPp.pp what names) *)
1638 (* (CicPp.pp other names) (string_of_bool is_left); *)
1639 (* Printf.printf "step: %d" step; *)
1640 (* print_newline (); *)
1642 let ok (t, s, m, ug) =
1643 compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
1646 let r = (beta_expand ~metas_ok:false ~match_only:true
1647 what ty (if is_left then left else right)
1648 context (metasenv @ metas) ugraph)
1650 (* let m' = metas_of_term what *)
1651 (* and m'' = metas_of_term (if is_left then left else right) in *)
1652 (* if (List.mem 527 m'') && (List.mem 6 m') then ( *)
1654 (* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1655 (* (string_of_equality ~env target) (CicPp.pp what names) *)
1656 (* (CicPp.pp other names) (string_of_bool is_left); *)
1657 (* Printf.printf "step: %d" step; *)
1658 (* print_newline (); *)
1659 (* print_endline "res:"; *)
1660 (* List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
1661 (* print_newline (); *)
1662 (* Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
1663 (* print_newline (); *)
1669 if step = 0 then newmeta, target
1670 else demodulate newmeta (step-1) metasenv target
1671 | (t, s, m, ug)::_ ->
1672 let newterm, newproof =
1674 | C.Lambda (nn, ty, bo) ->
1675 (* let bo' = M.apply_subst s (S.subst other bo) in *)
1676 let bo' = S.subst (M.apply_subst s other) bo in
1679 [C.MutInd (HL.Logic.eq_URI, 0, []);
1681 if is_left then [bo'; S.lift 1 right]
1682 else [S.lift 1 left; bo'])
1684 let t' = C.Lambda (nn, ty, bo'') in
1685 (* M.apply_subst s (S.subst other bo), *)
1688 (C.Appl [C.Const (eq_URI, []); ty; what; t';
1689 proof; other; proof'])
1692 let newmeta, newtarget =
1694 (* if is_left then (newterm, M.apply_subst s right) *)
1695 (* else (M.apply_subst s left, newterm) in *)
1696 if is_left then newterm, right
1699 let neworder = compare_terms left right in
1700 (* let newmetasenv = metasenv @ metas in *)
1701 (* let newargs = args @ args' in *)
1702 (* fix_metas newmeta *)
1703 (* (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
1704 let m = (metas_of_term left) @ (metas_of_term right) in
1705 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
1708 (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
1712 (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs)
1715 (* "demodulate, newtarget: %s\ntarget was: %s\n" *)
1716 (* (string_of_equality ~env newtarget) *)
1717 (* (string_of_equality ~env target); *)
1718 (* (\* let _, _, newm, newa = newtarget in *\) *)
1719 (* (\* Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
1720 (* (\* (print_metasenv newm) *\) *)
1721 (* (\* (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
1722 (* print_newline (); *)
1723 if is_identity env newtarget then
1726 demodulate newmeta first_step metasenv newtarget
1728 demodulate newmeta first_step (metasenv @ metas') target
1733 let demodulation newmeta env target source =
1739 let subsumption env target source =
1740 let _, (ty, tl, tr, _), tmetas, _ = target
1741 and _, (ty', sl, sr, _), smetas, _ = source in
1745 let metasenv, context, ugraph = env in
1746 let metasenv = metasenv @ tmetas @ smetas in
1747 let names = names_of_context context in
1748 let samesubst subst subst' =
1749 (* Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
1750 (* (print_subst subst) (print_subst subst'); *)
1751 (* print_newline (); *)
1752 let tbl = Hashtbl.create (List.length subst) in
1753 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
1755 (fun (m, (c, t1, t2)) ->
1757 let c', t1', t2' = Hashtbl.find tbl m in
1758 if (c = c') && (t1 = t1') && (t2 = t2') then true
1764 let subsaux left right left' right' =
1766 let subst, menv, ug = matching metasenv context left left' ugraph
1767 and subst', menv', ug' = matching metasenv context right right' ugraph
1769 (* Printf.printf "left = right: %s = %s\n" *)
1770 (* (CicPp.pp left names) (CicPp.pp right names); *)
1771 (* Printf.printf "left' = right': %s = %s\n" *)
1772 (* (CicPp.pp left' names) (CicPp.pp right' names); *)
1773 samesubst subst subst'
1775 (* print_endline (Printexc.to_string e); *)
1779 if subsaux tl tr sl sr then true
1780 else subsaux tl tr sr sl
1783 Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
1784 (string_of_equality ~env target) (string_of_equality ~env source);
1792 let extract_differing_subterms t1 t2 =
1793 let module C = Cic in
1796 | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
1798 | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
1799 let res = List.concat (List.map2 aux tl1 tl2) in
1801 if res = [] then [(h1, h2)] else [(t1, t2)]
1803 if List.length res > 1 then [(t1, t2)] else res
1805 if t1 <> t2 then [(t1, t2)] else []
1807 let res = aux t1 t2 in
1814 let rec string_of_proof = function
1815 | NoProof -> "NoProof"
1816 | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t)
1817 | SubProof (t, i, p) ->
1818 Printf.sprintf "SubProof(%s, %s, %s)"
1819 (CicPp.ppterm t) (string_of_int i) (string_of_proof p)
1820 | ProofSymBlock _ -> "ProofSymBlock"
1821 | ProofBlock _ -> "ProofBlock"
1822 | ProofGoalBlock (p1, p2) ->
1823 Printf.sprintf "ProofGoalBlock(%s, %s)"
1824 (string_of_proof p1) (string_of_proof p2)