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 ~metasenv subst term)
57 (CicMetaSubst.ppterm ~metasenv [] term)
58 (CicMetaSubst.ppcontext ~metasenv subst context)
59 (CicMetaSubst.ppmetasenv subst metasenv)
60 (CicMetaSubst.ppsubst ~metasenv 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 ~metasenv subst term)
68 (CicMetaSubst.ppterm ~metasenv [] term)
69 (CicMetaSubst.ppcontext ~metasenv subst context)
70 (CicMetaSubst.ppmetasenv subst metasenv)
71 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
72 raise (AssertFailure msg)
73 in profiler_toa.HExtlib.profile foo ()
80 | Cic.Appl (Cic.Meta _::_) -> true
83 let rec deref subst t =
84 let snd (_,a,_) = a in
89 (CicSubstitution.subst_meta
90 l (snd (CicUtil.lookup_subst n subst)))
92 CicUtil.Subst_not_found _ -> t)
93 | Cic.Appl(Cic.Meta(n,l)::args) ->
94 (match deref subst (Cic.Meta(n,l)) with
95 | Cic.Lambda _ as t ->
96 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
97 | r -> Cic.Appl(r::args))
98 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
99 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
104 let foo () = deref subst t
105 in profiler_deref.HExtlib.profile foo ()
107 exception WrongShape;;
108 let eta_reduce after_beta_expansion after_beta_expansion_body
109 before_beta_expansion
112 match before_beta_expansion,after_beta_expansion_body with
113 Cic.Appl l, Cic.Appl l' ->
114 let rec all_but_last check_last =
118 | [_] -> if check_last then raise WrongShape else []
119 | he::tl -> he::(all_but_last check_last tl)
121 let all_but_last check_last l =
122 match all_but_last check_last l with
127 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
128 let all_but_last = all_but_last false l in
129 (* here we should test alpha-equivalence; however we know by
130 construction that here alpha_equivalence is equivalent to = *)
131 if t = all_but_last then
135 | _,_ -> after_beta_expansion
137 WrongShape -> after_beta_expansion
139 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
140 let module S = CicSubstitution in
141 let module C = Cic in
143 let rec aux metasenv subst n context t' ugraph =
146 let subst,metasenv,ugraph1 =
147 fo_unif_subst test_equality_only subst context metasenv
148 (CicSubstitution.lift n arg) t' ugraph
151 subst,metasenv,C.Rel (1 + n),ugraph1
154 | UnificationFailure _ ->
156 | C.Rel m -> subst,metasenv,
157 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
158 | C.Var (uri,exp_named_subst) ->
159 let subst,metasenv,exp_named_subst',ugraph1 =
160 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
162 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
164 (* andrea: in general, beta_expand can create badly typed
165 terms. This happens quite seldom in practice, UNLESS we
166 iterate on the local context. For this reason, we renounce
167 to iterate and just lift *)
171 Some t -> Some (CicSubstitution.lift 1 t)
173 subst, metasenv, C.Meta (i,l), ugraph
175 | C.Implicit _ as t -> subst,metasenv,t,ugraph
177 let subst,metasenv,te',ugraph1 =
178 aux metasenv subst n context te ugraph in
179 let subst,metasenv,ty',ugraph2 =
180 aux metasenv subst n context ty ugraph1 in
181 (* TASSI: sure this is in serial? *)
182 subst,metasenv,(C.Cast (te', ty')),ugraph2
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
190 (* TASSI: sure this is in serial? *)
191 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
192 | C.Lambda (nn,s,t) ->
193 let subst,metasenv,s',ugraph1 =
194 aux metasenv subst n context s ugraph in
195 let subst,metasenv,t',ugraph2 =
196 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
198 (* TASSI: sure this is in serial? *)
199 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
200 | C.LetIn (nn,s,ty,t) ->
201 let subst,metasenv,s',ugraph1 =
202 aux metasenv subst n context s ugraph in
203 let subst,metasenv,ty',ugraph1 =
204 aux metasenv subst n context ty ugraph in
205 let subst,metasenv,t',ugraph2 =
206 aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
209 (* TASSI: sure this is in serial? *)
210 subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
212 let subst,metasenv,revl',ugraph1 =
214 (fun (subst,metasenv,appl,ugraph) t ->
215 let subst,metasenv,t',ugraph1 =
216 aux metasenv subst n context t ugraph in
217 subst,metasenv,(t'::appl),ugraph1
218 ) (subst,metasenv,[],ugraph) l
220 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
221 | C.Const (uri,exp_named_subst) ->
222 let subst,metasenv,exp_named_subst',ugraph1 =
223 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
225 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
226 | C.MutInd (uri,i,exp_named_subst) ->
227 let subst,metasenv,exp_named_subst',ugraph1 =
228 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
230 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
231 | C.MutConstruct (uri,i,j,exp_named_subst) ->
232 let subst,metasenv,exp_named_subst',ugraph1 =
233 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
235 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
236 | C.MutCase (sp,i,outt,t,pl) ->
237 let subst,metasenv,outt',ugraph1 =
238 aux metasenv subst n context outt ugraph in
239 let subst,metasenv,t',ugraph2 =
240 aux metasenv subst n context t ugraph1 in
241 let subst,metasenv,revpl',ugraph3 =
243 (fun (subst,metasenv,pl,ugraph) t ->
244 let subst,metasenv,t',ugraph1 =
245 aux metasenv subst n context t ugraph in
246 subst,metasenv,(t'::pl),ugraph1
247 ) (subst,metasenv,[],ugraph2) pl
249 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
250 (* TASSI: not sure this is serial *)
252 (*CSC: not implemented
253 let tylen = List.length fl in
256 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
259 C.Fix (i, substitutedfl)
261 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
263 (*CSC: not implemented
264 let tylen = List.length fl in
267 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
270 C.CoFix (i, substitutedfl)
273 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
275 and aux_exp_named_subst metasenv subst n context ens ugraph =
277 (fun (uri,t) (subst,metasenv,l,ugraph) ->
278 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
279 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
281 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
283 FreshNamesGenerator.mk_fresh_name ~subst
284 metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
286 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
287 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
288 subst, metasenv, t'', ugraph2
289 in profiler_beta_expand.HExtlib.profile foo ()
292 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
293 let _,subst,metasenv,hd,ugraph =
295 (fun arg (num,subst,metasenv,t,ugraph) ->
296 let subst,metasenv,t,ugraph1 =
297 beta_expand num test_equality_only
298 metasenv subst context t arg ugraph
300 num+1,subst,metasenv,t,ugraph1
301 ) args (1,subst,metasenv,t,ugraph)
303 subst,metasenv,hd,ugraph
306 (* NUOVA UNIFICAZIONE *)
307 (* A substitution is a (int * Cic.term) list that associates a
308 metavariable i with its body.
309 A metaenv is a (int * Cic.term) list that associate a metavariable
311 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
312 a new substitution which is _NOT_ unwinded. It must be unwinded before
315 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
316 let module C = Cic in
317 let module R = CicReduction in
318 let module S = CicSubstitution in
319 let t1 = deref subst t1 in
320 let t2 = deref subst t2 in
321 let (&&&) a b = (a && b) || ((not a) && (not b)) in
322 (* let bef = Sys.time () in *)
324 if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
328 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
329 in profiler_are_convertible.HExtlib.profile foo ()
331 (* let aft = Sys.time () in
332 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^ CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^ CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
334 subst, metasenv, ugraph
337 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
338 let _,subst,metasenv,ugraph1 =
341 (fun (j,subst,metasenv,ugraph) t1 t2 ->
344 | _,None -> j+1,subst,metasenv,ugraph
345 | Some t1', Some t2' ->
346 (* First possibility: restriction *)
347 (* Second possibility: unification *)
348 (* Third possibility: convertibility *)
351 ~subst ~metasenv context t1' t2' ugraph
354 j+1,subst,metasenv, ugraph1
357 let subst,metasenv,ugraph2 =
360 subst context metasenv t1' t2' ugraph
362 j+1,subst,metasenv,ugraph2
365 | UnificationFailure _ ->
366 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
367 let metasenv, subst =
368 CicMetaSubst.restrict
369 subst [(n,j)] metasenv in
370 j+1,subst,metasenv,ugraph1)
371 ) (1,subst,metasenv,ugraph) ln lm
375 (UnificationFailure (lazy "1"))
378 "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."
379 (CicMetaSubst.ppterm ~metasenv subst t1)
380 (CicMetaSubst.ppterm ~metasenv subst t2))) *)
381 | Invalid_argument _ ->
383 (UnificationFailure (lazy "2")))
386 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
387 (CicMetaSubst.ppterm ~metasenv subst t1)
388 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
389 in subst,metasenv,ugraph1
390 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
391 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
393 | (t, C.Meta (n,l)) ->
396 C.Meta (n,_), C.Meta (m,_) when n < m -> false
397 | _, C.Meta _ -> false
400 let lower = fun x y -> if swap then y else x in
401 let upper = fun x y -> if swap then x else y in
402 let fo_unif_subst_ordered
403 test_equality_only subst context metasenv m1 m2 ugraph =
404 fo_unif_subst test_equality_only subst context metasenv
405 (lower m1 m2) (upper m1 m2) ugraph
408 let subst,metasenv,ugraph1 =
409 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
412 type_of_aux' metasenv subst context t ugraph
416 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
418 UnificationFailure _ as e -> raise e
419 | Uncertain msg -> raise (UnificationFailure msg)
421 debug_print (lazy "siamo allo huge hack");
422 (* TODO huge hack!!!!
423 * we keep on unifying/refining in the hope that
424 * the problem will be eventually solved.
425 * In the meantime we're breaking a big invariant:
426 * the terms that we are unifying are no longer well
427 * typed in the current context (in the worst case
428 * we could even diverge) *)
429 (subst, metasenv,ugraph)) in
430 let t',metasenv,subst =
432 CicMetaSubst.delift n subst context metasenv l t
434 (CicMetaSubst.MetaSubstFailure msg)->
435 raise (UnificationFailure msg)
436 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
440 C.Sort (C.Type u) when not test_equality_only ->
441 let u' = CicUniv.fresh () in
442 let s = C.Sort (C.Type u') in
445 CicUniv.add_ge (upper u u') (lower u u') ugraph1
449 CicUniv.UniverseInconsistency msg ->
450 raise (UnificationFailure msg))
453 (* Unifying the types may have already instantiated n. Let's check *)
455 let (_, oldt,_) = CicUtil.lookup_subst n subst in
456 let lifted_oldt = S.subst_meta l oldt in
457 fo_unif_subst_ordered
458 test_equality_only subst context metasenv t lifted_oldt ugraph2
460 CicUtil.Subst_not_found _ ->
461 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
462 let subst = (n, (context, t'',ty)) :: subst in
464 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
465 subst, metasenv, ugraph2
467 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
468 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
469 if UriManager.eq uri1 uri2 then
470 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
471 exp_named_subst1 exp_named_subst2 ugraph
473 raise (UnificationFailure (lazy
475 "Can't unify %s with %s due to different constants"
476 (CicMetaSubst.ppterm ~metasenv subst t1)
477 (CicMetaSubst.ppterm ~metasenv subst t2))))
478 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
479 if UriManager.eq uri1 uri2 && i1 = i2 then
480 fo_unif_subst_exp_named_subst
482 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
484 raise (UnificationFailure
487 "Can't unify %s with %s due to different inductive principles"
488 (CicMetaSubst.ppterm ~metasenv subst t1)
489 (CicMetaSubst.ppterm ~metasenv subst t2))))
490 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
491 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
492 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
493 fo_unif_subst_exp_named_subst
495 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
497 raise (UnificationFailure
500 "Can't unify %s with %s due to different inductive constructors"
501 (CicMetaSubst.ppterm ~metasenv subst t1)
502 (CicMetaSubst.ppterm ~metasenv subst t2))))
503 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
504 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
505 subst context metasenv te t2 ugraph
506 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
507 subst context metasenv t1 te ugraph
508 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
509 let subst',metasenv',ugraph1 =
510 fo_unif_subst true subst context metasenv s1 s2 ugraph
512 fo_unif_subst test_equality_only
513 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
514 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
515 let subst',metasenv',ugraph1 =
516 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
518 fo_unif_subst test_equality_only
519 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
520 | (C.LetIn (_,s1,ty1,t1), t2)
521 | (t2, C.LetIn (_,s1,ty1,t1)) ->
523 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
524 | (C.Appl l1, C.Appl l2) ->
525 (* andrea: this case should be probably rewritten in the
528 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
531 (fun (subst,metasenv,ugraph) t1 t2 ->
533 test_equality_only subst context metasenv t1 t2 ugraph)
534 (subst,metasenv,ugraph) l1 l2
535 with (Invalid_argument msg) ->
536 raise (UnificationFailure (lazy msg)))
537 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
538 (* we verify that none of the args is a Meta,
539 since beta expanding with respoect to a metavariable
543 let (_,t,_) = CicUtil.lookup_subst i subst in
544 let lifted = S.subst_meta l t in
545 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
548 subst context metasenv reduced t2 ugraph
549 with CicUtil.Subst_not_found _ -> *)
550 let subst,metasenv,beta_expanded,ugraph1 =
552 test_equality_only metasenv subst context t2 args ugraph
554 fo_unif_subst test_equality_only subst context metasenv
555 (C.Meta (i,l)) beta_expanded ugraph1
556 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
558 let (_,t,_) = CicUtil.lookup_subst i subst in
559 let lifted = S.subst_meta l t in
560 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
563 subst context metasenv t1 reduced ugraph
564 with CicUtil.Subst_not_found _ -> *)
565 let subst,metasenv,beta_expanded,ugraph1 =
568 metasenv subst context t1 args ugraph
570 fo_unif_subst test_equality_only subst context metasenv
571 (C.Meta (i,l)) beta_expanded ugraph1
573 let lr1 = List.rev l1 in
574 let lr2 = List.rev l2 in
576 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
579 | _,[] -> assert false
582 test_equality_only subst context metasenv h1 h2 ugraph
585 fo_unif_subst test_equality_only subst context metasenv
586 h (C.Appl (List.rev l)) ugraph
587 | ((h1::l1),(h2::l2)) ->
588 let subst', metasenv',ugraph1 =
591 subst context metasenv h1 h2 ugraph
594 test_equality_only subst' metasenv' (l1,l2) ugraph1
598 test_equality_only subst metasenv (lr1, lr2) ugraph
600 | UnificationFailure s
601 | Uncertain s as exn ->
603 | (((Cic.Const (uri1, ens1)) as c1) :: tl1),
604 (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
605 CoercDb.is_a_coercion' c1 &&
606 CoercDb.is_a_coercion' c2 &&
607 not (UriManager.eq uri1 uri2) ->
609 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
612 let rec look_for_first_coercion c tl =
614 CicMetaSubst.apply_subst subst (HExtlib.list_last tl)
616 Cic.Appl ((Cic.Const (uri1,ens1) as c')::tl')
617 when CoercDb.is_a_coercion' c' ->
618 look_for_first_coercion c' tl'
619 | last_tl -> c,last_tl
621 let c1,last_tl1 = look_for_first_coercion c1 tl1 in
622 let c2,last_tl2 = look_for_first_coercion c2 tl2 in
624 CoercDb.coerc_carr_of_term (CoercGraph.source_of c1) in
626 CoercDb.coerc_carr_of_term (CoercGraph.source_of c2) in
627 if CoercDb.eq_carr car1 car2 then
628 (match last_tl1,last_tl2 with
629 C.Meta (i1,_),C.Meta(i2,_) when i1=i2 -> raise exn
632 let subst,metasenv,ugraph =
633 fo_unif_subst test_equality_only subst context
634 metasenv last_tl1 last_tl2 ugraph
636 fo_unif_subst test_equality_only subst context
637 metasenv (C.Appl l1) (C.Appl l2) ugraph
641 CoercGraph.meets metasenv subst context car1 car2
645 | (carr,metasenv,to1,to2)::xxx ->
648 | (m2,_,c2,c2')::_ ->
649 let m1,_,c1,c1' = carr,metasenv,to1,to2 in
651 function Some (_,t) -> CicPp.ppterm t
655 ("There are two minimal joins of "^
656 CoercDb.name_of_carr car1^" and "^
657 CoercDb.name_of_carr car2^": " ^
658 CoercDb.name_of_carr m1 ^ " via "^unopt c1^" + "^
659 unopt c1'^" and " ^ CoercDb.name_of_carr m2^" via "^
660 unopt c2^" + "^unopt c2'));
661 let last_tl1',(subst,metasenv,ugraph) =
662 match last_tl1,to1 with
663 | Cic.Meta (i1,l1),Some (last,coerced) ->
665 fo_unif_subst test_equality_only subst context
666 metasenv coerced last_tl1 ugraph
667 | _ -> last_tl1,(subst,metasenv,ugraph)
669 let last_tl2',(subst,metasenv,ugraph) =
670 match last_tl2,to2 with
671 | Cic.Meta (i2,l2),Some (last,coerced) ->
673 fo_unif_subst test_equality_only subst context
674 metasenv coerced last_tl2 ugraph
675 | _ -> last_tl2,(subst,metasenv,ugraph)
678 prerr_endline ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
680 let subst,metasenv,ugraph =
681 fo_unif_subst test_equality_only subst context
682 metasenv last_tl1' last_tl2' ugraph
684 fo_unif_subst test_equality_only subst context
685 metasenv (C.Appl l1) (C.Appl l2) ugraph)
688 let subst,metasenv,ugraph = res in
689 prerr_endline (">>>> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
692 (*CSC: This is necessary because of the "elim H" tactic
693 where the type of H is only reducible to an
694 inductive type. This could be extended from inductive
695 types to any rigid term. However, the code is
696 duplicated in two places: inside applications and
697 outside them. Probably it would be better to
698 work with lambda-bar terms instead. *)
699 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
700 | (_, Cic.MutInd _::_) ->
701 let t1' = R.whd ~subst context t1 in
703 C.Appl (C.MutInd _::_) ->
704 fo_unif_subst test_equality_only
705 subst context metasenv t1' t2 ugraph
706 | _ -> raise (UnificationFailure (lazy "88")))
707 | (Cic.MutInd _::_,_) ->
708 let t2' = R.whd ~subst context t2 in
710 C.Appl (C.MutInd _::_) ->
711 fo_unif_subst test_equality_only
712 subst context metasenv t1 t2' ugraph
715 (lazy ("not a mutind :"^CicMetaSubst.ppterm ~metasenv subst t2 ))))
717 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
718 let subst', metasenv',ugraph1 =
719 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
721 let subst'',metasenv'',ugraph2 =
722 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
726 (fun (subst,metasenv,ugraph) t1 t2 ->
728 test_equality_only subst context metasenv t1 t2 ugraph
729 ) (subst'',metasenv'',ugraph2) pl1 pl2
731 Invalid_argument _ ->
732 raise (UnificationFailure (lazy "6.1")))
734 "Error trying to unify %s with %s: the number of branches is not the same."
735 (CicMetaSubst.ppterm ~metasenv subst t1)
736 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
737 | (C.Rel _, _) | (_, C.Rel _) ->
739 subst, metasenv,ugraph
741 raise (UnificationFailure (lazy
743 "Can't unify %s with %s because they are not convertible"
744 (CicMetaSubst.ppterm ~metasenv subst t1)
745 (CicMetaSubst.ppterm ~metasenv subst t2))))
746 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
747 let subst,metasenv,beta_expanded,ugraph1 =
749 test_equality_only metasenv subst context t2 args ugraph
751 fo_unif_subst test_equality_only subst context metasenv
752 (C.Meta (i,l)) beta_expanded ugraph1
753 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
754 let subst,metasenv,beta_expanded,ugraph1 =
756 test_equality_only metasenv subst context t1 args ugraph
758 fo_unif_subst test_equality_only subst context metasenv
759 beta_expanded (C.Meta (i,l)) ugraph1
760 (* Works iff there are no arguments applied to it; similar to the
763 let t1' = R.whd ~subst context t1 in
766 fo_unif_subst test_equality_only
767 subst context metasenv t1' t2 ugraph
768 | _ -> raise (UnificationFailure (lazy "8")))
770 (* The following idea could be exploited again; right now we have no
771 longer any example requiring it
773 let t2' = R.whd ~subst context t2 in
776 fo_unif_subst test_equality_only
777 subst context metasenv t1 t2' ugraph
778 | _ -> raise (UnificationFailure (lazy "8")))
780 let t1' = R.whd ~subst context t1 in
783 fo_unif_subst test_equality_only
784 subst context metasenv t1' t2 ugraph
785 | _ -> (* raise (UnificationFailure "9")) *)
787 (UnificationFailure (lazy (sprintf
788 "Can't unify %s with %s because they are not convertible"
789 (CicMetaSubst.ppterm ~metasenv subst t1)
790 (CicMetaSubst.ppterm ~metasenv subst t2)))))
793 (* delta-beta reduction should almost never be a problem for
795 1. long computations require iota reduction
796 2. it is extremely rare that a close term t1 (that could be unified
797 to t2) beta-delta reduces to t1' while t2 does not beta-delta
798 reduces in the same way. This happens only if one meta of t2
799 occurs in head position during beta reduction. In this unluky
800 case too much reduction will be performed on t1 and unification
802 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
803 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
804 if t1 = t1' && t2 = t2' then
805 raise (UnificationFailure
808 "Can't unify %s with %s because they are not convertible"
809 (CicMetaSubst.ppterm ~metasenv subst t1)
810 (CicMetaSubst.ppterm ~metasenv subst t2))))
813 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
817 raise (UnificationFailure
820 "Can't unify %s with %s because they are not convertible"
821 (CicMetaSubst.ppterm ~metasenv subst t1)
822 (CicMetaSubst.ppterm ~metasenv subst t2))))
824 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
825 exp_named_subst1 exp_named_subst2 ugraph
829 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
831 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
832 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
834 Invalid_argument _ ->
839 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
842 raise (UnificationFailure (lazy (sprintf
843 "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))))
845 (* A substitution is a (int * Cic.term) list that associates a *)
846 (* metavariable i with its body. *)
847 (* metasenv is of type Cic.metasenv *)
848 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
849 (* a new substitution which is already unwinded and ready to be applied and *)
850 (* a new metasenv in which some hypothesis in the contexts of the *)
851 (* metavariables may have been restricted. *)
852 let fo_unif metasenv context t1 t2 ugraph =
853 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
855 let enrich_msg msg subst context metasenv t1 t2 ugraph =
858 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"
859 (CicMetaSubst.ppterm ~metasenv subst t1)
861 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
864 | UnificationFailure s
866 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
867 (CicMetaSubst.ppterm ~metasenv subst t2)
869 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
872 | UnificationFailure s
874 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
875 (CicMetaSubst.ppcontext ~metasenv subst context)
876 (CicMetaSubst.ppmetasenv subst metasenv)
877 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
879 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
880 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
882 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
883 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
885 | UnificationFailure s
887 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
888 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
890 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
891 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
893 | UnificationFailure s
895 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
896 (CicMetaSubst.ppcontext ~metasenv subst context)
897 (CicMetaSubst.ppmetasenv subst metasenv)
901 let fo_unif_subst subst context metasenv t1 t2 ugraph =
903 fo_unif_subst false subst context metasenv t1 t2 ugraph
905 | AssertFailure msg ->
906 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
907 | UnificationFailure msg ->
908 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))