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 ()
77 List.exists (function Cic.Meta _ -> true | _ -> false) l
79 let rec deref subst t =
80 let snd (_,a,_) = a in
85 (CicSubstitution.subst_meta
86 l (snd (CicUtil.lookup_subst n subst)))
88 CicUtil.Subst_not_found _ -> t)
89 | Cic.Appl(Cic.Meta(n,l)::args) ->
90 (match deref subst (Cic.Meta(n,l)) with
91 | Cic.Lambda _ as t ->
92 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
93 | r -> Cic.Appl(r::args))
94 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
95 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
100 let foo () = deref subst t
101 in profiler_deref.HExtlib.profile foo ()
103 exception WrongShape;;
104 let eta_reduce after_beta_expansion after_beta_expansion_body
105 before_beta_expansion
108 match before_beta_expansion,after_beta_expansion_body with
109 Cic.Appl l, Cic.Appl l' ->
110 let rec all_but_last check_last =
114 | [_] -> if check_last then raise WrongShape else []
115 | he::tl -> he::(all_but_last check_last tl)
117 let all_but_last check_last l =
118 match all_but_last check_last l with
123 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
124 let all_but_last = all_but_last false l in
125 (* here we should test alpha-equivalence; however we know by
126 construction that here alpha_equivalence is equivalent to = *)
127 if t = all_but_last then
131 | _,_ -> after_beta_expansion
133 WrongShape -> after_beta_expansion
135 let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
136 let module S = CicSubstitution in
137 let module C = Cic in
139 let rec aux metasenv subst n context t' ugraph =
142 let subst,metasenv,ugraph1 =
143 fo_unif_subst test_equality_only subst context metasenv
144 (CicSubstitution.lift n arg) t' ugraph
147 subst,metasenv,C.Rel (1 + n),ugraph1
150 | UnificationFailure _ ->
152 | C.Rel m -> subst,metasenv,
153 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
154 | C.Var (uri,exp_named_subst) ->
155 let subst,metasenv,exp_named_subst',ugraph1 =
156 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
158 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
160 (* andrea: in general, beta_expand can create badly typed
161 terms. This happens quite seldom in practice, UNLESS we
162 iterate on the local context. For this reason, we renounce
163 to iterate and just lift *)
167 Some t -> Some (CicSubstitution.lift 1 t)
169 subst, metasenv, C.Meta (i,l), ugraph
171 | C.Implicit _ as t -> subst,metasenv,t,ugraph
173 let subst,metasenv,te',ugraph1 =
174 aux metasenv subst n context te ugraph in
175 let subst,metasenv,ty',ugraph2 =
176 aux metasenv subst n context ty ugraph1 in
177 (* TASSI: sure this is in serial? *)
178 subst,metasenv,(C.Cast (te', ty')),ugraph2
180 let subst,metasenv,s',ugraph1 =
181 aux metasenv subst n context s ugraph in
182 let subst,metasenv,t',ugraph2 =
183 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
186 (* TASSI: sure this is in serial? *)
187 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
188 | C.Lambda (nn,s,t) ->
189 let subst,metasenv,s',ugraph1 =
190 aux metasenv subst n context s ugraph in
191 let subst,metasenv,t',ugraph2 =
192 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
194 (* TASSI: sure this is in serial? *)
195 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
196 | C.LetIn (nn,s,t) ->
197 let subst,metasenv,s',ugraph1 =
198 aux metasenv subst n context s ugraph in
199 let subst,metasenv,t',ugraph2 =
200 aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
203 (* TASSI: sure this is in serial? *)
204 subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
206 let subst,metasenv,revl',ugraph1 =
208 (fun (subst,metasenv,appl,ugraph) t ->
209 let subst,metasenv,t',ugraph1 =
210 aux metasenv subst n context t ugraph in
211 subst,metasenv,(t'::appl),ugraph1
212 ) (subst,metasenv,[],ugraph) l
214 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
215 | C.Const (uri,exp_named_subst) ->
216 let subst,metasenv,exp_named_subst',ugraph1 =
217 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
219 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
220 | C.MutInd (uri,i,exp_named_subst) ->
221 let subst,metasenv,exp_named_subst',ugraph1 =
222 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
224 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
225 | C.MutConstruct (uri,i,j,exp_named_subst) ->
226 let subst,metasenv,exp_named_subst',ugraph1 =
227 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
229 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
230 | C.MutCase (sp,i,outt,t,pl) ->
231 let subst,metasenv,outt',ugraph1 =
232 aux metasenv subst n context outt ugraph in
233 let subst,metasenv,t',ugraph2 =
234 aux metasenv subst n context t ugraph1 in
235 let subst,metasenv,revpl',ugraph3 =
237 (fun (subst,metasenv,pl,ugraph) t ->
238 let subst,metasenv,t',ugraph1 =
239 aux metasenv subst n context t ugraph in
240 subst,metasenv,(t'::pl),ugraph1
241 ) (subst,metasenv,[],ugraph2) pl
243 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
244 (* TASSI: not sure this is serial *)
246 (*CSC: not implemented
247 let tylen = List.length fl in
250 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
253 C.Fix (i, substitutedfl)
255 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
257 (*CSC: not implemented
258 let tylen = List.length fl in
261 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
264 C.CoFix (i, substitutedfl)
267 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
269 and aux_exp_named_subst metasenv subst n context ens ugraph =
271 (fun (uri,t) (subst,metasenv,l,ugraph) ->
272 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
273 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
275 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
277 FreshNamesGenerator.mk_fresh_name ~subst
278 metasenv context (Cic.Name "Hbeta") ~typ:argty
280 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
281 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
282 subst, metasenv, t'', ugraph2
283 in profiler_beta_expand.HExtlib.profile foo ()
286 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
287 let subst,metasenv,hd,ugraph =
289 (fun arg (subst,metasenv,t,ugraph) ->
290 let subst,metasenv,t,ugraph1 =
291 beta_expand test_equality_only
292 metasenv subst context t arg ugraph
294 subst,metasenv,t,ugraph1
295 ) args (subst,metasenv,t,ugraph)
297 subst,metasenv,hd,ugraph
300 (* NUOVA UNIFICAZIONE *)
301 (* A substitution is a (int * Cic.term) list that associates a
302 metavariable i with its body.
303 A metaenv is a (int * Cic.term) list that associate a metavariable
305 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
306 a new substitution which is _NOT_ unwinded. It must be unwinded before
309 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
310 let module C = Cic in
311 let module R = CicReduction in
312 let module S = CicSubstitution in
313 let t1 = deref subst t1 in
314 let t2 = deref subst t2 in
317 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
318 in profiler_are_convertible.HExtlib.profile foo ()
321 subst, metasenv, ugraph
324 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
325 let _,subst,metasenv,ugraph1 =
328 (fun (j,subst,metasenv,ugraph) t1 t2 ->
331 | _,None -> j+1,subst,metasenv,ugraph
332 | Some t1', Some t2' ->
333 (* First possibility: restriction *)
334 (* Second possibility: unification *)
335 (* Third possibility: convertibility *)
338 ~subst ~metasenv context t1' t2' ugraph
341 j+1,subst,metasenv, ugraph1
344 let subst,metasenv,ugraph2 =
347 subst context metasenv t1' t2' ugraph
349 j+1,subst,metasenv,ugraph2
352 | UnificationFailure _ ->
353 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
354 let metasenv, subst =
355 CicMetaSubst.restrict
356 subst [(n,j)] metasenv in
357 j+1,subst,metasenv,ugraph1)
358 ) (1,subst,metasenv,ugraph) ln lm
362 (UnificationFailure (lazy "1"))
365 "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."
366 (CicMetaSubst.ppterm subst t1)
367 (CicMetaSubst.ppterm subst t2))) *)
368 | Invalid_argument _ ->
370 (UnificationFailure (lazy "2")))
373 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
374 (CicMetaSubst.ppterm subst t1)
375 (CicMetaSubst.ppterm subst t2)))) *)
376 in subst,metasenv,ugraph1
377 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
378 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
380 | (t, C.Meta (n,l)) ->
383 C.Meta (n,_), C.Meta (m,_) when n < m -> false
384 | _, C.Meta _ -> false
387 let lower = fun x y -> if swap then y else x in
388 let upper = fun x y -> if swap then x else y in
389 let fo_unif_subst_ordered
390 test_equality_only subst context metasenv m1 m2 ugraph =
391 fo_unif_subst test_equality_only subst context metasenv
392 (lower m1 m2) (upper m1 m2) ugraph
395 let subst,metasenv,ugraph1 =
396 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
399 type_of_aux' metasenv subst context t ugraph
403 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
405 UnificationFailure _ as e -> raise e
406 | Uncertain msg -> raise (UnificationFailure msg)
408 debug_print (lazy "siamo allo huge hack");
409 (* TODO huge hack!!!!
410 * we keep on unifying/refining in the hope that
411 * the problem will be eventually solved.
412 * In the meantime we're breaking a big invariant:
413 * the terms that we are unifying are no longer well
414 * typed in the current context (in the worst case
415 * we could even diverge) *)
416 (subst, metasenv,ugraph)) in
417 let t',metasenv,subst =
419 CicMetaSubst.delift n subst context metasenv l t
421 (CicMetaSubst.MetaSubstFailure msg)->
422 raise (UnificationFailure msg)
423 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
427 C.Sort (C.Type u) when not test_equality_only ->
428 let u' = CicUniv.fresh () in
429 let s = C.Sort (C.Type u') in
431 CicUniv.add_ge (upper u u') (lower u u') ugraph1
436 (* Unifying the types may have already instantiated n. Let's check *)
438 let (_, oldt,_) = CicUtil.lookup_subst n subst in
439 let lifted_oldt = S.subst_meta l oldt in
440 fo_unif_subst_ordered
441 test_equality_only subst context metasenv t lifted_oldt ugraph2
443 CicUtil.Subst_not_found _ ->
444 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
445 let subst = (n, (context, t'',ty)) :: subst in
447 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
448 subst, metasenv, ugraph2
450 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
451 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
452 if UriManager.eq uri1 uri2 then
453 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
454 exp_named_subst1 exp_named_subst2 ugraph
456 raise (UnificationFailure (lazy
458 "Can't unify %s with %s due to different constants"
459 (CicMetaSubst.ppterm subst t1)
460 (CicMetaSubst.ppterm subst t2))))
461 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
462 if UriManager.eq uri1 uri2 && i1 = i2 then
463 fo_unif_subst_exp_named_subst
465 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
467 raise (UnificationFailure (lazy "4"))
469 "Can't unify %s with %s due to different inductive principles"
470 (CicMetaSubst.ppterm subst t1)
471 (CicMetaSubst.ppterm subst t2))) *)
472 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
473 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
474 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
475 fo_unif_subst_exp_named_subst
477 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
479 raise (UnificationFailure (lazy "5"))
481 "Can't unify %s with %s due to different inductive constructors"
482 (CicMetaSubst.ppterm subst t1)
483 (CicMetaSubst.ppterm subst t2))) *)
484 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
485 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
486 subst context metasenv te t2 ugraph
487 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
488 subst context metasenv t1 te ugraph
489 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
490 let subst',metasenv',ugraph1 =
491 fo_unif_subst true subst context metasenv s1 s2 ugraph
493 fo_unif_subst test_equality_only
494 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
495 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
496 let subst',metasenv',ugraph1 =
497 fo_unif_subst test_equality_only 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.LetIn (_,s1,t1), t2)
502 | (t2, C.LetIn (_,s1,t1)) ->
504 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
505 | (C.Appl l1, C.Appl l2) ->
506 (* andrea: this case should be probably rewritten in the
509 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
512 (fun (subst,metasenv,ugraph) t1 t2 ->
514 test_equality_only subst context metasenv t1 t2 ugraph)
515 (subst,metasenv,ugraph) l1 l2
516 with (Invalid_argument msg) ->
517 raise (UnificationFailure (lazy msg)))
518 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
519 (* we verify that none of the args is a Meta,
520 since beta expanding with respoect to a metavariable
524 let (_,t,_) = CicUtil.lookup_subst i subst in
525 let lifted = S.subst_meta l t in
526 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
529 subst context metasenv reduced t2 ugraph
530 with CicUtil.Subst_not_found _ -> *)
531 let subst,metasenv,beta_expanded,ugraph1 =
533 test_equality_only metasenv subst context t2 args ugraph
535 fo_unif_subst test_equality_only subst context metasenv
536 (C.Meta (i,l)) beta_expanded ugraph1
537 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
539 let (_,t,_) = CicUtil.lookup_subst i subst in
540 let lifted = S.subst_meta l t in
541 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
544 subst context metasenv t1 reduced ugraph
545 with CicUtil.Subst_not_found _ -> *)
546 let subst,metasenv,beta_expanded,ugraph1 =
549 metasenv subst context t1 args ugraph
551 fo_unif_subst test_equality_only subst context metasenv
552 (C.Meta (i,l)) beta_expanded ugraph1
554 let lr1 = List.rev l1 in
555 let lr2 = List.rev l2 in
557 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
560 | _,[] -> assert false
563 test_equality_only subst context metasenv h1 h2 ugraph
566 fo_unif_subst test_equality_only subst context metasenv
567 h (C.Appl (List.rev l)) ugraph
568 | ((h1::l1),(h2::l2)) ->
569 let subst', metasenv',ugraph1 =
572 subst context metasenv h1 h2 ugraph
575 test_equality_only subst' metasenv' (l1,l2) ugraph1
579 test_equality_only subst metasenv (lr1, lr2) ugraph
581 | UnificationFailure _
582 | Uncertain _ as exn ->
584 | (((Cic.Const (uri1, ens1)) as c1) :: tl1),
585 (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
586 CoercGraph.is_a_coercion c1 &&
587 CoercGraph.is_a_coercion c2 ->
588 let body1, attrs1, ugraph =
589 match CicEnvironment.get_obj ugraph uri1 with
590 | Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
593 let body2, attrs2, ugraph =
594 match CicEnvironment.get_obj ugraph uri2 with
595 | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
599 List.exists ((=) (`Class `Coercion)) attrs1 in
601 List.exists ((=) (`Class `Coercion)) attrs2 in
602 (match is_composite1, is_composite2 with
603 | false, false -> raise exn
605 let body1 = CicSubstitution.subst_vars ens1 body1 in
606 let appl = Cic.Appl (body1::tl1) in
607 let redappl = CicReduction.head_beta_reduce appl in
609 test_equality_only subst context metasenv
612 let body2 = CicSubstitution.subst_vars ens2 body2 in
613 let appl = Cic.Appl (body2::tl2) in
614 let redappl = CicReduction.head_beta_reduce appl in
616 test_equality_only subst context metasenv
619 let body1 = CicSubstitution.subst_vars ens1 body1 in
620 let appl1 = Cic.Appl (body1::tl1) in
621 let redappl1 = CicReduction.head_beta_reduce appl1 in
622 let body2 = CicSubstitution.subst_vars ens2 body2 in
623 let appl2 = Cic.Appl (body2::tl2) in
624 let redappl2 = CicReduction.head_beta_reduce appl2 in
626 test_equality_only subst context metasenv
627 redappl1 redappl2 ugraph)
628 (*CSC: This is necessary because of the "elim H" tactic
629 where the type of H is only reducible to an
630 inductive type. This could be extended from inductive
631 types to any rigid term. However, the code is
632 duplicated in two places: inside applications and
633 outside them. Probably it would be better to
634 work with lambda-bar terms instead. *)
635 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
636 | (_, Cic.MutInd _::_) ->
637 let t1' = R.whd ~subst context t1 in
639 C.Appl (C.MutInd _::_) ->
640 fo_unif_subst test_equality_only
641 subst context metasenv t1' t2 ugraph
642 | _ -> raise (UnificationFailure (lazy "88")))
643 | (Cic.MutInd _::_,_) ->
644 let t2' = R.whd ~subst context t2 in
646 C.Appl (C.MutInd _::_) ->
647 fo_unif_subst test_equality_only
648 subst context metasenv t1 t2' ugraph
649 | _ -> raise (UnificationFailure (lazy "99")))
651 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
652 let subst', metasenv',ugraph1 =
653 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
655 let subst'',metasenv'',ugraph2 =
656 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
660 (fun (subst,metasenv,ugraph) t1 t2 ->
662 test_equality_only subst context metasenv t1 t2 ugraph
663 ) (subst'',metasenv'',ugraph2) pl1 pl2
665 Invalid_argument _ ->
666 raise (UnificationFailure (lazy "6.1")))
668 "Error trying to unify %s with %s: the number of branches is not the same."
669 (CicMetaSubst.ppterm subst t1)
670 (CicMetaSubst.ppterm subst t2)))) *)
671 | (C.Rel _, _) | (_, C.Rel _) ->
673 subst, metasenv,ugraph
675 raise (UnificationFailure (lazy
677 "Can't unify %s with %s because they are not convertible"
678 (CicMetaSubst.ppterm subst t1)
679 (CicMetaSubst.ppterm subst t2))))
680 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
681 let subst,metasenv,beta_expanded,ugraph1 =
683 test_equality_only metasenv subst context t2 args ugraph
685 fo_unif_subst test_equality_only subst context metasenv
686 (C.Meta (i,l)) beta_expanded ugraph1
687 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
688 let subst,metasenv,beta_expanded,ugraph1 =
690 test_equality_only metasenv subst context t1 args ugraph
692 fo_unif_subst test_equality_only subst context metasenv
693 beta_expanded (C.Meta (i,l)) ugraph1
694 (* Works iff there are no arguments applied to it; similar to the
697 let t1' = R.whd ~subst context t1 in
700 fo_unif_subst test_equality_only
701 subst context metasenv t1' t2 ugraph
702 | _ -> raise (UnificationFailure (lazy "8")))
704 (* The following idea could be exploited again; right now we have no
705 longer any example requiring it
707 let t2' = R.whd ~subst context t2 in
710 fo_unif_subst test_equality_only
711 subst context metasenv t1 t2' ugraph
712 | _ -> raise (UnificationFailure (lazy "8")))
714 let t1' = R.whd ~subst context t1 in
717 fo_unif_subst test_equality_only
718 subst context metasenv t1' t2 ugraph
719 | _ -> (* raise (UnificationFailure "9")) *)
721 (UnificationFailure (lazy (sprintf
722 "Can't unify %s with %s because they are not convertible"
723 (CicMetaSubst.ppterm subst t1)
724 (CicMetaSubst.ppterm subst t2)))))
727 (* delta-beta reduction should almost never be a problem for
729 1. long computations require iota reduction
730 2. it is extremely rare that a close term t1 (that could be unified
731 to t2) beta-delta reduces to t1' while t2 does not beta-delta
732 reduces in the same way. This happens only if one meta of t2
733 occurs in head position during beta reduction. In this unluky
734 case too much reduction will be performed on t1 and unification
736 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
737 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
738 if t1 = t1' && t2 = t2' then
739 raise (UnificationFailure
742 "Can't unify %s with %s because they are not convertible"
743 (CicMetaSubst.ppterm subst t1)
744 (CicMetaSubst.ppterm subst t2))))
747 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
751 raise (UnificationFailure
754 "Can't unify %s with %s because they are not convertible"
755 (CicMetaSubst.ppterm subst t1)
756 (CicMetaSubst.ppterm subst t2))))
758 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
759 exp_named_subst1 exp_named_subst2 ugraph
763 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
765 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
766 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
768 Invalid_argument _ ->
773 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
776 raise (UnificationFailure (lazy (sprintf
777 "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))))
779 (* A substitution is a (int * Cic.term) list that associates a *)
780 (* metavariable i with its body. *)
781 (* metasenv is of type Cic.metasenv *)
782 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
783 (* a new substitution which is already unwinded and ready to be applied and *)
784 (* a new metasenv in which some hypothesis in the contexts of the *)
785 (* metavariables may have been restricted. *)
786 let fo_unif metasenv context t1 t2 ugraph =
787 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
789 let enrich_msg msg subst context metasenv t1 t2 ugraph =
792 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"
793 (CicMetaSubst.ppterm subst t1)
795 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
798 | UnificationFailure s
800 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
801 (CicMetaSubst.ppterm subst t2)
803 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
806 | UnificationFailure s
808 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
809 (CicMetaSubst.ppcontext subst context)
810 (CicMetaSubst.ppmetasenv subst metasenv)
811 (CicMetaSubst.ppsubst subst) (Lazy.force msg)
813 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
814 (CicMetaSubst.ppterm_in_context subst t1 context)
816 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
817 CicMetaSubst.ppterm_in_context subst ty_t1 context
819 | UnificationFailure s
821 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
822 (CicMetaSubst.ppterm_in_context subst t2 context)
824 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
825 CicMetaSubst.ppterm_in_context subst ty_t2 context
827 | UnificationFailure s
829 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
830 (CicMetaSubst.ppcontext subst context)
831 (CicMetaSubst.ppmetasenv subst metasenv)
835 let fo_unif_subst subst context metasenv t1 t2 ugraph =
837 fo_unif_subst false subst context metasenv t1 t2 ugraph
839 | AssertFailure msg ->
840 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
841 | UnificationFailure msg ->
842 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))