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 ^ " " ^ s);;
82 let rec beta_expand num test_eq_only swap metasenv subst context t arg =
83 let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
87 unify test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
89 unify test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
91 (metasenv, subst), NCic.Rel (1 + n)
92 with Uncertain _ | UnificationFailure _ ->
94 | NCic.Rel m as orig ->
95 (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
96 (* andrea: in general, beta_expand can create badly typed
97 terms. This happens quite seldom in practice, UNLESS we
98 iterate on the local context. For this reason, we renounce
99 to iterate and just lift *)
100 | NCic.Meta (i,(shift,lc)) ->
101 (metasenv,subst), NCic.Meta (i,(shift+1,lc))
102 | NCic.Prod (name, src, tgt) as orig ->
103 let (metasenv, subst), src1 = aux (n,context,true) acc src in
104 let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
105 let ms, tgt1 = aux k (metasenv, subst) tgt in
106 if src == src1 && tgt == tgt1 then ms, orig else
107 ms, NCic.Prod (name, src1, tgt1)
109 NCicUntrusted.map_term_fold_a
110 (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t
113 let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
114 let fresh_name = "Hbeta" ^ string_of_int num in
115 let (metasenv,subst), t1 =
116 aux (0, context, test_eq_only) (metasenv, subst) t in
117 let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in
119 ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
121 with NCicTypeChecker.TypeCheckerFailure _ ->
122 metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
124 and beta_expand_many test_equality_only swap metasenv subst context t args =
125 (*D*) inside 'B'; try let rc =
126 pp (String.concat ", " (List.map (NCicPp.ppterm ~metasenv ~subst ~context)
127 args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t);
128 let _, subst, metasenv, hd =
130 (fun arg (num,subst,metasenv,t) ->
131 let metasenv, subst, t =
132 beta_expand num test_equality_only swap metasenv subst context t arg
134 num+1,subst,metasenv,t)
135 args (1,subst,metasenv,t)
137 pp ("Head syntesized by b-exp: " ^
138 NCicPp.ppterm ~metasenv ~subst ~context hd);
140 (*D*) in outside (); rc with exn -> outside (); raise exn
142 and instantiate test_eq_only metasenv subst context n lc t swap =
143 (*D*) inside 'I'; try let rc =
144 let unify test_eq_only m s c t1 t2 =
145 if swap then unify test_eq_only m s c t2 t1
146 else unify test_eq_only m s c t1 t2
149 try NCicTypeChecker.typeof ~subst ~metasenv context t
150 with NCicTypeChecker.TypeCheckerFailure msg ->
151 prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
152 prerr_endline (Lazy.force msg);
155 let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
156 let lty = NCicSubstitution.subst_meta lc ty in
157 pp ("On the types: " ^ NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
158 ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t);
159 let metasenv, subst = unify test_eq_only metasenv subst context lty ty_t in
160 let (metasenv, subst), t =
161 try NCicMetaSubst.delift metasenv subst context n lc t
162 with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg)
163 | NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg)
165 (* Unifying the types may have already instantiated n. *)
167 let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
168 let oldt = NCicSubstitution.subst_meta lc oldt in
169 (* conjecture: always fail --> occur check *)
170 unify test_eq_only metasenv subst context oldt t
171 with NCicUtils.Subst_not_found _ ->
172 (* by cumulativity when unify(?,Type_i)
173 * we could ? := Type_j with j <= i... *)
174 let subst = (n, (name, ctx, t, ty)) :: subst in
176 List.filter (fun (m,_) -> not (n = m)) metasenv
179 (*D*) in outside(); rc with exn -> outside (); raise exn
181 and unify test_eq_only metasenv subst context t1 t2 =
182 (*D*) inside 'U'; try let rc =
183 let fo_unif test_eq_only metasenv subst t1 t2 =
184 (*D*) inside 'F'; try let rc =
185 pp (" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^
186 NCicPp.ppterm ~metasenv ~subst ~context t2);
191 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
192 if NCicEnvironment.universe_leq a b then metasenv, subst
193 else raise (fail_exc metasenv subst context t1 t2)
194 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
195 if NCicEnvironment.universe_eq a b then metasenv, subst
196 else raise (fail_exc metasenv subst context t1 t2)
197 | (C.Sort C.Prop,C.Sort (C.Type _)) ->
198 if (not test_eq_only) then metasenv, subst
199 else raise (fail_exc metasenv subst context t1 t2)
201 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
202 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
203 let metasenv, subst = unify true metasenv subst context s1 s2 in
204 unify test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
205 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
206 let metasenv,subst=unify test_eq_only metasenv subst context ty1 ty2 in
207 let metasenv,subst=unify test_eq_only metasenv subst context s1 s2 in
208 let context = (name1, C.Def (s1,ty1))::context in
209 unify test_eq_only metasenv subst context t1 t2
211 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
213 let l1 = NCicUtils.expand_local_context l1 in
214 let l2 = NCicUtils.expand_local_context l2 in
215 let metasenv, subst, to_restrict, _ =
217 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
219 let metasenv, subst =
220 unify test_eq_only metasenv subst context
221 (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
223 metasenv, subst, to_restrict, i-1
224 with UnificationFailure _ | Uncertain _ ->
225 metasenv, subst, i::to_restrict, i-1)
226 l1 l2 (metasenv, subst, [], List.length l1)
228 let metasenv, subst, _ =
229 NCicMetaSubst.restrict metasenv subst n1 to_restrict
233 | Invalid_argument _ -> assert false
234 | NCicMetaSubst.MetaSubstFailure msg ->
236 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
237 let term1 = NCicSubstitution.subst_meta lc1 term in
238 let term2 = NCicSubstitution.subst_meta lc2 term in
239 unify test_eq_only metasenv subst context term1 term2
240 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
242 | C.Meta (n,lc), t ->
244 let _,_,term,_ = NCicUtils.lookup_subst n subst in
245 let term = NCicSubstitution.subst_meta lc term in
246 unify test_eq_only metasenv subst context term t
247 with NCicUtils.Subst_not_found _->
248 instantiate test_eq_only metasenv subst context n lc t false)
250 | t, C.Meta (n,lc) ->
252 let _,_,term,_ = NCicUtils.lookup_subst n subst in
253 let term = NCicSubstitution.subst_meta lc term in
254 unify test_eq_only metasenv subst context t term
255 with NCicUtils.Subst_not_found _->
256 instantiate test_eq_only metasenv subst context n lc t true)
258 | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
259 let _,_,term,_ = NCicUtils.lookup_subst i subst in
260 let term = NCicSubstitution.subst_meta l term in
261 unify test_eq_only metasenv subst context (mk_appl term args) t2
263 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
264 let _,_,term,_ = NCicUtils.lookup_subst i subst in
265 let term = NCicSubstitution.subst_meta l term in
266 unify test_eq_only metasenv subst context t1 (mk_appl term args)
268 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
269 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
272 (fun (metasenv, subst) t1 t2 ->
273 unify test_eq_only metasenv subst context t1 t2)
274 (metasenv,subst) l1 l2
275 with Invalid_argument _ ->
276 raise (fail_exc metasenv subst context t1 t2))
278 | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
279 (* we verify that none of the args is a Meta,
280 since beta expanding w.r.t a metavariable makes no sense *)
281 let metasenv, subst, beta_expanded =
284 metasenv subst context t2 args
286 unify test_eq_only metasenv subst context
287 (C.Meta (i,l)) beta_expanded
289 | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
290 let metasenv, subst, beta_expanded =
293 metasenv subst context t1 args
295 unify test_eq_only metasenv subst context
296 beta_expanded (C.Meta (i,l))
298 (* processing this case here we avoid a useless small delta step *)
299 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
301 let relevance = NCicEnvironment.get_relevance r1 in
302 let relevance = match r1 with
303 | Ref.Ref (_,Ref.Con (_,_,lno)) ->
304 let _,relevance = HExtlib.split_nth lno relevance in
305 HExtlib.mk_list false lno @ relevance
308 let metasenv, subst, _ =
311 (fun (metasenv, subst, relevance) t1 t2 ->
313 match relevance with b::tl -> b,tl | _ -> true, [] in
314 let metasenv, subst =
315 try unify test_eq_only metasenv subst context t1 t2
316 with UnificationFailure _ | Uncertain _ when not b ->
319 metasenv, subst, relevance)
320 (metasenv, subst, relevance) tl1 tl2
321 with Invalid_argument _ ->
322 raise (uncert_exc metasenv subst context t1 t2)
326 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
327 C.Match (ref2,outtype2,term2,pl2)) ->
328 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
329 let _,_,ty,_ = List.nth itl tyno in
330 let rec remove_prods ~subst context ty =
331 let ty = NCicReduction.whd ~subst context ty in
334 | C.Prod (name,so,ta) ->
335 remove_prods ~subst ((name,(C.Decl so))::context) ta
339 match remove_prods ~subst [] ty with
340 | C.Sort C.Prop -> true
343 let rec remove_prods ~subst context ty =
344 let ty = NCicReduction.whd ~subst context ty in
347 | C.Prod (name,so,ta) ->
348 remove_prods ~subst ((name,(C.Decl so))::context) ta
351 if not (Ref.eq ref1 ref2) then
352 raise (uncert_exc metasenv subst context t1 t2)
354 let metasenv, subst =
355 unify test_eq_only metasenv subst context outtype1 outtype2 in
356 let metasenv, subst =
357 try unify test_eq_only metasenv subst context term1 term2
358 with UnificationFailure _ | Uncertain _ when is_prop ->
363 (fun (metasenv,subst) ->
364 unify test_eq_only metasenv subst context)
365 (metasenv, subst) pl1 pl2
366 with Invalid_argument _ ->
367 raise (uncert_exc metasenv subst context t1 t2))
368 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
369 | _ -> raise (uncert_exc metasenv subst context t1 t2)
370 (*D*) in outside(); rc with exn -> outside (); raise exn
372 let height_of = function
373 | NCic.Const (Ref.Ref (_,Ref.Def h))
374 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
375 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
376 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h, false
377 | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> 0, true
380 let put_in_whd m1 m2 =
381 NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
382 NCicReduction.reduce_machine ~delta:max_int ~subst context m2,
383 false (* not in normal form *)
385 let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
386 let h1, flex1 = height_of t1 in
387 let h2, flex2 = height_of t2 in
389 if flex1 then max 0 (h2 - 1) else
390 if flex2 then max 0 (h1 - 1) else
391 if h1 = h2 then max 0 (h1 -1) else min h1 h2
393 pp ("DELTA STEP TO: " ^ string_of_int delta);
394 let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in
395 let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in
396 m1', m2', (m1' == m1 && m2' == m2) || delta = 0
397 (* if we have as heads two Fix of height n>0, they may or may not
398 * reduce, depending on their rec argument... we thus check if
399 * something changed or not. This relies on the reduction machine
400 * preserving the original machine if it performs no action *)
402 let rec unif_machines metasenv subst =
404 | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),are_normal) ->
405 (*D*) inside 'M'; try let rc =
406 pp ((if are_normal then "*" else " ") ^ " " ^
407 NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
409 NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2));
410 let relevance = [] (* TO BE UNDERSTOOD
412 | C.Const r -> NCicEnvironment.get_relevance r
414 let unif_from_stack t1 t2 b metasenv subst =
416 let t1 = NCicReduction.from_stack t1 in
417 let t2 = NCicReduction.from_stack t2 in
418 unif_machines metasenv subst (put_in_whd t1 t2)
419 with UnificationFailure _ | Uncertain _ when not b ->
422 let rec check_stack l1 l2 r (metasenv, subst) =
424 | x1::tl1, x2::tl2, r::tr ->
425 check_stack tl1 tl2 tr
426 (unif_from_stack x1 x2 r metasenv subst)
427 | x1::tl1, x2::tl2, [] ->
428 check_stack tl1 tl2 []
429 (unif_from_stack x1 x2 true metasenv subst)
431 fo_unif test_eq_only metasenv subst
432 (NCicReduction.unwind (k1,e1,t1,List.rev l1))
433 (NCicReduction.unwind (k2,e2,t2,List.rev l2))
435 try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
436 with UnificationFailure _ | Uncertain _ when not are_normal ->
438 let delta = delta - 1 in
439 let red = NCicReduction.reduce_machine ~delta ~subst context in
441 unif_machines metasenv subst (small_delta_step m1 m2)
442 (*D*) in outside(); rc with exn -> outside (); raise exn
444 try fo_unif test_eq_only metasenv subst t1 t2
445 with UnificationFailure msg | Uncertain msg as exn ->
447 unif_machines metasenv subst
448 (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
450 | UnificationFailure _ -> raise (UnificationFailure msg)
451 | Uncertain _ -> raise exn
452 (*D*) in outside(); rc with exn -> outside (); raise exn
465 exception UnificationFailure of string Lazy.t;;
466 exception Uncertain of string Lazy.t;;
467 exception AssertFailure of string Lazy.t;;
469 let verbose = false;;
470 let debug_print = fun _ -> ()
472 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
473 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
474 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
475 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
477 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
479 let type_of_aux' metasenv subst context term ugraph =
482 profile.HExtlib.profile
483 (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
485 CicTypeChecker.TypeCheckerFailure msg ->
489 "Kernel Type checking error:
490 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
491 (CicMetaSubst.ppterm ~metasenv subst term)
492 (CicMetaSubst.ppterm ~metasenv [] term)
493 (CicMetaSubst.ppcontext ~metasenv subst context)
494 (CicMetaSubst.ppmetasenv subst metasenv)
495 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
496 raise (AssertFailure msg)
497 | CicTypeChecker.AssertFailure msg ->
500 "Kernel Type checking assertion failure:
501 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
502 (CicMetaSubst.ppterm ~metasenv subst term)
503 (CicMetaSubst.ppterm ~metasenv [] term)
504 (CicMetaSubst.ppcontext ~metasenv subst context)
505 (CicMetaSubst.ppmetasenv subst metasenv)
506 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
507 raise (AssertFailure msg)
508 in profiler_toa.HExtlib.profile foo ()
511 let exists_a_meta l =
515 | Cic.Appl (Cic.Meta _::_) -> true
518 let rec deref subst t =
519 let snd (_,a,_) = a in
524 (CicSubstitution.subst_meta
525 l (snd (CicUtil.lookup_subst n subst)))
527 CicUtil.Subst_not_found _ -> t)
528 | Cic.Appl(Cic.Meta(n,l)::args) ->
529 (match deref subst (Cic.Meta(n,l)) with
530 | Cic.Lambda _ as t ->
531 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
532 | r -> Cic.Appl(r::args))
533 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
534 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
539 let foo () = deref subst t
540 in profiler_deref.HExtlib.profile foo ()
542 exception WrongShape;;
543 let eta_reduce after_beta_expansion after_beta_expansion_body
544 before_beta_expansion
547 match before_beta_expansion,after_beta_expansion_body with
548 Cic.Appl l, Cic.Appl l' ->
549 let rec all_but_last check_last =
553 | [_] -> if check_last then raise WrongShape else []
554 | he::tl -> he::(all_but_last check_last tl)
556 let all_but_last check_last l =
557 match all_but_last check_last l with
562 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
563 let all_but_last = all_but_last false l in
564 (* here we should test alpha-equivalence; however we know by
565 construction that here alpha_equivalence is equivalent to = *)
566 if t = all_but_last then
570 | _,_ -> after_beta_expansion
572 WrongShape -> after_beta_expansion
574 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
575 let module S = CicSubstitution in
576 let module C = Cic in
578 let rec aux metasenv subst n context t' ugraph =
581 let subst,metasenv,ugraph1 =
582 fo_unif_subst test_equality_only subst context metasenv
583 (CicSubstitution.lift n arg) t' ugraph
586 subst,metasenv,C.Rel (1 + n),ugraph1
589 | UnificationFailure _ ->
591 | C.Rel m -> subst,metasenv,
592 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
593 | C.Var (uri,exp_named_subst) ->
594 let subst,metasenv,exp_named_subst',ugraph1 =
595 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
597 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
599 (* andrea: in general, beta_expand can create badly typed
600 terms. This happens quite seldom in practice, UNLESS we
601 iterate on the local context. For this reason, we renounce
602 to iterate and just lift *)
606 Some t -> Some (CicSubstitution.lift 1 t)
608 subst, metasenv, C.Meta (i,l), ugraph
610 | C.Implicit _ as t -> subst,metasenv,t,ugraph
612 let subst,metasenv,te',ugraph1 =
613 aux metasenv subst n context te ugraph in
614 let subst,metasenv,ty',ugraph2 =
615 aux metasenv subst n context ty ugraph1 in
616 (* TASSI: sure this is in serial? *)
617 subst,metasenv,(C.Cast (te', ty')),ugraph2
619 let subst,metasenv,s',ugraph1 =
620 aux metasenv subst n context s ugraph in
621 let subst,metasenv,t',ugraph2 =
622 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
625 (* TASSI: sure this is in serial? *)
626 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
627 | C.Lambda (nn,s,t) ->
628 let subst,metasenv,s',ugraph1 =
629 aux metasenv subst n context s ugraph in
630 let subst,metasenv,t',ugraph2 =
631 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
633 (* TASSI: sure this is in serial? *)
634 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
635 | C.LetIn (nn,s,ty,t) ->
636 let subst,metasenv,s',ugraph1 =
637 aux metasenv subst n context s ugraph in
638 let subst,metasenv,ty',ugraph1 =
639 aux metasenv subst n context ty ugraph in
640 let subst,metasenv,t',ugraph2 =
641 aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
644 (* TASSI: sure this is in serial? *)
645 subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
647 let subst,metasenv,revl',ugraph1 =
649 (fun (subst,metasenv,appl,ugraph) t ->
650 let subst,metasenv,t',ugraph1 =
651 aux metasenv subst n context t ugraph in
652 subst,metasenv,(t'::appl),ugraph1
653 ) (subst,metasenv,[],ugraph) l
655 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
656 | C.Const (uri,exp_named_subst) ->
657 let subst,metasenv,exp_named_subst',ugraph1 =
658 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
660 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
661 | C.MutInd (uri,i,exp_named_subst) ->
662 let subst,metasenv,exp_named_subst',ugraph1 =
663 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
665 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
666 | C.MutConstruct (uri,i,j,exp_named_subst) ->
667 let subst,metasenv,exp_named_subst',ugraph1 =
668 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
670 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
671 | C.MutCase (sp,i,outt,t,pl) ->
672 let subst,metasenv,outt',ugraph1 =
673 aux metasenv subst n context outt ugraph in
674 let subst,metasenv,t',ugraph2 =
675 aux metasenv subst n context t ugraph1 in
676 let subst,metasenv,revpl',ugraph3 =
678 (fun (subst,metasenv,pl,ugraph) t ->
679 let subst,metasenv,t',ugraph1 =
680 aux metasenv subst n context t ugraph in
681 subst,metasenv,(t'::pl),ugraph1
682 ) (subst,metasenv,[],ugraph2) pl
684 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
685 (* TASSI: not sure this is serial *)
687 (*CSC: not implemented
688 let tylen = List.length fl in
691 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
694 C.Fix (i, substitutedfl)
696 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
698 (*CSC: not implemented
699 let tylen = List.length fl in
702 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
705 C.CoFix (i, substitutedfl)
708 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
710 and aux_exp_named_subst metasenv subst n context ens ugraph =
712 (fun (uri,t) (subst,metasenv,l,ugraph) ->
713 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
714 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
716 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
718 FreshNamesGenerator.mk_fresh_name ~subst
719 metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
721 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
722 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
723 subst, metasenv, t'', ugraph2
724 in profiler_beta_expand.HExtlib.profile foo ()
727 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
728 let _,subst,metasenv,hd,ugraph =
730 (fun arg (num,subst,metasenv,t,ugraph) ->
731 let subst,metasenv,t,ugraph1 =
732 beta_expand num test_equality_only
733 metasenv subst context t arg ugraph
735 num+1,subst,metasenv,t,ugraph1
736 ) args (1,subst,metasenv,t,ugraph)
738 subst,metasenv,hd,ugraph
740 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
743 | (m2,_,c2,c2')::_ ->
744 let m1,c1,c1' = carr,to1,to2 in
746 function Some (_,t) -> CicPp.ppterm t
750 ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
751 CoercDb.string_of_carr car2^": " ^
752 CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
753 unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
754 unopt c2^" + "^unopt c2')
756 (* NUOVA UNIFICAZIONE *)
757 (* A substitution is a (int * Cic.term) list that associates a
758 metavariable i with its body.
759 A metaenv is a (int * Cic.term) list that associate a metavariable
761 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
762 a new substitution which is _NOT_ unwinded. It must be unwinded before
765 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
766 let module C = Cic in
767 let module R = CicReduction in
768 let module S = CicSubstitution in
769 let t1 = deref subst t1 in
770 let t2 = deref subst t2 in
771 let (&&&) a b = (a && b) || ((not a) && (not b)) in
772 (* let bef = Sys.time () in *)
774 if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
778 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
779 in profiler_are_convertible.HExtlib.profile foo ()
781 (* let aft = Sys.time () in
782 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
783 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
784 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
786 subst, metasenv, ugraph
789 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
790 let _,subst,metasenv,ugraph1 =
793 (fun (j,subst,metasenv,ugraph) t1 t2 ->
796 | _,None -> j+1,subst,metasenv,ugraph
797 | Some t1', Some t2' ->
798 (* First possibility: restriction *)
799 (* Second possibility: unification *)
800 (* Third possibility: convertibility *)
803 ~subst ~metasenv context t1' t2' ugraph
806 j+1,subst,metasenv, ugraph1
809 let subst,metasenv,ugraph2 =
812 subst context metasenv t1' t2' ugraph
814 j+1,subst,metasenv,ugraph2
817 | UnificationFailure _ ->
818 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
819 let metasenv, subst =
820 CicMetaSubst.restrict
821 subst [(n,j)] metasenv in
822 j+1,subst,metasenv,ugraph1)
823 ) (1,subst,metasenv,ugraph) ln lm
827 (UnificationFailure (lazy "1"))
830 "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."
831 (CicMetaSubst.ppterm ~metasenv subst t1)
832 (CicMetaSubst.ppterm ~metasenv subst t2))) *)
833 | Invalid_argument _ ->
835 (UnificationFailure (lazy "2")))
838 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
839 (CicMetaSubst.ppterm ~metasenv subst t1)
840 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
841 in subst,metasenv,ugraph1
842 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
843 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
845 | (t, C.Meta (n,l)) ->
848 C.Meta (n,_), C.Meta (m,_) when n < m -> false
849 | _, C.Meta _ -> false
852 let lower = fun x y -> if swap then y else x in
853 let upper = fun x y -> if swap then x else y in
854 let fo_unif_subst_ordered
855 test_equality_only subst context metasenv m1 m2 ugraph =
856 fo_unif_subst test_equality_only subst context metasenv
857 (lower m1 m2) (upper m1 m2) ugraph
860 let subst,metasenv,ugraph1 =
861 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
864 type_of_aux' metasenv subst context t ugraph
868 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
870 UnificationFailure _ as e -> raise e
871 | Uncertain msg -> raise (UnificationFailure msg)
873 debug_print (lazy "siamo allo huge hack");
874 (* TODO huge hack!!!!
875 * we keep on unifying/refining in the hope that
876 * the problem will be eventually solved.
877 * In the meantime we're breaking a big invariant:
878 * the terms that we are unifying are no longer well
879 * typed in the current context (in the worst case
880 * we could even diverge) *)
881 (subst, metasenv,ugraph)) in
882 let t',metasenv,subst =
884 CicMetaSubst.delift n subst context metasenv l t
886 (CicMetaSubst.MetaSubstFailure msg)->
887 raise (UnificationFailure msg)
888 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
892 C.Sort (C.Type u) when not test_equality_only ->
893 let u' = CicUniv.fresh () in
894 let s = C.Sort (C.Type u') in
897 CicUniv.add_ge (upper u u') (lower u u') ugraph1
901 CicUniv.UniverseInconsistency msg ->
902 raise (UnificationFailure msg))
905 (* Unifying the types may have already instantiated n. Let's check *)
907 let (_, oldt,_) = CicUtil.lookup_subst n subst in
908 let lifted_oldt = S.subst_meta l oldt in
909 fo_unif_subst_ordered
910 test_equality_only subst context metasenv t lifted_oldt ugraph2
912 CicUtil.Subst_not_found _ ->
913 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
914 let subst = (n, (context, t'',ty)) :: subst in
916 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
917 subst, metasenv, ugraph2
919 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
920 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
921 if UriManager.eq uri1 uri2 then
922 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
923 exp_named_subst1 exp_named_subst2 ugraph
925 raise (UnificationFailure (lazy
927 "Can't unify %s with %s due to different constants"
928 (CicMetaSubst.ppterm ~metasenv subst t1)
929 (CicMetaSubst.ppterm ~metasenv subst t2))))
930 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
931 if UriManager.eq uri1 uri2 && i1 = i2 then
932 fo_unif_subst_exp_named_subst
934 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
936 raise (UnificationFailure
939 "Can't unify %s with %s due to different inductive principles"
940 (CicMetaSubst.ppterm ~metasenv subst t1)
941 (CicMetaSubst.ppterm ~metasenv subst t2))))
942 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
943 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
944 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
945 fo_unif_subst_exp_named_subst
947 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
949 raise (UnificationFailure
952 "Can't unify %s with %s due to different inductive constructors"
953 (CicMetaSubst.ppterm ~metasenv subst t1)
954 (CicMetaSubst.ppterm ~metasenv subst t2))))
955 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
956 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
957 subst context metasenv te t2 ugraph
958 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
959 subst context metasenv t1 te ugraph
960 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
961 let subst',metasenv',ugraph1 =
962 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
964 fo_unif_subst test_equality_only
965 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
966 | (C.LetIn (_,s1,ty1,t1), t2)
967 | (t2, C.LetIn (_,s1,ty1,t1)) ->
969 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
970 | (C.Appl l1, C.Appl l2) ->
971 (* andrea: this case should be probably rewritten in the
974 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
977 (fun (subst,metasenv,ugraph) t1 t2 ->
979 test_equality_only subst context metasenv t1 t2 ugraph)
980 (subst,metasenv,ugraph) l1 l2
981 with (Invalid_argument msg) ->
982 raise (UnificationFailure (lazy msg)))
983 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
984 (* we verify that none of the args is a Meta,
985 since beta expanding with respoect to a metavariable
989 let (_,t,_) = CicUtil.lookup_subst i subst in
990 let lifted = S.subst_meta l t in
991 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
994 subst context metasenv reduced t2 ugraph
995 with CicUtil.Subst_not_found _ -> *)
996 let subst,metasenv,beta_expanded,ugraph1 =
998 test_equality_only metasenv subst context t2 args ugraph
1000 fo_unif_subst test_equality_only subst context metasenv
1001 (C.Meta (i,l)) beta_expanded ugraph1
1002 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
1004 let (_,t,_) = CicUtil.lookup_subst i subst in
1005 let lifted = S.subst_meta l t in
1006 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
1009 subst context metasenv t1 reduced ugraph
1010 with CicUtil.Subst_not_found _ -> *)
1011 let subst,metasenv,beta_expanded,ugraph1 =
1014 metasenv subst context t1 args ugraph
1016 fo_unif_subst test_equality_only subst context metasenv
1017 (C.Meta (i,l)) beta_expanded ugraph1
1019 let lr1 = List.rev l1 in
1020 let lr2 = List.rev l2 in
1022 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
1025 | _,[] -> assert false
1028 test_equality_only subst context metasenv h1 h2 ugraph
1031 fo_unif_subst test_equality_only subst context metasenv
1032 h (C.Appl (List.rev l)) ugraph
1033 | ((h1::l1),(h2::l2)) ->
1034 let subst', metasenv',ugraph1 =
1037 subst context metasenv h1 h2 ugraph
1040 test_equality_only subst' metasenv' (l1,l2) ugraph1
1044 test_equality_only subst metasenv (lr1, lr2) ugraph
1046 | UnificationFailure s
1047 | Uncertain s as exn ->
1050 | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
1051 (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
1052 CoercDb.is_a_coercion cc1 <> None &&
1053 CoercDb.is_a_coercion cc2 <> None &&
1054 not (UriManager.eq uri1 uri2) ->
1056 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1058 let inner_coerced t =
1059 let t = CicMetaSubst.apply_subst subst t in
1063 (match CoercGraph.coerced_arg l with
1065 | Some (t,_) -> aux (List.hd l) t t)
1068 aux (Cic.Implicit None) (Cic.Implicit None) t
1070 let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
1071 let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
1074 CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
1076 | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
1079 let head1_c, head2_c =
1081 CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
1083 | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
1086 let unfold uri ens args =
1088 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
1092 | Cic.Constant (_,Some bo,_,_,_) ->
1093 CicReduction.head_beta_reduce ~delta:false
1094 (Cic.Appl (bo::args))
1097 let conclude subst metasenv ugraph last_tl1' last_tl2' =
1098 let subst',metasenv,ugraph =
1101 ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
1102 " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
1104 fo_unif_subst test_equality_only subst context
1105 metasenv last_tl1' last_tl2' ugraph
1107 if subst = subst' then raise exn
1110 let subst,metasenv,ugrph as res =
1112 fo_unif_subst test_equality_only subst' context
1113 metasenv (C.Appl l1) (C.Appl l2) ugraph
1117 (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
1118 " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1122 if CoercDb.eq_carr car1 car2 then
1123 match last_tl1,last_tl2 with
1124 | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
1127 let subst,metasenv,ugraph =
1128 fo_unif_subst test_equality_only subst context
1129 metasenv last_tl1 last_tl2 ugraph
1131 fo_unif_subst test_equality_only subst context
1132 metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
1133 | _ when CoercDb.eq_carr head1_c head2_c ->
1134 (* composite VS composition + metas avoiding
1135 * coercions not only in coerced position *)
1136 if c1 <> cc1 && c2 <> cc2 then
1137 conclude subst metasenv ugraph
1142 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
1144 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
1146 fo_unif_subst test_equality_only subst context
1147 metasenv l1 l2 ugraph
1151 match last_tl1 with Cic.Meta _ -> true | _ -> false in
1153 match last_tl2 with Cic.Meta _ -> true | _ -> false in
1154 if not (grow1 || grow2) then
1155 (* no flexible terminals -> no pullback, but
1156 * we still unify them, in some cases it helps *)
1157 conclude subst metasenv ugraph last_tl1 last_tl2
1161 metasenv subst context (grow1,car1) (grow2,car2)
1165 | (carr,metasenv,to1,to2)::xxx ->
1166 warn_if_not_unique xxx to1 to2 carr car1 car2;
1167 let last_tl1',(subst,metasenv,ugraph) =
1168 match grow1,to1 with
1169 | true,Some (last,coerced) ->
1171 fo_unif_subst test_equality_only subst context
1172 metasenv coerced last_tl1 ugraph
1173 | _ -> last_tl1,(subst,metasenv,ugraph)
1175 let last_tl2',(subst,metasenv,ugraph) =
1176 match grow2,to2 with
1177 | true,Some (last,coerced) ->
1179 fo_unif_subst test_equality_only subst context
1180 metasenv coerced last_tl2 ugraph
1181 | _ -> last_tl2,(subst,metasenv,ugraph)
1183 conclude subst metasenv ugraph last_tl1' last_tl2')
1185 (* {{{ CSC: This is necessary because of the "elim H" tactic
1186 where the type of H is only reducible to an
1187 inductive type. This could be extended from inductive
1188 types to any rigid term. However, the code is
1189 duplicated in two places: inside applications and
1190 outside them. Probably it would be better to
1191 work with lambda-bar terms instead. *)
1192 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
1193 | (_, Cic.MutInd _::_) ->
1194 let t1' = R.whd ~subst context t1 in
1196 C.Appl (C.MutInd _::_) ->
1197 fo_unif_subst test_equality_only
1198 subst context metasenv t1' t2 ugraph
1199 | _ -> raise (UnificationFailure (lazy "88")))
1200 | (Cic.MutInd _::_,_) ->
1201 let t2' = R.whd ~subst context t2 in
1203 C.Appl (C.MutInd _::_) ->
1204 fo_unif_subst test_equality_only
1205 subst context metasenv t1 t2' ugraph
1208 (lazy ("not a mutind :"^
1209 CicMetaSubst.ppterm ~metasenv subst t2 ))))
1212 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
1213 let subst', metasenv',ugraph1 =
1214 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
1216 let subst'',metasenv'',ugraph2 =
1217 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
1221 (fun (subst,metasenv,ugraph) t1 t2 ->
1223 test_equality_only subst context metasenv t1 t2 ugraph
1224 ) (subst'',metasenv'',ugraph2) pl1 pl2
1226 Invalid_argument _ ->
1227 raise (UnificationFailure (lazy "6.1")))
1229 "Error trying to unify %s with %s: the number of branches is not the same."
1230 (CicMetaSubst.ppterm ~metasenv subst t1)
1231 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
1232 | (C.Rel _, _) | (_, C.Rel _) ->
1234 subst, metasenv,ugraph
1236 raise (UnificationFailure (lazy
1238 "Can't unify %s with %s because they are not convertible"
1239 (CicMetaSubst.ppterm ~metasenv subst t1)
1240 (CicMetaSubst.ppterm ~metasenv subst t2))))
1241 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
1242 let subst,metasenv,beta_expanded,ugraph1 =
1244 test_equality_only metasenv subst context t2 args ugraph
1246 fo_unif_subst test_equality_only subst context metasenv
1247 (C.Meta (i,l)) beta_expanded ugraph1
1248 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
1249 let subst,metasenv,beta_expanded,ugraph1 =
1251 test_equality_only metasenv subst context t1 args ugraph
1253 fo_unif_subst test_equality_only subst context metasenv
1254 beta_expanded (C.Meta (i,l)) ugraph1
1255 (* Works iff there are no arguments applied to it; similar to the
1257 | (_, C.MutInd _) ->
1258 let t1' = R.whd ~subst context t1 in
1261 fo_unif_subst test_equality_only
1262 subst context metasenv t1' t2 ugraph
1263 | _ -> raise (UnificationFailure (lazy "8")))
1265 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
1266 let subst',metasenv',ugraph1 =
1267 fo_unif_subst true subst context metasenv s1 s2 ugraph
1269 fo_unif_subst test_equality_only
1270 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1272 (match CicReduction.whd ~subst context t2 with
1274 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1275 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
1277 (match CicReduction.whd ~subst context t1 with
1279 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1280 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
1282 (* delta-beta reduction should almost never be a problem for
1284 1. long computations require iota reduction
1285 2. it is extremely rare that a close term t1 (that could be unified
1286 to t2) beta-delta reduces to t1' while t2 does not beta-delta
1287 reduces in the same way. This happens only if one meta of t2
1288 occurs in head position during beta reduction. In this unluky
1289 case too much reduction will be performed on t1 and unification
1290 will surely fail. *)
1291 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
1292 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
1293 if t1 = t1' && t2 = t2' then
1294 raise (UnificationFailure
1297 "Can't unify %s with %s because they are not convertible"
1298 (CicMetaSubst.ppterm ~metasenv subst t1)
1299 (CicMetaSubst.ppterm ~metasenv subst t2))))
1302 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
1304 UnificationFailure _
1306 raise (UnificationFailure
1309 "Can't unify %s with %s because they are not convertible"
1310 (CicMetaSubst.ppterm ~metasenv subst t1)
1311 (CicMetaSubst.ppterm ~metasenv subst t2))))
1313 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
1314 exp_named_subst1 exp_named_subst2 ugraph
1318 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
1319 assert (uri1=uri2) ;
1320 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1321 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
1323 Invalid_argument _ ->
1328 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
1331 raise (UnificationFailure (lazy (sprintf
1332 "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))))
1334 (* A substitution is a (int * Cic.term) list that associates a *)
1335 (* metavariable i with its body. *)
1336 (* metasenv is of type Cic.metasenv *)
1337 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
1338 (* a new substitution which is already unwinded and ready to be applied and *)
1339 (* a new metasenv in which some hypothesis in the contexts of the *)
1340 (* metavariables may have been restricted. *)
1341 let fo_unif metasenv context t1 t2 ugraph =
1342 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
1344 let enrich_msg msg subst context metasenv t1 t2 ugraph =
1347 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"
1348 (CicMetaSubst.ppterm ~metasenv subst t1)
1350 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1353 | UnificationFailure s
1355 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1356 (CicMetaSubst.ppterm ~metasenv subst t2)
1358 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1361 | UnificationFailure s
1363 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1364 (CicMetaSubst.ppcontext ~metasenv subst context)
1365 (CicMetaSubst.ppmetasenv subst metasenv)
1366 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
1368 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
1369 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
1371 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1372 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
1374 | UnificationFailure s
1376 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1377 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
1379 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1380 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
1382 | UnificationFailure s
1384 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1385 (CicMetaSubst.ppcontext ~metasenv subst context)
1386 (CicMetaSubst.ppmetasenv subst metasenv)
1390 let fo_unif_subst subst context metasenv t1 t2 ugraph =
1392 fo_unif_subst false subst context metasenv t1 t2 ugraph
1394 | AssertFailure msg ->
1395 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1396 | UnificationFailure msg ->
1397 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))