4 let string_of_equality ?env =
8 | _, (ty, left, right, o), _, _ ->
9 Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.ppterm ty)
10 (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
12 | Some (_, context, _) -> (
13 let names = names_of_context context in
15 | _, (ty, left, right, o), _, _ ->
16 Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.pp ty names)
17 (CicPp.pp left names) (string_of_comparison o)
18 (CicPp.pp right names)
23 let rec metas_of_term = function
24 | Cic.Meta (i, c) -> [i]
27 | Cic.MutInd (_, _, ens)
28 | Cic.MutConstruct (_, _, _, ens) ->
29 List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
32 | Cic.Lambda (_, s, t)
33 | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
34 | Cic.Appl l -> List.flatten (List.map metas_of_term l)
35 | Cic.MutCase (uri, i, s, t, l) ->
36 (metas_of_term s) @ (metas_of_term t) @
37 (List.flatten (List.map metas_of_term l))
40 (List.map (fun (s, i, t1, t2) ->
41 (metas_of_term t1) @ (metas_of_term t2)) il)
42 | Cic.CoFix (i, il) ->
44 (List.map (fun (s, t1, t2) ->
45 (metas_of_term t1) @ (metas_of_term t2)) il)
50 exception NotMetaConvertible;;
52 let meta_convertibility_aux table t1 t2 =
57 (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
59 let rec aux ((table_l, table_r) as table) t1 t2 =
60 (* Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *)
61 (* (CicPp.ppterm t1) (CicPp.ppterm t2) *)
62 (* (print_table table_l) (print_table table_r); *)
64 | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
65 let m1_binding, table_l =
66 try List.assoc m1 table_l, table_l
67 with Not_found -> m2, (m1, m2)::table_l
68 and m2_binding, table_r =
69 try List.assoc m2 table_r, table_r
70 with Not_found -> m1, (m2, m1)::table_r
72 (* let m1_binding, m2_binding, table = *)
73 (* let m1b, table = *)
74 (* try List.assoc m1 table, table *)
75 (* with Not_found -> m2, (m1, m2)::table *)
77 (* let m2b, table = *)
78 (* try List.assoc m2 table, table *)
79 (* with Not_found -> m1, (m2, m1)::table *)
83 (* Printf.printf "table_l: %s\ntable_r: %s\n\n" *)
84 (* (print_table table_l) (print_table table_r); *)
85 if (m1_binding <> m2) || (m2_binding <> m1) then
86 raise NotMetaConvertible
92 | None, Some _ | Some _, None -> raise NotMetaConvertible
94 | Some t1, Some t2 -> (aux res t1 t2))
95 (table_l, table_r) tl1 tl2
96 with Invalid_argument _ ->
97 raise NotMetaConvertible
99 | C.Var (u1, ens1), C.Var (u2, ens2)
100 | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
101 aux_ens table ens1 ens2
102 | C.Cast (s1, t1), C.Cast (s2, t2)
103 | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
104 | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
105 | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
106 let table = aux table s1 s2 in
108 | C.Appl l1, C.Appl l2 -> (
109 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
110 with Invalid_argument _ -> raise NotMetaConvertible
112 | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
113 when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
114 | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
115 when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
116 aux_ens table ens1 ens2
117 | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
118 when (UriManager.eq u1 u2) && i1 = i2 ->
119 let table = aux table s1 s2 in
120 let table = aux table t1 t2 in (
121 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
122 with Invalid_argument _ -> raise NotMetaConvertible
124 | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
127 (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
128 if i1 <> i2 then raise NotMetaConvertible
130 let res = (aux res s1 s2) in aux res t1 t2)
132 with Invalid_argument _ -> raise NotMetaConvertible
134 | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
137 (fun res (n1, s1, t1) (n2, s2, t2) ->
138 let res = aux res s1 s2 in aux res t1 t2)
140 with Invalid_argument _ -> raise NotMetaConvertible
142 | t1, t2 when t1 = t2 -> table
143 | _, _ -> raise NotMetaConvertible
145 and aux_ens table ens1 ens2 =
146 let cmp (u1, t1) (u2, t2) =
147 compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
149 let ens1 = List.sort cmp ens1
150 and ens2 = List.sort cmp ens2 in
153 (fun res (u1, t1) (u2, t2) ->
154 if not (UriManager.eq u1 u2) then raise NotMetaConvertible
157 with Invalid_argument _ -> raise NotMetaConvertible
163 let meta_convertibility_eq eq1 eq2 =
164 let _, (ty, left, right, _), _, _ = eq1
165 and _, (ty', left', right', _), _, _ = eq2 in
168 else if (left = left') && (right = right') then
170 else if (left = right') && (right = left') then
174 let table = meta_convertibility_aux ([], []) left left' in
175 let _ = meta_convertibility_aux table right right' in
177 with NotMetaConvertible ->
179 let table = meta_convertibility_aux ([], []) left right' in
180 let _ = meta_convertibility_aux table right left' in
182 with NotMetaConvertible ->
187 let meta_convertibility t1 t2 =
191 (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
197 let l, r = meta_convertibility_aux ([], []) t1 t2 in
198 (* Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *)
200 with NotMetaConvertible ->
205 let replace_metas (* context *) term =
206 let module C = Cic in
207 let rec aux = function
210 (* CicMkImplicit.identity_relocation_list_for_metavariable context *)
212 (* if c = irl then *)
213 (* C.Implicit (Some (`MetaIndex i)) *)
215 (* Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *)
216 (* (String.concat "\n" *)
218 (* (function None -> "" | Some t -> CicPp.ppterm t) c)); *)
221 C.Implicit (Some (`MetaInfo (i, c)))
222 | C.Var (u, ens) -> C.Var (u, aux_ens ens)
223 | C.Const (u, ens) -> C.Const (u, aux_ens ens)
224 | C.Cast (s, t) -> C.Cast (aux s, aux t)
225 | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
226 | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
227 | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
228 | C.Appl l -> C.Appl (List.map aux l)
229 | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
230 | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
231 | C.MutCase (uri, i, s, t, l) ->
232 C.MutCase (uri, i, aux s, aux t, List.map aux l)
235 List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
239 List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
243 List.map (fun (u, t) -> (u, aux t)) ens
249 let restore_metas (* context *) term =
250 let module C = Cic in
251 let rec aux = function
252 | C.Implicit (Some (`MetaInfo (i, c))) ->
254 (* CicMkImplicit.identity_relocation_list_for_metavariable context *)
257 (* let local_context:(C.term option) list = *)
258 (* Marshal.from_string mc 0 *)
260 (* C.Meta (i, local_context) *)
262 | C.Var (u, ens) -> C.Var (u, aux_ens ens)
263 | C.Const (u, ens) -> C.Const (u, aux_ens ens)
264 | C.Cast (s, t) -> C.Cast (aux s, aux t)
265 | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
266 | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
267 | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
268 | C.Appl l -> C.Appl (List.map aux l)
269 | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
270 | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
271 | C.MutCase (uri, i, s, t, l) ->
272 C.MutCase (uri, i, aux s, aux t, List.map aux l)
275 List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
279 List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
283 List.map (fun (u, t) -> (u, aux t)) ens
289 let rec restore_subst (* context *) subst =
291 (fun (i, (c, t, ty)) ->
292 i, (c, restore_metas (* context *) t, ty))
297 let rec check_irl start = function
299 | None::tl -> check_irl (start+1) tl
300 | (Some (Cic.Rel x))::tl ->
301 if x = start then check_irl (start+1) tl else false
305 let rec is_simple_term = function
306 | Cic.Appl ((Cic.Meta _)::_) -> false
307 | Cic.Appl l -> List.for_all is_simple_term l
308 | Cic.Meta (i, l) -> check_irl 1 l
314 let lookup_subst meta subst =
316 | Cic.Meta (i, _) -> (
317 try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
318 with Not_found -> meta
324 let unification_simple metasenv context t1 t2 ugraph =
325 let module C = Cic in
326 let module M = CicMetaSubst in
327 let module U = CicUnification in
328 let lookup = lookup_subst in
329 let rec occurs_check subst what where =
330 (* Printf.printf "occurs_check %s %s" *)
331 (* (CicPp.ppterm what) (CicPp.ppterm where); *)
332 (* print_newline (); *)
334 | t when what = t -> true
335 | C.Appl l -> List.exists (occurs_check subst what) l
337 let t = lookup where subst in
338 if t <> where then occurs_check subst what t else false
341 let rec unif subst menv s t =
342 (* Printf.printf "unif %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
343 (* (print_subst subst); *)
344 (* print_newline (); *)
345 let s = match s with C.Meta _ -> lookup s subst | _ -> s
346 and t = match t with C.Meta _ -> lookup t subst | _ -> t
348 (* Printf.printf "after apply_subst: %s %s\n%s" *)
349 (* (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
350 (* print_newline (); *)
352 | s, t when s = t -> subst, menv
353 | C.Meta (i, _), C.Meta (j, _) when i > j ->
355 | C.Meta _, t when occurs_check subst s t ->
356 raise (U.UnificationFailure "Inference.unification.unif")
357 (* | C.Meta (i, l), C.Meta (j, l') -> *)
358 (* let _, _, ty = CicUtil.lookup_meta i menv in *)
359 (* let _, _, ty' = CicUtil.lookup_meta j menv in *)
360 (* let binding1 = lookup s subst in *)
361 (* let binding2 = lookup t subst in *)
362 (* let subst, menv = *)
363 (* if binding1 != s then *)
364 (* if binding2 != t then *)
365 (* unif subst menv binding1 binding2 *)
367 (* if binding1 = t then *)
370 (* ((j, (context, binding1, ty'))::subst, *)
371 (* List.filter (fun (m, _, _) -> j <> m) menv) *)
373 (* if binding2 != t then *)
374 (* if s = binding2 then *)
377 (* ((i, (context, binding2, ty))::subst, *)
378 (* List.filter (fun (m, _, _) -> i <> m) menv) *)
380 (* ((i, (context, t, ty))::subst, *)
381 (* List.filter (fun (m, _, _) -> i <> m) menv) *)
385 | C.Meta (i, l), t ->
386 let _, _, ty = CicUtil.lookup_meta i menv in
388 if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
391 let menv = List.filter (fun (m, _, _) -> i <> m) menv in
393 | _, C.Meta _ -> unif subst menv t s
394 | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
395 raise (U.UnificationFailure "Inference.unification.unif")
396 | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
399 (fun (subst', menv) s t -> unif subst' menv s t)
400 (subst, menv) tls tlt
402 raise (U.UnificationFailure "Inference.unification.unif")
404 | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
406 let subst, menv = unif [] metasenv t1 t2 in
407 (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
408 (* print_newline (); *)
409 (* let rec fix_term = function *)
410 (* | (C.Meta (i, l) as t) -> *)
412 (* | C.Appl l -> C.Appl (List.map fix_term l) *)
415 (* let rec fix_subst = function *)
417 (* | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl) *)
419 (* List.rev (fix_subst subst), menv, ugraph *)
420 List.rev subst, menv, ugraph
424 let unification metasenv context t1 t2 ugraph =
425 (* Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
426 let subst, menv, ug =
427 if not (is_simple_term t1) || not (is_simple_term t2) then
428 CicUnification.fo_unif metasenv context t1 t2 ugraph
430 unification_simple metasenv context t1 t2 ugraph
432 let rec fix_term = function
433 | (Cic.Meta (i, l) as t) ->
434 let t' = lookup_subst t subst in
435 if t <> t' then fix_term t' else t
436 | Cic.Appl l -> Cic.Appl (List.map fix_term l)
439 let rec fix_subst = function
441 | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
443 (* Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
444 (* print_endline "|"; *)
445 (* fix_subst *) subst, menv, ug
448 (* let unification = CicUnification.fo_unif;; *)
450 exception MatchingFailure;;
453 let matching_simple metasenv context t1 t2 ugraph =
454 let module C = Cic in
455 let module M = CicMetaSubst in
456 let module U = CicUnification in
457 let lookup meta subst =
460 try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
461 with Not_found -> meta
465 let rec do_match subst menv s t =
466 (* Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
467 (* (print_subst subst); *)
468 (* print_newline (); *)
469 (* let s = match s with C.Meta _ -> lookup s subst | _ -> s *)
470 (* let t = match t with C.Meta _ -> lookup t subst | _ -> t in *)
471 (* Printf.printf "after apply_subst: %s %s\n%s" *)
472 (* (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
473 (* print_newline (); *)
475 | s, t when s = t -> subst, menv
476 (* | C.Meta (i, _), C.Meta (j, _) when i > j -> *)
477 (* do_match subst menv t s *)
478 (* | C.Meta _, t when occurs_check subst s t -> *)
479 (* raise MatchingFailure *)
480 (* | s, C.Meta _ when occurs_check subst t s -> *)
481 (* raise MatchingFailure *)
482 | s, C.Meta (i, l) ->
483 let filter_menv i menv =
484 List.filter (fun (m, _, _) -> i <> m) menv
487 let value = lookup t subst in
489 (* | C.Meta (i', l') when Hashtbl.mem table i' -> *)
490 (* (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *)
491 | value when value = t ->
492 let _, _, ty = CicUtil.lookup_meta i menv in
493 (i, (context, s, ty))::subst, filter_menv i menv
494 | value when value <> s ->
495 raise MatchingFailure
496 | value -> do_match subst menv s value
499 (* else if value <> s then *)
500 (* raise MatchingFailure *)
502 (* if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst *)
505 (* let menv = List.filter (fun (m, _, _) -> i <> m) menv in *)
507 (* | _, C.Meta _ -> do_match subst menv t s *)
508 (* | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *)
509 (* raise MatchingFailure *)
510 | C.Appl ls, C.Appl lt -> (
513 (fun (subst, menv) s t -> do_match subst menv s t)
516 (* print_endline (Printexc.to_string e); *)
517 (* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
518 (* print_newline (); *)
519 raise MatchingFailure
522 (* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
523 (* print_newline (); *)
524 raise MatchingFailure
526 let subst, menv = do_match [] metasenv t1 t2 in
527 (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
528 (* print_newline (); *)
533 let matching metasenv context t1 t2 ugraph =
534 (* if (is_simple_term t1) && (is_simple_term t2) then *)
535 (* let subst, menv, ug = *)
536 (* matching_simple metasenv context t1 t2 ugraph in *)
537 (* (\* Printf.printf "matching %s %s:\n%s\n" *\) *)
538 (* (\* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *)
539 (* (\* print_newline (); *\) *)
540 (* subst, menv, ug *)
543 let subst, metasenv, ugraph =
544 (* CicUnification.fo_unif metasenv context t1 t2 ugraph *)
545 unification metasenv context t1 t2 ugraph
547 let t' = CicMetaSubst.apply_subst subst t1 in
548 if not (meta_convertibility t1 t') then
549 raise MatchingFailure
551 let metas = metas_of_term t1 in
552 let fix_subst = function
553 | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
554 (j, (c, Cic.Meta (i, lc), ty))
557 let subst = List.map fix_subst subst in
559 (* Printf.printf "matching %s %s:\n%s\n" *)
560 (* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *)
561 (* print_newline (); *)
563 subst, metasenv, ugraph
565 (* Printf.printf "failed to match %s %s\n" *)
566 (* (CicPp.ppterm t1) (CicPp.ppterm t2); *)
567 raise MatchingFailure
571 (* let profile = CicUtil.profile "Inference.matching" in *)
572 (* (fun metasenv context t1 t2 ugraph -> *)
573 (* profile (matching metasenv context t1 t2) ugraph) *)
577 let beta_expand ?(metas_ok=true) ?(match_only=false)
578 what type_of_what where context metasenv ugraph =
579 let module S = CicSubstitution in
580 let module C = Cic in
582 let print_info = false in
585 (* let names = names_of_context context in *)
586 (* Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
587 (* (CicPp.pp what names) (CicPp.ppterm what) *)
588 (* (CicPp.pp where names) (CicPp.ppterm where); *)
589 (* print_newline (); *)
593 ((list of all possible beta expansions, subst, metasenv, ugraph),
596 let rec aux lift_amount term context metasenv subst ugraph =
597 (* Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
598 let res, lifted_term =
601 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
603 | C.Var (uri, exp_named_subst) ->
604 let ens', lifted_ens =
605 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
609 (fun (e, s, m, ug) ->
610 (C.Var (uri, e), s, m, ug)) ens'
612 expansions, C.Var (uri, lifted_ens)
617 (fun arg (res, lifted_tl) ->
620 let arg_res, lifted_arg =
621 aux lift_amount arg context metasenv subst ugraph in
624 (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
629 (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
631 (Some lifted_arg)::lifted_tl)
634 (fun (r, s, m, ug) -> None::r, s, m, ug)
641 (fun (l, s, m, ug) ->
642 (C.Meta (i, l), s, m, ug)) l'
644 e, C.Meta (i, lifted_l)
647 | C.Implicit _ as t -> [], t
651 aux lift_amount s context metasenv subst ugraph in
653 aux lift_amount t context metasenv subst ugraph
657 (fun (t, s, m, ug) ->
658 C.Cast (t, lifted_t), s, m, ug) l1 in
661 (fun (t, s, m, ug) ->
662 C.Cast (lifted_s, t), s, m, ug) l2 in
663 l1'@l2', C.Cast (lifted_s, lifted_t)
665 | C.Prod (nn, s, t) ->
667 aux lift_amount s context metasenv subst ugraph in
669 aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
670 metasenv subst ugraph
674 (fun (t, s, m, ug) ->
675 C.Prod (nn, t, lifted_t), s, m, ug) l1 in
678 (fun (t, s, m, ug) ->
679 C.Prod (nn, lifted_s, t), s, m, ug) l2 in
680 l1'@l2', C.Prod (nn, lifted_s, lifted_t)
682 | C.Lambda (nn, s, t) ->
684 aux lift_amount s context metasenv subst ugraph in
686 aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
687 metasenv subst ugraph
691 (fun (t, s, m, ug) ->
692 C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
695 (fun (t, s, m, ug) ->
696 C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
697 l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
699 | C.LetIn (nn, s, t) ->
701 aux lift_amount s context metasenv subst ugraph in
703 aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
704 metasenv subst ugraph
708 (fun (t, s, m, ug) ->
709 C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
712 (fun (t, s, m, ug) ->
713 C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
714 l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
718 aux_list lift_amount l context metasenv subst ugraph
720 (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
723 | C.Const (uri, exp_named_subst) ->
724 let ens', lifted_ens =
725 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
729 (fun (e, s, m, ug) ->
730 (C.Const (uri, e), s, m, ug)) ens'
732 (expansions, C.Const (uri, lifted_ens))
734 | C.MutInd (uri, i ,exp_named_subst) ->
735 let ens', lifted_ens =
736 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
740 (fun (e, s, m, ug) ->
741 (C.MutInd (uri, i, e), s, m, ug)) ens'
743 (expansions, C.MutInd (uri, i, lifted_ens))
745 | C.MutConstruct (uri, i, j, exp_named_subst) ->
746 let ens', lifted_ens =
747 aux_ens lift_amount exp_named_subst context metasenv subst ugraph
751 (fun (e, s, m, ug) ->
752 (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
754 (expansions, C.MutConstruct (uri, i, j, lifted_ens))
756 | C.MutCase (sp, i, outt, t, pl) ->
757 let pl_res, lifted_pl =
758 aux_list lift_amount pl context metasenv subst ugraph
760 let l1, lifted_outt =
761 aux lift_amount outt context metasenv subst ugraph in
763 aux lift_amount t context metasenv subst ugraph in
767 (fun (outt, s, m, ug) ->
768 C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
771 (fun (t, s, m, ug) ->
772 C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
775 (fun (pl, s, m, ug) ->
776 C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
778 (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
781 let len = List.length fl in
784 (fun (nm, idx, ty, bo) (res, lifted_tl) ->
785 let lifted_ty = S.lift lift_amount ty in
786 let bo_res, lifted_bo =
787 aux (lift_amount+len) bo context metasenv subst ugraph in
790 (fun (a, s, m, ug) ->
791 (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
796 (fun (r, s, m, ug) ->
797 (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
798 (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
802 (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
803 C.Fix (i, lifted_fl))
806 let len = List.length fl in
809 (fun (nm, ty, bo) (res, lifted_tl) ->
810 let lifted_ty = S.lift lift_amount ty in
811 let bo_res, lifted_bo =
812 aux (lift_amount+len) bo context metasenv subst ugraph in
815 (fun (a, s, m, ug) ->
816 (nm, lifted_ty, a)::lifted_tl, s, m, ug)
821 (fun (r, s, m, ug) ->
822 (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
823 (nm, lifted_ty, lifted_bo)::lifted_tl)
827 (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
828 C.CoFix (i, lifted_fl))
832 | C.Meta _ when (not metas_ok) ->
836 (* if match_only then replace_metas context term *)
840 let subst', metasenv', ugraph' =
841 (* Printf.printf "provo a unificare %s e %s\n" *)
842 (* (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
844 matching metasenv context term (S.lift lift_amount what) ugraph
846 CicUnification.fo_unif metasenv context
847 (S.lift lift_amount what) term ugraph
849 (* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
850 (* (CicPp.ppterm (S.lift lift_amount what)); *)
851 (* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
852 (* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
853 (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
854 (* if match_only then *)
855 (* let t' = CicMetaSubst.apply_subst subst' term in *)
856 (* if not (meta_convertibility term t') then ( *)
857 (* res, lifted_term *)
859 (* let metas = metas_of_term term in *)
860 (* let fix_subst = function *)
861 (* | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
862 (* (j, (c, C.Meta (i, lc), ty)) *)
865 (* let subst' = List.map fix_subst subst' in *)
866 (* ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
870 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
874 print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e));
878 (* Printf.printf "exit aux\n"; *)
881 and aux_list lift_amount l context metasenv subst ugraph =
883 (fun arg (res, lifted_tl) ->
884 let arg_res, lifted_arg =
885 aux lift_amount arg context metasenv subst ugraph in
887 (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
890 (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
891 lifted_arg::lifted_tl)
894 and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
896 (fun (u, arg) (res, lifted_tl) ->
897 let arg_res, lifted_arg =
898 aux lift_amount arg context metasenv subst ugraph in
901 (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
903 (l1 @ (List.map (fun (r, s, m, ug) ->
904 (u, lifted_arg)::r, s, m, ug) res),
905 (u, lifted_arg)::lifted_tl)
906 ) exp_named_subst ([], [])
911 (* if match_only then replace_metas (\* context *\) where *)
915 Printf.printf "searching %s inside %s\n"
916 (CicPp.ppterm what) (CicPp.ppterm where);
918 aux 0 where context metasenv [] ugraph
921 (* if match_only then *)
922 (* (fun (term, subst, metasenv, ugraph) -> *)
924 (* C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
925 (* and subst = restore_subst subst in *)
926 (* (term', subst, metasenv, ugraph)) *)
928 (fun (term, subst, metasenv, ugraph) ->
929 let term' = C.Lambda (C.Anonymous, type_of_what, term) in
930 (term', subst, metasenv, ugraph))
932 List.map mapfun expansions
937 Cic.term * (* proof *)
938 (Cic.term * (* type *)
939 Cic.term * (* left side *)
940 Cic.term * (* right side *)
941 Utils.comparison) * (* ordering *)
942 Cic.metasenv * (* environment for metas *)
943 Cic.term list (* arguments *)
947 let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
948 let module C = Cic in
949 let module S = CicSubstitution in
950 let module T = CicTypeChecker in
951 let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
952 let rec aux index newmeta = function
954 | (Some (_, C.Decl (term)))::tl ->
955 let do_find context term =
957 | C.Prod (name, s, t) ->
958 (* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
959 let (head, newmetas, args, _) =
960 PrimitiveTactics.new_metasenv_for_apply newmeta proof
961 context (S.lift index term)
967 | C.Meta (i, _) -> (max maxm i)
972 if List.length args = 0 then
975 C.Appl ((C.Rel index)::args)
978 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
979 Printf.printf "OK: %s\n" (CicPp.ppterm term);
980 let o = !Utils.compare_terms t1 t2 in
981 Some (p, (ty, t1, t2, o), newmetas, args), (newmeta+1)
984 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
985 let t1 = S.lift index t1
986 and t2 = S.lift index t2 in
987 let o = !Utils.compare_terms t1 t2 in
988 Some (C.Rel index, (ty, t1, t2, o), [], []), (newmeta+1)
991 match do_find context term with
993 let tl, newmeta' = (aux (index+1) newmeta tl) in
994 p::tl, max newmeta newmeta'
996 aux (index+1) newmeta tl
999 aux (index+1) newmeta tl
1001 aux 1 newmeta context
1005 let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) =
1006 let table = Hashtbl.create (List.length args) in
1009 (fun t (newargs, index) ->
1011 | Cic.Meta (i, l) ->
1012 Hashtbl.add table i index;
1013 ((Cic.Meta (index, l))::newargs, index+1)
1014 | _ -> assert false)
1018 ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
1023 (fun (i, context, term) menv ->
1025 let index = Hashtbl.find table i in
1026 (index, context, term)::menv
1028 (i, context, term)::menv)
1032 and left = repl left
1033 and right = repl right in
1034 let metas = (metas_of_term left) @ (metas_of_term right) in
1035 let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv'
1038 (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
1040 (newmeta + (List.length newargs) + 1,
1041 (repl proof, (ty, left, right, o), menv', newargs))
1045 exception TermIsNotAnEquality;;
1047 let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
1048 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
1049 let o = !Utils.compare_terms t1 t2 in
1050 (proof, (ty, t1, t2, o), [], [])
1052 raise TermIsNotAnEquality
1056 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
1059 let superposition_left (metasenv, context, ugraph) target source =
1060 let module C = Cic in
1061 let module S = CicSubstitution in
1062 let module M = CicMetaSubst in
1063 let module HL = HelmLibraryObjects in
1064 let module CR = CicReduction in
1065 (* we assume that target is ground (does not contain metavariables): this
1066 * should always be the case (I hope, at least) *)
1067 let proof, (eq_ty, left, right, t_order), _, _ = target in
1068 let eqproof, (ty, t1, t2, s_order), newmetas, args = source in
1070 let compare_terms = !Utils.compare_terms in
1075 let where, is_left =
1076 match t_order (* compare_terms left right *) with
1077 | Lt -> right, false
1080 Printf.printf "????????? %s = %s" (CicPp.ppterm left)
1081 (CicPp.ppterm right);
1083 assert false (* again, for ground terms this shouldn't happen... *)
1086 let metasenv' = newmetas @ metasenv in
1087 let result = s_order (* compare_terms t1 t2 *) in
1090 | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
1091 | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
1095 (fun (t, s, m, ug) ->
1096 compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
1097 (beta_expand t1 ty where context metasenv' ugraph)
1100 (fun (t, s, m, ug) ->
1101 compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
1102 (beta_expand t2 ty where context metasenv' ugraph)
1106 (* let what, other = *)
1107 (* if is_left then left, right *)
1108 (* else right, left *)
1110 let build_new what other eq_URI (t, s, m, ug) =
1111 let newgoal, newgoalproof =
1113 | C.Lambda (nn, ty, bo) ->
1114 let bo' = S.subst (M.apply_subst s other) bo in
1117 [C.MutInd (HL.Logic.eq_URI, 0, []);
1119 if is_left then [bo'; S.lift 1 right]
1120 else [S.lift 1 left; bo'])
1122 let t' = C.Lambda (nn, ty, bo'') in
1123 S.subst (M.apply_subst s other) bo,
1125 (C.Appl [C.Const (eq_URI, []); ty; what; t';
1126 proof; other; eqproof])
1130 if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
1131 else (eq_ty, left, newgoal, compare_terms left newgoal)
1133 (newgoalproof (* eqproof *), equation, [], [])
1135 let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
1136 and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
1141 let superposition_right newmeta (metasenv, context, ugraph) target source =
1142 let module C = Cic in
1143 let module S = CicSubstitution in
1144 let module M = CicMetaSubst in
1145 let module HL = HelmLibraryObjects in
1146 let module CR = CicReduction in
1147 let eqproof, (eq_ty, left, right, t_order), newmetas, args = target in
1148 let eqp', (ty', t1, t2, s_order), newm', args' = source in
1149 let maxmeta = ref newmeta in
1151 let compare_terms = !Utils.compare_terms in
1153 if eq_ty <> ty' then
1156 (* let ok term subst other other_eq_side ugraph = *)
1157 (* match term with *)
1158 (* | C.Lambda (nn, ty, bo) -> *)
1159 (* let bo' = S.subst (M.apply_subst subst other) bo in *)
1160 (* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
1162 (* | _ -> assert false *)
1164 let condition left right what other (t, s, m, ug) =
1165 let subst = M.apply_subst s in
1166 let cmp1 = compare_terms (subst what) (subst other) in
1167 let cmp2 = compare_terms (subst left) (subst right) in
1168 (* cmp1 = Gt && cmp2 = Gt *)
1169 cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
1170 (* && (ok t s other right ug) *)
1172 let metasenv' = metasenv @ newmetas @ newm' in
1173 let beta_expand = beta_expand ~metas_ok:false in
1174 let cmp1 = t_order (* compare_terms left right *)
1175 and cmp2 = s_order (* compare_terms t1 t2 *) in
1176 let res1, res2, res3, res4 =
1180 (beta_expand s eq_ty l context metasenv' ugraph)
1182 match cmp1, cmp2 with
1184 (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
1186 [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
1188 [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
1190 [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
1192 let res1 = res left right t1 t2
1193 and res2 = res left right t2 t1 in
1196 let res3 = res right left t1 t2
1197 and res4 = res right left t2 t1 in
1200 let res1 = res left right t1 t2
1201 and res3 = res right left t1 t2 in
1204 let res2 = res left right t2 t1
1205 and res4 = res right left t2 t1 in
1208 let res1 = res left right t1 t2
1209 and res2 = res left right t2 t1
1210 and res3 = res right left t1 t2
1211 and res4 = res right left t2 t1 in
1212 res1, res2, res3, res4
1214 let newmetas = newmetas @ newm' in
1215 let newargs = args @ args' in
1216 let build_new what other is_left eq_URI (t, s, m, ug) =
1217 (* let what, other = *)
1218 (* if is_left then left, right *)
1219 (* else right, left *)
1221 let newterm, neweqproof =
1223 | C.Lambda (nn, ty, bo) ->
1224 let bo' = M.apply_subst s (S.subst other bo) in
1227 [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
1228 if is_left then [bo'; S.lift 1 right]
1229 else [S.lift 1 left; bo'])
1231 let t' = C.Lambda (nn, ty, bo'') in
1234 (C.Appl [C.Const (eq_URI, []); ty; what; t';
1235 eqproof; other; eqp'])
1238 let newmeta, newequality =
1240 if is_left then (newterm, M.apply_subst s right)
1241 else (M.apply_subst s left, newterm) in
1242 let neworder = compare_terms left right in
1244 (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
1249 let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
1250 and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
1251 and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
1252 and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
1254 | _, (_, left, right, _), _, _ ->
1255 not (fst (CR.are_convertible context left right ugraph))
1258 (List.filter ok (new1 @ new2 @ new3 @ new4)))
1262 let is_identity ((_, context, ugraph) as env) = function
1263 | ((_, (ty, left, right, _), _, _) as equality) ->
1266 (fst (CicReduction.are_convertible context left right ugraph)))
1269 (* Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
1270 (* print_newline (); *)
1276 let demodulation newmeta (metasenv, context, ugraph) target source =
1277 let module C = Cic in
1278 let module S = CicSubstitution in
1279 let module M = CicMetaSubst in
1280 let module HL = HelmLibraryObjects in
1281 let module CR = CicReduction in
1283 let proof, (eq_ty, left, right, t_order), metas, args = target
1284 and proof', (ty, t1, t2, s_order), metas', args' = source in
1286 let compare_terms = !Utils.compare_terms in
1291 let first_step, get_params =
1292 match s_order (* compare_terms t1 t2 *) with
1293 | Gt -> 1, (function
1294 | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
1295 | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
1296 | _ -> assert false)
1297 | Lt -> 1, (function
1298 | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1299 | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1300 | _ -> assert false)
1302 let first_step = 3 in
1303 let get_params step =
1305 | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
1306 | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
1307 | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1308 | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1311 first_step, get_params
1313 let rec demodulate newmeta step metasenv target =
1314 let proof, (eq_ty, left, right, t_order), metas, args = target in
1315 let is_left, what, other, eq_URI = get_params step in
1317 let env = metasenv, context, ugraph in
1318 let names = names_of_context context in
1320 (* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1321 (* (string_of_equality ~env target) (CicPp.pp what names) *)
1322 (* (CicPp.pp other names) (string_of_bool is_left); *)
1323 (* Printf.printf "step: %d" step; *)
1324 (* print_newline (); *)
1326 let ok (t, s, m, ug) =
1327 compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
1330 let r = (beta_expand ~metas_ok:false ~match_only:true
1331 what ty (if is_left then left else right)
1332 context (metasenv @ metas) ugraph)
1334 (* let m' = metas_of_term what *)
1335 (* and m'' = metas_of_term (if is_left then left else right) in *)
1336 (* if (List.mem 527 m'') && (List.mem 6 m') then ( *)
1338 (* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1339 (* (string_of_equality ~env target) (CicPp.pp what names) *)
1340 (* (CicPp.pp other names) (string_of_bool is_left); *)
1341 (* Printf.printf "step: %d" step; *)
1342 (* print_newline (); *)
1343 (* print_endline "res:"; *)
1344 (* List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
1345 (* print_newline (); *)
1346 (* Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
1347 (* print_newline (); *)
1353 if step = 0 then newmeta, target
1354 else demodulate newmeta (step-1) metasenv target
1355 | (t, s, m, ug)::_ ->
1356 let newterm, newproof =
1358 | C.Lambda (nn, ty, bo) ->
1359 (* let bo' = M.apply_subst s (S.subst other bo) in *)
1360 let bo' = S.subst (M.apply_subst s other) bo in
1363 [C.MutInd (HL.Logic.eq_URI, 0, []);
1365 if is_left then [bo'; S.lift 1 right]
1366 else [S.lift 1 left; bo'])
1368 let t' = C.Lambda (nn, ty, bo'') in
1369 (* M.apply_subst s (S.subst other bo), *)
1372 (C.Appl [C.Const (eq_URI, []); ty; what; t';
1373 proof; other; proof'])
1376 let newmeta, newtarget =
1378 (* if is_left then (newterm, M.apply_subst s right) *)
1379 (* else (M.apply_subst s left, newterm) in *)
1380 if is_left then newterm, right
1383 let neworder = compare_terms left right in
1384 (* let newmetasenv = metasenv @ metas in *)
1385 (* let newargs = args @ args' in *)
1386 (* fix_metas newmeta *)
1387 (* (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
1388 let m = (metas_of_term left) @ (metas_of_term right) in
1389 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
1392 (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
1396 (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs)
1399 (* "demodulate, newtarget: %s\ntarget was: %s\n" *)
1400 (* (string_of_equality ~env newtarget) *)
1401 (* (string_of_equality ~env target); *)
1402 (* (\* let _, _, newm, newa = newtarget in *\) *)
1403 (* (\* Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
1404 (* (\* (print_metasenv newm) *\) *)
1405 (* (\* (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
1406 (* print_newline (); *)
1407 if is_identity env newtarget then
1410 demodulate newmeta first_step metasenv newtarget
1412 demodulate newmeta first_step (metasenv @ metas') target
1417 let demodulation newmeta env target source =
1423 let subsumption env target source =
1424 let _, (ty, tl, tr, _), tmetas, _ = target
1425 and _, (ty', sl, sr, _), smetas, _ = source in
1429 let metasenv, context, ugraph = env in
1430 let metasenv = metasenv @ tmetas @ smetas in
1431 let names = names_of_context context in
1432 let samesubst subst subst' =
1433 (* Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
1434 (* (print_subst subst) (print_subst subst'); *)
1435 (* print_newline (); *)
1436 let tbl = Hashtbl.create (List.length subst) in
1437 List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
1439 (fun (m, (c, t1, t2)) ->
1441 let c', t1', t2' = Hashtbl.find tbl m in
1442 if (c = c') && (t1 = t1') && (t2 = t2') then true
1448 let subsaux left right left' right' =
1450 let subst, menv, ug = matching metasenv context left left' ugraph
1451 and subst', menv', ug' = matching metasenv context right right' ugraph
1453 (* Printf.printf "left = right: %s = %s\n" *)
1454 (* (CicPp.pp left names) (CicPp.pp right names); *)
1455 (* Printf.printf "left' = right': %s = %s\n" *)
1456 (* (CicPp.pp left' names) (CicPp.pp right' names); *)
1457 samesubst subst subst'
1459 (* print_endline (Printexc.to_string e); *)
1463 if subsaux tl tr sl sr then true
1464 else subsaux tl tr sr sl
1467 Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
1468 (string_of_equality ~env target) (string_of_equality ~env source);
1475 let extract_differing_subterms t1 t2 =
1476 let module C = Cic in
1479 | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
1481 | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
1482 let res = List.concat (List.map2 aux tl1 tl2) in
1484 if res = [] then [(h1, h2)] else [(t1, t2)]
1486 if List.length res > 1 then [(t1, t2)] else res
1488 if t1 <> t2 then [(t1, t2)] else []
1490 let res = aux t1 t2 in