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 uncert_exc metasenv subst context t1 t2 =
22 "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
23 " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
26 let fail_exc metasenv subst context t1 t2 =
27 UnificationFailure (lazy (
28 "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
29 " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
34 | NCic.Appl l -> NCic.Appl (l@tl)
35 | _ -> NCic.Appl (hd :: tl)
42 | NCic.Appl (NCic.Meta _::_) -> true
46 exception WrongShape;;
49 let delift_if_not_occur body orig =
51 NCicSubstitution.psubst ~avoid_beta_redexes:true
52 (fun () -> raise WrongShape) [()] body
53 with WrongShape -> orig
56 | NCic.Lambda(_, _, NCic.Appl [hd; NCic.Rel 1]) as orig ->
57 delift_if_not_occur hd orig
58 | NCic.Lambda(_, _, NCic.Appl (hd :: l)) as orig
59 when HExtlib.list_last l = NCic.Rel 1 ->
61 let args, _ = HExtlib.split_nth (List.length l - 1) l in
64 delift_if_not_occur body orig
69 module Ref = NReference;;
71 let rec beta_expand num test_eq_only swap metasenv subst context t arg =
72 let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
76 unify test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
78 unify test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
80 (metasenv, subst), NCic.Rel (1 + n)
81 with Uncertain _ | UnificationFailure _ ->
83 | NCic.Rel m as orig ->
84 (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
85 (* andrea: in general, beta_expand can create badly typed
86 terms. This happens quite seldom in practice, UNLESS we
87 iterate on the local context. For this reason, we renounce
88 to iterate and just lift *)
89 | NCic.Meta (i,(shift,lc)) ->
90 (metasenv,subst), NCic.Meta (i,(shift+1,lc))
91 | NCic.Prod (name, src, tgt) as orig ->
92 let (metasenv, subst), src1 = aux (n,context,true) acc src in
93 let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
94 let ms, tgt1 = aux k (metasenv, subst) tgt in
95 if src == src1 && tgt == tgt1 then ms, orig else
96 ms, NCic.Prod (name, src1, tgt1)
98 NCicUntrusted.map_term_fold_a
99 (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t
102 let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
103 let fresh_name = "Hbeta" ^ string_of_int num in
104 let (metasenv,subst), t1 =
105 aux (0, context, test_eq_only) (metasenv, subst) t in
106 let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in
108 ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
110 with NCicTypeChecker.TypeCheckerFailure _ ->
111 metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
113 and beta_expand_many test_equality_only swap metasenv subst context t args =
114 let _, subst, metasenv, hd =
116 (fun arg (num,subst,metasenv,t) ->
117 let metasenv, subst, t =
118 beta_expand num test_equality_only swap metasenv subst context t arg
120 num+1,subst,metasenv,t)
121 args (1,subst,metasenv,t)
125 and instantiate test_eq_only metasenv subst context n lc t swap =
126 let unify test_eq_only m s c t1 t2 =
127 if swap then unify test_eq_only m s c t2 t1
128 else unify test_eq_only m s c t1 t2
131 try NCicTypeChecker.typeof ~subst ~metasenv context t
132 with NCicTypeChecker.TypeCheckerFailure _ -> assert false
134 let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
135 let ty = NCicSubstitution.subst_meta lc ty in
136 let metasenv, subst = unify test_eq_only metasenv subst context ty ty_t in
137 let (metasenv, subst), t =
138 NCicMetaSubst.delift metasenv subst context n lc t
140 (* Unifying the types may have already instantiated n. *)
142 let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
143 let oldt = NCicSubstitution.subst_meta lc oldt in
144 (* conjecture: always fail --> occur check *)
145 unify test_eq_only metasenv subst context oldt t
146 with NCicUtils.Subst_not_found _ ->
147 (* by cumulativity when unify(?,Type_i)
148 * we could ? := Type_j with j <= i... *)
149 let subst = (n, (name, ctx, t, ty)) :: subst in
151 List.filter (fun (m,_) -> not (n = m)) metasenv
155 and unify test_eq_only metasenv subst context t1 t2 =
156 let fo_unif test_eq_only metasenv subst t1 t2 =
161 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
162 if NCicEnvironment.universe_leq a b then metasenv, subst
163 else raise (fail_exc metasenv subst context t1 t2)
164 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
165 if NCicEnvironment.universe_eq a b then metasenv, subst
166 else raise (fail_exc metasenv subst context t1 t2)
167 | (C.Sort C.Prop,C.Sort (C.Type _)) ->
168 if (not test_eq_only) then metasenv, subst
169 else raise (fail_exc metasenv subst context t1 t2)
171 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
172 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
173 let metasenv, subst = unify true metasenv subst context s1 s2 in
174 unify test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
175 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
176 let metasenv,subst=unify test_eq_only metasenv subst context ty1 ty2 in
177 let metasenv,subst=unify test_eq_only metasenv subst context s1 s2 in
178 let context = (name1, C.Def (s1,ty1))::context in
179 unify test_eq_only metasenv subst context t1 t2
181 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
183 let l1 = NCicUtils.expand_local_context l1 in
184 let l2 = NCicUtils.expand_local_context l2 in
185 let metasenv, subst, to_restrict, _ =
187 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
189 let metasenv, subst =
190 unify test_eq_only metasenv subst context
191 (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
193 metasenv, subst, to_restrict, i-1
194 with UnificationFailure _ | Uncertain _ ->
195 metasenv, subst, i::to_restrict, i-1)
196 l1 l2 (metasenv, subst, [], List.length l1)
198 let metasenv, subst, _ =
199 NCicMetaSubst.restrict metasenv subst n1 to_restrict
203 | Invalid_argument _ -> assert false
204 | NCicMetaSubst.MetaSubstFailure msg ->
206 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
207 let term1 = NCicSubstitution.subst_meta lc1 term in
208 let term2 = NCicSubstitution.subst_meta lc2 term in
209 unify test_eq_only metasenv subst context term1 term2
210 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
212 | C.Meta (n,lc), t ->
214 let _,_,term,_ = NCicUtils.lookup_subst n subst in
215 let term = NCicSubstitution.subst_meta lc term in
216 unify test_eq_only metasenv subst context term t
217 with NCicUtils.Subst_not_found _->
218 instantiate test_eq_only metasenv subst context n lc t false)
220 | t, C.Meta (n,lc) ->
222 let _,_,term,_ = NCicUtils.lookup_subst n subst in
223 let term = NCicSubstitution.subst_meta lc term in
224 unify test_eq_only metasenv subst context t term
225 with NCicUtils.Subst_not_found _->
226 instantiate test_eq_only metasenv subst context n lc t true)
228 | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
229 let _,_,term,_ = NCicUtils.lookup_subst i subst in
230 let term = NCicSubstitution.subst_meta l term in
231 unify test_eq_only metasenv subst context (mk_appl term args) t2
233 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
234 let _,_,term,_ = NCicUtils.lookup_subst i subst in
235 let term = NCicSubstitution.subst_meta l term in
236 unify test_eq_only metasenv subst context t1 (mk_appl term args)
238 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
239 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
242 (fun (metasenv, subst) t1 t2 ->
243 unify test_eq_only metasenv subst context t1 t2)
244 (metasenv,subst) l1 l2
245 with Invalid_argument _ ->
246 raise (fail_exc metasenv subst context t1 t2))
248 | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
249 (* we verify that none of the args is a Meta,
250 since beta expanding w.r.t a metavariable makes no sense *)
251 let metasenv, subst, beta_expanded =
254 metasenv subst context t2 args
256 unify test_eq_only metasenv subst context
257 (C.Meta (i,l)) beta_expanded
259 | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
260 let metasenv, subst, beta_expanded =
263 metasenv subst context t1 args
265 unify test_eq_only metasenv subst context
266 beta_expanded (C.Meta (i,l))
268 (* processing this case here we avoid a useless small delta step *)
269 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
271 let relevance = NCicEnvironment.get_relevance r1 in
272 let relevance = match r1 with
273 | Ref.Ref (_,Ref.Con (_,_,lno)) ->
274 let _,relevance = HExtlib.split_nth lno relevance in
275 HExtlib.mk_list false lno @ relevance
278 let metasenv, subst, _ =
281 (fun (metasenv, subst, relevance) t1 t2 ->
283 match relevance with b::tl -> b,tl | _ -> true, [] in
284 let metasenv, subst =
285 try unify test_eq_only metasenv subst context t1 t2
286 with UnificationFailure _ | Uncertain _ when not b ->
289 metasenv, subst, relevance)
290 (metasenv, subst, relevance) tl1 tl2
291 with Invalid_argument _ ->
292 raise (uncert_exc metasenv subst context t1 t2)
296 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
297 C.Match (ref2,outtype2,term2,pl2)) ->
298 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
299 let _,_,ty,_ = List.nth itl tyno in
300 let rec remove_prods ~subst context ty =
301 let ty = NCicReduction.whd ~subst context ty in
304 | C.Prod (name,so,ta) ->
305 remove_prods ~subst ((name,(C.Decl so))::context) ta
309 match remove_prods ~subst [] ty with
310 | C.Sort C.Prop -> true
313 let rec remove_prods ~subst context ty =
314 let ty = NCicReduction.whd ~subst context ty in
317 | C.Prod (name,so,ta) ->
318 remove_prods ~subst ((name,(C.Decl so))::context) ta
321 if not (Ref.eq ref1 ref2) then
322 raise (uncert_exc metasenv subst context t1 t2)
324 let metasenv, subst =
325 unify test_eq_only metasenv subst context outtype1 outtype2 in
326 let metasenv, subst =
327 try unify test_eq_only metasenv subst context term1 term2
328 with UnificationFailure _ | Uncertain _ when is_prop ->
333 (fun (metasenv,subst) ->
334 unify 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 height_of is_whd = function
342 | NCic.Const (Ref.Ref (_,Ref.Def h))
343 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
344 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
345 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h, false
346 | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> max_int, true
347 | _ when is_whd -> 0, false
348 | _ -> max_int, false
350 let small_delta_step is_whd (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
351 let h1, flex1 = height_of is_whd t1 in
352 let h2, flex2 = height_of is_whd t2 in
353 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
354 NCicReduction.reduce_machine ~delta ~subst context m1,
355 NCicReduction.reduce_machine ~delta ~subst context m2,
356 if is_whd && flex1 && flex2 then 0 else delta
358 let rec unif_machines metasenv subst = function
359 | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) ->
361 let relevance = [] (* TO BE UNDERSTOOD
363 | C.Const r -> NCicEnvironment.get_relevance r
365 let unif_from_stack t1 t2 b metasenv subst =
367 let t1 = NCicReduction.from_stack t1 in
368 let t2 = NCicReduction.from_stack t2 in
369 unif_machines metasenv subst (small_delta_step true t1 t2)
370 with UnificationFailure _ | Uncertain _ when not b ->
373 let rec check_stack l1 l2 r (metasenv, subst) =
375 | x1::tl1, x2::tl2, r::tr ->
376 check_stack tl1 tl2 tr
377 (unif_from_stack x1 x2 r metasenv subst)
378 | x1::tl1, x2::tl2, [] ->
379 check_stack tl1 tl2 []
380 (unif_from_stack x1 x2 true metasenv subst)
382 fo_unif test_eq_only metasenv subst
383 (NCicReduction.unwind (k1,e1,t1,List.rev l1))
384 (NCicReduction.unwind (k2,e2,t2,List.rev l2))
386 check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
387 with UnificationFailure _ | Uncertain _ when delta > 0 ->
388 let delta = delta - 1 in
389 let red = NCicReduction.reduce_machine ~delta ~subst context in
390 unif_machines metasenv subst (red m1,red m2,delta)
392 try fo_unif test_eq_only metasenv subst t1 t2
393 with UnificationFailure msg | Uncertain msg as exn ->
395 unif_machines metasenv subst
396 (small_delta_step false (0,[],t1,[]) (0,[],t2,[]))
398 | UnificationFailure _ -> raise (UnificationFailure msg)
399 | Uncertain _ -> raise exn
402 let unify = unify false;;
410 exception UnificationFailure of string Lazy.t;;
411 exception Uncertain of string Lazy.t;;
412 exception AssertFailure of string Lazy.t;;
414 let verbose = false;;
415 let debug_print = fun _ -> ()
417 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
418 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
419 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
420 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
422 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
424 let type_of_aux' metasenv subst context term ugraph =
427 profile.HExtlib.profile
428 (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
430 CicTypeChecker.TypeCheckerFailure msg ->
434 "Kernel Type checking error:
435 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
436 (CicMetaSubst.ppterm ~metasenv subst term)
437 (CicMetaSubst.ppterm ~metasenv [] term)
438 (CicMetaSubst.ppcontext ~metasenv subst context)
439 (CicMetaSubst.ppmetasenv subst metasenv)
440 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
441 raise (AssertFailure msg)
442 | CicTypeChecker.AssertFailure msg ->
445 "Kernel Type checking assertion failure:
446 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
447 (CicMetaSubst.ppterm ~metasenv subst term)
448 (CicMetaSubst.ppterm ~metasenv [] term)
449 (CicMetaSubst.ppcontext ~metasenv subst context)
450 (CicMetaSubst.ppmetasenv subst metasenv)
451 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
452 raise (AssertFailure msg)
453 in profiler_toa.HExtlib.profile foo ()
456 let exists_a_meta l =
460 | Cic.Appl (Cic.Meta _::_) -> true
463 let rec deref subst t =
464 let snd (_,a,_) = a in
469 (CicSubstitution.subst_meta
470 l (snd (CicUtil.lookup_subst n subst)))
472 CicUtil.Subst_not_found _ -> t)
473 | Cic.Appl(Cic.Meta(n,l)::args) ->
474 (match deref subst (Cic.Meta(n,l)) with
475 | Cic.Lambda _ as t ->
476 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
477 | r -> Cic.Appl(r::args))
478 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
479 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
484 let foo () = deref subst t
485 in profiler_deref.HExtlib.profile foo ()
487 exception WrongShape;;
488 let eta_reduce after_beta_expansion after_beta_expansion_body
489 before_beta_expansion
492 match before_beta_expansion,after_beta_expansion_body with
493 Cic.Appl l, Cic.Appl l' ->
494 let rec all_but_last check_last =
498 | [_] -> if check_last then raise WrongShape else []
499 | he::tl -> he::(all_but_last check_last tl)
501 let all_but_last check_last l =
502 match all_but_last check_last l with
507 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
508 let all_but_last = all_but_last false l in
509 (* here we should test alpha-equivalence; however we know by
510 construction that here alpha_equivalence is equivalent to = *)
511 if t = all_but_last then
515 | _,_ -> after_beta_expansion
517 WrongShape -> after_beta_expansion
519 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
520 let module S = CicSubstitution in
521 let module C = Cic in
523 let rec aux metasenv subst n context t' ugraph =
526 let subst,metasenv,ugraph1 =
527 fo_unif_subst test_equality_only subst context metasenv
528 (CicSubstitution.lift n arg) t' ugraph
531 subst,metasenv,C.Rel (1 + n),ugraph1
534 | UnificationFailure _ ->
536 | C.Rel m -> subst,metasenv,
537 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
538 | C.Var (uri,exp_named_subst) ->
539 let subst,metasenv,exp_named_subst',ugraph1 =
540 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
542 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
544 (* andrea: in general, beta_expand can create badly typed
545 terms. This happens quite seldom in practice, UNLESS we
546 iterate on the local context. For this reason, we renounce
547 to iterate and just lift *)
551 Some t -> Some (CicSubstitution.lift 1 t)
553 subst, metasenv, C.Meta (i,l), ugraph
555 | C.Implicit _ as t -> subst,metasenv,t,ugraph
557 let subst,metasenv,te',ugraph1 =
558 aux metasenv subst n context te ugraph in
559 let subst,metasenv,ty',ugraph2 =
560 aux metasenv subst n context ty ugraph1 in
561 (* TASSI: sure this is in serial? *)
562 subst,metasenv,(C.Cast (te', ty')),ugraph2
564 let subst,metasenv,s',ugraph1 =
565 aux metasenv subst n context s ugraph in
566 let subst,metasenv,t',ugraph2 =
567 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
570 (* TASSI: sure this is in serial? *)
571 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
572 | C.Lambda (nn,s,t) ->
573 let subst,metasenv,s',ugraph1 =
574 aux metasenv subst n context s ugraph in
575 let subst,metasenv,t',ugraph2 =
576 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
578 (* TASSI: sure this is in serial? *)
579 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
580 | C.LetIn (nn,s,ty,t) ->
581 let subst,metasenv,s',ugraph1 =
582 aux metasenv subst n context s ugraph in
583 let subst,metasenv,ty',ugraph1 =
584 aux metasenv subst n context ty ugraph in
585 let subst,metasenv,t',ugraph2 =
586 aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
589 (* TASSI: sure this is in serial? *)
590 subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
592 let subst,metasenv,revl',ugraph1 =
594 (fun (subst,metasenv,appl,ugraph) t ->
595 let subst,metasenv,t',ugraph1 =
596 aux metasenv subst n context t ugraph in
597 subst,metasenv,(t'::appl),ugraph1
598 ) (subst,metasenv,[],ugraph) l
600 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
601 | C.Const (uri,exp_named_subst) ->
602 let subst,metasenv,exp_named_subst',ugraph1 =
603 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
605 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
606 | C.MutInd (uri,i,exp_named_subst) ->
607 let subst,metasenv,exp_named_subst',ugraph1 =
608 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
610 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
611 | C.MutConstruct (uri,i,j,exp_named_subst) ->
612 let subst,metasenv,exp_named_subst',ugraph1 =
613 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
615 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
616 | C.MutCase (sp,i,outt,t,pl) ->
617 let subst,metasenv,outt',ugraph1 =
618 aux metasenv subst n context outt ugraph in
619 let subst,metasenv,t',ugraph2 =
620 aux metasenv subst n context t ugraph1 in
621 let subst,metasenv,revpl',ugraph3 =
623 (fun (subst,metasenv,pl,ugraph) t ->
624 let subst,metasenv,t',ugraph1 =
625 aux metasenv subst n context t ugraph in
626 subst,metasenv,(t'::pl),ugraph1
627 ) (subst,metasenv,[],ugraph2) pl
629 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
630 (* TASSI: not sure this is serial *)
632 (*CSC: not implemented
633 let tylen = List.length fl in
636 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
639 C.Fix (i, substitutedfl)
641 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
643 (*CSC: not implemented
644 let tylen = List.length fl in
647 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
650 C.CoFix (i, substitutedfl)
653 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
655 and aux_exp_named_subst metasenv subst n context ens ugraph =
657 (fun (uri,t) (subst,metasenv,l,ugraph) ->
658 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
659 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
661 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
663 FreshNamesGenerator.mk_fresh_name ~subst
664 metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
666 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
667 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
668 subst, metasenv, t'', ugraph2
669 in profiler_beta_expand.HExtlib.profile foo ()
672 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
673 let _,subst,metasenv,hd,ugraph =
675 (fun arg (num,subst,metasenv,t,ugraph) ->
676 let subst,metasenv,t,ugraph1 =
677 beta_expand num test_equality_only
678 metasenv subst context t arg ugraph
680 num+1,subst,metasenv,t,ugraph1
681 ) args (1,subst,metasenv,t,ugraph)
683 subst,metasenv,hd,ugraph
685 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
688 | (m2,_,c2,c2')::_ ->
689 let m1,c1,c1' = carr,to1,to2 in
691 function Some (_,t) -> CicPp.ppterm t
695 ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
696 CoercDb.string_of_carr car2^": " ^
697 CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
698 unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
699 unopt c2^" + "^unopt c2')
701 (* NUOVA UNIFICAZIONE *)
702 (* A substitution is a (int * Cic.term) list that associates a
703 metavariable i with its body.
704 A metaenv is a (int * Cic.term) list that associate a metavariable
706 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
707 a new substitution which is _NOT_ unwinded. It must be unwinded before
710 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
711 let module C = Cic in
712 let module R = CicReduction in
713 let module S = CicSubstitution in
714 let t1 = deref subst t1 in
715 let t2 = deref subst t2 in
716 let (&&&) a b = (a && b) || ((not a) && (not b)) in
717 (* let bef = Sys.time () in *)
719 if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
723 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
724 in profiler_are_convertible.HExtlib.profile foo ()
726 (* let aft = Sys.time () in
727 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
728 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
729 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
731 subst, metasenv, ugraph
734 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
735 let _,subst,metasenv,ugraph1 =
738 (fun (j,subst,metasenv,ugraph) t1 t2 ->
741 | _,None -> j+1,subst,metasenv,ugraph
742 | Some t1', Some t2' ->
743 (* First possibility: restriction *)
744 (* Second possibility: unification *)
745 (* Third possibility: convertibility *)
748 ~subst ~metasenv context t1' t2' ugraph
751 j+1,subst,metasenv, ugraph1
754 let subst,metasenv,ugraph2 =
757 subst context metasenv t1' t2' ugraph
759 j+1,subst,metasenv,ugraph2
762 | UnificationFailure _ ->
763 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
764 let metasenv, subst =
765 CicMetaSubst.restrict
766 subst [(n,j)] metasenv in
767 j+1,subst,metasenv,ugraph1)
768 ) (1,subst,metasenv,ugraph) ln lm
772 (UnificationFailure (lazy "1"))
775 "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."
776 (CicMetaSubst.ppterm ~metasenv subst t1)
777 (CicMetaSubst.ppterm ~metasenv subst t2))) *)
778 | Invalid_argument _ ->
780 (UnificationFailure (lazy "2")))
783 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
784 (CicMetaSubst.ppterm ~metasenv subst t1)
785 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
786 in subst,metasenv,ugraph1
787 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
788 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
790 | (t, C.Meta (n,l)) ->
793 C.Meta (n,_), C.Meta (m,_) when n < m -> false
794 | _, C.Meta _ -> false
797 let lower = fun x y -> if swap then y else x in
798 let upper = fun x y -> if swap then x else y in
799 let fo_unif_subst_ordered
800 test_equality_only subst context metasenv m1 m2 ugraph =
801 fo_unif_subst test_equality_only subst context metasenv
802 (lower m1 m2) (upper m1 m2) ugraph
805 let subst,metasenv,ugraph1 =
806 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
809 type_of_aux' metasenv subst context t ugraph
813 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
815 UnificationFailure _ as e -> raise e
816 | Uncertain msg -> raise (UnificationFailure msg)
818 debug_print (lazy "siamo allo huge hack");
819 (* TODO huge hack!!!!
820 * we keep on unifying/refining in the hope that
821 * the problem will be eventually solved.
822 * In the meantime we're breaking a big invariant:
823 * the terms that we are unifying are no longer well
824 * typed in the current context (in the worst case
825 * we could even diverge) *)
826 (subst, metasenv,ugraph)) in
827 let t',metasenv,subst =
829 CicMetaSubst.delift n subst context metasenv l t
831 (CicMetaSubst.MetaSubstFailure msg)->
832 raise (UnificationFailure msg)
833 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
837 C.Sort (C.Type u) when not test_equality_only ->
838 let u' = CicUniv.fresh () in
839 let s = C.Sort (C.Type u') in
842 CicUniv.add_ge (upper u u') (lower u u') ugraph1
846 CicUniv.UniverseInconsistency msg ->
847 raise (UnificationFailure msg))
850 (* Unifying the types may have already instantiated n. Let's check *)
852 let (_, oldt,_) = CicUtil.lookup_subst n subst in
853 let lifted_oldt = S.subst_meta l oldt in
854 fo_unif_subst_ordered
855 test_equality_only subst context metasenv t lifted_oldt ugraph2
857 CicUtil.Subst_not_found _ ->
858 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
859 let subst = (n, (context, t'',ty)) :: subst in
861 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
862 subst, metasenv, ugraph2
864 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
865 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
866 if UriManager.eq uri1 uri2 then
867 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
868 exp_named_subst1 exp_named_subst2 ugraph
870 raise (UnificationFailure (lazy
872 "Can't unify %s with %s due to different constants"
873 (CicMetaSubst.ppterm ~metasenv subst t1)
874 (CicMetaSubst.ppterm ~metasenv subst t2))))
875 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
876 if UriManager.eq uri1 uri2 && i1 = i2 then
877 fo_unif_subst_exp_named_subst
879 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
881 raise (UnificationFailure
884 "Can't unify %s with %s due to different inductive principles"
885 (CicMetaSubst.ppterm ~metasenv subst t1)
886 (CicMetaSubst.ppterm ~metasenv subst t2))))
887 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
888 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
889 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
890 fo_unif_subst_exp_named_subst
892 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
894 raise (UnificationFailure
897 "Can't unify %s with %s due to different inductive constructors"
898 (CicMetaSubst.ppterm ~metasenv subst t1)
899 (CicMetaSubst.ppterm ~metasenv subst t2))))
900 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
901 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
902 subst context metasenv te t2 ugraph
903 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
904 subst context metasenv t1 te ugraph
905 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
906 let subst',metasenv',ugraph1 =
907 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
909 fo_unif_subst test_equality_only
910 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
911 | (C.LetIn (_,s1,ty1,t1), t2)
912 | (t2, C.LetIn (_,s1,ty1,t1)) ->
914 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
915 | (C.Appl l1, C.Appl l2) ->
916 (* andrea: this case should be probably rewritten in the
919 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
922 (fun (subst,metasenv,ugraph) t1 t2 ->
924 test_equality_only subst context metasenv t1 t2 ugraph)
925 (subst,metasenv,ugraph) l1 l2
926 with (Invalid_argument msg) ->
927 raise (UnificationFailure (lazy msg)))
928 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
929 (* we verify that none of the args is a Meta,
930 since beta expanding with respoect to a metavariable
934 let (_,t,_) = CicUtil.lookup_subst i subst in
935 let lifted = S.subst_meta l t in
936 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
939 subst context metasenv reduced t2 ugraph
940 with CicUtil.Subst_not_found _ -> *)
941 let subst,metasenv,beta_expanded,ugraph1 =
943 test_equality_only metasenv subst context t2 args ugraph
945 fo_unif_subst test_equality_only subst context metasenv
946 (C.Meta (i,l)) beta_expanded ugraph1
947 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
949 let (_,t,_) = CicUtil.lookup_subst i subst in
950 let lifted = S.subst_meta l t in
951 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
954 subst context metasenv t1 reduced ugraph
955 with CicUtil.Subst_not_found _ -> *)
956 let subst,metasenv,beta_expanded,ugraph1 =
959 metasenv subst context t1 args ugraph
961 fo_unif_subst test_equality_only subst context metasenv
962 (C.Meta (i,l)) beta_expanded ugraph1
964 let lr1 = List.rev l1 in
965 let lr2 = List.rev l2 in
967 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
970 | _,[] -> assert false
973 test_equality_only subst context metasenv h1 h2 ugraph
976 fo_unif_subst test_equality_only subst context metasenv
977 h (C.Appl (List.rev l)) ugraph
978 | ((h1::l1),(h2::l2)) ->
979 let subst', metasenv',ugraph1 =
982 subst context metasenv h1 h2 ugraph
985 test_equality_only subst' metasenv' (l1,l2) ugraph1
989 test_equality_only subst metasenv (lr1, lr2) ugraph
991 | UnificationFailure s
992 | Uncertain s as exn ->
995 | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
996 (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
997 CoercDb.is_a_coercion cc1 <> None &&
998 CoercDb.is_a_coercion cc2 <> None &&
999 not (UriManager.eq uri1 uri2) ->
1001 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1003 let inner_coerced t =
1004 let t = CicMetaSubst.apply_subst subst t in
1008 (match CoercGraph.coerced_arg l with
1010 | Some (t,_) -> aux (List.hd l) t t)
1013 aux (Cic.Implicit None) (Cic.Implicit None) t
1015 let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
1016 let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
1019 CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
1021 | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
1024 let head1_c, head2_c =
1026 CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
1028 | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
1031 let unfold uri ens args =
1033 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
1037 | Cic.Constant (_,Some bo,_,_,_) ->
1038 CicReduction.head_beta_reduce ~delta:false
1039 (Cic.Appl (bo::args))
1042 let conclude subst metasenv ugraph last_tl1' last_tl2' =
1043 let subst',metasenv,ugraph =
1046 ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
1047 " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
1049 fo_unif_subst test_equality_only subst context
1050 metasenv last_tl1' last_tl2' ugraph
1052 if subst = subst' then raise exn
1055 let subst,metasenv,ugrph as res =
1057 fo_unif_subst test_equality_only subst' context
1058 metasenv (C.Appl l1) (C.Appl l2) ugraph
1062 (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
1063 " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1067 if CoercDb.eq_carr car1 car2 then
1068 match last_tl1,last_tl2 with
1069 | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
1072 let subst,metasenv,ugraph =
1073 fo_unif_subst test_equality_only subst context
1074 metasenv last_tl1 last_tl2 ugraph
1076 fo_unif_subst test_equality_only subst context
1077 metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
1078 | _ when CoercDb.eq_carr head1_c head2_c ->
1079 (* composite VS composition + metas avoiding
1080 * coercions not only in coerced position *)
1081 if c1 <> cc1 && c2 <> cc2 then
1082 conclude subst metasenv ugraph
1087 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
1089 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
1091 fo_unif_subst test_equality_only subst context
1092 metasenv l1 l2 ugraph
1096 match last_tl1 with Cic.Meta _ -> true | _ -> false in
1098 match last_tl2 with Cic.Meta _ -> true | _ -> false in
1099 if not (grow1 || grow2) then
1100 (* no flexible terminals -> no pullback, but
1101 * we still unify them, in some cases it helps *)
1102 conclude subst metasenv ugraph last_tl1 last_tl2
1106 metasenv subst context (grow1,car1) (grow2,car2)
1110 | (carr,metasenv,to1,to2)::xxx ->
1111 warn_if_not_unique xxx to1 to2 carr car1 car2;
1112 let last_tl1',(subst,metasenv,ugraph) =
1113 match grow1,to1 with
1114 | true,Some (last,coerced) ->
1116 fo_unif_subst test_equality_only subst context
1117 metasenv coerced last_tl1 ugraph
1118 | _ -> last_tl1,(subst,metasenv,ugraph)
1120 let last_tl2',(subst,metasenv,ugraph) =
1121 match grow2,to2 with
1122 | true,Some (last,coerced) ->
1124 fo_unif_subst test_equality_only subst context
1125 metasenv coerced last_tl2 ugraph
1126 | _ -> last_tl2,(subst,metasenv,ugraph)
1128 conclude subst metasenv ugraph last_tl1' last_tl2')
1130 (* {{{ CSC: This is necessary because of the "elim H" tactic
1131 where the type of H is only reducible to an
1132 inductive type. This could be extended from inductive
1133 types to any rigid term. However, the code is
1134 duplicated in two places: inside applications and
1135 outside them. Probably it would be better to
1136 work with lambda-bar terms instead. *)
1137 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
1138 | (_, Cic.MutInd _::_) ->
1139 let t1' = R.whd ~subst context t1 in
1141 C.Appl (C.MutInd _::_) ->
1142 fo_unif_subst test_equality_only
1143 subst context metasenv t1' t2 ugraph
1144 | _ -> raise (UnificationFailure (lazy "88")))
1145 | (Cic.MutInd _::_,_) ->
1146 let t2' = R.whd ~subst context t2 in
1148 C.Appl (C.MutInd _::_) ->
1149 fo_unif_subst test_equality_only
1150 subst context metasenv t1 t2' ugraph
1153 (lazy ("not a mutind :"^
1154 CicMetaSubst.ppterm ~metasenv subst t2 ))))
1157 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
1158 let subst', metasenv',ugraph1 =
1159 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
1161 let subst'',metasenv'',ugraph2 =
1162 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
1166 (fun (subst,metasenv,ugraph) t1 t2 ->
1168 test_equality_only subst context metasenv t1 t2 ugraph
1169 ) (subst'',metasenv'',ugraph2) pl1 pl2
1171 Invalid_argument _ ->
1172 raise (UnificationFailure (lazy "6.1")))
1174 "Error trying to unify %s with %s: the number of branches is not the same."
1175 (CicMetaSubst.ppterm ~metasenv subst t1)
1176 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
1177 | (C.Rel _, _) | (_, C.Rel _) ->
1179 subst, metasenv,ugraph
1181 raise (UnificationFailure (lazy
1183 "Can't unify %s with %s because they are not convertible"
1184 (CicMetaSubst.ppterm ~metasenv subst t1)
1185 (CicMetaSubst.ppterm ~metasenv subst t2))))
1186 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
1187 let subst,metasenv,beta_expanded,ugraph1 =
1189 test_equality_only metasenv subst context t2 args ugraph
1191 fo_unif_subst test_equality_only subst context metasenv
1192 (C.Meta (i,l)) beta_expanded ugraph1
1193 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
1194 let subst,metasenv,beta_expanded,ugraph1 =
1196 test_equality_only metasenv subst context t1 args ugraph
1198 fo_unif_subst test_equality_only subst context metasenv
1199 beta_expanded (C.Meta (i,l)) ugraph1
1200 (* Works iff there are no arguments applied to it; similar to the
1202 | (_, C.MutInd _) ->
1203 let t1' = R.whd ~subst context t1 in
1206 fo_unif_subst test_equality_only
1207 subst context metasenv t1' t2 ugraph
1208 | _ -> raise (UnificationFailure (lazy "8")))
1210 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
1211 let subst',metasenv',ugraph1 =
1212 fo_unif_subst true subst context metasenv s1 s2 ugraph
1214 fo_unif_subst test_equality_only
1215 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1217 (match CicReduction.whd ~subst context t2 with
1219 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1220 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
1222 (match CicReduction.whd ~subst context t1 with
1224 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1225 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
1227 (* delta-beta reduction should almost never be a problem for
1229 1. long computations require iota reduction
1230 2. it is extremely rare that a close term t1 (that could be unified
1231 to t2) beta-delta reduces to t1' while t2 does not beta-delta
1232 reduces in the same way. This happens only if one meta of t2
1233 occurs in head position during beta reduction. In this unluky
1234 case too much reduction will be performed on t1 and unification
1235 will surely fail. *)
1236 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
1237 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
1238 if t1 = t1' && t2 = t2' then
1239 raise (UnificationFailure
1242 "Can't unify %s with %s because they are not convertible"
1243 (CicMetaSubst.ppterm ~metasenv subst t1)
1244 (CicMetaSubst.ppterm ~metasenv subst t2))))
1247 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
1249 UnificationFailure _
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))))
1258 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
1259 exp_named_subst1 exp_named_subst2 ugraph
1263 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
1264 assert (uri1=uri2) ;
1265 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1266 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
1268 Invalid_argument _ ->
1273 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
1276 raise (UnificationFailure (lazy (sprintf
1277 "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))))
1279 (* A substitution is a (int * Cic.term) list that associates a *)
1280 (* metavariable i with its body. *)
1281 (* metasenv is of type Cic.metasenv *)
1282 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
1283 (* a new substitution which is already unwinded and ready to be applied and *)
1284 (* a new metasenv in which some hypothesis in the contexts of the *)
1285 (* metavariables may have been restricted. *)
1286 let fo_unif metasenv context t1 t2 ugraph =
1287 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
1289 let enrich_msg msg subst context metasenv t1 t2 ugraph =
1292 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"
1293 (CicMetaSubst.ppterm ~metasenv subst t1)
1295 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1298 | UnificationFailure s
1300 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1301 (CicMetaSubst.ppterm ~metasenv subst t2)
1303 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1306 | UnificationFailure s
1308 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1309 (CicMetaSubst.ppcontext ~metasenv subst context)
1310 (CicMetaSubst.ppmetasenv subst metasenv)
1311 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
1313 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
1314 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
1316 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1317 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
1319 | UnificationFailure s
1321 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1322 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
1324 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1325 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
1327 | UnificationFailure s
1329 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1330 (CicMetaSubst.ppcontext ~metasenv subst context)
1331 (CicMetaSubst.ppmetasenv subst metasenv)
1335 let fo_unif_subst subst context metasenv t1 t2 ugraph =
1337 fo_unif_subst false subst context metasenv t1 t2 ugraph
1339 | AssertFailure msg ->
1340 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1341 | UnificationFailure msg ->
1342 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))