1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
30 exception UnificationFailure of string Lazy.t;;
31 exception Uncertain of string Lazy.t;;
32 exception AssertFailure of string Lazy.t;;
35 let debug_print = fun _ -> ()
37 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
38 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
39 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
40 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
42 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
44 let type_of_aux' metasenv subst context term ugraph =
47 profile.HExtlib.profile
48 (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
50 CicTypeChecker.TypeCheckerFailure msg ->
54 "Kernel Type checking error:
55 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
56 (CicMetaSubst.ppterm ~metasenv subst term)
57 (CicMetaSubst.ppterm ~metasenv [] term)
58 (CicMetaSubst.ppcontext ~metasenv subst context)
59 (CicMetaSubst.ppmetasenv subst metasenv)
60 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
61 raise (AssertFailure msg)
62 | CicTypeChecker.AssertFailure msg ->
65 "Kernel Type checking assertion failure:
66 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
67 (CicMetaSubst.ppterm ~metasenv subst term)
68 (CicMetaSubst.ppterm ~metasenv [] term)
69 (CicMetaSubst.ppcontext ~metasenv subst context)
70 (CicMetaSubst.ppmetasenv subst metasenv)
71 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
72 raise (AssertFailure msg)
73 in profiler_toa.HExtlib.profile foo ()
80 | Cic.Appl (Cic.Meta _::_) -> true
83 let rec deref subst t =
84 let snd (_,a,_) = a in
89 (CicSubstitution.subst_meta
90 l (snd (CicUtil.lookup_subst n subst)))
92 CicUtil.Subst_not_found _ -> t)
93 | Cic.Appl(Cic.Meta(n,l)::args) ->
94 (match deref subst (Cic.Meta(n,l)) with
95 | Cic.Lambda _ as t ->
96 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
97 | r -> Cic.Appl(r::args))
98 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
99 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
104 let foo () = deref subst t
105 in profiler_deref.HExtlib.profile foo ()
107 exception WrongShape;;
108 let eta_reduce after_beta_expansion after_beta_expansion_body
109 before_beta_expansion
112 match before_beta_expansion,after_beta_expansion_body with
113 Cic.Appl l, Cic.Appl l' ->
114 let rec all_but_last check_last =
118 | [_] -> if check_last then raise WrongShape else []
119 | he::tl -> he::(all_but_last check_last tl)
121 let all_but_last check_last l =
122 match all_but_last check_last l with
127 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
128 let all_but_last = all_but_last false l in
129 (* here we should test alpha-equivalence; however we know by
130 construction that here alpha_equivalence is equivalent to = *)
131 if t = all_but_last then
135 | _,_ -> after_beta_expansion
137 WrongShape -> after_beta_expansion
139 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
140 let module S = CicSubstitution in
141 let module C = Cic in
143 let rec aux metasenv subst n context t' ugraph =
146 let subst,metasenv,ugraph1 =
147 fo_unif_subst test_equality_only subst context metasenv
148 (CicSubstitution.lift n arg) t' ugraph
151 subst,metasenv,C.Rel (1 + n),ugraph1
154 | UnificationFailure _ ->
156 | C.Rel m -> subst,metasenv,
157 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
158 | C.Var (uri,exp_named_subst) ->
159 let subst,metasenv,exp_named_subst',ugraph1 =
160 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
162 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
164 (* andrea: in general, beta_expand can create badly typed
165 terms. This happens quite seldom in practice, UNLESS we
166 iterate on the local context. For this reason, we renounce
167 to iterate and just lift *)
171 Some t -> Some (CicSubstitution.lift 1 t)
173 subst, metasenv, C.Meta (i,l), ugraph
175 | C.Implicit _ as t -> subst,metasenv,t,ugraph
177 let subst,metasenv,te',ugraph1 =
178 aux metasenv subst n context te ugraph in
179 let subst,metasenv,ty',ugraph2 =
180 aux metasenv subst n context ty ugraph1 in
181 (* TASSI: sure this is in serial? *)
182 subst,metasenv,(C.Cast (te', ty')),ugraph2
184 let subst,metasenv,s',ugraph1 =
185 aux metasenv subst n context s ugraph in
186 let subst,metasenv,t',ugraph2 =
187 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
190 (* TASSI: sure this is in serial? *)
191 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
192 | C.Lambda (nn,s,t) ->
193 let subst,metasenv,s',ugraph1 =
194 aux metasenv subst n context s ugraph in
195 let subst,metasenv,t',ugraph2 =
196 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
198 (* TASSI: sure this is in serial? *)
199 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
200 | C.LetIn (nn,s,ty,t) ->
201 let subst,metasenv,s',ugraph1 =
202 aux metasenv subst n context s ugraph in
203 let subst,metasenv,ty',ugraph1 =
204 aux metasenv subst n context ty ugraph in
205 let subst,metasenv,t',ugraph2 =
206 aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
209 (* TASSI: sure this is in serial? *)
210 subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
212 let subst,metasenv,revl',ugraph1 =
214 (fun (subst,metasenv,appl,ugraph) t ->
215 let subst,metasenv,t',ugraph1 =
216 aux metasenv subst n context t ugraph in
217 subst,metasenv,(t'::appl),ugraph1
218 ) (subst,metasenv,[],ugraph) l
220 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
221 | C.Const (uri,exp_named_subst) ->
222 let subst,metasenv,exp_named_subst',ugraph1 =
223 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
225 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
226 | C.MutInd (uri,i,exp_named_subst) ->
227 let subst,metasenv,exp_named_subst',ugraph1 =
228 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
230 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
231 | C.MutConstruct (uri,i,j,exp_named_subst) ->
232 let subst,metasenv,exp_named_subst',ugraph1 =
233 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
235 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
236 | C.MutCase (sp,i,outt,t,pl) ->
237 let subst,metasenv,outt',ugraph1 =
238 aux metasenv subst n context outt ugraph in
239 let subst,metasenv,t',ugraph2 =
240 aux metasenv subst n context t ugraph1 in
241 let subst,metasenv,revpl',ugraph3 =
243 (fun (subst,metasenv,pl,ugraph) t ->
244 let subst,metasenv,t',ugraph1 =
245 aux metasenv subst n context t ugraph in
246 subst,metasenv,(t'::pl),ugraph1
247 ) (subst,metasenv,[],ugraph2) pl
249 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
250 (* TASSI: not sure this is serial *)
252 (*CSC: not implemented
253 let tylen = List.length fl in
256 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
259 C.Fix (i, substitutedfl)
261 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
263 (*CSC: not implemented
264 let tylen = List.length fl in
267 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
270 C.CoFix (i, substitutedfl)
273 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
275 and aux_exp_named_subst metasenv subst n context ens ugraph =
277 (fun (uri,t) (subst,metasenv,l,ugraph) ->
278 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
279 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
281 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
283 FreshNamesGenerator.mk_fresh_name ~subst
284 metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
286 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
287 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
288 subst, metasenv, t'', ugraph2
289 in profiler_beta_expand.HExtlib.profile foo ()
292 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
293 let _,subst,metasenv,hd,ugraph =
295 (fun arg (num,subst,metasenv,t,ugraph) ->
296 let subst,metasenv,t,ugraph1 =
297 beta_expand num test_equality_only
298 metasenv subst context t arg ugraph
300 num+1,subst,metasenv,t,ugraph1
301 ) args (1,subst,metasenv,t,ugraph)
303 subst,metasenv,hd,ugraph
305 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
308 | (m2,_,c2,c2')::_ ->
309 let m1,c1,c1' = carr,to1,to2 in
311 function Some (_,t) -> CicPp.ppterm t
315 ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
316 CoercDb.string_of_carr car2^": " ^
317 CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
318 unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
319 unopt c2^" + "^unopt c2')
321 (* NUOVA UNIFICAZIONE *)
322 (* A substitution is a (int * Cic.term) list that associates a
323 metavariable i with its body.
324 A metaenv is a (int * Cic.term) list that associate a metavariable
326 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
327 a new substitution which is _NOT_ unwinded. It must be unwinded before
330 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
331 let module C = Cic in
332 let module R = CicReduction in
333 let module S = CicSubstitution in
334 let t1 = deref subst t1 in
335 let t2 = deref subst t2 in
336 let (&&&) a b = (a && b) || ((not a) && (not b)) in
337 (* let bef = Sys.time () in *)
339 if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
343 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
344 in profiler_are_convertible.HExtlib.profile foo ()
346 (* let aft = Sys.time () in
347 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
348 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
349 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
351 subst, metasenv, ugraph
354 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
355 let _,subst,metasenv,ugraph1 =
358 (fun (j,subst,metasenv,ugraph) t1 t2 ->
361 | _,None -> j+1,subst,metasenv,ugraph
362 | Some t1', Some t2' ->
363 (* First possibility: restriction *)
364 (* Second possibility: unification *)
365 (* Third possibility: convertibility *)
368 ~subst ~metasenv context t1' t2' ugraph
371 j+1,subst,metasenv, ugraph1
374 let subst,metasenv,ugraph2 =
377 subst context metasenv t1' t2' ugraph
379 j+1,subst,metasenv,ugraph2
382 | UnificationFailure _ ->
383 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
384 let metasenv, subst =
385 CicMetaSubst.restrict
386 subst [(n,j)] metasenv in
387 j+1,subst,metasenv,ugraph1)
388 ) (1,subst,metasenv,ugraph) ln lm
392 (UnificationFailure (lazy "1"))
395 "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
396 (CicMetaSubst.ppterm ~metasenv subst t1)
397 (CicMetaSubst.ppterm ~metasenv subst t2))) *)
398 | Invalid_argument _ ->
400 (UnificationFailure (lazy "2")))
403 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
404 (CicMetaSubst.ppterm ~metasenv subst t1)
405 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
406 in subst,metasenv,ugraph1
407 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
408 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
410 | (t, C.Meta (n,l)) ->
413 C.Meta (n,_), C.Meta (m,_) when n < m -> false
414 | _, C.Meta _ -> false
417 let lower = fun x y -> if swap then y else x in
418 let upper = fun x y -> if swap then x else y in
419 let fo_unif_subst_ordered
420 test_equality_only subst context metasenv m1 m2 ugraph =
421 fo_unif_subst test_equality_only subst context metasenv
422 (lower m1 m2) (upper m1 m2) ugraph
425 let subst,metasenv,ugraph1 =
426 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
429 type_of_aux' metasenv subst context t ugraph
433 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
435 UnificationFailure _ as e -> raise e
436 | Uncertain msg -> raise (UnificationFailure msg)
438 debug_print (lazy "siamo allo huge hack");
439 (* TODO huge hack!!!!
440 * we keep on unifying/refining in the hope that
441 * the problem will be eventually solved.
442 * In the meantime we're breaking a big invariant:
443 * the terms that we are unifying are no longer well
444 * typed in the current context (in the worst case
445 * we could even diverge) *)
446 (subst, metasenv,ugraph)) in
447 let t',metasenv,subst =
449 CicMetaSubst.delift n subst context metasenv l t
451 (CicMetaSubst.MetaSubstFailure msg)->
452 raise (UnificationFailure msg)
453 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
457 C.Sort (C.Type u) when not test_equality_only ->
458 let u' = CicUniv.fresh () in
459 let s = C.Sort (C.Type u') in
462 CicUniv.add_ge (upper u u') (lower u u') ugraph1
466 CicUniv.UniverseInconsistency msg ->
467 raise (UnificationFailure msg))
470 (* Unifying the types may have already instantiated n. Let's check *)
472 let (_, oldt,_) = CicUtil.lookup_subst n subst in
473 let lifted_oldt = S.subst_meta l oldt in
474 fo_unif_subst_ordered
475 test_equality_only subst context metasenv t lifted_oldt ugraph2
477 CicUtil.Subst_not_found _ ->
478 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
479 let subst = (n, (context, t'',ty)) :: subst in
481 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
482 subst, metasenv, ugraph2
484 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
485 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
486 if UriManager.eq uri1 uri2 then
487 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
488 exp_named_subst1 exp_named_subst2 ugraph
490 raise (UnificationFailure (lazy
492 "Can't unify %s with %s due to different constants"
493 (CicMetaSubst.ppterm ~metasenv subst t1)
494 (CicMetaSubst.ppterm ~metasenv subst t2))))
495 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
496 if UriManager.eq uri1 uri2 && i1 = i2 then
497 fo_unif_subst_exp_named_subst
499 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
501 raise (UnificationFailure
504 "Can't unify %s with %s due to different inductive principles"
505 (CicMetaSubst.ppterm ~metasenv subst t1)
506 (CicMetaSubst.ppterm ~metasenv subst t2))))
507 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
508 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
509 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
510 fo_unif_subst_exp_named_subst
512 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
514 raise (UnificationFailure
517 "Can't unify %s with %s due to different inductive constructors"
518 (CicMetaSubst.ppterm ~metasenv subst t1)
519 (CicMetaSubst.ppterm ~metasenv subst t2))))
520 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
521 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
522 subst context metasenv te t2 ugraph
523 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
524 subst context metasenv t1 te ugraph
525 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
526 let subst',metasenv',ugraph1 =
527 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
529 fo_unif_subst test_equality_only
530 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
531 | (C.LetIn (_,s1,ty1,t1), t2)
532 | (t2, C.LetIn (_,s1,ty1,t1)) ->
534 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
535 | (C.Appl l1, C.Appl l2) ->
536 (* andrea: this case should be probably rewritten in the
539 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
542 (fun (subst,metasenv,ugraph) t1 t2 ->
544 test_equality_only subst context metasenv t1 t2 ugraph)
545 (subst,metasenv,ugraph) l1 l2
546 with (Invalid_argument msg) ->
547 raise (UnificationFailure (lazy msg)))
548 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
549 (* we verify that none of the args is a Meta,
550 since beta expanding with respoect to a metavariable
554 let (_,t,_) = CicUtil.lookup_subst i subst in
555 let lifted = S.subst_meta l t in
556 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
559 subst context metasenv reduced t2 ugraph
560 with CicUtil.Subst_not_found _ -> *)
561 let subst,metasenv,beta_expanded,ugraph1 =
563 test_equality_only metasenv subst context t2 args ugraph
565 fo_unif_subst test_equality_only subst context metasenv
566 (C.Meta (i,l)) beta_expanded ugraph1
567 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
569 let (_,t,_) = CicUtil.lookup_subst i subst in
570 let lifted = S.subst_meta l t in
571 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
574 subst context metasenv t1 reduced ugraph
575 with CicUtil.Subst_not_found _ -> *)
576 let subst,metasenv,beta_expanded,ugraph1 =
579 metasenv subst context t1 args ugraph
581 fo_unif_subst test_equality_only subst context metasenv
582 (C.Meta (i,l)) beta_expanded ugraph1
584 let lr1 = List.rev l1 in
585 let lr2 = List.rev l2 in
587 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
590 | _,[] -> assert false
593 test_equality_only subst context metasenv h1 h2 ugraph
596 fo_unif_subst test_equality_only subst context metasenv
597 h (C.Appl (List.rev l)) ugraph
598 | ((h1::l1),(h2::l2)) ->
599 let subst', metasenv',ugraph1 =
602 subst context metasenv h1 h2 ugraph
605 test_equality_only subst' metasenv' (l1,l2) ugraph1
609 test_equality_only subst metasenv (lr1, lr2) ugraph
611 | UnificationFailure s
612 | Uncertain s as exn ->
615 | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
616 (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
617 CoercDb.is_a_coercion cc1 <> None &&
618 CoercDb.is_a_coercion cc2 <> None &&
619 not (UriManager.eq uri1 uri2) ->
621 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
623 let inner_coerced t =
624 let t = CicMetaSubst.apply_subst subst t in
628 (match CoercGraph.coerced_arg l with
630 | Some (t,_) -> aux (List.hd l) t t)
633 aux (Cic.Implicit None) (Cic.Implicit None) t
635 let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
636 let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
639 CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
641 | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
644 let head1_c, head2_c =
646 CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
648 | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
651 let unfold uri ens args =
653 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
657 | Cic.Constant (_,Some bo,_,_,_) ->
658 CicReduction.head_beta_reduce ~delta:false
659 (Cic.Appl (bo::args))
662 let conclude subst metasenv ugraph last_tl1' last_tl2' =
663 let subst',metasenv,ugraph =
666 ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
667 " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
669 fo_unif_subst test_equality_only subst context
670 metasenv last_tl1' last_tl2' ugraph
672 if subst = subst' then raise exn
675 let subst,metasenv,ugrph as res =
677 fo_unif_subst test_equality_only subst' context
678 metasenv (C.Appl l1) (C.Appl l2) ugraph
682 (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
683 " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
687 if CoercDb.eq_carr car1 car2 then
688 match last_tl1,last_tl2 with
689 | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
692 let subst,metasenv,ugraph =
693 fo_unif_subst test_equality_only subst context
694 metasenv last_tl1 last_tl2 ugraph
696 fo_unif_subst test_equality_only subst context
697 metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
698 | _ when CoercDb.eq_carr head1_c head2_c ->
699 (* composite VS composition + metas avoiding
700 * coercions not only in coerced position *)
701 if c1 <> cc1 && c2 <> cc2 then
702 conclude subst metasenv ugraph
707 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
709 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
711 fo_unif_subst test_equality_only subst context
712 metasenv l1 l2 ugraph
716 match last_tl1 with Cic.Meta _ -> true | _ -> false in
718 match last_tl2 with Cic.Meta _ -> true | _ -> false in
719 if not (grow1 || grow2) then
720 (* no flexible terminals -> no pullback, but
721 * we still unify them, in some cases it helps *)
722 conclude subst metasenv ugraph last_tl1 last_tl2
726 metasenv subst context (grow1,car1) (grow2,car2)
730 | (carr,metasenv,to1,to2)::xxx ->
731 warn_if_not_unique xxx to1 to2 carr car1 car2;
732 let last_tl1',(subst,metasenv,ugraph) =
734 | true,Some (last,coerced) ->
736 fo_unif_subst test_equality_only subst context
737 metasenv coerced last_tl1 ugraph
738 | _ -> last_tl1,(subst,metasenv,ugraph)
740 let last_tl2',(subst,metasenv,ugraph) =
742 | true,Some (last,coerced) ->
744 fo_unif_subst test_equality_only subst context
745 metasenv coerced last_tl2 ugraph
746 | _ -> last_tl2,(subst,metasenv,ugraph)
748 conclude subst metasenv ugraph last_tl1' last_tl2')
750 (* {{{ CSC: This is necessary because of the "elim H" tactic
751 where the type of H is only reducible to an
752 inductive type. This could be extended from inductive
753 types to any rigid term. However, the code is
754 duplicated in two places: inside applications and
755 outside them. Probably it would be better to
756 work with lambda-bar terms instead. *)
757 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
758 | (_, Cic.MutInd _::_) ->
759 let t1' = R.whd ~subst context t1 in
761 C.Appl (C.MutInd _::_) ->
762 fo_unif_subst test_equality_only
763 subst context metasenv t1' t2 ugraph
764 | _ -> raise (UnificationFailure (lazy "88")))
765 | (Cic.MutInd _::_,_) ->
766 let t2' = R.whd ~subst context t2 in
768 C.Appl (C.MutInd _::_) ->
769 fo_unif_subst test_equality_only
770 subst context metasenv t1 t2' ugraph
773 (lazy ("not a mutind :"^
774 CicMetaSubst.ppterm ~metasenv subst t2 ))))
777 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
778 let subst', metasenv',ugraph1 =
779 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
781 let subst'',metasenv'',ugraph2 =
782 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
786 (fun (subst,metasenv,ugraph) t1 t2 ->
788 test_equality_only subst context metasenv t1 t2 ugraph
789 ) (subst'',metasenv'',ugraph2) pl1 pl2
791 Invalid_argument _ ->
792 raise (UnificationFailure (lazy "6.1")))
794 "Error trying to unify %s with %s: the number of branches is not the same."
795 (CicMetaSubst.ppterm ~metasenv subst t1)
796 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
797 | (C.Rel _, _) | (_, C.Rel _) ->
799 subst, metasenv,ugraph
801 raise (UnificationFailure (lazy
803 "Can't unify %s with %s because they are not convertible"
804 (CicMetaSubst.ppterm ~metasenv subst t1)
805 (CicMetaSubst.ppterm ~metasenv subst t2))))
806 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
807 let subst,metasenv,beta_expanded,ugraph1 =
809 test_equality_only metasenv subst context t2 args ugraph
811 fo_unif_subst test_equality_only subst context metasenv
812 (C.Meta (i,l)) beta_expanded ugraph1
813 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
814 let subst,metasenv,beta_expanded,ugraph1 =
816 test_equality_only metasenv subst context t1 args ugraph
818 fo_unif_subst test_equality_only subst context metasenv
819 beta_expanded (C.Meta (i,l)) ugraph1
820 (* Works iff there are no arguments applied to it; similar to the
823 let t1' = R.whd ~subst context t1 in
826 fo_unif_subst test_equality_only
827 subst context metasenv t1' t2 ugraph
828 | _ -> raise (UnificationFailure (lazy "8")))
830 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
831 let subst',metasenv',ugraph1 =
832 fo_unif_subst true subst context metasenv s1 s2 ugraph
834 fo_unif_subst test_equality_only
835 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
837 (match CicReduction.whd ~subst context t2 with
839 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
840 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
842 (match CicReduction.whd ~subst context t1 with
844 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
845 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
847 (* delta-beta reduction should almost never be a problem for
849 1. long computations require iota reduction
850 2. it is extremely rare that a close term t1 (that could be unified
851 to t2) beta-delta reduces to t1' while t2 does not beta-delta
852 reduces in the same way. This happens only if one meta of t2
853 occurs in head position during beta reduction. In this unluky
854 case too much reduction will be performed on t1 and unification
856 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
857 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
858 if t1 = t1' && t2 = t2' then
859 raise (UnificationFailure
862 "Can't unify %s with %s because they are not convertible"
863 (CicMetaSubst.ppterm ~metasenv subst t1)
864 (CicMetaSubst.ppterm ~metasenv subst t2))))
867 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
871 raise (UnificationFailure
874 "Can't unify %s with %s because they are not convertible"
875 (CicMetaSubst.ppterm ~metasenv subst t1)
876 (CicMetaSubst.ppterm ~metasenv subst t2))))
878 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
879 exp_named_subst1 exp_named_subst2 ugraph
883 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
885 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
886 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
888 Invalid_argument _ ->
893 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
896 raise (UnificationFailure (lazy (sprintf
897 "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2))))
899 (* A substitution is a (int * Cic.term) list that associates a *)
900 (* metavariable i with its body. *)
901 (* metasenv is of type Cic.metasenv *)
902 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
903 (* a new substitution which is already unwinded and ready to be applied and *)
904 (* a new metasenv in which some hypothesis in the contexts of the *)
905 (* metavariables may have been restricted. *)
906 let fo_unif metasenv context t1 t2 ugraph =
907 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
909 let enrich_msg msg subst context metasenv t1 t2 ugraph =
912 sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
913 (CicMetaSubst.ppterm ~metasenv subst t1)
915 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
918 | UnificationFailure s
920 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
921 (CicMetaSubst.ppterm ~metasenv subst t2)
923 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
926 | UnificationFailure s
928 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
929 (CicMetaSubst.ppcontext ~metasenv subst context)
930 (CicMetaSubst.ppmetasenv subst metasenv)
931 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
933 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
934 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
936 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
937 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
939 | UnificationFailure s
941 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
942 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
944 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
945 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
947 | UnificationFailure s
949 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
950 (CicMetaSubst.ppcontext ~metasenv subst context)
951 (CicMetaSubst.ppmetasenv subst metasenv)
955 let fo_unif_subst subst context metasenv t1 t2 ugraph =
957 fo_unif_subst false subst context metasenv t1 t2 ugraph
959 | AssertFailure msg ->
960 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
961 | UnificationFailure msg ->
962 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))