2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
14 exception UnificationFailure of string Lazy.t;;
15 exception Uncertain of string Lazy.t;;
16 exception AssertFailure of string Lazy.t;;
18 let (===) x y = Pervasives.compare x y = 0 ;;
20 let uncert_exc metasenv subst context t1 t2 =
22 "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
23 " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
26 let fail_exc metasenv subst context t1 t2 =
27 UnificationFailure (lazy (
28 "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
29 " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
34 | NCic.Appl l -> NCic.Appl (l@tl)
35 | _ -> NCic.Appl (hd :: tl)
42 | NCic.Appl (NCic.Meta _::_) -> true
46 exception WrongShape;;
49 let delift_if_not_occur body orig =
51 NCicSubstitution.psubst ~avoid_beta_redexes:true
52 (fun () -> raise WrongShape) [()] body
53 with WrongShape -> orig
56 | NCic.Lambda(_, _, NCic.Appl [hd; NCic.Rel 1]) as orig ->
57 delift_if_not_occur hd orig
58 | NCic.Lambda(_, _, NCic.Appl (hd :: l)) as orig
59 when HExtlib.list_last l = NCic.Rel 1 ->
61 let args, _ = HExtlib.split_nth (List.length l - 1) l in
64 delift_if_not_occur body orig
69 module Ref = NReference;;
72 let inside c = indent := !indent ^ String.make 1 c;;
73 let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
77 prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ s);;
82 let rec beta_expand num test_eq_only swap metasenv subst context t arg =
83 let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
87 unify test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
89 unify test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
91 (metasenv, subst), NCic.Rel (1 + n)
92 with Uncertain _ | UnificationFailure _ ->
94 | NCic.Rel m as orig ->
95 (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
96 (* andrea: in general, beta_expand can create badly typed
97 terms. This happens quite seldom in practice, UNLESS we
98 iterate on the local context. For this reason, we renounce
99 to iterate and just lift *)
100 | NCic.Meta (i,(shift,lc)) ->
101 (metasenv,subst), NCic.Meta (i,(shift+1,lc))
102 | NCic.Prod (name, src, tgt) as orig ->
103 let (metasenv, subst), src1 = aux (n,context,true) acc src in
104 let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
105 let ms, tgt1 = aux k (metasenv, subst) tgt in
106 if src == src1 && tgt == tgt1 then ms, orig else
107 ms, NCic.Prod (name, src1, tgt1)
109 NCicUntrusted.map_term_fold_a
110 (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t
113 let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
114 let fresh_name = "Hbeta" ^ string_of_int num in
115 let (metasenv,subst), t1 =
116 aux (0, context, test_eq_only) (metasenv, subst) t in
117 let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in
119 ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
121 with NCicTypeChecker.TypeCheckerFailure _ ->
122 metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
124 and beta_expand_many test_equality_only swap metasenv subst context t args =
125 (*D*) inside 'B'; try let rc =
126 pp (String.concat ", " (List.map (NCicPp.ppterm ~metasenv ~subst ~context)
127 args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t);
128 let _, subst, metasenv, hd =
130 (fun arg (num,subst,metasenv,t) ->
131 let metasenv, subst, t =
132 beta_expand num test_equality_only swap metasenv subst context t arg
134 num+1,subst,metasenv,t)
135 args (1,subst,metasenv,t)
137 pp ("Head syntesized by b-exp: " ^
138 NCicPp.ppterm ~metasenv ~subst ~context hd);
140 (*D*) in outside (); rc with exn -> outside (); raise exn
142 and instantiate test_eq_only metasenv subst context n lc t swap =
143 (*D*) inside 'I'; try let rc =
144 let unify test_eq_only m s c t1 t2 =
145 if swap then unify test_eq_only m s c t2 t1
146 else unify test_eq_only m s c t1 t2
149 try NCicTypeChecker.typeof ~subst ~metasenv context t
150 with NCicTypeChecker.TypeCheckerFailure msg ->
151 prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
152 prerr_endline (Lazy.force msg);
155 let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
156 let lty = NCicSubstitution.subst_meta lc ty in
157 pp ("On the types: " ^ NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
158 ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t);
159 let metasenv, subst = unify test_eq_only metasenv subst context lty ty_t in
160 let (metasenv, subst), t =
161 try NCicMetaSubst.delift metasenv subst context n lc t
162 with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg)
163 | NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg)
165 (* Unifying the types may have already instantiated n. *)
167 let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
168 let oldt = NCicSubstitution.subst_meta lc oldt in
169 (* conjecture: always fail --> occur check *)
170 unify test_eq_only metasenv subst context oldt t
171 with NCicUtils.Subst_not_found _ ->
172 (* by cumulativity when unify(?,Type_i)
173 * we could ? := Type_j with j <= i... *)
174 let subst = (n, (name, ctx, t, ty)) :: subst in
176 List.filter (fun (m,_) -> not (n = m)) metasenv
179 (*D*) in outside(); rc with exn -> outside (); raise exn
181 and unify test_eq_only metasenv subst context t1 t2 =
182 (*D*) inside 'U'; try let rc =
183 let fo_unif test_eq_only metasenv subst t1 t2 =
184 (*D*) inside 'F'; try let rc =
185 pp (" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^
186 NCicPp.ppterm ~metasenv ~subst ~context t2);
191 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
192 if NCicEnvironment.universe_leq a b then metasenv, subst
193 else raise (fail_exc metasenv subst context t1 t2)
194 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
195 if NCicEnvironment.universe_eq a b then metasenv, subst
196 else raise (fail_exc metasenv subst context t1 t2)
197 | (C.Sort C.Prop,C.Sort (C.Type _)) ->
198 if (not test_eq_only) then metasenv, subst
199 else raise (fail_exc metasenv subst context t1 t2)
201 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
202 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
203 let metasenv, subst = unify true metasenv subst context s1 s2 in
204 unify test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
205 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
206 let metasenv,subst=unify test_eq_only metasenv subst context ty1 ty2 in
207 let metasenv,subst=unify test_eq_only metasenv subst context s1 s2 in
208 let context = (name1, C.Def (s1,ty1))::context in
209 unify test_eq_only metasenv subst context t1 t2
211 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
213 let l1 = NCicUtils.expand_local_context l1 in
214 let l2 = NCicUtils.expand_local_context l2 in
215 let metasenv, subst, to_restrict, _ =
217 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
219 let metasenv, subst =
220 unify test_eq_only metasenv subst context
221 (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
223 metasenv, subst, to_restrict, i-1
224 with UnificationFailure _ | Uncertain _ ->
225 metasenv, subst, i::to_restrict, i-1)
226 l1 l2 (metasenv, subst, [], List.length l1)
228 let metasenv, subst, _ =
229 NCicMetaSubst.restrict metasenv subst n1 to_restrict
233 | Invalid_argument _ -> assert false
234 | NCicMetaSubst.MetaSubstFailure msg ->
236 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
237 let term1 = NCicSubstitution.subst_meta lc1 term in
238 let term2 = NCicSubstitution.subst_meta lc2 term in
239 unify test_eq_only metasenv subst context term1 term2
240 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
242 | C.Meta (n,lc), t ->
244 let _,_,term,_ = NCicUtils.lookup_subst n subst in
245 let term = NCicSubstitution.subst_meta lc term in
246 unify test_eq_only metasenv subst context term t
247 with NCicUtils.Subst_not_found _->
248 instantiate test_eq_only metasenv subst context n lc t false)
250 | t, C.Meta (n,lc) ->
252 let _,_,term,_ = NCicUtils.lookup_subst n subst in
253 let term = NCicSubstitution.subst_meta lc term in
254 unify test_eq_only metasenv subst context t term
255 with NCicUtils.Subst_not_found _->
256 instantiate test_eq_only metasenv subst context n lc t true)
258 | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
259 let _,_,term,_ = NCicUtils.lookup_subst i subst in
260 let term = NCicSubstitution.subst_meta l term in
261 unify test_eq_only metasenv subst context (mk_appl term args) t2
263 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
264 let _,_,term,_ = NCicUtils.lookup_subst i subst in
265 let term = NCicSubstitution.subst_meta l term in
266 unify test_eq_only metasenv subst context t1 (mk_appl term args)
268 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
269 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
272 (fun (metasenv, subst) t1 t2 ->
273 unify test_eq_only metasenv subst context t1 t2)
274 (metasenv,subst) l1 l2
275 with Invalid_argument _ ->
276 raise (fail_exc metasenv subst context t1 t2))
278 | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
279 (* we verify that none of the args is a Meta,
280 since beta expanding w.r.t a metavariable makes no sense *)
281 let metasenv, subst, beta_expanded =
284 metasenv subst context t2 args
286 unify test_eq_only metasenv subst context
287 (C.Meta (i,l)) beta_expanded
289 | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
290 let metasenv, subst, beta_expanded =
293 metasenv subst context t1 args
295 unify test_eq_only metasenv subst context
296 beta_expanded (C.Meta (i,l))
298 (* processing this case here we avoid a useless small delta step *)
299 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
301 let relevance = NCicEnvironment.get_relevance r1 in
302 let relevance = match r1 with
303 | Ref.Ref (_,Ref.Con (_,_,lno)) ->
304 let _,relevance = HExtlib.split_nth lno relevance in
305 HExtlib.mk_list false lno @ relevance
308 let metasenv, subst, _ =
311 (fun (metasenv, subst, relevance) t1 t2 ->
313 match relevance with b::tl -> b,tl | _ -> true, [] in
314 let metasenv, subst =
315 try unify test_eq_only metasenv subst context t1 t2
316 with UnificationFailure _ | Uncertain _ when not b ->
319 metasenv, subst, relevance)
320 (metasenv, subst, relevance) tl1 tl2
321 with Invalid_argument _ ->
322 raise (uncert_exc metasenv subst context t1 t2)
326 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
327 C.Match (ref2,outtype2,term2,pl2)) ->
328 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
329 let _,_,ty,_ = List.nth itl tyno in
330 let rec remove_prods ~subst context ty =
331 let ty = NCicReduction.whd ~subst context ty in
334 | C.Prod (name,so,ta) ->
335 remove_prods ~subst ((name,(C.Decl so))::context) ta
339 match remove_prods ~subst [] ty with
340 | C.Sort C.Prop -> true
343 let rec remove_prods ~subst context ty =
344 let ty = NCicReduction.whd ~subst context ty in
347 | C.Prod (name,so,ta) ->
348 remove_prods ~subst ((name,(C.Decl so))::context) ta
351 if not (Ref.eq ref1 ref2) then
352 raise (uncert_exc metasenv subst context t1 t2)
354 let metasenv, subst =
355 unify test_eq_only metasenv subst context outtype1 outtype2 in
356 let metasenv, subst =
357 try unify test_eq_only metasenv subst context term1 term2
358 with UnificationFailure _ | Uncertain _ when is_prop ->
363 (fun (metasenv,subst) ->
364 unify test_eq_only metasenv subst context)
365 (metasenv, subst) pl1 pl2
366 with Invalid_argument _ ->
367 raise (uncert_exc metasenv subst context t1 t2))
368 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
369 | _ -> raise (uncert_exc metasenv subst context t1 t2)
370 (*D*) in outside(); rc with exn -> outside (); raise exn
372 let height_of = function
373 | NCic.Const (Ref.Ref (_,Ref.Def h))
374 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
375 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
376 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
379 let put_in_whd m1 m2 =
380 NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
381 NCicReduction.reduce_machine ~delta:max_int ~subst context m2,
382 false (* not in normal form *)
384 let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
385 let h1 = height_of t1 in
386 let h2 = height_of t2 in
388 if flexible [t1] then max 0 (h2 - 1) else
389 if flexible [t2] then max 0 (h1 - 1) else
390 if h1 = h2 then max 0 (h1 -1) else min h1 h2
392 pp ("DELTA STEP TO: " ^ string_of_int delta);
393 let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in
394 let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in
395 if (m1' == m1 && m2' == m2 && delta > 0) then
396 (* if we have as heads a Fix of height n>m>0 and another term of height
397 * m, we set delta = m. The Fix may or may not reduce, depending on its
398 * rec argument. if no reduction was performed we decrease delta to m-1
399 * to reduce the other term *)
400 let delta = delta - 1 in
401 pp ("DELTA STEP TO: " ^ string_of_int delta);
402 let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in
403 let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in
404 m1', m2', (m1 == m1' && m2 == m2') || delta = 0
405 else m1', m2', delta = 0
407 let rec unif_machines metasenv subst =
409 | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),are_normal) ->
410 (*D*) inside 'M'; try let rc =
411 pp ((if are_normal then "*" else " ") ^ " " ^
412 NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
414 NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2));
415 let relevance = [] (* TO BE UNDERSTOOD
417 | C.Const r -> NCicEnvironment.get_relevance r
419 let unif_from_stack t1 t2 b metasenv subst =
421 let t1 = NCicReduction.from_stack t1 in
422 let t2 = NCicReduction.from_stack t2 in
423 unif_machines metasenv subst (put_in_whd t1 t2)
424 with UnificationFailure _ | Uncertain _ when not b ->
427 let rec check_stack l1 l2 r (metasenv, subst) =
429 | x1::tl1, x2::tl2, r::tr ->
430 check_stack tl1 tl2 tr
431 (unif_from_stack x1 x2 r metasenv subst)
432 | x1::tl1, x2::tl2, [] ->
433 check_stack tl1 tl2 []
434 (unif_from_stack x1 x2 true metasenv subst)
436 fo_unif test_eq_only metasenv subst
437 (NCicReduction.unwind (k1,e1,t1,List.rev l1))
438 (NCicReduction.unwind (k2,e2,t2,List.rev l2))
440 try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
441 with UnificationFailure _ | Uncertain _ when not are_normal ->
443 let delta = delta - 1 in
444 let red = NCicReduction.reduce_machine ~delta ~subst context in
446 unif_machines metasenv subst (small_delta_step m1 m2)
447 (*D*) in outside(); rc with exn -> outside (); raise exn
449 try fo_unif test_eq_only metasenv subst t1 t2
450 with UnificationFailure msg | Uncertain msg as exn ->
452 unif_machines metasenv subst
453 (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
455 | UnificationFailure _ -> raise (UnificationFailure msg)
456 | Uncertain _ -> raise exn
457 (*D*) in outside(); rc with exn -> outside (); raise exn
470 exception UnificationFailure of string Lazy.t;;
471 exception Uncertain of string Lazy.t;;
472 exception AssertFailure of string Lazy.t;;
474 let verbose = false;;
475 let debug_print = fun _ -> ()
477 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
478 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
479 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
480 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
482 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
484 let type_of_aux' metasenv subst context term ugraph =
487 profile.HExtlib.profile
488 (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
490 CicTypeChecker.TypeCheckerFailure msg ->
494 "Kernel Type checking error:
495 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
496 (CicMetaSubst.ppterm ~metasenv subst term)
497 (CicMetaSubst.ppterm ~metasenv [] term)
498 (CicMetaSubst.ppcontext ~metasenv subst context)
499 (CicMetaSubst.ppmetasenv subst metasenv)
500 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
501 raise (AssertFailure msg)
502 | CicTypeChecker.AssertFailure msg ->
505 "Kernel Type checking assertion failure:
506 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
507 (CicMetaSubst.ppterm ~metasenv subst term)
508 (CicMetaSubst.ppterm ~metasenv [] term)
509 (CicMetaSubst.ppcontext ~metasenv subst context)
510 (CicMetaSubst.ppmetasenv subst metasenv)
511 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
512 raise (AssertFailure msg)
513 in profiler_toa.HExtlib.profile foo ()
516 let exists_a_meta l =
520 | Cic.Appl (Cic.Meta _::_) -> true
523 let rec deref subst t =
524 let snd (_,a,_) = a in
529 (CicSubstitution.subst_meta
530 l (snd (CicUtil.lookup_subst n subst)))
532 CicUtil.Subst_not_found _ -> t)
533 | Cic.Appl(Cic.Meta(n,l)::args) ->
534 (match deref subst (Cic.Meta(n,l)) with
535 | Cic.Lambda _ as t ->
536 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
537 | r -> Cic.Appl(r::args))
538 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
539 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
544 let foo () = deref subst t
545 in profiler_deref.HExtlib.profile foo ()
547 exception WrongShape;;
548 let eta_reduce after_beta_expansion after_beta_expansion_body
549 before_beta_expansion
552 match before_beta_expansion,after_beta_expansion_body with
553 Cic.Appl l, Cic.Appl l' ->
554 let rec all_but_last check_last =
558 | [_] -> if check_last then raise WrongShape else []
559 | he::tl -> he::(all_but_last check_last tl)
561 let all_but_last check_last l =
562 match all_but_last check_last l with
567 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
568 let all_but_last = all_but_last false l in
569 (* here we should test alpha-equivalence; however we know by
570 construction that here alpha_equivalence is equivalent to = *)
571 if t = all_but_last then
575 | _,_ -> after_beta_expansion
577 WrongShape -> after_beta_expansion
579 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
580 let module S = CicSubstitution in
581 let module C = Cic in
583 let rec aux metasenv subst n context t' ugraph =
586 let subst,metasenv,ugraph1 =
587 fo_unif_subst test_equality_only subst context metasenv
588 (CicSubstitution.lift n arg) t' ugraph
591 subst,metasenv,C.Rel (1 + n),ugraph1
594 | UnificationFailure _ ->
596 | C.Rel m -> subst,metasenv,
597 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
598 | C.Var (uri,exp_named_subst) ->
599 let subst,metasenv,exp_named_subst',ugraph1 =
600 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
602 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
604 (* andrea: in general, beta_expand can create badly typed
605 terms. This happens quite seldom in practice, UNLESS we
606 iterate on the local context. For this reason, we renounce
607 to iterate and just lift *)
611 Some t -> Some (CicSubstitution.lift 1 t)
613 subst, metasenv, C.Meta (i,l), ugraph
615 | C.Implicit _ as t -> subst,metasenv,t,ugraph
617 let subst,metasenv,te',ugraph1 =
618 aux metasenv subst n context te ugraph in
619 let subst,metasenv,ty',ugraph2 =
620 aux metasenv subst n context ty ugraph1 in
621 (* TASSI: sure this is in serial? *)
622 subst,metasenv,(C.Cast (te', ty')),ugraph2
624 let subst,metasenv,s',ugraph1 =
625 aux metasenv subst n context s ugraph in
626 let subst,metasenv,t',ugraph2 =
627 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
630 (* TASSI: sure this is in serial? *)
631 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
632 | C.Lambda (nn,s,t) ->
633 let subst,metasenv,s',ugraph1 =
634 aux metasenv subst n context s ugraph in
635 let subst,metasenv,t',ugraph2 =
636 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
638 (* TASSI: sure this is in serial? *)
639 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
640 | C.LetIn (nn,s,ty,t) ->
641 let subst,metasenv,s',ugraph1 =
642 aux metasenv subst n context s ugraph in
643 let subst,metasenv,ty',ugraph1 =
644 aux metasenv subst n context ty ugraph in
645 let subst,metasenv,t',ugraph2 =
646 aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
649 (* TASSI: sure this is in serial? *)
650 subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
652 let subst,metasenv,revl',ugraph1 =
654 (fun (subst,metasenv,appl,ugraph) t ->
655 let subst,metasenv,t',ugraph1 =
656 aux metasenv subst n context t ugraph in
657 subst,metasenv,(t'::appl),ugraph1
658 ) (subst,metasenv,[],ugraph) l
660 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
661 | C.Const (uri,exp_named_subst) ->
662 let subst,metasenv,exp_named_subst',ugraph1 =
663 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
665 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
666 | C.MutInd (uri,i,exp_named_subst) ->
667 let subst,metasenv,exp_named_subst',ugraph1 =
668 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
670 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
671 | C.MutConstruct (uri,i,j,exp_named_subst) ->
672 let subst,metasenv,exp_named_subst',ugraph1 =
673 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
675 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
676 | C.MutCase (sp,i,outt,t,pl) ->
677 let subst,metasenv,outt',ugraph1 =
678 aux metasenv subst n context outt ugraph in
679 let subst,metasenv,t',ugraph2 =
680 aux metasenv subst n context t ugraph1 in
681 let subst,metasenv,revpl',ugraph3 =
683 (fun (subst,metasenv,pl,ugraph) t ->
684 let subst,metasenv,t',ugraph1 =
685 aux metasenv subst n context t ugraph in
686 subst,metasenv,(t'::pl),ugraph1
687 ) (subst,metasenv,[],ugraph2) pl
689 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
690 (* TASSI: not sure this is serial *)
692 (*CSC: not implemented
693 let tylen = List.length fl in
696 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
699 C.Fix (i, substitutedfl)
701 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
703 (*CSC: not implemented
704 let tylen = List.length fl in
707 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
710 C.CoFix (i, substitutedfl)
713 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
715 and aux_exp_named_subst metasenv subst n context ens ugraph =
717 (fun (uri,t) (subst,metasenv,l,ugraph) ->
718 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
719 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
721 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
723 FreshNamesGenerator.mk_fresh_name ~subst
724 metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
726 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
727 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
728 subst, metasenv, t'', ugraph2
729 in profiler_beta_expand.HExtlib.profile foo ()
732 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
733 let _,subst,metasenv,hd,ugraph =
735 (fun arg (num,subst,metasenv,t,ugraph) ->
736 let subst,metasenv,t,ugraph1 =
737 beta_expand num test_equality_only
738 metasenv subst context t arg ugraph
740 num+1,subst,metasenv,t,ugraph1
741 ) args (1,subst,metasenv,t,ugraph)
743 subst,metasenv,hd,ugraph
745 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
748 | (m2,_,c2,c2')::_ ->
749 let m1,c1,c1' = carr,to1,to2 in
751 function Some (_,t) -> CicPp.ppterm t
755 ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
756 CoercDb.string_of_carr car2^": " ^
757 CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
758 unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
759 unopt c2^" + "^unopt c2')
761 (* NUOVA UNIFICAZIONE *)
762 (* A substitution is a (int * Cic.term) list that associates a
763 metavariable i with its body.
764 A metaenv is a (int * Cic.term) list that associate a metavariable
766 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
767 a new substitution which is _NOT_ unwinded. It must be unwinded before
770 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
771 let module C = Cic in
772 let module R = CicReduction in
773 let module S = CicSubstitution in
774 let t1 = deref subst t1 in
775 let t2 = deref subst t2 in
776 let (&&&) a b = (a && b) || ((not a) && (not b)) in
777 (* let bef = Sys.time () in *)
779 if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
783 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
784 in profiler_are_convertible.HExtlib.profile foo ()
786 (* let aft = Sys.time () in
787 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
788 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
789 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
791 subst, metasenv, ugraph
794 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
795 let _,subst,metasenv,ugraph1 =
798 (fun (j,subst,metasenv,ugraph) t1 t2 ->
801 | _,None -> j+1,subst,metasenv,ugraph
802 | Some t1', Some t2' ->
803 (* First possibility: restriction *)
804 (* Second possibility: unification *)
805 (* Third possibility: convertibility *)
808 ~subst ~metasenv context t1' t2' ugraph
811 j+1,subst,metasenv, ugraph1
814 let subst,metasenv,ugraph2 =
817 subst context metasenv t1' t2' ugraph
819 j+1,subst,metasenv,ugraph2
822 | UnificationFailure _ ->
823 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
824 let metasenv, subst =
825 CicMetaSubst.restrict
826 subst [(n,j)] metasenv in
827 j+1,subst,metasenv,ugraph1)
828 ) (1,subst,metasenv,ugraph) ln lm
832 (UnificationFailure (lazy "1"))
835 "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."
836 (CicMetaSubst.ppterm ~metasenv subst t1)
837 (CicMetaSubst.ppterm ~metasenv subst t2))) *)
838 | Invalid_argument _ ->
840 (UnificationFailure (lazy "2")))
843 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
844 (CicMetaSubst.ppterm ~metasenv subst t1)
845 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
846 in subst,metasenv,ugraph1
847 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
848 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
850 | (t, C.Meta (n,l)) ->
853 C.Meta (n,_), C.Meta (m,_) when n < m -> false
854 | _, C.Meta _ -> false
857 let lower = fun x y -> if swap then y else x in
858 let upper = fun x y -> if swap then x else y in
859 let fo_unif_subst_ordered
860 test_equality_only subst context metasenv m1 m2 ugraph =
861 fo_unif_subst test_equality_only subst context metasenv
862 (lower m1 m2) (upper m1 m2) ugraph
865 let subst,metasenv,ugraph1 =
866 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
869 type_of_aux' metasenv subst context t ugraph
873 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
875 UnificationFailure _ as e -> raise e
876 | Uncertain msg -> raise (UnificationFailure msg)
878 debug_print (lazy "siamo allo huge hack");
879 (* TODO huge hack!!!!
880 * we keep on unifying/refining in the hope that
881 * the problem will be eventually solved.
882 * In the meantime we're breaking a big invariant:
883 * the terms that we are unifying are no longer well
884 * typed in the current context (in the worst case
885 * we could even diverge) *)
886 (subst, metasenv,ugraph)) in
887 let t',metasenv,subst =
889 CicMetaSubst.delift n subst context metasenv l t
891 (CicMetaSubst.MetaSubstFailure msg)->
892 raise (UnificationFailure msg)
893 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
897 C.Sort (C.Type u) when not test_equality_only ->
898 let u' = CicUniv.fresh () in
899 let s = C.Sort (C.Type u') in
902 CicUniv.add_ge (upper u u') (lower u u') ugraph1
906 CicUniv.UniverseInconsistency msg ->
907 raise (UnificationFailure msg))
910 (* Unifying the types may have already instantiated n. Let's check *)
912 let (_, oldt,_) = CicUtil.lookup_subst n subst in
913 let lifted_oldt = S.subst_meta l oldt in
914 fo_unif_subst_ordered
915 test_equality_only subst context metasenv t lifted_oldt ugraph2
917 CicUtil.Subst_not_found _ ->
918 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
919 let subst = (n, (context, t'',ty)) :: subst in
921 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
922 subst, metasenv, ugraph2
924 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
925 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
926 if UriManager.eq uri1 uri2 then
927 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
928 exp_named_subst1 exp_named_subst2 ugraph
930 raise (UnificationFailure (lazy
932 "Can't unify %s with %s due to different constants"
933 (CicMetaSubst.ppterm ~metasenv subst t1)
934 (CicMetaSubst.ppterm ~metasenv subst t2))))
935 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
936 if UriManager.eq uri1 uri2 && i1 = i2 then
937 fo_unif_subst_exp_named_subst
939 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
941 raise (UnificationFailure
944 "Can't unify %s with %s due to different inductive principles"
945 (CicMetaSubst.ppterm ~metasenv subst t1)
946 (CicMetaSubst.ppterm ~metasenv subst t2))))
947 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
948 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
949 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
950 fo_unif_subst_exp_named_subst
952 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
954 raise (UnificationFailure
957 "Can't unify %s with %s due to different inductive constructors"
958 (CicMetaSubst.ppterm ~metasenv subst t1)
959 (CicMetaSubst.ppterm ~metasenv subst t2))))
960 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
961 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
962 subst context metasenv te t2 ugraph
963 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
964 subst context metasenv t1 te ugraph
965 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
966 let subst',metasenv',ugraph1 =
967 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
969 fo_unif_subst test_equality_only
970 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
971 | (C.LetIn (_,s1,ty1,t1), t2)
972 | (t2, C.LetIn (_,s1,ty1,t1)) ->
974 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
975 | (C.Appl l1, C.Appl l2) ->
976 (* andrea: this case should be probably rewritten in the
979 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
982 (fun (subst,metasenv,ugraph) t1 t2 ->
984 test_equality_only subst context metasenv t1 t2 ugraph)
985 (subst,metasenv,ugraph) l1 l2
986 with (Invalid_argument msg) ->
987 raise (UnificationFailure (lazy msg)))
988 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
989 (* we verify that none of the args is a Meta,
990 since beta expanding with respoect to a metavariable
994 let (_,t,_) = CicUtil.lookup_subst i subst in
995 let lifted = S.subst_meta l t in
996 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
999 subst context metasenv reduced t2 ugraph
1000 with CicUtil.Subst_not_found _ -> *)
1001 let subst,metasenv,beta_expanded,ugraph1 =
1003 test_equality_only metasenv subst context t2 args ugraph
1005 fo_unif_subst test_equality_only subst context metasenv
1006 (C.Meta (i,l)) beta_expanded ugraph1
1007 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
1009 let (_,t,_) = CicUtil.lookup_subst i subst in
1010 let lifted = S.subst_meta l t in
1011 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
1014 subst context metasenv t1 reduced ugraph
1015 with CicUtil.Subst_not_found _ -> *)
1016 let subst,metasenv,beta_expanded,ugraph1 =
1019 metasenv subst context t1 args ugraph
1021 fo_unif_subst test_equality_only subst context metasenv
1022 (C.Meta (i,l)) beta_expanded ugraph1
1024 let lr1 = List.rev l1 in
1025 let lr2 = List.rev l2 in
1027 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
1030 | _,[] -> assert false
1033 test_equality_only subst context metasenv h1 h2 ugraph
1036 fo_unif_subst test_equality_only subst context metasenv
1037 h (C.Appl (List.rev l)) ugraph
1038 | ((h1::l1),(h2::l2)) ->
1039 let subst', metasenv',ugraph1 =
1042 subst context metasenv h1 h2 ugraph
1045 test_equality_only subst' metasenv' (l1,l2) ugraph1
1049 test_equality_only subst metasenv (lr1, lr2) ugraph
1051 | UnificationFailure s
1052 | Uncertain s as exn ->
1055 | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
1056 (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
1057 CoercDb.is_a_coercion cc1 <> None &&
1058 CoercDb.is_a_coercion cc2 <> None &&
1059 not (UriManager.eq uri1 uri2) ->
1061 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1063 let inner_coerced t =
1064 let t = CicMetaSubst.apply_subst subst t in
1068 (match CoercGraph.coerced_arg l with
1070 | Some (t,_) -> aux (List.hd l) t t)
1073 aux (Cic.Implicit None) (Cic.Implicit None) t
1075 let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
1076 let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
1079 CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
1081 | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
1084 let head1_c, head2_c =
1086 CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
1088 | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
1091 let unfold uri ens args =
1093 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
1097 | Cic.Constant (_,Some bo,_,_,_) ->
1098 CicReduction.head_beta_reduce ~delta:false
1099 (Cic.Appl (bo::args))
1102 let conclude subst metasenv ugraph last_tl1' last_tl2' =
1103 let subst',metasenv,ugraph =
1106 ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
1107 " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
1109 fo_unif_subst test_equality_only subst context
1110 metasenv last_tl1' last_tl2' ugraph
1112 if subst = subst' then raise exn
1115 let subst,metasenv,ugrph as res =
1117 fo_unif_subst test_equality_only subst' context
1118 metasenv (C.Appl l1) (C.Appl l2) ugraph
1122 (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
1123 " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1127 if CoercDb.eq_carr car1 car2 then
1128 match last_tl1,last_tl2 with
1129 | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
1132 let subst,metasenv,ugraph =
1133 fo_unif_subst test_equality_only subst context
1134 metasenv last_tl1 last_tl2 ugraph
1136 fo_unif_subst test_equality_only subst context
1137 metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
1138 | _ when CoercDb.eq_carr head1_c head2_c ->
1139 (* composite VS composition + metas avoiding
1140 * coercions not only in coerced position *)
1141 if c1 <> cc1 && c2 <> cc2 then
1142 conclude subst metasenv ugraph
1147 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
1149 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
1151 fo_unif_subst test_equality_only subst context
1152 metasenv l1 l2 ugraph
1156 match last_tl1 with Cic.Meta _ -> true | _ -> false in
1158 match last_tl2 with Cic.Meta _ -> true | _ -> false in
1159 if not (grow1 || grow2) then
1160 (* no flexible terminals -> no pullback, but
1161 * we still unify them, in some cases it helps *)
1162 conclude subst metasenv ugraph last_tl1 last_tl2
1166 metasenv subst context (grow1,car1) (grow2,car2)
1170 | (carr,metasenv,to1,to2)::xxx ->
1171 warn_if_not_unique xxx to1 to2 carr car1 car2;
1172 let last_tl1',(subst,metasenv,ugraph) =
1173 match grow1,to1 with
1174 | true,Some (last,coerced) ->
1176 fo_unif_subst test_equality_only subst context
1177 metasenv coerced last_tl1 ugraph
1178 | _ -> last_tl1,(subst,metasenv,ugraph)
1180 let last_tl2',(subst,metasenv,ugraph) =
1181 match grow2,to2 with
1182 | true,Some (last,coerced) ->
1184 fo_unif_subst test_equality_only subst context
1185 metasenv coerced last_tl2 ugraph
1186 | _ -> last_tl2,(subst,metasenv,ugraph)
1188 conclude subst metasenv ugraph last_tl1' last_tl2')
1190 (* {{{ CSC: This is necessary because of the "elim H" tactic
1191 where the type of H is only reducible to an
1192 inductive type. This could be extended from inductive
1193 types to any rigid term. However, the code is
1194 duplicated in two places: inside applications and
1195 outside them. Probably it would be better to
1196 work with lambda-bar terms instead. *)
1197 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
1198 | (_, Cic.MutInd _::_) ->
1199 let t1' = R.whd ~subst context t1 in
1201 C.Appl (C.MutInd _::_) ->
1202 fo_unif_subst test_equality_only
1203 subst context metasenv t1' t2 ugraph
1204 | _ -> raise (UnificationFailure (lazy "88")))
1205 | (Cic.MutInd _::_,_) ->
1206 let t2' = R.whd ~subst context t2 in
1208 C.Appl (C.MutInd _::_) ->
1209 fo_unif_subst test_equality_only
1210 subst context metasenv t1 t2' ugraph
1213 (lazy ("not a mutind :"^
1214 CicMetaSubst.ppterm ~metasenv subst t2 ))))
1217 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
1218 let subst', metasenv',ugraph1 =
1219 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
1221 let subst'',metasenv'',ugraph2 =
1222 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
1226 (fun (subst,metasenv,ugraph) t1 t2 ->
1228 test_equality_only subst context metasenv t1 t2 ugraph
1229 ) (subst'',metasenv'',ugraph2) pl1 pl2
1231 Invalid_argument _ ->
1232 raise (UnificationFailure (lazy "6.1")))
1234 "Error trying to unify %s with %s: the number of branches is not the same."
1235 (CicMetaSubst.ppterm ~metasenv subst t1)
1236 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
1237 | (C.Rel _, _) | (_, C.Rel _) ->
1239 subst, metasenv,ugraph
1241 raise (UnificationFailure (lazy
1243 "Can't unify %s with %s because they are not convertible"
1244 (CicMetaSubst.ppterm ~metasenv subst t1)
1245 (CicMetaSubst.ppterm ~metasenv subst t2))))
1246 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
1247 let subst,metasenv,beta_expanded,ugraph1 =
1249 test_equality_only metasenv subst context t2 args ugraph
1251 fo_unif_subst test_equality_only subst context metasenv
1252 (C.Meta (i,l)) beta_expanded ugraph1
1253 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
1254 let subst,metasenv,beta_expanded,ugraph1 =
1256 test_equality_only metasenv subst context t1 args ugraph
1258 fo_unif_subst test_equality_only subst context metasenv
1259 beta_expanded (C.Meta (i,l)) ugraph1
1260 (* Works iff there are no arguments applied to it; similar to the
1262 | (_, C.MutInd _) ->
1263 let t1' = R.whd ~subst context t1 in
1266 fo_unif_subst test_equality_only
1267 subst context metasenv t1' t2 ugraph
1268 | _ -> raise (UnificationFailure (lazy "8")))
1270 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
1271 let subst',metasenv',ugraph1 =
1272 fo_unif_subst true subst context metasenv s1 s2 ugraph
1274 fo_unif_subst test_equality_only
1275 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1277 (match CicReduction.whd ~subst context t2 with
1279 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1280 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
1282 (match CicReduction.whd ~subst context t1 with
1284 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1285 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
1287 (* delta-beta reduction should almost never be a problem for
1289 1. long computations require iota reduction
1290 2. it is extremely rare that a close term t1 (that could be unified
1291 to t2) beta-delta reduces to t1' while t2 does not beta-delta
1292 reduces in the same way. This happens only if one meta of t2
1293 occurs in head position during beta reduction. In this unluky
1294 case too much reduction will be performed on t1 and unification
1295 will surely fail. *)
1296 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
1297 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
1298 if t1 = t1' && t2 = t2' then
1299 raise (UnificationFailure
1302 "Can't unify %s with %s because they are not convertible"
1303 (CicMetaSubst.ppterm ~metasenv subst t1)
1304 (CicMetaSubst.ppterm ~metasenv subst t2))))
1307 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
1309 UnificationFailure _
1311 raise (UnificationFailure
1314 "Can't unify %s with %s because they are not convertible"
1315 (CicMetaSubst.ppterm ~metasenv subst t1)
1316 (CicMetaSubst.ppterm ~metasenv subst t2))))
1318 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
1319 exp_named_subst1 exp_named_subst2 ugraph
1323 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
1324 assert (uri1=uri2) ;
1325 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1326 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
1328 Invalid_argument _ ->
1333 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
1336 raise (UnificationFailure (lazy (sprintf
1337 "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))))
1339 (* A substitution is a (int * Cic.term) list that associates a *)
1340 (* metavariable i with its body. *)
1341 (* metasenv is of type Cic.metasenv *)
1342 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
1343 (* a new substitution which is already unwinded and ready to be applied and *)
1344 (* a new metasenv in which some hypothesis in the contexts of the *)
1345 (* metavariables may have been restricted. *)
1346 let fo_unif metasenv context t1 t2 ugraph =
1347 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
1349 let enrich_msg msg subst context metasenv t1 t2 ugraph =
1352 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"
1353 (CicMetaSubst.ppterm ~metasenv subst t1)
1355 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1358 | UnificationFailure s
1360 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1361 (CicMetaSubst.ppterm ~metasenv subst t2)
1363 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1366 | UnificationFailure s
1368 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1369 (CicMetaSubst.ppcontext ~metasenv subst context)
1370 (CicMetaSubst.ppmetasenv subst metasenv)
1371 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
1373 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
1374 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
1376 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1377 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
1379 | UnificationFailure s
1381 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1382 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
1384 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1385 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
1387 | UnificationFailure s
1389 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1390 (CicMetaSubst.ppcontext ~metasenv subst context)
1391 (CicMetaSubst.ppmetasenv subst metasenv)
1395 let fo_unif_subst subst context metasenv t1 t2 ugraph =
1397 fo_unif_subst false subst context metasenv t1 t2 ugraph
1399 | AssertFailure msg ->
1400 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1401 | UnificationFailure msg ->
1402 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))