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;;
72 let inside c = indent := !indent ^ String.make 1 c;;
73 let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
77 prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
83 let rec beta_expand num test_eq_only swap metasenv subst context t arg =
84 let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
88 unify test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
90 unify test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
92 (metasenv, subst), NCic.Rel (1 + n)
93 with Uncertain _ | UnificationFailure _ ->
95 | NCic.Rel m as orig ->
96 (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
97 (* andrea: in general, beta_expand can create badly typed
98 terms. This happens quite seldom in practice, UNLESS we
99 iterate on the local context. For this reason, we renounce
100 to iterate and just lift *)
101 | NCic.Meta (i,(shift,lc)) ->
102 (metasenv,subst), NCic.Meta (i,(shift+1,lc))
103 | NCic.Prod (name, src, tgt) as orig ->
104 let (metasenv, subst), src1 = aux (n,context,true) acc src in
105 let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
106 let ms, tgt1 = aux k (metasenv, subst) tgt in
107 if src == src1 && tgt == tgt1 then ms, orig else
108 ms, NCic.Prod (name, src1, tgt1)
110 NCicUntrusted.map_term_fold_a
111 (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t
114 let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
115 let fresh_name = "Hbeta" ^ string_of_int num in
116 let (metasenv,subst), t1 =
117 aux (0, context, test_eq_only) (metasenv, subst) t in
118 let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in
120 ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
122 with NCicTypeChecker.TypeCheckerFailure _ ->
123 metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
125 and beta_expand_many test_equality_only swap metasenv subst context t args =
126 (* (*D*) inside 'B'; try let rc = *)
127 pp (lazy (String.concat ", "
128 (List.map (NCicPp.ppterm ~metasenv ~subst ~context)
129 args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
130 let _, subst, metasenv, hd =
132 (fun arg (num,subst,metasenv,t) ->
133 let metasenv, subst, t =
134 beta_expand num test_equality_only swap metasenv subst context t arg
136 num+1,subst,metasenv,t)
137 args (1,subst,metasenv,t)
139 pp (lazy ("Head syntesized by b-exp: " ^
140 NCicPp.ppterm ~metasenv ~subst ~context hd));
142 (* (*D*) in outside (); rc with exn -> outside (); raise exn *)
144 and instantiate test_eq_only metasenv subst context n lc t swap =
145 (* (*D*) inside 'I'; try let rc = *)
146 let unify test_eq_only m s c t1 t2 =
147 if swap then unify test_eq_only m s c t2 t1
148 else unify test_eq_only m s c t1 t2
150 let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
151 let metasenv, subst =
153 | NCic.Implicit (`Typeof _) -> metasenv, subst
155 let lty = NCicSubstitution.subst_meta lc ty in
157 try NCicTypeChecker.typeof ~subst ~metasenv context t
158 with NCicTypeChecker.TypeCheckerFailure msg ->
159 prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
160 prerr_endline (Lazy.force msg);
163 pp (lazy("On the types: " ^
164 NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
165 ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
166 unify test_eq_only metasenv subst context lty ty_t
168 let (metasenv, subst), t =
169 try NCicMetaSubst.delift metasenv subst context n lc t
170 with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg)
171 | NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg)
173 (* Unifying the types may have already instantiated n. *)
175 let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
176 let oldt = NCicSubstitution.subst_meta lc oldt in
177 (* conjecture: always fail --> occur check *)
178 unify test_eq_only metasenv subst context oldt t
179 with NCicUtils.Subst_not_found _ ->
180 (* by cumulativity when unify(?,Type_i)
181 * we could ? := Type_j with j <= i... *)
182 let subst = (n, (name, ctx, t, ty)) :: subst in
183 pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
184 ~metasenv ~subst ~context:ctx (NCicSubstitution.subst_meta lc t)));
186 List.filter (fun (m,_) -> not (n = m)) metasenv
189 (* (*D*) in outside(); rc with exn -> outside (); raise exn *)
191 and unify test_eq_only metasenv subst context t1 t2 =
192 (* (*D*) inside 'U'; try let rc = *)
193 let fo_unif test_eq_only metasenv subst t1 t2 =
194 (* (*D*) inside 'F'; try let rc = *)
196 pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^
197 NCicPp.ppterm ~metasenv ~subst ~context t2));
203 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
204 if NCicEnvironment.universe_leq a b then metasenv, subst
205 else raise (fail_exc metasenv subst context t1 t2)
206 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
207 if NCicEnvironment.universe_eq a b then metasenv, subst
208 else raise (fail_exc metasenv subst context t1 t2)
209 | (C.Sort C.Prop,C.Sort (C.Type _)) ->
210 if (not test_eq_only) then metasenv, subst
211 else raise (fail_exc metasenv subst context t1 t2)
213 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
214 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
215 let metasenv, subst = unify true metasenv subst context s1 s2 in
216 unify test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
217 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
218 let metasenv,subst=unify test_eq_only metasenv subst context ty1 ty2 in
219 let metasenv,subst=unify test_eq_only metasenv subst context s1 s2 in
220 let context = (name1, C.Def (s1,ty1))::context in
221 unify test_eq_only metasenv subst context t1 t2
223 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
225 let l1 = NCicUtils.expand_local_context l1 in
226 let l2 = NCicUtils.expand_local_context l2 in
227 let metasenv, subst, to_restrict, _ =
229 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
231 let metasenv, subst =
232 unify test_eq_only metasenv subst context
233 (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
235 metasenv, subst, to_restrict, i-1
236 with UnificationFailure _ | Uncertain _ ->
237 metasenv, subst, i::to_restrict, i-1)
238 l1 l2 (metasenv, subst, [], List.length l1)
240 let metasenv, subst, _ =
241 NCicMetaSubst.restrict metasenv subst n1 to_restrict
245 | Invalid_argument _ -> assert false
246 | NCicMetaSubst.MetaSubstFailure msg ->
248 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
249 let term1 = NCicSubstitution.subst_meta lc1 term in
250 let term2 = NCicSubstitution.subst_meta lc2 term in
251 unify test_eq_only metasenv subst context term1 term2
252 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
254 | C.Meta (n,lc), t ->
256 let _,_,term,_ = NCicUtils.lookup_subst n subst in
257 let term = NCicSubstitution.subst_meta lc term in
258 unify test_eq_only metasenv subst context term t
259 with NCicUtils.Subst_not_found _->
260 instantiate test_eq_only metasenv subst context n lc t false)
262 | t, C.Meta (n,lc) ->
264 let _,_,term,_ = NCicUtils.lookup_subst n subst in
265 let term = NCicSubstitution.subst_meta lc term in
266 unify test_eq_only metasenv subst context t term
267 with NCicUtils.Subst_not_found _->
268 instantiate test_eq_only metasenv subst context n lc t true)
270 | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
271 let _,_,term,_ = NCicUtils.lookup_subst i subst in
272 let term = NCicSubstitution.subst_meta l term in
273 unify test_eq_only metasenv subst context (mk_appl term args) t2
275 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
276 let _,_,term,_ = NCicUtils.lookup_subst i subst in
277 let term = NCicSubstitution.subst_meta l term in
278 unify test_eq_only metasenv subst context t1 (mk_appl term args)
280 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
281 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
284 (fun (metasenv, subst) t1 t2 ->
285 unify test_eq_only metasenv subst context t1 t2)
286 (metasenv,subst) l1 l2
287 with Invalid_argument _ ->
288 raise (fail_exc metasenv subst context t1 t2))
290 | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
291 (* we verify that none of the args is a Meta,
292 since beta expanding w.r.t a metavariable makes no sense *)
293 let metasenv, subst, beta_expanded =
296 metasenv subst context t2 args
298 unify test_eq_only metasenv subst context
299 (C.Meta (i,l)) beta_expanded
301 | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
302 let metasenv, subst, beta_expanded =
305 metasenv subst context t1 args
307 unify test_eq_only metasenv subst context
308 beta_expanded (C.Meta (i,l))
310 (* processing this case here we avoid a useless small delta step *)
311 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
313 let relevance = NCicEnvironment.get_relevance r1 in
314 let relevance = match r1 with
315 | Ref.Ref (_,Ref.Con (_,_,lno)) ->
316 let _,relevance = HExtlib.split_nth lno relevance in
317 HExtlib.mk_list false lno @ relevance
320 let metasenv, subst, _ =
323 (fun (metasenv, subst, relevance) t1 t2 ->
325 match relevance with b::tl -> b,tl | _ -> true, [] in
326 let metasenv, subst =
327 try unify test_eq_only metasenv subst context t1 t2
328 with UnificationFailure _ | Uncertain _ when not b ->
331 metasenv, subst, relevance)
332 (metasenv, subst, relevance) tl1 tl2
333 with Invalid_argument _ ->
334 raise (uncert_exc metasenv subst context t1 t2)
338 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
339 C.Match (ref2,outtype2,term2,pl2)) ->
340 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
341 let _,_,ty,_ = List.nth itl tyno in
342 let rec remove_prods ~subst context ty =
343 let ty = NCicReduction.whd ~subst context ty in
346 | C.Prod (name,so,ta) ->
347 remove_prods ~subst ((name,(C.Decl so))::context) ta
351 match remove_prods ~subst [] ty with
352 | C.Sort C.Prop -> true
355 let rec remove_prods ~subst context ty =
356 let ty = NCicReduction.whd ~subst context ty in
359 | C.Prod (name,so,ta) ->
360 remove_prods ~subst ((name,(C.Decl so))::context) ta
363 if not (Ref.eq ref1 ref2) then
364 raise (uncert_exc metasenv subst context t1 t2)
366 let metasenv, subst =
367 unify test_eq_only metasenv subst context outtype1 outtype2 in
368 let metasenv, subst =
369 try unify test_eq_only metasenv subst context term1 term2
370 with UnificationFailure _ | Uncertain _ when is_prop ->
375 (fun (metasenv,subst) ->
376 unify test_eq_only metasenv subst context)
377 (metasenv, subst) pl1 pl2
378 with Invalid_argument _ ->
379 raise (uncert_exc metasenv subst context t1 t2))
380 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
381 | _ -> raise (uncert_exc metasenv subst context t1 t2)
382 (* (*D*) in outside(); rc with exn -> outside (); raise exn *)
384 let height_of = function
385 | NCic.Const (Ref.Ref (_,Ref.Def h))
386 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
387 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
388 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
391 let put_in_whd m1 m2 =
392 NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
393 NCicReduction.reduce_machine ~delta:max_int ~subst context m2
396 ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
398 assert (not (norm1 && norm2));
400 x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
402 NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
404 let h1 = height_of t1 in
405 let h2 = height_of t2 in
406 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
407 NCicReduction.reduce_machine ~delta ~subst context m1,
408 NCicReduction.reduce_machine ~delta ~subst context m2
410 let rec unif_machines metasenv subst =
412 | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
413 (* (*D*) inside 'M'; try let rc = *)
415 pp (lazy((if are_normal then "*" else " ") ^ " " ^
416 NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
418 NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2)));
420 let relevance = [] (* TO BE UNDERSTOOD
422 | C.Const r -> NCicEnvironment.get_relevance r
424 let unif_from_stack t1 t2 b metasenv subst =
426 let t1 = NCicReduction.from_stack t1 in
427 let t2 = NCicReduction.from_stack t2 in
428 unif_machines metasenv subst (put_in_whd t1 t2)
429 with UnificationFailure _ | Uncertain _ when not b ->
432 let rec check_stack l1 l2 r (metasenv, subst) =
434 | x1::tl1, x2::tl2, r::tr ->
435 check_stack tl1 tl2 tr
436 (unif_from_stack x1 x2 r metasenv subst)
437 | x1::tl1, x2::tl2, [] ->
438 check_stack tl1 tl2 []
439 (unif_from_stack x1 x2 true metasenv subst)
441 fo_unif test_eq_only metasenv subst
442 (NCicReduction.unwind (k1,e1,t1,List.rev l1))
443 (NCicReduction.unwind (k2,e2,t2,List.rev l2))
445 try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
446 with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
447 unif_machines metasenv subst (small_delta_step m1 m2)
448 (* (*D*) in outside(); rc with exn -> outside (); raise exn *)
450 try fo_unif test_eq_only metasenv subst t1 t2
451 with UnificationFailure msg | Uncertain msg as exn ->
453 unif_machines metasenv subst
454 (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
456 | UnificationFailure _ -> raise (UnificationFailure msg)
457 | Uncertain _ -> raise exn
458 (* (*D*) in outside(); rc with exn -> outside (); raise exn *)
471 exception UnificationFailure of string Lazy.t;;
472 exception Uncertain of string Lazy.t;;
473 exception AssertFailure of string Lazy.t;;
475 let verbose = false;;
476 let debug_print = fun _ -> ()
478 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
479 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
480 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
481 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
483 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
485 let type_of_aux' metasenv subst context term ugraph =
488 profile.HExtlib.profile
489 (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
491 CicTypeChecker.TypeCheckerFailure msg ->
495 "Kernel Type checking error:
496 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
497 (CicMetaSubst.ppterm ~metasenv subst term)
498 (CicMetaSubst.ppterm ~metasenv [] term)
499 (CicMetaSubst.ppcontext ~metasenv subst context)
500 (CicMetaSubst.ppmetasenv subst metasenv)
501 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
502 raise (AssertFailure msg)
503 | CicTypeChecker.AssertFailure msg ->
506 "Kernel Type checking assertion failure:
507 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
508 (CicMetaSubst.ppterm ~metasenv subst term)
509 (CicMetaSubst.ppterm ~metasenv [] term)
510 (CicMetaSubst.ppcontext ~metasenv subst context)
511 (CicMetaSubst.ppmetasenv subst metasenv)
512 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
513 raise (AssertFailure msg)
514 in profiler_toa.HExtlib.profile foo ()
517 let exists_a_meta l =
521 | Cic.Appl (Cic.Meta _::_) -> true
524 let rec deref subst t =
525 let snd (_,a,_) = a in
530 (CicSubstitution.subst_meta
531 l (snd (CicUtil.lookup_subst n subst)))
533 CicUtil.Subst_not_found _ -> t)
534 | Cic.Appl(Cic.Meta(n,l)::args) ->
535 (match deref subst (Cic.Meta(n,l)) with
536 | Cic.Lambda _ as t ->
537 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
538 | r -> Cic.Appl(r::args))
539 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
540 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
545 let foo () = deref subst t
546 in profiler_deref.HExtlib.profile foo ()
548 exception WrongShape;;
549 let eta_reduce after_beta_expansion after_beta_expansion_body
550 before_beta_expansion
553 match before_beta_expansion,after_beta_expansion_body with
554 Cic.Appl l, Cic.Appl l' ->
555 let rec all_but_last check_last =
559 | [_] -> if check_last then raise WrongShape else []
560 | he::tl -> he::(all_but_last check_last tl)
562 let all_but_last check_last l =
563 match all_but_last check_last l with
568 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
569 let all_but_last = all_but_last false l in
570 (* here we should test alpha-equivalence; however we know by
571 construction that here alpha_equivalence is equivalent to = *)
572 if t = all_but_last then
576 | _,_ -> after_beta_expansion
578 WrongShape -> after_beta_expansion
580 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
581 let module S = CicSubstitution in
582 let module C = Cic in
584 let rec aux metasenv subst n context t' ugraph =
587 let subst,metasenv,ugraph1 =
588 fo_unif_subst test_equality_only subst context metasenv
589 (CicSubstitution.lift n arg) t' ugraph
592 subst,metasenv,C.Rel (1 + n),ugraph1
595 | UnificationFailure _ ->
597 | C.Rel m -> subst,metasenv,
598 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
599 | C.Var (uri,exp_named_subst) ->
600 let subst,metasenv,exp_named_subst',ugraph1 =
601 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
603 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
605 (* andrea: in general, beta_expand can create badly typed
606 terms. This happens quite seldom in practice, UNLESS we
607 iterate on the local context. For this reason, we renounce
608 to iterate and just lift *)
612 Some t -> Some (CicSubstitution.lift 1 t)
614 subst, metasenv, C.Meta (i,l), ugraph
616 | C.Implicit _ as t -> subst,metasenv,t,ugraph
618 let subst,metasenv,te',ugraph1 =
619 aux metasenv subst n context te ugraph in
620 let subst,metasenv,ty',ugraph2 =
621 aux metasenv subst n context ty ugraph1 in
622 (* TASSI: sure this is in serial? *)
623 subst,metasenv,(C.Cast (te', ty')),ugraph2
625 let subst,metasenv,s',ugraph1 =
626 aux metasenv subst n context s ugraph in
627 let subst,metasenv,t',ugraph2 =
628 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
631 (* TASSI: sure this is in serial? *)
632 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
633 | C.Lambda (nn,s,t) ->
634 let subst,metasenv,s',ugraph1 =
635 aux metasenv subst n context s ugraph in
636 let subst,metasenv,t',ugraph2 =
637 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
639 (* TASSI: sure this is in serial? *)
640 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
641 | C.LetIn (nn,s,ty,t) ->
642 let subst,metasenv,s',ugraph1 =
643 aux metasenv subst n context s ugraph in
644 let subst,metasenv,ty',ugraph1 =
645 aux metasenv subst n context ty ugraph in
646 let subst,metasenv,t',ugraph2 =
647 aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
650 (* TASSI: sure this is in serial? *)
651 subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
653 let subst,metasenv,revl',ugraph1 =
655 (fun (subst,metasenv,appl,ugraph) t ->
656 let subst,metasenv,t',ugraph1 =
657 aux metasenv subst n context t ugraph in
658 subst,metasenv,(t'::appl),ugraph1
659 ) (subst,metasenv,[],ugraph) l
661 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
662 | C.Const (uri,exp_named_subst) ->
663 let subst,metasenv,exp_named_subst',ugraph1 =
664 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
666 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
667 | C.MutInd (uri,i,exp_named_subst) ->
668 let subst,metasenv,exp_named_subst',ugraph1 =
669 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
671 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
672 | C.MutConstruct (uri,i,j,exp_named_subst) ->
673 let subst,metasenv,exp_named_subst',ugraph1 =
674 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
676 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
677 | C.MutCase (sp,i,outt,t,pl) ->
678 let subst,metasenv,outt',ugraph1 =
679 aux metasenv subst n context outt ugraph in
680 let subst,metasenv,t',ugraph2 =
681 aux metasenv subst n context t ugraph1 in
682 let subst,metasenv,revpl',ugraph3 =
684 (fun (subst,metasenv,pl,ugraph) t ->
685 let subst,metasenv,t',ugraph1 =
686 aux metasenv subst n context t ugraph in
687 subst,metasenv,(t'::pl),ugraph1
688 ) (subst,metasenv,[],ugraph2) pl
690 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
691 (* TASSI: not sure this is serial *)
693 (*CSC: not implemented
694 let tylen = List.length fl in
697 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
700 C.Fix (i, substitutedfl)
702 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
704 (*CSC: not implemented
705 let tylen = List.length fl in
708 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
711 C.CoFix (i, substitutedfl)
714 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
716 and aux_exp_named_subst metasenv subst n context ens ugraph =
718 (fun (uri,t) (subst,metasenv,l,ugraph) ->
719 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
720 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
722 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
724 FreshNamesGenerator.mk_fresh_name ~subst
725 metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
727 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
728 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
729 subst, metasenv, t'', ugraph2
730 in profiler_beta_expand.HExtlib.profile foo ()
733 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
734 let _,subst,metasenv,hd,ugraph =
736 (fun arg (num,subst,metasenv,t,ugraph) ->
737 let subst,metasenv,t,ugraph1 =
738 beta_expand num test_equality_only
739 metasenv subst context t arg ugraph
741 num+1,subst,metasenv,t,ugraph1
742 ) args (1,subst,metasenv,t,ugraph)
744 subst,metasenv,hd,ugraph
746 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
749 | (m2,_,c2,c2')::_ ->
750 let m1,c1,c1' = carr,to1,to2 in
752 function Some (_,t) -> CicPp.ppterm t
756 ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
757 CoercDb.string_of_carr car2^": " ^
758 CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
759 unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
760 unopt c2^" + "^unopt c2')
762 (* NUOVA UNIFICAZIONE *)
763 (* A substitution is a (int * Cic.term) list that associates a
764 metavariable i with its body.
765 A metaenv is a (int * Cic.term) list that associate a metavariable
767 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
768 a new substitution which is _NOT_ unwinded. It must be unwinded before
771 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
772 let module C = Cic in
773 let module R = CicReduction in
774 let module S = CicSubstitution in
775 let t1 = deref subst t1 in
776 let t2 = deref subst t2 in
777 let (&&&) a b = (a && b) || ((not a) && (not b)) in
778 (* let bef = Sys.time () in *)
780 if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
784 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
785 in profiler_are_convertible.HExtlib.profile foo ()
787 (* let aft = Sys.time () in
788 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
789 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
790 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
792 subst, metasenv, ugraph
795 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
796 let _,subst,metasenv,ugraph1 =
799 (fun (j,subst,metasenv,ugraph) t1 t2 ->
802 | _,None -> j+1,subst,metasenv,ugraph
803 | Some t1', Some t2' ->
804 (* First possibility: restriction *)
805 (* Second possibility: unification *)
806 (* Third possibility: convertibility *)
809 ~subst ~metasenv context t1' t2' ugraph
812 j+1,subst,metasenv, ugraph1
815 let subst,metasenv,ugraph2 =
818 subst context metasenv t1' t2' ugraph
820 j+1,subst,metasenv,ugraph2
823 | UnificationFailure _ ->
824 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
825 let metasenv, subst =
826 CicMetaSubst.restrict
827 subst [(n,j)] metasenv in
828 j+1,subst,metasenv,ugraph1)
829 ) (1,subst,metasenv,ugraph) ln lm
833 (UnificationFailure (lazy "1"))
836 "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."
837 (CicMetaSubst.ppterm ~metasenv subst t1)
838 (CicMetaSubst.ppterm ~metasenv subst t2))) *)
839 | Invalid_argument _ ->
841 (UnificationFailure (lazy "2")))
844 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
845 (CicMetaSubst.ppterm ~metasenv subst t1)
846 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
847 in subst,metasenv,ugraph1
848 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
849 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
851 | (t, C.Meta (n,l)) ->
854 C.Meta (n,_), C.Meta (m,_) when n < m -> false
855 | _, C.Meta _ -> false
858 let lower = fun x y -> if swap then y else x in
859 let upper = fun x y -> if swap then x else y in
860 let fo_unif_subst_ordered
861 test_equality_only subst context metasenv m1 m2 ugraph =
862 fo_unif_subst test_equality_only subst context metasenv
863 (lower m1 m2) (upper m1 m2) ugraph
866 let subst,metasenv,ugraph1 =
867 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
870 type_of_aux' metasenv subst context t ugraph
874 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
876 UnificationFailure _ as e -> raise e
877 | Uncertain msg -> raise (UnificationFailure msg)
879 debug_print (lazy "siamo allo huge hack");
880 (* TODO huge hack!!!!
881 * we keep on unifying/refining in the hope that
882 * the problem will be eventually solved.
883 * In the meantime we're breaking a big invariant:
884 * the terms that we are unifying are no longer well
885 * typed in the current context (in the worst case
886 * we could even diverge) *)
887 (subst, metasenv,ugraph)) in
888 let t',metasenv,subst =
890 CicMetaSubst.delift n subst context metasenv l t
892 (CicMetaSubst.MetaSubstFailure msg)->
893 raise (UnificationFailure msg)
894 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
898 C.Sort (C.Type u) when not test_equality_only ->
899 let u' = CicUniv.fresh () in
900 let s = C.Sort (C.Type u') in
903 CicUniv.add_ge (upper u u') (lower u u') ugraph1
907 CicUniv.UniverseInconsistency msg ->
908 raise (UnificationFailure msg))
911 (* Unifying the types may have already instantiated n. Let's check *)
913 let (_, oldt,_) = CicUtil.lookup_subst n subst in
914 let lifted_oldt = S.subst_meta l oldt in
915 fo_unif_subst_ordered
916 test_equality_only subst context metasenv t lifted_oldt ugraph2
918 CicUtil.Subst_not_found _ ->
919 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
920 let subst = (n, (context, t'',ty)) :: subst in
922 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
923 subst, metasenv, ugraph2
925 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
926 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
927 if UriManager.eq uri1 uri2 then
928 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
929 exp_named_subst1 exp_named_subst2 ugraph
931 raise (UnificationFailure (lazy
933 "Can't unify %s with %s due to different constants"
934 (CicMetaSubst.ppterm ~metasenv subst t1)
935 (CicMetaSubst.ppterm ~metasenv subst t2))))
936 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
937 if UriManager.eq uri1 uri2 && i1 = i2 then
938 fo_unif_subst_exp_named_subst
940 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
942 raise (UnificationFailure
945 "Can't unify %s with %s due to different inductive principles"
946 (CicMetaSubst.ppterm ~metasenv subst t1)
947 (CicMetaSubst.ppterm ~metasenv subst t2))))
948 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
949 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
950 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
951 fo_unif_subst_exp_named_subst
953 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
955 raise (UnificationFailure
958 "Can't unify %s with %s due to different inductive constructors"
959 (CicMetaSubst.ppterm ~metasenv subst t1)
960 (CicMetaSubst.ppterm ~metasenv subst t2))))
961 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
962 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
963 subst context metasenv te t2 ugraph
964 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
965 subst context metasenv t1 te ugraph
966 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
967 let subst',metasenv',ugraph1 =
968 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
970 fo_unif_subst test_equality_only
971 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
972 | (C.LetIn (_,s1,ty1,t1), t2)
973 | (t2, C.LetIn (_,s1,ty1,t1)) ->
975 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
976 | (C.Appl l1, C.Appl l2) ->
977 (* andrea: this case should be probably rewritten in the
980 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
983 (fun (subst,metasenv,ugraph) t1 t2 ->
985 test_equality_only subst context metasenv t1 t2 ugraph)
986 (subst,metasenv,ugraph) l1 l2
987 with (Invalid_argument msg) ->
988 raise (UnificationFailure (lazy msg)))
989 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
990 (* we verify that none of the args is a Meta,
991 since beta expanding with respoect to a metavariable
995 let (_,t,_) = CicUtil.lookup_subst i subst in
996 let lifted = S.subst_meta l t in
997 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
1000 subst context metasenv reduced t2 ugraph
1001 with CicUtil.Subst_not_found _ -> *)
1002 let subst,metasenv,beta_expanded,ugraph1 =
1004 test_equality_only metasenv subst context t2 args ugraph
1006 fo_unif_subst test_equality_only subst context metasenv
1007 (C.Meta (i,l)) beta_expanded ugraph1
1008 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
1010 let (_,t,_) = CicUtil.lookup_subst i subst in
1011 let lifted = S.subst_meta l t in
1012 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
1015 subst context metasenv t1 reduced ugraph
1016 with CicUtil.Subst_not_found _ -> *)
1017 let subst,metasenv,beta_expanded,ugraph1 =
1020 metasenv subst context t1 args ugraph
1022 fo_unif_subst test_equality_only subst context metasenv
1023 (C.Meta (i,l)) beta_expanded ugraph1
1025 let lr1 = List.rev l1 in
1026 let lr2 = List.rev l2 in
1028 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
1031 | _,[] -> assert false
1034 test_equality_only subst context metasenv h1 h2 ugraph
1037 fo_unif_subst test_equality_only subst context metasenv
1038 h (C.Appl (List.rev l)) ugraph
1039 | ((h1::l1),(h2::l2)) ->
1040 let subst', metasenv',ugraph1 =
1043 subst context metasenv h1 h2 ugraph
1046 test_equality_only subst' metasenv' (l1,l2) ugraph1
1050 test_equality_only subst metasenv (lr1, lr2) ugraph
1052 | UnificationFailure s
1053 | Uncertain s as exn ->
1056 | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
1057 (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
1058 CoercDb.is_a_coercion cc1 <> None &&
1059 CoercDb.is_a_coercion cc2 <> None &&
1060 not (UriManager.eq uri1 uri2) ->
1062 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1064 let inner_coerced t =
1065 let t = CicMetaSubst.apply_subst subst t in
1069 (match CoercGraph.coerced_arg l with
1071 | Some (t,_) -> aux (List.hd l) t t)
1074 aux (Cic.Implicit None) (Cic.Implicit None) t
1076 let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
1077 let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
1080 CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
1082 | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
1085 let head1_c, head2_c =
1087 CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
1089 | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
1092 let unfold uri ens args =
1094 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
1098 | Cic.Constant (_,Some bo,_,_,_) ->
1099 CicReduction.head_beta_reduce ~delta:false
1100 (Cic.Appl (bo::args))
1103 let conclude subst metasenv ugraph last_tl1' last_tl2' =
1104 let subst',metasenv,ugraph =
1107 ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
1108 " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
1110 fo_unif_subst test_equality_only subst context
1111 metasenv last_tl1' last_tl2' ugraph
1113 if subst = subst' then raise exn
1116 let subst,metasenv,ugrph as res =
1118 fo_unif_subst test_equality_only subst' context
1119 metasenv (C.Appl l1) (C.Appl l2) ugraph
1123 (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
1124 " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1128 if CoercDb.eq_carr car1 car2 then
1129 match last_tl1,last_tl2 with
1130 | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
1133 let subst,metasenv,ugraph =
1134 fo_unif_subst test_equality_only subst context
1135 metasenv last_tl1 last_tl2 ugraph
1137 fo_unif_subst test_equality_only subst context
1138 metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
1139 | _ when CoercDb.eq_carr head1_c head2_c ->
1140 (* composite VS composition + metas avoiding
1141 * coercions not only in coerced position *)
1142 if c1 <> cc1 && c2 <> cc2 then
1143 conclude subst metasenv ugraph
1148 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
1150 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
1152 fo_unif_subst test_equality_only subst context
1153 metasenv l1 l2 ugraph
1157 match last_tl1 with Cic.Meta _ -> true | _ -> false in
1159 match last_tl2 with Cic.Meta _ -> true | _ -> false in
1160 if not (grow1 || grow2) then
1161 (* no flexible terminals -> no pullback, but
1162 * we still unify them, in some cases it helps *)
1163 conclude subst metasenv ugraph last_tl1 last_tl2
1167 metasenv subst context (grow1,car1) (grow2,car2)
1171 | (carr,metasenv,to1,to2)::xxx ->
1172 warn_if_not_unique xxx to1 to2 carr car1 car2;
1173 let last_tl1',(subst,metasenv,ugraph) =
1174 match grow1,to1 with
1175 | true,Some (last,coerced) ->
1177 fo_unif_subst test_equality_only subst context
1178 metasenv coerced last_tl1 ugraph
1179 | _ -> last_tl1,(subst,metasenv,ugraph)
1181 let last_tl2',(subst,metasenv,ugraph) =
1182 match grow2,to2 with
1183 | true,Some (last,coerced) ->
1185 fo_unif_subst test_equality_only subst context
1186 metasenv coerced last_tl2 ugraph
1187 | _ -> last_tl2,(subst,metasenv,ugraph)
1189 conclude subst metasenv ugraph last_tl1' last_tl2')
1191 (* {{{ CSC: This is necessary because of the "elim H" tactic
1192 where the type of H is only reducible to an
1193 inductive type. This could be extended from inductive
1194 types to any rigid term. However, the code is
1195 duplicated in two places: inside applications and
1196 outside them. Probably it would be better to
1197 work with lambda-bar terms instead. *)
1198 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
1199 | (_, Cic.MutInd _::_) ->
1200 let t1' = R.whd ~subst context t1 in
1202 C.Appl (C.MutInd _::_) ->
1203 fo_unif_subst test_equality_only
1204 subst context metasenv t1' t2 ugraph
1205 | _ -> raise (UnificationFailure (lazy "88")))
1206 | (Cic.MutInd _::_,_) ->
1207 let t2' = R.whd ~subst context t2 in
1209 C.Appl (C.MutInd _::_) ->
1210 fo_unif_subst test_equality_only
1211 subst context metasenv t1 t2' ugraph
1214 (lazy ("not a mutind :"^
1215 CicMetaSubst.ppterm ~metasenv subst t2 ))))
1218 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
1219 let subst', metasenv',ugraph1 =
1220 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
1222 let subst'',metasenv'',ugraph2 =
1223 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
1227 (fun (subst,metasenv,ugraph) t1 t2 ->
1229 test_equality_only subst context metasenv t1 t2 ugraph
1230 ) (subst'',metasenv'',ugraph2) pl1 pl2
1232 Invalid_argument _ ->
1233 raise (UnificationFailure (lazy "6.1")))
1235 "Error trying to unify %s with %s: the number of branches is not the same."
1236 (CicMetaSubst.ppterm ~metasenv subst t1)
1237 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
1238 | (C.Rel _, _) | (_, C.Rel _) ->
1240 subst, metasenv,ugraph
1242 raise (UnificationFailure (lazy
1244 "Can't unify %s with %s because they are not convertible"
1245 (CicMetaSubst.ppterm ~metasenv subst t1)
1246 (CicMetaSubst.ppterm ~metasenv subst t2))))
1247 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
1248 let subst,metasenv,beta_expanded,ugraph1 =
1250 test_equality_only metasenv subst context t2 args ugraph
1252 fo_unif_subst test_equality_only subst context metasenv
1253 (C.Meta (i,l)) beta_expanded ugraph1
1254 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
1255 let subst,metasenv,beta_expanded,ugraph1 =
1257 test_equality_only metasenv subst context t1 args ugraph
1259 fo_unif_subst test_equality_only subst context metasenv
1260 beta_expanded (C.Meta (i,l)) ugraph1
1261 (* Works iff there are no arguments applied to it; similar to the
1263 | (_, C.MutInd _) ->
1264 let t1' = R.whd ~subst context t1 in
1267 fo_unif_subst test_equality_only
1268 subst context metasenv t1' t2 ugraph
1269 | _ -> raise (UnificationFailure (lazy "8")))
1271 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
1272 let subst',metasenv',ugraph1 =
1273 fo_unif_subst true subst context metasenv s1 s2 ugraph
1275 fo_unif_subst test_equality_only
1276 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1278 (match CicReduction.whd ~subst context t2 with
1280 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1281 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
1283 (match CicReduction.whd ~subst context t1 with
1285 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1286 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
1288 (* delta-beta reduction should almost never be a problem for
1290 1. long computations require iota reduction
1291 2. it is extremely rare that a close term t1 (that could be unified
1292 to t2) beta-delta reduces to t1' while t2 does not beta-delta
1293 reduces in the same way. This happens only if one meta of t2
1294 occurs in head position during beta reduction. In this unluky
1295 case too much reduction will be performed on t1 and unification
1296 will surely fail. *)
1297 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
1298 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
1299 if t1 = t1' && t2 = t2' then
1300 raise (UnificationFailure
1303 "Can't unify %s with %s because they are not convertible"
1304 (CicMetaSubst.ppterm ~metasenv subst t1)
1305 (CicMetaSubst.ppterm ~metasenv subst t2))))
1308 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
1310 UnificationFailure _
1312 raise (UnificationFailure
1315 "Can't unify %s with %s because they are not convertible"
1316 (CicMetaSubst.ppterm ~metasenv subst t1)
1317 (CicMetaSubst.ppterm ~metasenv subst t2))))
1319 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
1320 exp_named_subst1 exp_named_subst2 ugraph
1324 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
1325 assert (uri1=uri2) ;
1326 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1327 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
1329 Invalid_argument _ ->
1334 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
1337 raise (UnificationFailure (lazy (sprintf
1338 "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))))
1340 (* A substitution is a (int * Cic.term) list that associates a *)
1341 (* metavariable i with its body. *)
1342 (* metasenv is of type Cic.metasenv *)
1343 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
1344 (* a new substitution which is already unwinded and ready to be applied and *)
1345 (* a new metasenv in which some hypothesis in the contexts of the *)
1346 (* metavariables may have been restricted. *)
1347 let fo_unif metasenv context t1 t2 ugraph =
1348 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
1350 let enrich_msg msg subst context metasenv t1 t2 ugraph =
1353 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"
1354 (CicMetaSubst.ppterm ~metasenv subst t1)
1356 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1359 | UnificationFailure s
1361 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1362 (CicMetaSubst.ppterm ~metasenv subst t2)
1364 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1367 | UnificationFailure s
1369 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1370 (CicMetaSubst.ppcontext ~metasenv subst context)
1371 (CicMetaSubst.ppmetasenv subst metasenv)
1372 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
1374 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
1375 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
1377 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1378 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
1380 | UnificationFailure s
1382 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1383 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
1385 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1386 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
1388 | UnificationFailure s
1390 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1391 (CicMetaSubst.ppcontext ~metasenv subst context)
1392 (CicMetaSubst.ppmetasenv subst metasenv)
1396 let fo_unif_subst subst context metasenv t1 t2 ugraph =
1398 fo_unif_subst false subst context metasenv t1 t2 ugraph
1400 | AssertFailure msg ->
1401 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1402 | UnificationFailure msg ->
1403 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))