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.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
509 let subst',metasenv',ugraph1 =
510 fo_unif_subst test_equality_only 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.LetIn (_,s1,ty1,t1), t2)
515 | (t2, C.LetIn (_,s1,ty1,t1)) ->
517 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
518 | (C.Appl l1, C.Appl l2) ->
519 (* andrea: this case should be probably rewritten in the
522 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
525 (fun (subst,metasenv,ugraph) t1 t2 ->
527 test_equality_only subst context metasenv t1 t2 ugraph)
528 (subst,metasenv,ugraph) l1 l2
529 with (Invalid_argument msg) ->
530 raise (UnificationFailure (lazy msg)))
531 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
532 (* we verify that none of the args is a Meta,
533 since beta expanding with respoect to a metavariable
537 let (_,t,_) = CicUtil.lookup_subst i subst in
538 let lifted = S.subst_meta l t in
539 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
542 subst context metasenv reduced t2 ugraph
543 with CicUtil.Subst_not_found _ -> *)
544 let subst,metasenv,beta_expanded,ugraph1 =
546 test_equality_only metasenv subst context t2 args ugraph
548 fo_unif_subst test_equality_only subst context metasenv
549 (C.Meta (i,l)) beta_expanded ugraph1
550 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
552 let (_,t,_) = CicUtil.lookup_subst i subst in
553 let lifted = S.subst_meta l t in
554 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
557 subst context metasenv t1 reduced ugraph
558 with CicUtil.Subst_not_found _ -> *)
559 let subst,metasenv,beta_expanded,ugraph1 =
562 metasenv subst context t1 args ugraph
564 fo_unif_subst test_equality_only subst context metasenv
565 (C.Meta (i,l)) beta_expanded ugraph1
567 let lr1 = List.rev l1 in
568 let lr2 = List.rev l2 in
570 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
573 | _,[] -> assert false
576 test_equality_only subst context metasenv h1 h2 ugraph
579 fo_unif_subst test_equality_only subst context metasenv
580 h (C.Appl (List.rev l)) ugraph
581 | ((h1::l1),(h2::l2)) ->
582 let subst', metasenv',ugraph1 =
585 subst context metasenv h1 h2 ugraph
588 test_equality_only subst' metasenv' (l1,l2) ugraph1
592 test_equality_only subst metasenv (lr1, lr2) ugraph
594 | UnificationFailure s
595 | Uncertain s as exn ->
597 | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
598 (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
599 CoercDb.is_a_coercion cc1 <> None &&
600 CoercDb.is_a_coercion cc2 <> None &&
601 not (UriManager.eq uri1 uri2) ->
603 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
606 let inner_coerced t =
607 let t = CicMetaSubst.apply_subst subst t in
611 (match CoercGraph.coerced_arg l with
613 | Some (t,_) -> aux (List.hd l) t t)
616 aux (Cic.Implicit None) (Cic.Implicit None) t
618 let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
619 let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
622 CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
624 | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
627 let head1_c, head2_c =
629 CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
631 | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
634 let unfold uri ens args =
636 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
640 | Cic.Constant (_,Some bo,_,_,_) ->
641 CicReduction.head_beta_reduce ~delta:false
642 (Cic.Appl (bo::args))
645 if CoercDb.eq_carr car1 car2 then
646 match last_tl1,last_tl2 with
647 | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
650 let subst,metasenv,ugraph =
651 fo_unif_subst test_equality_only subst context
652 metasenv last_tl1 last_tl2 ugraph
654 fo_unif_subst test_equality_only subst context
655 metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
656 | _ when CoercDb.eq_carr head1_c head2_c ->
658 (* composite VS composition + metas avoiding
659 * coercions not only in coerced position *)
661 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
662 else if c2 = cc2 then
663 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
666 fo_unif_subst test_equality_only subst context
667 metasenv l1 l2 ugraph
671 CoercGraph.meets metasenv subst context car1 car2
675 | (carr,metasenv,to1,to2)::xxx ->
678 | (m2,_,c2,c2')::_ ->
679 let m1,_,c1,c1' = carr,metasenv,to1,to2 in
681 function Some (_,t) -> CicPp.ppterm t
685 ("There are two minimal joins of "^
686 CoercDb.string_of_carr car1^" and "^
687 CoercDb.string_of_carr car2^": " ^
688 CoercDb.string_of_carr m1 ^ " via "^unopt c1^" + "^
689 unopt c1'^" and "^CoercDb.string_of_carr m2^" via "^
690 unopt c2^" + "^unopt c2'));
691 let last_tl1',(subst,metasenv,ugraph) =
692 match last_tl1,to1 with
693 | Cic.Meta (i1,l1),Some (last,coerced) ->
695 fo_unif_subst test_equality_only subst context
696 metasenv coerced last_tl1 ugraph
697 | _ -> last_tl1,(subst,metasenv,ugraph)
699 let last_tl2',(subst,metasenv,ugraph) =
700 match last_tl2,to2 with
701 | Cic.Meta (i2,l2),Some (last,coerced) ->
703 fo_unif_subst test_equality_only subst context
704 metasenv coerced last_tl2 ugraph
705 | _ -> last_tl2,(subst,metasenv,ugraph)
707 let subst',metasenv,ugraph =
709 prerr_endline ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
711 fo_unif_subst test_equality_only subst context
712 metasenv last_tl1' last_tl2' ugraph
714 if subst = subst' then raise exn else
715 fo_unif_subst test_equality_only subst' context
716 metasenv (C.Appl l1) (C.Appl l2) ugraph)
719 let subst,metasenv,ugraph = res in
720 prerr_endline (">>>> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
724 (*CSC: This is necessary because of the "elim H" tactic
725 where the type of H is only reducible to an
726 inductive type. This could be extended from inductive
727 types to any rigid term. However, the code is
728 duplicated in two places: inside applications and
729 outside them. Probably it would be better to
730 work with lambda-bar terms instead. *)
731 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
732 | (_, Cic.MutInd _::_) ->
733 let t1' = R.whd ~subst context t1 in
735 C.Appl (C.MutInd _::_) ->
736 fo_unif_subst test_equality_only
737 subst context metasenv t1' t2 ugraph
738 | _ -> raise (UnificationFailure (lazy "88")))
739 | (Cic.MutInd _::_,_) ->
740 let t2' = R.whd ~subst context t2 in
742 C.Appl (C.MutInd _::_) ->
743 fo_unif_subst test_equality_only
744 subst context metasenv t1 t2' ugraph
747 (lazy ("not a mutind :"^CicMetaSubst.ppterm ~metasenv subst t2 ))))
749 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
750 let subst', metasenv',ugraph1 =
751 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
753 let subst'',metasenv'',ugraph2 =
754 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
758 (fun (subst,metasenv,ugraph) t1 t2 ->
760 test_equality_only subst context metasenv t1 t2 ugraph
761 ) (subst'',metasenv'',ugraph2) pl1 pl2
763 Invalid_argument _ ->
764 raise (UnificationFailure (lazy "6.1")))
766 "Error trying to unify %s with %s: the number of branches is not the same."
767 (CicMetaSubst.ppterm ~metasenv subst t1)
768 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
769 | (C.Rel _, _) | (_, C.Rel _) ->
771 subst, metasenv,ugraph
773 raise (UnificationFailure (lazy
775 "Can't unify %s with %s because they are not convertible"
776 (CicMetaSubst.ppterm ~metasenv subst t1)
777 (CicMetaSubst.ppterm ~metasenv subst t2))))
778 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
779 let subst,metasenv,beta_expanded,ugraph1 =
781 test_equality_only metasenv subst context t2 args ugraph
783 fo_unif_subst test_equality_only subst context metasenv
784 (C.Meta (i,l)) beta_expanded ugraph1
785 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
786 let subst,metasenv,beta_expanded,ugraph1 =
788 test_equality_only metasenv subst context t1 args ugraph
790 fo_unif_subst test_equality_only subst context metasenv
791 beta_expanded (C.Meta (i,l)) ugraph1
792 (* Works iff there are no arguments applied to it; similar to the
795 let t1' = R.whd ~subst context t1 in
798 fo_unif_subst test_equality_only
799 subst context metasenv t1' t2 ugraph
800 | _ -> raise (UnificationFailure (lazy "8")))
802 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
803 let subst',metasenv',ugraph1 =
804 fo_unif_subst true subst context metasenv s1 s2 ugraph
806 fo_unif_subst test_equality_only
807 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
809 (match CicReduction.whd ~subst context t2 with
811 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
812 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
814 (match CicReduction.whd ~subst context t1 with
816 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
817 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
819 (* delta-beta reduction should almost never be a problem for
821 1. long computations require iota reduction
822 2. it is extremely rare that a close term t1 (that could be unified
823 to t2) beta-delta reduces to t1' while t2 does not beta-delta
824 reduces in the same way. This happens only if one meta of t2
825 occurs in head position during beta reduction. In this unluky
826 case too much reduction will be performed on t1 and unification
828 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
829 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
830 if t1 = t1' && t2 = t2' then
831 raise (UnificationFailure
834 "Can't unify %s with %s because they are not convertible"
835 (CicMetaSubst.ppterm ~metasenv subst t1)
836 (CicMetaSubst.ppterm ~metasenv subst t2))))
839 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
843 raise (UnificationFailure
846 "Can't unify %s with %s because they are not convertible"
847 (CicMetaSubst.ppterm ~metasenv subst t1)
848 (CicMetaSubst.ppterm ~metasenv subst t2))))
850 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
851 exp_named_subst1 exp_named_subst2 ugraph
855 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
857 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
858 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
860 Invalid_argument _ ->
865 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
868 raise (UnificationFailure (lazy (sprintf
869 "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))))
871 (* A substitution is a (int * Cic.term) list that associates a *)
872 (* metavariable i with its body. *)
873 (* metasenv is of type Cic.metasenv *)
874 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
875 (* a new substitution which is already unwinded and ready to be applied and *)
876 (* a new metasenv in which some hypothesis in the contexts of the *)
877 (* metavariables may have been restricted. *)
878 let fo_unif metasenv context t1 t2 ugraph =
879 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
881 let enrich_msg msg subst context metasenv t1 t2 ugraph =
884 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"
885 (CicMetaSubst.ppterm ~metasenv subst t1)
887 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
890 | UnificationFailure s
892 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
893 (CicMetaSubst.ppterm ~metasenv subst t2)
895 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
898 | UnificationFailure s
900 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
901 (CicMetaSubst.ppcontext ~metasenv subst context)
902 (CicMetaSubst.ppmetasenv subst metasenv)
903 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
905 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
906 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
908 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
909 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
911 | UnificationFailure s
913 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
914 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
916 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
917 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
919 | UnificationFailure s
921 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
922 (CicMetaSubst.ppcontext ~metasenv subst context)
923 (CicMetaSubst.ppmetasenv subst metasenv)
927 let fo_unif_subst subst context metasenv t1 t2 ugraph =
929 fo_unif_subst false subst context metasenv t1 t2 ugraph
931 | AssertFailure msg ->
932 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
933 | UnificationFailure msg ->
934 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))