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 (* name, ty, eq_ty, left, right *)
20 (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) *
21 (Utils.pos * equality) * proof
22 | ProofGoalBlock of proof * equality
23 | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof
27 let string_of_equality ?env =
31 | w, _, (ty, left, right, o), _, _ ->
32 Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty)
33 (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
35 | Some (_, context, _) -> (
36 let names = names_of_context context in
38 | w, _, (ty, left, right, o), _, _ ->
39 Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names)
40 (CicPp.pp left names) (string_of_comparison o)
41 (CicPp.pp right names)
46 let build_proof_term equality =
47 (* Printf.printf "build_term_proof %s" (string_of_equality equality); *)
48 (* print_newline (); *)
52 let rec do_build_proof proof =
55 Printf.fprintf stderr "WARNING: no proof!\n";
56 (* (string_of_equality equality); *)
58 | BasicProof term -> term
59 | ProofGoalBlock (proofbit, equality) ->
60 print_endline "found ProofGoalBlock, going up...";
61 let _, proof, _, _, _ = equality in
62 do_build_goal_proof proofbit proof
63 | ProofSymBlock (ens, proof) ->
64 let proof = do_build_proof proof in
66 Cic.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens); (* symmetry *)
69 | ProofBlock (subst, eq_URI, t', (pos, eq), eqproof) ->
70 (* Printf.printf "\nsubst:\n%s\n" (print_subst subst); *)
71 (* print_newline (); *)
73 let name, ty, eq_ty, left, right = t' in
75 Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
78 let t' = Cic.Lambda (name, ty, (* CicSubstitution.lift 1 *) bo) in
79 (* Printf.printf " ProofBlock: eq = %s, eq' = %s" *)
80 (* (string_of_equality eq) (string_of_equality eq'); *)
81 (* print_newline (); *)
83 (* let s = String.make !indent ' ' in *)
86 (* print_endline (s ^ "build proof'------------"); *)
89 let _, proof', _, _, _ = eq in
92 (* print_endline (s ^ "END proof'"); *)
94 (* print_endline (s ^ "build eqproof-----------"); *)
96 let eqproof = do_build_proof eqproof in
98 (* print_endline (s ^ "END eqproof"); *)
102 let _, _, (ty, what, other, _), menv', args' = eq in
104 if pos = Utils.Left then what, other else other, what
106 CicMetaSubst.apply_subst subst
107 (Cic.Appl [Cic.Const (eq_URI, []); ty;
108 what; t'; eqproof; other; proof'])
110 and do_build_goal_proof proofbit proof =
111 (* match proofbit with *)
112 (* | BasicProof _ -> do_build_proof proof *)
115 | ProofGoalBlock (pb, eq) ->
116 do_build_proof (ProofGoalBlock (replace_proof proofbit pb, eq))
117 (* let _, proof, _, _, _ = eq in *)
118 (* let newproof = replace_proof proofbit proof in *)
119 (* do_build_proof newproof *)
121 (* | ProofBlock (subst, eq_URI, t', poseq, eqproof) -> *)
122 (* let eqproof' = replace_proof proofbit eqproof in *)
123 (* do_build_proof (ProofBlock (subst, eq_URI, t', poseq, eqproof')) *)
124 | _ -> do_build_proof (replace_proof proofbit proof) (* assert false *)
126 and replace_proof newproof = function
127 | ProofBlock (subst, eq_URI, t', poseq, eqproof) ->
129 (* if eq_URI = HelmLibraryObjects.Logic.eq_ind_URI then *)
130 (* HelmLibraryObjects.Logic.eq_ind_r_URI *)
132 (* HelmLibraryObjects.Logic.eq_ind_URI *)
134 let eqproof' = replace_proof newproof eqproof in
135 ProofBlock (subst, uri(* eq_URI *), t', poseq, eqproof')
136 (* ProofBlock (subst, eq_URI, t', poseq, newproof) *)
137 | ProofGoalBlock (pb, equality) ->
138 let pb' = replace_proof newproof pb in
139 ProofGoalBlock (pb', equality)
140 (* let w, proof, t, menv, args = equality in *)
141 (* let proof' = replace_proof newproof proof in *)
142 (* ProofGoalBlock (pb, (w, proof', t, menv, args)) *)
143 | BasicProof _ -> newproof
146 let _, proof, _, _, _ = equality in
151 let rec metas_of_term = function
152 | Cic.Meta (i, c) -> [i]
155 | Cic.MutInd (_, _, ens)
156 | Cic.MutConstruct (_, _, _, ens) ->
157 List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
160 | Cic.Lambda (_, s, t)
161 | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
162 | Cic.Appl l -> List.flatten (List.map metas_of_term l)
163 | Cic.MutCase (uri, i, s, t, l) ->
164 (metas_of_term s) @ (metas_of_term t) @
165 (List.flatten (List.map metas_of_term l))
168 (List.map (fun (s, i, t1, t2) ->
169 (metas_of_term t1) @ (metas_of_term t2)) il)
170 | Cic.CoFix (i, il) ->
172 (List.map (fun (s, t1, t2) ->
173 (metas_of_term t1) @ (metas_of_term t2)) il)
178 exception NotMetaConvertible;;
180 let meta_convertibility_aux table t1 t2 =
181 let module C = Cic in
185 (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
187 let rec aux ((table_l, table_r) as table) t1 t2 =
188 (* Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *)
189 (* (CicPp.ppterm t1) (CicPp.ppterm t2) *)
190 (* (print_table table_l) (print_table table_r); *)
192 | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
193 let m1_binding, table_l =
194 try List.assoc m1 table_l, table_l
195 with Not_found -> m2, (m1, m2)::table_l
196 and m2_binding, table_r =
197 try List.assoc m2 table_r, table_r
198 with Not_found -> m1, (m2, m1)::table_r
200 (* let m1_binding, m2_binding, table = *)
201 (* let m1b, table = *)
202 (* try List.assoc m1 table, table *)
203 (* with Not_found -> m2, (m1, m2)::table *)
205 (* let m2b, table = *)
206 (* try List.assoc m2 table, table *)
207 (* with Not_found -> m1, (m2, m1)::table *)
209 (* m1b, m2b, table *)
211 (* Printf.printf "table_l: %s\ntable_r: %s\n\n" *)
212 (* (print_table table_l) (print_table table_r); *)
213 if (m1_binding <> m2) || (m2_binding <> m1) then
214 raise NotMetaConvertible
220 | None, Some _ | Some _, None -> raise NotMetaConvertible
222 | Some t1, Some t2 -> (aux res t1 t2))
223 (table_l, table_r) tl1 tl2
224 with Invalid_argument _ ->
225 raise NotMetaConvertible
227 | C.Var (u1, ens1), C.Var (u2, ens2)
228 | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
229 aux_ens table ens1 ens2
230 | C.Cast (s1, t1), C.Cast (s2, t2)
231 | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
232 | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
233 | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
234 let table = aux table s1 s2 in
236 | C.Appl l1, C.Appl l2 -> (
237 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
238 with Invalid_argument _ -> raise NotMetaConvertible
240 | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
241 when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
242 | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
243 when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
244 aux_ens table ens1 ens2
245 | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
246 when (UriManager.eq u1 u2) && i1 = i2 ->
247 let table = aux table s1 s2 in
248 let table = aux table t1 t2 in (
249 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
250 with Invalid_argument _ -> raise NotMetaConvertible
252 | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
255 (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
256 if i1 <> i2 then raise NotMetaConvertible
258 let res = (aux res s1 s2) in aux res t1 t2)
260 with Invalid_argument _ -> raise NotMetaConvertible
262 | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
265 (fun res (n1, s1, t1) (n2, s2, t2) ->
266 let res = aux res s1 s2 in aux res t1 t2)
268 with Invalid_argument _ -> raise NotMetaConvertible
270 | t1, t2 when t1 = t2 -> table
271 | _, _ -> raise NotMetaConvertible
273 and aux_ens table ens1 ens2 =
274 let cmp (u1, t1) (u2, t2) =
275 compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
277 let ens1 = List.sort cmp ens1
278 and ens2 = List.sort cmp ens2 in
281 (fun res (u1, t1) (u2, t2) ->
282 if not (UriManager.eq u1 u2) then raise NotMetaConvertible
285 with Invalid_argument _ -> raise NotMetaConvertible
291 let meta_convertibility_eq eq1 eq2 =
292 let _, _, (ty, left, right, _), _, _ = eq1
293 and _, _, (ty', left', right', _), _, _ = eq2 in
296 else if (left = left') && (right = right') then
298 else if (left = right') && (right = left') then
302 let table = meta_convertibility_aux ([], []) left left' in
303 let _ = meta_convertibility_aux table right right' in
305 with NotMetaConvertible ->
307 let table = meta_convertibility_aux ([], []) left right' in
308 let _ = meta_convertibility_aux table right left' in
310 with NotMetaConvertible ->
315 let meta_convertibility t1 t2 =
319 (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
325 let l, r = meta_convertibility_aux ([], []) t1 t2 in
326 (* Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *)
328 with NotMetaConvertible ->
333 let replace_metas (* context *) term =
334 let module C = Cic in
335 let rec aux = function
338 (* CicMkImplicit.identity_relocation_list_for_metavariable context *)
340 (* if c = irl then *)
341 (* C.Implicit (Some (`MetaIndex i)) *)
343 (* Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *)
344 (* (String.concat "\n" *)
346 (* (function None -> "" | Some t -> CicPp.ppterm t) c)); *)
349 C.Implicit (Some (`MetaInfo (i, c)))
350 | C.Var (u, ens) -> C.Var (u, aux_ens ens)
351 | C.Const (u, ens) -> C.Const (u, aux_ens ens)
352 | C.Cast (s, t) -> C.Cast (aux s, aux t)
353 | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
354 | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
355 | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
356 | C.Appl l -> C.Appl (List.map aux l)
357 | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
358 | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
359 | C.MutCase (uri, i, s, t, l) ->
360 C.MutCase (uri, i, aux s, aux t, List.map aux l)
363 List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
367 List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
371 List.map (fun (u, t) -> (u, aux t)) ens
377 let restore_metas (* context *) term =
378 let module C = Cic in
379 let rec aux = function
380 | C.Implicit (Some (`MetaInfo (i, c))) ->
382 (* CicMkImplicit.identity_relocation_list_for_metavariable context *)
385 (* let local_context:(C.term option) list = *)
386 (* Marshal.from_string mc 0 *)
388 (* C.Meta (i, local_context) *)
390 | C.Var (u, ens) -> C.Var (u, aux_ens ens)
391 | C.Const (u, ens) -> C.Const (u, aux_ens ens)
392 | C.Cast (s, t) -> C.Cast (aux s, aux t)
393 | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
394 | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
395 | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
396 | C.Appl l -> C.Appl (List.map aux l)
397 | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
398 | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
399 | C.MutCase (uri, i, s, t, l) ->
400 C.MutCase (uri, i, aux s, aux t, List.map aux l)
403 List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
407 List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
411 List.map (fun (u, t) -> (u, aux t)) ens
417 let rec restore_subst (* context *) subst =
419 (fun (i, (c, t, ty)) ->
420 i, (c, restore_metas (* context *) t, ty))
425 let rec check_irl start = function
427 | None::tl -> check_irl (start+1) tl
428 | (Some (Cic.Rel x))::tl ->
429 if x = start then check_irl (start+1) tl else false
433 let rec is_simple_term = function
434 | Cic.Appl ((Cic.Meta _)::_) -> false
435 | Cic.Appl l -> List.for_all is_simple_term l
436 | Cic.Meta (i, l) -> check_irl 1 l
442 let lookup_subst meta subst =
444 | Cic.Meta (i, _) -> (
445 try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
446 with Not_found -> meta
452 let unification_simple metasenv context t1 t2 ugraph =
453 let module C = Cic in
454 let module M = CicMetaSubst in
455 let module U = CicUnification in
456 let lookup = lookup_subst in
457 let rec occurs_check subst what where =
458 (* Printf.printf "occurs_check %s %s" *)
459 (* (CicPp.ppterm what) (CicPp.ppterm where); *)
460 (* print_newline (); *)
462 | t when what = t -> true
463 | C.Appl l -> List.exists (occurs_check subst what) l
465 let t = lookup where subst in
466 if t <> where then occurs_check subst what t else false
469 let rec unif subst menv s t =
470 (* Printf.printf "unif %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
471 (* (print_subst subst); *)
472 (* print_newline (); *)
473 let s = match s with C.Meta _ -> lookup s subst | _ -> s
474 and t = match t with C.Meta _ -> lookup t subst | _ -> t
476 (* Printf.printf "after apply_subst: %s %s\n%s" *)
477 (* (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
478 (* print_newline (); *)
480 | s, t when s = t -> subst, menv
481 | C.Meta (i, _), C.Meta (j, _) when i > j ->
483 | C.Meta _, t when occurs_check subst s t ->
484 raise (U.UnificationFailure "Inference.unification.unif")
485 (* | C.Meta (i, l), C.Meta (j, l') -> *)
486 (* let _, _, ty = CicUtil.lookup_meta i menv in *)
487 (* let _, _, ty' = CicUtil.lookup_meta j menv in *)
488 (* let binding1 = lookup s subst in *)
489 (* let binding2 = lookup t subst in *)
490 (* let subst, menv = *)
491 (* if binding1 != s then *)
492 (* if binding2 != t then *)
493 (* unif subst menv binding1 binding2 *)
495 (* if binding1 = t then *)
498 (* ((j, (context, binding1, ty'))::subst, *)
499 (* List.filter (fun (m, _, _) -> j <> m) menv) *)
501 (* if binding2 != t then *)
502 (* if s = binding2 then *)
505 (* ((i, (context, binding2, ty))::subst, *)
506 (* List.filter (fun (m, _, _) -> i <> m) menv) *)
508 (* ((i, (context, t, ty))::subst, *)
509 (* List.filter (fun (m, _, _) -> i <> m) menv) *)
513 | C.Meta (i, l), t ->
514 let _, _, ty = CicUtil.lookup_meta i menv in
516 if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
519 let menv = List.filter (fun (m, _, _) -> i <> m) menv in
521 | _, C.Meta _ -> unif subst menv t s
522 | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
523 raise (U.UnificationFailure "Inference.unification.unif")
524 | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
527 (fun (subst', menv) s t -> unif subst' menv s t)
528 (subst, menv) tls tlt
530 raise (U.UnificationFailure "Inference.unification.unif")
532 | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
534 let subst, menv = unif [] metasenv t1 t2 in
535 (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
536 (* print_newline (); *)
537 (* let rec fix_term = function *)
538 (* | (C.Meta (i, l) as t) -> *)
540 (* | C.Appl l -> C.Appl (List.map fix_term l) *)
543 (* let rec fix_subst = function *)
545 (* | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl) *)
547 (* List.rev (fix_subst subst), menv, ugraph *)
548 List.rev subst, menv, ugraph
552 let unification metasenv context t1 t2 ugraph =
553 (* Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
554 let subst, menv, ug =
555 if not (is_simple_term t1) || not (is_simple_term t2) then
556 CicUnification.fo_unif metasenv context t1 t2 ugraph
558 unification_simple metasenv context t1 t2 ugraph
560 let rec fix_term = function
561 | (Cic.Meta (i, l) as t) ->
562 let t' = lookup_subst t subst in
563 if t <> t' then fix_term t' else t
564 | Cic.Appl l -> Cic.Appl (List.map fix_term l)
567 let rec fix_subst = function
569 | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
571 (* Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
572 (* print_endline "|"; *)
573 fix_subst subst, menv, ug
577 (* let unification = CicUnification.fo_unif;; *)
579 exception MatchingFailure;;
582 let matching_simple metasenv context t1 t2 ugraph =
583 let module C = Cic in
584 let module M = CicMetaSubst in
585 let module U = CicUnification in
586 let lookup meta subst =
589 try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
590 with Not_found -> meta
594 let rec do_match subst menv s t =
595 (* Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
596 (* (print_subst subst); *)
597 (* print_newline (); *)
598 (* let s = match s with C.Meta _ -> lookup s subst | _ -> s *)
599 (* let t = match t with C.Meta _ -> lookup t subst | _ -> t in *)
600 (* Printf.printf "after apply_subst: %s %s\n%s" *)
601 (* (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
602 (* print_newline (); *)
604 | s, t when s = t -> subst, menv
605 (* | C.Meta (i, _), C.Meta (j, _) when i > j -> *)
606 (* do_match subst menv t s *)
607 (* | C.Meta _, t when occurs_check subst s t -> *)
608 (* raise MatchingFailure *)
609 (* | s, C.Meta _ when occurs_check subst t s -> *)
610 (* raise MatchingFailure *)
611 | s, C.Meta (i, l) ->
612 let filter_menv i menv =
613 List.filter (fun (m, _, _) -> i <> m) menv
616 let value = lookup t subst in
618 (* | C.Meta (i', l') when Hashtbl.mem table i' -> *)
619 (* (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *)
620 | value when value = t ->
621 let _, _, ty = CicUtil.lookup_meta i menv in
622 (i, (context, s, ty))::subst, filter_menv i menv
623 | value when value <> s ->
624 raise MatchingFailure
625 | value -> do_match subst menv s value
628 (* else if value <> s then *)
629 (* raise MatchingFailure *)
631 (* if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst *)
634 (* let menv = List.filter (fun (m, _, _) -> i <> m) menv in *)
636 (* | _, C.Meta _ -> do_match subst menv t s *)
637 (* | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *)
638 (* raise MatchingFailure *)
639 | C.Appl ls, C.Appl lt -> (
642 (fun (subst, menv) s t -> do_match subst menv s t)
645 (* print_endline (Printexc.to_string e); *)
646 (* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
647 (* print_newline (); *)
648 raise MatchingFailure
651 (* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
652 (* print_newline (); *)
653 raise MatchingFailure
655 let subst, menv = do_match [] metasenv t1 t2 in
656 (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
657 (* print_newline (); *)
662 let matching metasenv context t1 t2 ugraph =
663 (* if (is_simple_term t1) && (is_simple_term t2) then *)
664 (* let subst, menv, ug = *)
665 (* matching_simple metasenv context t1 t2 ugraph in *)
666 (* (\* Printf.printf "matching %s %s:\n%s\n" *\) *)
667 (* (\* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *)
668 (* (\* print_newline (); *\) *)
669 (* subst, menv, ug *)
672 let subst, metasenv, ugraph =
673 (* CicUnification.fo_unif metasenv context t1 t2 ugraph *)
674 unification metasenv context t1 t2 ugraph
676 let t' = CicMetaSubst.apply_subst subst t1 in
677 if not (meta_convertibility t1 t') then
678 raise MatchingFailure
680 let metas = metas_of_term t1 in
681 let fix_subst = function
682 | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
683 (j, (c, Cic.Meta (i, lc), ty))
686 let subst = List.map fix_subst subst in
688 (* Printf.printf "matching %s %s:\n%s\n" *)
689 (* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *)
690 (* print_newline (); *)
692 subst, metasenv, ugraph
694 (* Printf.printf "failed to match %s %s\n" *)
695 (* (CicPp.ppterm t1) (CicPp.ppterm t2); *)
696 raise MatchingFailure
700 (* let profile = CicUtil.profile "Inference.matching" in *)
701 (* (fun metasenv context t1 t2 ugraph -> *)
702 (* profile (matching metasenv context t1 t2) ugraph) *)
706 let beta_expand ?(metas_ok=true) ?(match_only=false)
707 what type_of_what where context metasenv ugraph =
708 let module S = CicSubstitution in
709 let module C = Cic in
711 let print_info = false in
714 (* let names = names_of_context context in *)
715 (* Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
716 (* (CicPp.pp what names) (CicPp.ppterm what) *)
717 (* (CicPp.pp where names) (CicPp.ppterm where); *)
718 (* print_newline (); *)
722 ((list of all possible beta expansions, subst, metasenv, ugraph),
725 let rec aux lift_amount term context metasenv subst ugraph =
726 (* Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
727 let res, lifted_term =
730 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
732 | C.Var (uri, exp_named_subst) ->
733 let ens', lifted_ens =
734 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
738 (fun (e, s, m, ug) ->
739 (C.Var (uri, e), s, m, ug)) ens'
741 expansions, C.Var (uri, lifted_ens)
746 (fun arg (res, lifted_tl) ->
749 let arg_res, lifted_arg =
750 aux lift_amount arg context metasenv subst ugraph in
753 (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
758 (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
760 (Some lifted_arg)::lifted_tl)
763 (fun (r, s, m, ug) -> None::r, s, m, ug)
770 (fun (l, s, m, ug) ->
771 (C.Meta (i, l), s, m, ug)) l'
773 e, C.Meta (i, lifted_l)
776 | C.Implicit _ as t -> [], t
780 aux lift_amount s context metasenv subst ugraph in
782 aux lift_amount t context metasenv subst ugraph
786 (fun (t, s, m, ug) ->
787 C.Cast (t, lifted_t), s, m, ug) l1 in
790 (fun (t, s, m, ug) ->
791 C.Cast (lifted_s, t), s, m, ug) l2 in
792 l1'@l2', C.Cast (lifted_s, lifted_t)
794 | C.Prod (nn, s, t) ->
796 aux lift_amount s context metasenv subst ugraph in
798 aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
799 metasenv subst ugraph
803 (fun (t, s, m, ug) ->
804 C.Prod (nn, t, lifted_t), s, m, ug) l1 in
807 (fun (t, s, m, ug) ->
808 C.Prod (nn, lifted_s, t), s, m, ug) l2 in
809 l1'@l2', C.Prod (nn, lifted_s, lifted_t)
811 | C.Lambda (nn, s, t) ->
813 aux lift_amount s context metasenv subst ugraph in
815 aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
816 metasenv subst ugraph
820 (fun (t, s, m, ug) ->
821 C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
824 (fun (t, s, m, ug) ->
825 C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
826 l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
828 | C.LetIn (nn, s, t) ->
830 aux lift_amount s context metasenv subst ugraph in
832 aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
833 metasenv subst ugraph
837 (fun (t, s, m, ug) ->
838 C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
841 (fun (t, s, m, ug) ->
842 C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
843 l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
847 aux_list lift_amount l context metasenv subst ugraph
849 (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
852 | C.Const (uri, exp_named_subst) ->
853 let ens', lifted_ens =
854 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
858 (fun (e, s, m, ug) ->
859 (C.Const (uri, e), s, m, ug)) ens'
861 (expansions, C.Const (uri, lifted_ens))
863 | C.MutInd (uri, i ,exp_named_subst) ->
864 let ens', lifted_ens =
865 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
869 (fun (e, s, m, ug) ->
870 (C.MutInd (uri, i, e), s, m, ug)) ens'
872 (expansions, C.MutInd (uri, i, lifted_ens))
874 | C.MutConstruct (uri, i, j, exp_named_subst) ->
875 let ens', lifted_ens =
876 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
880 (fun (e, s, m, ug) ->
881 (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
883 (expansions, C.MutConstruct (uri, i, j, lifted_ens))
885 | C.MutCase (sp, i, outt, t, pl) ->
886 let pl_res, lifted_pl =
887 aux_list lift_amount pl context metasenv subst ugraph
889 let l1, lifted_outt =
890 aux lift_amount outt context metasenv subst ugraph in
892 aux lift_amount t context metasenv subst ugraph in
896 (fun (outt, s, m, ug) ->
897 C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
900 (fun (t, s, m, ug) ->
901 C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
904 (fun (pl, s, m, ug) ->
905 C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
907 (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
910 let len = List.length fl in
913 (fun (nm, idx, ty, bo) (res, lifted_tl) ->
914 let lifted_ty = S.lift lift_amount ty in
915 let bo_res, lifted_bo =
916 aux (lift_amount+len) bo context metasenv subst ugraph in
919 (fun (a, s, m, ug) ->
920 (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
925 (fun (r, s, m, ug) ->
926 (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
927 (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
931 (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
932 C.Fix (i, lifted_fl))
935 let len = List.length fl in
938 (fun (nm, ty, bo) (res, lifted_tl) ->
939 let lifted_ty = S.lift lift_amount ty in
940 let bo_res, lifted_bo =
941 aux (lift_amount+len) bo context metasenv subst ugraph in
944 (fun (a, s, m, ug) ->
945 (nm, lifted_ty, a)::lifted_tl, s, m, ug)
950 (fun (r, s, m, ug) ->
951 (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
952 (nm, lifted_ty, lifted_bo)::lifted_tl)
956 (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
957 C.CoFix (i, lifted_fl))
961 | C.Meta _ when (not metas_ok) ->
965 (* if match_only then replace_metas context term *)
969 let subst', metasenv', ugraph' =
970 (* Printf.printf "provo a unificare %s e %s\n" *)
971 (* (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
973 matching metasenv context term (S.lift lift_amount what) ugraph
975 CicUnification.fo_unif metasenv context
976 (S.lift lift_amount what) term ugraph
978 (* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
979 (* (CicPp.ppterm (S.lift lift_amount what)); *)
980 (* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
981 (* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
982 (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
983 (* if match_only then *)
984 (* let t' = CicMetaSubst.apply_subst subst' term in *)
985 (* if not (meta_convertibility term t') then ( *)
986 (* res, lifted_term *)
988 (* let metas = metas_of_term term in *)
989 (* let fix_subst = function *)
990 (* | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
991 (* (j, (c, C.Meta (i, lc), ty)) *)
994 (* let subst' = List.map fix_subst subst' in *)
995 (* ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
999 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
1002 if print_info then (
1003 print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e));
1007 (* Printf.printf "exit aux\n"; *)
1010 and aux_list lift_amount l context metasenv subst ugraph =
1012 (fun arg (res, lifted_tl) ->
1013 let arg_res, lifted_arg =
1014 aux lift_amount arg context metasenv subst ugraph in
1016 (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
1019 (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
1020 lifted_arg::lifted_tl)
1023 and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
1025 (fun (u, arg) (res, lifted_tl) ->
1026 let arg_res, lifted_arg =
1027 aux lift_amount arg context metasenv subst ugraph in
1030 (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
1032 (l1 @ (List.map (fun (r, s, m, ug) ->
1033 (u, lifted_arg)::r, s, m, ug) res),
1034 (u, lifted_arg)::lifted_tl)
1035 ) exp_named_subst ([], [])
1040 (* if match_only then replace_metas (\* context *\) where *)
1043 if print_info then (
1044 Printf.printf "searching %s inside %s\n"
1045 (CicPp.ppterm what) (CicPp.ppterm where);
1047 aux 0 where context metasenv [] ugraph
1050 (* if match_only then *)
1051 (* (fun (term, subst, metasenv, ugraph) -> *)
1053 (* C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
1054 (* and subst = restore_subst subst in *)
1055 (* (term', subst, metasenv, ugraph)) *)
1057 (fun (term, subst, metasenv, ugraph) ->
1058 let term' = C.Lambda (C.Anonymous, type_of_what, term) in
1059 (term', subst, metasenv, ugraph))
1061 List.map mapfun expansions
1065 let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
1066 let module C = Cic in
1067 let module S = CicSubstitution in
1068 let module T = CicTypeChecker in
1069 let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
1070 let rec aux index newmeta = function
1072 | (Some (_, C.Decl (term)))::tl ->
1073 let do_find context term =
1075 | C.Prod (name, s, t) ->
1076 (* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
1077 let (head, newmetas, args, newmeta) =
1078 ProofEngineHelpers.saturate_term newmeta []
1079 context (S.lift index term)
1082 if List.length args = 0 then
1085 C.Appl ((C.Rel index)::args)
1088 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
1089 Printf.printf "OK: %s\n" (CicPp.ppterm term);
1090 let o = !Utils.compare_terms t1 t2 in
1091 let w = compute_equality_weight ty t1 t2 in
1092 let proof = BasicProof p in
1093 let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
1095 | _ -> None, newmeta
1097 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
1098 let t1 = S.lift index t1
1099 and t2 = S.lift index t2 in
1100 let o = !Utils.compare_terms t1 t2 in
1101 let w = compute_equality_weight ty t1 t2 in
1102 let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in
1104 | _ -> None, newmeta
1106 match do_find context term with
1107 | Some p, newmeta ->
1108 let tl, newmeta' = (aux (index+1) newmeta tl) in
1109 p::tl, max newmeta newmeta'
1111 aux (index+1) newmeta tl
1114 aux (index+1) newmeta tl
1116 aux 1 newmeta context
1120 let find_library_equalities ~(dbd:Mysql.dbd) status maxmeta =
1121 let module C = Cic in
1122 let module S = CicSubstitution in
1123 let module T = CicTypeChecker in
1127 let t = CicUtil.term_of_uri uri in
1128 let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
1130 (MetadataQuery.equations_for_goal ~dbd status)
1132 let eq_uri1 = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI
1133 and eq_uri2 = HelmLibraryObjects.Logic.eq_URI in
1135 uri == eq_uri1 || uri == eq_uri2
1137 let rec aux newmeta = function
1139 | (term, termty)::tl ->
1142 | C.Prod (name, s, t) ->
1143 let head, newmetas, args, newmeta =
1144 ProofEngineHelpers.saturate_term newmeta [] [] termty
1147 if List.length args = 0 then
1153 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
1154 Printf.printf "OK: %s\n" (CicPp.ppterm term);
1155 let o = !Utils.compare_terms t1 t2 in
1156 let w = compute_equality_weight ty t1 t2 in
1157 let proof = BasicProof p in
1158 let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
1160 | _ -> None, newmeta
1162 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
1163 let o = !Utils.compare_terms t1 t2 in
1164 let w = compute_equality_weight ty t1 t2 in
1165 let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in
1167 | _ -> None, newmeta
1171 let tl, newmeta' = aux newmeta tl in
1172 e::tl, max newmeta newmeta'
1176 aux maxmeta candidates
1180 let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
1181 (* print_endline ("fix_metas " ^ (string_of_int newmeta)); *)
1182 let table = Hashtbl.create (List.length args) in
1183 let is_this_case = ref false in
1184 let newargs, newmeta =
1186 (fun t (newargs, index) ->
1188 | Cic.Meta (i, l) ->
1189 Hashtbl.add table i index;
1190 (* if index = 5469 then ( *)
1191 (* Printf.printf "?5469 COMES FROM (%d): %s\n" *)
1192 (* i (string_of_equality equality); *)
1193 (* print_newline (); *)
1194 (* is_this_case := true *)
1196 ((Cic.Meta (index, l))::newargs, index+1)
1197 | _ -> assert false)
1198 args ([], newmeta+1)
1201 ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
1206 (fun (i, context, term) menv ->
1208 let index = Hashtbl.find table i in
1209 (index, context, term)::menv
1211 (i, context, term)::menv)
1215 and left = repl left
1216 and right = repl right in
1217 let metas = (metas_of_term left) @ (metas_of_term right) in
1218 let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv'
1221 (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
1223 let rec fix_proof = function
1224 | NoProof -> NoProof
1225 | BasicProof term -> BasicProof (repl term)
1226 | ProofBlock (subst, eq_URI, t', (pos, eq), p) ->
1228 (* Printf.printf "fix_proof of equality %s, subst is:\n%s\n" *)
1229 (* (string_of_equality equality) (print_subst subst); *)
1235 | Cic.Meta (i, l) -> (
1237 let j = Hashtbl.find table i in
1238 if List.mem_assoc i subst then
1241 (* let _, context, ty = CicUtil.lookup_meta j menv' in *)
1242 (* (i, (context, Cic.Meta (j, l), ty))::s *)
1243 let _, context, ty = CicUtil.lookup_meta i menv in
1244 (i, (context, Cic.Meta (j, l), ty))::s
1247 | _ -> assert false)
1252 (* (fun (i, e) -> *)
1253 (* try let j = Hashtbl.find table i in (j, e) *)
1254 (* with _ -> (i, e)) subst *)
1257 (* Printf.printf "subst' is:\n%s\n" (print_subst subst'); *)
1258 (* print_newline (); *)
1260 ProofBlock (subst' @ subst, eq_URI, t', (pos, eq), p)
1261 (* | ProofSymBlock (ens, p) -> *)
1262 (* let ens' = List.map (fun (u, t) -> (u, repl t)) ens in *)
1263 (* ProofSymBlock (ens', fix_proof p) *)
1266 (* (newmeta + (List.length newargs) + 2, *)
1267 let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
1268 (* if !is_this_case then ( *)
1269 (* print_endline "\nTHIS IS THE TROUBLE!!!"; *)
1270 (* let pt = build_proof_term neweq in *)
1271 (* Printf.printf "equality: %s\nproof: %s\n" *)
1272 (* (string_of_equality neweq) (CicPp.ppterm pt); *)
1273 (* print_endline (String.make 79 '-'); *)
1275 (newmeta + 1, neweq)
1276 (* (w, fix_proof p, (ty, left, right, o), menv', newargs)) *)
1280 exception TermIsNotAnEquality;;
1282 let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
1283 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
1284 let o = !Utils.compare_terms t1 t2 in
1285 let w = compute_equality_weight ty t1 t2 in
1286 let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
1288 (* (proof, (ty, t1, t2, o), [], []) *)
1290 raise TermIsNotAnEquality
1294 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
1298 let superposition_left (metasenv, context, ugraph) target source =
1299 let module C = Cic in
1300 let module S = CicSubstitution in
1301 let module M = CicMetaSubst in
1302 let module HL = HelmLibraryObjects in
1303 let module CR = CicReduction in
1304 (* we assume that target is ground (does not contain metavariables): this
1305 * should always be the case (I hope, at least) *)
1306 let proof, (eq_ty, left, right, t_order), _, _ = target in
1307 let eqproof, (ty, t1, t2, s_order), newmetas, args = source in
1309 let compare_terms = !Utils.compare_terms in
1314 let where, is_left =
1315 match t_order (* compare_terms left right *) with
1316 | Lt -> right, false
1319 Printf.printf "????????? %s = %s" (CicPp.ppterm left)
1320 (CicPp.ppterm right);
1322 assert false (* again, for ground terms this shouldn't happen... *)
1325 let metasenv' = newmetas @ metasenv in
1326 let result = s_order (* compare_terms t1 t2 *) in
1329 | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
1330 | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
1334 (fun (t, s, m, ug) ->
1335 compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
1336 (beta_expand t1 ty where context metasenv' ugraph)
1339 (fun (t, s, m, ug) ->
1340 compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
1341 (beta_expand t2 ty where context metasenv' ugraph)
1345 (* let what, other = *)
1346 (* if is_left then left, right *)
1347 (* else right, left *)
1349 let build_new what other eq_URI (t, s, m, ug) =
1350 let newgoal, newgoalproof =
1352 | C.Lambda (nn, ty, bo) ->
1353 let bo' = S.subst (M.apply_subst s other) bo in
1356 [C.MutInd (HL.Logic.eq_URI, 0, []);
1358 if is_left then [bo'; S.lift 1 right]
1359 else [S.lift 1 left; bo'])
1361 let t' = C.Lambda (nn, ty, bo'') in
1362 S.subst (M.apply_subst s other) bo,
1364 (C.Appl [C.Const (eq_URI, []); ty; what; t';
1365 proof; other; eqproof])
1369 if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
1370 else (eq_ty, left, newgoal, compare_terms left newgoal)
1372 (newgoalproof (* eqproof *), equation, [], [])
1374 let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
1375 and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
1380 let superposition_right newmeta (metasenv, context, ugraph) target source =
1381 let module C = Cic in
1382 let module S = CicSubstitution in
1383 let module M = CicMetaSubst in
1384 let module HL = HelmLibraryObjects in
1385 let module CR = CicReduction in
1386 let eqproof, (eq_ty, left, right, t_order), newmetas, args = target in
1387 let eqp', (ty', t1, t2, s_order), newm', args' = source in
1388 let maxmeta = ref newmeta in
1390 let compare_terms = !Utils.compare_terms in
1392 if eq_ty <> ty' then
1395 (* let ok term subst other other_eq_side ugraph = *)
1396 (* match term with *)
1397 (* | C.Lambda (nn, ty, bo) -> *)
1398 (* let bo' = S.subst (M.apply_subst subst other) bo in *)
1399 (* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
1401 (* | _ -> assert false *)
1403 let condition left right what other (t, s, m, ug) =
1404 let subst = M.apply_subst s in
1405 let cmp1 = compare_terms (subst what) (subst other) in
1406 let cmp2 = compare_terms (subst left) (subst right) in
1407 (* cmp1 = Gt && cmp2 = Gt *)
1408 cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
1409 (* && (ok t s other right ug) *)
1411 let metasenv' = metasenv @ newmetas @ newm' in
1412 let beta_expand = beta_expand ~metas_ok:false in
1413 let cmp1 = t_order (* compare_terms left right *)
1414 and cmp2 = s_order (* compare_terms t1 t2 *) in
1415 let res1, res2, res3, res4 =
1419 (beta_expand s eq_ty l context metasenv' ugraph)
1421 match cmp1, cmp2 with
1423 (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
1425 [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
1427 [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
1429 [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
1431 let res1 = res left right t1 t2
1432 and res2 = res left right t2 t1 in
1435 let res3 = res right left t1 t2
1436 and res4 = res right left t2 t1 in
1439 let res1 = res left right t1 t2
1440 and res3 = res right left t1 t2 in
1443 let res2 = res left right t2 t1
1444 and res4 = res right left t2 t1 in
1447 let res1 = res left right t1 t2
1448 and res2 = res left right t2 t1
1449 and res3 = res right left t1 t2
1450 and res4 = res right left t2 t1 in
1451 res1, res2, res3, res4
1453 let newmetas = newmetas @ newm' in
1454 let newargs = args @ args' in
1455 let build_new what other is_left eq_URI (t, s, m, ug) =
1456 (* let what, other = *)
1457 (* if is_left then left, right *)
1458 (* else right, left *)
1460 let newterm, neweqproof =
1462 | C.Lambda (nn, ty, bo) ->
1463 let bo' = M.apply_subst s (S.subst other bo) in
1466 [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
1467 if is_left then [bo'; S.lift 1 right]
1468 else [S.lift 1 left; bo'])
1470 let t' = C.Lambda (nn, ty, bo'') in
1473 (C.Appl [C.Const (eq_URI, []); ty; what; t';
1474 eqproof; other; eqp'])
1477 let newmeta, newequality =
1479 if is_left then (newterm, M.apply_subst s right)
1480 else (M.apply_subst s left, newterm) in
1481 let neworder = compare_terms left right in
1483 (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
1488 let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
1489 and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
1490 and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
1491 and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
1493 | _, (_, left, right, _), _, _ ->
1494 not (fst (CR.are_convertible context left right ugraph))
1497 (List.filter ok (new1 @ new2 @ new3 @ new4)))
1502 let is_identity ((_, context, ugraph) as env) = function
1503 | ((_, _, (ty, left, right, _), _, _) as equality) ->
1505 (fst (CicReduction.are_convertible context left right ugraph)))
1510 let demodulation newmeta (metasenv, context, ugraph) target source =
1511 let module C = Cic in
1512 let module S = CicSubstitution in
1513 let module M = CicMetaSubst in
1514 let module HL = HelmLibraryObjects in
1515 let module CR = CicReduction in
1517 let proof, (eq_ty, left, right, t_order), metas, args = target
1518 and proof', (ty, t1, t2, s_order), metas', args' = source in
1520 let compare_terms = !Utils.compare_terms in
1525 let first_step, get_params =
1526 match s_order (* compare_terms t1 t2 *) with
1527 | Gt -> 1, (function
1528 | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
1529 | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
1530 | _ -> assert false)
1531 | Lt -> 1, (function
1532 | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1533 | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1534 | _ -> assert false)
1536 let first_step = 3 in
1537 let get_params step =
1539 | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
1540 | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
1541 | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1542 | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1545 first_step, get_params
1547 let rec demodulate newmeta step metasenv target =
1548 let proof, (eq_ty, left, right, t_order), metas, args = target in
1549 let is_left, what, other, eq_URI = get_params step in
1551 let env = metasenv, context, ugraph in
1552 let names = names_of_context context in
1554 (* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1555 (* (string_of_equality ~env target) (CicPp.pp what names) *)
1556 (* (CicPp.pp other names) (string_of_bool is_left); *)
1557 (* Printf.printf "step: %d" step; *)
1558 (* print_newline (); *)
1560 let ok (t, s, m, ug) =
1561 compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
1564 let r = (beta_expand ~metas_ok:false ~match_only:true
1565 what ty (if is_left then left else right)
1566 context (metasenv @ metas) ugraph)
1568 (* let m' = metas_of_term what *)
1569 (* and m'' = metas_of_term (if is_left then left else right) in *)
1570 (* if (List.mem 527 m'') && (List.mem 6 m') then ( *)
1572 (* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1573 (* (string_of_equality ~env target) (CicPp.pp what names) *)
1574 (* (CicPp.pp other names) (string_of_bool is_left); *)
1575 (* Printf.printf "step: %d" step; *)
1576 (* print_newline (); *)
1577 (* print_endline "res:"; *)
1578 (* List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
1579 (* print_newline (); *)
1580 (* Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
1581 (* print_newline (); *)
1587 if step = 0 then newmeta, target
1588 else demodulate newmeta (step-1) metasenv target
1589 | (t, s, m, ug)::_ ->
1590 let newterm, newproof =
1592 | C.Lambda (nn, ty, bo) ->
1593 (* let bo' = M.apply_subst s (S.subst other bo) in *)
1594 let bo' = S.subst (M.apply_subst s other) bo in
1597 [C.MutInd (HL.Logic.eq_URI, 0, []);
1599 if is_left then [bo'; S.lift 1 right]
1600 else [S.lift 1 left; bo'])
1602 let t' = C.Lambda (nn, ty, bo'') in
1603 (* M.apply_subst s (S.subst other bo), *)
1606 (C.Appl [C.Const (eq_URI, []); ty; what; t';
1607 proof; other; proof'])
1610 let newmeta, newtarget =
1612 (* if is_left then (newterm, M.apply_subst s right) *)
1613 (* else (M.apply_subst s left, newterm) in *)
1614 if is_left then newterm, right
1617 let neworder = compare_terms left right in
1618 (* let newmetasenv = metasenv @ metas in *)
1619 (* let newargs = args @ args' in *)
1620 (* fix_metas newmeta *)
1621 (* (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
1622 let m = (metas_of_term left) @ (metas_of_term right) in
1623 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
1626 (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
1630 (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs)
1633 (* "demodulate, newtarget: %s\ntarget was: %s\n" *)
1634 (* (string_of_equality ~env newtarget) *)
1635 (* (string_of_equality ~env target); *)
1636 (* (\* let _, _, newm, newa = newtarget in *\) *)
1637 (* (\* Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
1638 (* (\* (print_metasenv newm) *\) *)
1639 (* (\* (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
1640 (* print_newline (); *)
1641 if is_identity env newtarget then
1644 demodulate newmeta first_step metasenv newtarget
1646 demodulate newmeta first_step (metasenv @ metas') target
1651 let demodulation newmeta env target source =
1657 let subsumption env target source =
1658 let _, (ty, tl, tr, _), tmetas, _ = target
1659 and _, (ty', sl, sr, _), smetas, _ = source in
1663 let metasenv, context, ugraph = env in
1664 let metasenv = metasenv @ tmetas @ smetas in
1665 let names = names_of_context context in
1666 let samesubst subst subst' =
1667 (* Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
1668 (* (print_subst subst) (print_subst subst'); *)
1669 (* print_newline (); *)
1670 let tbl = Hashtbl.create (List.length subst) in
1671 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
1673 (fun (m, (c, t1, t2)) ->
1675 let c', t1', t2' = Hashtbl.find tbl m in
1676 if (c = c') && (t1 = t1') && (t2 = t2') then true
1682 let subsaux left right left' right' =
1684 let subst, menv, ug = matching metasenv context left left' ugraph
1685 and subst', menv', ug' = matching metasenv context right right' ugraph
1687 (* Printf.printf "left = right: %s = %s\n" *)
1688 (* (CicPp.pp left names) (CicPp.pp right names); *)
1689 (* Printf.printf "left' = right': %s = %s\n" *)
1690 (* (CicPp.pp left' names) (CicPp.pp right' names); *)
1691 samesubst subst subst'
1693 (* print_endline (Printexc.to_string e); *)
1697 if subsaux tl tr sl sr then true
1698 else subsaux tl tr sr sl
1701 Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
1702 (string_of_equality ~env target) (string_of_equality ~env source);
1710 let extract_differing_subterms t1 t2 =
1711 let module C = Cic in
1714 | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
1716 | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
1717 let res = List.concat (List.map2 aux tl1 tl2) in
1719 if res = [] then [(h1, h2)] else [(t1, t2)]
1721 if List.length res > 1 then [(t1, t2)] else res
1723 if t1 <> t2 then [(t1, t2)] else []
1725 let res = aux t1 t2 in