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
576 test_equality_only subst metasenv (lr1, lr2) ugraph
578 | UnificationFailure _
579 | Uncertain _ as exn ->
581 | (((Cic.Const (uri1, ens1)) as c1) :: tl1),
582 (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
583 CoercGraph.is_a_coercion c1 &&
584 CoercGraph.is_a_coercion c2 ->
585 let body1, attrs1, ugraph =
586 match CicEnvironment.get_obj ugraph uri1 with
587 | Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
590 let body2, attrs2, ugraph =
591 match CicEnvironment.get_obj ugraph uri2 with
592 | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
596 List.exists ((=) (`Class `Coercion)) attrs1 in
598 List.exists ((=) (`Class `Coercion)) attrs2 in
599 (match is_composite1, is_composite2 with
600 | false, false -> raise exn
602 let body1 = CicSubstitution.subst_vars ens1 body1 in
603 let appl = Cic.Appl (body1::tl1) in
604 let redappl = CicReduction.head_beta_reduce appl in
606 test_equality_only subst context metasenv
609 let body2 = CicSubstitution.subst_vars ens2 body2 in
610 let appl = Cic.Appl (body2::tl2) in
611 let redappl = CicReduction.head_beta_reduce appl in
613 test_equality_only subst context metasenv
616 let body1 = CicSubstitution.subst_vars ens1 body1 in
617 let appl1 = Cic.Appl (body1::tl1) in
618 let redappl1 = CicReduction.head_beta_reduce appl1 in
619 let body2 = CicSubstitution.subst_vars ens2 body2 in
620 let appl2 = Cic.Appl (body2::tl2) in
621 let redappl2 = CicReduction.head_beta_reduce appl2 in
623 test_equality_only subst context metasenv
624 redappl1 redappl2 ugraph)
626 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
627 let subst', metasenv',ugraph1 =
628 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
630 let subst'',metasenv'',ugraph2 =
631 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
635 (fun (subst,metasenv,ugraph) t1 t2 ->
637 test_equality_only subst context metasenv t1 t2 ugraph
638 ) (subst'',metasenv'',ugraph2) pl1 pl2
640 Invalid_argument _ ->
641 raise (UnificationFailure (lazy "6.1")))
643 "Error trying to unify %s with %s: the number of branches is not the same."
644 (CicMetaSubst.ppterm subst t1)
645 (CicMetaSubst.ppterm subst t2)))) *)
646 | (C.Rel _, _) | (_, C.Rel _) ->
648 subst, metasenv,ugraph
650 raise (UnificationFailure (lazy
652 "Can't unify %s with %s because they are not convertible"
653 (CicMetaSubst.ppterm subst t1)
654 (CicMetaSubst.ppterm subst t2))))
655 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
656 let subst,metasenv,beta_expanded,ugraph1 =
658 test_equality_only metasenv subst context t2 args ugraph
660 fo_unif_subst test_equality_only subst context metasenv
661 (C.Meta (i,l)) beta_expanded ugraph1
662 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
663 let subst,metasenv,beta_expanded,ugraph1 =
665 test_equality_only metasenv subst context t1 args ugraph
667 fo_unif_subst test_equality_only subst context metasenv
668 beta_expanded (C.Meta (i,l)) ugraph1
669 | (C.Sort _ ,_) | (_, C.Sort _)
670 | (C.Const _, _) | (_, C.Const _)
671 | (C.MutInd _, _) | (_, C.MutInd _)
672 | (C.MutConstruct _, _) | (_, C.MutConstruct _)
673 | (C.Fix _, _) | (_, C.Fix _)
674 | (C.CoFix _, _) | (_, C.CoFix _) ->
676 subst, metasenv, ugraph
679 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
682 subst, metasenv, ugraph1
685 (UnificationFailure (lazy (sprintf
686 "Can't unify %s with %s because they are not convertible"
687 (CicMetaSubst.ppterm subst t1)
688 (CicMetaSubst.ppterm subst t2))))
690 let t2' = R.whd ~subst context t2 in
693 fo_unif_subst test_equality_only
694 subst context metasenv t1 t2' ugraph
695 | _ -> raise (UnificationFailure (lazy "8")))
697 let t1' = R.whd ~subst context t1 in
700 fo_unif_subst test_equality_only
701 subst context metasenv t1' t2 ugraph
702 | _ -> (* raise (UnificationFailure "9")) *)
704 (UnificationFailure (lazy (sprintf
705 "Can't unify %s with %s because they are not convertible"
706 (CicMetaSubst.ppterm subst t1)
707 (CicMetaSubst.ppterm subst t2)))))
709 raise (UnificationFailure (lazy "10"))
711 "Can't unify %s with %s because they are not convertible"
712 (CicMetaSubst.ppterm subst t1)
713 (CicMetaSubst.ppterm subst t2))) *)
715 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
716 exp_named_subst1 exp_named_subst2 ugraph
720 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
722 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
723 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
725 Invalid_argument _ ->
730 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
733 raise (UnificationFailure (lazy (sprintf
734 "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))))
736 (* A substitution is a (int * Cic.term) list that associates a *)
737 (* metavariable i with its body. *)
738 (* metasenv is of type Cic.metasenv *)
739 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
740 (* a new substitution which is already unwinded and ready to be applied and *)
741 (* a new metasenv in which some hypothesis in the contexts of the *)
742 (* metavariables may have been restricted. *)
743 let fo_unif metasenv context t1 t2 ugraph =
744 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
746 let enrich_msg msg subst context metasenv t1 t2 ugraph =
749 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"
750 (CicMetaSubst.ppterm subst t1)
752 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
755 | UnificationFailure s
757 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
758 (CicMetaSubst.ppterm subst t2)
760 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
763 | UnificationFailure s
765 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
766 (CicMetaSubst.ppcontext subst context)
767 (CicMetaSubst.ppmetasenv subst metasenv)
768 (CicMetaSubst.ppsubst subst) (Lazy.force msg)
770 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
771 (CicMetaSubst.ppterm_in_context subst t1 context)
773 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
774 CicMetaSubst.ppterm_in_context subst ty_t1 context
776 | UnificationFailure s
778 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
779 (CicMetaSubst.ppterm_in_context subst t2 context)
781 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
782 CicMetaSubst.ppterm_in_context subst ty_t2 context
784 | UnificationFailure s
786 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
787 (CicMetaSubst.ppcontext subst context)
788 (CicMetaSubst.ppmetasenv subst metasenv)
792 let fo_unif_subst subst context metasenv t1 t2 ugraph =
794 fo_unif_subst false subst context metasenv t1 t2 ugraph
796 | AssertFailure msg ->
797 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
798 | UnificationFailure msg ->
799 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))