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 unif_ty = ref true
137 let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
138 let module S = CicSubstitution in
139 let module C = Cic in
141 let rec aux metasenv subst n context t' ugraph =
144 let subst,metasenv,ugraph1 =
145 fo_unif_subst test_equality_only subst context metasenv
146 (CicSubstitution.lift n arg) t' ugraph
149 subst,metasenv,C.Rel (1 + n),ugraph1
152 | UnificationFailure _ ->
154 | C.Rel m -> subst,metasenv,
155 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
156 | C.Var (uri,exp_named_subst) ->
157 let subst,metasenv,exp_named_subst',ugraph1 =
158 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
160 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
162 (* andrea: in general, beta_expand can create badly typed
163 terms. This happens quite seldom in practice, UNLESS we
164 iterate on the local context. For this reason, we renounce
165 to iterate and just lift *)
169 Some t -> Some (CicSubstitution.lift 1 t)
171 subst, metasenv, C.Meta (i,l), ugraph
173 | C.Implicit _ as t -> subst,metasenv,t,ugraph
175 let subst,metasenv,te',ugraph1 =
176 aux metasenv subst n context te ugraph in
177 let subst,metasenv,ty',ugraph2 =
178 aux metasenv subst n context ty ugraph1 in
179 (* TASSI: sure this is in serial? *)
180 subst,metasenv,(C.Cast (te', ty')),ugraph2
182 let subst,metasenv,s',ugraph1 =
183 aux metasenv subst n context s ugraph in
184 let subst,metasenv,t',ugraph2 =
185 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
188 (* TASSI: sure this is in serial? *)
189 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
190 | C.Lambda (nn,s,t) ->
191 let subst,metasenv,s',ugraph1 =
192 aux metasenv subst n context s ugraph in
193 let subst,metasenv,t',ugraph2 =
194 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
196 (* TASSI: sure this is in serial? *)
197 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
198 | C.LetIn (nn,s,t) ->
199 let subst,metasenv,s',ugraph1 =
200 aux metasenv subst n context s ugraph in
201 let subst,metasenv,t',ugraph2 =
202 aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
205 (* TASSI: sure this is in serial? *)
206 subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
208 let subst,metasenv,revl',ugraph1 =
210 (fun (subst,metasenv,appl,ugraph) t ->
211 let subst,metasenv,t',ugraph1 =
212 aux metasenv subst n context t ugraph in
213 subst,metasenv,(t'::appl),ugraph1
214 ) (subst,metasenv,[],ugraph) l
216 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
217 | C.Const (uri,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.Const (uri,exp_named_subst')),ugraph1
222 | C.MutInd (uri,i,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.MutInd (uri,i,exp_named_subst')),ugraph1
227 | C.MutConstruct (uri,i,j,exp_named_subst) ->
228 let subst,metasenv,exp_named_subst',ugraph1 =
229 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
231 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
232 | C.MutCase (sp,i,outt,t,pl) ->
233 let subst,metasenv,outt',ugraph1 =
234 aux metasenv subst n context outt ugraph in
235 let subst,metasenv,t',ugraph2 =
236 aux metasenv subst n context t ugraph1 in
237 let subst,metasenv,revpl',ugraph3 =
239 (fun (subst,metasenv,pl,ugraph) t ->
240 let subst,metasenv,t',ugraph1 =
241 aux metasenv subst n context t ugraph in
242 subst,metasenv,(t'::pl),ugraph1
243 ) (subst,metasenv,[],ugraph2) pl
245 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
246 (* TASSI: not sure this is serial *)
248 (*CSC: not implemented
249 let tylen = List.length fl in
252 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
255 C.Fix (i, substitutedfl)
257 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
259 (*CSC: not implemented
260 let tylen = List.length fl in
263 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
266 C.CoFix (i, substitutedfl)
269 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
271 and aux_exp_named_subst metasenv subst n context ens ugraph =
273 (fun (uri,t) (subst,metasenv,l,ugraph) ->
274 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
275 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
277 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
279 FreshNamesGenerator.mk_fresh_name ~subst
280 metasenv context (Cic.Name "Hbeta") ~typ:argty
282 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
283 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
284 subst, metasenv, t'', ugraph2
285 in profiler_beta_expand.HExtlib.profile foo ()
288 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
289 let subst,metasenv,hd,ugraph =
291 (fun arg (subst,metasenv,t,ugraph) ->
292 let subst,metasenv,t,ugraph1 =
293 beta_expand test_equality_only
294 metasenv subst context t arg ugraph
296 subst,metasenv,t,ugraph1
297 ) args (subst,metasenv,t,ugraph)
299 subst,metasenv,hd,ugraph
302 (* NUOVA UNIFICAZIONE *)
303 (* A substitution is a (int * Cic.term) list that associates a
304 metavariable i with its body.
305 A metaenv is a (int * Cic.term) list that associate a metavariable
307 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
308 a new substitution which is _NOT_ unwinded. It must be unwinded before
311 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
312 let module C = Cic in
313 let module R = CicReduction in
314 let module S = CicSubstitution in
315 let t1 = deref subst t1 in
316 let t2 = deref subst t2 in
319 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
320 in profiler_are_convertible.HExtlib.profile foo ()
323 subst, metasenv, ugraph
326 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
327 let _,subst,metasenv,ugraph1 =
330 (fun (j,subst,metasenv,ugraph) t1 t2 ->
333 | _,None -> j+1,subst,metasenv,ugraph
334 | Some t1', Some t2' ->
335 (* First possibility: restriction *)
336 (* Second possibility: unification *)
337 (* Third possibility: convertibility *)
340 ~subst ~metasenv context t1' t2' ugraph
343 j+1,subst,metasenv, ugraph1
346 let subst,metasenv,ugraph2 =
349 subst context metasenv t1' t2' ugraph
351 j+1,subst,metasenv,ugraph2
354 | UnificationFailure _ ->
355 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
356 let metasenv, subst =
357 CicMetaSubst.restrict
358 subst [(n,j)] metasenv in
359 j+1,subst,metasenv,ugraph1)
360 ) (1,subst,metasenv,ugraph) ln lm
364 (UnificationFailure (lazy "1"))
367 "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."
368 (CicMetaSubst.ppterm subst t1)
369 (CicMetaSubst.ppterm subst t2))) *)
370 | Invalid_argument _ ->
372 (UnificationFailure (lazy "2")))
375 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
376 (CicMetaSubst.ppterm subst t1)
377 (CicMetaSubst.ppterm subst t2)))) *)
378 in subst,metasenv,ugraph1
379 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
380 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
382 | (t, C.Meta (n,l)) ->
385 C.Meta (n,_), C.Meta (m,_) when n < m -> false
386 | _, C.Meta _ -> false
389 let lower = fun x y -> if swap then y else x in
390 let upper = fun x y -> if swap then x else y in
391 let fo_unif_subst_ordered
392 test_equality_only subst context metasenv m1 m2 ugraph =
393 fo_unif_subst test_equality_only subst context metasenv
394 (lower m1 m2) (upper m1 m2) ugraph
397 let subst,metasenv,ugraph1 =
398 if not (!unif_ty) then subst,metasenv,ugraph else
399 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
402 type_of_aux' metasenv subst context t ugraph
406 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
408 UnificationFailure _ as e -> raise e
409 | Uncertain msg -> raise (UnificationFailure msg)
411 debug_print (lazy "siamo allo huge hack");
412 (* TODO huge hack!!!!
413 * we keep on unifying/refining in the hope that
414 * the problem will be eventually solved.
415 * In the meantime we're breaking a big invariant:
416 * the terms that we are unifying are no longer well
417 * typed in the current context (in the worst case
418 * we could even diverge) *)
419 (subst, metasenv,ugraph)) in
420 let t',metasenv,subst =
422 CicMetaSubst.delift n subst context metasenv l t
424 (CicMetaSubst.MetaSubstFailure msg)->
425 raise (UnificationFailure msg)
426 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
430 C.Sort (C.Type u) when not test_equality_only ->
431 let u' = CicUniv.fresh () in
432 let s = C.Sort (C.Type u') in
434 CicUniv.add_ge (upper u u') (lower u u') ugraph1
439 (* Unifying the types may have already instantiated n. Let's check *)
441 let (_, oldt,_) = CicUtil.lookup_subst n subst in
442 let lifted_oldt = S.subst_meta l oldt in
443 fo_unif_subst_ordered
444 test_equality_only subst context metasenv t lifted_oldt ugraph2
446 CicUtil.Subst_not_found _ ->
447 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
448 let subst = (n, (context, t'',ty)) :: subst in
450 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
451 subst, metasenv, ugraph2
453 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
454 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
455 if UriManager.eq uri1 uri2 then
456 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
457 exp_named_subst1 exp_named_subst2 ugraph
459 raise (UnificationFailure (lazy
461 "Can't unify %s with %s due to different constants"
462 (CicMetaSubst.ppterm subst t1)
463 (CicMetaSubst.ppterm subst t2))))
464 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
465 if UriManager.eq uri1 uri2 && i1 = i2 then
466 fo_unif_subst_exp_named_subst
468 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
470 raise (UnificationFailure (lazy "4"))
472 "Can't unify %s with %s due to different inductive principles"
473 (CicMetaSubst.ppterm subst t1)
474 (CicMetaSubst.ppterm subst t2))) *)
475 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
476 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
477 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
478 fo_unif_subst_exp_named_subst
480 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
482 raise (UnificationFailure (lazy "5"))
484 "Can't unify %s with %s due to different inductive constructors"
485 (CicMetaSubst.ppterm subst t1)
486 (CicMetaSubst.ppterm subst t2))) *)
487 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
488 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
489 subst context metasenv te t2 ugraph
490 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
491 subst context metasenv t1 te ugraph
492 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
493 let subst',metasenv',ugraph1 =
494 fo_unif_subst true 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.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
499 let subst',metasenv',ugraph1 =
500 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
502 fo_unif_subst test_equality_only
503 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
504 | (C.LetIn (_,s1,t1), t2)
505 | (t2, C.LetIn (_,s1,t1)) ->
507 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
508 | (C.Appl l1, C.Appl l2) ->
509 (* andrea: this case should be probably rewritten in the
512 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
515 (fun (subst,metasenv,ugraph) t1 t2 ->
517 test_equality_only subst context metasenv t1 t2 ugraph)
518 (subst,metasenv,ugraph) l1 l2
519 with (Invalid_argument msg) ->
520 raise (UnificationFailure (lazy msg)))
521 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
522 (* we verify that none of the args is a Meta,
523 since beta expanding with respoect to a metavariable
527 let (_,t,_) = CicUtil.lookup_subst i subst in
528 let lifted = S.subst_meta l t in
529 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
532 subst context metasenv reduced t2 ugraph
533 with CicUtil.Subst_not_found _ -> *)
534 let subst,metasenv,beta_expanded,ugraph1 =
536 test_equality_only metasenv subst context t2 args ugraph
538 fo_unif_subst test_equality_only subst context metasenv
539 (C.Meta (i,l)) beta_expanded ugraph1
540 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
542 let (_,t,_) = CicUtil.lookup_subst i subst in
543 let lifted = S.subst_meta l t in
544 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
547 subst context metasenv t1 reduced ugraph
548 with CicUtil.Subst_not_found _ -> *)
549 let subst,metasenv,beta_expanded,ugraph1 =
552 metasenv subst context t1 args ugraph
554 fo_unif_subst test_equality_only subst context metasenv
555 (C.Meta (i,l)) beta_expanded ugraph1
557 let lr1 = List.rev l1 in
558 let lr2 = List.rev l2 in
560 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
563 | _,[] -> assert false
566 test_equality_only subst context metasenv h1 h2 ugraph
569 fo_unif_subst test_equality_only subst context metasenv
570 h (C.Appl (List.rev l)) ugraph
571 | ((h1::l1),(h2::l2)) ->
572 let subst', metasenv',ugraph1 =
575 subst context metasenv h1 h2 ugraph
578 test_equality_only subst' metasenv' (l1,l2) ugraph1
582 test_equality_only subst metasenv (lr1, lr2) ugraph
584 | UnificationFailure _
585 | Uncertain _ as exn ->
587 | (((Cic.Const (uri1, ens1)) as c1) :: tl1),
588 (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
589 CoercGraph.is_a_coercion c1 &&
590 CoercGraph.is_a_coercion c2 ->
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
602 List.exists ((=) (`Class `Coercion)) attrs1 in
604 List.exists ((=) (`Class `Coercion)) attrs2 in
605 (match is_composite1, is_composite2 with
606 | false, false -> raise exn
608 let body1 = CicSubstitution.subst_vars ens1 body1 in
609 let appl = Cic.Appl (body1::tl1) in
610 let redappl = CicReduction.head_beta_reduce appl in
612 test_equality_only subst context metasenv
615 let body2 = CicSubstitution.subst_vars ens2 body2 in
616 let appl = Cic.Appl (body2::tl2) in
617 let redappl = CicReduction.head_beta_reduce appl in
619 test_equality_only subst context metasenv
622 let body1 = CicSubstitution.subst_vars ens1 body1 in
623 let appl1 = Cic.Appl (body1::tl1) in
624 let redappl1 = CicReduction.head_beta_reduce appl1 in
625 let body2 = CicSubstitution.subst_vars ens2 body2 in
626 let appl2 = Cic.Appl (body2::tl2) in
627 let redappl2 = CicReduction.head_beta_reduce appl2 in
629 test_equality_only subst context metasenv
630 redappl1 redappl2 ugraph)
632 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
633 let subst', metasenv',ugraph1 =
634 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
636 let subst'',metasenv'',ugraph2 =
637 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
641 (fun (subst,metasenv,ugraph) t1 t2 ->
643 test_equality_only subst context metasenv t1 t2 ugraph
644 ) (subst'',metasenv'',ugraph2) pl1 pl2
646 Invalid_argument _ ->
647 raise (UnificationFailure (lazy "6.1")))
649 "Error trying to unify %s with %s: the number of branches is not the same."
650 (CicMetaSubst.ppterm subst t1)
651 (CicMetaSubst.ppterm subst t2)))) *)
652 | (C.Rel _, _) | (_, C.Rel _) ->
654 subst, metasenv,ugraph
656 raise (UnificationFailure (lazy
658 "Can't unify %s with %s because they are not convertible"
659 (CicMetaSubst.ppterm subst t1)
660 (CicMetaSubst.ppterm subst t2))))
661 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
662 let subst,metasenv,beta_expanded,ugraph1 =
664 test_equality_only metasenv subst context t2 args ugraph
666 fo_unif_subst test_equality_only subst context metasenv
667 (C.Meta (i,l)) beta_expanded ugraph1
668 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
669 let subst,metasenv,beta_expanded,ugraph1 =
671 test_equality_only metasenv subst context t1 args ugraph
673 fo_unif_subst test_equality_only subst context metasenv
674 beta_expanded (C.Meta (i,l)) ugraph1
675 | (C.Sort _ ,_) | (_, C.Sort _)
676 | (C.Const _, _) | (_, C.Const _)
677 | (C.MutInd _, _) | (_, C.MutInd _)
678 | (C.MutConstruct _, _) | (_, C.MutConstruct _)
679 | (C.Fix _, _) | (_, C.Fix _)
680 | (C.CoFix _, _) | (_, C.CoFix _) ->
682 subst, metasenv, ugraph
685 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
688 subst, metasenv, ugraph1
691 (UnificationFailure (lazy (sprintf
692 "Can't unify %s with %s because they are not convertible"
693 (CicMetaSubst.ppterm subst t1)
694 (CicMetaSubst.ppterm subst t2))))
696 let t2' = R.whd ~subst context t2 in
699 fo_unif_subst test_equality_only
700 subst context metasenv t1 t2' ugraph
701 | _ -> raise (UnificationFailure (lazy "8")))
703 let t1' = R.whd ~subst context t1 in
706 fo_unif_subst test_equality_only
707 subst context metasenv t1' t2 ugraph
708 | _ -> (* raise (UnificationFailure "9")) *)
710 (UnificationFailure (lazy (sprintf
711 "Can't unify %s with %s because they are not convertible"
712 (CicMetaSubst.ppterm subst t1)
713 (CicMetaSubst.ppterm subst t2)))))
715 raise (UnificationFailure (lazy "10"))
717 "Can't unify %s with %s because they are not convertible"
718 (CicMetaSubst.ppterm subst t1)
719 (CicMetaSubst.ppterm subst t2))) *)
721 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
722 exp_named_subst1 exp_named_subst2 ugraph
726 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
728 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
729 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
731 Invalid_argument _ ->
736 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
739 raise (UnificationFailure (lazy (sprintf
740 "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))))
742 (* A substitution is a (int * Cic.term) list that associates a *)
743 (* metavariable i with its body. *)
744 (* metasenv is of type Cic.metasenv *)
745 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
746 (* a new substitution which is already unwinded and ready to be applied and *)
747 (* a new metasenv in which some hypothesis in the contexts of the *)
748 (* metavariables may have been restricted. *)
749 let fo_unif metasenv context t1 t2 ugraph =
750 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
752 let enrich_msg msg subst context metasenv t1 t2 ugraph =
755 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"
756 (CicMetaSubst.ppterm subst t1)
758 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
761 | UnificationFailure s
763 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
764 (CicMetaSubst.ppterm subst t2)
766 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
769 | UnificationFailure s
771 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
772 (CicMetaSubst.ppcontext subst context)
773 (CicMetaSubst.ppmetasenv subst metasenv)
774 (CicMetaSubst.ppsubst subst) (Lazy.force msg)
776 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
777 (CicMetaSubst.ppterm_in_context subst t1 context)
779 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
780 CicMetaSubst.ppterm_in_context subst ty_t1 context
782 | UnificationFailure s
784 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
785 (CicMetaSubst.ppterm_in_context subst t2 context)
787 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
788 CicMetaSubst.ppterm_in_context subst ty_t2 context
790 | UnificationFailure s
792 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
793 (CicMetaSubst.ppcontext subst context)
794 (CicMetaSubst.ppmetasenv subst metasenv)
798 let fo_unif_subst subst context metasenv t1 t2 ugraph =
800 fo_unif_subst false subst context metasenv t1 t2 ugraph
802 | AssertFailure msg ->
803 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
804 | UnificationFailure msg ->
805 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))