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;;
43 let delift_if_not_occur body orig =
45 NCicSubstitution.psubst ~avoid_beta_redexes:true
46 (fun () -> raise WrongShape) [()] body
47 with WrongShape -> orig
50 | NCic.Lambda(name, src, NCic.Appl [hd; NCic.Rel 1]) as orig ->
51 delift_if_not_occur hd orig
52 | NCic.Lambda(name, src, NCic.Appl (hd :: l)) as orig
53 when HExtlib.list_last l = NCic.Rel 1 ->
55 let args, _ = Hextlib.split_nth (List.length l - 1) l in
58 delift_if_not_occur body orig
62 let rec beta_expand num test_eq_only swap metasenv subst context t arg =
63 let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
66 unify test_eq_only metasenv subst context
67 (NCicSubstitution.lift n arg) t'
69 (metasenv, subst), C.Rel (1 + n)
70 with Uncertain _ | UnificationFailure _ ->
73 (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
74 (* andrea: in general, beta_expand can create badly typed
75 terms. This happens quite seldom in practice, UNLESS we
76 iterate on the local context. For this reason, we renounce
77 to iterate and just lift *)
78 | NCic.Meta (i,(shift,lc)) ->
79 (metasenv,subst), NCic.Meta (i,(shift+1,lc))
80 | NCic.Prod (name, src, tgt) as orig ->
81 let (metasenv, subst), src1 = aux (n,context,true) acc src in
82 let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
83 let (metasenv,subst), tgt1 = aux k (metasenv, subst) tgt in
84 if src == src1 && tgt == tgt1 then orig else
85 NCic.Prod (name, src1, tgt1)
87 NCicUntrusted.map_term_fold_a
88 (fun e (n,ctx) -> n+1,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,_), t1 =
94 aux (0, context, test_eq_only) (metasenv, subst) t in
95 let t2 = eta_reduce (C.Lambda (fresh_name,argty,t1)) in
97 ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
99 with NCicTypeChecker.TypeCheckerFailure _ ->
100 NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
102 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
103 let _, subst, metasenv, hd =
105 (fun arg (num,subst,metasenv,t) ->
106 let subst, metasenv, t =
107 beta_expand num test_equality_only metasenv subst context t arg
109 num+1,subst,metasenv,t)
110 args (1,subst,metasenv,t)
114 and instantiate test_eq_only metasenv subst context n lc t swap =
115 let unif m s c t1 t2 =
116 if swap then unify m s c t2 t1 else unify m s c t1 t2
119 try NCicTypeChecker.typeof ~subst ~metasenv context t
120 with NCicTypeChecker.TypeCheckerFailure _ -> assert false
122 let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
123 let ty = NCicSubstitution.subst_meta lc ty in
124 let metasenv, subst = unify metasenv susbt context ty ty_t in
125 let (metasenv, subst), t =
126 NCicMetaSubst.delift metasenv subst context n lc t
128 (* Unifying the types may have already instantiated n. *)
130 let _, _,oldt,_ = CicUtil.lookup_subst n subst in
131 let oldt = NCicSubstitution.subst_meta lc oldt in
132 (* conjecture: always fail --> occur check *)
133 unify test_eq_only metasenv subst context oldt t
134 with CicUtil.Subst_not_found _ ->
135 (* by cumulativity when unify(?,Type_i)
136 * we could ? := Type_j with j <= i... *)
137 let subst = (n, (name, ctx, t, ty)) :: subst in
139 List.filter (fun (m,_) -> not (n = m)) metasenv
143 and unify metasenv subst context t1 t2 =
144 let rec aux test_eq_only metasenv subst context t1 t2 =
145 let fo_unif test_eq_only metasenv subst t1 t2 =
150 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
151 if NCicEnvironment.universe_leq a b then metasenv, subst
152 else raise (fail_exc metasenv subst context t1 t2)
153 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
154 if NCicEnvironment.universe_eq a b then metasenv, subst
155 else raise (fail_exc metasenv subst context t1 t2)
156 | (C.Sort C.Prop,C.Sort (C.Type _)) ->
157 if (not test_eq_only) then metasenv, subst
158 else raise (fail_exc metasenv subst context t1 t2)
160 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
161 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
162 let metasenv, subst = aux true metasenv subst context s1 s2 in
163 aux test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
164 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
165 let metasenv,subst=aux test_eq_only metasenv subst context ty1 ty2 in
166 let metasenv,subst=aux test_eq_only metasenv subst context s1 s2 in
167 let context = (name1, C.Def (s1,ty1))::context in
168 aux test_eq_only metasenv subst context t1 t2
170 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
172 let l1 = NCicUtils.expand_local_context l1 in
173 let l2 = NCicUtils.expand_local_context l2 in
174 let metasenv, subst, to_restrict, _ =
176 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
178 aux test_eq_only metasenv subst context
179 (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2),
181 with UnificationFailure _ | Uncertain _ ->
182 metasenv, subst, i::to_restrict, i-1)
183 l1 l2 (metasenv, subst, [], List.length l1)
185 let metasenv, subst, _ =
186 NCicMetaSubst.restrict metasenv subst n1 to_restrict
190 | Invalid_argument _ -> assert false
191 | NCicMetaSubst.MetaSubstFailure msg ->
193 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
194 let term1 = NCicSubstitution.subst_meta lc1 term in
195 let term2 = NCicSubstitution.subst_meta lc2 term in
196 aux test_eq_only metasenv subst context term1 term2
197 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
199 | C.Meta (n,lc), t ->
201 let _,_,term,_ = NCicUtils.lookup_subst n subst in
202 let term = NCicSubstitution.subst_meta lc term in
203 aux test_eq_only metasenv subst context term t
204 with NCicUtils.Subst_not_found _->
205 instantiate test_eq_only metasenv subst context n lc t false
207 | t, C.Meta (n,lc) ->
209 let _,_,term,_ = NCicUtils.lookup_subst n subst in
210 let term = NCicSubstitution.subst_meta lc term in
211 aux test_eq_only metasenv subst context t term
212 with NCicUtils.Subst_not_found _->
213 instantiate test_eq_only metasenv subst context n lc t true
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 (mk_appl term args) t2
220 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
221 let _,_,term,_ = NCicUtils.lookup_subst i subst in
222 let term = NCicSubstitution.subst_meta l term in
223 aux test_eq_only metasenv subst context t1 (mk_appl term args)
225 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
226 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
229 (fun (metasenv, subst) t1 t2 ->
230 aux test_eq_only metasenv subst context t1 t2)
231 (metasenv,subst) l1 l2
232 with Invalid_argument _ ->
233 raise (fail_exc metasenv subst context t1 t2)
235 | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
236 (* we verify that none of the args is a Meta,
237 since beta expanding w.r.t a metavariable makes no sense *)
238 let subst, metasenv, beta_expanded =
239 beta_expand_many (* passare swap *)
240 test_equality_only metasenv subst context t2 args ugraph
242 aux test_eq_only metasenv subst context
243 (C.Meta (i,l)) beta_expanded
244 | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
245 let subst,metasenv,beta_expanded =
248 metasenv subst context t1 args ugraph
250 fo_unif_subst test_equality_only subst context metasenv
251 (C.Meta (i,l)) beta_expanded ugraph1
254 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
255 when (Ref.eq r1 r2 &&
256 List.length (E.get_relevance r1) >= List.length tl1) ->
257 let relevance = E.get_relevance r1 in
258 let relevance = match r1 with
259 | Ref.Ref (_,Ref.Con (_,_,lno)) ->
260 let _,relevance = HExtlib.split_nth lno relevance in
261 HExtlib.mk_list false lno @ relevance
264 let fail = ref ~-1 in
266 HExtlib.list_forall_default3
267 (fun t1 t2 b -> fail := !fail+1; not b || aux test_eq_only context t1 t2)
268 tl1 tl2 true relevance
269 with Invalid_argument _ -> false)
273 let relevance = get_relevance_p ~subst context _hd1 tl1 in
274 let _,relevance = HExtlib.split_nth !fail relevance in
275 let b,relevance = (match relevance with
278 let _,tl1 = HExtlib.split_nth (!fail+1) tl1 in
279 let _,tl2 = HExtlib.split_nth (!fail+1) tl2 in
283 HExtlib.list_forall_default3
284 (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
285 tl1 tl2 true relevance
286 with Invalid_argument _ -> false)
288 | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
289 aux test_eq_only context hd1 hd2 &&
290 let relevance = get_relevance ~subst context hd1 tl1 in
292 HExtlib.list_forall_default3
293 (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
294 tl1 tl2 true relevance
295 with Invalid_argument _ -> false)
297 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
298 C.Match (ref2,outtype2,term2,pl2)) ->
299 let _,_,itl,_,_ = E.get_checked_indtys ref1 in
300 let _,_,ty,_ = List.nth itl tyno in
301 let rec remove_prods ~subst context ty =
302 let ty = whd ~subst context ty in
305 | C.Prod (name,so,ta) ->
306 remove_prods ~subst ((name,(C.Decl so))::context) ta
310 match remove_prods ~subst [] ty with
311 | C.Sort C.Prop -> true
314 let rec remove_prods ~subst context ty =
315 let ty = whd ~subst context ty in
318 | C.Prod (name,so,ta) ->
319 remove_prods ~subst ((name,(C.Decl so))::context) ta
322 if not (Ref.eq ref1 ref2) then
323 raise (uncert_exc metasenv subst context t1 t2)
325 let metasenv, subst =
326 aux test_eq_only metasenv subst context outtype1 outtype2 in
327 let metasenv, subst =
328 try aux test_eq_only metasenv subst context term1 term2
329 with UnificationFailure _ | Uncertain _ when is_prop ->
334 (fun (metasenv,subst) -> aux test_eq_only metasenv subst context)
335 (metasenv, subst) pl1 pl2
336 with Invalid_argument _ ->
337 raise (uncert_exc metasenv subst context t1 t2)
338 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
339 | _ -> raise (uncert_exc metasenv subst context t1 t2)
341 let rec unif_machines metasenv subst = function
342 | ((k1,e1,NCic.Meta _ as t1,s1 as m1),(k2,e2,t2,s2 as m2),delta)
343 | ((k1,e1,t1,s1 as m1),(k2,e2,NCic.Meta _ as t2,s2 as m2),delta) ->
345 fo_unif test_eq_only metasenv subst (R.unwind m1) (R.unwind m2)
346 with UnificationFailure _ | Uncertain _ when delta > 0 ->
347 let delta = delta - 1 in
348 let red = R.reduce ~delta ~subst context in
349 unif_machines metasenv subst (red m1,red m2,delta)
350 | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) ->
352 let metasenv, subst =
353 fo_unif test_eq_only metasenv subst
354 (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[]))
358 | C.Const r -> NCicEnvironment.get_relevance r
361 let rec check_stack f l1 l2 r a =
363 | x1::tl1, x2::tl2, r::tr ->
364 check_stack f tl1 tl2 tr (f x1 x2 r a)
365 | x1::tl1, x2::tl2, [] ->
366 check_stack f tl1 tl2 tr (f x1 x2 true a)
368 | _ -> raise (Invalid_argument "check_stack")
371 (fun t1 t2 b (metasenv,subst) ->
373 let t1 = RS.from_stack t1 in
374 let t2 = RS.from_stack t2 in
375 unif_machines metasenv subst (small_delta_step t1 t2)
376 with UnificationFailure _ | Uncertain _ when not b ->
378 s1 s2 relevance (metasenv,subst)
379 with Invalid_argument _ ->
380 raise (UnificationFailure (lazy ( "Can't unify " ^ NCicPp.ppterm
381 ~metasenv ~subst ~context (R.unwind m1) ^ " with " ^ NCicPp.ppterm
382 ~metasenv ~subst ~context (R.unwind m2))))
383 with UnificationFailure _ | Uncertain _ when delta > 0 ->
384 let delta = delta - 1 in
385 let red = R.reduce ~delta ~subst context in
386 unif_machines metasenv subst (red m1,red m2,delta)
388 let height_of = function
389 | NCic.Const (Ref.Ref (_,Ref.Def h))
390 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
391 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
392 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
393 | NCic.Meta _ -> max_int
396 let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
397 let h1 = height_of t1 in
398 let h2 = height_of t2 in
399 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
400 R.reduce ~delta ~subst context m1,
401 R.reduce ~delta ~subst context m2,
404 try fo_unif test_eq_only metasenv subst t1 t2
405 with UnificationFailure msg |Uncertain msg as exn ->
407 unif_machines metasenv subst
408 (small_delta_step (0,[],t1,[]) (0,[],t2,[]))
410 | UnificationFailure _ -> raise (UnificationFailure msg)
411 | Uncertain _ -> raise exn
413 aux false metasenv subst context t1 t2
422 exception UnificationFailure of string Lazy.t;;
423 exception Uncertain of string Lazy.t;;
424 exception AssertFailure of string Lazy.t;;
426 let verbose = false;;
427 let debug_print = fun _ -> ()
429 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
430 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
431 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
432 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
434 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
436 let type_of_aux' metasenv subst context term ugraph =
439 profile.HExtlib.profile
440 (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
442 CicTypeChecker.TypeCheckerFailure msg ->
446 "Kernel Type checking error:
447 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
448 (CicMetaSubst.ppterm ~metasenv subst term)
449 (CicMetaSubst.ppterm ~metasenv [] term)
450 (CicMetaSubst.ppcontext ~metasenv subst context)
451 (CicMetaSubst.ppmetasenv subst metasenv)
452 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
453 raise (AssertFailure msg)
454 | CicTypeChecker.AssertFailure msg ->
457 "Kernel Type checking assertion failure:
458 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
459 (CicMetaSubst.ppterm ~metasenv subst term)
460 (CicMetaSubst.ppterm ~metasenv [] term)
461 (CicMetaSubst.ppcontext ~metasenv subst context)
462 (CicMetaSubst.ppmetasenv subst metasenv)
463 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
464 raise (AssertFailure msg)
465 in profiler_toa.HExtlib.profile foo ()
468 let exists_a_meta l =
472 | Cic.Appl (Cic.Meta _::_) -> true
475 let rec deref subst t =
476 let snd (_,a,_) = a in
481 (CicSubstitution.subst_meta
482 l (snd (CicUtil.lookup_subst n subst)))
484 CicUtil.Subst_not_found _ -> t)
485 | Cic.Appl(Cic.Meta(n,l)::args) ->
486 (match deref subst (Cic.Meta(n,l)) with
487 | Cic.Lambda _ as t ->
488 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
489 | r -> Cic.Appl(r::args))
490 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
491 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
496 let foo () = deref subst t
497 in profiler_deref.HExtlib.profile foo ()
499 exception WrongShape;;
500 let eta_reduce after_beta_expansion after_beta_expansion_body
501 before_beta_expansion
504 match before_beta_expansion,after_beta_expansion_body with
505 Cic.Appl l, Cic.Appl l' ->
506 let rec all_but_last check_last =
510 | [_] -> if check_last then raise WrongShape else []
511 | he::tl -> he::(all_but_last check_last tl)
513 let all_but_last check_last l =
514 match all_but_last check_last l with
519 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
520 let all_but_last = all_but_last false l in
521 (* here we should test alpha-equivalence; however we know by
522 construction that here alpha_equivalence is equivalent to = *)
523 if t = all_but_last then
527 | _,_ -> after_beta_expansion
529 WrongShape -> after_beta_expansion
531 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
532 let module S = CicSubstitution in
533 let module C = Cic in
535 let rec aux metasenv subst n context t' ugraph =
538 let subst,metasenv,ugraph1 =
539 fo_unif_subst test_equality_only subst context metasenv
540 (CicSubstitution.lift n arg) t' ugraph
543 subst,metasenv,C.Rel (1 + n),ugraph1
546 | UnificationFailure _ ->
548 | C.Rel m -> subst,metasenv,
549 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
550 | C.Var (uri,exp_named_subst) ->
551 let subst,metasenv,exp_named_subst',ugraph1 =
552 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
554 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
556 (* andrea: in general, beta_expand can create badly typed
557 terms. This happens quite seldom in practice, UNLESS we
558 iterate on the local context. For this reason, we renounce
559 to iterate and just lift *)
563 Some t -> Some (CicSubstitution.lift 1 t)
565 subst, metasenv, C.Meta (i,l), ugraph
567 | C.Implicit _ as t -> subst,metasenv,t,ugraph
569 let subst,metasenv,te',ugraph1 =
570 aux metasenv subst n context te ugraph in
571 let subst,metasenv,ty',ugraph2 =
572 aux metasenv subst n context ty ugraph1 in
573 (* TASSI: sure this is in serial? *)
574 subst,metasenv,(C.Cast (te', ty')),ugraph2
576 let subst,metasenv,s',ugraph1 =
577 aux metasenv subst n context s ugraph in
578 let subst,metasenv,t',ugraph2 =
579 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
582 (* TASSI: sure this is in serial? *)
583 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
584 | C.Lambda (nn,s,t) ->
585 let subst,metasenv,s',ugraph1 =
586 aux metasenv subst n context s ugraph in
587 let subst,metasenv,t',ugraph2 =
588 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
590 (* TASSI: sure this is in serial? *)
591 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
592 | C.LetIn (nn,s,ty,t) ->
593 let subst,metasenv,s',ugraph1 =
594 aux metasenv subst n context s ugraph in
595 let subst,metasenv,ty',ugraph1 =
596 aux metasenv subst n context ty ugraph in
597 let subst,metasenv,t',ugraph2 =
598 aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
601 (* TASSI: sure this is in serial? *)
602 subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
604 let subst,metasenv,revl',ugraph1 =
606 (fun (subst,metasenv,appl,ugraph) t ->
607 let subst,metasenv,t',ugraph1 =
608 aux metasenv subst n context t ugraph in
609 subst,metasenv,(t'::appl),ugraph1
610 ) (subst,metasenv,[],ugraph) l
612 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
613 | C.Const (uri,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.Const (uri,exp_named_subst')),ugraph1
618 | C.MutInd (uri,i,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.MutInd (uri,i,exp_named_subst')),ugraph1
623 | C.MutConstruct (uri,i,j,exp_named_subst) ->
624 let subst,metasenv,exp_named_subst',ugraph1 =
625 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
627 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
628 | C.MutCase (sp,i,outt,t,pl) ->
629 let subst,metasenv,outt',ugraph1 =
630 aux metasenv subst n context outt ugraph in
631 let subst,metasenv,t',ugraph2 =
632 aux metasenv subst n context t ugraph1 in
633 let subst,metasenv,revpl',ugraph3 =
635 (fun (subst,metasenv,pl,ugraph) t ->
636 let subst,metasenv,t',ugraph1 =
637 aux metasenv subst n context t ugraph in
638 subst,metasenv,(t'::pl),ugraph1
639 ) (subst,metasenv,[],ugraph2) pl
641 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
642 (* TASSI: not sure this is serial *)
644 (*CSC: not implemented
645 let tylen = List.length fl in
648 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
651 C.Fix (i, substitutedfl)
653 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
655 (*CSC: not implemented
656 let tylen = List.length fl in
659 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
662 C.CoFix (i, substitutedfl)
665 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
667 and aux_exp_named_subst metasenv subst n context ens ugraph =
669 (fun (uri,t) (subst,metasenv,l,ugraph) ->
670 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
671 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
673 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
675 FreshNamesGenerator.mk_fresh_name ~subst
676 metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
678 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
679 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
680 subst, metasenv, t'', ugraph2
681 in profiler_beta_expand.HExtlib.profile foo ()
684 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
685 let _,subst,metasenv,hd,ugraph =
687 (fun arg (num,subst,metasenv,t,ugraph) ->
688 let subst,metasenv,t,ugraph1 =
689 beta_expand num test_equality_only
690 metasenv subst context t arg ugraph
692 num+1,subst,metasenv,t,ugraph1
693 ) args (1,subst,metasenv,t,ugraph)
695 subst,metasenv,hd,ugraph
697 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
700 | (m2,_,c2,c2')::_ ->
701 let m1,c1,c1' = carr,to1,to2 in
703 function Some (_,t) -> CicPp.ppterm t
707 ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
708 CoercDb.string_of_carr car2^": " ^
709 CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
710 unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
711 unopt c2^" + "^unopt c2')
713 (* NUOVA UNIFICAZIONE *)
714 (* A substitution is a (int * Cic.term) list that associates a
715 metavariable i with its body.
716 A metaenv is a (int * Cic.term) list that associate a metavariable
718 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
719 a new substitution which is _NOT_ unwinded. It must be unwinded before
722 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
723 let module C = Cic in
724 let module R = CicReduction in
725 let module S = CicSubstitution in
726 let t1 = deref subst t1 in
727 let t2 = deref subst t2 in
728 let (&&&) a b = (a && b) || ((not a) && (not b)) in
729 (* let bef = Sys.time () in *)
731 if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
735 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
736 in profiler_are_convertible.HExtlib.profile foo ()
738 (* let aft = Sys.time () in
739 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
740 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
741 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
743 subst, metasenv, ugraph
746 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
747 let _,subst,metasenv,ugraph1 =
750 (fun (j,subst,metasenv,ugraph) t1 t2 ->
753 | _,None -> j+1,subst,metasenv,ugraph
754 | Some t1', Some t2' ->
755 (* First possibility: restriction *)
756 (* Second possibility: unification *)
757 (* Third possibility: convertibility *)
760 ~subst ~metasenv context t1' t2' ugraph
763 j+1,subst,metasenv, ugraph1
766 let subst,metasenv,ugraph2 =
769 subst context metasenv t1' t2' ugraph
771 j+1,subst,metasenv,ugraph2
774 | UnificationFailure _ ->
775 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
776 let metasenv, subst =
777 CicMetaSubst.restrict
778 subst [(n,j)] metasenv in
779 j+1,subst,metasenv,ugraph1)
780 ) (1,subst,metasenv,ugraph) ln lm
784 (UnificationFailure (lazy "1"))
787 "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."
788 (CicMetaSubst.ppterm ~metasenv subst t1)
789 (CicMetaSubst.ppterm ~metasenv subst t2))) *)
790 | Invalid_argument _ ->
792 (UnificationFailure (lazy "2")))
795 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
796 (CicMetaSubst.ppterm ~metasenv subst t1)
797 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
798 in subst,metasenv,ugraph1
799 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
800 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
802 | (t, C.Meta (n,l)) ->
805 C.Meta (n,_), C.Meta (m,_) when n < m -> false
806 | _, C.Meta _ -> false
809 let lower = fun x y -> if swap then y else x in
810 let upper = fun x y -> if swap then x else y in
811 let fo_unif_subst_ordered
812 test_equality_only subst context metasenv m1 m2 ugraph =
813 fo_unif_subst test_equality_only subst context metasenv
814 (lower m1 m2) (upper m1 m2) ugraph
817 let subst,metasenv,ugraph1 =
818 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
821 type_of_aux' metasenv subst context t ugraph
825 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
827 UnificationFailure _ as e -> raise e
828 | Uncertain msg -> raise (UnificationFailure msg)
830 debug_print (lazy "siamo allo huge hack");
831 (* TODO huge hack!!!!
832 * we keep on unifying/refining in the hope that
833 * the problem will be eventually solved.
834 * In the meantime we're breaking a big invariant:
835 * the terms that we are unifying are no longer well
836 * typed in the current context (in the worst case
837 * we could even diverge) *)
838 (subst, metasenv,ugraph)) in
839 let t',metasenv,subst =
841 CicMetaSubst.delift n subst context metasenv l t
843 (CicMetaSubst.MetaSubstFailure msg)->
844 raise (UnificationFailure msg)
845 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
849 C.Sort (C.Type u) when not test_equality_only ->
850 let u' = CicUniv.fresh () in
851 let s = C.Sort (C.Type u') in
854 CicUniv.add_ge (upper u u') (lower u u') ugraph1
858 CicUniv.UniverseInconsistency msg ->
859 raise (UnificationFailure msg))
862 (* Unifying the types may have already instantiated n. Let's check *)
864 let (_, oldt,_) = CicUtil.lookup_subst n subst in
865 let lifted_oldt = S.subst_meta l oldt in
866 fo_unif_subst_ordered
867 test_equality_only subst context metasenv t lifted_oldt ugraph2
869 CicUtil.Subst_not_found _ ->
870 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
871 let subst = (n, (context, t'',ty)) :: subst in
873 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
874 subst, metasenv, ugraph2
876 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
877 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
878 if UriManager.eq uri1 uri2 then
879 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
880 exp_named_subst1 exp_named_subst2 ugraph
882 raise (UnificationFailure (lazy
884 "Can't unify %s with %s due to different constants"
885 (CicMetaSubst.ppterm ~metasenv subst t1)
886 (CicMetaSubst.ppterm ~metasenv subst t2))))
887 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
888 if UriManager.eq uri1 uri2 && i1 = i2 then
889 fo_unif_subst_exp_named_subst
891 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
893 raise (UnificationFailure
896 "Can't unify %s with %s due to different inductive principles"
897 (CicMetaSubst.ppterm ~metasenv subst t1)
898 (CicMetaSubst.ppterm ~metasenv subst t2))))
899 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
900 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
901 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
902 fo_unif_subst_exp_named_subst
904 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
906 raise (UnificationFailure
909 "Can't unify %s with %s due to different inductive constructors"
910 (CicMetaSubst.ppterm ~metasenv subst t1)
911 (CicMetaSubst.ppterm ~metasenv subst t2))))
912 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
913 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
914 subst context metasenv te t2 ugraph
915 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
916 subst context metasenv t1 te ugraph
917 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
918 let subst',metasenv',ugraph1 =
919 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
921 fo_unif_subst test_equality_only
922 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
923 | (C.LetIn (_,s1,ty1,t1), t2)
924 | (t2, C.LetIn (_,s1,ty1,t1)) ->
926 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
927 | (C.Appl l1, C.Appl l2) ->
928 (* andrea: this case should be probably rewritten in the
931 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
934 (fun (subst,metasenv,ugraph) t1 t2 ->
936 test_equality_only subst context metasenv t1 t2 ugraph)
937 (subst,metasenv,ugraph) l1 l2
938 with (Invalid_argument msg) ->
939 raise (UnificationFailure (lazy msg)))
940 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
941 (* we verify that none of the args is a Meta,
942 since beta expanding with respoect to a metavariable
946 let (_,t,_) = CicUtil.lookup_subst i subst in
947 let lifted = S.subst_meta l t in
948 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
951 subst context metasenv reduced t2 ugraph
952 with CicUtil.Subst_not_found _ -> *)
953 let subst,metasenv,beta_expanded,ugraph1 =
955 test_equality_only metasenv subst context t2 args ugraph
957 fo_unif_subst test_equality_only subst context metasenv
958 (C.Meta (i,l)) beta_expanded ugraph1
959 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
961 let (_,t,_) = CicUtil.lookup_subst i subst in
962 let lifted = S.subst_meta l t in
963 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
966 subst context metasenv t1 reduced ugraph
967 with CicUtil.Subst_not_found _ -> *)
968 let subst,metasenv,beta_expanded,ugraph1 =
971 metasenv subst context t1 args ugraph
973 fo_unif_subst test_equality_only subst context metasenv
974 (C.Meta (i,l)) beta_expanded ugraph1
976 let lr1 = List.rev l1 in
977 let lr2 = List.rev l2 in
979 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
982 | _,[] -> assert false
985 test_equality_only subst context metasenv h1 h2 ugraph
988 fo_unif_subst test_equality_only subst context metasenv
989 h (C.Appl (List.rev l)) ugraph
990 | ((h1::l1),(h2::l2)) ->
991 let subst', metasenv',ugraph1 =
994 subst context metasenv h1 h2 ugraph
997 test_equality_only subst' metasenv' (l1,l2) ugraph1
1001 test_equality_only subst metasenv (lr1, lr2) ugraph
1003 | UnificationFailure s
1004 | Uncertain s as exn ->
1007 | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
1008 (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
1009 CoercDb.is_a_coercion cc1 <> None &&
1010 CoercDb.is_a_coercion cc2 <> None &&
1011 not (UriManager.eq uri1 uri2) ->
1013 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1015 let inner_coerced t =
1016 let t = CicMetaSubst.apply_subst subst t in
1020 (match CoercGraph.coerced_arg l with
1022 | Some (t,_) -> aux (List.hd l) t t)
1025 aux (Cic.Implicit None) (Cic.Implicit None) t
1027 let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
1028 let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
1031 CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
1033 | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
1036 let head1_c, head2_c =
1038 CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
1040 | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
1043 let unfold uri ens args =
1045 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
1049 | Cic.Constant (_,Some bo,_,_,_) ->
1050 CicReduction.head_beta_reduce ~delta:false
1051 (Cic.Appl (bo::args))
1054 let conclude subst metasenv ugraph last_tl1' last_tl2' =
1055 let subst',metasenv,ugraph =
1058 ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
1059 " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
1061 fo_unif_subst test_equality_only subst context
1062 metasenv last_tl1' last_tl2' ugraph
1064 if subst = subst' then raise exn
1067 let subst,metasenv,ugrph as res =
1069 fo_unif_subst test_equality_only subst' context
1070 metasenv (C.Appl l1) (C.Appl l2) ugraph
1074 (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
1075 " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1079 if CoercDb.eq_carr car1 car2 then
1080 match last_tl1,last_tl2 with
1081 | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
1084 let subst,metasenv,ugraph =
1085 fo_unif_subst test_equality_only subst context
1086 metasenv last_tl1 last_tl2 ugraph
1088 fo_unif_subst test_equality_only subst context
1089 metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
1090 | _ when CoercDb.eq_carr head1_c head2_c ->
1091 (* composite VS composition + metas avoiding
1092 * coercions not only in coerced position *)
1093 if c1 <> cc1 && c2 <> cc2 then
1094 conclude subst metasenv ugraph
1099 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
1101 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
1103 fo_unif_subst test_equality_only subst context
1104 metasenv l1 l2 ugraph
1108 match last_tl1 with Cic.Meta _ -> true | _ -> false in
1110 match last_tl2 with Cic.Meta _ -> true | _ -> false in
1111 if not (grow1 || grow2) then
1112 (* no flexible terminals -> no pullback, but
1113 * we still unify them, in some cases it helps *)
1114 conclude subst metasenv ugraph last_tl1 last_tl2
1118 metasenv subst context (grow1,car1) (grow2,car2)
1122 | (carr,metasenv,to1,to2)::xxx ->
1123 warn_if_not_unique xxx to1 to2 carr car1 car2;
1124 let last_tl1',(subst,metasenv,ugraph) =
1125 match grow1,to1 with
1126 | true,Some (last,coerced) ->
1128 fo_unif_subst test_equality_only subst context
1129 metasenv coerced last_tl1 ugraph
1130 | _ -> last_tl1,(subst,metasenv,ugraph)
1132 let last_tl2',(subst,metasenv,ugraph) =
1133 match grow2,to2 with
1134 | true,Some (last,coerced) ->
1136 fo_unif_subst test_equality_only subst context
1137 metasenv coerced last_tl2 ugraph
1138 | _ -> last_tl2,(subst,metasenv,ugraph)
1140 conclude subst metasenv ugraph last_tl1' last_tl2')
1142 (* {{{ CSC: This is necessary because of the "elim H" tactic
1143 where the type of H is only reducible to an
1144 inductive type. This could be extended from inductive
1145 types to any rigid term. However, the code is
1146 duplicated in two places: inside applications and
1147 outside them. Probably it would be better to
1148 work with lambda-bar terms instead. *)
1149 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
1150 | (_, Cic.MutInd _::_) ->
1151 let t1' = R.whd ~subst context t1 in
1153 C.Appl (C.MutInd _::_) ->
1154 fo_unif_subst test_equality_only
1155 subst context metasenv t1' t2 ugraph
1156 | _ -> raise (UnificationFailure (lazy "88")))
1157 | (Cic.MutInd _::_,_) ->
1158 let t2' = R.whd ~subst context t2 in
1160 C.Appl (C.MutInd _::_) ->
1161 fo_unif_subst test_equality_only
1162 subst context metasenv t1 t2' ugraph
1165 (lazy ("not a mutind :"^
1166 CicMetaSubst.ppterm ~metasenv subst t2 ))))
1169 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
1170 let subst', metasenv',ugraph1 =
1171 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
1173 let subst'',metasenv'',ugraph2 =
1174 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
1178 (fun (subst,metasenv,ugraph) t1 t2 ->
1180 test_equality_only subst context metasenv t1 t2 ugraph
1181 ) (subst'',metasenv'',ugraph2) pl1 pl2
1183 Invalid_argument _ ->
1184 raise (UnificationFailure (lazy "6.1")))
1186 "Error trying to unify %s with %s: the number of branches is not the same."
1187 (CicMetaSubst.ppterm ~metasenv subst t1)
1188 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
1189 | (C.Rel _, _) | (_, C.Rel _) ->
1191 subst, metasenv,ugraph
1193 raise (UnificationFailure (lazy
1195 "Can't unify %s with %s because they are not convertible"
1196 (CicMetaSubst.ppterm ~metasenv subst t1)
1197 (CicMetaSubst.ppterm ~metasenv subst t2))))
1198 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
1199 let subst,metasenv,beta_expanded,ugraph1 =
1201 test_equality_only metasenv subst context t2 args ugraph
1203 fo_unif_subst test_equality_only subst context metasenv
1204 (C.Meta (i,l)) beta_expanded ugraph1
1205 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
1206 let subst,metasenv,beta_expanded,ugraph1 =
1208 test_equality_only metasenv subst context t1 args ugraph
1210 fo_unif_subst test_equality_only subst context metasenv
1211 beta_expanded (C.Meta (i,l)) ugraph1
1212 (* Works iff there are no arguments applied to it; similar to the
1214 | (_, C.MutInd _) ->
1215 let t1' = R.whd ~subst context t1 in
1218 fo_unif_subst test_equality_only
1219 subst context metasenv t1' t2 ugraph
1220 | _ -> raise (UnificationFailure (lazy "8")))
1222 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
1223 let subst',metasenv',ugraph1 =
1224 fo_unif_subst true subst context metasenv s1 s2 ugraph
1226 fo_unif_subst test_equality_only
1227 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1229 (match CicReduction.whd ~subst context t2 with
1231 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1232 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
1234 (match CicReduction.whd ~subst context t1 with
1236 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1237 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
1239 (* delta-beta reduction should almost never be a problem for
1241 1. long computations require iota reduction
1242 2. it is extremely rare that a close term t1 (that could be unified
1243 to t2) beta-delta reduces to t1' while t2 does not beta-delta
1244 reduces in the same way. This happens only if one meta of t2
1245 occurs in head position during beta reduction. In this unluky
1246 case too much reduction will be performed on t1 and unification
1247 will surely fail. *)
1248 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
1249 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
1250 if t1 = t1' && t2 = t2' then
1251 raise (UnificationFailure
1254 "Can't unify %s with %s because they are not convertible"
1255 (CicMetaSubst.ppterm ~metasenv subst t1)
1256 (CicMetaSubst.ppterm ~metasenv subst t2))))
1259 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
1261 UnificationFailure _
1263 raise (UnificationFailure
1266 "Can't unify %s with %s because they are not convertible"
1267 (CicMetaSubst.ppterm ~metasenv subst t1)
1268 (CicMetaSubst.ppterm ~metasenv subst t2))))
1270 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
1271 exp_named_subst1 exp_named_subst2 ugraph
1275 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
1276 assert (uri1=uri2) ;
1277 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1278 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
1280 Invalid_argument _ ->
1285 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
1288 raise (UnificationFailure (lazy (sprintf
1289 "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))))
1291 (* A substitution is a (int * Cic.term) list that associates a *)
1292 (* metavariable i with its body. *)
1293 (* metasenv is of type Cic.metasenv *)
1294 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
1295 (* a new substitution which is already unwinded and ready to be applied and *)
1296 (* a new metasenv in which some hypothesis in the contexts of the *)
1297 (* metavariables may have been restricted. *)
1298 let fo_unif metasenv context t1 t2 ugraph =
1299 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
1301 let enrich_msg msg subst context metasenv t1 t2 ugraph =
1304 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"
1305 (CicMetaSubst.ppterm ~metasenv subst t1)
1307 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1310 | UnificationFailure s
1312 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1313 (CicMetaSubst.ppterm ~metasenv subst t2)
1315 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1318 | UnificationFailure s
1320 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1321 (CicMetaSubst.ppcontext ~metasenv subst context)
1322 (CicMetaSubst.ppmetasenv subst metasenv)
1323 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
1325 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
1326 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
1328 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1329 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
1331 | UnificationFailure s
1333 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1334 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
1336 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1337 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
1339 | UnificationFailure s
1341 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1342 (CicMetaSubst.ppcontext ~metasenv subst context)
1343 (CicMetaSubst.ppmetasenv subst metasenv)
1347 let fo_unif_subst subst context metasenv t1 t2 ugraph =
1349 fo_unif_subst false subst context metasenv t1 t2 ugraph
1351 | AssertFailure msg ->
1352 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1353 | UnificationFailure msg ->
1354 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))