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 type_of_aux' metasenv subst context term ugraph =
45 CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph
47 CicTypeChecker.TypeCheckerFailure msg ->
51 "Kernel Type checking error:
52 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
53 (CicMetaSubst.ppterm subst term)
54 (CicMetaSubst.ppterm [] term)
55 (CicMetaSubst.ppcontext subst context)
56 (CicMetaSubst.ppmetasenv subst metasenv)
57 (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
58 raise (AssertFailure msg)
59 | CicTypeChecker.AssertFailure msg ->
62 "Kernel Type checking assertion failure:
63 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
64 (CicMetaSubst.ppterm subst term)
65 (CicMetaSubst.ppterm [] term)
66 (CicMetaSubst.ppcontext subst context)
67 (CicMetaSubst.ppmetasenv subst metasenv)
68 (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
69 raise (AssertFailure msg)
70 in profiler_toa.HExtlib.profile foo ()
74 List.exists (function Cic.Meta _ -> true | _ -> false) l
76 let rec deref subst t =
77 let snd (_,a,_) = a in
82 (CicSubstitution.subst_meta
83 l (snd (CicUtil.lookup_subst n subst)))
85 CicUtil.Subst_not_found _ -> t)
86 | Cic.Appl(Cic.Meta(n,l)::args) ->
87 (match deref subst (Cic.Meta(n,l)) with
88 | Cic.Lambda _ as t ->
89 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
90 | r -> Cic.Appl(r::args))
91 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
92 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
97 let foo () = deref subst t
98 in profiler_deref.HExtlib.profile foo ()
100 exception WrongShape;;
101 let eta_reduce after_beta_expansion after_beta_expansion_body
102 before_beta_expansion
105 match before_beta_expansion,after_beta_expansion_body with
106 Cic.Appl l, Cic.Appl l' ->
107 let rec all_but_last check_last =
111 | [_] -> if check_last then raise WrongShape else []
112 | he::tl -> he::(all_but_last check_last tl)
114 let all_but_last check_last l =
115 match all_but_last check_last l with
120 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
121 let all_but_last = all_but_last false l in
122 (* here we should test alpha-equivalence; however we know by
123 construction that here alpha_equivalence is equivalent to = *)
124 if t = all_but_last then
128 | _,_ -> after_beta_expansion
130 WrongShape -> after_beta_expansion
132 let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
133 let module S = CicSubstitution in
134 let module C = Cic in
136 let rec aux metasenv subst n context t' ugraph =
139 let subst,metasenv,ugraph1 =
140 fo_unif_subst test_equality_only subst context metasenv
141 (CicSubstitution.lift n arg) t' ugraph
144 subst,metasenv,C.Rel (1 + n),ugraph1
147 | UnificationFailure _ ->
149 | C.Rel m -> subst,metasenv,
150 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
151 | C.Var (uri,exp_named_subst) ->
152 let subst,metasenv,exp_named_subst',ugraph1 =
153 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
155 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
157 (* andrea: in general, beta_expand can create badly typed
158 terms. This happens quite seldom in practice, UNLESS we
159 iterate on the local context. For this reason, we renounce
160 to iterate and just lift *)
164 Some t -> Some (CicSubstitution.lift 1 t)
166 subst, metasenv, C.Meta (i,l), ugraph
168 | C.Implicit _ as t -> subst,metasenv,t,ugraph
170 let subst,metasenv,te',ugraph1 =
171 aux metasenv subst n context te ugraph in
172 let subst,metasenv,ty',ugraph2 =
173 aux metasenv subst n context ty ugraph1 in
174 (* TASSI: sure this is in serial? *)
175 subst,metasenv,(C.Cast (te', ty')),ugraph2
177 let subst,metasenv,s',ugraph1 =
178 aux metasenv subst n context s ugraph in
179 let subst,metasenv,t',ugraph2 =
180 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
183 (* TASSI: sure this is in serial? *)
184 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
185 | C.Lambda (nn,s,t) ->
186 let subst,metasenv,s',ugraph1 =
187 aux metasenv subst n context s ugraph in
188 let subst,metasenv,t',ugraph2 =
189 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
191 (* TASSI: sure this is in serial? *)
192 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
193 | C.LetIn (nn,s,t) ->
194 let subst,metasenv,s',ugraph1 =
195 aux metasenv subst n context s ugraph in
196 let subst,metasenv,t',ugraph2 =
197 aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
200 (* TASSI: sure this is in serial? *)
201 subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
203 let subst,metasenv,revl',ugraph1 =
205 (fun (subst,metasenv,appl,ugraph) t ->
206 let subst,metasenv,t',ugraph1 =
207 aux metasenv subst n context t ugraph in
208 subst,metasenv,(t'::appl),ugraph1
209 ) (subst,metasenv,[],ugraph) l
211 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
212 | C.Const (uri,exp_named_subst) ->
213 let subst,metasenv,exp_named_subst',ugraph1 =
214 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
216 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
217 | C.MutInd (uri,i,exp_named_subst) ->
218 let subst,metasenv,exp_named_subst',ugraph1 =
219 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
221 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
222 | C.MutConstruct (uri,i,j,exp_named_subst) ->
223 let subst,metasenv,exp_named_subst',ugraph1 =
224 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
226 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
227 | C.MutCase (sp,i,outt,t,pl) ->
228 let subst,metasenv,outt',ugraph1 =
229 aux metasenv subst n context outt ugraph in
230 let subst,metasenv,t',ugraph2 =
231 aux metasenv subst n context t ugraph1 in
232 let subst,metasenv,revpl',ugraph3 =
234 (fun (subst,metasenv,pl,ugraph) t ->
235 let subst,metasenv,t',ugraph1 =
236 aux metasenv subst n context t ugraph in
237 subst,metasenv,(t'::pl),ugraph1
238 ) (subst,metasenv,[],ugraph2) pl
240 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
241 (* TASSI: not sure this is serial *)
243 (*CSC: not implemented
244 let tylen = List.length fl in
247 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
250 C.Fix (i, substitutedfl)
252 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
254 (*CSC: not implemented
255 let tylen = List.length fl in
258 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
261 C.CoFix (i, substitutedfl)
264 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
266 and aux_exp_named_subst metasenv subst n context ens ugraph =
268 (fun (uri,t) (subst,metasenv,l,ugraph) ->
269 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
270 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
272 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
274 FreshNamesGenerator.mk_fresh_name ~subst
275 metasenv context (Cic.Name "Hbeta") ~typ:argty
277 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
278 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
279 subst, metasenv, t'', ugraph2
280 in profiler_beta_expand.HExtlib.profile foo ()
283 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
284 let subst,metasenv,hd,ugraph =
286 (fun arg (subst,metasenv,t,ugraph) ->
287 let subst,metasenv,t,ugraph1 =
288 beta_expand test_equality_only
289 metasenv subst context t arg ugraph
291 subst,metasenv,t,ugraph1
292 ) args (subst,metasenv,t,ugraph)
294 subst,metasenv,hd,ugraph
297 (* NUOVA UNIFICAZIONE *)
298 (* A substitution is a (int * Cic.term) list that associates a
299 metavariable i with its body.
300 A metaenv is a (int * Cic.term) list that associate a metavariable
302 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
303 a new substitution which is _NOT_ unwinded. It must be unwinded before
306 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
307 let module C = Cic in
308 let module R = CicReduction in
309 let module S = CicSubstitution in
310 let t1 = deref subst t1 in
311 let t2 = deref subst t2 in
314 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
315 in profiler_are_convertible.HExtlib.profile foo ()
318 subst, metasenv, ugraph
321 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
322 let _,subst,metasenv,ugraph1 =
325 (fun (j,subst,metasenv,ugraph) t1 t2 ->
328 | _,None -> j+1,subst,metasenv,ugraph
329 | Some t1', Some t2' ->
330 (* First possibility: restriction *)
331 (* Second possibility: unification *)
332 (* Third possibility: convertibility *)
335 ~subst ~metasenv context t1' t2' ugraph
338 j+1,subst,metasenv, ugraph1
341 let subst,metasenv,ugraph2 =
344 subst context metasenv t1' t2' ugraph
346 j+1,subst,metasenv,ugraph2
349 | UnificationFailure _ ->
350 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
351 let metasenv, subst =
352 CicMetaSubst.restrict
353 subst [(n,j)] metasenv in
354 j+1,subst,metasenv,ugraph1)
355 ) (1,subst,metasenv,ugraph) ln lm
359 (UnificationFailure (lazy "1"))
362 "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."
363 (CicMetaSubst.ppterm subst t1)
364 (CicMetaSubst.ppterm subst t2))) *)
365 | Invalid_argument _ ->
367 (UnificationFailure (lazy "2")))
370 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
371 (CicMetaSubst.ppterm subst t1)
372 (CicMetaSubst.ppterm subst t2)))) *)
373 in subst,metasenv,ugraph1
374 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
375 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
377 | (t, C.Meta (n,l)) ->
380 C.Meta (n,_), C.Meta (m,_) when n < m -> false
381 | _, C.Meta _ -> false
384 let lower = fun x y -> if swap then y else x in
385 let upper = fun x y -> if swap then x else y in
386 let fo_unif_subst_ordered
387 test_equality_only subst context metasenv m1 m2 ugraph =
388 fo_unif_subst test_equality_only subst context metasenv
389 (lower m1 m2) (upper m1 m2) ugraph
392 let subst,metasenv,ugraph1 =
393 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
396 type_of_aux' metasenv subst context t ugraph
400 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
402 UnificationFailure _ as e -> raise e
403 | Uncertain msg -> raise (UnificationFailure msg)
405 debug_print (lazy "siamo allo huge hack");
406 (* TODO huge hack!!!!
407 * we keep on unifying/refining in the hope that
408 * the problem will be eventually solved.
409 * In the meantime we're breaking a big invariant:
410 * the terms that we are unifying are no longer well
411 * typed in the current context (in the worst case
412 * we could even diverge) *)
413 (subst, metasenv,ugraph)) in
414 let t',metasenv,subst =
416 CicMetaSubst.delift n subst context metasenv l t
418 (CicMetaSubst.MetaSubstFailure msg)->
419 raise (UnificationFailure msg)
420 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
424 C.Sort (C.Type u) when not test_equality_only ->
425 let u' = CicUniv.fresh () in
426 let s = C.Sort (C.Type u') in
428 CicUniv.add_ge (upper u u') (lower u u') ugraph1
433 (* Unifying the types may have already instantiated n. Let's check *)
435 let (_, oldt,_) = CicUtil.lookup_subst n subst in
436 let lifted_oldt = S.subst_meta l oldt in
437 fo_unif_subst_ordered
438 test_equality_only subst context metasenv t lifted_oldt ugraph2
440 CicUtil.Subst_not_found _ ->
441 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
442 let subst = (n, (context, t'',ty)) :: subst in
444 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
445 subst, metasenv, ugraph2
447 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
448 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
449 if UriManager.eq uri1 uri2 then
450 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
451 exp_named_subst1 exp_named_subst2 ugraph
453 raise (UnificationFailure (lazy
455 "Can't unify %s with %s due to different constants"
456 (CicMetaSubst.ppterm subst t1)
457 (CicMetaSubst.ppterm subst t2))))
458 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
459 if UriManager.eq uri1 uri2 && i1 = i2 then
460 fo_unif_subst_exp_named_subst
462 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
464 raise (UnificationFailure (lazy "4"))
466 "Can't unify %s with %s due to different inductive principles"
467 (CicMetaSubst.ppterm subst t1)
468 (CicMetaSubst.ppterm subst t2))) *)
469 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
470 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
471 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
472 fo_unif_subst_exp_named_subst
474 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
476 raise (UnificationFailure (lazy "5"))
478 "Can't unify %s with %s due to different inductive constructors"
479 (CicMetaSubst.ppterm subst t1)
480 (CicMetaSubst.ppterm subst t2))) *)
481 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
482 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
483 subst context metasenv te t2 ugraph
484 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
485 subst context metasenv t1 te ugraph
486 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
487 let subst',metasenv',ugraph1 =
488 fo_unif_subst true subst context metasenv s1 s2 ugraph
490 fo_unif_subst test_equality_only
491 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
492 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
493 let subst',metasenv',ugraph1 =
494 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
496 fo_unif_subst test_equality_only
497 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
498 | (C.LetIn (_,s1,t1), t2)
499 | (t2, C.LetIn (_,s1,t1)) ->
501 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
502 | (C.Appl l1, C.Appl l2) ->
503 (* andrea: this case should be probably rewritten in the
506 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
509 (fun (subst,metasenv,ugraph) t1 t2 ->
511 test_equality_only subst context metasenv t1 t2 ugraph)
512 (subst,metasenv,ugraph) l1 l2
513 with (Invalid_argument msg) ->
514 raise (UnificationFailure (lazy msg)))
515 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
516 (* we verify that none of the args is a Meta,
517 since beta expanding with respoect to a metavariable
521 let (_,t,_) = CicUtil.lookup_subst i subst in
522 let lifted = S.subst_meta l t in
523 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
526 subst context metasenv reduced t2 ugraph
527 with CicUtil.Subst_not_found _ -> *)
528 let subst,metasenv,beta_expanded,ugraph1 =
530 test_equality_only metasenv subst context t2 args ugraph
532 fo_unif_subst test_equality_only subst context metasenv
533 (C.Meta (i,l)) beta_expanded ugraph1
534 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
536 let (_,t,_) = CicUtil.lookup_subst i subst in
537 let lifted = S.subst_meta l t in
538 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
541 subst context metasenv t1 reduced ugraph
542 with CicUtil.Subst_not_found _ -> *)
543 let subst,metasenv,beta_expanded,ugraph1 =
546 metasenv subst context t1 args ugraph
548 fo_unif_subst test_equality_only subst context metasenv
549 (C.Meta (i,l)) beta_expanded ugraph1
551 let lr1 = List.rev l1 in
552 let lr2 = List.rev l2 in
554 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
557 | _,[] -> assert false
560 test_equality_only subst context metasenv h1 h2 ugraph
563 fo_unif_subst test_equality_only subst context metasenv
564 h (C.Appl (List.rev l)) ugraph
565 | ((h1::l1),(h2::l2)) ->
566 let subst', metasenv',ugraph1 =
569 subst context metasenv h1 h2 ugraph
572 test_equality_only subst' metasenv' (l1,l2) ugraph1
575 test_equality_only subst metasenv (lr1, lr2) ugraph)
576 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
577 let subst', metasenv',ugraph1 =
578 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
580 let subst'',metasenv'',ugraph2 =
581 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
585 (fun (subst,metasenv,ugraph) t1 t2 ->
587 test_equality_only subst context metasenv t1 t2 ugraph
588 ) (subst'',metasenv'',ugraph2) pl1 pl2
590 Invalid_argument _ ->
591 raise (UnificationFailure (lazy "6.1")))
593 "Error trying to unify %s with %s: the number of branches is not the same."
594 (CicMetaSubst.ppterm subst t1)
595 (CicMetaSubst.ppterm subst t2)))) *)
596 | (C.Rel _, _) | (_, C.Rel _) ->
598 subst, metasenv,ugraph
600 raise (UnificationFailure (lazy
602 "Can't unify %s with %s because they are not convertible"
603 (CicMetaSubst.ppterm subst t1)
604 (CicMetaSubst.ppterm subst t2))))
605 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
606 let subst,metasenv,beta_expanded,ugraph1 =
608 test_equality_only metasenv subst context t2 args ugraph
610 fo_unif_subst test_equality_only subst context metasenv
611 (C.Meta (i,l)) beta_expanded ugraph1
612 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
613 let subst,metasenv,beta_expanded,ugraph1 =
615 test_equality_only metasenv subst context t1 args ugraph
617 fo_unif_subst test_equality_only subst context metasenv
618 beta_expanded (C.Meta (i,l)) ugraph1
619 | (C.Sort _ ,_) | (_, C.Sort _)
620 | (C.Const _, _) | (_, C.Const _)
621 | (C.MutInd _, _) | (_, C.MutInd _)
622 | (C.MutConstruct _, _) | (_, C.MutConstruct _)
623 | (C.Fix _, _) | (_, C.Fix _)
624 | (C.CoFix _, _) | (_, C.CoFix _) ->
626 subst, metasenv, ugraph
629 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
632 subst, metasenv, ugraph1
635 (UnificationFailure (lazy (sprintf
636 "Can't unify %s with %s because they are not convertible"
637 (CicMetaSubst.ppterm subst t1)
638 (CicMetaSubst.ppterm subst t2))))
640 let t2' = R.whd ~subst context t2 in
643 fo_unif_subst test_equality_only
644 subst context metasenv t1 t2' ugraph
645 | _ -> raise (UnificationFailure (lazy "8")))
647 let t1' = R.whd ~subst context t1 in
650 fo_unif_subst test_equality_only
651 subst context metasenv t1' t2 ugraph
652 | _ -> (* raise (UnificationFailure "9")) *)
654 (UnificationFailure (lazy (sprintf
655 "Can't unify %s with %s because they are not convertible"
656 (CicMetaSubst.ppterm subst t1)
657 (CicMetaSubst.ppterm subst t2)))))
659 raise (UnificationFailure (lazy "10"))
661 "Can't unify %s with %s because they are not convertible"
662 (CicMetaSubst.ppterm subst t1)
663 (CicMetaSubst.ppterm subst t2))) *)
665 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
666 exp_named_subst1 exp_named_subst2 ugraph
670 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
672 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
673 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
675 Invalid_argument _ ->
680 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
683 raise (UnificationFailure (lazy (sprintf
684 "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))))
686 (* A substitution is a (int * Cic.term) list that associates a *)
687 (* metavariable i with its body. *)
688 (* metasenv is of type Cic.metasenv *)
689 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
690 (* a new substitution which is already unwinded and ready to be applied and *)
691 (* a new metasenv in which some hypothesis in the contexts of the *)
692 (* metavariables may have been restricted. *)
693 let fo_unif metasenv context t1 t2 ugraph =
694 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
696 let enrich_msg msg subst context metasenv t1 t2 ugraph =
699 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"
700 (CicMetaSubst.ppterm subst t1)
702 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
705 | UnificationFailure s
707 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
708 (CicMetaSubst.ppterm subst t2)
710 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
713 | UnificationFailure s
715 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
716 (CicMetaSubst.ppcontext subst context)
717 (CicMetaSubst.ppmetasenv subst metasenv)
718 (CicMetaSubst.ppsubst subst) (Lazy.force msg)
720 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
721 (CicMetaSubst.ppterm_in_context subst t1 context)
723 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
724 CicMetaSubst.ppterm_in_context subst ty_t1 context
726 | UnificationFailure s
728 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
729 (CicMetaSubst.ppterm_in_context subst t2 context)
731 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
732 CicMetaSubst.ppterm_in_context subst ty_t2 context
734 | UnificationFailure s
736 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
737 (CicMetaSubst.ppcontext subst context)
738 (CicMetaSubst.ppmetasenv subst metasenv)
742 let fo_unif_subst subst context metasenv t1 t2 ugraph =
744 fo_unif_subst false subst context metasenv t1 t2 ugraph
746 | AssertFailure msg ->
747 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
748 | UnificationFailure msg ->
749 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))