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_______________________________________________________________ *)
14 exception UnificationFailure of string Lazy.t;;
15 exception Uncertain of string Lazy.t;;
16 exception AssertFailure of string Lazy.t;;
18 let (===) x y = Pervasives.compare x y = 0 ;;
20 let fail_exc metasenv subst context t1 t2 =
21 UnificationFailure (lazy (
22 "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
23 " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
26 let unify metasenv subst context t1 t2 =
27 (* are_convertible?? *)
28 let rec aux test_eq_only metasenv subst context t1 t2 =
29 let fo_unif test_eq_only t1 t2 =
34 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
35 if NCicEnvironment.universe_leq a b then metasenv, subst
36 else raise (fail_exc metasenv subst context t1 t2)
37 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
38 if NCicEnvironment.universe_eq a b then metasenv, subst
39 else raise (fail_exc metasenv subst context t1 t2)
40 | (C.Sort C.Prop,C.Sort (C.Type _)) ->
41 if (not test_eq_only) then metasenv, subst
42 else raise (fail_exc metasenv subst context t1 t2)
44 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
45 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
46 let metasenv, subst = aux true metasenv subst context s1 s2 in
47 aux test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
48 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
49 let metasenv,subst=aux test_eq_only metasenv subst context ty1 ty2 in
50 let metasenv,subst=aux test_eq_only metasenv subst context s1 s2 in
51 let context = (name1, C.Def (s1,ty1))::context in
52 aux test_eq_only metasenv subst context t1 t2
54 | (C.Meta (n1,(s1, C.Irl _)), C.Meta (n2,(s2, C.Irl _)))
55 when n1 = n2 && s1 = s2 -> true
56 | (C.Meta (n1,(s1, l1)), C.Meta (n2,(s2, l2))) when n1 = n2 &&
57 let l1 = NCicUtils.expand_local_context l1 in
58 let l2 = NCicUtils.expand_local_context l2 in
60 (fun t1 t2 -> aux test_eq_only context
61 (NCicSubstitution.lift s1 t1)
62 (NCicSubstitution.lift s2 t2))
64 with Invalid_argument _ -> assert false) -> true
66 | C.Meta (n1,l1), _ ->
68 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
69 let term = NCicSubstitution.subst_meta l1 term in
70 aux test_eq_only context term t2
71 with NCicUtils.Subst_not_found _ -> false)
72 | _, C.Meta (n2,l2) ->
74 let _,_,term,_ = NCicUtils.lookup_subst n2 subst in
75 let term = NCicSubstitution.subst_meta l2 term in
76 aux test_eq_only context t1 term
77 with NCicUtils.Subst_not_found _ -> false)
79 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
81 List.length (E.get_relevance r1) >= List.length tl1) ->
82 let relevance = E.get_relevance r1 in
83 let relevance = match r1 with
84 | Ref.Ref (_,Ref.Con (_,_,lno)) ->
85 let _,relevance = HExtlib.split_nth lno relevance in
86 HExtlib.mk_list false lno @ relevance
91 HExtlib.list_forall_default3
92 (fun t1 t2 b -> fail := !fail+1; not b || aux test_eq_only context t1 t2)
93 tl1 tl2 true relevance
94 with Invalid_argument _ -> false)
98 let relevance = get_relevance_p ~subst context _hd1 tl1 in
99 let _,relevance = HExtlib.split_nth !fail relevance in
100 let b,relevance = (match relevance with
103 let _,tl1 = HExtlib.split_nth (!fail+1) tl1 in
104 let _,tl2 = HExtlib.split_nth (!fail+1) tl2 in
108 HExtlib.list_forall_default3
109 (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
110 tl1 tl2 true relevance
111 with Invalid_argument _ -> false)
113 | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
114 aux test_eq_only context hd1 hd2 &&
115 let relevance = get_relevance ~subst context hd1 tl1 in
117 HExtlib.list_forall_default3
118 (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
119 tl1 tl2 true relevance
120 with Invalid_argument _ -> false)
122 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
123 C.Match (ref2,outtype2,term2,pl2)) ->
124 let _,_,itl,_,_ = E.get_checked_indtys ref1 in
125 let _,_,ty,_ = List.nth itl tyno in
126 let rec remove_prods ~subst context ty =
127 let ty = whd ~subst context ty in
130 | C.Prod (name,so,ta) ->
131 remove_prods ~subst ((name,(C.Decl so))::context) ta
135 match remove_prods ~subst [] ty with
136 | C.Sort C.Prop -> true
137 let rec remove_prods ~subst context ty =
138 let ty = whd ~subst context ty in
141 | C.Prod (name,so,ta) ->
142 remove_prods ~subst ((name,(C.Decl so))::context) ta
145 if not (Ref.eq ref1 ref2) then
146 raise (uncert_exc metasenv subst context t1 t2)
148 let metasenv, subst =
149 aux test_eq_only metasenv subst context outtype1 outtype2 in
150 let metasenv, subst =
151 try aux test_eq_only metasenv subst context term1 term2
152 with UnificationFailure _ | Uncertain _ when is_prop ->
157 (fun (metasenv,subst) -> aux test_eq_only metasenv subst context)
158 (metasenv, subst) pl1 pl2
159 with Invalid_argument _ ->
160 raise (uncert_exc metasenv subst context t1 t2)
161 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
162 | _ -> raise (uncert_exc metasenv subst context t1 t2)
164 let unif_machines ...
168 with Uncertain msg as exn ->
171 | UnificationFailure _ -> raise (UnificationFailure msg)
172 | Uncertain _ -> raise exn
174 aux false metasenv subst context t1 t2
176 let are_convertible ?(subst=[]) get_relevance =
177 let rec aux test_eq_only metasenv subst context t1 t2 =
179 if alpha_eq test_eq_only t1 t2 then
182 let height_of = function
183 | C.Const (Ref.Ref (_,Ref.Def h))
184 | C.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
185 | C.Appl(C.Const(Ref.Ref(_,Ref.Def h))::_)
186 | C.Appl(C.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
189 let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
190 let h1 = height_of t1 in
191 let h2 = height_of t2 in
192 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
193 R.reduce ~delta ~subst context m1,
194 R.reduce ~delta ~subst context m2,
197 let rec convert_machines ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) =
198 (alpha_eq test_eq_only
199 (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[])) &&
202 C.Const r -> NCicEnvironment.get_relevance r
205 HExtlib.list_forall_default3
208 let t1 = RS.from_stack t1 in
209 let t2 = RS.from_stack t2 in
210 convert_machines (small_delta_step t1 t2)) s1 s2 true relevance
211 with Invalid_argument _ -> false) ||
213 let delta = delta - 1 in
214 let red = R.reduce ~delta ~subst context in
215 convert_machines (red m1,red m2,delta))
217 convert_machines (small_delta_step (0,[],t1,[]) (0,[],t2,[]))
228 exception UnificationFailure of string Lazy.t;;
229 exception Uncertain of string Lazy.t;;
230 exception AssertFailure of string Lazy.t;;
232 let verbose = false;;
233 let debug_print = fun _ -> ()
235 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
236 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
237 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
238 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
240 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
242 let type_of_aux' metasenv subst context term ugraph =
245 profile.HExtlib.profile
246 (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
248 CicTypeChecker.TypeCheckerFailure msg ->
252 "Kernel Type checking error:
253 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
254 (CicMetaSubst.ppterm ~metasenv subst term)
255 (CicMetaSubst.ppterm ~metasenv [] term)
256 (CicMetaSubst.ppcontext ~metasenv subst context)
257 (CicMetaSubst.ppmetasenv subst metasenv)
258 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
259 raise (AssertFailure msg)
260 | CicTypeChecker.AssertFailure msg ->
263 "Kernel Type checking assertion failure:
264 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
265 (CicMetaSubst.ppterm ~metasenv subst term)
266 (CicMetaSubst.ppterm ~metasenv [] term)
267 (CicMetaSubst.ppcontext ~metasenv subst context)
268 (CicMetaSubst.ppmetasenv subst metasenv)
269 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
270 raise (AssertFailure msg)
271 in profiler_toa.HExtlib.profile foo ()
274 let exists_a_meta l =
278 | Cic.Appl (Cic.Meta _::_) -> true
281 let rec deref subst t =
282 let snd (_,a,_) = a in
287 (CicSubstitution.subst_meta
288 l (snd (CicUtil.lookup_subst n subst)))
290 CicUtil.Subst_not_found _ -> t)
291 | Cic.Appl(Cic.Meta(n,l)::args) ->
292 (match deref subst (Cic.Meta(n,l)) with
293 | Cic.Lambda _ as t ->
294 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
295 | r -> Cic.Appl(r::args))
296 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
297 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
302 let foo () = deref subst t
303 in profiler_deref.HExtlib.profile foo ()
305 exception WrongShape;;
306 let eta_reduce after_beta_expansion after_beta_expansion_body
307 before_beta_expansion
310 match before_beta_expansion,after_beta_expansion_body with
311 Cic.Appl l, Cic.Appl l' ->
312 let rec all_but_last check_last =
316 | [_] -> if check_last then raise WrongShape else []
317 | he::tl -> he::(all_but_last check_last tl)
319 let all_but_last check_last l =
320 match all_but_last check_last l with
325 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
326 let all_but_last = all_but_last false l in
327 (* here we should test alpha-equivalence; however we know by
328 construction that here alpha_equivalence is equivalent to = *)
329 if t = all_but_last then
333 | _,_ -> after_beta_expansion
335 WrongShape -> after_beta_expansion
337 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
338 let module S = CicSubstitution in
339 let module C = Cic in
341 let rec aux metasenv subst n context t' ugraph =
344 let subst,metasenv,ugraph1 =
345 fo_unif_subst test_equality_only subst context metasenv
346 (CicSubstitution.lift n arg) t' ugraph
349 subst,metasenv,C.Rel (1 + n),ugraph1
352 | UnificationFailure _ ->
354 | C.Rel m -> subst,metasenv,
355 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
356 | C.Var (uri,exp_named_subst) ->
357 let subst,metasenv,exp_named_subst',ugraph1 =
358 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
360 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
362 (* andrea: in general, beta_expand can create badly typed
363 terms. This happens quite seldom in practice, UNLESS we
364 iterate on the local context. For this reason, we renounce
365 to iterate and just lift *)
369 Some t -> Some (CicSubstitution.lift 1 t)
371 subst, metasenv, C.Meta (i,l), ugraph
373 | C.Implicit _ as t -> subst,metasenv,t,ugraph
375 let subst,metasenv,te',ugraph1 =
376 aux metasenv subst n context te ugraph in
377 let subst,metasenv,ty',ugraph2 =
378 aux metasenv subst n context ty ugraph1 in
379 (* TASSI: sure this is in serial? *)
380 subst,metasenv,(C.Cast (te', ty')),ugraph2
382 let subst,metasenv,s',ugraph1 =
383 aux metasenv subst n context s ugraph in
384 let subst,metasenv,t',ugraph2 =
385 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
388 (* TASSI: sure this is in serial? *)
389 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
390 | C.Lambda (nn,s,t) ->
391 let subst,metasenv,s',ugraph1 =
392 aux metasenv subst n context s ugraph in
393 let subst,metasenv,t',ugraph2 =
394 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
396 (* TASSI: sure this is in serial? *)
397 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
398 | C.LetIn (nn,s,ty,t) ->
399 let subst,metasenv,s',ugraph1 =
400 aux metasenv subst n context s ugraph in
401 let subst,metasenv,ty',ugraph1 =
402 aux metasenv subst n context ty ugraph in
403 let subst,metasenv,t',ugraph2 =
404 aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
407 (* TASSI: sure this is in serial? *)
408 subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
410 let subst,metasenv,revl',ugraph1 =
412 (fun (subst,metasenv,appl,ugraph) t ->
413 let subst,metasenv,t',ugraph1 =
414 aux metasenv subst n context t ugraph in
415 subst,metasenv,(t'::appl),ugraph1
416 ) (subst,metasenv,[],ugraph) l
418 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
419 | C.Const (uri,exp_named_subst) ->
420 let subst,metasenv,exp_named_subst',ugraph1 =
421 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
423 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
424 | C.MutInd (uri,i,exp_named_subst) ->
425 let subst,metasenv,exp_named_subst',ugraph1 =
426 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
428 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
429 | C.MutConstruct (uri,i,j,exp_named_subst) ->
430 let subst,metasenv,exp_named_subst',ugraph1 =
431 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
433 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
434 | C.MutCase (sp,i,outt,t,pl) ->
435 let subst,metasenv,outt',ugraph1 =
436 aux metasenv subst n context outt ugraph in
437 let subst,metasenv,t',ugraph2 =
438 aux metasenv subst n context t ugraph1 in
439 let subst,metasenv,revpl',ugraph3 =
441 (fun (subst,metasenv,pl,ugraph) t ->
442 let subst,metasenv,t',ugraph1 =
443 aux metasenv subst n context t ugraph in
444 subst,metasenv,(t'::pl),ugraph1
445 ) (subst,metasenv,[],ugraph2) pl
447 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
448 (* TASSI: not sure this is serial *)
450 (*CSC: not implemented
451 let tylen = List.length fl in
454 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
457 C.Fix (i, substitutedfl)
459 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
461 (*CSC: not implemented
462 let tylen = List.length fl in
465 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
468 C.CoFix (i, substitutedfl)
471 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
473 and aux_exp_named_subst metasenv subst n context ens ugraph =
475 (fun (uri,t) (subst,metasenv,l,ugraph) ->
476 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
477 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
479 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
481 FreshNamesGenerator.mk_fresh_name ~subst
482 metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
484 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
485 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
486 subst, metasenv, t'', ugraph2
487 in profiler_beta_expand.HExtlib.profile foo ()
490 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
491 let _,subst,metasenv,hd,ugraph =
493 (fun arg (num,subst,metasenv,t,ugraph) ->
494 let subst,metasenv,t,ugraph1 =
495 beta_expand num test_equality_only
496 metasenv subst context t arg ugraph
498 num+1,subst,metasenv,t,ugraph1
499 ) args (1,subst,metasenv,t,ugraph)
501 subst,metasenv,hd,ugraph
503 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
506 | (m2,_,c2,c2')::_ ->
507 let m1,c1,c1' = carr,to1,to2 in
509 function Some (_,t) -> CicPp.ppterm t
513 ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
514 CoercDb.string_of_carr car2^": " ^
515 CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
516 unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
517 unopt c2^" + "^unopt c2')
519 (* NUOVA UNIFICAZIONE *)
520 (* A substitution is a (int * Cic.term) list that associates a
521 metavariable i with its body.
522 A metaenv is a (int * Cic.term) list that associate a metavariable
524 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
525 a new substitution which is _NOT_ unwinded. It must be unwinded before
528 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
529 let module C = Cic in
530 let module R = CicReduction in
531 let module S = CicSubstitution in
532 let t1 = deref subst t1 in
533 let t2 = deref subst t2 in
534 let (&&&) a b = (a && b) || ((not a) && (not b)) in
535 (* let bef = Sys.time () in *)
537 if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
541 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
542 in profiler_are_convertible.HExtlib.profile foo ()
544 (* let aft = Sys.time () in
545 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
546 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
547 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
549 subst, metasenv, ugraph
552 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
553 let _,subst,metasenv,ugraph1 =
556 (fun (j,subst,metasenv,ugraph) t1 t2 ->
559 | _,None -> j+1,subst,metasenv,ugraph
560 | Some t1', Some t2' ->
561 (* First possibility: restriction *)
562 (* Second possibility: unification *)
563 (* Third possibility: convertibility *)
566 ~subst ~metasenv context t1' t2' ugraph
569 j+1,subst,metasenv, ugraph1
572 let subst,metasenv,ugraph2 =
575 subst context metasenv t1' t2' ugraph
577 j+1,subst,metasenv,ugraph2
580 | UnificationFailure _ ->
581 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
582 let metasenv, subst =
583 CicMetaSubst.restrict
584 subst [(n,j)] metasenv in
585 j+1,subst,metasenv,ugraph1)
586 ) (1,subst,metasenv,ugraph) ln lm
590 (UnificationFailure (lazy "1"))
593 "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."
594 (CicMetaSubst.ppterm ~metasenv subst t1)
595 (CicMetaSubst.ppterm ~metasenv subst t2))) *)
596 | Invalid_argument _ ->
598 (UnificationFailure (lazy "2")))
601 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
602 (CicMetaSubst.ppterm ~metasenv subst t1)
603 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
604 in subst,metasenv,ugraph1
605 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
606 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
608 | (t, C.Meta (n,l)) ->
611 C.Meta (n,_), C.Meta (m,_) when n < m -> false
612 | _, C.Meta _ -> false
615 let lower = fun x y -> if swap then y else x in
616 let upper = fun x y -> if swap then x else y in
617 let fo_unif_subst_ordered
618 test_equality_only subst context metasenv m1 m2 ugraph =
619 fo_unif_subst test_equality_only subst context metasenv
620 (lower m1 m2) (upper m1 m2) ugraph
623 let subst,metasenv,ugraph1 =
624 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
627 type_of_aux' metasenv subst context t ugraph
631 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
633 UnificationFailure _ as e -> raise e
634 | Uncertain msg -> raise (UnificationFailure msg)
636 debug_print (lazy "siamo allo huge hack");
637 (* TODO huge hack!!!!
638 * we keep on unifying/refining in the hope that
639 * the problem will be eventually solved.
640 * In the meantime we're breaking a big invariant:
641 * the terms that we are unifying are no longer well
642 * typed in the current context (in the worst case
643 * we could even diverge) *)
644 (subst, metasenv,ugraph)) in
645 let t',metasenv,subst =
647 CicMetaSubst.delift n subst context metasenv l t
649 (CicMetaSubst.MetaSubstFailure msg)->
650 raise (UnificationFailure msg)
651 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
655 C.Sort (C.Type u) when not test_equality_only ->
656 let u' = CicUniv.fresh () in
657 let s = C.Sort (C.Type u') in
660 CicUniv.add_ge (upper u u') (lower u u') ugraph1
664 CicUniv.UniverseInconsistency msg ->
665 raise (UnificationFailure msg))
668 (* Unifying the types may have already instantiated n. Let's check *)
670 let (_, oldt,_) = CicUtil.lookup_subst n subst in
671 let lifted_oldt = S.subst_meta l oldt in
672 fo_unif_subst_ordered
673 test_equality_only subst context metasenv t lifted_oldt ugraph2
675 CicUtil.Subst_not_found _ ->
676 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
677 let subst = (n, (context, t'',ty)) :: subst in
679 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
680 subst, metasenv, ugraph2
682 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
683 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
684 if UriManager.eq uri1 uri2 then
685 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
686 exp_named_subst1 exp_named_subst2 ugraph
688 raise (UnificationFailure (lazy
690 "Can't unify %s with %s due to different constants"
691 (CicMetaSubst.ppterm ~metasenv subst t1)
692 (CicMetaSubst.ppterm ~metasenv subst t2))))
693 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
694 if UriManager.eq uri1 uri2 && i1 = i2 then
695 fo_unif_subst_exp_named_subst
697 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
699 raise (UnificationFailure
702 "Can't unify %s with %s due to different inductive principles"
703 (CicMetaSubst.ppterm ~metasenv subst t1)
704 (CicMetaSubst.ppterm ~metasenv subst t2))))
705 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
706 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
707 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
708 fo_unif_subst_exp_named_subst
710 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
712 raise (UnificationFailure
715 "Can't unify %s with %s due to different inductive constructors"
716 (CicMetaSubst.ppterm ~metasenv subst t1)
717 (CicMetaSubst.ppterm ~metasenv subst t2))))
718 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
719 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
720 subst context metasenv te t2 ugraph
721 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
722 subst context metasenv t1 te ugraph
723 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
724 let subst',metasenv',ugraph1 =
725 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
727 fo_unif_subst test_equality_only
728 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
729 | (C.LetIn (_,s1,ty1,t1), t2)
730 | (t2, C.LetIn (_,s1,ty1,t1)) ->
732 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
733 | (C.Appl l1, C.Appl l2) ->
734 (* andrea: this case should be probably rewritten in the
737 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
740 (fun (subst,metasenv,ugraph) t1 t2 ->
742 test_equality_only subst context metasenv t1 t2 ugraph)
743 (subst,metasenv,ugraph) l1 l2
744 with (Invalid_argument msg) ->
745 raise (UnificationFailure (lazy msg)))
746 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
747 (* we verify that none of the args is a Meta,
748 since beta expanding with respoect to a metavariable
752 let (_,t,_) = CicUtil.lookup_subst i subst in
753 let lifted = S.subst_meta l t in
754 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
757 subst context metasenv reduced t2 ugraph
758 with CicUtil.Subst_not_found _ -> *)
759 let subst,metasenv,beta_expanded,ugraph1 =
761 test_equality_only metasenv subst context t2 args ugraph
763 fo_unif_subst test_equality_only subst context metasenv
764 (C.Meta (i,l)) beta_expanded ugraph1
765 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
767 let (_,t,_) = CicUtil.lookup_subst i subst in
768 let lifted = S.subst_meta l t in
769 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
772 subst context metasenv t1 reduced ugraph
773 with CicUtil.Subst_not_found _ -> *)
774 let subst,metasenv,beta_expanded,ugraph1 =
777 metasenv subst context t1 args ugraph
779 fo_unif_subst test_equality_only subst context metasenv
780 (C.Meta (i,l)) beta_expanded ugraph1
782 let lr1 = List.rev l1 in
783 let lr2 = List.rev l2 in
785 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
788 | _,[] -> assert false
791 test_equality_only subst context metasenv h1 h2 ugraph
794 fo_unif_subst test_equality_only subst context metasenv
795 h (C.Appl (List.rev l)) ugraph
796 | ((h1::l1),(h2::l2)) ->
797 let subst', metasenv',ugraph1 =
800 subst context metasenv h1 h2 ugraph
803 test_equality_only subst' metasenv' (l1,l2) ugraph1
807 test_equality_only subst metasenv (lr1, lr2) ugraph
809 | UnificationFailure s
810 | Uncertain s as exn ->
813 | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
814 (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
815 CoercDb.is_a_coercion cc1 <> None &&
816 CoercDb.is_a_coercion cc2 <> None &&
817 not (UriManager.eq uri1 uri2) ->
819 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
821 let inner_coerced t =
822 let t = CicMetaSubst.apply_subst subst t in
826 (match CoercGraph.coerced_arg l with
828 | Some (t,_) -> aux (List.hd l) t t)
831 aux (Cic.Implicit None) (Cic.Implicit None) t
833 let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
834 let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
837 CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
839 | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
842 let head1_c, head2_c =
844 CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
846 | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
849 let unfold uri ens args =
851 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
855 | Cic.Constant (_,Some bo,_,_,_) ->
856 CicReduction.head_beta_reduce ~delta:false
857 (Cic.Appl (bo::args))
860 let conclude subst metasenv ugraph last_tl1' last_tl2' =
861 let subst',metasenv,ugraph =
864 ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
865 " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
867 fo_unif_subst test_equality_only subst context
868 metasenv last_tl1' last_tl2' ugraph
870 if subst = subst' then raise exn
873 let subst,metasenv,ugrph as res =
875 fo_unif_subst test_equality_only subst' context
876 metasenv (C.Appl l1) (C.Appl l2) ugraph
880 (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
881 " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
885 if CoercDb.eq_carr car1 car2 then
886 match last_tl1,last_tl2 with
887 | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
890 let subst,metasenv,ugraph =
891 fo_unif_subst test_equality_only subst context
892 metasenv last_tl1 last_tl2 ugraph
894 fo_unif_subst test_equality_only subst context
895 metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
896 | _ when CoercDb.eq_carr head1_c head2_c ->
897 (* composite VS composition + metas avoiding
898 * coercions not only in coerced position *)
899 if c1 <> cc1 && c2 <> cc2 then
900 conclude subst metasenv ugraph
905 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
907 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
909 fo_unif_subst test_equality_only subst context
910 metasenv l1 l2 ugraph
914 match last_tl1 with Cic.Meta _ -> true | _ -> false in
916 match last_tl2 with Cic.Meta _ -> true | _ -> false in
917 if not (grow1 || grow2) then
918 (* no flexible terminals -> no pullback, but
919 * we still unify them, in some cases it helps *)
920 conclude subst metasenv ugraph last_tl1 last_tl2
924 metasenv subst context (grow1,car1) (grow2,car2)
928 | (carr,metasenv,to1,to2)::xxx ->
929 warn_if_not_unique xxx to1 to2 carr car1 car2;
930 let last_tl1',(subst,metasenv,ugraph) =
932 | true,Some (last,coerced) ->
934 fo_unif_subst test_equality_only subst context
935 metasenv coerced last_tl1 ugraph
936 | _ -> last_tl1,(subst,metasenv,ugraph)
938 let last_tl2',(subst,metasenv,ugraph) =
940 | true,Some (last,coerced) ->
942 fo_unif_subst test_equality_only subst context
943 metasenv coerced last_tl2 ugraph
944 | _ -> last_tl2,(subst,metasenv,ugraph)
946 conclude subst metasenv ugraph last_tl1' last_tl2')
948 (* {{{ CSC: This is necessary because of the "elim H" tactic
949 where the type of H is only reducible to an
950 inductive type. This could be extended from inductive
951 types to any rigid term. However, the code is
952 duplicated in two places: inside applications and
953 outside them. Probably it would be better to
954 work with lambda-bar terms instead. *)
955 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
956 | (_, Cic.MutInd _::_) ->
957 let t1' = R.whd ~subst context t1 in
959 C.Appl (C.MutInd _::_) ->
960 fo_unif_subst test_equality_only
961 subst context metasenv t1' t2 ugraph
962 | _ -> raise (UnificationFailure (lazy "88")))
963 | (Cic.MutInd _::_,_) ->
964 let t2' = R.whd ~subst context t2 in
966 C.Appl (C.MutInd _::_) ->
967 fo_unif_subst test_equality_only
968 subst context metasenv t1 t2' ugraph
971 (lazy ("not a mutind :"^
972 CicMetaSubst.ppterm ~metasenv subst t2 ))))
975 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
976 let subst', metasenv',ugraph1 =
977 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
979 let subst'',metasenv'',ugraph2 =
980 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
984 (fun (subst,metasenv,ugraph) t1 t2 ->
986 test_equality_only subst context metasenv t1 t2 ugraph
987 ) (subst'',metasenv'',ugraph2) pl1 pl2
989 Invalid_argument _ ->
990 raise (UnificationFailure (lazy "6.1")))
992 "Error trying to unify %s with %s: the number of branches is not the same."
993 (CicMetaSubst.ppterm ~metasenv subst t1)
994 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
995 | (C.Rel _, _) | (_, C.Rel _) ->
997 subst, metasenv,ugraph
999 raise (UnificationFailure (lazy
1001 "Can't unify %s with %s because they are not convertible"
1002 (CicMetaSubst.ppterm ~metasenv subst t1)
1003 (CicMetaSubst.ppterm ~metasenv subst t2))))
1004 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
1005 let subst,metasenv,beta_expanded,ugraph1 =
1007 test_equality_only metasenv subst context t2 args ugraph
1009 fo_unif_subst test_equality_only subst context metasenv
1010 (C.Meta (i,l)) beta_expanded ugraph1
1011 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
1012 let subst,metasenv,beta_expanded,ugraph1 =
1014 test_equality_only metasenv subst context t1 args ugraph
1016 fo_unif_subst test_equality_only subst context metasenv
1017 beta_expanded (C.Meta (i,l)) ugraph1
1018 (* Works iff there are no arguments applied to it; similar to the
1020 | (_, C.MutInd _) ->
1021 let t1' = R.whd ~subst context t1 in
1024 fo_unif_subst test_equality_only
1025 subst context metasenv t1' t2 ugraph
1026 | _ -> raise (UnificationFailure (lazy "8")))
1028 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
1029 let subst',metasenv',ugraph1 =
1030 fo_unif_subst true subst context metasenv s1 s2 ugraph
1032 fo_unif_subst test_equality_only
1033 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1035 (match CicReduction.whd ~subst context t2 with
1037 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1038 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
1040 (match CicReduction.whd ~subst context t1 with
1042 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1043 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
1045 (* delta-beta reduction should almost never be a problem for
1047 1. long computations require iota reduction
1048 2. it is extremely rare that a close term t1 (that could be unified
1049 to t2) beta-delta reduces to t1' while t2 does not beta-delta
1050 reduces in the same way. This happens only if one meta of t2
1051 occurs in head position during beta reduction. In this unluky
1052 case too much reduction will be performed on t1 and unification
1053 will surely fail. *)
1054 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
1055 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
1056 if t1 = t1' && t2 = t2' then
1057 raise (UnificationFailure
1060 "Can't unify %s with %s because they are not convertible"
1061 (CicMetaSubst.ppterm ~metasenv subst t1)
1062 (CicMetaSubst.ppterm ~metasenv subst t2))))
1065 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
1067 UnificationFailure _
1069 raise (UnificationFailure
1072 "Can't unify %s with %s because they are not convertible"
1073 (CicMetaSubst.ppterm ~metasenv subst t1)
1074 (CicMetaSubst.ppterm ~metasenv subst t2))))
1076 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
1077 exp_named_subst1 exp_named_subst2 ugraph
1081 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
1082 assert (uri1=uri2) ;
1083 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1084 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
1086 Invalid_argument _ ->
1091 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
1094 raise (UnificationFailure (lazy (sprintf
1095 "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))))
1097 (* A substitution is a (int * Cic.term) list that associates a *)
1098 (* metavariable i with its body. *)
1099 (* metasenv is of type Cic.metasenv *)
1100 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
1101 (* a new substitution which is already unwinded and ready to be applied and *)
1102 (* a new metasenv in which some hypothesis in the contexts of the *)
1103 (* metavariables may have been restricted. *)
1104 let fo_unif metasenv context t1 t2 ugraph =
1105 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
1107 let enrich_msg msg subst context metasenv t1 t2 ugraph =
1110 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"
1111 (CicMetaSubst.ppterm ~metasenv subst t1)
1113 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1116 | UnificationFailure s
1118 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1119 (CicMetaSubst.ppterm ~metasenv subst t2)
1121 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1124 | UnificationFailure s
1126 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1127 (CicMetaSubst.ppcontext ~metasenv subst context)
1128 (CicMetaSubst.ppmetasenv subst metasenv)
1129 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
1131 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
1132 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
1134 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1135 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
1137 | UnificationFailure s
1139 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1140 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
1142 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1143 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
1145 | UnificationFailure s
1147 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1148 (CicMetaSubst.ppcontext ~metasenv subst context)
1149 (CicMetaSubst.ppmetasenv subst metasenv)
1153 let fo_unif_subst subst context metasenv t1 t2 ugraph =
1155 fo_unif_subst false subst context metasenv t1 t2 ugraph
1157 | AssertFailure msg ->
1158 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1159 | UnificationFailure msg ->
1160 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))