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/.
28 exception UnificationFailure of string Lazy.t;;
29 exception Uncertain of string Lazy.t;;
30 exception AssertFailure of string Lazy.t;;
33 let debug_print = fun _ -> ()
35 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
36 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
37 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
38 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
40 let type_of_aux' metasenv subst context term ugraph =
43 CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph
45 CicTypeChecker.TypeCheckerFailure msg ->
49 "Kernel Type checking error:
50 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
51 (CicMetaSubst.ppterm subst term)
52 (CicMetaSubst.ppterm [] term)
53 (CicMetaSubst.ppcontext subst context)
54 (CicMetaSubst.ppmetasenv subst metasenv)
55 (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
56 raise (AssertFailure msg)
57 | CicTypeChecker.AssertFailure msg ->
60 "Kernel Type checking assertion failure:
61 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
62 (CicMetaSubst.ppterm subst term)
63 (CicMetaSubst.ppterm [] term)
64 (CicMetaSubst.ppcontext subst context)
65 (CicMetaSubst.ppmetasenv subst metasenv)
66 (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
67 raise (AssertFailure msg)
68 in profiler_toa.HExtlib.profile foo ()
72 List.exists (function Cic.Meta _ -> true | _ -> false) l
74 let rec deref subst t =
75 let snd (_,a,_) = a in
80 (CicSubstitution.subst_meta
81 l (snd (CicUtil.lookup_subst n subst)))
83 CicUtil.Subst_not_found _ -> t)
84 | Cic.Appl(Cic.Meta(n,l)::args) ->
85 (match deref subst (Cic.Meta(n,l)) with
86 | Cic.Lambda _ as t ->
87 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
88 | r -> Cic.Appl(r::args))
89 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
90 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
95 let foo () = deref subst t
96 in profiler_deref.HExtlib.profile foo ()
98 exception WrongShape;;
99 let eta_reduce after_beta_expansion after_beta_expansion_body
100 before_beta_expansion
103 match before_beta_expansion,after_beta_expansion_body with
104 Cic.Appl l, Cic.Appl l' ->
105 let rec all_but_last check_last =
109 | [_] -> if check_last then raise WrongShape else []
110 | he::tl -> he::(all_but_last check_last tl)
112 let all_but_last check_last l =
113 match all_but_last check_last l with
118 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
119 let all_but_last = all_but_last false l in
120 (* here we should test alpha-equivalence; however we know by
121 construction that here alpha_equivalence is equivalent to = *)
122 if t = all_but_last then
126 | _,_ -> after_beta_expansion
128 WrongShape -> after_beta_expansion
130 let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
131 let module S = CicSubstitution in
132 let module C = Cic in
134 let rec aux metasenv subst n context t' ugraph =
137 let subst,metasenv,ugraph1 =
138 fo_unif_subst test_equality_only subst context metasenv
139 (CicSubstitution.lift n arg) t' ugraph
142 subst,metasenv,C.Rel (1 + n),ugraph1
145 | UnificationFailure _ ->
147 | C.Rel m -> subst,metasenv,
148 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
149 | C.Var (uri,exp_named_subst) ->
150 let subst,metasenv,exp_named_subst',ugraph1 =
151 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
153 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
155 (* andrea: in general, beta_expand can create badly typed
156 terms. This happens quite seldom in practice, UNLESS we
157 iterate on the local context. For this reason, we renounce
158 to iterate and just lift *)
162 Some t -> Some (CicSubstitution.lift 1 t)
164 subst, metasenv, C.Meta (i,l), ugraph
166 | C.Implicit _ as t -> subst,metasenv,t,ugraph
168 let subst,metasenv,te',ugraph1 =
169 aux metasenv subst n context te ugraph in
170 let subst,metasenv,ty',ugraph2 =
171 aux metasenv subst n context ty ugraph1 in
172 (* TASSI: sure this is in serial? *)
173 subst,metasenv,(C.Cast (te', ty')),ugraph2
175 let subst,metasenv,s',ugraph1 =
176 aux metasenv subst n context s ugraph in
177 let subst,metasenv,t',ugraph2 =
178 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
181 (* TASSI: sure this is in serial? *)
182 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
183 | C.Lambda (nn,s,t) ->
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 ugraph1
189 (* TASSI: sure this is in serial? *)
190 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
191 | C.LetIn (nn,s,t) ->
192 let subst,metasenv,s',ugraph1 =
193 aux metasenv subst n context s ugraph in
194 let subst,metasenv,t',ugraph2 =
195 aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
198 (* TASSI: sure this is in serial? *)
199 subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
201 let subst,metasenv,revl',ugraph1 =
203 (fun (subst,metasenv,appl,ugraph) t ->
204 let subst,metasenv,t',ugraph1 =
205 aux metasenv subst n context t ugraph in
206 subst,metasenv,(t'::appl),ugraph1
207 ) (subst,metasenv,[],ugraph) l
209 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
210 | C.Const (uri,exp_named_subst) ->
211 let subst,metasenv,exp_named_subst',ugraph1 =
212 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
214 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
215 | C.MutInd (uri,i,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.MutInd (uri,i,exp_named_subst')),ugraph1
220 | C.MutConstruct (uri,i,j,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.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
225 | C.MutCase (sp,i,outt,t,pl) ->
226 let subst,metasenv,outt',ugraph1 =
227 aux metasenv subst n context outt ugraph in
228 let subst,metasenv,t',ugraph2 =
229 aux metasenv subst n context t ugraph1 in
230 let subst,metasenv,revpl',ugraph3 =
232 (fun (subst,metasenv,pl,ugraph) t ->
233 let subst,metasenv,t',ugraph1 =
234 aux metasenv subst n context t ugraph in
235 subst,metasenv,(t'::pl),ugraph1
236 ) (subst,metasenv,[],ugraph2) pl
238 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
239 (* TASSI: not sure this is serial *)
241 (*CSC: not implemented
242 let tylen = List.length fl in
245 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
248 C.Fix (i, substitutedfl)
250 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
252 (*CSC: not implemented
253 let tylen = List.length fl in
256 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
259 C.CoFix (i, substitutedfl)
262 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
264 and aux_exp_named_subst metasenv subst n context ens ugraph =
266 (fun (uri,t) (subst,metasenv,l,ugraph) ->
267 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
268 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
270 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
272 FreshNamesGenerator.mk_fresh_name ~subst
273 metasenv context (Cic.Name "Hbeta") ~typ:argty
275 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
276 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
277 subst, metasenv, t'', ugraph2
278 in profiler_beta_expand.HExtlib.profile foo ()
281 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
282 let subst,metasenv,hd,ugraph =
284 (fun arg (subst,metasenv,t,ugraph) ->
285 let subst,metasenv,t,ugraph1 =
286 beta_expand test_equality_only
287 metasenv subst context t arg ugraph
289 subst,metasenv,t,ugraph1
290 ) args (subst,metasenv,t,ugraph)
292 subst,metasenv,hd,ugraph
295 (* NUOVA UNIFICAZIONE *)
296 (* A substitution is a (int * Cic.term) list that associates a
297 metavariable i with its body.
298 A metaenv is a (int * Cic.term) list that associate a metavariable
300 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
301 a new substitution which is _NOT_ unwinded. It must be unwinded before
304 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
305 let module C = Cic in
306 let module R = CicReduction in
307 let module S = CicSubstitution in
308 let t1 = deref subst t1 in
309 let t2 = deref subst t2 in
312 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
313 in profiler_are_convertible.HExtlib.profile foo ()
316 subst, metasenv, ugraph
319 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
320 let _,subst,metasenv,ugraph1 =
323 (fun (j,subst,metasenv,ugraph) t1 t2 ->
326 | _,None -> j+1,subst,metasenv,ugraph
327 | Some t1', Some t2' ->
328 (* First possibility: restriction *)
329 (* Second possibility: unification *)
330 (* Third possibility: convertibility *)
333 ~subst ~metasenv context t1' t2' ugraph
336 j+1,subst,metasenv, ugraph1
339 let subst,metasenv,ugraph2 =
342 subst context metasenv t1' t2' ugraph
344 j+1,subst,metasenv,ugraph2
347 | UnificationFailure _ ->
348 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
349 let metasenv, subst =
350 CicMetaSubst.restrict
351 subst [(n,j)] metasenv in
352 j+1,subst,metasenv,ugraph1)
353 ) (1,subst,metasenv,ugraph) ln lm
357 (UnificationFailure (lazy "1"))
360 "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."
361 (CicMetaSubst.ppterm subst t1)
362 (CicMetaSubst.ppterm subst t2))) *)
363 | Invalid_argument _ ->
365 (UnificationFailure (lazy "2")))
368 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
369 (CicMetaSubst.ppterm subst t1)
370 (CicMetaSubst.ppterm subst t2)))) *)
371 in subst,metasenv,ugraph1
372 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
373 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
375 | (t, C.Meta (n,l)) ->
378 C.Meta (n,_), C.Meta (m,_) when n < m -> false
379 | _, C.Meta _ -> false
382 let lower = fun x y -> if swap then y else x in
383 let upper = fun x y -> if swap then x else y in
384 let fo_unif_subst_ordered
385 test_equality_only subst context metasenv m1 m2 ugraph =
386 fo_unif_subst test_equality_only subst context metasenv
387 (lower m1 m2) (upper m1 m2) ugraph
390 let subst,metasenv,ugraph1 =
391 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
394 type_of_aux' metasenv subst context t ugraph
398 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
400 UnificationFailure _ as e -> raise e
401 | Uncertain msg -> raise (UnificationFailure msg)
403 debug_print (lazy "siamo allo huge hack");
404 (* TODO huge hack!!!!
405 * we keep on unifying/refining in the hope that
406 * the problem will be eventually solved.
407 * In the meantime we're breaking a big invariant:
408 * the terms that we are unifying are no longer well
409 * typed in the current context (in the worst case
410 * we could even diverge) *)
411 (subst, metasenv,ugraph)) in
412 let t',metasenv,subst =
414 CicMetaSubst.delift n subst context metasenv l t
416 (CicMetaSubst.MetaSubstFailure msg)->
417 raise (UnificationFailure msg)
418 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
422 C.Sort (C.Type u) when not test_equality_only ->
423 let u' = CicUniv.fresh () in
424 let s = C.Sort (C.Type u') in
426 CicUniv.add_ge (upper u u') (lower u u') ugraph1
431 (* Unifying the types may have already instantiated n. Let's check *)
433 let (_, oldt,_) = CicUtil.lookup_subst n subst in
434 let lifted_oldt = S.subst_meta l oldt in
435 fo_unif_subst_ordered
436 test_equality_only subst context metasenv t lifted_oldt ugraph2
438 CicUtil.Subst_not_found _ ->
439 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
440 let subst = (n, (context, t'',ty)) :: subst in
442 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
443 subst, metasenv, ugraph2
445 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
446 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
447 if UriManager.eq uri1 uri2 then
448 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
449 exp_named_subst1 exp_named_subst2 ugraph
451 raise (UnificationFailure (lazy
453 "Can't unify %s with %s due to different constants"
454 (CicMetaSubst.ppterm subst t1)
455 (CicMetaSubst.ppterm subst t2))))
456 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
457 if UriManager.eq uri1 uri2 && i1 = i2 then
458 fo_unif_subst_exp_named_subst
460 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
462 raise (UnificationFailure (lazy "4"))
464 "Can't unify %s with %s due to different inductive principles"
465 (CicMetaSubst.ppterm subst t1)
466 (CicMetaSubst.ppterm subst t2))) *)
467 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
468 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
469 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
470 fo_unif_subst_exp_named_subst
472 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
474 raise (UnificationFailure (lazy "5"))
476 "Can't unify %s with %s due to different inductive constructors"
477 (CicMetaSubst.ppterm subst t1)
478 (CicMetaSubst.ppterm subst t2))) *)
479 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
480 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
481 subst context metasenv te t2 ugraph
482 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
483 subst context metasenv t1 te ugraph
484 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
485 let subst',metasenv',ugraph1 =
486 fo_unif_subst true subst context metasenv s1 s2 ugraph
488 fo_unif_subst test_equality_only
489 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
490 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
491 let subst',metasenv',ugraph1 =
492 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
494 fo_unif_subst test_equality_only
495 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
496 | (C.LetIn (_,s1,t1), t2)
497 | (t2, C.LetIn (_,s1,t1)) ->
499 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
500 | (C.Appl l1, C.Appl l2) ->
501 (* andrea: this case should be probably rewritten in the
504 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
507 (fun (subst,metasenv,ugraph) t1 t2 ->
509 test_equality_only subst context metasenv t1 t2 ugraph)
510 (subst,metasenv,ugraph) l1 l2
511 with (Invalid_argument msg) ->
512 raise (UnificationFailure (lazy msg)))
513 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
514 (* we verify that none of the args is a Meta,
515 since beta expanding with respoect to a metavariable
519 let (_,t,_) = CicUtil.lookup_subst i subst in
520 let lifted = S.subst_meta l t in
521 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
524 subst context metasenv reduced t2 ugraph
525 with CicUtil.Subst_not_found _ -> *)
526 let subst,metasenv,beta_expanded,ugraph1 =
528 test_equality_only metasenv subst context t2 args ugraph
530 fo_unif_subst test_equality_only subst context metasenv
531 (C.Meta (i,l)) beta_expanded ugraph1
532 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
534 let (_,t,_) = CicUtil.lookup_subst i subst in
535 let lifted = S.subst_meta l t in
536 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
539 subst context metasenv t1 reduced ugraph
540 with CicUtil.Subst_not_found _ -> *)
541 let subst,metasenv,beta_expanded,ugraph1 =
544 metasenv subst context t1 args ugraph
546 fo_unif_subst test_equality_only subst context metasenv
547 (C.Meta (i,l)) beta_expanded ugraph1
549 let lr1 = List.rev l1 in
550 let lr2 = List.rev l2 in
552 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
555 | _,[] -> assert false
558 test_equality_only subst context metasenv h1 h2 ugraph
561 fo_unif_subst test_equality_only subst context metasenv
562 h (C.Appl (List.rev l)) ugraph
563 | ((h1::l1),(h2::l2)) ->
564 let subst', metasenv',ugraph1 =
567 subst context metasenv h1 h2 ugraph
570 test_equality_only subst' metasenv' (l1,l2) ugraph1
573 test_equality_only subst metasenv (lr1, lr2) ugraph)
574 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
575 let subst', metasenv',ugraph1 =
576 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
578 let subst'',metasenv'',ugraph2 =
579 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
583 (fun (subst,metasenv,ugraph) t1 t2 ->
585 test_equality_only subst context metasenv t1 t2 ugraph
586 ) (subst'',metasenv'',ugraph2) pl1 pl2
588 Invalid_argument _ ->
589 raise (UnificationFailure (lazy "6.1")))
591 "Error trying to unify %s with %s: the number of branches is not the same."
592 (CicMetaSubst.ppterm subst t1)
593 (CicMetaSubst.ppterm subst t2)))) *)
594 | (C.Rel _, _) | (_, C.Rel _) ->
596 subst, metasenv,ugraph
598 raise (UnificationFailure (lazy
600 "Can't unify %s with %s because they are not convertible"
601 (CicMetaSubst.ppterm subst t1)
602 (CicMetaSubst.ppterm subst t2))))
603 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
604 let subst,metasenv,beta_expanded,ugraph1 =
606 test_equality_only metasenv subst context t2 args ugraph
608 fo_unif_subst test_equality_only subst context metasenv
609 (C.Meta (i,l)) beta_expanded ugraph1
610 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
611 let subst,metasenv,beta_expanded,ugraph1 =
613 test_equality_only metasenv subst context t1 args ugraph
615 fo_unif_subst test_equality_only subst context metasenv
616 beta_expanded (C.Meta (i,l)) ugraph1
617 | (C.Sort _ ,_) | (_, C.Sort _)
618 | (C.Const _, _) | (_, C.Const _)
619 | (C.MutInd _, _) | (_, C.MutInd _)
620 | (C.MutConstruct _, _) | (_, C.MutConstruct _)
621 | (C.Fix _, _) | (_, C.Fix _)
622 | (C.CoFix _, _) | (_, C.CoFix _) ->
624 subst, metasenv, ugraph
627 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
630 subst, metasenv, ugraph1
633 (UnificationFailure (lazy (sprintf
634 "Can't unify %s with %s because they are not convertible"
635 (CicMetaSubst.ppterm subst t1)
636 (CicMetaSubst.ppterm subst t2))))
638 let t2' = R.whd ~subst context t2 in
641 fo_unif_subst test_equality_only
642 subst context metasenv t1 t2' ugraph
643 | _ -> raise (UnificationFailure (lazy "8")))
645 let t1' = R.whd ~subst context t1 in
648 fo_unif_subst test_equality_only
649 subst context metasenv t1' t2 ugraph
650 | _ -> (* raise (UnificationFailure "9")) *)
652 (UnificationFailure (lazy (sprintf
653 "Can't unify %s with %s because they are not convertible"
654 (CicMetaSubst.ppterm subst t1)
655 (CicMetaSubst.ppterm subst t2)))))
657 raise (UnificationFailure (lazy "10"))
659 "Can't unify %s with %s because they are not convertible"
660 (CicMetaSubst.ppterm subst t1)
661 (CicMetaSubst.ppterm subst t2))) *)
663 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
664 exp_named_subst1 exp_named_subst2 ugraph
668 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
670 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
671 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
673 Invalid_argument _ ->
678 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
681 raise (UnificationFailure (lazy (sprintf
682 "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))))
684 (* A substitution is a (int * Cic.term) list that associates a *)
685 (* metavariable i with its body. *)
686 (* metasenv is of type Cic.metasenv *)
687 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
688 (* a new substitution which is already unwinded and ready to be applied and *)
689 (* a new metasenv in which some hypothesis in the contexts of the *)
690 (* metavariables may have been restricted. *)
691 let fo_unif metasenv context t1 t2 ugraph =
692 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
694 let enrich_msg msg subst context metasenv t1 t2 ugraph =
697 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"
698 (CicMetaSubst.ppterm subst t1)
700 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
703 | UnificationFailure s
705 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
706 (CicMetaSubst.ppterm subst t2)
708 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
711 | UnificationFailure s
713 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
714 (CicMetaSubst.ppcontext subst context)
715 (CicMetaSubst.ppmetasenv subst metasenv)
716 (CicMetaSubst.ppsubst subst) (Lazy.force msg)
718 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
719 (CicMetaSubst.ppterm_in_context subst t1 context)
721 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
722 CicMetaSubst.ppterm_in_context subst ty_t1 context
724 | UnificationFailure s
726 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
727 (CicMetaSubst.ppterm_in_context subst t2 context)
729 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
730 CicMetaSubst.ppterm_in_context subst ty_t2 context
732 | UnificationFailure s
734 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
735 (CicMetaSubst.ppcontext subst context)
736 (CicMetaSubst.ppmetasenv subst metasenv)
740 let fo_unif_subst subst context metasenv t1 t2 ugraph =
742 fo_unif_subst false subst context metasenv t1 t2 ugraph
744 | AssertFailure msg ->
745 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
746 | UnificationFailure msg ->
747 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))