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
470 "Can't unify %s with %s due to different inductive principles"
471 (CicMetaSubst.ppterm subst t1)
472 (CicMetaSubst.ppterm subst t2))))
473 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
474 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
475 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
476 fo_unif_subst_exp_named_subst
478 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
480 raise (UnificationFailure
483 "Can't unify %s with %s due to different inductive constructors"
484 (CicMetaSubst.ppterm subst t1)
485 (CicMetaSubst.ppterm subst t2))))
486 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
487 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
488 subst context metasenv te t2 ugraph
489 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
490 subst context metasenv t1 te ugraph
491 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
492 let subst',metasenv',ugraph1 =
493 fo_unif_subst true subst context metasenv s1 s2 ugraph
495 fo_unif_subst test_equality_only
496 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
497 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
498 let subst',metasenv',ugraph1 =
499 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
501 fo_unif_subst test_equality_only
502 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
503 | (C.LetIn (_,s1,t1), t2)
504 | (t2, C.LetIn (_,s1,t1)) ->
506 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
507 | (C.Appl l1, C.Appl l2) ->
508 (* andrea: this case should be probably rewritten in the
511 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
514 (fun (subst,metasenv,ugraph) t1 t2 ->
516 test_equality_only subst context metasenv t1 t2 ugraph)
517 (subst,metasenv,ugraph) l1 l2
518 with (Invalid_argument msg) ->
519 raise (UnificationFailure (lazy msg)))
520 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
521 (* we verify that none of the args is a Meta,
522 since beta expanding with respoect to a metavariable
526 let (_,t,_) = CicUtil.lookup_subst i subst in
527 let lifted = S.subst_meta l t in
528 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
531 subst context metasenv reduced t2 ugraph
532 with CicUtil.Subst_not_found _ -> *)
533 let subst,metasenv,beta_expanded,ugraph1 =
535 test_equality_only metasenv subst context t2 args ugraph
537 fo_unif_subst test_equality_only subst context metasenv
538 (C.Meta (i,l)) beta_expanded ugraph1
539 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
541 let (_,t,_) = CicUtil.lookup_subst i subst in
542 let lifted = S.subst_meta l t in
543 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
546 subst context metasenv t1 reduced ugraph
547 with CicUtil.Subst_not_found _ -> *)
548 let subst,metasenv,beta_expanded,ugraph1 =
551 metasenv subst context t1 args ugraph
553 fo_unif_subst test_equality_only subst context metasenv
554 (C.Meta (i,l)) beta_expanded ugraph1
556 let lr1 = List.rev l1 in
557 let lr2 = List.rev l2 in
559 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
562 | _,[] -> assert false
565 test_equality_only subst context metasenv h1 h2 ugraph
568 fo_unif_subst test_equality_only subst context metasenv
569 h (C.Appl (List.rev l)) ugraph
570 | ((h1::l1),(h2::l2)) ->
571 let subst', metasenv',ugraph1 =
574 subst context metasenv h1 h2 ugraph
577 test_equality_only subst' metasenv' (l1,l2) ugraph1
581 test_equality_only subst metasenv (lr1, lr2) ugraph
583 | UnificationFailure s
584 | Uncertain s as exn ->
586 | (((Cic.Const (uri1, ens1)) as c1) :: tl1),
587 (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
588 CoercGraph.is_a_coercion c1 &&
589 CoercGraph.is_a_coercion c2 &&
590 not (UriManager.eq uri1 uri2) ->
591 let body1, attrs1, ugraph =
592 match CicEnvironment.get_obj ugraph uri1 with
593 | Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
596 let body2, attrs2, ugraph =
597 match CicEnvironment.get_obj ugraph uri2 with
598 | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
603 (function `Class (`Coercion _) -> true | _-> false)
608 (function `Class (`Coercion _) -> true | _-> false)
611 (match is_composite1, is_composite2 with
612 | false, false -> raise exn
614 let body1 = CicSubstitution.subst_vars ens1 body1 in
615 let appl = Cic.Appl (body1::tl1) in
616 let redappl = CicReduction.head_beta_reduce appl in
618 test_equality_only subst context metasenv
621 let body2 = CicSubstitution.subst_vars ens2 body2 in
622 let appl = Cic.Appl (body2::tl2) in
623 let redappl = CicReduction.head_beta_reduce appl in
625 test_equality_only subst context metasenv
628 let body1 = CicSubstitution.subst_vars ens1 body1 in
629 let appl1 = Cic.Appl (body1::tl1) in
630 let redappl1 = CicReduction.head_beta_reduce appl1 in
631 let body2 = CicSubstitution.subst_vars ens2 body2 in
632 let appl2 = Cic.Appl (body2::tl2) in
633 let redappl2 = CicReduction.head_beta_reduce appl2 in
635 test_equality_only subst context metasenv
636 redappl1 redappl2 ugraph)
637 (*CSC: This is necessary because of the "elim H" tactic
638 where the type of H is only reducible to an
639 inductive type. This could be extended from inductive
640 types to any rigid term. However, the code is
641 duplicated in two places: inside applications and
642 outside them. Probably it would be better to
643 work with lambda-bar terms instead. *)
644 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
645 | (_, Cic.MutInd _::_) ->
646 let t1' = R.whd ~subst context t1 in
648 C.Appl (C.MutInd _::_) ->
649 fo_unif_subst test_equality_only
650 subst context metasenv t1' t2 ugraph
651 | _ -> raise (UnificationFailure (lazy "88")))
652 | (Cic.MutInd _::_,_) ->
653 let t2' = R.whd ~subst context t2 in
655 C.Appl (C.MutInd _::_) ->
656 fo_unif_subst test_equality_only
657 subst context metasenv t1 t2' ugraph
658 | _ -> raise (UnificationFailure (lazy "99")))
660 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
661 let subst', metasenv',ugraph1 =
662 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
664 let subst'',metasenv'',ugraph2 =
665 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
669 (fun (subst,metasenv,ugraph) t1 t2 ->
671 test_equality_only subst context metasenv t1 t2 ugraph
672 ) (subst'',metasenv'',ugraph2) pl1 pl2
674 Invalid_argument _ ->
675 raise (UnificationFailure (lazy "6.1")))
677 "Error trying to unify %s with %s: the number of branches is not the same."
678 (CicMetaSubst.ppterm subst t1)
679 (CicMetaSubst.ppterm subst t2)))) *)
680 | (C.Rel _, _) | (_, C.Rel _) ->
682 subst, metasenv,ugraph
684 raise (UnificationFailure (lazy
686 "Can't unify %s with %s because they are not convertible"
687 (CicMetaSubst.ppterm subst t1)
688 (CicMetaSubst.ppterm subst t2))))
689 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
690 let subst,metasenv,beta_expanded,ugraph1 =
692 test_equality_only metasenv subst context t2 args ugraph
694 fo_unif_subst test_equality_only subst context metasenv
695 (C.Meta (i,l)) beta_expanded ugraph1
696 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
697 let subst,metasenv,beta_expanded,ugraph1 =
699 test_equality_only metasenv subst context t1 args ugraph
701 fo_unif_subst test_equality_only subst context metasenv
702 beta_expanded (C.Meta (i,l)) ugraph1
703 (* Works iff there are no arguments applied to it; similar to the
706 let t1' = R.whd ~subst context t1 in
709 fo_unif_subst test_equality_only
710 subst context metasenv t1' t2 ugraph
711 | _ -> raise (UnificationFailure (lazy "8")))
713 (* The following idea could be exploited again; right now we have no
714 longer any example requiring it
716 let t2' = R.whd ~subst context t2 in
719 fo_unif_subst test_equality_only
720 subst context metasenv t1 t2' ugraph
721 | _ -> raise (UnificationFailure (lazy "8")))
723 let t1' = R.whd ~subst context t1 in
726 fo_unif_subst test_equality_only
727 subst context metasenv t1' t2 ugraph
728 | _ -> (* raise (UnificationFailure "9")) *)
730 (UnificationFailure (lazy (sprintf
731 "Can't unify %s with %s because they are not convertible"
732 (CicMetaSubst.ppterm subst t1)
733 (CicMetaSubst.ppterm subst t2)))))
736 (* delta-beta reduction should almost never be a problem for
738 1. long computations require iota reduction
739 2. it is extremely rare that a close term t1 (that could be unified
740 to t2) beta-delta reduces to t1' while t2 does not beta-delta
741 reduces in the same way. This happens only if one meta of t2
742 occurs in head position during beta reduction. In this unluky
743 case too much reduction will be performed on t1 and unification
745 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
746 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
747 if t1 = t1' && t2 = t2' then
748 raise (UnificationFailure
751 "Can't unify %s with %s because they are not convertible"
752 (CicMetaSubst.ppterm subst t1)
753 (CicMetaSubst.ppterm subst t2))))
756 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
760 raise (UnificationFailure
763 "Can't unify %s with %s because they are not convertible"
764 (CicMetaSubst.ppterm subst t1)
765 (CicMetaSubst.ppterm subst t2))))
767 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
768 exp_named_subst1 exp_named_subst2 ugraph
772 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
774 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
775 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
777 Invalid_argument _ ->
782 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
785 raise (UnificationFailure (lazy (sprintf
786 "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))))
788 (* A substitution is a (int * Cic.term) list that associates a *)
789 (* metavariable i with its body. *)
790 (* metasenv is of type Cic.metasenv *)
791 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
792 (* a new substitution which is already unwinded and ready to be applied and *)
793 (* a new metasenv in which some hypothesis in the contexts of the *)
794 (* metavariables may have been restricted. *)
795 let fo_unif metasenv context t1 t2 ugraph =
796 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
798 let enrich_msg msg subst context metasenv t1 t2 ugraph =
801 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"
802 (CicMetaSubst.ppterm subst t1)
804 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
807 | UnificationFailure s
809 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
810 (CicMetaSubst.ppterm subst t2)
812 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
815 | UnificationFailure s
817 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
818 (CicMetaSubst.ppcontext subst context)
819 (CicMetaSubst.ppmetasenv subst metasenv)
820 (CicMetaSubst.ppsubst subst) (Lazy.force msg)
822 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
823 (CicMetaSubst.ppterm_in_context subst t1 context)
825 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
826 CicMetaSubst.ppterm_in_context subst ty_t1 context
828 | UnificationFailure s
830 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
831 (CicMetaSubst.ppterm_in_context subst t2 context)
833 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
834 CicMetaSubst.ppterm_in_context subst ty_t2 context
836 | UnificationFailure s
838 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
839 (CicMetaSubst.ppcontext subst context)
840 (CicMetaSubst.ppmetasenv subst metasenv)
844 let fo_unif_subst subst context metasenv t1 t2 ugraph =
846 fo_unif_subst false subst context metasenv t1 t2 ugraph
848 | AssertFailure msg ->
849 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
850 | UnificationFailure msg ->
851 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))