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 -> prerr_endline "no sup for" ;
89 raise (fail_exc metasenv subst context meta t)
90 | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
92 NCic.Sort (NCic.Type (
93 match NCicEnvironment.sup NCicEnvironment.type0 with
96 | NCic.Meta _ as orig -> orig
97 | t -> NCicUtils.map (fun _ _ -> ()) () aux t
102 let rec beta_expand num test_eq_only swap metasenv subst context t arg =
103 let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
105 let metasenv, subst =
107 unify test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
109 unify test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
111 (metasenv, subst), NCic.Rel (1 + n)
112 with Uncertain _ | UnificationFailure _ ->
114 | NCic.Rel m as orig ->
115 (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
116 (* andrea: in general, beta_expand can create badly typed
117 terms. This happens quite seldom in practice, UNLESS we
118 iterate on the local context. For this reason, we renounce
119 to iterate and just lift *)
120 | NCic.Meta (i,(shift,lc)) ->
121 (metasenv,subst), NCic.Meta (i,(shift+1,lc))
122 | NCic.Prod (name, src, tgt) as orig ->
123 let (metasenv, subst), src1 = aux (n,context,true) acc src in
124 let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
125 let ms, tgt1 = aux k (metasenv, subst) tgt in
126 if src == src1 && tgt == tgt1 then ms, orig else
127 ms, NCic.Prod (name, src1, tgt1)
129 NCicUntrusted.map_term_fold_a
130 (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t
133 let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
134 let fresh_name = "Hbeta" ^ string_of_int num in
135 let (metasenv,subst), t1 =
136 aux (0, context, test_eq_only) (metasenv, subst) t in
137 let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in
139 ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
141 with NCicTypeChecker.TypeCheckerFailure _ ->
142 metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
144 and beta_expand_many test_equality_only swap metasenv subst context t args =
145 (* (*D*) inside 'B'; try let rc = *)
146 pp (lazy (String.concat ", "
147 (List.map (NCicPp.ppterm ~metasenv ~subst ~context)
148 args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
149 let _, subst, metasenv, hd =
151 (fun arg (num,subst,metasenv,t) ->
152 let metasenv, subst, t =
153 beta_expand num test_equality_only swap metasenv subst context t arg
155 num+1,subst,metasenv,t)
156 args (1,subst,metasenv,t)
158 pp (lazy ("Head syntesized by b-exp: " ^
159 NCicPp.ppterm ~metasenv ~subst ~context hd));
161 (* (*D*) in outside (); rc with exn -> outside (); raise exn *)
163 and instantiate test_eq_only metasenv subst context n lc t swap =
164 (*D*) inside 'I'; try let rc =
165 pp (lazy(string_of_int n ^ " :=?= "^
166 NCicPp.ppterm ~metasenv ~subst ~context t));
167 let unify test_eq_only m s c t1 t2 =
168 if swap then unify test_eq_only m s c t2 t1
169 else unify test_eq_only m s c t1 t2
171 let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
172 let metasenv, subst, t =
174 | NCic.Implicit (`Typeof _) ->
176 (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *)
179 "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^
180 NCicPp.ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^
181 NCicPp.ppmetasenv ~subst metasenv));
183 try t, NCicTypeChecker.typeof ~subst ~metasenv context t
185 | NCicTypeChecker.AssertFailure msg ->
186 (pp (lazy "fine typeof (fallimento)");
188 fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t
191 (prerr_endline ( ("ILLTYPED: " ^
192 NCicPp.ppterm ~metasenv ~subst ~context t
193 ^ "\nBECAUSE:" ^ Lazy.force msg ^ "\nCONTEXT:\n" ^
194 NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^
195 NCicPp.ppmetasenv ~subst metasenv
200 pp (lazy ("typeof: " ^
201 NCicPp.ppterm ~metasenv ~subst ~context ft));
202 ft, NCicTypeChecker.typeof ~subst ~metasenv context ft
203 with NCicTypeChecker.AssertFailure _ ->
205 | NCicTypeChecker.TypeCheckerFailure msg ->
208 let lty = NCicSubstitution.subst_meta lc ty in
209 pp (lazy("On the types: " ^
210 NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
211 NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
212 ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
213 let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
216 pp (lazy(string_of_int n ^ " := 111 = "^
217 NCicPp.ppterm ~metasenv ~subst ~context t));
218 let (metasenv, subst), t =
219 try NCicMetaSubst.delift metasenv subst context n lc t
220 with NCicMetaSubst.Uncertain msg ->
221 pp (lazy ("delift fails: " ^ Lazy.force msg));
222 raise (Uncertain msg)
223 | NCicMetaSubst.MetaSubstFailure msg ->
224 pp (lazy ("delift fails: " ^ Lazy.force msg));
225 raise (UnificationFailure msg)
227 pp (lazy(string_of_int n ^ " := 222 = "^
228 NCicPp.ppterm ~metasenv ~subst ~context:ctx t
229 ^ "\n" ^ NCicPp.ppmetasenv ~subst metasenv
232 (* Unifying the types may have already instantiated n. *)
234 let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
235 let oldt = NCicSubstitution.subst_meta lc oldt in
236 let t = NCicSubstitution.subst_meta lc t in
237 (* conjecture: always fail --> occur check *)
238 unify test_eq_only metasenv subst context oldt t
239 with NCicUtils.Subst_not_found _ ->
240 (* by cumulativity when unify(?,Type_i)
241 * we could ? := Type_j with j <= i... *)
242 let subst = (n, (name, ctx, t, ty)) :: subst in
243 pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
244 ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
246 List.filter (fun (m,_) -> not (n = m)) metasenv
249 (*D*) in outside(); rc with exn -> outside (); raise exn
251 and unify test_eq_only metasenv subst context t1 t2 =
252 (*D*) inside 'U'; try let rc =
253 let fo_unif test_eq_only metasenv subst t1 t2 =
254 (*D*) inside 'F'; try let rc =
255 pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^
256 NCicPp.ppterm ~metasenv ~subst ~context t2));
261 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
262 if NCicEnvironment.universe_leq a b then metasenv, subst
263 else raise (fail_exc metasenv subst context t1 t2)
264 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
265 if NCicEnvironment.universe_eq a b then metasenv, subst
266 else raise (fail_exc metasenv subst context t1 t2)
267 | (C.Sort C.Prop,C.Sort (C.Type _)) ->
268 if (not test_eq_only) then metasenv, subst
269 else raise (fail_exc metasenv subst context t1 t2)
271 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
272 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
273 let metasenv, subst = unify true metasenv subst context s1 s2 in
274 unify test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
275 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
276 let metasenv,subst=unify test_eq_only metasenv subst context ty1 ty2 in
277 let metasenv,subst=unify test_eq_only metasenv subst context s1 s2 in
278 let context = (name1, C.Def (s1,ty1))::context in
279 unify test_eq_only metasenv subst context t1 t2
281 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
283 let l1 = NCicUtils.expand_local_context l1 in
284 let l2 = NCicUtils.expand_local_context l2 in
285 let metasenv, subst, to_restrict, _ =
287 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
289 let metasenv, subst =
290 unify test_eq_only metasenv subst context
291 (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
293 metasenv, subst, to_restrict, i-1
294 with UnificationFailure _ | Uncertain _ ->
295 metasenv, subst, i::to_restrict, i-1)
296 l1 l2 (metasenv, subst, [], List.length l1)
298 if to_restrict <> [] then
299 let metasenv, subst, _ =
300 NCicMetaSubst.restrict metasenv subst n1 to_restrict
305 | Invalid_argument _ -> assert false
306 | NCicMetaSubst.MetaSubstFailure msg ->
308 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
309 let term1 = NCicSubstitution.subst_meta lc1 term in
310 let term2 = NCicSubstitution.subst_meta lc2 term in
311 unify test_eq_only metasenv subst context term1 term2
312 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
314 | C.Meta (n,lc), t ->
316 let _,_,term,_ = NCicUtils.lookup_subst n subst in
317 let term = NCicSubstitution.subst_meta lc term in
318 unify test_eq_only metasenv subst context term t
319 with NCicUtils.Subst_not_found _->
320 instantiate test_eq_only metasenv subst context n lc t false)
322 | t, C.Meta (n,lc) ->
324 let _,_,term,_ = NCicUtils.lookup_subst n subst in
325 let term = NCicSubstitution.subst_meta lc term in
326 unify test_eq_only metasenv subst context t term
327 with NCicUtils.Subst_not_found _->
328 instantiate test_eq_only metasenv subst context n lc t true)
330 | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
331 let _,_,term,_ = NCicUtils.lookup_subst i subst in
332 let term = NCicSubstitution.subst_meta l term in
333 unify test_eq_only metasenv subst context (mk_appl term args) t2
335 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
336 let _,_,term,_ = NCicUtils.lookup_subst i subst in
337 let term = NCicSubstitution.subst_meta l term in
338 unify test_eq_only metasenv subst context t1 (mk_appl term args)
340 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
341 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
344 (fun (metasenv, subst) t1 t2 ->
345 unify test_eq_only metasenv subst context t1 t2)
346 (metasenv,subst) l1 l2
347 with Invalid_argument _ ->
348 raise (fail_exc metasenv subst context t1 t2))
350 | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
351 (* we verify that none of the args is a Meta,
352 since beta expanding w.r.t a metavariable makes no sense *)
353 let metasenv, subst, beta_expanded =
356 metasenv subst context t2 args
358 unify test_eq_only metasenv subst context
359 (C.Meta (i,l)) beta_expanded
361 | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
362 let metasenv, subst, beta_expanded =
365 metasenv subst context t1 args
367 unify test_eq_only metasenv subst context
368 beta_expanded (C.Meta (i,l))
370 (* processing this case here we avoid a useless small delta step *)
371 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
373 let relevance = NCicEnvironment.get_relevance r1 in
374 let relevance = match r1 with
375 | Ref.Ref (_,Ref.Con (_,_,lno)) ->
376 let _,relevance = HExtlib.split_nth lno relevance in
377 HExtlib.mk_list false lno @ relevance
380 let metasenv, subst, _ =
383 (fun (metasenv, subst, relevance) t1 t2 ->
385 match relevance with b::tl -> b,tl | _ -> true, [] in
386 let metasenv, subst =
387 try unify test_eq_only metasenv subst context t1 t2
388 with UnificationFailure _ | Uncertain _ when not b ->
391 metasenv, subst, relevance)
392 (metasenv, subst, relevance) tl1 tl2
393 with Invalid_argument _ ->
394 raise (uncert_exc metasenv subst context t1 t2)
398 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
399 C.Match (ref2,outtype2,term2,pl2)) ->
400 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
401 let _,_,ty,_ = List.nth itl tyno in
402 let rec remove_prods ~subst context ty =
403 let ty = NCicReduction.whd ~subst context ty in
406 | C.Prod (name,so,ta) ->
407 remove_prods ~subst ((name,(C.Decl so))::context) ta
411 match remove_prods ~subst [] ty with
412 | C.Sort C.Prop -> true
415 let rec remove_prods ~subst context ty =
416 let ty = NCicReduction.whd ~subst context ty in
419 | C.Prod (name,so,ta) ->
420 remove_prods ~subst ((name,(C.Decl so))::context) ta
423 if not (Ref.eq ref1 ref2) then
424 raise (uncert_exc metasenv subst context t1 t2)
426 let metasenv, subst =
427 unify test_eq_only metasenv subst context outtype1 outtype2 in
428 let metasenv, subst =
429 try unify test_eq_only metasenv subst context term1 term2
430 with UnificationFailure _ | Uncertain _ when is_prop ->
435 (fun (metasenv,subst) ->
436 unify test_eq_only metasenv subst context)
437 (metasenv, subst) pl1 pl2
438 with Invalid_argument _ ->
439 raise (uncert_exc metasenv subst context t1 t2))
440 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
441 | _ -> raise (uncert_exc metasenv subst context t1 t2)
442 (*D*) in outside(); rc with exn -> outside (); raise exn
444 let height_of = function
445 | NCic.Const (Ref.Ref (_,Ref.Def h))
446 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
447 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
448 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
451 let put_in_whd m1 m2 =
452 NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
453 NCicReduction.reduce_machine ~delta:max_int ~subst context m2
456 ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
458 assert (not (norm1 && norm2));
460 x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
462 NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
464 let h1 = height_of t1 in
465 let h2 = height_of t2 in
466 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
467 NCicReduction.reduce_machine ~delta ~subst context m1,
468 NCicReduction.reduce_machine ~delta ~subst context m2
470 let rec unif_machines metasenv subst =
472 | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
473 (*D*) inside 'M'; try let rc =
475 pp (lazy((if are_normal then "*" else " ") ^ " " ^
476 NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
478 NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2)));
480 let relevance = [] (* TO BE UNDERSTOOD
482 | C.Const r -> NCicEnvironment.get_relevance r
484 let unif_from_stack t1 t2 b metasenv subst =
486 let t1 = NCicReduction.from_stack t1 in
487 let t2 = NCicReduction.from_stack t2 in
488 unif_machines metasenv subst (put_in_whd t1 t2)
489 with UnificationFailure _ | Uncertain _ when not b ->
492 let rec check_stack l1 l2 r (metasenv, subst) =
494 | x1::tl1, x2::tl2, r::tr ->
495 check_stack tl1 tl2 tr
496 (unif_from_stack x1 x2 r metasenv subst)
497 | x1::tl1, x2::tl2, [] ->
498 check_stack tl1 tl2 []
499 (unif_from_stack x1 x2 true metasenv subst)
501 fo_unif test_eq_only metasenv subst
502 (NCicReduction.unwind (k1,e1,t1,List.rev l1))
503 (NCicReduction.unwind (k2,e2,t2,List.rev l2))
505 try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
506 with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
507 unif_machines metasenv subst (small_delta_step m1 m2)
508 (*D*) in outside(); rc with exn -> outside (); raise exn
510 try fo_unif test_eq_only metasenv subst t1 t2
511 with UnificationFailure msg | Uncertain msg as exn ->
513 unif_machines metasenv subst
514 (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
516 | UnificationFailure _ -> raise (UnificationFailure msg)
517 | Uncertain _ -> raise exn
518 (*D*) in outside(); rc with exn -> outside (); raise exn
531 exception UnificationFailure of string Lazy.t;;
532 exception Uncertain of string Lazy.t;;
533 exception AssertFailure of string Lazy.t;;
535 let verbose = false;;
536 let debug_print = fun _ -> ()
538 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
539 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
540 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
541 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
543 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
545 let type_of_aux' metasenv subst context term ugraph =
548 profile.HExtlib.profile
549 (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
551 CicTypeChecker.TypeCheckerFailure msg ->
555 "Kernel Type checking error:
556 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
557 (CicMetaSubst.ppterm ~metasenv subst term)
558 (CicMetaSubst.ppterm ~metasenv [] term)
559 (CicMetaSubst.ppcontext ~metasenv subst context)
560 (CicMetaSubst.ppmetasenv subst metasenv)
561 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
562 raise (AssertFailure msg)
563 | CicTypeChecker.AssertFailure msg ->
566 "Kernel Type checking assertion failure:
567 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
568 (CicMetaSubst.ppterm ~metasenv subst term)
569 (CicMetaSubst.ppterm ~metasenv [] term)
570 (CicMetaSubst.ppcontext ~metasenv subst context)
571 (CicMetaSubst.ppmetasenv subst metasenv)
572 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
573 raise (AssertFailure msg)
574 in profiler_toa.HExtlib.profile foo ()
577 let exists_a_meta l =
581 | Cic.Appl (Cic.Meta _::_) -> true
584 let rec deref subst t =
585 let snd (_,a,_) = a in
590 (CicSubstitution.subst_meta
591 l (snd (CicUtil.lookup_subst n subst)))
593 CicUtil.Subst_not_found _ -> t)
594 | Cic.Appl(Cic.Meta(n,l)::args) ->
595 (match deref subst (Cic.Meta(n,l)) with
596 | Cic.Lambda _ as t ->
597 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
598 | r -> Cic.Appl(r::args))
599 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
600 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
605 let foo () = deref subst t
606 in profiler_deref.HExtlib.profile foo ()
608 exception WrongShape;;
609 let eta_reduce after_beta_expansion after_beta_expansion_body
610 before_beta_expansion
613 match before_beta_expansion,after_beta_expansion_body with
614 Cic.Appl l, Cic.Appl l' ->
615 let rec all_but_last check_last =
619 | [_] -> if check_last then raise WrongShape else []
620 | he::tl -> he::(all_but_last check_last tl)
622 let all_but_last check_last l =
623 match all_but_last check_last l with
628 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
629 let all_but_last = all_but_last false l in
630 (* here we should test alpha-equivalence; however we know by
631 construction that here alpha_equivalence is equivalent to = *)
632 if t = all_but_last then
636 | _,_ -> after_beta_expansion
638 WrongShape -> after_beta_expansion
640 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
641 let module S = CicSubstitution in
642 let module C = Cic in
644 let rec aux metasenv subst n context t' ugraph =
647 let subst,metasenv,ugraph1 =
648 fo_unif_subst test_equality_only subst context metasenv
649 (CicSubstitution.lift n arg) t' ugraph
652 subst,metasenv,C.Rel (1 + n),ugraph1
655 | UnificationFailure _ ->
657 | C.Rel m -> subst,metasenv,
658 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
659 | C.Var (uri,exp_named_subst) ->
660 let subst,metasenv,exp_named_subst',ugraph1 =
661 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
663 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
665 (* andrea: in general, beta_expand can create badly typed
666 terms. This happens quite seldom in practice, UNLESS we
667 iterate on the local context. For this reason, we renounce
668 to iterate and just lift *)
672 Some t -> Some (CicSubstitution.lift 1 t)
674 subst, metasenv, C.Meta (i,l), ugraph
676 | C.Implicit _ as t -> subst,metasenv,t,ugraph
678 let subst,metasenv,te',ugraph1 =
679 aux metasenv subst n context te ugraph in
680 let subst,metasenv,ty',ugraph2 =
681 aux metasenv subst n context ty ugraph1 in
682 (* TASSI: sure this is in serial? *)
683 subst,metasenv,(C.Cast (te', ty')),ugraph2
685 let subst,metasenv,s',ugraph1 =
686 aux metasenv subst n context s ugraph in
687 let subst,metasenv,t',ugraph2 =
688 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
691 (* TASSI: sure this is in serial? *)
692 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
693 | C.Lambda (nn,s,t) ->
694 let subst,metasenv,s',ugraph1 =
695 aux metasenv subst n context s ugraph in
696 let subst,metasenv,t',ugraph2 =
697 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
699 (* TASSI: sure this is in serial? *)
700 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
701 | C.LetIn (nn,s,ty,t) ->
702 let subst,metasenv,s',ugraph1 =
703 aux metasenv subst n context s ugraph in
704 let subst,metasenv,ty',ugraph1 =
705 aux metasenv subst n context ty ugraph in
706 let subst,metasenv,t',ugraph2 =
707 aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
710 (* TASSI: sure this is in serial? *)
711 subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
713 let subst,metasenv,revl',ugraph1 =
715 (fun (subst,metasenv,appl,ugraph) t ->
716 let subst,metasenv,t',ugraph1 =
717 aux metasenv subst n context t ugraph in
718 subst,metasenv,(t'::appl),ugraph1
719 ) (subst,metasenv,[],ugraph) l
721 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
722 | C.Const (uri,exp_named_subst) ->
723 let subst,metasenv,exp_named_subst',ugraph1 =
724 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
726 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
727 | C.MutInd (uri,i,exp_named_subst) ->
728 let subst,metasenv,exp_named_subst',ugraph1 =
729 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
731 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
732 | C.MutConstruct (uri,i,j,exp_named_subst) ->
733 let subst,metasenv,exp_named_subst',ugraph1 =
734 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
736 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
737 | C.MutCase (sp,i,outt,t,pl) ->
738 let subst,metasenv,outt',ugraph1 =
739 aux metasenv subst n context outt ugraph in
740 let subst,metasenv,t',ugraph2 =
741 aux metasenv subst n context t ugraph1 in
742 let subst,metasenv,revpl',ugraph3 =
744 (fun (subst,metasenv,pl,ugraph) t ->
745 let subst,metasenv,t',ugraph1 =
746 aux metasenv subst n context t ugraph in
747 subst,metasenv,(t'::pl),ugraph1
748 ) (subst,metasenv,[],ugraph2) pl
750 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
751 (* TASSI: not sure this is serial *)
753 (*CSC: not implemented
754 let tylen = List.length fl in
757 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
760 C.Fix (i, substitutedfl)
762 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
764 (*CSC: not implemented
765 let tylen = List.length fl in
768 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
771 C.CoFix (i, substitutedfl)
774 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
776 and aux_exp_named_subst metasenv subst n context ens ugraph =
778 (fun (uri,t) (subst,metasenv,l,ugraph) ->
779 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
780 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
782 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
784 FreshNamesGenerator.mk_fresh_name ~subst
785 metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
787 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
788 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
789 subst, metasenv, t'', ugraph2
790 in profiler_beta_expand.HExtlib.profile foo ()
793 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
794 let _,subst,metasenv,hd,ugraph =
796 (fun arg (num,subst,metasenv,t,ugraph) ->
797 let subst,metasenv,t,ugraph1 =
798 beta_expand num test_equality_only
799 metasenv subst context t arg ugraph
801 num+1,subst,metasenv,t,ugraph1
802 ) args (1,subst,metasenv,t,ugraph)
804 subst,metasenv,hd,ugraph
806 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
809 | (m2,_,c2,c2')::_ ->
810 let m1,c1,c1' = carr,to1,to2 in
812 function Some (_,t) -> CicPp.ppterm t
816 ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
817 CoercDb.string_of_carr car2^": " ^
818 CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
819 unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
820 unopt c2^" + "^unopt c2')
822 (* NUOVA UNIFICAZIONE *)
823 (* A substitution is a (int * Cic.term) list that associates a
824 metavariable i with its body.
825 A metaenv is a (int * Cic.term) list that associate a metavariable
827 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
828 a new substitution which is _NOT_ unwinded. It must be unwinded before
831 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
832 let module C = Cic in
833 let module R = CicReduction in
834 let module S = CicSubstitution in
835 let t1 = deref subst t1 in
836 let t2 = deref subst t2 in
837 let (&&&) a b = (a && b) || ((not a) && (not b)) in
838 (* let bef = Sys.time () in *)
840 if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
844 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
845 in profiler_are_convertible.HExtlib.profile foo ()
847 (* let aft = Sys.time () in
848 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
849 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
850 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
852 subst, metasenv, ugraph
855 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
856 let _,subst,metasenv,ugraph1 =
859 (fun (j,subst,metasenv,ugraph) t1 t2 ->
862 | _,None -> j+1,subst,metasenv,ugraph
863 | Some t1', Some t2' ->
864 (* First possibility: restriction *)
865 (* Second possibility: unification *)
866 (* Third possibility: convertibility *)
869 ~subst ~metasenv context t1' t2' ugraph
872 j+1,subst,metasenv, ugraph1
875 let subst,metasenv,ugraph2 =
878 subst context metasenv t1' t2' ugraph
880 j+1,subst,metasenv,ugraph2
883 | UnificationFailure _ ->
884 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
885 let metasenv, subst =
886 CicMetaSubst.restrict
887 subst [(n,j)] metasenv in
888 j+1,subst,metasenv,ugraph1)
889 ) (1,subst,metasenv,ugraph) ln lm
893 (UnificationFailure (lazy "1"))
896 "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."
897 (CicMetaSubst.ppterm ~metasenv subst t1)
898 (CicMetaSubst.ppterm ~metasenv subst t2))) *)
899 | Invalid_argument _ ->
901 (UnificationFailure (lazy "2")))
904 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
905 (CicMetaSubst.ppterm ~metasenv subst t1)
906 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
907 in subst,metasenv,ugraph1
908 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
909 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
911 | (t, C.Meta (n,l)) ->
914 C.Meta (n,_), C.Meta (m,_) when n < m -> false
915 | _, C.Meta _ -> false
918 let lower = fun x y -> if swap then y else x in
919 let upper = fun x y -> if swap then x else y in
920 let fo_unif_subst_ordered
921 test_equality_only subst context metasenv m1 m2 ugraph =
922 fo_unif_subst test_equality_only subst context metasenv
923 (lower m1 m2) (upper m1 m2) ugraph
926 let subst,metasenv,ugraph1 =
927 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
930 type_of_aux' metasenv subst context t ugraph
934 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
936 UnificationFailure _ as e -> raise e
937 | Uncertain msg -> raise (UnificationFailure msg)
939 debug_print (lazy "siamo allo huge hack");
940 (* TODO huge hack!!!!
941 * we keep on unifying/refining in the hope that
942 * the problem will be eventually solved.
943 * In the meantime we're breaking a big invariant:
944 * the terms that we are unifying are no longer well
945 * typed in the current context (in the worst case
946 * we could even diverge) *)
947 (subst, metasenv,ugraph)) in
948 let t',metasenv,subst =
950 CicMetaSubst.delift n subst context metasenv l t
952 (CicMetaSubst.MetaSubstFailure msg)->
953 raise (UnificationFailure msg)
954 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
958 C.Sort (C.Type u) when not test_equality_only ->
959 let u' = CicUniv.fresh () in
960 let s = C.Sort (C.Type u') in
963 CicUniv.add_ge (upper u u') (lower u u') ugraph1
967 CicUniv.UniverseInconsistency msg ->
968 raise (UnificationFailure msg))
971 (* Unifying the types may have already instantiated n. Let's check *)
973 let (_, oldt,_) = CicUtil.lookup_subst n subst in
974 let lifted_oldt = S.subst_meta l oldt in
975 fo_unif_subst_ordered
976 test_equality_only subst context metasenv t lifted_oldt ugraph2
978 CicUtil.Subst_not_found _ ->
979 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
980 let subst = (n, (context, t'',ty)) :: subst in
982 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
983 subst, metasenv, ugraph2
985 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
986 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
987 if UriManager.eq uri1 uri2 then
988 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
989 exp_named_subst1 exp_named_subst2 ugraph
991 raise (UnificationFailure (lazy
993 "Can't unify %s with %s due to different constants"
994 (CicMetaSubst.ppterm ~metasenv subst t1)
995 (CicMetaSubst.ppterm ~metasenv subst t2))))
996 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
997 if UriManager.eq uri1 uri2 && i1 = i2 then
998 fo_unif_subst_exp_named_subst
1000 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
1002 raise (UnificationFailure
1005 "Can't unify %s with %s due to different inductive principles"
1006 (CicMetaSubst.ppterm ~metasenv subst t1)
1007 (CicMetaSubst.ppterm ~metasenv subst t2))))
1008 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
1009 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
1010 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
1011 fo_unif_subst_exp_named_subst
1013 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
1015 raise (UnificationFailure
1018 "Can't unify %s with %s due to different inductive constructors"
1019 (CicMetaSubst.ppterm ~metasenv subst t1)
1020 (CicMetaSubst.ppterm ~metasenv subst t2))))
1021 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
1022 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
1023 subst context metasenv te t2 ugraph
1024 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
1025 subst context metasenv t1 te ugraph
1026 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
1027 let subst',metasenv',ugraph1 =
1028 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
1030 fo_unif_subst test_equality_only
1031 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1032 | (C.LetIn (_,s1,ty1,t1), t2)
1033 | (t2, C.LetIn (_,s1,ty1,t1)) ->
1035 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
1036 | (C.Appl l1, C.Appl l2) ->
1037 (* andrea: this case should be probably rewritten in the
1040 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
1043 (fun (subst,metasenv,ugraph) t1 t2 ->
1045 test_equality_only subst context metasenv t1 t2 ugraph)
1046 (subst,metasenv,ugraph) l1 l2
1047 with (Invalid_argument msg) ->
1048 raise (UnificationFailure (lazy msg)))
1049 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
1050 (* we verify that none of the args is a Meta,
1051 since beta expanding with respoect to a metavariable
1055 let (_,t,_) = CicUtil.lookup_subst i subst in
1056 let lifted = S.subst_meta l t in
1057 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
1060 subst context metasenv reduced t2 ugraph
1061 with CicUtil.Subst_not_found _ -> *)
1062 let subst,metasenv,beta_expanded,ugraph1 =
1064 test_equality_only metasenv subst context t2 args ugraph
1066 fo_unif_subst test_equality_only subst context metasenv
1067 (C.Meta (i,l)) beta_expanded ugraph1
1068 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
1070 let (_,t,_) = CicUtil.lookup_subst i subst in
1071 let lifted = S.subst_meta l t in
1072 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
1075 subst context metasenv t1 reduced ugraph
1076 with CicUtil.Subst_not_found _ -> *)
1077 let subst,metasenv,beta_expanded,ugraph1 =
1080 metasenv subst context t1 args ugraph
1082 fo_unif_subst test_equality_only subst context metasenv
1083 (C.Meta (i,l)) beta_expanded ugraph1
1085 let lr1 = List.rev l1 in
1086 let lr2 = List.rev l2 in
1088 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
1091 | _,[] -> assert false
1094 test_equality_only subst context metasenv h1 h2 ugraph
1097 fo_unif_subst test_equality_only subst context metasenv
1098 h (C.Appl (List.rev l)) ugraph
1099 | ((h1::l1),(h2::l2)) ->
1100 let subst', metasenv',ugraph1 =
1103 subst context metasenv h1 h2 ugraph
1106 test_equality_only subst' metasenv' (l1,l2) ugraph1
1110 test_equality_only subst metasenv (lr1, lr2) ugraph
1112 | UnificationFailure s
1113 | Uncertain s as exn ->
1116 | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
1117 (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
1118 CoercDb.is_a_coercion cc1 <> None &&
1119 CoercDb.is_a_coercion cc2 <> None &&
1120 not (UriManager.eq uri1 uri2) ->
1122 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1124 let inner_coerced t =
1125 let t = CicMetaSubst.apply_subst subst t in
1129 (match CoercGraph.coerced_arg l with
1131 | Some (t,_) -> aux (List.hd l) t t)
1134 aux (Cic.Implicit None) (Cic.Implicit None) t
1136 let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
1137 let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
1140 CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
1142 | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
1145 let head1_c, head2_c =
1147 CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
1149 | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
1152 let unfold uri ens args =
1154 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
1158 | Cic.Constant (_,Some bo,_,_,_) ->
1159 CicReduction.head_beta_reduce ~delta:false
1160 (Cic.Appl (bo::args))
1163 let conclude subst metasenv ugraph last_tl1' last_tl2' =
1164 let subst',metasenv,ugraph =
1167 ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
1168 " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
1170 fo_unif_subst test_equality_only subst context
1171 metasenv last_tl1' last_tl2' ugraph
1173 if subst = subst' then raise exn
1176 let subst,metasenv,ugrph as res =
1178 fo_unif_subst test_equality_only subst' context
1179 metasenv (C.Appl l1) (C.Appl l2) ugraph
1183 (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
1184 " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1188 if CoercDb.eq_carr car1 car2 then
1189 match last_tl1,last_tl2 with
1190 | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
1193 let subst,metasenv,ugraph =
1194 fo_unif_subst test_equality_only subst context
1195 metasenv last_tl1 last_tl2 ugraph
1197 fo_unif_subst test_equality_only subst context
1198 metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
1199 | _ when CoercDb.eq_carr head1_c head2_c ->
1200 (* composite VS composition + metas avoiding
1201 * coercions not only in coerced position *)
1202 if c1 <> cc1 && c2 <> cc2 then
1203 conclude subst metasenv ugraph
1208 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
1210 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
1212 fo_unif_subst test_equality_only subst context
1213 metasenv l1 l2 ugraph
1217 match last_tl1 with Cic.Meta _ -> true | _ -> false in
1219 match last_tl2 with Cic.Meta _ -> true | _ -> false in
1220 if not (grow1 || grow2) then
1221 (* no flexible terminals -> no pullback, but
1222 * we still unify them, in some cases it helps *)
1223 conclude subst metasenv ugraph last_tl1 last_tl2
1227 metasenv subst context (grow1,car1) (grow2,car2)
1231 | (carr,metasenv,to1,to2)::xxx ->
1232 warn_if_not_unique xxx to1 to2 carr car1 car2;
1233 let last_tl1',(subst,metasenv,ugraph) =
1234 match grow1,to1 with
1235 | true,Some (last,coerced) ->
1237 fo_unif_subst test_equality_only subst context
1238 metasenv coerced last_tl1 ugraph
1239 | _ -> last_tl1,(subst,metasenv,ugraph)
1241 let last_tl2',(subst,metasenv,ugraph) =
1242 match grow2,to2 with
1243 | true,Some (last,coerced) ->
1245 fo_unif_subst test_equality_only subst context
1246 metasenv coerced last_tl2 ugraph
1247 | _ -> last_tl2,(subst,metasenv,ugraph)
1249 conclude subst metasenv ugraph last_tl1' last_tl2')
1251 (* {{{ CSC: This is necessary because of the "elim H" tactic
1252 where the type of H is only reducible to an
1253 inductive type. This could be extended from inductive
1254 types to any rigid term. However, the code is
1255 duplicated in two places: inside applications and
1256 outside them. Probably it would be better to
1257 work with lambda-bar terms instead. *)
1258 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
1259 | (_, Cic.MutInd _::_) ->
1260 let t1' = R.whd ~subst context t1 in
1262 C.Appl (C.MutInd _::_) ->
1263 fo_unif_subst test_equality_only
1264 subst context metasenv t1' t2 ugraph
1265 | _ -> raise (UnificationFailure (lazy "88")))
1266 | (Cic.MutInd _::_,_) ->
1267 let t2' = R.whd ~subst context t2 in
1269 C.Appl (C.MutInd _::_) ->
1270 fo_unif_subst test_equality_only
1271 subst context metasenv t1 t2' ugraph
1274 (lazy ("not a mutind :"^
1275 CicMetaSubst.ppterm ~metasenv subst t2 ))))
1278 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
1279 let subst', metasenv',ugraph1 =
1280 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
1282 let subst'',metasenv'',ugraph2 =
1283 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
1287 (fun (subst,metasenv,ugraph) t1 t2 ->
1289 test_equality_only subst context metasenv t1 t2 ugraph
1290 ) (subst'',metasenv'',ugraph2) pl1 pl2
1292 Invalid_argument _ ->
1293 raise (UnificationFailure (lazy "6.1")))
1295 "Error trying to unify %s with %s: the number of branches is not the same."
1296 (CicMetaSubst.ppterm ~metasenv subst t1)
1297 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
1298 | (C.Rel _, _) | (_, C.Rel _) ->
1300 subst, metasenv,ugraph
1302 raise (UnificationFailure (lazy
1304 "Can't unify %s with %s because they are not convertible"
1305 (CicMetaSubst.ppterm ~metasenv subst t1)
1306 (CicMetaSubst.ppterm ~metasenv subst t2))))
1307 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
1308 let subst,metasenv,beta_expanded,ugraph1 =
1310 test_equality_only metasenv subst context t2 args ugraph
1312 fo_unif_subst test_equality_only subst context metasenv
1313 (C.Meta (i,l)) beta_expanded ugraph1
1314 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
1315 let subst,metasenv,beta_expanded,ugraph1 =
1317 test_equality_only metasenv subst context t1 args ugraph
1319 fo_unif_subst test_equality_only subst context metasenv
1320 beta_expanded (C.Meta (i,l)) ugraph1
1321 (* Works iff there are no arguments applied to it; similar to the
1323 | (_, C.MutInd _) ->
1324 let t1' = R.whd ~subst context t1 in
1327 fo_unif_subst test_equality_only
1328 subst context metasenv t1' t2 ugraph
1329 | _ -> raise (UnificationFailure (lazy "8")))
1331 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
1332 let subst',metasenv',ugraph1 =
1333 fo_unif_subst true subst context metasenv s1 s2 ugraph
1335 fo_unif_subst test_equality_only
1336 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1338 (match CicReduction.whd ~subst context t2 with
1340 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1341 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
1343 (match CicReduction.whd ~subst context t1 with
1345 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1346 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
1348 (* delta-beta reduction should almost never be a problem for
1350 1. long computations require iota reduction
1351 2. it is extremely rare that a close term t1 (that could be unified
1352 to t2) beta-delta reduces to t1' while t2 does not beta-delta
1353 reduces in the same way. This happens only if one meta of t2
1354 occurs in head position during beta reduction. In this unluky
1355 case too much reduction will be performed on t1 and unification
1356 will surely fail. *)
1357 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
1358 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
1359 if t1 = t1' && t2 = t2' then
1360 raise (UnificationFailure
1363 "Can't unify %s with %s because they are not convertible"
1364 (CicMetaSubst.ppterm ~metasenv subst t1)
1365 (CicMetaSubst.ppterm ~metasenv subst t2))))
1368 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
1370 UnificationFailure _
1372 raise (UnificationFailure
1375 "Can't unify %s with %s because they are not convertible"
1376 (CicMetaSubst.ppterm ~metasenv subst t1)
1377 (CicMetaSubst.ppterm ~metasenv subst t2))))
1379 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
1380 exp_named_subst1 exp_named_subst2 ugraph
1384 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
1385 assert (uri1=uri2) ;
1386 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1387 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
1389 Invalid_argument _ ->
1394 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
1397 raise (UnificationFailure (lazy (sprintf
1398 "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))))
1400 (* A substitution is a (int * Cic.term) list that associates a *)
1401 (* metavariable i with its body. *)
1402 (* metasenv is of type Cic.metasenv *)
1403 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
1404 (* a new substitution which is already unwinded and ready to be applied and *)
1405 (* a new metasenv in which some hypothesis in the contexts of the *)
1406 (* metavariables may have been restricted. *)
1407 let fo_unif metasenv context t1 t2 ugraph =
1408 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
1410 let enrich_msg msg subst context metasenv t1 t2 ugraph =
1413 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"
1414 (CicMetaSubst.ppterm ~metasenv subst t1)
1416 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1419 | UnificationFailure s
1421 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1422 (CicMetaSubst.ppterm ~metasenv subst t2)
1424 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1427 | UnificationFailure s
1429 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1430 (CicMetaSubst.ppcontext ~metasenv subst context)
1431 (CicMetaSubst.ppmetasenv subst metasenv)
1432 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
1434 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
1435 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
1437 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1438 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
1440 | UnificationFailure s
1442 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1443 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
1445 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1446 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
1448 | UnificationFailure s
1450 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1451 (CicMetaSubst.ppcontext ~metasenv subst context)
1452 (CicMetaSubst.ppmetasenv subst metasenv)
1456 let fo_unif_subst subst context metasenv t1 t2 ugraph =
1458 fo_unif_subst false subst context metasenv t1 t2 ugraph
1460 | AssertFailure msg ->
1461 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1462 | UnificationFailure msg ->
1463 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))