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);;
76 prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
81 let fix_sorts metasenv subst context meta t =
82 let rec aux () = function
83 | NCic.Sort (NCic.Type u) as orig ->
84 (match NCicEnvironment.sup u with
85 | None -> raise (fail_exc metasenv subst context meta t)
86 | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1))
87 | NCic.Meta _ as orig -> orig
88 | t -> NCicUtils.map (fun _ _ -> ()) () aux t
93 let rec beta_expand num test_eq_only swap metasenv subst context t arg =
94 let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
98 unify test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
100 unify test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
102 (metasenv, subst), NCic.Rel (1 + n)
103 with Uncertain _ | UnificationFailure _ ->
105 | NCic.Rel m as orig ->
106 (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
107 (* andrea: in general, beta_expand can create badly typed
108 terms. This happens quite seldom in practice, UNLESS we
109 iterate on the local context. For this reason, we renounce
110 to iterate and just lift *)
111 | NCic.Meta (i,(shift,lc)) ->
112 (metasenv,subst), NCic.Meta (i,(shift+1,lc))
113 | NCic.Prod (name, src, tgt) as orig ->
114 let (metasenv, subst), src1 = aux (n,context,true) acc src in
115 let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
116 let ms, tgt1 = aux k (metasenv, subst) tgt in
117 if src == src1 && tgt == tgt1 then ms, orig else
118 ms, NCic.Prod (name, src1, tgt1)
120 NCicUntrusted.map_term_fold_a
121 (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t
124 let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
125 let fresh_name = "Hbeta" ^ string_of_int num in
126 let (metasenv,subst), t1 =
127 aux (0, context, test_eq_only) (metasenv, subst) t in
128 let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in
130 ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
132 with NCicTypeChecker.TypeCheckerFailure _ ->
133 metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
135 and beta_expand_many test_equality_only swap metasenv subst context t args =
136 (* (*D*) inside 'B'; try let rc = *)
137 pp (lazy (String.concat ", "
138 (List.map (NCicPp.ppterm ~metasenv ~subst ~context)
139 args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
140 let _, subst, metasenv, hd =
142 (fun arg (num,subst,metasenv,t) ->
143 let metasenv, subst, t =
144 beta_expand num test_equality_only swap metasenv subst context t arg
146 num+1,subst,metasenv,t)
147 args (1,subst,metasenv,t)
149 pp (lazy ("Head syntesized by b-exp: " ^
150 NCicPp.ppterm ~metasenv ~subst ~context hd));
152 (* (*D*) in outside (); rc with exn -> outside (); raise exn *)
154 and instantiate test_eq_only metasenv subst context n lc t swap =
155 (*D*) inside 'I'; try let rc =
156 let unify test_eq_only m s c t1 t2 =
157 if swap then unify test_eq_only m s c t2 t1
158 else unify test_eq_only m s c t1 t2
161 if swap then fix_sorts metasenv subst context (NCic.Meta (n,lc)) t
163 NCic.Sort (NCic.Type (
164 match NCicEnvironment.sup NCicEnvironment.type0 with Some x ->x| _ ->
167 let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
168 let metasenv, subst, t =
170 | NCic.Implicit (`Typeof _) -> metasenv, subst, fix_sorts t
172 pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
174 try t, NCicTypeChecker.typeof ~subst ~metasenv context t
175 with NCicTypeChecker.TypeCheckerFailure _ ->
176 let ft = fix_sorts t in
177 if ft == t then assert false else
179 pp (lazy ("typeof: " ^
180 NCicPp.ppterm ~metasenv ~subst ~context ft));
181 ft, NCicTypeChecker.typeof ~subst ~metasenv context ft
182 with NCicTypeChecker.TypeCheckerFailure msg ->
183 prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context ft);
184 prerr_endline (Lazy.force msg);
187 let lty = NCicSubstitution.subst_meta lc ty in
188 pp (lazy("On the types: " ^
189 NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
190 ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
191 let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
194 let (metasenv, subst), t =
195 try NCicMetaSubst.delift metasenv subst context n lc t
196 with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg)
197 | NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg)
199 (* Unifying the types may have already instantiated n. *)
201 let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
202 let oldt = NCicSubstitution.subst_meta lc oldt in
203 let t = NCicSubstitution.subst_meta lc t in
204 (* conjecture: always fail --> occur check *)
205 unify test_eq_only metasenv subst context oldt t
206 with NCicUtils.Subst_not_found _ ->
207 (* by cumulativity when unify(?,Type_i)
208 * we could ? := Type_j with j <= i... *)
209 let subst = (n, (name, ctx, t, ty)) :: subst in
210 pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
211 ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
213 List.filter (fun (m,_) -> not (n = m)) metasenv
216 (*D*) in outside(); rc with exn -> outside (); raise exn
218 and unify test_eq_only metasenv subst context t1 t2 =
219 (*D*) inside 'U'; try let rc =
220 let fo_unif test_eq_only metasenv subst t1 t2 =
221 (*D*) inside 'F'; try let rc =
222 pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^
223 NCicPp.ppterm ~metasenv ~subst ~context t2));
228 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
229 if NCicEnvironment.universe_leq a b then metasenv, subst
230 else raise (fail_exc metasenv subst context t1 t2)
231 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
232 if NCicEnvironment.universe_eq a b then metasenv, subst
233 else raise (fail_exc metasenv subst context t1 t2)
234 | (C.Sort C.Prop,C.Sort (C.Type _)) ->
235 if (not test_eq_only) then metasenv, subst
236 else raise (fail_exc metasenv subst context t1 t2)
238 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
239 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
240 let metasenv, subst = unify true metasenv subst context s1 s2 in
241 unify test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
242 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
243 let metasenv,subst=unify test_eq_only metasenv subst context ty1 ty2 in
244 let metasenv,subst=unify test_eq_only metasenv subst context s1 s2 in
245 let context = (name1, C.Def (s1,ty1))::context in
246 unify test_eq_only metasenv subst context t1 t2
248 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
250 let l1 = NCicUtils.expand_local_context l1 in
251 let l2 = NCicUtils.expand_local_context l2 in
252 let metasenv, subst, to_restrict, _ =
254 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
256 let metasenv, subst =
257 unify test_eq_only metasenv subst context
258 (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
260 metasenv, subst, to_restrict, i-1
261 with UnificationFailure _ | Uncertain _ ->
262 metasenv, subst, i::to_restrict, i-1)
263 l1 l2 (metasenv, subst, [], List.length l1)
265 let metasenv, subst, _ =
266 NCicMetaSubst.restrict metasenv subst n1 to_restrict
270 | Invalid_argument _ -> assert false
271 | NCicMetaSubst.MetaSubstFailure msg ->
273 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
274 let term1 = NCicSubstitution.subst_meta lc1 term in
275 let term2 = NCicSubstitution.subst_meta lc2 term in
276 unify test_eq_only metasenv subst context term1 term2
277 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
279 | C.Meta (n,lc), t ->
281 let _,_,term,_ = NCicUtils.lookup_subst n subst in
282 let term = NCicSubstitution.subst_meta lc term in
283 unify test_eq_only metasenv subst context term t
284 with NCicUtils.Subst_not_found _->
285 instantiate test_eq_only metasenv subst context n lc t false)
287 | t, C.Meta (n,lc) ->
289 let _,_,term,_ = NCicUtils.lookup_subst n subst in
290 let term = NCicSubstitution.subst_meta lc term in
291 unify test_eq_only metasenv subst context t term
292 with NCicUtils.Subst_not_found _->
293 instantiate test_eq_only metasenv subst context n lc t true)
295 | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
296 let _,_,term,_ = NCicUtils.lookup_subst i subst in
297 let term = NCicSubstitution.subst_meta l term in
298 unify test_eq_only metasenv subst context (mk_appl term args) t2
300 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
301 let _,_,term,_ = NCicUtils.lookup_subst i subst in
302 let term = NCicSubstitution.subst_meta l term in
303 unify test_eq_only metasenv subst context t1 (mk_appl term args)
305 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
306 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
309 (fun (metasenv, subst) t1 t2 ->
310 unify test_eq_only metasenv subst context t1 t2)
311 (metasenv,subst) l1 l2
312 with Invalid_argument _ ->
313 raise (fail_exc metasenv subst context t1 t2))
315 | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
316 (* we verify that none of the args is a Meta,
317 since beta expanding w.r.t a metavariable makes no sense *)
318 let metasenv, subst, beta_expanded =
321 metasenv subst context t2 args
323 unify test_eq_only metasenv subst context
324 (C.Meta (i,l)) beta_expanded
326 | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
327 let metasenv, subst, beta_expanded =
330 metasenv subst context t1 args
332 unify test_eq_only metasenv subst context
333 beta_expanded (C.Meta (i,l))
335 (* processing this case here we avoid a useless small delta step *)
336 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
338 let relevance = NCicEnvironment.get_relevance r1 in
339 let relevance = match r1 with
340 | Ref.Ref (_,Ref.Con (_,_,lno)) ->
341 let _,relevance = HExtlib.split_nth lno relevance in
342 HExtlib.mk_list false lno @ relevance
345 let metasenv, subst, _ =
348 (fun (metasenv, subst, relevance) t1 t2 ->
350 match relevance with b::tl -> b,tl | _ -> true, [] in
351 let metasenv, subst =
352 try unify test_eq_only metasenv subst context t1 t2
353 with UnificationFailure _ | Uncertain _ when not b ->
356 metasenv, subst, relevance)
357 (metasenv, subst, relevance) tl1 tl2
358 with Invalid_argument _ ->
359 raise (uncert_exc metasenv subst context t1 t2)
363 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
364 C.Match (ref2,outtype2,term2,pl2)) ->
365 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
366 let _,_,ty,_ = List.nth itl tyno in
367 let rec remove_prods ~subst context ty =
368 let ty = NCicReduction.whd ~subst context ty in
371 | C.Prod (name,so,ta) ->
372 remove_prods ~subst ((name,(C.Decl so))::context) ta
376 match remove_prods ~subst [] ty with
377 | C.Sort C.Prop -> true
380 let rec remove_prods ~subst context ty =
381 let ty = NCicReduction.whd ~subst context ty in
384 | C.Prod (name,so,ta) ->
385 remove_prods ~subst ((name,(C.Decl so))::context) ta
388 if not (Ref.eq ref1 ref2) then
389 raise (uncert_exc metasenv subst context t1 t2)
391 let metasenv, subst =
392 unify test_eq_only metasenv subst context outtype1 outtype2 in
393 let metasenv, subst =
394 try unify test_eq_only metasenv subst context term1 term2
395 with UnificationFailure _ | Uncertain _ when is_prop ->
400 (fun (metasenv,subst) ->
401 unify test_eq_only metasenv subst context)
402 (metasenv, subst) pl1 pl2
403 with Invalid_argument _ ->
404 raise (uncert_exc metasenv subst context t1 t2))
405 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
406 | _ -> raise (uncert_exc metasenv subst context t1 t2)
407 (*D*) in outside(); rc with exn -> outside (); raise exn
409 let height_of = function
410 | NCic.Const (Ref.Ref (_,Ref.Def h))
411 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
412 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
413 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
416 let put_in_whd m1 m2 =
417 NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
418 NCicReduction.reduce_machine ~delta:max_int ~subst context m2
421 ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
423 assert (not (norm1 && norm2));
425 x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
427 NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
429 let h1 = height_of t1 in
430 let h2 = height_of t2 in
431 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
432 NCicReduction.reduce_machine ~delta ~subst context m1,
433 NCicReduction.reduce_machine ~delta ~subst context m2
435 let rec unif_machines metasenv subst =
437 | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
438 (*D*) inside 'M'; try let rc =
440 pp (lazy((if are_normal then "*" else " ") ^ " " ^
441 NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
443 NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2)));
445 let relevance = [] (* TO BE UNDERSTOOD
447 | C.Const r -> NCicEnvironment.get_relevance r
449 let unif_from_stack t1 t2 b metasenv subst =
451 let t1 = NCicReduction.from_stack t1 in
452 let t2 = NCicReduction.from_stack t2 in
453 unif_machines metasenv subst (put_in_whd t1 t2)
454 with UnificationFailure _ | Uncertain _ when not b ->
457 let rec check_stack l1 l2 r (metasenv, subst) =
459 | x1::tl1, x2::tl2, r::tr ->
460 check_stack tl1 tl2 tr
461 (unif_from_stack x1 x2 r metasenv subst)
462 | x1::tl1, x2::tl2, [] ->
463 check_stack tl1 tl2 []
464 (unif_from_stack x1 x2 true metasenv subst)
466 fo_unif test_eq_only metasenv subst
467 (NCicReduction.unwind (k1,e1,t1,List.rev l1))
468 (NCicReduction.unwind (k2,e2,t2,List.rev l2))
470 try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
471 with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
472 unif_machines metasenv subst (small_delta_step m1 m2)
473 (*D*) in outside(); rc with exn -> outside (); raise exn
475 try fo_unif test_eq_only metasenv subst t1 t2
476 with UnificationFailure msg | Uncertain msg as exn ->
478 unif_machines metasenv subst
479 (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
481 | UnificationFailure _ -> raise (UnificationFailure msg)
482 | Uncertain _ -> raise exn
483 (*D*) in outside(); rc with exn -> outside (); raise exn
496 exception UnificationFailure of string Lazy.t;;
497 exception Uncertain of string Lazy.t;;
498 exception AssertFailure of string Lazy.t;;
500 let verbose = false;;
501 let debug_print = fun _ -> ()
503 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
504 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
505 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
506 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
508 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
510 let type_of_aux' metasenv subst context term ugraph =
513 profile.HExtlib.profile
514 (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
516 CicTypeChecker.TypeCheckerFailure msg ->
520 "Kernel Type checking error:
521 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
522 (CicMetaSubst.ppterm ~metasenv subst term)
523 (CicMetaSubst.ppterm ~metasenv [] term)
524 (CicMetaSubst.ppcontext ~metasenv subst context)
525 (CicMetaSubst.ppmetasenv subst metasenv)
526 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
527 raise (AssertFailure msg)
528 | CicTypeChecker.AssertFailure msg ->
531 "Kernel Type checking assertion failure:
532 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
533 (CicMetaSubst.ppterm ~metasenv subst term)
534 (CicMetaSubst.ppterm ~metasenv [] term)
535 (CicMetaSubst.ppcontext ~metasenv subst context)
536 (CicMetaSubst.ppmetasenv subst metasenv)
537 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
538 raise (AssertFailure msg)
539 in profiler_toa.HExtlib.profile foo ()
542 let exists_a_meta l =
546 | Cic.Appl (Cic.Meta _::_) -> true
549 let rec deref subst t =
550 let snd (_,a,_) = a in
555 (CicSubstitution.subst_meta
556 l (snd (CicUtil.lookup_subst n subst)))
558 CicUtil.Subst_not_found _ -> t)
559 | Cic.Appl(Cic.Meta(n,l)::args) ->
560 (match deref subst (Cic.Meta(n,l)) with
561 | Cic.Lambda _ as t ->
562 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
563 | r -> Cic.Appl(r::args))
564 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
565 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
570 let foo () = deref subst t
571 in profiler_deref.HExtlib.profile foo ()
573 exception WrongShape;;
574 let eta_reduce after_beta_expansion after_beta_expansion_body
575 before_beta_expansion
578 match before_beta_expansion,after_beta_expansion_body with
579 Cic.Appl l, Cic.Appl l' ->
580 let rec all_but_last check_last =
584 | [_] -> if check_last then raise WrongShape else []
585 | he::tl -> he::(all_but_last check_last tl)
587 let all_but_last check_last l =
588 match all_but_last check_last l with
593 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
594 let all_but_last = all_but_last false l in
595 (* here we should test alpha-equivalence; however we know by
596 construction that here alpha_equivalence is equivalent to = *)
597 if t = all_but_last then
601 | _,_ -> after_beta_expansion
603 WrongShape -> after_beta_expansion
605 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
606 let module S = CicSubstitution in
607 let module C = Cic in
609 let rec aux metasenv subst n context t' ugraph =
612 let subst,metasenv,ugraph1 =
613 fo_unif_subst test_equality_only subst context metasenv
614 (CicSubstitution.lift n arg) t' ugraph
617 subst,metasenv,C.Rel (1 + n),ugraph1
620 | UnificationFailure _ ->
622 | C.Rel m -> subst,metasenv,
623 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
624 | C.Var (uri,exp_named_subst) ->
625 let subst,metasenv,exp_named_subst',ugraph1 =
626 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
628 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
630 (* andrea: in general, beta_expand can create badly typed
631 terms. This happens quite seldom in practice, UNLESS we
632 iterate on the local context. For this reason, we renounce
633 to iterate and just lift *)
637 Some t -> Some (CicSubstitution.lift 1 t)
639 subst, metasenv, C.Meta (i,l), ugraph
641 | C.Implicit _ as t -> subst,metasenv,t,ugraph
643 let subst,metasenv,te',ugraph1 =
644 aux metasenv subst n context te ugraph in
645 let subst,metasenv,ty',ugraph2 =
646 aux metasenv subst n context ty ugraph1 in
647 (* TASSI: sure this is in serial? *)
648 subst,metasenv,(C.Cast (te', ty')),ugraph2
650 let subst,metasenv,s',ugraph1 =
651 aux metasenv subst n context s ugraph in
652 let subst,metasenv,t',ugraph2 =
653 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
656 (* TASSI: sure this is in serial? *)
657 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
658 | C.Lambda (nn,s,t) ->
659 let subst,metasenv,s',ugraph1 =
660 aux metasenv subst n context s ugraph in
661 let subst,metasenv,t',ugraph2 =
662 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
664 (* TASSI: sure this is in serial? *)
665 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
666 | C.LetIn (nn,s,ty,t) ->
667 let subst,metasenv,s',ugraph1 =
668 aux metasenv subst n context s ugraph in
669 let subst,metasenv,ty',ugraph1 =
670 aux metasenv subst n context ty ugraph in
671 let subst,metasenv,t',ugraph2 =
672 aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
675 (* TASSI: sure this is in serial? *)
676 subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
678 let subst,metasenv,revl',ugraph1 =
680 (fun (subst,metasenv,appl,ugraph) t ->
681 let subst,metasenv,t',ugraph1 =
682 aux metasenv subst n context t ugraph in
683 subst,metasenv,(t'::appl),ugraph1
684 ) (subst,metasenv,[],ugraph) l
686 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
687 | C.Const (uri,exp_named_subst) ->
688 let subst,metasenv,exp_named_subst',ugraph1 =
689 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
691 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
692 | C.MutInd (uri,i,exp_named_subst) ->
693 let subst,metasenv,exp_named_subst',ugraph1 =
694 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
696 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
697 | C.MutConstruct (uri,i,j,exp_named_subst) ->
698 let subst,metasenv,exp_named_subst',ugraph1 =
699 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
701 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
702 | C.MutCase (sp,i,outt,t,pl) ->
703 let subst,metasenv,outt',ugraph1 =
704 aux metasenv subst n context outt ugraph in
705 let subst,metasenv,t',ugraph2 =
706 aux metasenv subst n context t ugraph1 in
707 let subst,metasenv,revpl',ugraph3 =
709 (fun (subst,metasenv,pl,ugraph) t ->
710 let subst,metasenv,t',ugraph1 =
711 aux metasenv subst n context t ugraph in
712 subst,metasenv,(t'::pl),ugraph1
713 ) (subst,metasenv,[],ugraph2) pl
715 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
716 (* TASSI: not sure this is serial *)
718 (*CSC: not implemented
719 let tylen = List.length fl in
722 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
725 C.Fix (i, substitutedfl)
727 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
729 (*CSC: not implemented
730 let tylen = List.length fl in
733 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
736 C.CoFix (i, substitutedfl)
739 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
741 and aux_exp_named_subst metasenv subst n context ens ugraph =
743 (fun (uri,t) (subst,metasenv,l,ugraph) ->
744 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
745 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
747 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
749 FreshNamesGenerator.mk_fresh_name ~subst
750 metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
752 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
753 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
754 subst, metasenv, t'', ugraph2
755 in profiler_beta_expand.HExtlib.profile foo ()
758 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
759 let _,subst,metasenv,hd,ugraph =
761 (fun arg (num,subst,metasenv,t,ugraph) ->
762 let subst,metasenv,t,ugraph1 =
763 beta_expand num test_equality_only
764 metasenv subst context t arg ugraph
766 num+1,subst,metasenv,t,ugraph1
767 ) args (1,subst,metasenv,t,ugraph)
769 subst,metasenv,hd,ugraph
771 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
774 | (m2,_,c2,c2')::_ ->
775 let m1,c1,c1' = carr,to1,to2 in
777 function Some (_,t) -> CicPp.ppterm t
781 ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
782 CoercDb.string_of_carr car2^": " ^
783 CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
784 unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
785 unopt c2^" + "^unopt c2')
787 (* NUOVA UNIFICAZIONE *)
788 (* A substitution is a (int * Cic.term) list that associates a
789 metavariable i with its body.
790 A metaenv is a (int * Cic.term) list that associate a metavariable
792 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
793 a new substitution which is _NOT_ unwinded. It must be unwinded before
796 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
797 let module C = Cic in
798 let module R = CicReduction in
799 let module S = CicSubstitution in
800 let t1 = deref subst t1 in
801 let t2 = deref subst t2 in
802 let (&&&) a b = (a && b) || ((not a) && (not b)) in
803 (* let bef = Sys.time () in *)
805 if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
809 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
810 in profiler_are_convertible.HExtlib.profile foo ()
812 (* let aft = Sys.time () in
813 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
814 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
815 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
817 subst, metasenv, ugraph
820 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
821 let _,subst,metasenv,ugraph1 =
824 (fun (j,subst,metasenv,ugraph) t1 t2 ->
827 | _,None -> j+1,subst,metasenv,ugraph
828 | Some t1', Some t2' ->
829 (* First possibility: restriction *)
830 (* Second possibility: unification *)
831 (* Third possibility: convertibility *)
834 ~subst ~metasenv context t1' t2' ugraph
837 j+1,subst,metasenv, ugraph1
840 let subst,metasenv,ugraph2 =
843 subst context metasenv t1' t2' ugraph
845 j+1,subst,metasenv,ugraph2
848 | UnificationFailure _ ->
849 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
850 let metasenv, subst =
851 CicMetaSubst.restrict
852 subst [(n,j)] metasenv in
853 j+1,subst,metasenv,ugraph1)
854 ) (1,subst,metasenv,ugraph) ln lm
858 (UnificationFailure (lazy "1"))
861 "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."
862 (CicMetaSubst.ppterm ~metasenv subst t1)
863 (CicMetaSubst.ppterm ~metasenv subst t2))) *)
864 | Invalid_argument _ ->
866 (UnificationFailure (lazy "2")))
869 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
870 (CicMetaSubst.ppterm ~metasenv subst t1)
871 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
872 in subst,metasenv,ugraph1
873 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
874 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
876 | (t, C.Meta (n,l)) ->
879 C.Meta (n,_), C.Meta (m,_) when n < m -> false
880 | _, C.Meta _ -> false
883 let lower = fun x y -> if swap then y else x in
884 let upper = fun x y -> if swap then x else y in
885 let fo_unif_subst_ordered
886 test_equality_only subst context metasenv m1 m2 ugraph =
887 fo_unif_subst test_equality_only subst context metasenv
888 (lower m1 m2) (upper m1 m2) ugraph
891 let subst,metasenv,ugraph1 =
892 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
895 type_of_aux' metasenv subst context t ugraph
899 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
901 UnificationFailure _ as e -> raise e
902 | Uncertain msg -> raise (UnificationFailure msg)
904 debug_print (lazy "siamo allo huge hack");
905 (* TODO huge hack!!!!
906 * we keep on unifying/refining in the hope that
907 * the problem will be eventually solved.
908 * In the meantime we're breaking a big invariant:
909 * the terms that we are unifying are no longer well
910 * typed in the current context (in the worst case
911 * we could even diverge) *)
912 (subst, metasenv,ugraph)) in
913 let t',metasenv,subst =
915 CicMetaSubst.delift n subst context metasenv l t
917 (CicMetaSubst.MetaSubstFailure msg)->
918 raise (UnificationFailure msg)
919 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
923 C.Sort (C.Type u) when not test_equality_only ->
924 let u' = CicUniv.fresh () in
925 let s = C.Sort (C.Type u') in
928 CicUniv.add_ge (upper u u') (lower u u') ugraph1
932 CicUniv.UniverseInconsistency msg ->
933 raise (UnificationFailure msg))
936 (* Unifying the types may have already instantiated n. Let's check *)
938 let (_, oldt,_) = CicUtil.lookup_subst n subst in
939 let lifted_oldt = S.subst_meta l oldt in
940 fo_unif_subst_ordered
941 test_equality_only subst context metasenv t lifted_oldt ugraph2
943 CicUtil.Subst_not_found _ ->
944 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
945 let subst = (n, (context, t'',ty)) :: subst in
947 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
948 subst, metasenv, ugraph2
950 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
951 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
952 if UriManager.eq uri1 uri2 then
953 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
954 exp_named_subst1 exp_named_subst2 ugraph
956 raise (UnificationFailure (lazy
958 "Can't unify %s with %s due to different constants"
959 (CicMetaSubst.ppterm ~metasenv subst t1)
960 (CicMetaSubst.ppterm ~metasenv subst t2))))
961 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
962 if UriManager.eq uri1 uri2 && i1 = i2 then
963 fo_unif_subst_exp_named_subst
965 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
967 raise (UnificationFailure
970 "Can't unify %s with %s due to different inductive principles"
971 (CicMetaSubst.ppterm ~metasenv subst t1)
972 (CicMetaSubst.ppterm ~metasenv subst t2))))
973 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
974 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
975 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
976 fo_unif_subst_exp_named_subst
978 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
980 raise (UnificationFailure
983 "Can't unify %s with %s due to different inductive constructors"
984 (CicMetaSubst.ppterm ~metasenv subst t1)
985 (CicMetaSubst.ppterm ~metasenv subst t2))))
986 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
987 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
988 subst context metasenv te t2 ugraph
989 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
990 subst context metasenv t1 te ugraph
991 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
992 let subst',metasenv',ugraph1 =
993 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
995 fo_unif_subst test_equality_only
996 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
997 | (C.LetIn (_,s1,ty1,t1), t2)
998 | (t2, C.LetIn (_,s1,ty1,t1)) ->
1000 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
1001 | (C.Appl l1, C.Appl l2) ->
1002 (* andrea: this case should be probably rewritten in the
1005 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
1008 (fun (subst,metasenv,ugraph) t1 t2 ->
1010 test_equality_only subst context metasenv t1 t2 ugraph)
1011 (subst,metasenv,ugraph) l1 l2
1012 with (Invalid_argument msg) ->
1013 raise (UnificationFailure (lazy msg)))
1014 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
1015 (* we verify that none of the args is a Meta,
1016 since beta expanding with respoect to a metavariable
1020 let (_,t,_) = CicUtil.lookup_subst i subst in
1021 let lifted = S.subst_meta l t in
1022 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
1025 subst context metasenv reduced t2 ugraph
1026 with CicUtil.Subst_not_found _ -> *)
1027 let subst,metasenv,beta_expanded,ugraph1 =
1029 test_equality_only metasenv subst context t2 args ugraph
1031 fo_unif_subst test_equality_only subst context metasenv
1032 (C.Meta (i,l)) beta_expanded ugraph1
1033 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
1035 let (_,t,_) = CicUtil.lookup_subst i subst in
1036 let lifted = S.subst_meta l t in
1037 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
1040 subst context metasenv t1 reduced ugraph
1041 with CicUtil.Subst_not_found _ -> *)
1042 let subst,metasenv,beta_expanded,ugraph1 =
1045 metasenv subst context t1 args ugraph
1047 fo_unif_subst test_equality_only subst context metasenv
1048 (C.Meta (i,l)) beta_expanded ugraph1
1050 let lr1 = List.rev l1 in
1051 let lr2 = List.rev l2 in
1053 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
1056 | _,[] -> assert false
1059 test_equality_only subst context metasenv h1 h2 ugraph
1062 fo_unif_subst test_equality_only subst context metasenv
1063 h (C.Appl (List.rev l)) ugraph
1064 | ((h1::l1),(h2::l2)) ->
1065 let subst', metasenv',ugraph1 =
1068 subst context metasenv h1 h2 ugraph
1071 test_equality_only subst' metasenv' (l1,l2) ugraph1
1075 test_equality_only subst metasenv (lr1, lr2) ugraph
1077 | UnificationFailure s
1078 | Uncertain s as exn ->
1081 | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
1082 (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
1083 CoercDb.is_a_coercion cc1 <> None &&
1084 CoercDb.is_a_coercion cc2 <> None &&
1085 not (UriManager.eq uri1 uri2) ->
1087 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1089 let inner_coerced t =
1090 let t = CicMetaSubst.apply_subst subst t in
1094 (match CoercGraph.coerced_arg l with
1096 | Some (t,_) -> aux (List.hd l) t t)
1099 aux (Cic.Implicit None) (Cic.Implicit None) t
1101 let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
1102 let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
1105 CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
1107 | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
1110 let head1_c, head2_c =
1112 CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
1114 | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
1117 let unfold uri ens args =
1119 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
1123 | Cic.Constant (_,Some bo,_,_,_) ->
1124 CicReduction.head_beta_reduce ~delta:false
1125 (Cic.Appl (bo::args))
1128 let conclude subst metasenv ugraph last_tl1' last_tl2' =
1129 let subst',metasenv,ugraph =
1132 ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
1133 " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
1135 fo_unif_subst test_equality_only subst context
1136 metasenv last_tl1' last_tl2' ugraph
1138 if subst = subst' then raise exn
1141 let subst,metasenv,ugrph as res =
1143 fo_unif_subst test_equality_only subst' context
1144 metasenv (C.Appl l1) (C.Appl l2) ugraph
1148 (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
1149 " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1153 if CoercDb.eq_carr car1 car2 then
1154 match last_tl1,last_tl2 with
1155 | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
1158 let subst,metasenv,ugraph =
1159 fo_unif_subst test_equality_only subst context
1160 metasenv last_tl1 last_tl2 ugraph
1162 fo_unif_subst test_equality_only subst context
1163 metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
1164 | _ when CoercDb.eq_carr head1_c head2_c ->
1165 (* composite VS composition + metas avoiding
1166 * coercions not only in coerced position *)
1167 if c1 <> cc1 && c2 <> cc2 then
1168 conclude subst metasenv ugraph
1173 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
1175 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
1177 fo_unif_subst test_equality_only subst context
1178 metasenv l1 l2 ugraph
1182 match last_tl1 with Cic.Meta _ -> true | _ -> false in
1184 match last_tl2 with Cic.Meta _ -> true | _ -> false in
1185 if not (grow1 || grow2) then
1186 (* no flexible terminals -> no pullback, but
1187 * we still unify them, in some cases it helps *)
1188 conclude subst metasenv ugraph last_tl1 last_tl2
1192 metasenv subst context (grow1,car1) (grow2,car2)
1196 | (carr,metasenv,to1,to2)::xxx ->
1197 warn_if_not_unique xxx to1 to2 carr car1 car2;
1198 let last_tl1',(subst,metasenv,ugraph) =
1199 match grow1,to1 with
1200 | true,Some (last,coerced) ->
1202 fo_unif_subst test_equality_only subst context
1203 metasenv coerced last_tl1 ugraph
1204 | _ -> last_tl1,(subst,metasenv,ugraph)
1206 let last_tl2',(subst,metasenv,ugraph) =
1207 match grow2,to2 with
1208 | true,Some (last,coerced) ->
1210 fo_unif_subst test_equality_only subst context
1211 metasenv coerced last_tl2 ugraph
1212 | _ -> last_tl2,(subst,metasenv,ugraph)
1214 conclude subst metasenv ugraph last_tl1' last_tl2')
1216 (* {{{ CSC: This is necessary because of the "elim H" tactic
1217 where the type of H is only reducible to an
1218 inductive type. This could be extended from inductive
1219 types to any rigid term. However, the code is
1220 duplicated in two places: inside applications and
1221 outside them. Probably it would be better to
1222 work with lambda-bar terms instead. *)
1223 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
1224 | (_, Cic.MutInd _::_) ->
1225 let t1' = R.whd ~subst context t1 in
1227 C.Appl (C.MutInd _::_) ->
1228 fo_unif_subst test_equality_only
1229 subst context metasenv t1' t2 ugraph
1230 | _ -> raise (UnificationFailure (lazy "88")))
1231 | (Cic.MutInd _::_,_) ->
1232 let t2' = R.whd ~subst context t2 in
1234 C.Appl (C.MutInd _::_) ->
1235 fo_unif_subst test_equality_only
1236 subst context metasenv t1 t2' ugraph
1239 (lazy ("not a mutind :"^
1240 CicMetaSubst.ppterm ~metasenv subst t2 ))))
1243 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
1244 let subst', metasenv',ugraph1 =
1245 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
1247 let subst'',metasenv'',ugraph2 =
1248 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
1252 (fun (subst,metasenv,ugraph) t1 t2 ->
1254 test_equality_only subst context metasenv t1 t2 ugraph
1255 ) (subst'',metasenv'',ugraph2) pl1 pl2
1257 Invalid_argument _ ->
1258 raise (UnificationFailure (lazy "6.1")))
1260 "Error trying to unify %s with %s: the number of branches is not the same."
1261 (CicMetaSubst.ppterm ~metasenv subst t1)
1262 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
1263 | (C.Rel _, _) | (_, C.Rel _) ->
1265 subst, metasenv,ugraph
1267 raise (UnificationFailure (lazy
1269 "Can't unify %s with %s because they are not convertible"
1270 (CicMetaSubst.ppterm ~metasenv subst t1)
1271 (CicMetaSubst.ppterm ~metasenv subst t2))))
1272 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
1273 let subst,metasenv,beta_expanded,ugraph1 =
1275 test_equality_only metasenv subst context t2 args ugraph
1277 fo_unif_subst test_equality_only subst context metasenv
1278 (C.Meta (i,l)) beta_expanded ugraph1
1279 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
1280 let subst,metasenv,beta_expanded,ugraph1 =
1282 test_equality_only metasenv subst context t1 args ugraph
1284 fo_unif_subst test_equality_only subst context metasenv
1285 beta_expanded (C.Meta (i,l)) ugraph1
1286 (* Works iff there are no arguments applied to it; similar to the
1288 | (_, C.MutInd _) ->
1289 let t1' = R.whd ~subst context t1 in
1292 fo_unif_subst test_equality_only
1293 subst context metasenv t1' t2 ugraph
1294 | _ -> raise (UnificationFailure (lazy "8")))
1296 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
1297 let subst',metasenv',ugraph1 =
1298 fo_unif_subst true subst context metasenv s1 s2 ugraph
1300 fo_unif_subst test_equality_only
1301 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1303 (match CicReduction.whd ~subst context t2 with
1305 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1306 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
1308 (match CicReduction.whd ~subst context t1 with
1310 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1311 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
1313 (* delta-beta reduction should almost never be a problem for
1315 1. long computations require iota reduction
1316 2. it is extremely rare that a close term t1 (that could be unified
1317 to t2) beta-delta reduces to t1' while t2 does not beta-delta
1318 reduces in the same way. This happens only if one meta of t2
1319 occurs in head position during beta reduction. In this unluky
1320 case too much reduction will be performed on t1 and unification
1321 will surely fail. *)
1322 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
1323 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
1324 if t1 = t1' && t2 = t2' then
1325 raise (UnificationFailure
1328 "Can't unify %s with %s because they are not convertible"
1329 (CicMetaSubst.ppterm ~metasenv subst t1)
1330 (CicMetaSubst.ppterm ~metasenv subst t2))))
1333 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
1335 UnificationFailure _
1337 raise (UnificationFailure
1340 "Can't unify %s with %s because they are not convertible"
1341 (CicMetaSubst.ppterm ~metasenv subst t1)
1342 (CicMetaSubst.ppterm ~metasenv subst t2))))
1344 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
1345 exp_named_subst1 exp_named_subst2 ugraph
1349 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
1350 assert (uri1=uri2) ;
1351 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1352 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
1354 Invalid_argument _ ->
1359 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
1362 raise (UnificationFailure (lazy (sprintf
1363 "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))))
1365 (* A substitution is a (int * Cic.term) list that associates a *)
1366 (* metavariable i with its body. *)
1367 (* metasenv is of type Cic.metasenv *)
1368 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
1369 (* a new substitution which is already unwinded and ready to be applied and *)
1370 (* a new metasenv in which some hypothesis in the contexts of the *)
1371 (* metavariables may have been restricted. *)
1372 let fo_unif metasenv context t1 t2 ugraph =
1373 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
1375 let enrich_msg msg subst context metasenv t1 t2 ugraph =
1378 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"
1379 (CicMetaSubst.ppterm ~metasenv subst t1)
1381 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1384 | UnificationFailure s
1386 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1387 (CicMetaSubst.ppterm ~metasenv subst t2)
1389 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1392 | UnificationFailure s
1394 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1395 (CicMetaSubst.ppcontext ~metasenv subst context)
1396 (CicMetaSubst.ppmetasenv subst metasenv)
1397 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
1399 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
1400 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
1402 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1403 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
1405 | UnificationFailure s
1407 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1408 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
1410 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1411 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
1413 | UnificationFailure s
1415 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1416 (CicMetaSubst.ppcontext ~metasenv subst context)
1417 (CicMetaSubst.ppmetasenv subst metasenv)
1421 let fo_unif_subst subst context metasenv t1 t2 ugraph =
1423 fo_unif_subst false subst context metasenv t1 t2 ugraph
1425 | AssertFailure msg ->
1426 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1427 | UnificationFailure msg ->
1428 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))