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))
28 | NCic.Appl l -> NCic.Appl (l@tl)
29 | _ -> NCic.Appl (hd :: tl)
36 | NCic.Appl (NCic.Meta _::_) -> true
40 exception WrongShape;;
42 let eta_reduce after_beta_expansion after_beta_expansion_body
46 match before_beta_expansion,after_beta_expansion_body with
47 | NCic.Appl l1, NCic.Appl l2 ->
48 let rec all_but_last check_last = function
51 | [_] -> if check_last then raise WrongShape else []
52 | he::tl -> he::(all_but_last check_last tl)
54 let all_but_last check_last l =
55 match all_but_last check_last l with
61 NCicSubstitution.subst (NCic.Sort NCic.Prop) (all_but_last true l2) in
62 let all_but_last = all_but_last false l in
63 if t = all_but_last then all_but_last else after_beta_expansion
64 | _ -> after_beta_expansion
65 with WrongShape -> after_beta_expansion
68 let rec beta_expand num test_equality_only metasenv subst context t arg =
69 let rec aux (n,context as k) (metasenv, subst as acc) t' =
72 unify (* test_equality_only *) metasenv subst context
73 (NCicSubstitution.lift n arg) t'
75 (metasenv, subst), C.Rel (1 + n)
76 with Uncertain _ | UnificationFailure _ ->
79 (metasenv, subst), if m <= n then NCic.Rel m else NCic.Rel (m+1)
80 (* andrea: in general, beta_expand can create badly typed
81 terms. This happens quite seldom in practice, UNLESS we
82 iterate on the local context. For this reason, we renounce
83 to iterate and just lift *)
84 | NCic.Meta (i,(shift,lc)) ->
85 (metasenv,subst), NCic.Meta (i,(shift+1,lc))
87 NCicUntrusted.map_term_fold_a
88 (fun e (n,ctx) -> n+i,e::ctx) k aux acc t
91 let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
92 let fresh_name = "Hbeta" ^ string_of_int num in
93 let (metasenv,subst), t = aux (0, context) (metasenv, subst) t in
94 let t = eta_reduce (C.Lambda (fresh_name,argty,t)) t t in
97 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
98 let _, subst, metasenv, hd =
100 (fun arg (num,subst,metasenv,t) ->
101 let subst, metasenv, t =
102 beta_expand num test_equality_only metasenv subst context t arg
104 num+1,subst,metasenv,t)
105 args (1,subst,metasenv,t)
109 and instantiate test_eq_only metasenv subst context n lc t swap =
110 let unif m s c t1 t2 =
111 if swap then unify m s c t2 t1 else unify m s c t1 t2
114 try NCicTypeChecker.typeof ~subst ~metasenv context t
115 with NCicTypeChecker.TypeCheckerFailure _ -> assert false
117 let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
118 let ty = NCicSubstitution.subst_meta lc ty in
119 let metasenv, subst = unify metasenv susbt context ty ty_t in
120 let (metasenv, subst), t =
121 NCicMetaSubst.delift metasenv subst context n lc t
123 (* Unifying the types may have already instantiated n. *)
125 let _, _,oldt,_ = CicUtil.lookup_subst n subst in
126 let oldt = NCicSubstitution.subst_meta lc oldt in
127 (* conjecture: always fail --> occur check *)
128 unify test_eq_only metasenv subst context oldt t
129 with CicUtil.Subst_not_found _ ->
130 (* by cumulativity when unify(?,Type_i)
131 * we could ? := Type_j with j <= i... *)
132 let subst = (n, (name, ctx, t, ty)) :: subst in
134 List.filter (fun (m,_) -> not (n = m)) metasenv
138 and unify metasenv subst context t1 t2 =
139 let rec aux test_eq_only metasenv subst context t1 t2 =
140 let fo_unif test_eq_only metasenv subst t1 t2 =
145 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
146 if NCicEnvironment.universe_leq a b then metasenv, subst
147 else raise (fail_exc metasenv subst context t1 t2)
148 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
149 if NCicEnvironment.universe_eq a b then metasenv, subst
150 else raise (fail_exc metasenv subst context t1 t2)
151 | (C.Sort C.Prop,C.Sort (C.Type _)) ->
152 if (not test_eq_only) then metasenv, subst
153 else raise (fail_exc metasenv subst context t1 t2)
155 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
156 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
157 let metasenv, subst = aux true metasenv subst context s1 s2 in
158 aux test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
159 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
160 let metasenv,subst=aux test_eq_only metasenv subst context ty1 ty2 in
161 let metasenv,subst=aux test_eq_only metasenv subst context s1 s2 in
162 let context = (name1, C.Def (s1,ty1))::context in
163 aux test_eq_only metasenv subst context t1 t2
165 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
167 let l1 = NCicUtils.expand_local_context l1 in
168 let l2 = NCicUtils.expand_local_context l2 in
169 let metasenv, subst, to_restrict, _ =
171 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
173 aux test_eq_only metasenv subst context
174 (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2),
176 with UnificationFailure _ | Uncertain _ ->
177 metasenv, subst, i::to_restrict, i-1)
178 l1 l2 (metasenv, subst, [], List.length l1)
180 let metasenv, subst, _ =
181 NCicMetaSubst.restrict metasenv subst n1 to_restrict
185 | Invalid_argument _ -> assert false
186 | NCicMetaSubst.MetaSubstFailure msg ->
188 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
189 let term1 = NCicSubstitution.subst_meta lc1 term in
190 let term2 = NCicSubstitution.subst_meta lc2 term in
191 aux test_eq_only metasenv subst context term1 term2
192 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
194 | C.Meta (n,lc), t ->
196 let _,_,term,_ = NCicUtils.lookup_subst n subst in
197 let term = NCicSubstitution.subst_meta lc term in
198 aux test_eq_only metasenv subst context term t
199 with NCicUtils.Subst_not_found _->
200 instantiate test_eq_only metasenv subst context n lc t false
202 | t, C.Meta (n,lc) ->
204 let _,_,term,_ = NCicUtils.lookup_subst n subst in
205 let term = NCicSubstitution.subst_meta lc term in
206 aux test_eq_only metasenv subst context t term
207 with NCicUtils.Subst_not_found _->
208 instantiate test_eq_only metasenv subst context n lc t true
210 | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
211 let _,_,term,_ = NCicUtils.lookup_subst i subst in
212 let term = NCicSubstitution.subst_meta l term in
213 aux test_eq_only metasenv subst context (mk_appl term args) t2
215 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
216 let _,_,term,_ = NCicUtils.lookup_subst i subst in
217 let term = NCicSubstitution.subst_meta l term in
218 aux test_eq_only metasenv subst context t1 (mk_appl term args)
220 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
221 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
224 (fun (metasenv, subst) t1 t2 ->
225 aux test_eq_only metasenv subst context t1 t2)
226 (metasenv,subst) l1 l2
227 with Invalid_argument _ ->
228 raise (fail_exc metasenv subst context t1 t2)
230 | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
231 (* we verify that none of the args is a Meta,
232 since beta expanding w.r.t a metavariable makes no sense *)
233 let subst, metasenv, beta_expanded =
235 test_equality_only metasenv subst context t2 args ugraph
237 aux test_eq_only metasenv subst context
238 (C.Meta (i,l)) beta_expanded
239 | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
240 let subst,metasenv,beta_expanded =
243 metasenv subst context t1 args ugraph
245 fo_unif_subst test_equality_only subst context metasenv
246 (C.Meta (i,l)) beta_expanded ugraph1
249 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
250 when (Ref.eq r1 r2 &&
251 List.length (E.get_relevance r1) >= List.length tl1) ->
252 let relevance = E.get_relevance r1 in
253 let relevance = match r1 with
254 | Ref.Ref (_,Ref.Con (_,_,lno)) ->
255 let _,relevance = HExtlib.split_nth lno relevance in
256 HExtlib.mk_list false lno @ relevance
259 let fail = ref ~-1 in
261 HExtlib.list_forall_default3
262 (fun t1 t2 b -> fail := !fail+1; not b || aux test_eq_only context t1 t2)
263 tl1 tl2 true relevance
264 with Invalid_argument _ -> false)
268 let relevance = get_relevance_p ~subst context _hd1 tl1 in
269 let _,relevance = HExtlib.split_nth !fail relevance in
270 let b,relevance = (match relevance with
273 let _,tl1 = HExtlib.split_nth (!fail+1) tl1 in
274 let _,tl2 = HExtlib.split_nth (!fail+1) tl2 in
278 HExtlib.list_forall_default3
279 (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
280 tl1 tl2 true relevance
281 with Invalid_argument _ -> false)
283 | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
284 aux test_eq_only context hd1 hd2 &&
285 let relevance = get_relevance ~subst context hd1 tl1 in
287 HExtlib.list_forall_default3
288 (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
289 tl1 tl2 true relevance
290 with Invalid_argument _ -> false)
292 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
293 C.Match (ref2,outtype2,term2,pl2)) ->
294 let _,_,itl,_,_ = E.get_checked_indtys ref1 in
295 let _,_,ty,_ = List.nth itl tyno in
296 let rec remove_prods ~subst context ty =
297 let ty = whd ~subst context ty in
300 | C.Prod (name,so,ta) ->
301 remove_prods ~subst ((name,(C.Decl so))::context) ta
305 match remove_prods ~subst [] ty with
306 | C.Sort C.Prop -> true
309 let rec remove_prods ~subst context ty =
310 let ty = whd ~subst context ty in
313 | C.Prod (name,so,ta) ->
314 remove_prods ~subst ((name,(C.Decl so))::context) ta
317 if not (Ref.eq ref1 ref2) then
318 raise (uncert_exc metasenv subst context t1 t2)
320 let metasenv, subst =
321 aux test_eq_only metasenv subst context outtype1 outtype2 in
322 let metasenv, subst =
323 try aux test_eq_only metasenv subst context term1 term2
324 with UnificationFailure _ | Uncertain _ when is_prop ->
329 (fun (metasenv,subst) -> aux test_eq_only metasenv subst context)
330 (metasenv, subst) pl1 pl2
331 with Invalid_argument _ ->
332 raise (uncert_exc metasenv subst context t1 t2)
333 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
334 | _ -> raise (uncert_exc metasenv subst context t1 t2)
336 let rec unif_machines metasenv subst = function
337 | ((k1,e1,NCic.Meta _ as t1,s1 as m1),(k2,e2,t2,s2 as m2),delta)
338 | ((k1,e1,t1,s1 as m1),(k2,e2,NCic.Meta _ as t2,s2 as m2),delta) ->
340 fo_unif test_eq_only metasenv subst (R.unwind m1) (R.unwind m2)
341 with UnificationFailure _ | Uncertain _ when delta > 0 ->
342 let delta = delta - 1 in
343 let red = R.reduce ~delta ~subst context in
344 unif_machines metasenv subst (red m1,red m2,delta)
345 | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) ->
347 let metasenv, subst =
348 fo_unif test_eq_only metasenv subst
349 (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[]))
353 | C.Const r -> NCicEnvironment.get_relevance r
356 let rec check_stack f l1 l2 r a =
358 | x1::tl1, x2::tl2, r::tr ->
359 check_stack f tl1 tl2 tr (f x1 x2 r a)
360 | x1::tl1, x2::tl2, [] ->
361 check_stack f tl1 tl2 tr (f x1 x2 true a)
363 | _ -> raise (Invalid_argument "check_stack")
366 (fun t1 t2 b (metasenv,subst) ->
368 let t1 = RS.from_stack t1 in
369 let t2 = RS.from_stack t2 in
370 unif_machines metasenv subst (small_delta_step t1 t2)
371 with UnificationFailure _ | Uncertain _ when not b ->
373 s1 s2 relevance (metasenv,subst)
374 with Invalid_argument _ ->
375 raise (UnificationFailure (lazy ( "Can't unify " ^ NCicPp.ppterm
376 ~metasenv ~subst ~context (R.unwind m1) ^ " with " ^ NCicPp.ppterm
377 ~metasenv ~subst ~context (R.unwind m2))))
378 with UnificationFailure _ | Uncertain _ when delta > 0 ->
379 let delta = delta - 1 in
380 let red = R.reduce ~delta ~subst context in
381 unif_machines metasenv subst (red m1,red m2,delta)
383 let height_of = function
384 | NCic.Const (Ref.Ref (_,Ref.Def h))
385 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
386 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
387 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
388 | NCic.Meta _ -> max_int
391 let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
392 let h1 = height_of t1 in
393 let h2 = height_of t2 in
394 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
395 R.reduce ~delta ~subst context m1,
396 R.reduce ~delta ~subst context m2,
399 try fo_unif test_eq_only metasenv subst t1 t2
400 with UnificationFailure msg |Uncertain msg as exn ->
402 unif_machines metasenv subst
403 (small_delta_step (0,[],t1,[]) (0,[],t2,[]))
405 | UnificationFailure _ -> raise (UnificationFailure msg)
406 | Uncertain _ -> raise exn
408 aux false metasenv subst context t1 t2
417 exception UnificationFailure of string Lazy.t;;
418 exception Uncertain of string Lazy.t;;
419 exception AssertFailure of string Lazy.t;;
421 let verbose = false;;
422 let debug_print = fun _ -> ()
424 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
425 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
426 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
427 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
429 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
431 let type_of_aux' metasenv subst context term ugraph =
434 profile.HExtlib.profile
435 (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
437 CicTypeChecker.TypeCheckerFailure msg ->
441 "Kernel Type checking error:
442 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
443 (CicMetaSubst.ppterm ~metasenv subst term)
444 (CicMetaSubst.ppterm ~metasenv [] term)
445 (CicMetaSubst.ppcontext ~metasenv subst context)
446 (CicMetaSubst.ppmetasenv subst metasenv)
447 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
448 raise (AssertFailure msg)
449 | CicTypeChecker.AssertFailure msg ->
452 "Kernel Type checking assertion failure:
453 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
454 (CicMetaSubst.ppterm ~metasenv subst term)
455 (CicMetaSubst.ppterm ~metasenv [] term)
456 (CicMetaSubst.ppcontext ~metasenv subst context)
457 (CicMetaSubst.ppmetasenv subst metasenv)
458 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
459 raise (AssertFailure msg)
460 in profiler_toa.HExtlib.profile foo ()
463 let exists_a_meta l =
467 | Cic.Appl (Cic.Meta _::_) -> true
470 let rec deref subst t =
471 let snd (_,a,_) = a in
476 (CicSubstitution.subst_meta
477 l (snd (CicUtil.lookup_subst n subst)))
479 CicUtil.Subst_not_found _ -> t)
480 | Cic.Appl(Cic.Meta(n,l)::args) ->
481 (match deref subst (Cic.Meta(n,l)) with
482 | Cic.Lambda _ as t ->
483 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
484 | r -> Cic.Appl(r::args))
485 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
486 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
491 let foo () = deref subst t
492 in profiler_deref.HExtlib.profile foo ()
494 exception WrongShape;;
495 let eta_reduce after_beta_expansion after_beta_expansion_body
496 before_beta_expansion
499 match before_beta_expansion,after_beta_expansion_body with
500 Cic.Appl l, Cic.Appl l' ->
501 let rec all_but_last check_last =
505 | [_] -> if check_last then raise WrongShape else []
506 | he::tl -> he::(all_but_last check_last tl)
508 let all_but_last check_last l =
509 match all_but_last check_last l with
514 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
515 let all_but_last = all_but_last false l in
516 (* here we should test alpha-equivalence; however we know by
517 construction that here alpha_equivalence is equivalent to = *)
518 if t = all_but_last then
522 | _,_ -> after_beta_expansion
524 WrongShape -> after_beta_expansion
526 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
527 let module S = CicSubstitution in
528 let module C = Cic in
530 let rec aux metasenv subst n context t' ugraph =
533 let subst,metasenv,ugraph1 =
534 fo_unif_subst test_equality_only subst context metasenv
535 (CicSubstitution.lift n arg) t' ugraph
538 subst,metasenv,C.Rel (1 + n),ugraph1
541 | UnificationFailure _ ->
543 | C.Rel m -> subst,metasenv,
544 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
545 | C.Var (uri,exp_named_subst) ->
546 let subst,metasenv,exp_named_subst',ugraph1 =
547 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
549 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
551 (* andrea: in general, beta_expand can create badly typed
552 terms. This happens quite seldom in practice, UNLESS we
553 iterate on the local context. For this reason, we renounce
554 to iterate and just lift *)
558 Some t -> Some (CicSubstitution.lift 1 t)
560 subst, metasenv, C.Meta (i,l), ugraph
562 | C.Implicit _ as t -> subst,metasenv,t,ugraph
564 let subst,metasenv,te',ugraph1 =
565 aux metasenv subst n context te ugraph in
566 let subst,metasenv,ty',ugraph2 =
567 aux metasenv subst n context ty ugraph1 in
568 (* TASSI: sure this is in serial? *)
569 subst,metasenv,(C.Cast (te', ty')),ugraph2
571 let subst,metasenv,s',ugraph1 =
572 aux metasenv subst n context s ugraph in
573 let subst,metasenv,t',ugraph2 =
574 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
577 (* TASSI: sure this is in serial? *)
578 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
579 | C.Lambda (nn,s,t) ->
580 let subst,metasenv,s',ugraph1 =
581 aux metasenv subst n context s ugraph in
582 let subst,metasenv,t',ugraph2 =
583 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
585 (* TASSI: sure this is in serial? *)
586 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
587 | C.LetIn (nn,s,ty,t) ->
588 let subst,metasenv,s',ugraph1 =
589 aux metasenv subst n context s ugraph in
590 let subst,metasenv,ty',ugraph1 =
591 aux metasenv subst n context ty ugraph in
592 let subst,metasenv,t',ugraph2 =
593 aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
596 (* TASSI: sure this is in serial? *)
597 subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
599 let subst,metasenv,revl',ugraph1 =
601 (fun (subst,metasenv,appl,ugraph) t ->
602 let subst,metasenv,t',ugraph1 =
603 aux metasenv subst n context t ugraph in
604 subst,metasenv,(t'::appl),ugraph1
605 ) (subst,metasenv,[],ugraph) l
607 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
608 | C.Const (uri,exp_named_subst) ->
609 let subst,metasenv,exp_named_subst',ugraph1 =
610 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
612 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
613 | C.MutInd (uri,i,exp_named_subst) ->
614 let subst,metasenv,exp_named_subst',ugraph1 =
615 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
617 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
618 | C.MutConstruct (uri,i,j,exp_named_subst) ->
619 let subst,metasenv,exp_named_subst',ugraph1 =
620 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
622 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
623 | C.MutCase (sp,i,outt,t,pl) ->
624 let subst,metasenv,outt',ugraph1 =
625 aux metasenv subst n context outt ugraph in
626 let subst,metasenv,t',ugraph2 =
627 aux metasenv subst n context t ugraph1 in
628 let subst,metasenv,revpl',ugraph3 =
630 (fun (subst,metasenv,pl,ugraph) t ->
631 let subst,metasenv,t',ugraph1 =
632 aux metasenv subst n context t ugraph in
633 subst,metasenv,(t'::pl),ugraph1
634 ) (subst,metasenv,[],ugraph2) pl
636 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
637 (* TASSI: not sure this is serial *)
639 (*CSC: not implemented
640 let tylen = List.length fl in
643 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
646 C.Fix (i, substitutedfl)
648 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
650 (*CSC: not implemented
651 let tylen = List.length fl in
654 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
657 C.CoFix (i, substitutedfl)
660 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
662 and aux_exp_named_subst metasenv subst n context ens ugraph =
664 (fun (uri,t) (subst,metasenv,l,ugraph) ->
665 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
666 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
668 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
670 FreshNamesGenerator.mk_fresh_name ~subst
671 metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
673 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
674 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
675 subst, metasenv, t'', ugraph2
676 in profiler_beta_expand.HExtlib.profile foo ()
679 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
680 let _,subst,metasenv,hd,ugraph =
682 (fun arg (num,subst,metasenv,t,ugraph) ->
683 let subst,metasenv,t,ugraph1 =
684 beta_expand num test_equality_only
685 metasenv subst context t arg ugraph
687 num+1,subst,metasenv,t,ugraph1
688 ) args (1,subst,metasenv,t,ugraph)
690 subst,metasenv,hd,ugraph
692 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
695 | (m2,_,c2,c2')::_ ->
696 let m1,c1,c1' = carr,to1,to2 in
698 function Some (_,t) -> CicPp.ppterm t
702 ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
703 CoercDb.string_of_carr car2^": " ^
704 CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
705 unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
706 unopt c2^" + "^unopt c2')
708 (* NUOVA UNIFICAZIONE *)
709 (* A substitution is a (int * Cic.term) list that associates a
710 metavariable i with its body.
711 A metaenv is a (int * Cic.term) list that associate a metavariable
713 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
714 a new substitution which is _NOT_ unwinded. It must be unwinded before
717 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
718 let module C = Cic in
719 let module R = CicReduction in
720 let module S = CicSubstitution in
721 let t1 = deref subst t1 in
722 let t2 = deref subst t2 in
723 let (&&&) a b = (a && b) || ((not a) && (not b)) in
724 (* let bef = Sys.time () in *)
726 if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
730 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
731 in profiler_are_convertible.HExtlib.profile foo ()
733 (* let aft = Sys.time () in
734 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
735 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
736 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
738 subst, metasenv, ugraph
741 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
742 let _,subst,metasenv,ugraph1 =
745 (fun (j,subst,metasenv,ugraph) t1 t2 ->
748 | _,None -> j+1,subst,metasenv,ugraph
749 | Some t1', Some t2' ->
750 (* First possibility: restriction *)
751 (* Second possibility: unification *)
752 (* Third possibility: convertibility *)
755 ~subst ~metasenv context t1' t2' ugraph
758 j+1,subst,metasenv, ugraph1
761 let subst,metasenv,ugraph2 =
764 subst context metasenv t1' t2' ugraph
766 j+1,subst,metasenv,ugraph2
769 | UnificationFailure _ ->
770 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
771 let metasenv, subst =
772 CicMetaSubst.restrict
773 subst [(n,j)] metasenv in
774 j+1,subst,metasenv,ugraph1)
775 ) (1,subst,metasenv,ugraph) ln lm
779 (UnificationFailure (lazy "1"))
782 "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."
783 (CicMetaSubst.ppterm ~metasenv subst t1)
784 (CicMetaSubst.ppterm ~metasenv subst t2))) *)
785 | Invalid_argument _ ->
787 (UnificationFailure (lazy "2")))
790 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
791 (CicMetaSubst.ppterm ~metasenv subst t1)
792 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
793 in subst,metasenv,ugraph1
794 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
795 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
797 | (t, C.Meta (n,l)) ->
800 C.Meta (n,_), C.Meta (m,_) when n < m -> false
801 | _, C.Meta _ -> false
804 let lower = fun x y -> if swap then y else x in
805 let upper = fun x y -> if swap then x else y in
806 let fo_unif_subst_ordered
807 test_equality_only subst context metasenv m1 m2 ugraph =
808 fo_unif_subst test_equality_only subst context metasenv
809 (lower m1 m2) (upper m1 m2) ugraph
812 let subst,metasenv,ugraph1 =
813 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
816 type_of_aux' metasenv subst context t ugraph
820 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
822 UnificationFailure _ as e -> raise e
823 | Uncertain msg -> raise (UnificationFailure msg)
825 debug_print (lazy "siamo allo huge hack");
826 (* TODO huge hack!!!!
827 * we keep on unifying/refining in the hope that
828 * the problem will be eventually solved.
829 * In the meantime we're breaking a big invariant:
830 * the terms that we are unifying are no longer well
831 * typed in the current context (in the worst case
832 * we could even diverge) *)
833 (subst, metasenv,ugraph)) in
834 let t',metasenv,subst =
836 CicMetaSubst.delift n subst context metasenv l t
838 (CicMetaSubst.MetaSubstFailure msg)->
839 raise (UnificationFailure msg)
840 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
844 C.Sort (C.Type u) when not test_equality_only ->
845 let u' = CicUniv.fresh () in
846 let s = C.Sort (C.Type u') in
849 CicUniv.add_ge (upper u u') (lower u u') ugraph1
853 CicUniv.UniverseInconsistency msg ->
854 raise (UnificationFailure msg))
857 (* Unifying the types may have already instantiated n. Let's check *)
859 let (_, oldt,_) = CicUtil.lookup_subst n subst in
860 let lifted_oldt = S.subst_meta l oldt in
861 fo_unif_subst_ordered
862 test_equality_only subst context metasenv t lifted_oldt ugraph2
864 CicUtil.Subst_not_found _ ->
865 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
866 let subst = (n, (context, t'',ty)) :: subst in
868 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
869 subst, metasenv, ugraph2
871 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
872 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
873 if UriManager.eq uri1 uri2 then
874 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
875 exp_named_subst1 exp_named_subst2 ugraph
877 raise (UnificationFailure (lazy
879 "Can't unify %s with %s due to different constants"
880 (CicMetaSubst.ppterm ~metasenv subst t1)
881 (CicMetaSubst.ppterm ~metasenv subst t2))))
882 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
883 if UriManager.eq uri1 uri2 && i1 = i2 then
884 fo_unif_subst_exp_named_subst
886 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
888 raise (UnificationFailure
891 "Can't unify %s with %s due to different inductive principles"
892 (CicMetaSubst.ppterm ~metasenv subst t1)
893 (CicMetaSubst.ppterm ~metasenv subst t2))))
894 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
895 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
896 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
897 fo_unif_subst_exp_named_subst
899 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
901 raise (UnificationFailure
904 "Can't unify %s with %s due to different inductive constructors"
905 (CicMetaSubst.ppterm ~metasenv subst t1)
906 (CicMetaSubst.ppterm ~metasenv subst t2))))
907 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
908 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
909 subst context metasenv te t2 ugraph
910 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
911 subst context metasenv t1 te ugraph
912 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
913 let subst',metasenv',ugraph1 =
914 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
916 fo_unif_subst test_equality_only
917 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
918 | (C.LetIn (_,s1,ty1,t1), t2)
919 | (t2, C.LetIn (_,s1,ty1,t1)) ->
921 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
922 | (C.Appl l1, C.Appl l2) ->
923 (* andrea: this case should be probably rewritten in the
926 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
929 (fun (subst,metasenv,ugraph) t1 t2 ->
931 test_equality_only subst context metasenv t1 t2 ugraph)
932 (subst,metasenv,ugraph) l1 l2
933 with (Invalid_argument msg) ->
934 raise (UnificationFailure (lazy msg)))
935 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
936 (* we verify that none of the args is a Meta,
937 since beta expanding with respoect to a metavariable
941 let (_,t,_) = CicUtil.lookup_subst i subst in
942 let lifted = S.subst_meta l t in
943 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
946 subst context metasenv reduced t2 ugraph
947 with CicUtil.Subst_not_found _ -> *)
948 let subst,metasenv,beta_expanded,ugraph1 =
950 test_equality_only metasenv subst context t2 args ugraph
952 fo_unif_subst test_equality_only subst context metasenv
953 (C.Meta (i,l)) beta_expanded ugraph1
954 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
956 let (_,t,_) = CicUtil.lookup_subst i subst in
957 let lifted = S.subst_meta l t in
958 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
961 subst context metasenv t1 reduced ugraph
962 with CicUtil.Subst_not_found _ -> *)
963 let subst,metasenv,beta_expanded,ugraph1 =
966 metasenv subst context t1 args ugraph
968 fo_unif_subst test_equality_only subst context metasenv
969 (C.Meta (i,l)) beta_expanded ugraph1
971 let lr1 = List.rev l1 in
972 let lr2 = List.rev l2 in
974 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
977 | _,[] -> assert false
980 test_equality_only subst context metasenv h1 h2 ugraph
983 fo_unif_subst test_equality_only subst context metasenv
984 h (C.Appl (List.rev l)) ugraph
985 | ((h1::l1),(h2::l2)) ->
986 let subst', metasenv',ugraph1 =
989 subst context metasenv h1 h2 ugraph
992 test_equality_only subst' metasenv' (l1,l2) ugraph1
996 test_equality_only subst metasenv (lr1, lr2) ugraph
998 | UnificationFailure s
999 | Uncertain s as exn ->
1002 | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
1003 (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
1004 CoercDb.is_a_coercion cc1 <> None &&
1005 CoercDb.is_a_coercion cc2 <> None &&
1006 not (UriManager.eq uri1 uri2) ->
1008 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1010 let inner_coerced t =
1011 let t = CicMetaSubst.apply_subst subst t in
1015 (match CoercGraph.coerced_arg l with
1017 | Some (t,_) -> aux (List.hd l) t t)
1020 aux (Cic.Implicit None) (Cic.Implicit None) t
1022 let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
1023 let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
1026 CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
1028 | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
1031 let head1_c, head2_c =
1033 CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
1035 | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
1038 let unfold uri ens args =
1040 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
1044 | Cic.Constant (_,Some bo,_,_,_) ->
1045 CicReduction.head_beta_reduce ~delta:false
1046 (Cic.Appl (bo::args))
1049 let conclude subst metasenv ugraph last_tl1' last_tl2' =
1050 let subst',metasenv,ugraph =
1053 ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
1054 " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
1056 fo_unif_subst test_equality_only subst context
1057 metasenv last_tl1' last_tl2' ugraph
1059 if subst = subst' then raise exn
1062 let subst,metasenv,ugrph as res =
1064 fo_unif_subst test_equality_only subst' context
1065 metasenv (C.Appl l1) (C.Appl l2) ugraph
1069 (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
1070 " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1074 if CoercDb.eq_carr car1 car2 then
1075 match last_tl1,last_tl2 with
1076 | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
1079 let subst,metasenv,ugraph =
1080 fo_unif_subst test_equality_only subst context
1081 metasenv last_tl1 last_tl2 ugraph
1083 fo_unif_subst test_equality_only subst context
1084 metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
1085 | _ when CoercDb.eq_carr head1_c head2_c ->
1086 (* composite VS composition + metas avoiding
1087 * coercions not only in coerced position *)
1088 if c1 <> cc1 && c2 <> cc2 then
1089 conclude subst metasenv ugraph
1094 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
1096 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
1098 fo_unif_subst test_equality_only subst context
1099 metasenv l1 l2 ugraph
1103 match last_tl1 with Cic.Meta _ -> true | _ -> false in
1105 match last_tl2 with Cic.Meta _ -> true | _ -> false in
1106 if not (grow1 || grow2) then
1107 (* no flexible terminals -> no pullback, but
1108 * we still unify them, in some cases it helps *)
1109 conclude subst metasenv ugraph last_tl1 last_tl2
1113 metasenv subst context (grow1,car1) (grow2,car2)
1117 | (carr,metasenv,to1,to2)::xxx ->
1118 warn_if_not_unique xxx to1 to2 carr car1 car2;
1119 let last_tl1',(subst,metasenv,ugraph) =
1120 match grow1,to1 with
1121 | true,Some (last,coerced) ->
1123 fo_unif_subst test_equality_only subst context
1124 metasenv coerced last_tl1 ugraph
1125 | _ -> last_tl1,(subst,metasenv,ugraph)
1127 let last_tl2',(subst,metasenv,ugraph) =
1128 match grow2,to2 with
1129 | true,Some (last,coerced) ->
1131 fo_unif_subst test_equality_only subst context
1132 metasenv coerced last_tl2 ugraph
1133 | _ -> last_tl2,(subst,metasenv,ugraph)
1135 conclude subst metasenv ugraph last_tl1' last_tl2')
1137 (* {{{ CSC: This is necessary because of the "elim H" tactic
1138 where the type of H is only reducible to an
1139 inductive type. This could be extended from inductive
1140 types to any rigid term. However, the code is
1141 duplicated in two places: inside applications and
1142 outside them. Probably it would be better to
1143 work with lambda-bar terms instead. *)
1144 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
1145 | (_, Cic.MutInd _::_) ->
1146 let t1' = R.whd ~subst context t1 in
1148 C.Appl (C.MutInd _::_) ->
1149 fo_unif_subst test_equality_only
1150 subst context metasenv t1' t2 ugraph
1151 | _ -> raise (UnificationFailure (lazy "88")))
1152 | (Cic.MutInd _::_,_) ->
1153 let t2' = R.whd ~subst context t2 in
1155 C.Appl (C.MutInd _::_) ->
1156 fo_unif_subst test_equality_only
1157 subst context metasenv t1 t2' ugraph
1160 (lazy ("not a mutind :"^
1161 CicMetaSubst.ppterm ~metasenv subst t2 ))))
1164 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
1165 let subst', metasenv',ugraph1 =
1166 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
1168 let subst'',metasenv'',ugraph2 =
1169 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
1173 (fun (subst,metasenv,ugraph) t1 t2 ->
1175 test_equality_only subst context metasenv t1 t2 ugraph
1176 ) (subst'',metasenv'',ugraph2) pl1 pl2
1178 Invalid_argument _ ->
1179 raise (UnificationFailure (lazy "6.1")))
1181 "Error trying to unify %s with %s: the number of branches is not the same."
1182 (CicMetaSubst.ppterm ~metasenv subst t1)
1183 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
1184 | (C.Rel _, _) | (_, C.Rel _) ->
1186 subst, metasenv,ugraph
1188 raise (UnificationFailure (lazy
1190 "Can't unify %s with %s because they are not convertible"
1191 (CicMetaSubst.ppterm ~metasenv subst t1)
1192 (CicMetaSubst.ppterm ~metasenv subst t2))))
1193 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
1194 let subst,metasenv,beta_expanded,ugraph1 =
1196 test_equality_only metasenv subst context t2 args ugraph
1198 fo_unif_subst test_equality_only subst context metasenv
1199 (C.Meta (i,l)) beta_expanded ugraph1
1200 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
1201 let subst,metasenv,beta_expanded,ugraph1 =
1203 test_equality_only metasenv subst context t1 args ugraph
1205 fo_unif_subst test_equality_only subst context metasenv
1206 beta_expanded (C.Meta (i,l)) ugraph1
1207 (* Works iff there are no arguments applied to it; similar to the
1209 | (_, C.MutInd _) ->
1210 let t1' = R.whd ~subst context t1 in
1213 fo_unif_subst test_equality_only
1214 subst context metasenv t1' t2 ugraph
1215 | _ -> raise (UnificationFailure (lazy "8")))
1217 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
1218 let subst',metasenv',ugraph1 =
1219 fo_unif_subst true subst context metasenv s1 s2 ugraph
1221 fo_unif_subst test_equality_only
1222 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1224 (match CicReduction.whd ~subst context t2 with
1226 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1227 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
1229 (match CicReduction.whd ~subst context t1 with
1231 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1232 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
1234 (* delta-beta reduction should almost never be a problem for
1236 1. long computations require iota reduction
1237 2. it is extremely rare that a close term t1 (that could be unified
1238 to t2) beta-delta reduces to t1' while t2 does not beta-delta
1239 reduces in the same way. This happens only if one meta of t2
1240 occurs in head position during beta reduction. In this unluky
1241 case too much reduction will be performed on t1 and unification
1242 will surely fail. *)
1243 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
1244 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
1245 if t1 = t1' && t2 = t2' then
1246 raise (UnificationFailure
1249 "Can't unify %s with %s because they are not convertible"
1250 (CicMetaSubst.ppterm ~metasenv subst t1)
1251 (CicMetaSubst.ppterm ~metasenv subst t2))))
1254 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
1256 UnificationFailure _
1258 raise (UnificationFailure
1261 "Can't unify %s with %s because they are not convertible"
1262 (CicMetaSubst.ppterm ~metasenv subst t1)
1263 (CicMetaSubst.ppterm ~metasenv subst t2))))
1265 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
1266 exp_named_subst1 exp_named_subst2 ugraph
1270 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
1271 assert (uri1=uri2) ;
1272 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1273 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
1275 Invalid_argument _ ->
1280 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
1283 raise (UnificationFailure (lazy (sprintf
1284 "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))))
1286 (* A substitution is a (int * Cic.term) list that associates a *)
1287 (* metavariable i with its body. *)
1288 (* metasenv is of type Cic.metasenv *)
1289 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
1290 (* a new substitution which is already unwinded and ready to be applied and *)
1291 (* a new metasenv in which some hypothesis in the contexts of the *)
1292 (* metavariables may have been restricted. *)
1293 let fo_unif metasenv context t1 t2 ugraph =
1294 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
1296 let enrich_msg msg subst context metasenv t1 t2 ugraph =
1299 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"
1300 (CicMetaSubst.ppterm ~metasenv subst t1)
1302 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1305 | UnificationFailure s
1307 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1308 (CicMetaSubst.ppterm ~metasenv subst t2)
1310 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1313 | UnificationFailure s
1315 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1316 (CicMetaSubst.ppcontext ~metasenv subst context)
1317 (CicMetaSubst.ppmetasenv subst metasenv)
1318 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
1320 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
1321 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
1323 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1324 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
1326 | UnificationFailure s
1328 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1329 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
1331 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1332 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
1334 | UnificationFailure s
1336 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1337 (CicMetaSubst.ppcontext ~metasenv subst context)
1338 (CicMetaSubst.ppmetasenv subst metasenv)
1342 let fo_unif_subst subst context metasenv t1 t2 ugraph =
1344 fo_unif_subst false subst context metasenv t1 t2 ugraph
1346 | AssertFailure msg ->
1347 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1348 | UnificationFailure msg ->
1349 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))