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 fix_sorts swap metasenv subst context meta t =
84 let rec aux () = function
85 | NCic.Sort (NCic.Type u) as orig ->
87 match NCicEnvironment.sup u with
88 | None -> raise (fail_exc metasenv subst context meta t)
89 | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
91 NCic.Sort (NCic.Type (
92 match NCicEnvironment.sup NCicEnvironment.type0 with
95 | NCic.Meta _ as orig -> orig
96 | t -> NCicUtils.map (fun _ _ -> ()) () aux t
101 let rec beta_expand num test_eq_only swap metasenv subst context t arg =
102 let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
104 let metasenv, subst =
106 unify test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
108 unify test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
110 (metasenv, subst), NCic.Rel (1 + n)
111 with Uncertain _ | UnificationFailure _ ->
113 | NCic.Rel m as orig ->
114 (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
115 (* andrea: in general, beta_expand can create badly typed
116 terms. This happens quite seldom in practice, UNLESS we
117 iterate on the local context. For this reason, we renounce
118 to iterate and just lift *)
119 | NCic.Meta (i,(shift,lc)) ->
120 (metasenv,subst), NCic.Meta (i,(shift+1,lc))
121 | NCic.Prod (name, src, tgt) as orig ->
122 let (metasenv, subst), src1 = aux (n,context,true) acc src in
123 let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
124 let ms, tgt1 = aux k (metasenv, subst) tgt in
125 if src == src1 && tgt == tgt1 then ms, orig else
126 ms, NCic.Prod (name, src1, tgt1)
128 NCicUntrusted.map_term_fold_a
129 (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t
132 let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
133 let fresh_name = "Hbeta" ^ string_of_int num in
134 let (metasenv,subst), t1 =
135 aux (0, context, test_eq_only) (metasenv, subst) t in
136 let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in
138 ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
140 with NCicTypeChecker.TypeCheckerFailure _ ->
141 metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
143 and beta_expand_many test_equality_only swap metasenv subst context t args =
144 (* (*D*) inside 'B'; try let rc = *)
145 pp (lazy (String.concat ", "
146 (List.map (NCicPp.ppterm ~metasenv ~subst ~context)
147 args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
148 let _, subst, metasenv, hd =
150 (fun arg (num,subst,metasenv,t) ->
151 let metasenv, subst, t =
152 beta_expand num test_equality_only swap metasenv subst context t arg
154 num+1,subst,metasenv,t)
155 args (1,subst,metasenv,t)
157 pp (lazy ("Head syntesized by b-exp: " ^
158 NCicPp.ppterm ~metasenv ~subst ~context hd));
160 (* (*D*) in outside (); rc with exn -> outside (); raise exn *)
162 and instantiate test_eq_only metasenv subst context n lc t swap =
163 (*D*) inside 'I'; try let rc =
164 let unify test_eq_only m s c t1 t2 =
165 if swap then unify test_eq_only m s c t2 t1
166 else unify test_eq_only m s c t1 t2
168 let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
169 let metasenv, subst, t =
171 | NCic.Implicit (`Typeof _) ->
172 metasenv,subst,fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t
174 pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
176 try t, NCicTypeChecker.typeof ~subst ~metasenv context t
177 with NCicTypeChecker.TypeCheckerFailure _ ->
179 fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t
181 if ft == t then assert false
184 pp (lazy ("typeof: " ^
185 NCicPp.ppterm ~metasenv ~subst ~context ft));
186 ft, NCicTypeChecker.typeof ~subst ~metasenv context ft
187 with NCicTypeChecker.TypeCheckerFailure _ ->
190 let lty = NCicSubstitution.subst_meta lc ty in
191 pp (lazy("On the types: " ^
192 NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
193 NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
194 ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
195 let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
198 let (metasenv, subst), t =
199 try NCicMetaSubst.delift metasenv subst context n lc t
200 with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg)
201 | NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg)
203 (* Unifying the types may have already instantiated n. *)
205 let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
206 let oldt = NCicSubstitution.subst_meta lc oldt in
207 let t = NCicSubstitution.subst_meta lc t in
208 (* conjecture: always fail --> occur check *)
209 unify test_eq_only metasenv subst context oldt t
210 with NCicUtils.Subst_not_found _ ->
211 (* by cumulativity when unify(?,Type_i)
212 * we could ? := Type_j with j <= i... *)
213 let subst = (n, (name, ctx, t, ty)) :: subst in
214 pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
215 ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
217 List.filter (fun (m,_) -> not (n = m)) metasenv
220 (*D*) in outside(); rc with exn -> outside (); raise exn
222 and unify test_eq_only metasenv subst context t1 t2 =
223 (*D*) inside 'U'; try let rc =
224 let fo_unif test_eq_only metasenv subst t1 t2 =
225 (*D*) inside 'F'; try let rc =
226 pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^
227 NCicPp.ppterm ~metasenv ~subst ~context t2));
232 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
233 if NCicEnvironment.universe_leq a b then metasenv, subst
234 else raise (fail_exc metasenv subst context t1 t2)
235 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
236 if NCicEnvironment.universe_eq a b then metasenv, subst
237 else raise (fail_exc metasenv subst context t1 t2)
238 | (C.Sort C.Prop,C.Sort (C.Type _)) ->
239 if (not test_eq_only) then metasenv, subst
240 else raise (fail_exc metasenv subst context t1 t2)
242 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
243 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
244 let metasenv, subst = unify true metasenv subst context s1 s2 in
245 unify test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
246 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
247 let metasenv,subst=unify test_eq_only metasenv subst context ty1 ty2 in
248 let metasenv,subst=unify test_eq_only metasenv subst context s1 s2 in
249 let context = (name1, C.Def (s1,ty1))::context in
250 unify test_eq_only metasenv subst context t1 t2
252 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
254 let l1 = NCicUtils.expand_local_context l1 in
255 let l2 = NCicUtils.expand_local_context l2 in
256 let metasenv, subst, to_restrict, _ =
258 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
260 let metasenv, subst =
261 unify test_eq_only metasenv subst context
262 (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
264 metasenv, subst, to_restrict, i-1
265 with UnificationFailure _ | Uncertain _ ->
266 metasenv, subst, i::to_restrict, i-1)
267 l1 l2 (metasenv, subst, [], List.length l1)
269 let metasenv, subst, _ =
270 NCicMetaSubst.restrict metasenv subst n1 to_restrict
274 | Invalid_argument _ -> assert false
275 | NCicMetaSubst.MetaSubstFailure msg ->
277 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
278 let term1 = NCicSubstitution.subst_meta lc1 term in
279 let term2 = NCicSubstitution.subst_meta lc2 term in
280 unify test_eq_only metasenv subst context term1 term2
281 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
283 | C.Meta (n,lc), t ->
285 let _,_,term,_ = NCicUtils.lookup_subst n subst in
286 let term = NCicSubstitution.subst_meta lc term in
287 unify test_eq_only metasenv subst context term t
288 with NCicUtils.Subst_not_found _->
289 instantiate test_eq_only metasenv subst context n lc t false)
291 | t, C.Meta (n,lc) ->
293 let _,_,term,_ = NCicUtils.lookup_subst n subst in
294 let term = NCicSubstitution.subst_meta lc term in
295 unify test_eq_only metasenv subst context t term
296 with NCicUtils.Subst_not_found _->
297 instantiate test_eq_only metasenv subst context n lc t true)
299 | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
300 let _,_,term,_ = NCicUtils.lookup_subst i subst in
301 let term = NCicSubstitution.subst_meta l term in
302 unify test_eq_only metasenv subst context (mk_appl term args) t2
304 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
305 let _,_,term,_ = NCicUtils.lookup_subst i subst in
306 let term = NCicSubstitution.subst_meta l term in
307 unify test_eq_only metasenv subst context t1 (mk_appl term args)
309 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
310 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
313 (fun (metasenv, subst) t1 t2 ->
314 unify test_eq_only metasenv subst context t1 t2)
315 (metasenv,subst) l1 l2
316 with Invalid_argument _ ->
317 raise (fail_exc metasenv subst context t1 t2))
319 | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
320 (* we verify that none of the args is a Meta,
321 since beta expanding w.r.t a metavariable makes no sense *)
322 let metasenv, subst, beta_expanded =
325 metasenv subst context t2 args
327 unify test_eq_only metasenv subst context
328 (C.Meta (i,l)) beta_expanded
330 | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
331 let metasenv, subst, beta_expanded =
334 metasenv subst context t1 args
336 unify test_eq_only metasenv subst context
337 beta_expanded (C.Meta (i,l))
339 (* processing this case here we avoid a useless small delta step *)
340 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
342 let relevance = NCicEnvironment.get_relevance r1 in
343 let relevance = match r1 with
344 | Ref.Ref (_,Ref.Con (_,_,lno)) ->
345 let _,relevance = HExtlib.split_nth lno relevance in
346 HExtlib.mk_list false lno @ relevance
349 let metasenv, subst, _ =
352 (fun (metasenv, subst, relevance) t1 t2 ->
354 match relevance with b::tl -> b,tl | _ -> true, [] in
355 let metasenv, subst =
356 try unify test_eq_only metasenv subst context t1 t2
357 with UnificationFailure _ | Uncertain _ when not b ->
360 metasenv, subst, relevance)
361 (metasenv, subst, relevance) tl1 tl2
362 with Invalid_argument _ ->
363 raise (uncert_exc metasenv subst context t1 t2)
367 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
368 C.Match (ref2,outtype2,term2,pl2)) ->
369 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
370 let _,_,ty,_ = List.nth itl tyno in
371 let rec remove_prods ~subst context ty =
372 let ty = NCicReduction.whd ~subst context ty in
375 | C.Prod (name,so,ta) ->
376 remove_prods ~subst ((name,(C.Decl so))::context) ta
380 match remove_prods ~subst [] ty with
381 | C.Sort C.Prop -> true
384 let rec remove_prods ~subst context ty =
385 let ty = NCicReduction.whd ~subst context ty in
388 | C.Prod (name,so,ta) ->
389 remove_prods ~subst ((name,(C.Decl so))::context) ta
392 if not (Ref.eq ref1 ref2) then
393 raise (uncert_exc metasenv subst context t1 t2)
395 let metasenv, subst =
396 unify test_eq_only metasenv subst context outtype1 outtype2 in
397 let metasenv, subst =
398 try unify test_eq_only metasenv subst context term1 term2
399 with UnificationFailure _ | Uncertain _ when is_prop ->
404 (fun (metasenv,subst) ->
405 unify test_eq_only metasenv subst context)
406 (metasenv, subst) pl1 pl2
407 with Invalid_argument _ ->
408 raise (uncert_exc metasenv subst context t1 t2))
409 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
410 | _ -> raise (uncert_exc metasenv subst context t1 t2)
411 (*D*) in outside(); rc with exn -> outside (); raise exn
413 let height_of = function
414 | NCic.Const (Ref.Ref (_,Ref.Def h))
415 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
416 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
417 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
420 let put_in_whd m1 m2 =
421 NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
422 NCicReduction.reduce_machine ~delta:max_int ~subst context m2
425 ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
427 assert (not (norm1 && norm2));
429 x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
431 NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
433 let h1 = height_of t1 in
434 let h2 = height_of t2 in
435 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
436 NCicReduction.reduce_machine ~delta ~subst context m1,
437 NCicReduction.reduce_machine ~delta ~subst context m2
439 let rec unif_machines metasenv subst =
441 | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
442 (*D*) inside 'M'; try let rc =
444 pp (lazy((if are_normal then "*" else " ") ^ " " ^
445 NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
447 NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2)));
449 let relevance = [] (* TO BE UNDERSTOOD
451 | C.Const r -> NCicEnvironment.get_relevance r
453 let unif_from_stack t1 t2 b metasenv subst =
455 let t1 = NCicReduction.from_stack t1 in
456 let t2 = NCicReduction.from_stack t2 in
457 unif_machines metasenv subst (put_in_whd t1 t2)
458 with UnificationFailure _ | Uncertain _ when not b ->
461 let rec check_stack l1 l2 r (metasenv, subst) =
463 | x1::tl1, x2::tl2, r::tr ->
464 check_stack tl1 tl2 tr
465 (unif_from_stack x1 x2 r metasenv subst)
466 | x1::tl1, x2::tl2, [] ->
467 check_stack tl1 tl2 []
468 (unif_from_stack x1 x2 true metasenv subst)
470 fo_unif test_eq_only metasenv subst
471 (NCicReduction.unwind (k1,e1,t1,List.rev l1))
472 (NCicReduction.unwind (k2,e2,t2,List.rev l2))
474 try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
475 with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
476 unif_machines metasenv subst (small_delta_step m1 m2)
477 (*D*) in outside(); rc with exn -> outside (); raise exn
479 try fo_unif test_eq_only metasenv subst t1 t2
480 with UnificationFailure msg | Uncertain msg as exn ->
482 unif_machines metasenv subst
483 (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
485 | UnificationFailure _ -> raise (UnificationFailure msg)
486 | Uncertain _ -> raise exn
487 (*D*) in outside(); rc with exn -> outside (); raise exn
500 exception UnificationFailure of string Lazy.t;;
501 exception Uncertain of string Lazy.t;;
502 exception AssertFailure of string Lazy.t;;
504 let verbose = false;;
505 let debug_print = fun _ -> ()
507 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
508 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
509 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
510 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
512 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
514 let type_of_aux' metasenv subst context term ugraph =
517 profile.HExtlib.profile
518 (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
520 CicTypeChecker.TypeCheckerFailure msg ->
524 "Kernel Type checking error:
525 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
526 (CicMetaSubst.ppterm ~metasenv subst term)
527 (CicMetaSubst.ppterm ~metasenv [] term)
528 (CicMetaSubst.ppcontext ~metasenv subst context)
529 (CicMetaSubst.ppmetasenv subst metasenv)
530 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
531 raise (AssertFailure msg)
532 | CicTypeChecker.AssertFailure msg ->
535 "Kernel Type checking assertion failure:
536 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
537 (CicMetaSubst.ppterm ~metasenv subst term)
538 (CicMetaSubst.ppterm ~metasenv [] term)
539 (CicMetaSubst.ppcontext ~metasenv subst context)
540 (CicMetaSubst.ppmetasenv subst metasenv)
541 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
542 raise (AssertFailure msg)
543 in profiler_toa.HExtlib.profile foo ()
546 let exists_a_meta l =
550 | Cic.Appl (Cic.Meta _::_) -> true
553 let rec deref subst t =
554 let snd (_,a,_) = a in
559 (CicSubstitution.subst_meta
560 l (snd (CicUtil.lookup_subst n subst)))
562 CicUtil.Subst_not_found _ -> t)
563 | Cic.Appl(Cic.Meta(n,l)::args) ->
564 (match deref subst (Cic.Meta(n,l)) with
565 | Cic.Lambda _ as t ->
566 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
567 | r -> Cic.Appl(r::args))
568 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
569 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
574 let foo () = deref subst t
575 in profiler_deref.HExtlib.profile foo ()
577 exception WrongShape;;
578 let eta_reduce after_beta_expansion after_beta_expansion_body
579 before_beta_expansion
582 match before_beta_expansion,after_beta_expansion_body with
583 Cic.Appl l, Cic.Appl l' ->
584 let rec all_but_last check_last =
588 | [_] -> if check_last then raise WrongShape else []
589 | he::tl -> he::(all_but_last check_last tl)
591 let all_but_last check_last l =
592 match all_but_last check_last l with
597 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
598 let all_but_last = all_but_last false l in
599 (* here we should test alpha-equivalence; however we know by
600 construction that here alpha_equivalence is equivalent to = *)
601 if t = all_but_last then
605 | _,_ -> after_beta_expansion
607 WrongShape -> after_beta_expansion
609 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
610 let module S = CicSubstitution in
611 let module C = Cic in
613 let rec aux metasenv subst n context t' ugraph =
616 let subst,metasenv,ugraph1 =
617 fo_unif_subst test_equality_only subst context metasenv
618 (CicSubstitution.lift n arg) t' ugraph
621 subst,metasenv,C.Rel (1 + n),ugraph1
624 | UnificationFailure _ ->
626 | C.Rel m -> subst,metasenv,
627 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
628 | C.Var (uri,exp_named_subst) ->
629 let subst,metasenv,exp_named_subst',ugraph1 =
630 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
632 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
634 (* andrea: in general, beta_expand can create badly typed
635 terms. This happens quite seldom in practice, UNLESS we
636 iterate on the local context. For this reason, we renounce
637 to iterate and just lift *)
641 Some t -> Some (CicSubstitution.lift 1 t)
643 subst, metasenv, C.Meta (i,l), ugraph
645 | C.Implicit _ as t -> subst,metasenv,t,ugraph
647 let subst,metasenv,te',ugraph1 =
648 aux metasenv subst n context te ugraph in
649 let subst,metasenv,ty',ugraph2 =
650 aux metasenv subst n context ty ugraph1 in
651 (* TASSI: sure this is in serial? *)
652 subst,metasenv,(C.Cast (te', ty')),ugraph2
654 let subst,metasenv,s',ugraph1 =
655 aux metasenv subst n context s ugraph in
656 let subst,metasenv,t',ugraph2 =
657 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
660 (* TASSI: sure this is in serial? *)
661 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
662 | C.Lambda (nn,s,t) ->
663 let subst,metasenv,s',ugraph1 =
664 aux metasenv subst n context s ugraph in
665 let subst,metasenv,t',ugraph2 =
666 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
668 (* TASSI: sure this is in serial? *)
669 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
670 | C.LetIn (nn,s,ty,t) ->
671 let subst,metasenv,s',ugraph1 =
672 aux metasenv subst n context s ugraph in
673 let subst,metasenv,ty',ugraph1 =
674 aux metasenv subst n context ty ugraph in
675 let subst,metasenv,t',ugraph2 =
676 aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
679 (* TASSI: sure this is in serial? *)
680 subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
682 let subst,metasenv,revl',ugraph1 =
684 (fun (subst,metasenv,appl,ugraph) t ->
685 let subst,metasenv,t',ugraph1 =
686 aux metasenv subst n context t ugraph in
687 subst,metasenv,(t'::appl),ugraph1
688 ) (subst,metasenv,[],ugraph) l
690 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
691 | C.Const (uri,exp_named_subst) ->
692 let subst,metasenv,exp_named_subst',ugraph1 =
693 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
695 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
696 | C.MutInd (uri,i,exp_named_subst) ->
697 let subst,metasenv,exp_named_subst',ugraph1 =
698 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
700 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
701 | C.MutConstruct (uri,i,j,exp_named_subst) ->
702 let subst,metasenv,exp_named_subst',ugraph1 =
703 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
705 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
706 | C.MutCase (sp,i,outt,t,pl) ->
707 let subst,metasenv,outt',ugraph1 =
708 aux metasenv subst n context outt ugraph in
709 let subst,metasenv,t',ugraph2 =
710 aux metasenv subst n context t ugraph1 in
711 let subst,metasenv,revpl',ugraph3 =
713 (fun (subst,metasenv,pl,ugraph) t ->
714 let subst,metasenv,t',ugraph1 =
715 aux metasenv subst n context t ugraph in
716 subst,metasenv,(t'::pl),ugraph1
717 ) (subst,metasenv,[],ugraph2) pl
719 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
720 (* TASSI: not sure this is serial *)
722 (*CSC: not implemented
723 let tylen = List.length fl in
726 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
729 C.Fix (i, substitutedfl)
731 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
733 (*CSC: not implemented
734 let tylen = List.length fl in
737 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
740 C.CoFix (i, substitutedfl)
743 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
745 and aux_exp_named_subst metasenv subst n context ens ugraph =
747 (fun (uri,t) (subst,metasenv,l,ugraph) ->
748 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
749 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
751 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
753 FreshNamesGenerator.mk_fresh_name ~subst
754 metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
756 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
757 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
758 subst, metasenv, t'', ugraph2
759 in profiler_beta_expand.HExtlib.profile foo ()
762 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
763 let _,subst,metasenv,hd,ugraph =
765 (fun arg (num,subst,metasenv,t,ugraph) ->
766 let subst,metasenv,t,ugraph1 =
767 beta_expand num test_equality_only
768 metasenv subst context t arg ugraph
770 num+1,subst,metasenv,t,ugraph1
771 ) args (1,subst,metasenv,t,ugraph)
773 subst,metasenv,hd,ugraph
775 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
778 | (m2,_,c2,c2')::_ ->
779 let m1,c1,c1' = carr,to1,to2 in
781 function Some (_,t) -> CicPp.ppterm t
785 ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
786 CoercDb.string_of_carr car2^": " ^
787 CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
788 unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
789 unopt c2^" + "^unopt c2')
791 (* NUOVA UNIFICAZIONE *)
792 (* A substitution is a (int * Cic.term) list that associates a
793 metavariable i with its body.
794 A metaenv is a (int * Cic.term) list that associate a metavariable
796 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
797 a new substitution which is _NOT_ unwinded. It must be unwinded before
800 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
801 let module C = Cic in
802 let module R = CicReduction in
803 let module S = CicSubstitution in
804 let t1 = deref subst t1 in
805 let t2 = deref subst t2 in
806 let (&&&) a b = (a && b) || ((not a) && (not b)) in
807 (* let bef = Sys.time () in *)
809 if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
813 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
814 in profiler_are_convertible.HExtlib.profile foo ()
816 (* let aft = Sys.time () in
817 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
818 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
819 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
821 subst, metasenv, ugraph
824 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
825 let _,subst,metasenv,ugraph1 =
828 (fun (j,subst,metasenv,ugraph) t1 t2 ->
831 | _,None -> j+1,subst,metasenv,ugraph
832 | Some t1', Some t2' ->
833 (* First possibility: restriction *)
834 (* Second possibility: unification *)
835 (* Third possibility: convertibility *)
838 ~subst ~metasenv context t1' t2' ugraph
841 j+1,subst,metasenv, ugraph1
844 let subst,metasenv,ugraph2 =
847 subst context metasenv t1' t2' ugraph
849 j+1,subst,metasenv,ugraph2
852 | UnificationFailure _ ->
853 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
854 let metasenv, subst =
855 CicMetaSubst.restrict
856 subst [(n,j)] metasenv in
857 j+1,subst,metasenv,ugraph1)
858 ) (1,subst,metasenv,ugraph) ln lm
862 (UnificationFailure (lazy "1"))
865 "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."
866 (CicMetaSubst.ppterm ~metasenv subst t1)
867 (CicMetaSubst.ppterm ~metasenv subst t2))) *)
868 | Invalid_argument _ ->
870 (UnificationFailure (lazy "2")))
873 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
874 (CicMetaSubst.ppterm ~metasenv subst t1)
875 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
876 in subst,metasenv,ugraph1
877 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
878 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
880 | (t, C.Meta (n,l)) ->
883 C.Meta (n,_), C.Meta (m,_) when n < m -> false
884 | _, C.Meta _ -> false
887 let lower = fun x y -> if swap then y else x in
888 let upper = fun x y -> if swap then x else y in
889 let fo_unif_subst_ordered
890 test_equality_only subst context metasenv m1 m2 ugraph =
891 fo_unif_subst test_equality_only subst context metasenv
892 (lower m1 m2) (upper m1 m2) ugraph
895 let subst,metasenv,ugraph1 =
896 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
899 type_of_aux' metasenv subst context t ugraph
903 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
905 UnificationFailure _ as e -> raise e
906 | Uncertain msg -> raise (UnificationFailure msg)
908 debug_print (lazy "siamo allo huge hack");
909 (* TODO huge hack!!!!
910 * we keep on unifying/refining in the hope that
911 * the problem will be eventually solved.
912 * In the meantime we're breaking a big invariant:
913 * the terms that we are unifying are no longer well
914 * typed in the current context (in the worst case
915 * we could even diverge) *)
916 (subst, metasenv,ugraph)) in
917 let t',metasenv,subst =
919 CicMetaSubst.delift n subst context metasenv l t
921 (CicMetaSubst.MetaSubstFailure msg)->
922 raise (UnificationFailure msg)
923 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
927 C.Sort (C.Type u) when not test_equality_only ->
928 let u' = CicUniv.fresh () in
929 let s = C.Sort (C.Type u') in
932 CicUniv.add_ge (upper u u') (lower u u') ugraph1
936 CicUniv.UniverseInconsistency msg ->
937 raise (UnificationFailure msg))
940 (* Unifying the types may have already instantiated n. Let's check *)
942 let (_, oldt,_) = CicUtil.lookup_subst n subst in
943 let lifted_oldt = S.subst_meta l oldt in
944 fo_unif_subst_ordered
945 test_equality_only subst context metasenv t lifted_oldt ugraph2
947 CicUtil.Subst_not_found _ ->
948 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
949 let subst = (n, (context, t'',ty)) :: subst in
951 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
952 subst, metasenv, ugraph2
954 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
955 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
956 if UriManager.eq uri1 uri2 then
957 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
958 exp_named_subst1 exp_named_subst2 ugraph
960 raise (UnificationFailure (lazy
962 "Can't unify %s with %s due to different constants"
963 (CicMetaSubst.ppterm ~metasenv subst t1)
964 (CicMetaSubst.ppterm ~metasenv subst t2))))
965 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
966 if UriManager.eq uri1 uri2 && i1 = i2 then
967 fo_unif_subst_exp_named_subst
969 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
971 raise (UnificationFailure
974 "Can't unify %s with %s due to different inductive principles"
975 (CicMetaSubst.ppterm ~metasenv subst t1)
976 (CicMetaSubst.ppterm ~metasenv subst t2))))
977 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
978 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
979 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
980 fo_unif_subst_exp_named_subst
982 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
984 raise (UnificationFailure
987 "Can't unify %s with %s due to different inductive constructors"
988 (CicMetaSubst.ppterm ~metasenv subst t1)
989 (CicMetaSubst.ppterm ~metasenv subst t2))))
990 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
991 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
992 subst context metasenv te t2 ugraph
993 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
994 subst context metasenv t1 te ugraph
995 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
996 let subst',metasenv',ugraph1 =
997 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
999 fo_unif_subst test_equality_only
1000 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1001 | (C.LetIn (_,s1,ty1,t1), t2)
1002 | (t2, C.LetIn (_,s1,ty1,t1)) ->
1004 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
1005 | (C.Appl l1, C.Appl l2) ->
1006 (* andrea: this case should be probably rewritten in the
1009 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
1012 (fun (subst,metasenv,ugraph) t1 t2 ->
1014 test_equality_only subst context metasenv t1 t2 ugraph)
1015 (subst,metasenv,ugraph) l1 l2
1016 with (Invalid_argument msg) ->
1017 raise (UnificationFailure (lazy msg)))
1018 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
1019 (* we verify that none of the args is a Meta,
1020 since beta expanding with respoect to a metavariable
1024 let (_,t,_) = CicUtil.lookup_subst i subst in
1025 let lifted = S.subst_meta l t in
1026 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
1029 subst context metasenv reduced t2 ugraph
1030 with CicUtil.Subst_not_found _ -> *)
1031 let subst,metasenv,beta_expanded,ugraph1 =
1033 test_equality_only metasenv subst context t2 args ugraph
1035 fo_unif_subst test_equality_only subst context metasenv
1036 (C.Meta (i,l)) beta_expanded ugraph1
1037 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
1039 let (_,t,_) = CicUtil.lookup_subst i subst in
1040 let lifted = S.subst_meta l t in
1041 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
1044 subst context metasenv t1 reduced ugraph
1045 with CicUtil.Subst_not_found _ -> *)
1046 let subst,metasenv,beta_expanded,ugraph1 =
1049 metasenv subst context t1 args ugraph
1051 fo_unif_subst test_equality_only subst context metasenv
1052 (C.Meta (i,l)) beta_expanded ugraph1
1054 let lr1 = List.rev l1 in
1055 let lr2 = List.rev l2 in
1057 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
1060 | _,[] -> assert false
1063 test_equality_only subst context metasenv h1 h2 ugraph
1066 fo_unif_subst test_equality_only subst context metasenv
1067 h (C.Appl (List.rev l)) ugraph
1068 | ((h1::l1),(h2::l2)) ->
1069 let subst', metasenv',ugraph1 =
1072 subst context metasenv h1 h2 ugraph
1075 test_equality_only subst' metasenv' (l1,l2) ugraph1
1079 test_equality_only subst metasenv (lr1, lr2) ugraph
1081 | UnificationFailure s
1082 | Uncertain s as exn ->
1085 | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
1086 (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
1087 CoercDb.is_a_coercion cc1 <> None &&
1088 CoercDb.is_a_coercion cc2 <> None &&
1089 not (UriManager.eq uri1 uri2) ->
1091 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1093 let inner_coerced t =
1094 let t = CicMetaSubst.apply_subst subst t in
1098 (match CoercGraph.coerced_arg l with
1100 | Some (t,_) -> aux (List.hd l) t t)
1103 aux (Cic.Implicit None) (Cic.Implicit None) t
1105 let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
1106 let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
1109 CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
1111 | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
1114 let head1_c, head2_c =
1116 CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
1118 | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
1121 let unfold uri ens args =
1123 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
1127 | Cic.Constant (_,Some bo,_,_,_) ->
1128 CicReduction.head_beta_reduce ~delta:false
1129 (Cic.Appl (bo::args))
1132 let conclude subst metasenv ugraph last_tl1' last_tl2' =
1133 let subst',metasenv,ugraph =
1136 ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
1137 " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
1139 fo_unif_subst test_equality_only subst context
1140 metasenv last_tl1' last_tl2' ugraph
1142 if subst = subst' then raise exn
1145 let subst,metasenv,ugrph as res =
1147 fo_unif_subst test_equality_only subst' context
1148 metasenv (C.Appl l1) (C.Appl l2) ugraph
1152 (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
1153 " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1157 if CoercDb.eq_carr car1 car2 then
1158 match last_tl1,last_tl2 with
1159 | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
1162 let subst,metasenv,ugraph =
1163 fo_unif_subst test_equality_only subst context
1164 metasenv last_tl1 last_tl2 ugraph
1166 fo_unif_subst test_equality_only subst context
1167 metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
1168 | _ when CoercDb.eq_carr head1_c head2_c ->
1169 (* composite VS composition + metas avoiding
1170 * coercions not only in coerced position *)
1171 if c1 <> cc1 && c2 <> cc2 then
1172 conclude subst metasenv ugraph
1177 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
1179 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
1181 fo_unif_subst test_equality_only subst context
1182 metasenv l1 l2 ugraph
1186 match last_tl1 with Cic.Meta _ -> true | _ -> false in
1188 match last_tl2 with Cic.Meta _ -> true | _ -> false in
1189 if not (grow1 || grow2) then
1190 (* no flexible terminals -> no pullback, but
1191 * we still unify them, in some cases it helps *)
1192 conclude subst metasenv ugraph last_tl1 last_tl2
1196 metasenv subst context (grow1,car1) (grow2,car2)
1200 | (carr,metasenv,to1,to2)::xxx ->
1201 warn_if_not_unique xxx to1 to2 carr car1 car2;
1202 let last_tl1',(subst,metasenv,ugraph) =
1203 match grow1,to1 with
1204 | true,Some (last,coerced) ->
1206 fo_unif_subst test_equality_only subst context
1207 metasenv coerced last_tl1 ugraph
1208 | _ -> last_tl1,(subst,metasenv,ugraph)
1210 let last_tl2',(subst,metasenv,ugraph) =
1211 match grow2,to2 with
1212 | true,Some (last,coerced) ->
1214 fo_unif_subst test_equality_only subst context
1215 metasenv coerced last_tl2 ugraph
1216 | _ -> last_tl2,(subst,metasenv,ugraph)
1218 conclude subst metasenv ugraph last_tl1' last_tl2')
1220 (* {{{ CSC: This is necessary because of the "elim H" tactic
1221 where the type of H is only reducible to an
1222 inductive type. This could be extended from inductive
1223 types to any rigid term. However, the code is
1224 duplicated in two places: inside applications and
1225 outside them. Probably it would be better to
1226 work with lambda-bar terms instead. *)
1227 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
1228 | (_, Cic.MutInd _::_) ->
1229 let t1' = R.whd ~subst context t1 in
1231 C.Appl (C.MutInd _::_) ->
1232 fo_unif_subst test_equality_only
1233 subst context metasenv t1' t2 ugraph
1234 | _ -> raise (UnificationFailure (lazy "88")))
1235 | (Cic.MutInd _::_,_) ->
1236 let t2' = R.whd ~subst context t2 in
1238 C.Appl (C.MutInd _::_) ->
1239 fo_unif_subst test_equality_only
1240 subst context metasenv t1 t2' ugraph
1243 (lazy ("not a mutind :"^
1244 CicMetaSubst.ppterm ~metasenv subst t2 ))))
1247 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
1248 let subst', metasenv',ugraph1 =
1249 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
1251 let subst'',metasenv'',ugraph2 =
1252 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
1256 (fun (subst,metasenv,ugraph) t1 t2 ->
1258 test_equality_only subst context metasenv t1 t2 ugraph
1259 ) (subst'',metasenv'',ugraph2) pl1 pl2
1261 Invalid_argument _ ->
1262 raise (UnificationFailure (lazy "6.1")))
1264 "Error trying to unify %s with %s: the number of branches is not the same."
1265 (CicMetaSubst.ppterm ~metasenv subst t1)
1266 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
1267 | (C.Rel _, _) | (_, C.Rel _) ->
1269 subst, metasenv,ugraph
1271 raise (UnificationFailure (lazy
1273 "Can't unify %s with %s because they are not convertible"
1274 (CicMetaSubst.ppterm ~metasenv subst t1)
1275 (CicMetaSubst.ppterm ~metasenv subst t2))))
1276 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
1277 let subst,metasenv,beta_expanded,ugraph1 =
1279 test_equality_only metasenv subst context t2 args ugraph
1281 fo_unif_subst test_equality_only subst context metasenv
1282 (C.Meta (i,l)) beta_expanded ugraph1
1283 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
1284 let subst,metasenv,beta_expanded,ugraph1 =
1286 test_equality_only metasenv subst context t1 args ugraph
1288 fo_unif_subst test_equality_only subst context metasenv
1289 beta_expanded (C.Meta (i,l)) ugraph1
1290 (* Works iff there are no arguments applied to it; similar to the
1292 | (_, C.MutInd _) ->
1293 let t1' = R.whd ~subst context t1 in
1296 fo_unif_subst test_equality_only
1297 subst context metasenv t1' t2 ugraph
1298 | _ -> raise (UnificationFailure (lazy "8")))
1300 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
1301 let subst',metasenv',ugraph1 =
1302 fo_unif_subst true subst context metasenv s1 s2 ugraph
1304 fo_unif_subst test_equality_only
1305 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1307 (match CicReduction.whd ~subst context t2 with
1309 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1310 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
1312 (match CicReduction.whd ~subst context t1 with
1314 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1315 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
1317 (* delta-beta reduction should almost never be a problem for
1319 1. long computations require iota reduction
1320 2. it is extremely rare that a close term t1 (that could be unified
1321 to t2) beta-delta reduces to t1' while t2 does not beta-delta
1322 reduces in the same way. This happens only if one meta of t2
1323 occurs in head position during beta reduction. In this unluky
1324 case too much reduction will be performed on t1 and unification
1325 will surely fail. *)
1326 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
1327 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
1328 if t1 = t1' && t2 = t2' then
1329 raise (UnificationFailure
1332 "Can't unify %s with %s because they are not convertible"
1333 (CicMetaSubst.ppterm ~metasenv subst t1)
1334 (CicMetaSubst.ppterm ~metasenv subst t2))))
1337 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
1339 UnificationFailure _
1341 raise (UnificationFailure
1344 "Can't unify %s with %s because they are not convertible"
1345 (CicMetaSubst.ppterm ~metasenv subst t1)
1346 (CicMetaSubst.ppterm ~metasenv subst t2))))
1348 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
1349 exp_named_subst1 exp_named_subst2 ugraph
1353 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
1354 assert (uri1=uri2) ;
1355 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1356 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
1358 Invalid_argument _ ->
1363 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
1366 raise (UnificationFailure (lazy (sprintf
1367 "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))))
1369 (* A substitution is a (int * Cic.term) list that associates a *)
1370 (* metavariable i with its body. *)
1371 (* metasenv is of type Cic.metasenv *)
1372 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
1373 (* a new substitution which is already unwinded and ready to be applied and *)
1374 (* a new metasenv in which some hypothesis in the contexts of the *)
1375 (* metavariables may have been restricted. *)
1376 let fo_unif metasenv context t1 t2 ugraph =
1377 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
1379 let enrich_msg msg subst context metasenv t1 t2 ugraph =
1382 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"
1383 (CicMetaSubst.ppterm ~metasenv subst t1)
1385 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1388 | UnificationFailure s
1390 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1391 (CicMetaSubst.ppterm ~metasenv subst t2)
1393 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1396 | UnificationFailure s
1398 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1399 (CicMetaSubst.ppcontext ~metasenv subst context)
1400 (CicMetaSubst.ppmetasenv subst metasenv)
1401 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
1403 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
1404 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
1406 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1407 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
1409 | UnificationFailure s
1411 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1412 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
1414 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1415 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
1417 | UnificationFailure s
1419 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1420 (CicMetaSubst.ppcontext ~metasenv subst context)
1421 (CicMetaSubst.ppmetasenv subst metasenv)
1425 let fo_unif_subst subst context metasenv t1 t2 ugraph =
1427 fo_unif_subst false subst context metasenv t1 t2 ugraph
1429 | AssertFailure msg ->
1430 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1431 | UnificationFailure msg ->
1432 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))