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
323 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
324 in profiler_are_convertible.HExtlib.profile foo ()
327 subst, metasenv, ugraph
330 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
331 let _,subst,metasenv,ugraph1 =
334 (fun (j,subst,metasenv,ugraph) t1 t2 ->
337 | _,None -> j+1,subst,metasenv,ugraph
338 | Some t1', Some t2' ->
339 (* First possibility: restriction *)
340 (* Second possibility: unification *)
341 (* Third possibility: convertibility *)
344 ~subst ~metasenv context t1' t2' ugraph
347 j+1,subst,metasenv, ugraph1
350 let subst,metasenv,ugraph2 =
353 subst context metasenv t1' t2' ugraph
355 j+1,subst,metasenv,ugraph2
358 | UnificationFailure _ ->
359 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
360 let metasenv, subst =
361 CicMetaSubst.restrict
362 subst [(n,j)] metasenv in
363 j+1,subst,metasenv,ugraph1)
364 ) (1,subst,metasenv,ugraph) ln lm
368 (UnificationFailure (lazy "1"))
371 "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."
372 (CicMetaSubst.ppterm ~metasenv subst t1)
373 (CicMetaSubst.ppterm ~metasenv subst t2))) *)
374 | Invalid_argument _ ->
376 (UnificationFailure (lazy "2")))
379 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
380 (CicMetaSubst.ppterm ~metasenv subst t1)
381 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
382 in subst,metasenv,ugraph1
383 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
384 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
386 | (t, C.Meta (n,l)) ->
389 C.Meta (n,_), C.Meta (m,_) when n < m -> false
390 | _, C.Meta _ -> false
393 let lower = fun x y -> if swap then y else x in
394 let upper = fun x y -> if swap then x else y in
395 let fo_unif_subst_ordered
396 test_equality_only subst context metasenv m1 m2 ugraph =
397 fo_unif_subst test_equality_only subst context metasenv
398 (lower m1 m2) (upper m1 m2) ugraph
401 let subst,metasenv,ugraph1 =
402 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
405 type_of_aux' metasenv subst context t ugraph
409 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
411 UnificationFailure _ as e -> raise e
412 | Uncertain msg -> raise (UnificationFailure msg)
414 debug_print (lazy "siamo allo huge hack");
415 (* TODO huge hack!!!!
416 * we keep on unifying/refining in the hope that
417 * the problem will be eventually solved.
418 * In the meantime we're breaking a big invariant:
419 * the terms that we are unifying are no longer well
420 * typed in the current context (in the worst case
421 * we could even diverge) *)
422 (subst, metasenv,ugraph)) in
423 let t',metasenv,subst =
425 CicMetaSubst.delift n subst context metasenv l t
427 (CicMetaSubst.MetaSubstFailure msg)->
428 raise (UnificationFailure msg)
429 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
433 C.Sort (C.Type u) when not test_equality_only ->
434 let u' = CicUniv.fresh () in
435 let s = C.Sort (C.Type u') in
438 CicUniv.add_ge (upper u u') (lower u u') ugraph1
442 CicUniv.UniverseInconsistency msg ->
443 raise (UnificationFailure msg))
446 (* Unifying the types may have already instantiated n. Let's check *)
448 let (_, oldt,_) = CicUtil.lookup_subst n subst in
449 let lifted_oldt = S.subst_meta l oldt in
450 fo_unif_subst_ordered
451 test_equality_only subst context metasenv t lifted_oldt ugraph2
453 CicUtil.Subst_not_found _ ->
454 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
455 let subst = (n, (context, t'',ty)) :: subst in
457 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
458 subst, metasenv, ugraph2
460 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
461 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
462 if UriManager.eq uri1 uri2 then
463 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
464 exp_named_subst1 exp_named_subst2 ugraph
466 raise (UnificationFailure (lazy
468 "Can't unify %s with %s due to different constants"
469 (CicMetaSubst.ppterm ~metasenv subst t1)
470 (CicMetaSubst.ppterm ~metasenv subst t2))))
471 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
472 if UriManager.eq uri1 uri2 && i1 = i2 then
473 fo_unif_subst_exp_named_subst
475 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
477 raise (UnificationFailure
480 "Can't unify %s with %s due to different inductive principles"
481 (CicMetaSubst.ppterm ~metasenv subst t1)
482 (CicMetaSubst.ppterm ~metasenv subst t2))))
483 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
484 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
485 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
486 fo_unif_subst_exp_named_subst
488 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
490 raise (UnificationFailure
493 "Can't unify %s with %s due to different inductive constructors"
494 (CicMetaSubst.ppterm ~metasenv subst t1)
495 (CicMetaSubst.ppterm ~metasenv subst t2))))
496 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
497 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
498 subst context metasenv te t2 ugraph
499 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
500 subst context metasenv t1 te ugraph
501 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
502 let subst',metasenv',ugraph1 =
503 fo_unif_subst true subst context metasenv s1 s2 ugraph
505 fo_unif_subst test_equality_only
506 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
507 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
508 let subst',metasenv',ugraph1 =
509 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
511 fo_unif_subst test_equality_only
512 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
513 | (C.LetIn (_,s1,ty1,t1), t2)
514 | (t2, C.LetIn (_,s1,ty1,t1)) ->
516 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
517 | (C.Appl l1, C.Appl l2) ->
518 (* andrea: this case should be probably rewritten in the
521 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
524 (fun (subst,metasenv,ugraph) t1 t2 ->
526 test_equality_only subst context metasenv t1 t2 ugraph)
527 (subst,metasenv,ugraph) l1 l2
528 with (Invalid_argument msg) ->
529 raise (UnificationFailure (lazy msg)))
530 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
531 (* we verify that none of the args is a Meta,
532 since beta expanding with respoect to a metavariable
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 reduced t2 ugraph
542 with CicUtil.Subst_not_found _ -> *)
543 let subst,metasenv,beta_expanded,ugraph1 =
545 test_equality_only metasenv subst context t2 args ugraph
547 fo_unif_subst test_equality_only subst context metasenv
548 (C.Meta (i,l)) beta_expanded ugraph1
549 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
551 let (_,t,_) = CicUtil.lookup_subst i subst in
552 let lifted = S.subst_meta l t in
553 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
556 subst context metasenv t1 reduced ugraph
557 with CicUtil.Subst_not_found _ -> *)
558 let subst,metasenv,beta_expanded,ugraph1 =
561 metasenv subst context t1 args ugraph
563 fo_unif_subst test_equality_only subst context metasenv
564 (C.Meta (i,l)) beta_expanded ugraph1
566 let lr1 = List.rev l1 in
567 let lr2 = List.rev l2 in
569 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
572 | _,[] -> assert false
575 test_equality_only subst context metasenv h1 h2 ugraph
578 fo_unif_subst test_equality_only subst context metasenv
579 h (C.Appl (List.rev l)) ugraph
580 | ((h1::l1),(h2::l2)) ->
581 let subst', metasenv',ugraph1 =
584 subst context metasenv h1 h2 ugraph
587 test_equality_only subst' metasenv' (l1,l2) ugraph1
591 test_equality_only subst metasenv (lr1, lr2) ugraph
593 | UnificationFailure s
594 | Uncertain s as exn ->
596 | (((Cic.Const (uri1, ens1)) as c1) :: tl1),
597 (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
598 CoercDb.is_a_coercion' c1 &&
599 CoercDb.is_a_coercion' c2 &&
600 not (UriManager.eq uri1 uri2) ->
602 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
605 let rec look_for_first_coercion c tl =
607 CicMetaSubst.apply_subst subst (HExtlib.list_last tl)
609 Cic.Appl ((Cic.Const (uri1,ens1) as c')::tl')
610 when CoercDb.is_a_coercion' c' ->
611 look_for_first_coercion c' tl'
612 | last_tl -> c,last_tl
614 let c1,last_tl1 = look_for_first_coercion c1 tl1 in
615 let c2,last_tl2 = look_for_first_coercion c2 tl2 in
617 CoercDb.coerc_carr_of_term (CoercGraph.source_of c1) in
619 CoercDb.coerc_carr_of_term (CoercGraph.source_of c2) in
620 if CoercDb.eq_carr car1 car2 then
621 (match last_tl1,last_tl2 with
622 C.Meta (i1,_),C.Meta(i2,_) when i1=i2 -> raise exn
625 let subst,metasenv,ugraph =
626 fo_unif_subst test_equality_only subst context
627 metasenv last_tl1 last_tl2 ugraph
629 fo_unif_subst test_equality_only subst context
630 metasenv (C.Appl l1) (C.Appl l2) ugraph
634 CoercGraph.meets metasenv subst context car1 car2
638 | (carr,metasenv,to1,to2)::xxx ->
641 | (m2,_,c2,c2')::_ ->
642 let m1,_,c1,c1' = carr,metasenv,to1,to2 in
644 function Some (_,t) -> CicPp.ppterm t
648 ("There are two minimal joins of "^
649 CoercDb.name_of_carr car1^" and "^
650 CoercDb.name_of_carr car2^": " ^
651 CoercDb.name_of_carr m1 ^ " via "^unopt c1^" + "^
652 unopt c1'^" and " ^ CoercDb.name_of_carr m2^" via "^
653 unopt c2^" + "^unopt c2'));
654 let last_tl1',(subst,metasenv,ugraph) =
655 match last_tl1,to1 with
656 | Cic.Meta (i1,l1),Some (last,coerced) ->
658 fo_unif_subst test_equality_only subst context
659 metasenv coerced last_tl1 ugraph
660 | _ -> last_tl1,(subst,metasenv,ugraph)
662 let last_tl2',(subst,metasenv,ugraph) =
663 match last_tl2,to2 with
664 | Cic.Meta (i2,l2),Some (last,coerced) ->
666 fo_unif_subst test_equality_only subst context
667 metasenv coerced last_tl2 ugraph
668 | _ -> last_tl2,(subst,metasenv,ugraph)
671 prerr_endline ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
673 let subst,metasenv,ugraph =
674 fo_unif_subst test_equality_only subst context
675 metasenv last_tl1' last_tl2' ugraph
677 fo_unif_subst test_equality_only subst context
678 metasenv (C.Appl l1) (C.Appl l2) ugraph)
681 let subst,metasenv,ugraph = res in
682 prerr_endline (">>>> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
685 (*CSC: This is necessary because of the "elim H" tactic
686 where the type of H is only reducible to an
687 inductive type. This could be extended from inductive
688 types to any rigid term. However, the code is
689 duplicated in two places: inside applications and
690 outside them. Probably it would be better to
691 work with lambda-bar terms instead. *)
692 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
693 | (_, Cic.MutInd _::_) ->
694 let t1' = R.whd ~subst context t1 in
696 C.Appl (C.MutInd _::_) ->
697 fo_unif_subst test_equality_only
698 subst context metasenv t1' t2 ugraph
699 | _ -> raise (UnificationFailure (lazy "88")))
700 | (Cic.MutInd _::_,_) ->
701 let t2' = R.whd ~subst context t2 in
703 C.Appl (C.MutInd _::_) ->
704 fo_unif_subst test_equality_only
705 subst context metasenv t1 t2' ugraph
708 (lazy ("not a mutind :"^CicMetaSubst.ppterm ~metasenv subst t2 ))))
710 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
711 let subst', metasenv',ugraph1 =
712 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
714 let subst'',metasenv'',ugraph2 =
715 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
719 (fun (subst,metasenv,ugraph) t1 t2 ->
721 test_equality_only subst context metasenv t1 t2 ugraph
722 ) (subst'',metasenv'',ugraph2) pl1 pl2
724 Invalid_argument _ ->
725 raise (UnificationFailure (lazy "6.1")))
727 "Error trying to unify %s with %s: the number of branches is not the same."
728 (CicMetaSubst.ppterm ~metasenv subst t1)
729 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
730 | (C.Rel _, _) | (_, C.Rel _) ->
732 subst, metasenv,ugraph
734 raise (UnificationFailure (lazy
736 "Can't unify %s with %s because they are not convertible"
737 (CicMetaSubst.ppterm ~metasenv subst t1)
738 (CicMetaSubst.ppterm ~metasenv subst t2))))
739 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
740 let subst,metasenv,beta_expanded,ugraph1 =
742 test_equality_only metasenv subst context t2 args ugraph
744 fo_unif_subst test_equality_only subst context metasenv
745 (C.Meta (i,l)) beta_expanded ugraph1
746 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
747 let subst,metasenv,beta_expanded,ugraph1 =
749 test_equality_only metasenv subst context t1 args ugraph
751 fo_unif_subst test_equality_only subst context metasenv
752 beta_expanded (C.Meta (i,l)) ugraph1
753 (* Works iff there are no arguments applied to it; similar to the
756 let t1' = R.whd ~subst context t1 in
759 fo_unif_subst test_equality_only
760 subst context metasenv t1' t2 ugraph
761 | _ -> raise (UnificationFailure (lazy "8")))
763 (* The following idea could be exploited again; right now we have no
764 longer any example requiring it
766 let t2' = R.whd ~subst context t2 in
769 fo_unif_subst test_equality_only
770 subst context metasenv t1 t2' ugraph
771 | _ -> raise (UnificationFailure (lazy "8")))
773 let t1' = R.whd ~subst context t1 in
776 fo_unif_subst test_equality_only
777 subst context metasenv t1' t2 ugraph
778 | _ -> (* raise (UnificationFailure "9")) *)
780 (UnificationFailure (lazy (sprintf
781 "Can't unify %s with %s because they are not convertible"
782 (CicMetaSubst.ppterm ~metasenv subst t1)
783 (CicMetaSubst.ppterm ~metasenv subst t2)))))
786 (* delta-beta reduction should almost never be a problem for
788 1. long computations require iota reduction
789 2. it is extremely rare that a close term t1 (that could be unified
790 to t2) beta-delta reduces to t1' while t2 does not beta-delta
791 reduces in the same way. This happens only if one meta of t2
792 occurs in head position during beta reduction. In this unluky
793 case too much reduction will be performed on t1 and unification
795 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
796 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
797 if t1 = t1' && t2 = t2' then
798 raise (UnificationFailure
801 "Can't unify %s with %s because they are not convertible"
802 (CicMetaSubst.ppterm ~metasenv subst t1)
803 (CicMetaSubst.ppterm ~metasenv subst t2))))
806 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
810 raise (UnificationFailure
813 "Can't unify %s with %s because they are not convertible"
814 (CicMetaSubst.ppterm ~metasenv subst t1)
815 (CicMetaSubst.ppterm ~metasenv subst t2))))
817 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
818 exp_named_subst1 exp_named_subst2 ugraph
822 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
824 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
825 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
827 Invalid_argument _ ->
832 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
835 raise (UnificationFailure (lazy (sprintf
836 "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))))
838 (* A substitution is a (int * Cic.term) list that associates a *)
839 (* metavariable i with its body. *)
840 (* metasenv is of type Cic.metasenv *)
841 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
842 (* a new substitution which is already unwinded and ready to be applied and *)
843 (* a new metasenv in which some hypothesis in the contexts of the *)
844 (* metavariables may have been restricted. *)
845 let fo_unif metasenv context t1 t2 ugraph =
846 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
848 let enrich_msg msg subst context metasenv t1 t2 ugraph =
851 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"
852 (CicMetaSubst.ppterm ~metasenv subst t1)
854 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
857 | UnificationFailure s
859 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
860 (CicMetaSubst.ppterm ~metasenv subst t2)
862 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
865 | UnificationFailure s
867 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
868 (CicMetaSubst.ppcontext ~metasenv subst context)
869 (CicMetaSubst.ppmetasenv subst metasenv)
870 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
872 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
873 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
875 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
876 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
878 | UnificationFailure s
880 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
881 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
883 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
884 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
886 | UnificationFailure s
888 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
889 (CicMetaSubst.ppcontext ~metasenv subst context)
890 (CicMetaSubst.ppmetasenv subst metasenv)
894 let fo_unif_subst subst context metasenv t1 t2 ugraph =
896 fo_unif_subst false subst context metasenv t1 t2 ugraph
898 | AssertFailure msg ->
899 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
900 | UnificationFailure msg ->
901 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))