2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
17 exception UnificationFailure of string Lazy.t;;
18 exception Uncertain of string Lazy.t;;
19 exception AssertFailure of string Lazy.t;;
22 let debug_print = fun _ -> ()
24 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
25 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
26 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
27 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
29 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
31 let type_of_aux' metasenv subst context term ugraph =
34 profile.HExtlib.profile
35 (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
37 CicTypeChecker.TypeCheckerFailure msg ->
41 "Kernel Type checking error:
42 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
43 (CicMetaSubst.ppterm ~metasenv subst term)
44 (CicMetaSubst.ppterm ~metasenv [] term)
45 (CicMetaSubst.ppcontext ~metasenv subst context)
46 (CicMetaSubst.ppmetasenv subst metasenv)
47 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
48 raise (AssertFailure msg)
49 | CicTypeChecker.AssertFailure msg ->
52 "Kernel Type checking assertion failure:
53 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
54 (CicMetaSubst.ppterm ~metasenv subst term)
55 (CicMetaSubst.ppterm ~metasenv [] term)
56 (CicMetaSubst.ppcontext ~metasenv subst context)
57 (CicMetaSubst.ppmetasenv subst metasenv)
58 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
59 raise (AssertFailure msg)
60 in profiler_toa.HExtlib.profile foo ()
67 | Cic.Appl (Cic.Meta _::_) -> true
70 let rec deref subst t =
71 let snd (_,a,_) = a in
76 (CicSubstitution.subst_meta
77 l (snd (CicUtil.lookup_subst n subst)))
79 CicUtil.Subst_not_found _ -> t)
80 | Cic.Appl(Cic.Meta(n,l)::args) ->
81 (match deref subst (Cic.Meta(n,l)) with
82 | Cic.Lambda _ as t ->
83 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
84 | r -> Cic.Appl(r::args))
85 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
86 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
91 let foo () = deref subst t
92 in profiler_deref.HExtlib.profile foo ()
94 exception WrongShape;;
95 let eta_reduce after_beta_expansion after_beta_expansion_body
99 match before_beta_expansion,after_beta_expansion_body with
100 Cic.Appl l, Cic.Appl l' ->
101 let rec all_but_last check_last =
105 | [_] -> if check_last then raise WrongShape else []
106 | he::tl -> he::(all_but_last check_last tl)
108 let all_but_last check_last l =
109 match all_but_last check_last l with
114 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
115 let all_but_last = all_but_last false l in
116 (* here we should test alpha-equivalence; however we know by
117 construction that here alpha_equivalence is equivalent to = *)
118 if t = all_but_last then
122 | _,_ -> after_beta_expansion
124 WrongShape -> after_beta_expansion
126 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
127 let module S = CicSubstitution in
128 let module C = Cic in
130 let rec aux metasenv subst n context t' ugraph =
133 let subst,metasenv,ugraph1 =
134 fo_unif_subst test_equality_only subst context metasenv
135 (CicSubstitution.lift n arg) t' ugraph
138 subst,metasenv,C.Rel (1 + n),ugraph1
141 | UnificationFailure _ ->
143 | C.Rel m -> subst,metasenv,
144 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
145 | C.Var (uri,exp_named_subst) ->
146 let subst,metasenv,exp_named_subst',ugraph1 =
147 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
149 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
151 (* andrea: in general, beta_expand can create badly typed
152 terms. This happens quite seldom in practice, UNLESS we
153 iterate on the local context. For this reason, we renounce
154 to iterate and just lift *)
158 Some t -> Some (CicSubstitution.lift 1 t)
160 subst, metasenv, C.Meta (i,l), ugraph
162 | C.Implicit _ as t -> subst,metasenv,t,ugraph
164 let subst,metasenv,te',ugraph1 =
165 aux metasenv subst n context te ugraph in
166 let subst,metasenv,ty',ugraph2 =
167 aux metasenv subst n context ty ugraph1 in
168 (* TASSI: sure this is in serial? *)
169 subst,metasenv,(C.Cast (te', ty')),ugraph2
171 let subst,metasenv,s',ugraph1 =
172 aux metasenv subst n context s ugraph in
173 let subst,metasenv,t',ugraph2 =
174 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
177 (* TASSI: sure this is in serial? *)
178 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
179 | C.Lambda (nn,s,t) ->
180 let subst,metasenv,s',ugraph1 =
181 aux metasenv subst n context s ugraph in
182 let subst,metasenv,t',ugraph2 =
183 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
185 (* TASSI: sure this is in serial? *)
186 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
187 | C.LetIn (nn,s,ty,t) ->
188 let subst,metasenv,s',ugraph1 =
189 aux metasenv subst n context s ugraph in
190 let subst,metasenv,ty',ugraph1 =
191 aux metasenv subst n context ty ugraph in
192 let subst,metasenv,t',ugraph2 =
193 aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
196 (* TASSI: sure this is in serial? *)
197 subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
199 let subst,metasenv,revl',ugraph1 =
201 (fun (subst,metasenv,appl,ugraph) t ->
202 let subst,metasenv,t',ugraph1 =
203 aux metasenv subst n context t ugraph in
204 subst,metasenv,(t'::appl),ugraph1
205 ) (subst,metasenv,[],ugraph) l
207 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
208 | C.Const (uri,exp_named_subst) ->
209 let subst,metasenv,exp_named_subst',ugraph1 =
210 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
212 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
213 | C.MutInd (uri,i,exp_named_subst) ->
214 let subst,metasenv,exp_named_subst',ugraph1 =
215 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
217 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
218 | C.MutConstruct (uri,i,j,exp_named_subst) ->
219 let subst,metasenv,exp_named_subst',ugraph1 =
220 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
222 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
223 | C.MutCase (sp,i,outt,t,pl) ->
224 let subst,metasenv,outt',ugraph1 =
225 aux metasenv subst n context outt ugraph in
226 let subst,metasenv,t',ugraph2 =
227 aux metasenv subst n context t ugraph1 in
228 let subst,metasenv,revpl',ugraph3 =
230 (fun (subst,metasenv,pl,ugraph) t ->
231 let subst,metasenv,t',ugraph1 =
232 aux metasenv subst n context t ugraph in
233 subst,metasenv,(t'::pl),ugraph1
234 ) (subst,metasenv,[],ugraph2) pl
236 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
237 (* TASSI: not sure this is serial *)
239 (*CSC: not implemented
240 let tylen = List.length fl in
243 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
246 C.Fix (i, substitutedfl)
248 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
250 (*CSC: not implemented
251 let tylen = List.length fl in
254 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
257 C.CoFix (i, substitutedfl)
260 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
262 and aux_exp_named_subst metasenv subst n context ens ugraph =
264 (fun (uri,t) (subst,metasenv,l,ugraph) ->
265 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
266 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
268 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
270 FreshNamesGenerator.mk_fresh_name ~subst
271 metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
273 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
274 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
275 subst, metasenv, t'', ugraph2
276 in profiler_beta_expand.HExtlib.profile foo ()
279 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
280 let _,subst,metasenv,hd,ugraph =
282 (fun arg (num,subst,metasenv,t,ugraph) ->
283 let subst,metasenv,t,ugraph1 =
284 beta_expand num test_equality_only
285 metasenv subst context t arg ugraph
287 num+1,subst,metasenv,t,ugraph1
288 ) args (1,subst,metasenv,t,ugraph)
290 subst,metasenv,hd,ugraph
292 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
295 | (m2,_,c2,c2')::_ ->
296 let m1,c1,c1' = carr,to1,to2 in
298 function Some (_,t) -> CicPp.ppterm t
302 ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
303 CoercDb.string_of_carr car2^": " ^
304 CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
305 unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
306 unopt c2^" + "^unopt c2')
308 (* NUOVA UNIFICAZIONE *)
309 (* A substitution is a (int * Cic.term) list that associates a
310 metavariable i with its body.
311 A metaenv is a (int * Cic.term) list that associate a metavariable
313 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
314 a new substitution which is _NOT_ unwinded. It must be unwinded before
317 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
318 let module C = Cic in
319 let module R = CicReduction in
320 let module S = CicSubstitution in
321 let t1 = deref subst t1 in
322 let t2 = deref subst t2 in
323 let (&&&) a b = (a && b) || ((not a) && (not b)) in
324 (* let bef = Sys.time () in *)
326 if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
330 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
331 in profiler_are_convertible.HExtlib.profile foo ()
333 (* let aft = Sys.time () in
334 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
335 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
336 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
338 subst, metasenv, ugraph
341 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
342 let _,subst,metasenv,ugraph1 =
345 (fun (j,subst,metasenv,ugraph) t1 t2 ->
348 | _,None -> j+1,subst,metasenv,ugraph
349 | Some t1', Some t2' ->
350 (* First possibility: restriction *)
351 (* Second possibility: unification *)
352 (* Third possibility: convertibility *)
355 ~subst ~metasenv context t1' t2' ugraph
358 j+1,subst,metasenv, ugraph1
361 let subst,metasenv,ugraph2 =
364 subst context metasenv t1' t2' ugraph
366 j+1,subst,metasenv,ugraph2
369 | UnificationFailure _ ->
370 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
371 let metasenv, subst =
372 CicMetaSubst.restrict
373 subst [(n,j)] metasenv in
374 j+1,subst,metasenv,ugraph1)
375 ) (1,subst,metasenv,ugraph) ln lm
379 (UnificationFailure (lazy "1"))
382 "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."
383 (CicMetaSubst.ppterm ~metasenv subst t1)
384 (CicMetaSubst.ppterm ~metasenv subst t2))) *)
385 | Invalid_argument _ ->
387 (UnificationFailure (lazy "2")))
390 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
391 (CicMetaSubst.ppterm ~metasenv subst t1)
392 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
393 in subst,metasenv,ugraph1
394 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
395 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
397 | (t, C.Meta (n,l)) ->
400 C.Meta (n,_), C.Meta (m,_) when n < m -> false
401 | _, C.Meta _ -> false
404 let lower = fun x y -> if swap then y else x in
405 let upper = fun x y -> if swap then x else y in
406 let fo_unif_subst_ordered
407 test_equality_only subst context metasenv m1 m2 ugraph =
408 fo_unif_subst test_equality_only subst context metasenv
409 (lower m1 m2) (upper m1 m2) ugraph
412 let subst,metasenv,ugraph1 =
413 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
416 type_of_aux' metasenv subst context t ugraph
420 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
422 UnificationFailure _ as e -> raise e
423 | Uncertain msg -> raise (UnificationFailure msg)
425 debug_print (lazy "siamo allo huge hack");
426 (* TODO huge hack!!!!
427 * we keep on unifying/refining in the hope that
428 * the problem will be eventually solved.
429 * In the meantime we're breaking a big invariant:
430 * the terms that we are unifying are no longer well
431 * typed in the current context (in the worst case
432 * we could even diverge) *)
433 (subst, metasenv,ugraph)) in
434 let t',metasenv,subst =
436 CicMetaSubst.delift n subst context metasenv l t
438 (CicMetaSubst.MetaSubstFailure msg)->
439 raise (UnificationFailure msg)
440 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
444 C.Sort (C.Type u) when not test_equality_only ->
445 let u' = CicUniv.fresh () in
446 let s = C.Sort (C.Type u') in
449 CicUniv.add_ge (upper u u') (lower u u') ugraph1
453 CicUniv.UniverseInconsistency msg ->
454 raise (UnificationFailure msg))
457 (* Unifying the types may have already instantiated n. Let's check *)
459 let (_, oldt,_) = CicUtil.lookup_subst n subst in
460 let lifted_oldt = S.subst_meta l oldt in
461 fo_unif_subst_ordered
462 test_equality_only subst context metasenv t lifted_oldt ugraph2
464 CicUtil.Subst_not_found _ ->
465 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
466 let subst = (n, (context, t'',ty)) :: subst in
468 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
469 subst, metasenv, ugraph2
471 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
472 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
473 if UriManager.eq uri1 uri2 then
474 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
475 exp_named_subst1 exp_named_subst2 ugraph
477 raise (UnificationFailure (lazy
479 "Can't unify %s with %s due to different constants"
480 (CicMetaSubst.ppterm ~metasenv subst t1)
481 (CicMetaSubst.ppterm ~metasenv subst t2))))
482 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
483 if UriManager.eq uri1 uri2 && i1 = i2 then
484 fo_unif_subst_exp_named_subst
486 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
488 raise (UnificationFailure
491 "Can't unify %s with %s due to different inductive principles"
492 (CicMetaSubst.ppterm ~metasenv subst t1)
493 (CicMetaSubst.ppterm ~metasenv subst t2))))
494 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
495 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
496 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
497 fo_unif_subst_exp_named_subst
499 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
501 raise (UnificationFailure
504 "Can't unify %s with %s due to different inductive constructors"
505 (CicMetaSubst.ppterm ~metasenv subst t1)
506 (CicMetaSubst.ppterm ~metasenv subst t2))))
507 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
508 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
509 subst context metasenv te t2 ugraph
510 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
511 subst context metasenv t1 te ugraph
512 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
513 let subst',metasenv',ugraph1 =
514 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
516 fo_unif_subst test_equality_only
517 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
518 | (C.LetIn (_,s1,ty1,t1), t2)
519 | (t2, C.LetIn (_,s1,ty1,t1)) ->
521 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
522 | (C.Appl l1, C.Appl l2) ->
523 (* andrea: this case should be probably rewritten in the
526 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
529 (fun (subst,metasenv,ugraph) t1 t2 ->
531 test_equality_only subst context metasenv t1 t2 ugraph)
532 (subst,metasenv,ugraph) l1 l2
533 with (Invalid_argument msg) ->
534 raise (UnificationFailure (lazy msg)))
535 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
536 (* we verify that none of the args is a Meta,
537 since beta expanding with respoect to a metavariable
541 let (_,t,_) = CicUtil.lookup_subst i subst in
542 let lifted = S.subst_meta l t in
543 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
546 subst context metasenv reduced t2 ugraph
547 with CicUtil.Subst_not_found _ -> *)
548 let subst,metasenv,beta_expanded,ugraph1 =
550 test_equality_only metasenv subst context t2 args ugraph
552 fo_unif_subst test_equality_only subst context metasenv
553 (C.Meta (i,l)) beta_expanded ugraph1
554 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
556 let (_,t,_) = CicUtil.lookup_subst i subst in
557 let lifted = S.subst_meta l t in
558 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
561 subst context metasenv t1 reduced ugraph
562 with CicUtil.Subst_not_found _ -> *)
563 let subst,metasenv,beta_expanded,ugraph1 =
566 metasenv subst context t1 args ugraph
568 fo_unif_subst test_equality_only subst context metasenv
569 (C.Meta (i,l)) beta_expanded ugraph1
571 let lr1 = List.rev l1 in
572 let lr2 = List.rev l2 in
574 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
577 | _,[] -> assert false
580 test_equality_only subst context metasenv h1 h2 ugraph
583 fo_unif_subst test_equality_only subst context metasenv
584 h (C.Appl (List.rev l)) ugraph
585 | ((h1::l1),(h2::l2)) ->
586 let subst', metasenv',ugraph1 =
589 subst context metasenv h1 h2 ugraph
592 test_equality_only subst' metasenv' (l1,l2) ugraph1
596 test_equality_only subst metasenv (lr1, lr2) ugraph
598 | UnificationFailure s
599 | Uncertain s as exn ->
602 | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
603 (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
604 CoercDb.is_a_coercion cc1 <> None &&
605 CoercDb.is_a_coercion cc2 <> None &&
606 not (UriManager.eq uri1 uri2) ->
608 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
610 let inner_coerced t =
611 let t = CicMetaSubst.apply_subst subst t in
615 (match CoercGraph.coerced_arg l with
617 | Some (t,_) -> aux (List.hd l) t t)
620 aux (Cic.Implicit None) (Cic.Implicit None) t
622 let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
623 let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
626 CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
628 | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
631 let head1_c, head2_c =
633 CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
635 | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
638 let unfold uri ens args =
640 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
644 | Cic.Constant (_,Some bo,_,_,_) ->
645 CicReduction.head_beta_reduce ~delta:false
646 (Cic.Appl (bo::args))
649 let conclude subst metasenv ugraph last_tl1' last_tl2' =
650 let subst',metasenv,ugraph =
653 ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
654 " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
656 fo_unif_subst test_equality_only subst context
657 metasenv last_tl1' last_tl2' ugraph
659 if subst = subst' then raise exn
662 let subst,metasenv,ugrph as res =
664 fo_unif_subst test_equality_only subst' context
665 metasenv (C.Appl l1) (C.Appl l2) ugraph
669 (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
670 " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
674 if CoercDb.eq_carr car1 car2 then
675 match last_tl1,last_tl2 with
676 | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
679 let subst,metasenv,ugraph =
680 fo_unif_subst test_equality_only subst context
681 metasenv last_tl1 last_tl2 ugraph
683 fo_unif_subst test_equality_only subst context
684 metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
685 | _ when CoercDb.eq_carr head1_c head2_c ->
686 (* composite VS composition + metas avoiding
687 * coercions not only in coerced position *)
688 if c1 <> cc1 && c2 <> cc2 then
689 conclude subst metasenv ugraph
694 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
696 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
698 fo_unif_subst test_equality_only subst context
699 metasenv l1 l2 ugraph
703 match last_tl1 with Cic.Meta _ -> true | _ -> false in
705 match last_tl2 with Cic.Meta _ -> true | _ -> false in
706 if not (grow1 || grow2) then
707 (* no flexible terminals -> no pullback, but
708 * we still unify them, in some cases it helps *)
709 conclude subst metasenv ugraph last_tl1 last_tl2
713 metasenv subst context (grow1,car1) (grow2,car2)
717 | (carr,metasenv,to1,to2)::xxx ->
718 warn_if_not_unique xxx to1 to2 carr car1 car2;
719 let last_tl1',(subst,metasenv,ugraph) =
721 | true,Some (last,coerced) ->
723 fo_unif_subst test_equality_only subst context
724 metasenv coerced last_tl1 ugraph
725 | _ -> last_tl1,(subst,metasenv,ugraph)
727 let last_tl2',(subst,metasenv,ugraph) =
729 | true,Some (last,coerced) ->
731 fo_unif_subst test_equality_only subst context
732 metasenv coerced last_tl2 ugraph
733 | _ -> last_tl2,(subst,metasenv,ugraph)
735 conclude subst metasenv ugraph last_tl1' last_tl2')
737 (* {{{ CSC: This is necessary because of the "elim H" tactic
738 where the type of H is only reducible to an
739 inductive type. This could be extended from inductive
740 types to any rigid term. However, the code is
741 duplicated in two places: inside applications and
742 outside them. Probably it would be better to
743 work with lambda-bar terms instead. *)
744 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
745 | (_, Cic.MutInd _::_) ->
746 let t1' = R.whd ~subst context t1 in
748 C.Appl (C.MutInd _::_) ->
749 fo_unif_subst test_equality_only
750 subst context metasenv t1' t2 ugraph
751 | _ -> raise (UnificationFailure (lazy "88")))
752 | (Cic.MutInd _::_,_) ->
753 let t2' = R.whd ~subst context t2 in
755 C.Appl (C.MutInd _::_) ->
756 fo_unif_subst test_equality_only
757 subst context metasenv t1 t2' ugraph
760 (lazy ("not a mutind :"^
761 CicMetaSubst.ppterm ~metasenv subst t2 ))))
764 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
765 let subst', metasenv',ugraph1 =
766 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
768 let subst'',metasenv'',ugraph2 =
769 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
773 (fun (subst,metasenv,ugraph) t1 t2 ->
775 test_equality_only subst context metasenv t1 t2 ugraph
776 ) (subst'',metasenv'',ugraph2) pl1 pl2
778 Invalid_argument _ ->
779 raise (UnificationFailure (lazy "6.1")))
781 "Error trying to unify %s with %s: the number of branches is not the same."
782 (CicMetaSubst.ppterm ~metasenv subst t1)
783 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
784 | (C.Rel _, _) | (_, C.Rel _) ->
786 subst, metasenv,ugraph
788 raise (UnificationFailure (lazy
790 "Can't unify %s with %s because they are not convertible"
791 (CicMetaSubst.ppterm ~metasenv subst t1)
792 (CicMetaSubst.ppterm ~metasenv subst t2))))
793 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
794 let subst,metasenv,beta_expanded,ugraph1 =
796 test_equality_only metasenv subst context t2 args ugraph
798 fo_unif_subst test_equality_only subst context metasenv
799 (C.Meta (i,l)) beta_expanded ugraph1
800 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
801 let subst,metasenv,beta_expanded,ugraph1 =
803 test_equality_only metasenv subst context t1 args ugraph
805 fo_unif_subst test_equality_only subst context metasenv
806 beta_expanded (C.Meta (i,l)) ugraph1
807 (* Works iff there are no arguments applied to it; similar to the
810 let t1' = R.whd ~subst context t1 in
813 fo_unif_subst test_equality_only
814 subst context metasenv t1' t2 ugraph
815 | _ -> raise (UnificationFailure (lazy "8")))
817 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
818 let subst',metasenv',ugraph1 =
819 fo_unif_subst true subst context metasenv s1 s2 ugraph
821 fo_unif_subst test_equality_only
822 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
824 (match CicReduction.whd ~subst context t2 with
826 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
827 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
829 (match CicReduction.whd ~subst context t1 with
831 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
832 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
834 (* delta-beta reduction should almost never be a problem for
836 1. long computations require iota reduction
837 2. it is extremely rare that a close term t1 (that could be unified
838 to t2) beta-delta reduces to t1' while t2 does not beta-delta
839 reduces in the same way. This happens only if one meta of t2
840 occurs in head position during beta reduction. In this unluky
841 case too much reduction will be performed on t1 and unification
843 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
844 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
845 if t1 = t1' && t2 = t2' then
846 raise (UnificationFailure
849 "Can't unify %s with %s because they are not convertible"
850 (CicMetaSubst.ppterm ~metasenv subst t1)
851 (CicMetaSubst.ppterm ~metasenv subst t2))))
854 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
858 raise (UnificationFailure
861 "Can't unify %s with %s because they are not convertible"
862 (CicMetaSubst.ppterm ~metasenv subst t1)
863 (CicMetaSubst.ppterm ~metasenv subst t2))))
865 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
866 exp_named_subst1 exp_named_subst2 ugraph
870 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
872 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
873 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
875 Invalid_argument _ ->
880 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
883 raise (UnificationFailure (lazy (sprintf
884 "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))))
886 (* A substitution is a (int * Cic.term) list that associates a *)
887 (* metavariable i with its body. *)
888 (* metasenv is of type Cic.metasenv *)
889 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
890 (* a new substitution which is already unwinded and ready to be applied and *)
891 (* a new metasenv in which some hypothesis in the contexts of the *)
892 (* metavariables may have been restricted. *)
893 let fo_unif metasenv context t1 t2 ugraph =
894 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
896 let enrich_msg msg subst context metasenv t1 t2 ugraph =
899 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"
900 (CicMetaSubst.ppterm ~metasenv subst t1)
902 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
905 | UnificationFailure s
907 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
908 (CicMetaSubst.ppterm ~metasenv subst t2)
910 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
913 | UnificationFailure s
915 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
916 (CicMetaSubst.ppcontext ~metasenv subst context)
917 (CicMetaSubst.ppmetasenv subst metasenv)
918 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
920 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
921 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
923 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
924 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
926 | UnificationFailure s
928 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
929 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
931 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
932 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
934 | UnificationFailure s
936 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
937 (CicMetaSubst.ppcontext ~metasenv subst context)
938 (CicMetaSubst.ppmetasenv subst metasenv)
942 let fo_unif_subst subst context metasenv t1 t2 ugraph =
944 fo_unif_subst false subst context metasenv t1 t2 ugraph
946 | AssertFailure msg ->
947 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
948 | UnificationFailure msg ->
949 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))