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 subst term)
57 (CicMetaSubst.ppterm [] term)
58 (CicMetaSubst.ppcontext subst context)
59 (CicMetaSubst.ppmetasenv subst metasenv)
60 (CicMetaSubst.ppsubst 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 subst term)
68 (CicMetaSubst.ppterm [] term)
69 (CicMetaSubst.ppcontext subst context)
70 (CicMetaSubst.ppmetasenv subst metasenv)
71 (CicMetaSubst.ppsubst 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 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,t) ->
201 let subst,metasenv,s',ugraph1 =
202 aux metasenv subst n context s ugraph in
203 let subst,metasenv,t',ugraph2 =
204 aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
207 (* TASSI: sure this is in serial? *)
208 subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
210 let subst,metasenv,revl',ugraph1 =
212 (fun (subst,metasenv,appl,ugraph) t ->
213 let subst,metasenv,t',ugraph1 =
214 aux metasenv subst n context t ugraph in
215 subst,metasenv,(t'::appl),ugraph1
216 ) (subst,metasenv,[],ugraph) l
218 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
219 | C.Const (uri,exp_named_subst) ->
220 let subst,metasenv,exp_named_subst',ugraph1 =
221 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
223 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
224 | C.MutInd (uri,i,exp_named_subst) ->
225 let subst,metasenv,exp_named_subst',ugraph1 =
226 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
228 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
229 | C.MutConstruct (uri,i,j,exp_named_subst) ->
230 let subst,metasenv,exp_named_subst',ugraph1 =
231 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
233 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
234 | C.MutCase (sp,i,outt,t,pl) ->
235 let subst,metasenv,outt',ugraph1 =
236 aux metasenv subst n context outt ugraph in
237 let subst,metasenv,t',ugraph2 =
238 aux metasenv subst n context t ugraph1 in
239 let subst,metasenv,revpl',ugraph3 =
241 (fun (subst,metasenv,pl,ugraph) t ->
242 let subst,metasenv,t',ugraph1 =
243 aux metasenv subst n context t ugraph in
244 subst,metasenv,(t'::pl),ugraph1
245 ) (subst,metasenv,[],ugraph2) pl
247 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
248 (* TASSI: not sure this is serial *)
250 (*CSC: not implemented
251 let tylen = List.length fl in
254 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
257 C.Fix (i, substitutedfl)
259 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
261 (*CSC: not implemented
262 let tylen = List.length fl in
265 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
268 C.CoFix (i, substitutedfl)
271 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
273 and aux_exp_named_subst metasenv subst n context ens ugraph =
275 (fun (uri,t) (subst,metasenv,l,ugraph) ->
276 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
277 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
279 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
281 FreshNamesGenerator.mk_fresh_name ~subst
282 metasenv context (Cic.Name "Hbeta") ~typ:argty
284 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
285 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
286 subst, metasenv, t'', ugraph2
287 in profiler_beta_expand.HExtlib.profile foo ()
290 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
291 let subst,metasenv,hd,ugraph =
293 (fun arg (subst,metasenv,t,ugraph) ->
294 let subst,metasenv,t,ugraph1 =
295 beta_expand test_equality_only
296 metasenv subst context t arg ugraph
298 subst,metasenv,t,ugraph1
299 ) args (subst,metasenv,t,ugraph)
301 subst,metasenv,hd,ugraph
304 (* NUOVA UNIFICAZIONE *)
305 (* A substitution is a (int * Cic.term) list that associates a
306 metavariable i with its body.
307 A metaenv is a (int * Cic.term) list that associate a metavariable
309 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
310 a new substitution which is _NOT_ unwinded. It must be unwinded before
313 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
314 let module C = Cic in
315 let module R = CicReduction in
316 let module S = CicSubstitution in
317 let t1 = deref subst t1 in
318 let t2 = deref subst t2 in
321 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
322 in profiler_are_convertible.HExtlib.profile foo ()
325 subst, metasenv, ugraph
328 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
329 let _,subst,metasenv,ugraph1 =
332 (fun (j,subst,metasenv,ugraph) t1 t2 ->
335 | _,None -> j+1,subst,metasenv,ugraph
336 | Some t1', Some t2' ->
337 (* First possibility: restriction *)
338 (* Second possibility: unification *)
339 (* Third possibility: convertibility *)
342 ~subst ~metasenv context t1' t2' ugraph
345 j+1,subst,metasenv, ugraph1
348 let subst,metasenv,ugraph2 =
351 subst context metasenv t1' t2' ugraph
353 j+1,subst,metasenv,ugraph2
356 | UnificationFailure _ ->
357 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
358 let metasenv, subst =
359 CicMetaSubst.restrict
360 subst [(n,j)] metasenv in
361 j+1,subst,metasenv,ugraph1)
362 ) (1,subst,metasenv,ugraph) ln lm
366 (UnificationFailure (lazy "1"))
369 "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."
370 (CicMetaSubst.ppterm subst t1)
371 (CicMetaSubst.ppterm subst t2))) *)
372 | Invalid_argument _ ->
374 (UnificationFailure (lazy "2")))
377 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
378 (CicMetaSubst.ppterm subst t1)
379 (CicMetaSubst.ppterm subst t2)))) *)
380 in subst,metasenv,ugraph1
381 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
382 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
384 | (t, C.Meta (n,l)) ->
387 C.Meta (n,_), C.Meta (m,_) when n < m -> false
388 | _, C.Meta _ -> false
391 let lower = fun x y -> if swap then y else x in
392 let upper = fun x y -> if swap then x else y in
393 let fo_unif_subst_ordered
394 test_equality_only subst context metasenv m1 m2 ugraph =
395 fo_unif_subst test_equality_only subst context metasenv
396 (lower m1 m2) (upper m1 m2) ugraph
399 let subst,metasenv,ugraph1 =
400 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
403 type_of_aux' metasenv subst context t ugraph
407 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
409 UnificationFailure _ as e -> raise e
410 | Uncertain msg -> raise (UnificationFailure msg)
412 debug_print (lazy "siamo allo huge hack");
413 (* TODO huge hack!!!!
414 * we keep on unifying/refining in the hope that
415 * the problem will be eventually solved.
416 * In the meantime we're breaking a big invariant:
417 * the terms that we are unifying are no longer well
418 * typed in the current context (in the worst case
419 * we could even diverge) *)
420 (subst, metasenv,ugraph)) in
421 let t',metasenv,subst =
423 CicMetaSubst.delift n subst context metasenv l t
425 (CicMetaSubst.MetaSubstFailure msg)->
426 raise (UnificationFailure msg)
427 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
431 C.Sort (C.Type u) when not test_equality_only ->
432 let u' = CicUniv.fresh () in
433 let s = C.Sort (C.Type u') in
435 CicUniv.add_ge (upper u u') (lower u u') ugraph1
440 (* Unifying the types may have already instantiated n. Let's check *)
442 let (_, oldt,_) = CicUtil.lookup_subst n subst in
443 let lifted_oldt = S.subst_meta l oldt in
444 fo_unif_subst_ordered
445 test_equality_only subst context metasenv t lifted_oldt ugraph2
447 CicUtil.Subst_not_found _ ->
448 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
449 let subst = (n, (context, t'',ty)) :: subst in
451 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
452 subst, metasenv, ugraph2
454 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
455 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
456 if UriManager.eq uri1 uri2 then
457 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
458 exp_named_subst1 exp_named_subst2 ugraph
460 raise (UnificationFailure (lazy
462 "Can't unify %s with %s due to different constants"
463 (CicMetaSubst.ppterm subst t1)
464 (CicMetaSubst.ppterm subst t2))))
465 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
466 if UriManager.eq uri1 uri2 && i1 = i2 then
467 fo_unif_subst_exp_named_subst
469 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
471 raise (UnificationFailure
474 "Can't unify %s with %s due to different inductive principles"
475 (CicMetaSubst.ppterm subst t1)
476 (CicMetaSubst.ppterm subst t2))))
477 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
478 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
479 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
480 fo_unif_subst_exp_named_subst
482 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
484 raise (UnificationFailure
487 "Can't unify %s with %s due to different inductive constructors"
488 (CicMetaSubst.ppterm subst t1)
489 (CicMetaSubst.ppterm subst t2))))
490 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
491 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
492 subst context metasenv te t2 ugraph
493 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
494 subst context metasenv t1 te ugraph
495 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
496 let subst',metasenv',ugraph1 =
497 fo_unif_subst true subst context metasenv s1 s2 ugraph
499 fo_unif_subst test_equality_only
500 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
501 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
502 let subst',metasenv',ugraph1 =
503 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
505 fo_unif_subst test_equality_only
506 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
507 | (C.LetIn (_,s1,t1), t2)
508 | (t2, C.LetIn (_,s1,t1)) ->
510 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
511 | (C.Appl l1, C.Appl l2) ->
512 (* andrea: this case should be probably rewritten in the
515 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
518 (fun (subst,metasenv,ugraph) t1 t2 ->
520 test_equality_only subst context metasenv t1 t2 ugraph)
521 (subst,metasenv,ugraph) l1 l2
522 with (Invalid_argument msg) ->
523 raise (UnificationFailure (lazy msg)))
524 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
525 (* we verify that none of the args is a Meta,
526 since beta expanding with respoect to a metavariable
530 let (_,t,_) = CicUtil.lookup_subst i subst in
531 let lifted = S.subst_meta l t in
532 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
535 subst context metasenv reduced t2 ugraph
536 with CicUtil.Subst_not_found _ -> *)
537 let subst,metasenv,beta_expanded,ugraph1 =
539 test_equality_only metasenv subst context t2 args ugraph
541 fo_unif_subst test_equality_only subst context metasenv
542 (C.Meta (i,l)) beta_expanded ugraph1
543 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
545 let (_,t,_) = CicUtil.lookup_subst i subst in
546 let lifted = S.subst_meta l t in
547 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
550 subst context metasenv t1 reduced ugraph
551 with CicUtil.Subst_not_found _ -> *)
552 let subst,metasenv,beta_expanded,ugraph1 =
555 metasenv subst context t1 args ugraph
557 fo_unif_subst test_equality_only subst context metasenv
558 (C.Meta (i,l)) beta_expanded ugraph1
560 let lr1 = List.rev l1 in
561 let lr2 = List.rev l2 in
563 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
566 | _,[] -> assert false
569 test_equality_only subst context metasenv h1 h2 ugraph
572 fo_unif_subst test_equality_only subst context metasenv
573 h (C.Appl (List.rev l)) ugraph
574 | ((h1::l1),(h2::l2)) ->
575 let subst', metasenv',ugraph1 =
578 subst context metasenv h1 h2 ugraph
581 test_equality_only subst' metasenv' (l1,l2) ugraph1
585 test_equality_only subst metasenv (lr1, lr2) ugraph
587 | UnificationFailure s
588 | Uncertain s as exn ->
590 | (((Cic.Const (uri1, ens1)) as c1) :: tl1),
591 (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
592 CoercGraph.is_a_coercion c1 &&
593 CoercGraph.is_a_coercion c2 &&
594 not (UriManager.eq uri1 uri2) ->
595 let body1, attrs1, ugraph =
596 match CicEnvironment.get_obj ugraph uri1 with
597 | Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
600 let body2, attrs2, ugraph =
601 match CicEnvironment.get_obj ugraph uri2 with
602 | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
607 (function `Class (`Coercion _) -> true | _-> false)
612 (function `Class (`Coercion _) -> true | _-> false)
615 (match is_composite1, is_composite2 with
616 | false, false -> raise exn
618 let body1 = CicSubstitution.subst_vars ens1 body1 in
619 let appl = Cic.Appl (body1::tl1) in
620 let redappl = CicReduction.head_beta_reduce appl in
622 test_equality_only subst context metasenv
625 let body2 = CicSubstitution.subst_vars ens2 body2 in
626 let appl = Cic.Appl (body2::tl2) in
627 let redappl = CicReduction.head_beta_reduce appl in
629 test_equality_only subst context metasenv
632 let body1 = CicSubstitution.subst_vars ens1 body1 in
633 let appl1 = Cic.Appl (body1::tl1) in
634 let redappl1 = CicReduction.head_beta_reduce appl1 in
635 let body2 = CicSubstitution.subst_vars ens2 body2 in
636 let appl2 = Cic.Appl (body2::tl2) in
637 let redappl2 = CicReduction.head_beta_reduce appl2 in
639 test_equality_only subst context metasenv
640 redappl1 redappl2 ugraph)
641 (*CSC: This is necessary because of the "elim H" tactic
642 where the type of H is only reducible to an
643 inductive type. This could be extended from inductive
644 types to any rigid term. However, the code is
645 duplicated in two places: inside applications and
646 outside them. Probably it would be better to
647 work with lambda-bar terms instead. *)
648 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
649 | (_, Cic.MutInd _::_) ->
650 let t1' = R.whd ~subst context t1 in
652 C.Appl (C.MutInd _::_) ->
653 fo_unif_subst test_equality_only
654 subst context metasenv t1' t2 ugraph
655 | _ -> raise (UnificationFailure (lazy "88")))
656 | (Cic.MutInd _::_,_) ->
657 let t2' = R.whd ~subst context t2 in
659 C.Appl (C.MutInd _::_) ->
660 fo_unif_subst test_equality_only
661 subst context metasenv t1 t2' ugraph
664 (lazy ("not a mutind :"^CicMetaSubst.ppterm subst t2 ))))
666 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
667 let subst', metasenv',ugraph1 =
668 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
670 let subst'',metasenv'',ugraph2 =
671 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
675 (fun (subst,metasenv,ugraph) t1 t2 ->
677 test_equality_only subst context metasenv t1 t2 ugraph
678 ) (subst'',metasenv'',ugraph2) pl1 pl2
680 Invalid_argument _ ->
681 raise (UnificationFailure (lazy "6.1")))
683 "Error trying to unify %s with %s: the number of branches is not the same."
684 (CicMetaSubst.ppterm subst t1)
685 (CicMetaSubst.ppterm subst t2)))) *)
686 | (C.Rel _, _) | (_, C.Rel _) ->
688 subst, metasenv,ugraph
690 raise (UnificationFailure (lazy
692 "Can't unify %s with %s because they are not convertible"
693 (CicMetaSubst.ppterm subst t1)
694 (CicMetaSubst.ppterm subst t2))))
695 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
696 let subst,metasenv,beta_expanded,ugraph1 =
698 test_equality_only metasenv subst context t2 args ugraph
700 fo_unif_subst test_equality_only subst context metasenv
701 (C.Meta (i,l)) beta_expanded ugraph1
702 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
703 let subst,metasenv,beta_expanded,ugraph1 =
705 test_equality_only metasenv subst context t1 args ugraph
707 fo_unif_subst test_equality_only subst context metasenv
708 beta_expanded (C.Meta (i,l)) ugraph1
709 (* Works iff there are no arguments applied to it; similar to the
712 let t1' = R.whd ~subst context t1 in
715 fo_unif_subst test_equality_only
716 subst context metasenv t1' t2 ugraph
717 | _ -> raise (UnificationFailure (lazy "8")))
719 (* The following idea could be exploited again; right now we have no
720 longer any example requiring it
722 let t2' = R.whd ~subst context t2 in
725 fo_unif_subst test_equality_only
726 subst context metasenv t1 t2' ugraph
727 | _ -> raise (UnificationFailure (lazy "8")))
729 let t1' = R.whd ~subst context t1 in
732 fo_unif_subst test_equality_only
733 subst context metasenv t1' t2 ugraph
734 | _ -> (* raise (UnificationFailure "9")) *)
736 (UnificationFailure (lazy (sprintf
737 "Can't unify %s with %s because they are not convertible"
738 (CicMetaSubst.ppterm subst t1)
739 (CicMetaSubst.ppterm subst t2)))))
742 (* delta-beta reduction should almost never be a problem for
744 1. long computations require iota reduction
745 2. it is extremely rare that a close term t1 (that could be unified
746 to t2) beta-delta reduces to t1' while t2 does not beta-delta
747 reduces in the same way. This happens only if one meta of t2
748 occurs in head position during beta reduction. In this unluky
749 case too much reduction will be performed on t1 and unification
751 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
752 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
753 if t1 = t1' && t2 = t2' then
754 raise (UnificationFailure
757 "Can't unify %s with %s because they are not convertible"
758 (CicMetaSubst.ppterm subst t1)
759 (CicMetaSubst.ppterm subst t2))))
762 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
766 raise (UnificationFailure
769 "Can't unify %s with %s because they are not convertible"
770 (CicMetaSubst.ppterm subst t1)
771 (CicMetaSubst.ppterm subst t2))))
773 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
774 exp_named_subst1 exp_named_subst2 ugraph
778 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
780 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
781 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
783 Invalid_argument _ ->
788 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
791 raise (UnificationFailure (lazy (sprintf
792 "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))))
794 (* A substitution is a (int * Cic.term) list that associates a *)
795 (* metavariable i with its body. *)
796 (* metasenv is of type Cic.metasenv *)
797 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
798 (* a new substitution which is already unwinded and ready to be applied and *)
799 (* a new metasenv in which some hypothesis in the contexts of the *)
800 (* metavariables may have been restricted. *)
801 let fo_unif metasenv context t1 t2 ugraph =
802 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
804 let enrich_msg msg subst context metasenv t1 t2 ugraph =
807 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"
808 (CicMetaSubst.ppterm subst t1)
810 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
813 | UnificationFailure s
815 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
816 (CicMetaSubst.ppterm subst t2)
818 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
821 | UnificationFailure s
823 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
824 (CicMetaSubst.ppcontext subst context)
825 (CicMetaSubst.ppmetasenv subst metasenv)
826 (CicMetaSubst.ppsubst subst) (Lazy.force msg)
828 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
829 (CicMetaSubst.ppterm_in_context subst t1 context)
831 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
832 CicMetaSubst.ppterm_in_context subst ty_t1 context
834 | UnificationFailure s
836 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
837 (CicMetaSubst.ppterm_in_context subst t2 context)
839 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
840 CicMetaSubst.ppterm_in_context subst ty_t2 context
842 | UnificationFailure s
844 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
845 (CicMetaSubst.ppcontext subst context)
846 (CicMetaSubst.ppmetasenv subst metasenv)
850 let fo_unif_subst subst context metasenv t1 t2 ugraph =
852 fo_unif_subst false subst context metasenv t1 t2 ugraph
854 | AssertFailure msg ->
855 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
856 | UnificationFailure msg ->
857 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))