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 NCicUtils.does_not_occur 0 1 (NCic.Appl (List.tail (List.rev l2)))
50 let rec all_but_last check_last = function
53 | [_] -> if check_last then raise WrongShape else []
54 | he::tl -> he::(all_but_last check_last tl)
56 let all_but_last check_last l =
57 match all_but_last check_last l with
62 let impossible_term = NCic.Rel ~-1 in
63 let t = NCicSubstitution.subst impossible_term (all_but_last true l2) in
64 let all_but_last = all_but_last false l1 in
65 if t = all_but_last then all_but_last else after_beta_expansion
66 | _ -> after_beta_expansion
67 with WrongShape -> after_beta_expansion
70 let rec beta_expand num test_eq_only swap metasenv subst context t arg =
71 let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
74 unify test_eq_only metasenv subst context
75 (NCicSubstitution.lift n arg) t'
77 (metasenv, subst), C.Rel (1 + n)
78 with Uncertain _ | UnificationFailure _ ->
81 (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
82 (* andrea: in general, beta_expand can create badly typed
83 terms. This happens quite seldom in practice, UNLESS we
84 iterate on the local context. For this reason, we renounce
85 to iterate and just lift *)
86 | NCic.Meta (i,(shift,lc)) ->
87 (metasenv,subst), NCic.Meta (i,(shift+1,lc))
88 | NCic.Prod (name, src, tgt) as orig ->
89 let (metasenv, subst), src1 = aux (n,context,true) acc src in
90 let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
91 let (metasenv,subst), tgt1 = aux k (metasenv, subst) tgt in
92 if src == src1 && tgt == tgt1 then orig else
93 NCic.Prod (name, src1, tgt1)
95 NCicUntrusted.map_term_fold_a
96 (fun e (n,ctx) -> n+1,e::ctx) k aux acc t
99 let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
100 let fresh_name = "Hbeta" ^ string_of_int num in
101 let (metasenv,subst,_), t1 =
102 aux (0, context, test_eq_only) (metasenv, subst) t in
103 let t2 = eta_reduce (C.Lambda (fresh_name,argty,t1)) t1 t in
106 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
107 let _, subst, metasenv, hd =
109 (fun arg (num,subst,metasenv,t) ->
110 let subst, metasenv, t =
111 beta_expand num test_equality_only metasenv subst context t arg
113 num+1,subst,metasenv,t)
114 args (1,subst,metasenv,t)
118 and instantiate test_eq_only metasenv subst context n lc t swap =
119 let unif m s c t1 t2 =
120 if swap then unify m s c t2 t1 else unify m s c t1 t2
123 try NCicTypeChecker.typeof ~subst ~metasenv context t
124 with NCicTypeChecker.TypeCheckerFailure _ -> assert false
126 let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
127 let ty = NCicSubstitution.subst_meta lc ty in
128 let metasenv, subst = unify metasenv susbt context ty ty_t in
129 let (metasenv, subst), t =
130 NCicMetaSubst.delift metasenv subst context n lc t
132 (* Unifying the types may have already instantiated n. *)
134 let _, _,oldt,_ = CicUtil.lookup_subst n subst in
135 let oldt = NCicSubstitution.subst_meta lc oldt in
136 (* conjecture: always fail --> occur check *)
137 unify test_eq_only metasenv subst context oldt t
138 with CicUtil.Subst_not_found _ ->
139 (* by cumulativity when unify(?,Type_i)
140 * we could ? := Type_j with j <= i... *)
141 let subst = (n, (name, ctx, t, ty)) :: subst in
143 List.filter (fun (m,_) -> not (n = m)) metasenv
147 and unify metasenv subst context t1 t2 =
148 let rec aux test_eq_only metasenv subst context t1 t2 =
149 let fo_unif test_eq_only metasenv subst t1 t2 =
154 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
155 if NCicEnvironment.universe_leq a b then metasenv, subst
156 else raise (fail_exc metasenv subst context t1 t2)
157 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
158 if NCicEnvironment.universe_eq a b then metasenv, subst
159 else raise (fail_exc metasenv subst context t1 t2)
160 | (C.Sort C.Prop,C.Sort (C.Type _)) ->
161 if (not test_eq_only) then metasenv, subst
162 else raise (fail_exc metasenv subst context t1 t2)
164 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
165 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
166 let metasenv, subst = aux true metasenv subst context s1 s2 in
167 aux test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
168 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
169 let metasenv,subst=aux test_eq_only metasenv subst context ty1 ty2 in
170 let metasenv,subst=aux test_eq_only metasenv subst context s1 s2 in
171 let context = (name1, C.Def (s1,ty1))::context in
172 aux test_eq_only metasenv subst context t1 t2
174 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
176 let l1 = NCicUtils.expand_local_context l1 in
177 let l2 = NCicUtils.expand_local_context l2 in
178 let metasenv, subst, to_restrict, _ =
180 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
182 aux test_eq_only metasenv subst context
183 (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2),
185 with UnificationFailure _ | Uncertain _ ->
186 metasenv, subst, i::to_restrict, i-1)
187 l1 l2 (metasenv, subst, [], List.length l1)
189 let metasenv, subst, _ =
190 NCicMetaSubst.restrict metasenv subst n1 to_restrict
194 | Invalid_argument _ -> assert false
195 | NCicMetaSubst.MetaSubstFailure msg ->
197 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
198 let term1 = NCicSubstitution.subst_meta lc1 term in
199 let term2 = NCicSubstitution.subst_meta lc2 term in
200 aux test_eq_only metasenv subst context term1 term2
201 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
203 | C.Meta (n,lc), t ->
205 let _,_,term,_ = NCicUtils.lookup_subst n subst in
206 let term = NCicSubstitution.subst_meta lc term in
207 aux test_eq_only metasenv subst context term t
208 with NCicUtils.Subst_not_found _->
209 instantiate test_eq_only metasenv subst context n lc t false
211 | t, C.Meta (n,lc) ->
213 let _,_,term,_ = NCicUtils.lookup_subst n subst in
214 let term = NCicSubstitution.subst_meta lc term in
215 aux test_eq_only metasenv subst context t term
216 with NCicUtils.Subst_not_found _->
217 instantiate test_eq_only metasenv subst context n lc t true
219 | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
220 let _,_,term,_ = NCicUtils.lookup_subst i subst in
221 let term = NCicSubstitution.subst_meta l term in
222 aux test_eq_only metasenv subst context (mk_appl term args) t2
224 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
225 let _,_,term,_ = NCicUtils.lookup_subst i subst in
226 let term = NCicSubstitution.subst_meta l term in
227 aux test_eq_only metasenv subst context t1 (mk_appl term args)
229 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
230 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
233 (fun (metasenv, subst) t1 t2 ->
234 aux test_eq_only metasenv subst context t1 t2)
235 (metasenv,subst) l1 l2
236 with Invalid_argument _ ->
237 raise (fail_exc metasenv subst context t1 t2)
239 | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
240 (* we verify that none of the args is a Meta,
241 since beta expanding w.r.t a metavariable makes no sense *)
242 let subst, metasenv, beta_expanded =
243 beta_expand_many (* passare swap *)
244 test_equality_only metasenv subst context t2 args ugraph
246 aux test_eq_only metasenv subst context
247 (C.Meta (i,l)) beta_expanded
248 | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
249 let subst,metasenv,beta_expanded =
252 metasenv subst context t1 args ugraph
254 fo_unif_subst test_equality_only subst context metasenv
255 (C.Meta (i,l)) beta_expanded ugraph1
258 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
259 when (Ref.eq r1 r2 &&
260 List.length (E.get_relevance r1) >= List.length tl1) ->
261 let relevance = E.get_relevance r1 in
262 let relevance = match r1 with
263 | Ref.Ref (_,Ref.Con (_,_,lno)) ->
264 let _,relevance = HExtlib.split_nth lno relevance in
265 HExtlib.mk_list false lno @ relevance
268 let fail = ref ~-1 in
270 HExtlib.list_forall_default3
271 (fun t1 t2 b -> fail := !fail+1; not b || aux test_eq_only context t1 t2)
272 tl1 tl2 true relevance
273 with Invalid_argument _ -> false)
277 let relevance = get_relevance_p ~subst context _hd1 tl1 in
278 let _,relevance = HExtlib.split_nth !fail relevance in
279 let b,relevance = (match relevance with
282 let _,tl1 = HExtlib.split_nth (!fail+1) tl1 in
283 let _,tl2 = HExtlib.split_nth (!fail+1) tl2 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.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
293 aux test_eq_only context hd1 hd2 &&
294 let relevance = get_relevance ~subst context hd1 tl1 in
296 HExtlib.list_forall_default3
297 (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
298 tl1 tl2 true relevance
299 with Invalid_argument _ -> false)
301 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
302 C.Match (ref2,outtype2,term2,pl2)) ->
303 let _,_,itl,_,_ = E.get_checked_indtys ref1 in
304 let _,_,ty,_ = List.nth itl tyno in
305 let rec remove_prods ~subst context ty =
306 let ty = whd ~subst context ty in
309 | C.Prod (name,so,ta) ->
310 remove_prods ~subst ((name,(C.Decl so))::context) ta
314 match remove_prods ~subst [] ty with
315 | C.Sort C.Prop -> true
318 let rec remove_prods ~subst context ty =
319 let ty = whd ~subst context ty in
322 | C.Prod (name,so,ta) ->
323 remove_prods ~subst ((name,(C.Decl so))::context) ta
326 if not (Ref.eq ref1 ref2) then
327 raise (uncert_exc metasenv subst context t1 t2)
329 let metasenv, subst =
330 aux test_eq_only metasenv subst context outtype1 outtype2 in
331 let metasenv, subst =
332 try aux test_eq_only metasenv subst context term1 term2
333 with UnificationFailure _ | Uncertain _ when is_prop ->
338 (fun (metasenv,subst) -> aux test_eq_only metasenv subst context)
339 (metasenv, subst) pl1 pl2
340 with Invalid_argument _ ->
341 raise (uncert_exc metasenv subst context t1 t2)
342 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
343 | _ -> raise (uncert_exc metasenv subst context t1 t2)
345 let rec unif_machines metasenv subst = function
346 | ((k1,e1,NCic.Meta _ as t1,s1 as m1),(k2,e2,t2,s2 as m2),delta)
347 | ((k1,e1,t1,s1 as m1),(k2,e2,NCic.Meta _ as t2,s2 as m2),delta) ->
349 fo_unif test_eq_only metasenv subst (R.unwind m1) (R.unwind m2)
350 with UnificationFailure _ | Uncertain _ when delta > 0 ->
351 let delta = delta - 1 in
352 let red = R.reduce ~delta ~subst context in
353 unif_machines metasenv subst (red m1,red m2,delta)
354 | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) ->
356 let metasenv, subst =
357 fo_unif test_eq_only metasenv subst
358 (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[]))
362 | C.Const r -> NCicEnvironment.get_relevance r
365 let rec check_stack f l1 l2 r a =
367 | x1::tl1, x2::tl2, r::tr ->
368 check_stack f tl1 tl2 tr (f x1 x2 r a)
369 | x1::tl1, x2::tl2, [] ->
370 check_stack f tl1 tl2 tr (f x1 x2 true a)
372 | _ -> raise (Invalid_argument "check_stack")
375 (fun t1 t2 b (metasenv,subst) ->
377 let t1 = RS.from_stack t1 in
378 let t2 = RS.from_stack t2 in
379 unif_machines metasenv subst (small_delta_step t1 t2)
380 with UnificationFailure _ | Uncertain _ when not b ->
382 s1 s2 relevance (metasenv,subst)
383 with Invalid_argument _ ->
384 raise (UnificationFailure (lazy ( "Can't unify " ^ NCicPp.ppterm
385 ~metasenv ~subst ~context (R.unwind m1) ^ " with " ^ NCicPp.ppterm
386 ~metasenv ~subst ~context (R.unwind m2))))
387 with UnificationFailure _ | Uncertain _ when delta > 0 ->
388 let delta = delta - 1 in
389 let red = R.reduce ~delta ~subst context in
390 unif_machines metasenv subst (red m1,red m2,delta)
392 let height_of = function
393 | NCic.Const (Ref.Ref (_,Ref.Def h))
394 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
395 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
396 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
397 | NCic.Meta _ -> max_int
400 let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
401 let h1 = height_of t1 in
402 let h2 = height_of t2 in
403 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
404 R.reduce ~delta ~subst context m1,
405 R.reduce ~delta ~subst context m2,
408 try fo_unif test_eq_only metasenv subst t1 t2
409 with UnificationFailure msg |Uncertain msg as exn ->
411 unif_machines metasenv subst
412 (small_delta_step (0,[],t1,[]) (0,[],t2,[]))
414 | UnificationFailure _ -> raise (UnificationFailure msg)
415 | Uncertain _ -> raise exn
417 aux false metasenv subst context t1 t2
426 exception UnificationFailure of string Lazy.t;;
427 exception Uncertain of string Lazy.t;;
428 exception AssertFailure of string Lazy.t;;
430 let verbose = false;;
431 let debug_print = fun _ -> ()
433 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
434 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
435 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
436 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
438 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
440 let type_of_aux' metasenv subst context term ugraph =
443 profile.HExtlib.profile
444 (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
446 CicTypeChecker.TypeCheckerFailure msg ->
450 "Kernel Type checking error:
451 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
452 (CicMetaSubst.ppterm ~metasenv subst term)
453 (CicMetaSubst.ppterm ~metasenv [] term)
454 (CicMetaSubst.ppcontext ~metasenv subst context)
455 (CicMetaSubst.ppmetasenv subst metasenv)
456 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
457 raise (AssertFailure msg)
458 | CicTypeChecker.AssertFailure msg ->
461 "Kernel Type checking assertion failure:
462 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
463 (CicMetaSubst.ppterm ~metasenv subst term)
464 (CicMetaSubst.ppterm ~metasenv [] term)
465 (CicMetaSubst.ppcontext ~metasenv subst context)
466 (CicMetaSubst.ppmetasenv subst metasenv)
467 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
468 raise (AssertFailure msg)
469 in profiler_toa.HExtlib.profile foo ()
472 let exists_a_meta l =
476 | Cic.Appl (Cic.Meta _::_) -> true
479 let rec deref subst t =
480 let snd (_,a,_) = a in
485 (CicSubstitution.subst_meta
486 l (snd (CicUtil.lookup_subst n subst)))
488 CicUtil.Subst_not_found _ -> t)
489 | Cic.Appl(Cic.Meta(n,l)::args) ->
490 (match deref subst (Cic.Meta(n,l)) with
491 | Cic.Lambda _ as t ->
492 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
493 | r -> Cic.Appl(r::args))
494 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
495 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
500 let foo () = deref subst t
501 in profiler_deref.HExtlib.profile foo ()
503 exception WrongShape;;
504 let eta_reduce after_beta_expansion after_beta_expansion_body
505 before_beta_expansion
508 match before_beta_expansion,after_beta_expansion_body with
509 Cic.Appl l, Cic.Appl l' ->
510 let rec all_but_last check_last =
514 | [_] -> if check_last then raise WrongShape else []
515 | he::tl -> he::(all_but_last check_last tl)
517 let all_but_last check_last l =
518 match all_but_last check_last l with
523 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
524 let all_but_last = all_but_last false l in
525 (* here we should test alpha-equivalence; however we know by
526 construction that here alpha_equivalence is equivalent to = *)
527 if t = all_but_last then
531 | _,_ -> after_beta_expansion
533 WrongShape -> after_beta_expansion
535 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
536 let module S = CicSubstitution in
537 let module C = Cic in
539 let rec aux metasenv subst n context t' ugraph =
542 let subst,metasenv,ugraph1 =
543 fo_unif_subst test_equality_only subst context metasenv
544 (CicSubstitution.lift n arg) t' ugraph
547 subst,metasenv,C.Rel (1 + n),ugraph1
550 | UnificationFailure _ ->
552 | C.Rel m -> subst,metasenv,
553 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
554 | C.Var (uri,exp_named_subst) ->
555 let subst,metasenv,exp_named_subst',ugraph1 =
556 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
558 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
560 (* andrea: in general, beta_expand can create badly typed
561 terms. This happens quite seldom in practice, UNLESS we
562 iterate on the local context. For this reason, we renounce
563 to iterate and just lift *)
567 Some t -> Some (CicSubstitution.lift 1 t)
569 subst, metasenv, C.Meta (i,l), ugraph
571 | C.Implicit _ as t -> subst,metasenv,t,ugraph
573 let subst,metasenv,te',ugraph1 =
574 aux metasenv subst n context te ugraph in
575 let subst,metasenv,ty',ugraph2 =
576 aux metasenv subst n context ty ugraph1 in
577 (* TASSI: sure this is in serial? *)
578 subst,metasenv,(C.Cast (te', ty')),ugraph2
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
586 (* TASSI: sure this is in serial? *)
587 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
588 | C.Lambda (nn,s,t) ->
589 let subst,metasenv,s',ugraph1 =
590 aux metasenv subst n context s ugraph in
591 let subst,metasenv,t',ugraph2 =
592 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
594 (* TASSI: sure this is in serial? *)
595 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
596 | C.LetIn (nn,s,ty,t) ->
597 let subst,metasenv,s',ugraph1 =
598 aux metasenv subst n context s ugraph in
599 let subst,metasenv,ty',ugraph1 =
600 aux metasenv subst n context ty ugraph in
601 let subst,metasenv,t',ugraph2 =
602 aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
605 (* TASSI: sure this is in serial? *)
606 subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
608 let subst,metasenv,revl',ugraph1 =
610 (fun (subst,metasenv,appl,ugraph) t ->
611 let subst,metasenv,t',ugraph1 =
612 aux metasenv subst n context t ugraph in
613 subst,metasenv,(t'::appl),ugraph1
614 ) (subst,metasenv,[],ugraph) l
616 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
617 | C.Const (uri,exp_named_subst) ->
618 let subst,metasenv,exp_named_subst',ugraph1 =
619 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
621 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
622 | C.MutInd (uri,i,exp_named_subst) ->
623 let subst,metasenv,exp_named_subst',ugraph1 =
624 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
626 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
627 | C.MutConstruct (uri,i,j,exp_named_subst) ->
628 let subst,metasenv,exp_named_subst',ugraph1 =
629 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
631 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
632 | C.MutCase (sp,i,outt,t,pl) ->
633 let subst,metasenv,outt',ugraph1 =
634 aux metasenv subst n context outt ugraph in
635 let subst,metasenv,t',ugraph2 =
636 aux metasenv subst n context t ugraph1 in
637 let subst,metasenv,revpl',ugraph3 =
639 (fun (subst,metasenv,pl,ugraph) t ->
640 let subst,metasenv,t',ugraph1 =
641 aux metasenv subst n context t ugraph in
642 subst,metasenv,(t'::pl),ugraph1
643 ) (subst,metasenv,[],ugraph2) pl
645 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
646 (* TASSI: not sure this is serial *)
648 (*CSC: not implemented
649 let tylen = List.length fl in
652 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
655 C.Fix (i, substitutedfl)
657 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
659 (*CSC: not implemented
660 let tylen = List.length fl in
663 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
666 C.CoFix (i, substitutedfl)
669 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
671 and aux_exp_named_subst metasenv subst n context ens ugraph =
673 (fun (uri,t) (subst,metasenv,l,ugraph) ->
674 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
675 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
677 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
679 FreshNamesGenerator.mk_fresh_name ~subst
680 metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
682 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
683 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
684 subst, metasenv, t'', ugraph2
685 in profiler_beta_expand.HExtlib.profile foo ()
688 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
689 let _,subst,metasenv,hd,ugraph =
691 (fun arg (num,subst,metasenv,t,ugraph) ->
692 let subst,metasenv,t,ugraph1 =
693 beta_expand num test_equality_only
694 metasenv subst context t arg ugraph
696 num+1,subst,metasenv,t,ugraph1
697 ) args (1,subst,metasenv,t,ugraph)
699 subst,metasenv,hd,ugraph
701 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
704 | (m2,_,c2,c2')::_ ->
705 let m1,c1,c1' = carr,to1,to2 in
707 function Some (_,t) -> CicPp.ppterm t
711 ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
712 CoercDb.string_of_carr car2^": " ^
713 CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
714 unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
715 unopt c2^" + "^unopt c2')
717 (* NUOVA UNIFICAZIONE *)
718 (* A substitution is a (int * Cic.term) list that associates a
719 metavariable i with its body.
720 A metaenv is a (int * Cic.term) list that associate a metavariable
722 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
723 a new substitution which is _NOT_ unwinded. It must be unwinded before
726 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
727 let module C = Cic in
728 let module R = CicReduction in
729 let module S = CicSubstitution in
730 let t1 = deref subst t1 in
731 let t2 = deref subst t2 in
732 let (&&&) a b = (a && b) || ((not a) && (not b)) in
733 (* let bef = Sys.time () in *)
735 if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
739 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
740 in profiler_are_convertible.HExtlib.profile foo ()
742 (* let aft = Sys.time () in
743 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
744 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
745 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
747 subst, metasenv, ugraph
750 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
751 let _,subst,metasenv,ugraph1 =
754 (fun (j,subst,metasenv,ugraph) t1 t2 ->
757 | _,None -> j+1,subst,metasenv,ugraph
758 | Some t1', Some t2' ->
759 (* First possibility: restriction *)
760 (* Second possibility: unification *)
761 (* Third possibility: convertibility *)
764 ~subst ~metasenv context t1' t2' ugraph
767 j+1,subst,metasenv, ugraph1
770 let subst,metasenv,ugraph2 =
773 subst context metasenv t1' t2' ugraph
775 j+1,subst,metasenv,ugraph2
778 | UnificationFailure _ ->
779 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
780 let metasenv, subst =
781 CicMetaSubst.restrict
782 subst [(n,j)] metasenv in
783 j+1,subst,metasenv,ugraph1)
784 ) (1,subst,metasenv,ugraph) ln lm
788 (UnificationFailure (lazy "1"))
791 "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."
792 (CicMetaSubst.ppterm ~metasenv subst t1)
793 (CicMetaSubst.ppterm ~metasenv subst t2))) *)
794 | Invalid_argument _ ->
796 (UnificationFailure (lazy "2")))
799 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
800 (CicMetaSubst.ppterm ~metasenv subst t1)
801 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
802 in subst,metasenv,ugraph1
803 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
804 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
806 | (t, C.Meta (n,l)) ->
809 C.Meta (n,_), C.Meta (m,_) when n < m -> false
810 | _, C.Meta _ -> false
813 let lower = fun x y -> if swap then y else x in
814 let upper = fun x y -> if swap then x else y in
815 let fo_unif_subst_ordered
816 test_equality_only subst context metasenv m1 m2 ugraph =
817 fo_unif_subst test_equality_only subst context metasenv
818 (lower m1 m2) (upper m1 m2) ugraph
821 let subst,metasenv,ugraph1 =
822 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
825 type_of_aux' metasenv subst context t ugraph
829 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
831 UnificationFailure _ as e -> raise e
832 | Uncertain msg -> raise (UnificationFailure msg)
834 debug_print (lazy "siamo allo huge hack");
835 (* TODO huge hack!!!!
836 * we keep on unifying/refining in the hope that
837 * the problem will be eventually solved.
838 * In the meantime we're breaking a big invariant:
839 * the terms that we are unifying are no longer well
840 * typed in the current context (in the worst case
841 * we could even diverge) *)
842 (subst, metasenv,ugraph)) in
843 let t',metasenv,subst =
845 CicMetaSubst.delift n subst context metasenv l t
847 (CicMetaSubst.MetaSubstFailure msg)->
848 raise (UnificationFailure msg)
849 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
853 C.Sort (C.Type u) when not test_equality_only ->
854 let u' = CicUniv.fresh () in
855 let s = C.Sort (C.Type u') in
858 CicUniv.add_ge (upper u u') (lower u u') ugraph1
862 CicUniv.UniverseInconsistency msg ->
863 raise (UnificationFailure msg))
866 (* Unifying the types may have already instantiated n. Let's check *)
868 let (_, oldt,_) = CicUtil.lookup_subst n subst in
869 let lifted_oldt = S.subst_meta l oldt in
870 fo_unif_subst_ordered
871 test_equality_only subst context metasenv t lifted_oldt ugraph2
873 CicUtil.Subst_not_found _ ->
874 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
875 let subst = (n, (context, t'',ty)) :: subst in
877 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
878 subst, metasenv, ugraph2
880 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
881 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
882 if UriManager.eq uri1 uri2 then
883 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
884 exp_named_subst1 exp_named_subst2 ugraph
886 raise (UnificationFailure (lazy
888 "Can't unify %s with %s due to different constants"
889 (CicMetaSubst.ppterm ~metasenv subst t1)
890 (CicMetaSubst.ppterm ~metasenv subst t2))))
891 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
892 if UriManager.eq uri1 uri2 && i1 = i2 then
893 fo_unif_subst_exp_named_subst
895 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
897 raise (UnificationFailure
900 "Can't unify %s with %s due to different inductive principles"
901 (CicMetaSubst.ppterm ~metasenv subst t1)
902 (CicMetaSubst.ppterm ~metasenv subst t2))))
903 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
904 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
905 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
906 fo_unif_subst_exp_named_subst
908 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
910 raise (UnificationFailure
913 "Can't unify %s with %s due to different inductive constructors"
914 (CicMetaSubst.ppterm ~metasenv subst t1)
915 (CicMetaSubst.ppterm ~metasenv subst t2))))
916 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
917 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
918 subst context metasenv te t2 ugraph
919 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
920 subst context metasenv t1 te ugraph
921 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
922 let subst',metasenv',ugraph1 =
923 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
925 fo_unif_subst test_equality_only
926 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
927 | (C.LetIn (_,s1,ty1,t1), t2)
928 | (t2, C.LetIn (_,s1,ty1,t1)) ->
930 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
931 | (C.Appl l1, C.Appl l2) ->
932 (* andrea: this case should be probably rewritten in the
935 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
938 (fun (subst,metasenv,ugraph) t1 t2 ->
940 test_equality_only subst context metasenv t1 t2 ugraph)
941 (subst,metasenv,ugraph) l1 l2
942 with (Invalid_argument msg) ->
943 raise (UnificationFailure (lazy msg)))
944 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
945 (* we verify that none of the args is a Meta,
946 since beta expanding with respoect to a metavariable
950 let (_,t,_) = CicUtil.lookup_subst i subst in
951 let lifted = S.subst_meta l t in
952 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
955 subst context metasenv reduced t2 ugraph
956 with CicUtil.Subst_not_found _ -> *)
957 let subst,metasenv,beta_expanded,ugraph1 =
959 test_equality_only metasenv subst context t2 args ugraph
961 fo_unif_subst test_equality_only subst context metasenv
962 (C.Meta (i,l)) beta_expanded ugraph1
963 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
965 let (_,t,_) = CicUtil.lookup_subst i subst in
966 let lifted = S.subst_meta l t in
967 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
970 subst context metasenv t1 reduced ugraph
971 with CicUtil.Subst_not_found _ -> *)
972 let subst,metasenv,beta_expanded,ugraph1 =
975 metasenv subst context t1 args ugraph
977 fo_unif_subst test_equality_only subst context metasenv
978 (C.Meta (i,l)) beta_expanded ugraph1
980 let lr1 = List.rev l1 in
981 let lr2 = List.rev l2 in
983 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
986 | _,[] -> assert false
989 test_equality_only subst context metasenv h1 h2 ugraph
992 fo_unif_subst test_equality_only subst context metasenv
993 h (C.Appl (List.rev l)) ugraph
994 | ((h1::l1),(h2::l2)) ->
995 let subst', metasenv',ugraph1 =
998 subst context metasenv h1 h2 ugraph
1001 test_equality_only subst' metasenv' (l1,l2) ugraph1
1005 test_equality_only subst metasenv (lr1, lr2) ugraph
1007 | UnificationFailure s
1008 | Uncertain s as exn ->
1011 | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
1012 (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
1013 CoercDb.is_a_coercion cc1 <> None &&
1014 CoercDb.is_a_coercion cc2 <> None &&
1015 not (UriManager.eq uri1 uri2) ->
1017 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1019 let inner_coerced t =
1020 let t = CicMetaSubst.apply_subst subst t in
1024 (match CoercGraph.coerced_arg l with
1026 | Some (t,_) -> aux (List.hd l) t t)
1029 aux (Cic.Implicit None) (Cic.Implicit None) t
1031 let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
1032 let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
1035 CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
1037 | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
1040 let head1_c, head2_c =
1042 CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
1044 | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
1047 let unfold uri ens args =
1049 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
1053 | Cic.Constant (_,Some bo,_,_,_) ->
1054 CicReduction.head_beta_reduce ~delta:false
1055 (Cic.Appl (bo::args))
1058 let conclude subst metasenv ugraph last_tl1' last_tl2' =
1059 let subst',metasenv,ugraph =
1062 ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
1063 " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
1065 fo_unif_subst test_equality_only subst context
1066 metasenv last_tl1' last_tl2' ugraph
1068 if subst = subst' then raise exn
1071 let subst,metasenv,ugrph as res =
1073 fo_unif_subst test_equality_only subst' context
1074 metasenv (C.Appl l1) (C.Appl l2) ugraph
1078 (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
1079 " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1083 if CoercDb.eq_carr car1 car2 then
1084 match last_tl1,last_tl2 with
1085 | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
1088 let subst,metasenv,ugraph =
1089 fo_unif_subst test_equality_only subst context
1090 metasenv last_tl1 last_tl2 ugraph
1092 fo_unif_subst test_equality_only subst context
1093 metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
1094 | _ when CoercDb.eq_carr head1_c head2_c ->
1095 (* composite VS composition + metas avoiding
1096 * coercions not only in coerced position *)
1097 if c1 <> cc1 && c2 <> cc2 then
1098 conclude subst metasenv ugraph
1103 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
1105 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
1107 fo_unif_subst test_equality_only subst context
1108 metasenv l1 l2 ugraph
1112 match last_tl1 with Cic.Meta _ -> true | _ -> false in
1114 match last_tl2 with Cic.Meta _ -> true | _ -> false in
1115 if not (grow1 || grow2) then
1116 (* no flexible terminals -> no pullback, but
1117 * we still unify them, in some cases it helps *)
1118 conclude subst metasenv ugraph last_tl1 last_tl2
1122 metasenv subst context (grow1,car1) (grow2,car2)
1126 | (carr,metasenv,to1,to2)::xxx ->
1127 warn_if_not_unique xxx to1 to2 carr car1 car2;
1128 let last_tl1',(subst,metasenv,ugraph) =
1129 match grow1,to1 with
1130 | true,Some (last,coerced) ->
1132 fo_unif_subst test_equality_only subst context
1133 metasenv coerced last_tl1 ugraph
1134 | _ -> last_tl1,(subst,metasenv,ugraph)
1136 let last_tl2',(subst,metasenv,ugraph) =
1137 match grow2,to2 with
1138 | true,Some (last,coerced) ->
1140 fo_unif_subst test_equality_only subst context
1141 metasenv coerced last_tl2 ugraph
1142 | _ -> last_tl2,(subst,metasenv,ugraph)
1144 conclude subst metasenv ugraph last_tl1' last_tl2')
1146 (* {{{ CSC: This is necessary because of the "elim H" tactic
1147 where the type of H is only reducible to an
1148 inductive type. This could be extended from inductive
1149 types to any rigid term. However, the code is
1150 duplicated in two places: inside applications and
1151 outside them. Probably it would be better to
1152 work with lambda-bar terms instead. *)
1153 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
1154 | (_, Cic.MutInd _::_) ->
1155 let t1' = R.whd ~subst context t1 in
1157 C.Appl (C.MutInd _::_) ->
1158 fo_unif_subst test_equality_only
1159 subst context metasenv t1' t2 ugraph
1160 | _ -> raise (UnificationFailure (lazy "88")))
1161 | (Cic.MutInd _::_,_) ->
1162 let t2' = R.whd ~subst context t2 in
1164 C.Appl (C.MutInd _::_) ->
1165 fo_unif_subst test_equality_only
1166 subst context metasenv t1 t2' ugraph
1169 (lazy ("not a mutind :"^
1170 CicMetaSubst.ppterm ~metasenv subst t2 ))))
1173 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
1174 let subst', metasenv',ugraph1 =
1175 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
1177 let subst'',metasenv'',ugraph2 =
1178 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
1182 (fun (subst,metasenv,ugraph) t1 t2 ->
1184 test_equality_only subst context metasenv t1 t2 ugraph
1185 ) (subst'',metasenv'',ugraph2) pl1 pl2
1187 Invalid_argument _ ->
1188 raise (UnificationFailure (lazy "6.1")))
1190 "Error trying to unify %s with %s: the number of branches is not the same."
1191 (CicMetaSubst.ppterm ~metasenv subst t1)
1192 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
1193 | (C.Rel _, _) | (_, C.Rel _) ->
1195 subst, metasenv,ugraph
1197 raise (UnificationFailure (lazy
1199 "Can't unify %s with %s because they are not convertible"
1200 (CicMetaSubst.ppterm ~metasenv subst t1)
1201 (CicMetaSubst.ppterm ~metasenv subst t2))))
1202 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
1203 let subst,metasenv,beta_expanded,ugraph1 =
1205 test_equality_only metasenv subst context t2 args ugraph
1207 fo_unif_subst test_equality_only subst context metasenv
1208 (C.Meta (i,l)) beta_expanded ugraph1
1209 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
1210 let subst,metasenv,beta_expanded,ugraph1 =
1212 test_equality_only metasenv subst context t1 args ugraph
1214 fo_unif_subst test_equality_only subst context metasenv
1215 beta_expanded (C.Meta (i,l)) ugraph1
1216 (* Works iff there are no arguments applied to it; similar to the
1218 | (_, C.MutInd _) ->
1219 let t1' = R.whd ~subst context t1 in
1222 fo_unif_subst test_equality_only
1223 subst context metasenv t1' t2 ugraph
1224 | _ -> raise (UnificationFailure (lazy "8")))
1226 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
1227 let subst',metasenv',ugraph1 =
1228 fo_unif_subst true subst context metasenv s1 s2 ugraph
1230 fo_unif_subst test_equality_only
1231 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1233 (match CicReduction.whd ~subst context t2 with
1235 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1236 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
1238 (match CicReduction.whd ~subst context t1 with
1240 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1241 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
1243 (* delta-beta reduction should almost never be a problem for
1245 1. long computations require iota reduction
1246 2. it is extremely rare that a close term t1 (that could be unified
1247 to t2) beta-delta reduces to t1' while t2 does not beta-delta
1248 reduces in the same way. This happens only if one meta of t2
1249 occurs in head position during beta reduction. In this unluky
1250 case too much reduction will be performed on t1 and unification
1251 will surely fail. *)
1252 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
1253 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
1254 if t1 = t1' && t2 = t2' then
1255 raise (UnificationFailure
1258 "Can't unify %s with %s because they are not convertible"
1259 (CicMetaSubst.ppterm ~metasenv subst t1)
1260 (CicMetaSubst.ppterm ~metasenv subst t2))))
1263 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
1265 UnificationFailure _
1267 raise (UnificationFailure
1270 "Can't unify %s with %s because they are not convertible"
1271 (CicMetaSubst.ppterm ~metasenv subst t1)
1272 (CicMetaSubst.ppterm ~metasenv subst t2))))
1274 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
1275 exp_named_subst1 exp_named_subst2 ugraph
1279 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
1280 assert (uri1=uri2) ;
1281 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1282 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
1284 Invalid_argument _ ->
1289 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
1292 raise (UnificationFailure (lazy (sprintf
1293 "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))))
1295 (* A substitution is a (int * Cic.term) list that associates a *)
1296 (* metavariable i with its body. *)
1297 (* metasenv is of type Cic.metasenv *)
1298 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
1299 (* a new substitution which is already unwinded and ready to be applied and *)
1300 (* a new metasenv in which some hypothesis in the contexts of the *)
1301 (* metavariables may have been restricted. *)
1302 let fo_unif metasenv context t1 t2 ugraph =
1303 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
1305 let enrich_msg msg subst context metasenv t1 t2 ugraph =
1308 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"
1309 (CicMetaSubst.ppterm ~metasenv subst t1)
1311 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1314 | UnificationFailure s
1316 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1317 (CicMetaSubst.ppterm ~metasenv subst t2)
1319 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1322 | UnificationFailure s
1324 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1325 (CicMetaSubst.ppcontext ~metasenv subst context)
1326 (CicMetaSubst.ppmetasenv subst metasenv)
1327 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
1329 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
1330 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
1332 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1333 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
1335 | UnificationFailure s
1337 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1338 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
1340 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1341 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
1343 | UnificationFailure s
1345 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1346 (CicMetaSubst.ppcontext ~metasenv subst context)
1347 (CicMetaSubst.ppmetasenv subst metasenv)
1351 let fo_unif_subst subst context metasenv t1 t2 ugraph =
1353 fo_unif_subst false subst context metasenv t1 t2 ugraph
1355 | AssertFailure msg ->
1356 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1357 | UnificationFailure msg ->
1358 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))