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 *)
15 | BasicProof of Cic.term
17 Cic.substitution * UriManager.uri *
18 (* name, ty, eq_ty, left, right *)
19 (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) *
20 (Utils.pos * equality) * equality
25 let string_of_equality ?env =
29 | w, _, (ty, left, right, o), _, _ ->
30 Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty)
31 (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
33 | Some (_, context, _) -> (
34 let names = names_of_context context in
36 | w, _, (ty, left, right, o), _, _ ->
37 Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names)
38 (CicPp.pp left names) (string_of_comparison o)
39 (CicPp.pp right names)
44 let rec build_term_proof equality =
45 (* Printf.printf "build_term_proof %s" (string_of_equality equality); *)
46 (* print_newline (); *)
47 let _, proof, _, _, _ = equality in
50 Printf.fprintf stderr "WARNING: no proof for %s\n"
51 (string_of_equality equality);
53 | BasicProof term -> term
54 | ProofBlock (subst, eq_URI, t', (pos, eq), eq') ->
55 let name, ty, eq_ty, left, right = t' in
57 Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
60 let t' = Cic.Lambda (name, ty, CicSubstitution.lift 1 bo) in
61 (* Printf.printf " ProofBlock: eq = %s, eq' = %s" *)
62 (* (string_of_equality eq) (string_of_equality eq'); *)
63 (* print_newline (); *)
64 let proof' = build_term_proof eq in
65 let eqproof = build_term_proof eq' in
66 let _, _, (ty, what, other, _), menv', args' = eq in
67 let what, other = if pos = Utils.Left then what, other else other, what in
68 CicMetaSubst.apply_subst subst
69 (Cic.Appl [Cic.Const (eq_URI, []); ty;
70 what; t'; eqproof; other; proof'])
74 let rec metas_of_term = function
75 | Cic.Meta (i, c) -> [i]
78 | Cic.MutInd (_, _, ens)
79 | Cic.MutConstruct (_, _, _, ens) ->
80 List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
83 | Cic.Lambda (_, s, t)
84 | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
85 | Cic.Appl l -> List.flatten (List.map metas_of_term l)
86 | Cic.MutCase (uri, i, s, t, l) ->
87 (metas_of_term s) @ (metas_of_term t) @
88 (List.flatten (List.map metas_of_term l))
91 (List.map (fun (s, i, t1, t2) ->
92 (metas_of_term t1) @ (metas_of_term t2)) il)
93 | Cic.CoFix (i, il) ->
95 (List.map (fun (s, t1, t2) ->
96 (metas_of_term t1) @ (metas_of_term t2)) il)
101 exception NotMetaConvertible;;
103 let meta_convertibility_aux table t1 t2 =
104 let module C = Cic in
108 (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
110 let rec aux ((table_l, table_r) as table) t1 t2 =
111 (* Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *)
112 (* (CicPp.ppterm t1) (CicPp.ppterm t2) *)
113 (* (print_table table_l) (print_table table_r); *)
115 | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
116 let m1_binding, table_l =
117 try List.assoc m1 table_l, table_l
118 with Not_found -> m2, (m1, m2)::table_l
119 and m2_binding, table_r =
120 try List.assoc m2 table_r, table_r
121 with Not_found -> m1, (m2, m1)::table_r
123 (* let m1_binding, m2_binding, table = *)
124 (* let m1b, table = *)
125 (* try List.assoc m1 table, table *)
126 (* with Not_found -> m2, (m1, m2)::table *)
128 (* let m2b, table = *)
129 (* try List.assoc m2 table, table *)
130 (* with Not_found -> m1, (m2, m1)::table *)
132 (* m1b, m2b, table *)
134 (* Printf.printf "table_l: %s\ntable_r: %s\n\n" *)
135 (* (print_table table_l) (print_table table_r); *)
136 if (m1_binding <> m2) || (m2_binding <> m1) then
137 raise NotMetaConvertible
143 | None, Some _ | Some _, None -> raise NotMetaConvertible
145 | Some t1, Some t2 -> (aux res t1 t2))
146 (table_l, table_r) tl1 tl2
147 with Invalid_argument _ ->
148 raise NotMetaConvertible
150 | C.Var (u1, ens1), C.Var (u2, ens2)
151 | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
152 aux_ens table ens1 ens2
153 | C.Cast (s1, t1), C.Cast (s2, t2)
154 | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
155 | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
156 | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
157 let table = aux table s1 s2 in
159 | C.Appl l1, C.Appl l2 -> (
160 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
161 with Invalid_argument _ -> raise NotMetaConvertible
163 | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
164 when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
165 | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
166 when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
167 aux_ens table ens1 ens2
168 | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
169 when (UriManager.eq u1 u2) && i1 = i2 ->
170 let table = aux table s1 s2 in
171 let table = aux table t1 t2 in (
172 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
173 with Invalid_argument _ -> raise NotMetaConvertible
175 | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
178 (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
179 if i1 <> i2 then raise NotMetaConvertible
181 let res = (aux res s1 s2) in aux res t1 t2)
183 with Invalid_argument _ -> raise NotMetaConvertible
185 | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
188 (fun res (n1, s1, t1) (n2, s2, t2) ->
189 let res = aux res s1 s2 in aux res t1 t2)
191 with Invalid_argument _ -> raise NotMetaConvertible
193 | t1, t2 when t1 = t2 -> table
194 | _, _ -> raise NotMetaConvertible
196 and aux_ens table ens1 ens2 =
197 let cmp (u1, t1) (u2, t2) =
198 compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
200 let ens1 = List.sort cmp ens1
201 and ens2 = List.sort cmp ens2 in
204 (fun res (u1, t1) (u2, t2) ->
205 if not (UriManager.eq u1 u2) then raise NotMetaConvertible
208 with Invalid_argument _ -> raise NotMetaConvertible
214 let meta_convertibility_eq eq1 eq2 =
215 let _, _, (ty, left, right, _), _, _ = eq1
216 and _, _, (ty', left', right', _), _, _ = eq2 in
219 else if (left = left') && (right = right') then
221 else if (left = right') && (right = left') then
225 let table = meta_convertibility_aux ([], []) left left' in
226 let _ = meta_convertibility_aux table right right' in
228 with NotMetaConvertible ->
230 let table = meta_convertibility_aux ([], []) left right' in
231 let _ = meta_convertibility_aux table right left' in
233 with NotMetaConvertible ->
238 let meta_convertibility t1 t2 =
242 (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
248 let l, r = meta_convertibility_aux ([], []) t1 t2 in
249 (* Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *)
251 with NotMetaConvertible ->
256 let replace_metas (* context *) term =
257 let module C = Cic in
258 let rec aux = function
261 (* CicMkImplicit.identity_relocation_list_for_metavariable context *)
263 (* if c = irl then *)
264 (* C.Implicit (Some (`MetaIndex i)) *)
266 (* Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *)
267 (* (String.concat "\n" *)
269 (* (function None -> "" | Some t -> CicPp.ppterm t) c)); *)
272 C.Implicit (Some (`MetaInfo (i, c)))
273 | C.Var (u, ens) -> C.Var (u, aux_ens ens)
274 | C.Const (u, ens) -> C.Const (u, aux_ens ens)
275 | C.Cast (s, t) -> C.Cast (aux s, aux t)
276 | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
277 | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
278 | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
279 | C.Appl l -> C.Appl (List.map aux l)
280 | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
281 | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
282 | C.MutCase (uri, i, s, t, l) ->
283 C.MutCase (uri, i, aux s, aux t, List.map aux l)
286 List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
290 List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
294 List.map (fun (u, t) -> (u, aux t)) ens
300 let restore_metas (* context *) term =
301 let module C = Cic in
302 let rec aux = function
303 | C.Implicit (Some (`MetaInfo (i, c))) ->
305 (* CicMkImplicit.identity_relocation_list_for_metavariable context *)
308 (* let local_context:(C.term option) list = *)
309 (* Marshal.from_string mc 0 *)
311 (* C.Meta (i, local_context) *)
313 | C.Var (u, ens) -> C.Var (u, aux_ens ens)
314 | C.Const (u, ens) -> C.Const (u, aux_ens ens)
315 | C.Cast (s, t) -> C.Cast (aux s, aux t)
316 | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
317 | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
318 | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
319 | C.Appl l -> C.Appl (List.map aux l)
320 | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
321 | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
322 | C.MutCase (uri, i, s, t, l) ->
323 C.MutCase (uri, i, aux s, aux t, List.map aux l)
326 List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
330 List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
334 List.map (fun (u, t) -> (u, aux t)) ens
340 let rec restore_subst (* context *) subst =
342 (fun (i, (c, t, ty)) ->
343 i, (c, restore_metas (* context *) t, ty))
348 let rec check_irl start = function
350 | None::tl -> check_irl (start+1) tl
351 | (Some (Cic.Rel x))::tl ->
352 if x = start then check_irl (start+1) tl else false
356 let rec is_simple_term = function
357 | Cic.Appl ((Cic.Meta _)::_) -> false
358 | Cic.Appl l -> List.for_all is_simple_term l
359 | Cic.Meta (i, l) -> check_irl 1 l
365 let lookup_subst meta subst =
367 | Cic.Meta (i, _) -> (
368 try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
369 with Not_found -> meta
375 let unification_simple metasenv context t1 t2 ugraph =
376 let module C = Cic in
377 let module M = CicMetaSubst in
378 let module U = CicUnification in
379 let lookup = lookup_subst in
380 let rec occurs_check subst what where =
381 (* Printf.printf "occurs_check %s %s" *)
382 (* (CicPp.ppterm what) (CicPp.ppterm where); *)
383 (* print_newline (); *)
385 | t when what = t -> true
386 | C.Appl l -> List.exists (occurs_check subst what) l
388 let t = lookup where subst in
389 if t <> where then occurs_check subst what t else false
392 let rec unif subst menv s t =
393 (* Printf.printf "unif %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
394 (* (print_subst subst); *)
395 (* print_newline (); *)
396 let s = match s with C.Meta _ -> lookup s subst | _ -> s
397 and t = match t with C.Meta _ -> lookup t subst | _ -> t
399 (* Printf.printf "after apply_subst: %s %s\n%s" *)
400 (* (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
401 (* print_newline (); *)
403 | s, t when s = t -> subst, menv
404 | C.Meta (i, _), C.Meta (j, _) when i > j ->
406 | C.Meta _, t when occurs_check subst s t ->
407 raise (U.UnificationFailure "Inference.unification.unif")
408 (* | C.Meta (i, l), C.Meta (j, l') -> *)
409 (* let _, _, ty = CicUtil.lookup_meta i menv in *)
410 (* let _, _, ty' = CicUtil.lookup_meta j menv in *)
411 (* let binding1 = lookup s subst in *)
412 (* let binding2 = lookup t subst in *)
413 (* let subst, menv = *)
414 (* if binding1 != s then *)
415 (* if binding2 != t then *)
416 (* unif subst menv binding1 binding2 *)
418 (* if binding1 = t then *)
421 (* ((j, (context, binding1, ty'))::subst, *)
422 (* List.filter (fun (m, _, _) -> j <> m) menv) *)
424 (* if binding2 != t then *)
425 (* if s = binding2 then *)
428 (* ((i, (context, binding2, ty))::subst, *)
429 (* List.filter (fun (m, _, _) -> i <> m) menv) *)
431 (* ((i, (context, t, ty))::subst, *)
432 (* List.filter (fun (m, _, _) -> i <> m) menv) *)
436 | C.Meta (i, l), t ->
437 let _, _, ty = CicUtil.lookup_meta i menv in
439 if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
442 let menv = List.filter (fun (m, _, _) -> i <> m) menv in
444 | _, C.Meta _ -> unif subst menv t s
445 | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
446 raise (U.UnificationFailure "Inference.unification.unif")
447 | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
450 (fun (subst', menv) s t -> unif subst' menv s t)
451 (subst, menv) tls tlt
453 raise (U.UnificationFailure "Inference.unification.unif")
455 | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
457 let subst, menv = unif [] metasenv t1 t2 in
458 (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
459 (* print_newline (); *)
460 (* let rec fix_term = function *)
461 (* | (C.Meta (i, l) as t) -> *)
463 (* | C.Appl l -> C.Appl (List.map fix_term l) *)
466 (* let rec fix_subst = function *)
468 (* | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl) *)
470 (* List.rev (fix_subst subst), menv, ugraph *)
471 List.rev subst, menv, ugraph
475 let unification metasenv context t1 t2 ugraph =
476 (* Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
477 let subst, menv, ug =
478 if not (is_simple_term t1) || not (is_simple_term t2) then
479 CicUnification.fo_unif metasenv context t1 t2 ugraph
481 unification_simple metasenv context t1 t2 ugraph
483 let rec fix_term = function
484 | (Cic.Meta (i, l) as t) ->
485 let t' = lookup_subst t subst in
486 if t <> t' then fix_term t' else t
487 | Cic.Appl l -> Cic.Appl (List.map fix_term l)
490 let rec fix_subst = function
492 | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
494 (* Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
495 (* print_endline "|"; *)
496 (* fix_subst *) subst, menv, ug
499 (* let unification = CicUnification.fo_unif;; *)
501 exception MatchingFailure;;
504 let matching_simple metasenv context t1 t2 ugraph =
505 let module C = Cic in
506 let module M = CicMetaSubst in
507 let module U = CicUnification in
508 let lookup meta subst =
511 try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
512 with Not_found -> meta
516 let rec do_match subst menv s t =
517 (* Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
518 (* (print_subst subst); *)
519 (* print_newline (); *)
520 (* let s = match s with C.Meta _ -> lookup s subst | _ -> s *)
521 (* let t = match t with C.Meta _ -> lookup t subst | _ -> t in *)
522 (* Printf.printf "after apply_subst: %s %s\n%s" *)
523 (* (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
524 (* print_newline (); *)
526 | s, t when s = t -> subst, menv
527 (* | C.Meta (i, _), C.Meta (j, _) when i > j -> *)
528 (* do_match subst menv t s *)
529 (* | C.Meta _, t when occurs_check subst s t -> *)
530 (* raise MatchingFailure *)
531 (* | s, C.Meta _ when occurs_check subst t s -> *)
532 (* raise MatchingFailure *)
533 | s, C.Meta (i, l) ->
534 let filter_menv i menv =
535 List.filter (fun (m, _, _) -> i <> m) menv
538 let value = lookup t subst in
540 (* | C.Meta (i', l') when Hashtbl.mem table i' -> *)
541 (* (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *)
542 | value when value = t ->
543 let _, _, ty = CicUtil.lookup_meta i menv in
544 (i, (context, s, ty))::subst, filter_menv i menv
545 | value when value <> s ->
546 raise MatchingFailure
547 | value -> do_match subst menv s value
550 (* else if value <> s then *)
551 (* raise MatchingFailure *)
553 (* if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst *)
556 (* let menv = List.filter (fun (m, _, _) -> i <> m) menv in *)
558 (* | _, C.Meta _ -> do_match subst menv t s *)
559 (* | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *)
560 (* raise MatchingFailure *)
561 | C.Appl ls, C.Appl lt -> (
564 (fun (subst, menv) s t -> do_match subst menv s t)
567 (* print_endline (Printexc.to_string e); *)
568 (* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
569 (* print_newline (); *)
570 raise MatchingFailure
573 (* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
574 (* print_newline (); *)
575 raise MatchingFailure
577 let subst, menv = do_match [] metasenv t1 t2 in
578 (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
579 (* print_newline (); *)
584 let matching metasenv context t1 t2 ugraph =
585 (* if (is_simple_term t1) && (is_simple_term t2) then *)
586 (* let subst, menv, ug = *)
587 (* matching_simple metasenv context t1 t2 ugraph in *)
588 (* (\* Printf.printf "matching %s %s:\n%s\n" *\) *)
589 (* (\* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *)
590 (* (\* print_newline (); *\) *)
591 (* subst, menv, ug *)
594 let subst, metasenv, ugraph =
595 (* CicUnification.fo_unif metasenv context t1 t2 ugraph *)
596 unification metasenv context t1 t2 ugraph
598 let t' = CicMetaSubst.apply_subst subst t1 in
599 if not (meta_convertibility t1 t') then
600 raise MatchingFailure
602 let metas = metas_of_term t1 in
603 let fix_subst = function
604 | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
605 (j, (c, Cic.Meta (i, lc), ty))
608 let subst = List.map fix_subst subst in
610 (* Printf.printf "matching %s %s:\n%s\n" *)
611 (* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *)
612 (* print_newline (); *)
614 subst, metasenv, ugraph
616 (* Printf.printf "failed to match %s %s\n" *)
617 (* (CicPp.ppterm t1) (CicPp.ppterm t2); *)
618 raise MatchingFailure
622 (* let profile = CicUtil.profile "Inference.matching" in *)
623 (* (fun metasenv context t1 t2 ugraph -> *)
624 (* profile (matching metasenv context t1 t2) ugraph) *)
628 let beta_expand ?(metas_ok=true) ?(match_only=false)
629 what type_of_what where context metasenv ugraph =
630 let module S = CicSubstitution in
631 let module C = Cic in
633 let print_info = false in
636 (* let names = names_of_context context in *)
637 (* Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
638 (* (CicPp.pp what names) (CicPp.ppterm what) *)
639 (* (CicPp.pp where names) (CicPp.ppterm where); *)
640 (* print_newline (); *)
644 ((list of all possible beta expansions, subst, metasenv, ugraph),
647 let rec aux lift_amount term context metasenv subst ugraph =
648 (* Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
649 let res, lifted_term =
652 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
654 | C.Var (uri, exp_named_subst) ->
655 let ens', lifted_ens =
656 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
660 (fun (e, s, m, ug) ->
661 (C.Var (uri, e), s, m, ug)) ens'
663 expansions, C.Var (uri, lifted_ens)
668 (fun arg (res, lifted_tl) ->
671 let arg_res, lifted_arg =
672 aux lift_amount arg context metasenv subst ugraph in
675 (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
680 (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
682 (Some lifted_arg)::lifted_tl)
685 (fun (r, s, m, ug) -> None::r, s, m, ug)
692 (fun (l, s, m, ug) ->
693 (C.Meta (i, l), s, m, ug)) l'
695 e, C.Meta (i, lifted_l)
698 | C.Implicit _ as t -> [], t
702 aux lift_amount s context metasenv subst ugraph in
704 aux lift_amount t context metasenv subst ugraph
708 (fun (t, s, m, ug) ->
709 C.Cast (t, lifted_t), s, m, ug) l1 in
712 (fun (t, s, m, ug) ->
713 C.Cast (lifted_s, t), s, m, ug) l2 in
714 l1'@l2', C.Cast (lifted_s, lifted_t)
716 | C.Prod (nn, s, t) ->
718 aux lift_amount s context metasenv subst ugraph in
720 aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
721 metasenv subst ugraph
725 (fun (t, s, m, ug) ->
726 C.Prod (nn, t, lifted_t), s, m, ug) l1 in
729 (fun (t, s, m, ug) ->
730 C.Prod (nn, lifted_s, t), s, m, ug) l2 in
731 l1'@l2', C.Prod (nn, lifted_s, lifted_t)
733 | C.Lambda (nn, s, t) ->
735 aux lift_amount s context metasenv subst ugraph in
737 aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
738 metasenv subst ugraph
742 (fun (t, s, m, ug) ->
743 C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
746 (fun (t, s, m, ug) ->
747 C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
748 l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
750 | C.LetIn (nn, s, t) ->
752 aux lift_amount s context metasenv subst ugraph in
754 aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
755 metasenv subst ugraph
759 (fun (t, s, m, ug) ->
760 C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
763 (fun (t, s, m, ug) ->
764 C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
765 l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
769 aux_list lift_amount l context metasenv subst ugraph
771 (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
774 | C.Const (uri, exp_named_subst) ->
775 let ens', lifted_ens =
776 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
780 (fun (e, s, m, ug) ->
781 (C.Const (uri, e), s, m, ug)) ens'
783 (expansions, C.Const (uri, lifted_ens))
785 | C.MutInd (uri, i ,exp_named_subst) ->
786 let ens', lifted_ens =
787 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
791 (fun (e, s, m, ug) ->
792 (C.MutInd (uri, i, e), s, m, ug)) ens'
794 (expansions, C.MutInd (uri, i, lifted_ens))
796 | C.MutConstruct (uri, i, j, exp_named_subst) ->
797 let ens', lifted_ens =
798 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
802 (fun (e, s, m, ug) ->
803 (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
805 (expansions, C.MutConstruct (uri, i, j, lifted_ens))
807 | C.MutCase (sp, i, outt, t, pl) ->
808 let pl_res, lifted_pl =
809 aux_list lift_amount pl context metasenv subst ugraph
811 let l1, lifted_outt =
812 aux lift_amount outt context metasenv subst ugraph in
814 aux lift_amount t context metasenv subst ugraph in
818 (fun (outt, s, m, ug) ->
819 C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
822 (fun (t, s, m, ug) ->
823 C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
826 (fun (pl, s, m, ug) ->
827 C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
829 (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
832 let len = List.length fl in
835 (fun (nm, idx, ty, bo) (res, lifted_tl) ->
836 let lifted_ty = S.lift lift_amount ty in
837 let bo_res, lifted_bo =
838 aux (lift_amount+len) bo context metasenv subst ugraph in
841 (fun (a, s, m, ug) ->
842 (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
847 (fun (r, s, m, ug) ->
848 (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
849 (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
853 (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
854 C.Fix (i, lifted_fl))
857 let len = List.length fl in
860 (fun (nm, ty, bo) (res, lifted_tl) ->
861 let lifted_ty = S.lift lift_amount ty in
862 let bo_res, lifted_bo =
863 aux (lift_amount+len) bo context metasenv subst ugraph in
866 (fun (a, s, m, ug) ->
867 (nm, lifted_ty, a)::lifted_tl, s, m, ug)
872 (fun (r, s, m, ug) ->
873 (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
874 (nm, lifted_ty, lifted_bo)::lifted_tl)
878 (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
879 C.CoFix (i, lifted_fl))
883 | C.Meta _ when (not metas_ok) ->
887 (* if match_only then replace_metas context term *)
891 let subst', metasenv', ugraph' =
892 (* Printf.printf "provo a unificare %s e %s\n" *)
893 (* (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
895 matching metasenv context term (S.lift lift_amount what) ugraph
897 CicUnification.fo_unif metasenv context
898 (S.lift lift_amount what) term ugraph
900 (* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
901 (* (CicPp.ppterm (S.lift lift_amount what)); *)
902 (* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
903 (* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
904 (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
905 (* if match_only then *)
906 (* let t' = CicMetaSubst.apply_subst subst' term in *)
907 (* if not (meta_convertibility term t') then ( *)
908 (* res, lifted_term *)
910 (* let metas = metas_of_term term in *)
911 (* let fix_subst = function *)
912 (* | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
913 (* (j, (c, C.Meta (i, lc), ty)) *)
916 (* let subst' = List.map fix_subst subst' in *)
917 (* ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
921 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
925 print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e));
929 (* Printf.printf "exit aux\n"; *)
932 and aux_list lift_amount l context metasenv subst ugraph =
934 (fun arg (res, lifted_tl) ->
935 let arg_res, lifted_arg =
936 aux lift_amount arg context metasenv subst ugraph in
938 (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
941 (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
942 lifted_arg::lifted_tl)
945 and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
947 (fun (u, arg) (res, lifted_tl) ->
948 let arg_res, lifted_arg =
949 aux lift_amount arg context metasenv subst ugraph in
952 (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
954 (l1 @ (List.map (fun (r, s, m, ug) ->
955 (u, lifted_arg)::r, s, m, ug) res),
956 (u, lifted_arg)::lifted_tl)
957 ) exp_named_subst ([], [])
962 (* if match_only then replace_metas (\* context *\) where *)
966 Printf.printf "searching %s inside %s\n"
967 (CicPp.ppterm what) (CicPp.ppterm where);
969 aux 0 where context metasenv [] ugraph
972 (* if match_only then *)
973 (* (fun (term, subst, metasenv, ugraph) -> *)
975 (* C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
976 (* and subst = restore_subst subst in *)
977 (* (term', subst, metasenv, ugraph)) *)
979 (fun (term, subst, metasenv, ugraph) ->
980 let term' = C.Lambda (C.Anonymous, type_of_what, term) in
981 (term', subst, metasenv, ugraph))
983 List.map mapfun expansions
987 let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
988 let module C = Cic in
989 let module S = CicSubstitution in
990 let module T = CicTypeChecker in
991 let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
992 let rec aux index newmeta = function
994 | (Some (_, C.Decl (term)))::tl ->
995 let do_find context term =
997 | C.Prod (name, s, t) ->
998 (* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
999 let (head, newmetas, args, _) =
1000 PrimitiveTactics.new_metasenv_for_apply newmeta proof
1001 context (S.lift index term)
1007 | C.Meta (i, _) -> (max maxm i)
1008 | _ -> assert false)
1012 if List.length args = 0 then
1015 C.Appl ((C.Rel index)::args)
1018 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
1019 Printf.printf "OK: %s\n" (CicPp.ppterm term);
1020 let o = !Utils.compare_terms t1 t2 in
1021 let w = compute_equality_weight ty t1 t2 in
1022 let proof = BasicProof p in
1023 let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
1025 | _ -> None, newmeta
1027 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
1028 let t1 = S.lift index t1
1029 and t2 = S.lift index t2 in
1030 let o = !Utils.compare_terms t1 t2 in
1031 let w = compute_equality_weight ty t1 t2 in
1032 let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in
1034 | _ -> None, newmeta
1036 match do_find context term with
1037 | Some p, newmeta ->
1038 let tl, newmeta' = (aux (index+1) newmeta tl) in
1039 p::tl, max newmeta newmeta'
1041 aux (index+1) newmeta tl
1044 aux (index+1) newmeta tl
1046 aux 1 newmeta context
1050 let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
1051 let table = Hashtbl.create (List.length args) in
1054 (fun t (newargs, index) ->
1056 | Cic.Meta (i, l) ->
1057 Hashtbl.add table i index;
1058 ((Cic.Meta (index, l))::newargs, index+1)
1059 | _ -> assert false)
1063 ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
1068 (fun (i, context, term) menv ->
1070 let index = Hashtbl.find table i in
1071 (index, context, term)::menv
1073 (i, context, term)::menv)
1077 and left = repl left
1078 and right = repl right in
1079 let metas = (metas_of_term left) @ (metas_of_term right) in
1080 let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv'
1083 (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
1085 (newmeta + (List.length newargs) + 1,
1086 (w, p, (ty, left, right, o), menv', newargs))
1090 exception TermIsNotAnEquality;;
1092 let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
1093 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
1094 let o = !Utils.compare_terms t1 t2 in
1095 let w = compute_equality_weight ty t1 t2 in
1096 let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
1098 (* (proof, (ty, t1, t2, o), [], []) *)
1100 raise TermIsNotAnEquality
1104 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
1108 let superposition_left (metasenv, context, ugraph) target source =
1109 let module C = Cic in
1110 let module S = CicSubstitution in
1111 let module M = CicMetaSubst in
1112 let module HL = HelmLibraryObjects in
1113 let module CR = CicReduction in
1114 (* we assume that target is ground (does not contain metavariables): this
1115 * should always be the case (I hope, at least) *)
1116 let proof, (eq_ty, left, right, t_order), _, _ = target in
1117 let eqproof, (ty, t1, t2, s_order), newmetas, args = source in
1119 let compare_terms = !Utils.compare_terms in
1124 let where, is_left =
1125 match t_order (* compare_terms left right *) with
1126 | Lt -> right, false
1129 Printf.printf "????????? %s = %s" (CicPp.ppterm left)
1130 (CicPp.ppterm right);
1132 assert false (* again, for ground terms this shouldn't happen... *)
1135 let metasenv' = newmetas @ metasenv in
1136 let result = s_order (* compare_terms t1 t2 *) in
1139 | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
1140 | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
1144 (fun (t, s, m, ug) ->
1145 compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
1146 (beta_expand t1 ty where context metasenv' ugraph)
1149 (fun (t, s, m, ug) ->
1150 compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
1151 (beta_expand t2 ty where context metasenv' ugraph)
1155 (* let what, other = *)
1156 (* if is_left then left, right *)
1157 (* else right, left *)
1159 let build_new what other eq_URI (t, s, m, ug) =
1160 let newgoal, newgoalproof =
1162 | C.Lambda (nn, ty, bo) ->
1163 let bo' = S.subst (M.apply_subst s other) bo in
1166 [C.MutInd (HL.Logic.eq_URI, 0, []);
1168 if is_left then [bo'; S.lift 1 right]
1169 else [S.lift 1 left; bo'])
1171 let t' = C.Lambda (nn, ty, bo'') in
1172 S.subst (M.apply_subst s other) bo,
1174 (C.Appl [C.Const (eq_URI, []); ty; what; t';
1175 proof; other; eqproof])
1179 if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
1180 else (eq_ty, left, newgoal, compare_terms left newgoal)
1182 (newgoalproof (* eqproof *), equation, [], [])
1184 let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
1185 and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
1190 let superposition_right newmeta (metasenv, context, ugraph) target source =
1191 let module C = Cic in
1192 let module S = CicSubstitution in
1193 let module M = CicMetaSubst in
1194 let module HL = HelmLibraryObjects in
1195 let module CR = CicReduction in
1196 let eqproof, (eq_ty, left, right, t_order), newmetas, args = target in
1197 let eqp', (ty', t1, t2, s_order), newm', args' = source in
1198 let maxmeta = ref newmeta in
1200 let compare_terms = !Utils.compare_terms in
1202 if eq_ty <> ty' then
1205 (* let ok term subst other other_eq_side ugraph = *)
1206 (* match term with *)
1207 (* | C.Lambda (nn, ty, bo) -> *)
1208 (* let bo' = S.subst (M.apply_subst subst other) bo in *)
1209 (* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
1211 (* | _ -> assert false *)
1213 let condition left right what other (t, s, m, ug) =
1214 let subst = M.apply_subst s in
1215 let cmp1 = compare_terms (subst what) (subst other) in
1216 let cmp2 = compare_terms (subst left) (subst right) in
1217 (* cmp1 = Gt && cmp2 = Gt *)
1218 cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
1219 (* && (ok t s other right ug) *)
1221 let metasenv' = metasenv @ newmetas @ newm' in
1222 let beta_expand = beta_expand ~metas_ok:false in
1223 let cmp1 = t_order (* compare_terms left right *)
1224 and cmp2 = s_order (* compare_terms t1 t2 *) in
1225 let res1, res2, res3, res4 =
1229 (beta_expand s eq_ty l context metasenv' ugraph)
1231 match cmp1, cmp2 with
1233 (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
1235 [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
1237 [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
1239 [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
1241 let res1 = res left right t1 t2
1242 and res2 = res left right t2 t1 in
1245 let res3 = res right left t1 t2
1246 and res4 = res right left t2 t1 in
1249 let res1 = res left right t1 t2
1250 and res3 = res right left t1 t2 in
1253 let res2 = res left right t2 t1
1254 and res4 = res right left t2 t1 in
1257 let res1 = res left right t1 t2
1258 and res2 = res left right t2 t1
1259 and res3 = res right left t1 t2
1260 and res4 = res right left t2 t1 in
1261 res1, res2, res3, res4
1263 let newmetas = newmetas @ newm' in
1264 let newargs = args @ args' in
1265 let build_new what other is_left eq_URI (t, s, m, ug) =
1266 (* let what, other = *)
1267 (* if is_left then left, right *)
1268 (* else right, left *)
1270 let newterm, neweqproof =
1272 | C.Lambda (nn, ty, bo) ->
1273 let bo' = M.apply_subst s (S.subst other bo) in
1276 [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
1277 if is_left then [bo'; S.lift 1 right]
1278 else [S.lift 1 left; bo'])
1280 let t' = C.Lambda (nn, ty, bo'') in
1283 (C.Appl [C.Const (eq_URI, []); ty; what; t';
1284 eqproof; other; eqp'])
1287 let newmeta, newequality =
1289 if is_left then (newterm, M.apply_subst s right)
1290 else (M.apply_subst s left, newterm) in
1291 let neworder = compare_terms left right in
1293 (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
1298 let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
1299 and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
1300 and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
1301 and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
1303 | _, (_, left, right, _), _, _ ->
1304 not (fst (CR.are_convertible context left right ugraph))
1307 (List.filter ok (new1 @ new2 @ new3 @ new4)))
1312 let is_identity ((_, context, ugraph) as env) = function
1313 | ((_, _, (ty, left, right, _), _, _) as equality) ->
1315 (fst (CicReduction.are_convertible context left right ugraph)))
1320 let demodulation newmeta (metasenv, context, ugraph) target source =
1321 let module C = Cic in
1322 let module S = CicSubstitution in
1323 let module M = CicMetaSubst in
1324 let module HL = HelmLibraryObjects in
1325 let module CR = CicReduction in
1327 let proof, (eq_ty, left, right, t_order), metas, args = target
1328 and proof', (ty, t1, t2, s_order), metas', args' = source in
1330 let compare_terms = !Utils.compare_terms in
1335 let first_step, get_params =
1336 match s_order (* compare_terms t1 t2 *) with
1337 | Gt -> 1, (function
1338 | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
1339 | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
1340 | _ -> assert false)
1341 | Lt -> 1, (function
1342 | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1343 | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1344 | _ -> assert false)
1346 let first_step = 3 in
1347 let get_params step =
1349 | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
1350 | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
1351 | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1352 | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1355 first_step, get_params
1357 let rec demodulate newmeta step metasenv target =
1358 let proof, (eq_ty, left, right, t_order), metas, args = target in
1359 let is_left, what, other, eq_URI = get_params step in
1361 let env = metasenv, context, ugraph in
1362 let names = names_of_context context in
1364 (* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1365 (* (string_of_equality ~env target) (CicPp.pp what names) *)
1366 (* (CicPp.pp other names) (string_of_bool is_left); *)
1367 (* Printf.printf "step: %d" step; *)
1368 (* print_newline (); *)
1370 let ok (t, s, m, ug) =
1371 compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
1374 let r = (beta_expand ~metas_ok:false ~match_only:true
1375 what ty (if is_left then left else right)
1376 context (metasenv @ metas) ugraph)
1378 (* let m' = metas_of_term what *)
1379 (* and m'' = metas_of_term (if is_left then left else right) in *)
1380 (* if (List.mem 527 m'') && (List.mem 6 m') then ( *)
1382 (* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1383 (* (string_of_equality ~env target) (CicPp.pp what names) *)
1384 (* (CicPp.pp other names) (string_of_bool is_left); *)
1385 (* Printf.printf "step: %d" step; *)
1386 (* print_newline (); *)
1387 (* print_endline "res:"; *)
1388 (* List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
1389 (* print_newline (); *)
1390 (* Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
1391 (* print_newline (); *)
1397 if step = 0 then newmeta, target
1398 else demodulate newmeta (step-1) metasenv target
1399 | (t, s, m, ug)::_ ->
1400 let newterm, newproof =
1402 | C.Lambda (nn, ty, bo) ->
1403 (* let bo' = M.apply_subst s (S.subst other bo) in *)
1404 let bo' = S.subst (M.apply_subst s other) bo in
1407 [C.MutInd (HL.Logic.eq_URI, 0, []);
1409 if is_left then [bo'; S.lift 1 right]
1410 else [S.lift 1 left; bo'])
1412 let t' = C.Lambda (nn, ty, bo'') in
1413 (* M.apply_subst s (S.subst other bo), *)
1416 (C.Appl [C.Const (eq_URI, []); ty; what; t';
1417 proof; other; proof'])
1420 let newmeta, newtarget =
1422 (* if is_left then (newterm, M.apply_subst s right) *)
1423 (* else (M.apply_subst s left, newterm) in *)
1424 if is_left then newterm, right
1427 let neworder = compare_terms left right in
1428 (* let newmetasenv = metasenv @ metas in *)
1429 (* let newargs = args @ args' in *)
1430 (* fix_metas newmeta *)
1431 (* (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
1432 let m = (metas_of_term left) @ (metas_of_term right) in
1433 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
1436 (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
1440 (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs)
1443 (* "demodulate, newtarget: %s\ntarget was: %s\n" *)
1444 (* (string_of_equality ~env newtarget) *)
1445 (* (string_of_equality ~env target); *)
1446 (* (\* let _, _, newm, newa = newtarget in *\) *)
1447 (* (\* Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
1448 (* (\* (print_metasenv newm) *\) *)
1449 (* (\* (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
1450 (* print_newline (); *)
1451 if is_identity env newtarget then
1454 demodulate newmeta first_step metasenv newtarget
1456 demodulate newmeta first_step (metasenv @ metas') target
1461 let demodulation newmeta env target source =
1467 let subsumption env target source =
1468 let _, (ty, tl, tr, _), tmetas, _ = target
1469 and _, (ty', sl, sr, _), smetas, _ = source in
1473 let metasenv, context, ugraph = env in
1474 let metasenv = metasenv @ tmetas @ smetas in
1475 let names = names_of_context context in
1476 let samesubst subst subst' =
1477 (* Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
1478 (* (print_subst subst) (print_subst subst'); *)
1479 (* print_newline (); *)
1480 let tbl = Hashtbl.create (List.length subst) in
1481 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
1483 (fun (m, (c, t1, t2)) ->
1485 let c', t1', t2' = Hashtbl.find tbl m in
1486 if (c = c') && (t1 = t1') && (t2 = t2') then true
1492 let subsaux left right left' right' =
1494 let subst, menv, ug = matching metasenv context left left' ugraph
1495 and subst', menv', ug' = matching metasenv context right right' ugraph
1497 (* Printf.printf "left = right: %s = %s\n" *)
1498 (* (CicPp.pp left names) (CicPp.pp right names); *)
1499 (* Printf.printf "left' = right': %s = %s\n" *)
1500 (* (CicPp.pp left' names) (CicPp.pp right' names); *)
1501 samesubst subst subst'
1503 (* print_endline (Printexc.to_string e); *)
1507 if subsaux tl tr sl sr then true
1508 else subsaux tl tr sr sl
1511 Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
1512 (string_of_equality ~env target) (string_of_equality ~env source);
1520 let extract_differing_subterms t1 t2 =
1521 let module C = Cic in
1524 | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
1526 | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
1527 let res = List.concat (List.map2 aux tl1 tl2) in
1529 if res = [] then [(h1, h2)] else [(t1, t2)]
1531 if List.length res > 1 then [(t1, t2)] else res
1533 if t1 <> t2 then [(t1, t2)] else []
1535 let res = aux t1 t2 in