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 fail_exc metasenv subst context t1 t2 =
21 UnificationFailure (lazy (
22 "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
23 " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
28 | NCic.Appl l -> NCic.Appl (l@tl)
29 | _ -> NCic.Appl (hd :: tl)
36 | NCic.Appl (NCic.Meta _::_) -> true
40 exception WrongShape;;
42 let eta_reduce after_beta_expansion after_beta_expansion_body
46 match before_beta_expansion,after_beta_expansion_body with
47 Cic.Appl l, Cic.Appl l' ->
48 let rec all_but_last check_last =
52 | [_] -> if check_last then raise WrongShape else []
53 | he::tl -> he::(all_but_last check_last tl)
55 let all_but_last check_last l =
56 match all_but_last check_last l with
61 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
62 let all_but_last = all_but_last false l in
63 (* here we should test alpha-equivalence; however we know by
64 construction that here alpha_equivalence is equivalent to = *)
65 if t = all_but_last then
69 | _,_ -> after_beta_expansion
71 WrongShape -> after_beta_expansion
73 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
74 let module S = CicSubstitution in
77 let rec aux metasenv subst n context t' ugraph =
80 let subst,metasenv,ugraph1 =
81 fo_unif_subst test_equality_only subst context metasenv
82 (CicSubstitution.lift n arg) t' ugraph
85 subst,metasenv,C.Rel (1 + n),ugraph1
88 | UnificationFailure _ ->
90 | C.Rel m -> subst,metasenv,
91 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
92 | C.Var (uri,exp_named_subst) ->
93 let subst,metasenv,exp_named_subst',ugraph1 =
94 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
96 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
98 (* andrea: in general, beta_expand can create badly typed
99 terms. This happens quite seldom in practice, UNLESS we
100 iterate on the local context. For this reason, we renounce
101 to iterate and just lift *)
105 Some t -> Some (CicSubstitution.lift 1 t)
107 subst, metasenv, C.Meta (i,l), ugraph
109 | C.Implicit _ as t -> subst,metasenv,t,ugraph
111 let subst,metasenv,te',ugraph1 =
112 aux metasenv subst n context te ugraph in
113 let subst,metasenv,ty',ugraph2 =
114 aux metasenv subst n context ty ugraph1 in
115 (* TASSI: sure this is in serial? *)
116 subst,metasenv,(C.Cast (te', ty')),ugraph2
118 let subst,metasenv,s',ugraph1 =
119 aux metasenv subst n context s ugraph in
120 let subst,metasenv,t',ugraph2 =
121 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
124 (* TASSI: sure this is in serial? *)
125 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
126 | C.Lambda (nn,s,t) ->
127 let subst,metasenv,s',ugraph1 =
128 aux metasenv subst n context s ugraph in
129 let subst,metasenv,t',ugraph2 =
130 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
132 (* TASSI: sure this is in serial? *)
133 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
134 | C.LetIn (nn,s,ty,t) ->
135 let subst,metasenv,s',ugraph1 =
136 aux metasenv subst n context s ugraph in
137 let subst,metasenv,ty',ugraph1 =
138 aux metasenv subst n context ty ugraph in
139 let subst,metasenv,t',ugraph2 =
140 aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
143 (* TASSI: sure this is in serial? *)
144 subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
146 let subst,metasenv,revl',ugraph1 =
148 (fun (subst,metasenv,appl,ugraph) t ->
149 let subst,metasenv,t',ugraph1 =
150 aux metasenv subst n context t ugraph in
151 subst,metasenv,(t'::appl),ugraph1
152 ) (subst,metasenv,[],ugraph) l
154 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
155 | C.Const (uri,exp_named_subst) ->
156 let subst,metasenv,exp_named_subst',ugraph1 =
157 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
159 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
160 | C.MutInd (uri,i,exp_named_subst) ->
161 let subst,metasenv,exp_named_subst',ugraph1 =
162 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
164 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
165 | C.MutConstruct (uri,i,j,exp_named_subst) ->
166 let subst,metasenv,exp_named_subst',ugraph1 =
167 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
169 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
170 | C.MutCase (sp,i,outt,t,pl) ->
171 let subst,metasenv,outt',ugraph1 =
172 aux metasenv subst n context outt ugraph in
173 let subst,metasenv,t',ugraph2 =
174 aux metasenv subst n context t ugraph1 in
175 let subst,metasenv,revpl',ugraph3 =
177 (fun (subst,metasenv,pl,ugraph) t ->
178 let subst,metasenv,t',ugraph1 =
179 aux metasenv subst n context t ugraph in
180 subst,metasenv,(t'::pl),ugraph1
181 ) (subst,metasenv,[],ugraph2) pl
183 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
184 (* TASSI: not sure this is serial *)
186 (*CSC: not implemented
187 let tylen = List.length fl in
190 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
193 C.Fix (i, substitutedfl)
195 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
197 (*CSC: not implemented
198 let tylen = List.length fl in
201 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
204 C.CoFix (i, substitutedfl)
207 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
209 and aux_exp_named_subst metasenv subst n context ens ugraph =
211 (fun (uri,t) (subst,metasenv,l,ugraph) ->
212 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
213 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
215 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
217 FreshNamesGenerator.mk_fresh_name ~subst
218 metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
220 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
221 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
222 subst, metasenv, t'', ugraph2
223 in profiler_beta_expand.HExtlib.profile foo ()
226 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
227 let _,subst,metasenv,hd,ugraph =
229 (fun arg (num,subst,metasenv,t,ugraph) ->
230 let subst,metasenv,t,ugraph1 =
231 beta_expand num test_equality_only
232 metasenv subst context t arg ugraph
234 num+1,subst,metasenv,t,ugraph1
235 ) args (1,subst,metasenv,t,ugraph)
237 subst,metasenv,hd,ugraph
241 let rec instantiate test_eq_only metasenv subst context n lc t swap =
242 let unif m s c t1 t2 =
243 if swap then unify m s c t2 t1 else unify m s c t1 t2
246 try NCicTypeChecker.typeof ~subst ~metasenv context t
247 with NCicTypeChecker.TypeCheckerFailure _ -> assert false
249 let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
250 let ty = NCicSubstitution.subst_meta lc ty in
251 let metasenv, subst = unify metasenv susbt context ty ty_t in
252 let (metasenv, subst), t =
253 NCicMetaSubst.delift metasenv subst context n lc t
255 (* Unifying the types may have already instantiated n. *)
257 let _, _,oldt,_ = CicUtil.lookup_subst n subst in
258 let oldt = NCicSubstitution.subst_meta lc oldt in
259 (* conjecture: always fail --> occur check *)
260 unify test_eq_only metasenv subst context oldt t
261 with CicUtil.Subst_not_found _ ->
262 (* by cumulativity when unify(?,Type_i)
263 * we could ? := Type_j with j <= i... *)
264 let subst = (n, (name, ctx, t, ty)) :: subst in
266 List.filter (fun (m,_) -> not (n = m)) metasenv
270 and unify metasenv subst context t1 t2 =
271 let rec aux test_eq_only metasenv subst context t1 t2 =
272 let fo_unif test_eq_only metasenv subst t1 t2 =
277 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
278 if NCicEnvironment.universe_leq a b then metasenv, subst
279 else raise (fail_exc metasenv subst context t1 t2)
280 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
281 if NCicEnvironment.universe_eq a b then metasenv, subst
282 else raise (fail_exc metasenv subst context t1 t2)
283 | (C.Sort C.Prop,C.Sort (C.Type _)) ->
284 if (not test_eq_only) then metasenv, subst
285 else raise (fail_exc metasenv subst context t1 t2)
287 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
288 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
289 let metasenv, subst = aux true metasenv subst context s1 s2 in
290 aux test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
291 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
292 let metasenv,subst=aux test_eq_only metasenv subst context ty1 ty2 in
293 let metasenv,subst=aux test_eq_only metasenv subst context s1 s2 in
294 let context = (name1, C.Def (s1,ty1))::context in
295 aux test_eq_only metasenv subst context t1 t2
297 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
299 let l1 = NCicUtils.expand_local_context l1 in
300 let l2 = NCicUtils.expand_local_context l2 in
301 let metasenv, subst, to_restrict, _ =
303 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
305 aux test_eq_only metasenv subst context
306 (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2),
308 with UnificationFailure _ | Uncertain _ ->
309 metasenv, subst, i::to_restrict, i-1)
310 l1 l2 (metasenv, subst, [], List.length l1)
312 let metasenv, subst, _ =
313 NCicMetaSubst.restrict metasenv subst n1 to_restrict
317 | Invalid_argument _ -> assert false
318 | NCicMetaSubst.MetaSubstFailure msg ->
320 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
321 let term1 = NCicSubstitution.subst_meta lc1 term in
322 let term2 = NCicSubstitution.subst_meta lc2 term in
323 aux test_eq_only metasenv subst context term1 term2
324 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
326 | C.Meta (n,lc), t ->
328 let _,_,term,_ = NCicUtils.lookup_subst n subst in
329 let term = NCicSubstitution.subst_meta lc term in
330 aux test_eq_only metasenv subst context term t
331 with NCicUtils.Subst_not_found _->
332 instantiate test_eq_only metasenv subst context n lc t false
334 | t, C.Meta (n,lc) ->
336 let _,_,term,_ = NCicUtils.lookup_subst n subst in
337 let term = NCicSubstitution.subst_meta lc term in
338 aux test_eq_only metasenv subst context t term
339 with NCicUtils.Subst_not_found _->
340 instantiate test_eq_only metasenv subst context n lc t true
342 | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
343 let _,_,term,_ = NCicUtils.lookup_subst i subst in
344 let term = NCicSubstitution.subst_meta l term in
345 aux test_eq_only metasenv subst context (mk_appl term args) t2
347 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
348 let _,_,term,_ = NCicUtils.lookup_subst i subst in
349 let term = NCicSubstitution.subst_meta l term in
350 aux test_eq_only metasenv subst context t1 (mk_appl term args)
352 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
353 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
356 (fun (metasenv, subst) t1 t2 ->
357 aux test_eq_only metasenv subst context t1 t2)
358 (metasenv,subst) l1 l2
359 with Invalid_argument _ ->
360 raise (fail_exc metasenv subst context t1 t2)
362 | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
363 (* we verify that none of the args is a Meta,
364 since beta expanding w.r.t a metavariable makes no sense *)
365 let subst, metasenv, beta_expanded =
367 test_equality_only metasenv subst context t2 args ugraph
369 aux test_eq_only metasenv subst context
370 (C.Meta (i,l)) beta_expanded
371 | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
372 let subst,metasenv,beta_expanded =
375 metasenv subst context t1 args ugraph
377 fo_unif_subst test_equality_only subst context metasenv
378 (C.Meta (i,l)) beta_expanded ugraph1
381 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
382 when (Ref.eq r1 r2 &&
383 List.length (E.get_relevance r1) >= List.length tl1) ->
384 let relevance = E.get_relevance r1 in
385 let relevance = match r1 with
386 | Ref.Ref (_,Ref.Con (_,_,lno)) ->
387 let _,relevance = HExtlib.split_nth lno relevance in
388 HExtlib.mk_list false lno @ relevance
391 let fail = ref ~-1 in
393 HExtlib.list_forall_default3
394 (fun t1 t2 b -> fail := !fail+1; not b || aux test_eq_only context t1 t2)
395 tl1 tl2 true relevance
396 with Invalid_argument _ -> false)
400 let relevance = get_relevance_p ~subst context _hd1 tl1 in
401 let _,relevance = HExtlib.split_nth !fail relevance in
402 let b,relevance = (match relevance with
405 let _,tl1 = HExtlib.split_nth (!fail+1) tl1 in
406 let _,tl2 = HExtlib.split_nth (!fail+1) tl2 in
410 HExtlib.list_forall_default3
411 (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
412 tl1 tl2 true relevance
413 with Invalid_argument _ -> false)
415 | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
416 aux test_eq_only context hd1 hd2 &&
417 let relevance = get_relevance ~subst context hd1 tl1 in
419 HExtlib.list_forall_default3
420 (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
421 tl1 tl2 true relevance
422 with Invalid_argument _ -> false)
424 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
425 C.Match (ref2,outtype2,term2,pl2)) ->
426 let _,_,itl,_,_ = E.get_checked_indtys ref1 in
427 let _,_,ty,_ = List.nth itl tyno in
428 let rec remove_prods ~subst context ty =
429 let ty = whd ~subst context ty in
432 | C.Prod (name,so,ta) ->
433 remove_prods ~subst ((name,(C.Decl so))::context) ta
437 match remove_prods ~subst [] ty with
438 | C.Sort C.Prop -> true
441 let rec remove_prods ~subst context ty =
442 let ty = whd ~subst context ty in
445 | C.Prod (name,so,ta) ->
446 remove_prods ~subst ((name,(C.Decl so))::context) ta
449 if not (Ref.eq ref1 ref2) then
450 raise (uncert_exc metasenv subst context t1 t2)
452 let metasenv, subst =
453 aux test_eq_only metasenv subst context outtype1 outtype2 in
454 let metasenv, subst =
455 try aux test_eq_only metasenv subst context term1 term2
456 with UnificationFailure _ | Uncertain _ when is_prop ->
461 (fun (metasenv,subst) -> aux test_eq_only metasenv subst context)
462 (metasenv, subst) pl1 pl2
463 with Invalid_argument _ ->
464 raise (uncert_exc metasenv subst context t1 t2)
465 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
466 | _ -> raise (uncert_exc metasenv subst context t1 t2)
468 let rec unif_machines metasenv subst = function
469 | ((k1,e1,NCic.Meta _ as t1,s1 as m1),(k2,e2,t2,s2 as m2),delta)
470 | ((k1,e1,t1,s1 as m1),(k2,e2,NCic.Meta _ as t2,s2 as m2),delta) ->
472 fo_unif test_eq_only metasenv subst (R.unwind m1) (R.unwind m2)
473 with UnificationFailure _ | Uncertain _ when delta > 0 ->
474 let delta = delta - 1 in
475 let red = R.reduce ~delta ~subst context in
476 unif_machines metasenv subst (red m1,red m2,delta)
477 | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) ->
479 let metasenv, subst =
480 fo_unif test_eq_only metasenv subst
481 (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[]))
485 | C.Const r -> NCicEnvironment.get_relevance r
488 let rec check_stack f l1 l2 r a =
490 | x1::tl1, x2::tl2, r::tr ->
491 check_stack f tl1 tl2 tr (f x1 x2 r a)
492 | x1::tl1, x2::tl2, [] ->
493 check_stack f tl1 tl2 tr (f x1 x2 true a)
495 | _ -> raise (Invalid_argument "check_stack")
498 (fun t1 t2 b (metasenv,subst) ->
500 let t1 = RS.from_stack t1 in
501 let t2 = RS.from_stack t2 in
502 unif_machines metasenv subst (small_delta_step t1 t2)
503 with UnificationFailure _ | Uncertain _ when not b ->
505 s1 s2 relevance (metasenv,subst)
506 with Invalid_argument _ ->
507 raise (UnificationFailure (lazy ( "Can't unify " ^ NCicPp.ppterm
508 ~metasenv ~subst ~context (R.unwind m1) ^ " with " ^ NCicPp.ppterm
509 ~metasenv ~subst ~context (R.unwind m2))))
510 with UnificationFailure _ | Uncertain _ when delta > 0 ->
511 let delta = delta - 1 in
512 let red = R.reduce ~delta ~subst context in
513 unif_machines metasenv subst (red m1,red m2,delta)
515 let height_of = function
516 | NCic.Const (Ref.Ref (_,Ref.Def h))
517 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
518 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
519 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
520 | NCic.Meta _ -> max_int
523 let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
524 let h1 = height_of t1 in
525 let h2 = height_of t2 in
526 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
527 R.reduce ~delta ~subst context m1,
528 R.reduce ~delta ~subst context m2,
531 try fo_unif test_eq_only metasenv subst t1 t2
532 with UnificationFailure msg |Uncertain msg as exn ->
534 unif_machines metasenv subst
535 (small_delta_step (0,[],t1,[]) (0,[],t2,[]))
537 | UnificationFailure _ -> raise (UnificationFailure msg)
538 | Uncertain _ -> raise exn
540 aux false metasenv subst context t1 t2
549 exception UnificationFailure of string Lazy.t;;
550 exception Uncertain of string Lazy.t;;
551 exception AssertFailure of string Lazy.t;;
553 let verbose = false;;
554 let debug_print = fun _ -> ()
556 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
557 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
558 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
559 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
561 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
563 let type_of_aux' metasenv subst context term ugraph =
566 profile.HExtlib.profile
567 (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
569 CicTypeChecker.TypeCheckerFailure msg ->
573 "Kernel Type checking error:
574 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
575 (CicMetaSubst.ppterm ~metasenv subst term)
576 (CicMetaSubst.ppterm ~metasenv [] term)
577 (CicMetaSubst.ppcontext ~metasenv subst context)
578 (CicMetaSubst.ppmetasenv subst metasenv)
579 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
580 raise (AssertFailure msg)
581 | CicTypeChecker.AssertFailure msg ->
584 "Kernel Type checking assertion failure:
585 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
586 (CicMetaSubst.ppterm ~metasenv subst term)
587 (CicMetaSubst.ppterm ~metasenv [] term)
588 (CicMetaSubst.ppcontext ~metasenv subst context)
589 (CicMetaSubst.ppmetasenv subst metasenv)
590 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
591 raise (AssertFailure msg)
592 in profiler_toa.HExtlib.profile foo ()
595 let exists_a_meta l =
599 | Cic.Appl (Cic.Meta _::_) -> true
602 let rec deref subst t =
603 let snd (_,a,_) = a in
608 (CicSubstitution.subst_meta
609 l (snd (CicUtil.lookup_subst n subst)))
611 CicUtil.Subst_not_found _ -> t)
612 | Cic.Appl(Cic.Meta(n,l)::args) ->
613 (match deref subst (Cic.Meta(n,l)) with
614 | Cic.Lambda _ as t ->
615 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
616 | r -> Cic.Appl(r::args))
617 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
618 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
623 let foo () = deref subst t
624 in profiler_deref.HExtlib.profile foo ()
626 exception WrongShape;;
627 let eta_reduce after_beta_expansion after_beta_expansion_body
628 before_beta_expansion
631 match before_beta_expansion,after_beta_expansion_body with
632 Cic.Appl l, Cic.Appl l' ->
633 let rec all_but_last check_last =
637 | [_] -> if check_last then raise WrongShape else []
638 | he::tl -> he::(all_but_last check_last tl)
640 let all_but_last check_last l =
641 match all_but_last check_last l with
646 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
647 let all_but_last = all_but_last false l in
648 (* here we should test alpha-equivalence; however we know by
649 construction that here alpha_equivalence is equivalent to = *)
650 if t = all_but_last then
654 | _,_ -> after_beta_expansion
656 WrongShape -> after_beta_expansion
658 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
659 let module S = CicSubstitution in
660 let module C = Cic in
662 let rec aux metasenv subst n context t' ugraph =
665 let subst,metasenv,ugraph1 =
666 fo_unif_subst test_equality_only subst context metasenv
667 (CicSubstitution.lift n arg) t' ugraph
670 subst,metasenv,C.Rel (1 + n),ugraph1
673 | UnificationFailure _ ->
675 | C.Rel m -> subst,metasenv,
676 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
677 | C.Var (uri,exp_named_subst) ->
678 let subst,metasenv,exp_named_subst',ugraph1 =
679 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
681 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
683 (* andrea: in general, beta_expand can create badly typed
684 terms. This happens quite seldom in practice, UNLESS we
685 iterate on the local context. For this reason, we renounce
686 to iterate and just lift *)
690 Some t -> Some (CicSubstitution.lift 1 t)
692 subst, metasenv, C.Meta (i,l), ugraph
694 | C.Implicit _ as t -> subst,metasenv,t,ugraph
696 let subst,metasenv,te',ugraph1 =
697 aux metasenv subst n context te ugraph in
698 let subst,metasenv,ty',ugraph2 =
699 aux metasenv subst n context ty ugraph1 in
700 (* TASSI: sure this is in serial? *)
701 subst,metasenv,(C.Cast (te', ty')),ugraph2
703 let subst,metasenv,s',ugraph1 =
704 aux metasenv subst n context s ugraph in
705 let subst,metasenv,t',ugraph2 =
706 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
709 (* TASSI: sure this is in serial? *)
710 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
711 | C.Lambda (nn,s,t) ->
712 let subst,metasenv,s',ugraph1 =
713 aux metasenv subst n context s ugraph in
714 let subst,metasenv,t',ugraph2 =
715 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
717 (* TASSI: sure this is in serial? *)
718 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
719 | C.LetIn (nn,s,ty,t) ->
720 let subst,metasenv,s',ugraph1 =
721 aux metasenv subst n context s ugraph in
722 let subst,metasenv,ty',ugraph1 =
723 aux metasenv subst n context ty ugraph in
724 let subst,metasenv,t',ugraph2 =
725 aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
728 (* TASSI: sure this is in serial? *)
729 subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
731 let subst,metasenv,revl',ugraph1 =
733 (fun (subst,metasenv,appl,ugraph) t ->
734 let subst,metasenv,t',ugraph1 =
735 aux metasenv subst n context t ugraph in
736 subst,metasenv,(t'::appl),ugraph1
737 ) (subst,metasenv,[],ugraph) l
739 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
740 | C.Const (uri,exp_named_subst) ->
741 let subst,metasenv,exp_named_subst',ugraph1 =
742 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
744 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
745 | C.MutInd (uri,i,exp_named_subst) ->
746 let subst,metasenv,exp_named_subst',ugraph1 =
747 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
749 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
750 | C.MutConstruct (uri,i,j,exp_named_subst) ->
751 let subst,metasenv,exp_named_subst',ugraph1 =
752 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
754 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
755 | C.MutCase (sp,i,outt,t,pl) ->
756 let subst,metasenv,outt',ugraph1 =
757 aux metasenv subst n context outt ugraph in
758 let subst,metasenv,t',ugraph2 =
759 aux metasenv subst n context t ugraph1 in
760 let subst,metasenv,revpl',ugraph3 =
762 (fun (subst,metasenv,pl,ugraph) t ->
763 let subst,metasenv,t',ugraph1 =
764 aux metasenv subst n context t ugraph in
765 subst,metasenv,(t'::pl),ugraph1
766 ) (subst,metasenv,[],ugraph2) pl
768 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
769 (* TASSI: not sure this is serial *)
771 (*CSC: not implemented
772 let tylen = List.length fl in
775 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
778 C.Fix (i, substitutedfl)
780 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
782 (*CSC: not implemented
783 let tylen = List.length fl in
786 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
789 C.CoFix (i, substitutedfl)
792 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
794 and aux_exp_named_subst metasenv subst n context ens ugraph =
796 (fun (uri,t) (subst,metasenv,l,ugraph) ->
797 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
798 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
800 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
802 FreshNamesGenerator.mk_fresh_name ~subst
803 metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
805 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
806 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
807 subst, metasenv, t'', ugraph2
808 in profiler_beta_expand.HExtlib.profile foo ()
811 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
812 let _,subst,metasenv,hd,ugraph =
814 (fun arg (num,subst,metasenv,t,ugraph) ->
815 let subst,metasenv,t,ugraph1 =
816 beta_expand num test_equality_only
817 metasenv subst context t arg ugraph
819 num+1,subst,metasenv,t,ugraph1
820 ) args (1,subst,metasenv,t,ugraph)
822 subst,metasenv,hd,ugraph
824 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
827 | (m2,_,c2,c2')::_ ->
828 let m1,c1,c1' = carr,to1,to2 in
830 function Some (_,t) -> CicPp.ppterm t
834 ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
835 CoercDb.string_of_carr car2^": " ^
836 CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
837 unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
838 unopt c2^" + "^unopt c2')
840 (* NUOVA UNIFICAZIONE *)
841 (* A substitution is a (int * Cic.term) list that associates a
842 metavariable i with its body.
843 A metaenv is a (int * Cic.term) list that associate a metavariable
845 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
846 a new substitution which is _NOT_ unwinded. It must be unwinded before
849 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
850 let module C = Cic in
851 let module R = CicReduction in
852 let module S = CicSubstitution in
853 let t1 = deref subst t1 in
854 let t2 = deref subst t2 in
855 let (&&&) a b = (a && b) || ((not a) && (not b)) in
856 (* let bef = Sys.time () in *)
858 if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
862 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
863 in profiler_are_convertible.HExtlib.profile foo ()
865 (* let aft = Sys.time () in
866 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
867 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
868 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
870 subst, metasenv, ugraph
873 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
874 let _,subst,metasenv,ugraph1 =
877 (fun (j,subst,metasenv,ugraph) t1 t2 ->
880 | _,None -> j+1,subst,metasenv,ugraph
881 | Some t1', Some t2' ->
882 (* First possibility: restriction *)
883 (* Second possibility: unification *)
884 (* Third possibility: convertibility *)
887 ~subst ~metasenv context t1' t2' ugraph
890 j+1,subst,metasenv, ugraph1
893 let subst,metasenv,ugraph2 =
896 subst context metasenv t1' t2' ugraph
898 j+1,subst,metasenv,ugraph2
901 | UnificationFailure _ ->
902 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
903 let metasenv, subst =
904 CicMetaSubst.restrict
905 subst [(n,j)] metasenv in
906 j+1,subst,metasenv,ugraph1)
907 ) (1,subst,metasenv,ugraph) ln lm
911 (UnificationFailure (lazy "1"))
914 "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."
915 (CicMetaSubst.ppterm ~metasenv subst t1)
916 (CicMetaSubst.ppterm ~metasenv subst t2))) *)
917 | Invalid_argument _ ->
919 (UnificationFailure (lazy "2")))
922 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
923 (CicMetaSubst.ppterm ~metasenv subst t1)
924 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
925 in subst,metasenv,ugraph1
926 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
927 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
929 | (t, C.Meta (n,l)) ->
932 C.Meta (n,_), C.Meta (m,_) when n < m -> false
933 | _, C.Meta _ -> false
936 let lower = fun x y -> if swap then y else x in
937 let upper = fun x y -> if swap then x else y in
938 let fo_unif_subst_ordered
939 test_equality_only subst context metasenv m1 m2 ugraph =
940 fo_unif_subst test_equality_only subst context metasenv
941 (lower m1 m2) (upper m1 m2) ugraph
944 let subst,metasenv,ugraph1 =
945 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
948 type_of_aux' metasenv subst context t ugraph
952 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
954 UnificationFailure _ as e -> raise e
955 | Uncertain msg -> raise (UnificationFailure msg)
957 debug_print (lazy "siamo allo huge hack");
958 (* TODO huge hack!!!!
959 * we keep on unifying/refining in the hope that
960 * the problem will be eventually solved.
961 * In the meantime we're breaking a big invariant:
962 * the terms that we are unifying are no longer well
963 * typed in the current context (in the worst case
964 * we could even diverge) *)
965 (subst, metasenv,ugraph)) in
966 let t',metasenv,subst =
968 CicMetaSubst.delift n subst context metasenv l t
970 (CicMetaSubst.MetaSubstFailure msg)->
971 raise (UnificationFailure msg)
972 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
976 C.Sort (C.Type u) when not test_equality_only ->
977 let u' = CicUniv.fresh () in
978 let s = C.Sort (C.Type u') in
981 CicUniv.add_ge (upper u u') (lower u u') ugraph1
985 CicUniv.UniverseInconsistency msg ->
986 raise (UnificationFailure msg))
989 (* Unifying the types may have already instantiated n. Let's check *)
991 let (_, oldt,_) = CicUtil.lookup_subst n subst in
992 let lifted_oldt = S.subst_meta l oldt in
993 fo_unif_subst_ordered
994 test_equality_only subst context metasenv t lifted_oldt ugraph2
996 CicUtil.Subst_not_found _ ->
997 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
998 let subst = (n, (context, t'',ty)) :: subst in
1000 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
1001 subst, metasenv, ugraph2
1003 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
1004 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
1005 if UriManager.eq uri1 uri2 then
1006 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
1007 exp_named_subst1 exp_named_subst2 ugraph
1009 raise (UnificationFailure (lazy
1011 "Can't unify %s with %s due to different constants"
1012 (CicMetaSubst.ppterm ~metasenv subst t1)
1013 (CicMetaSubst.ppterm ~metasenv subst t2))))
1014 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
1015 if UriManager.eq uri1 uri2 && i1 = i2 then
1016 fo_unif_subst_exp_named_subst
1018 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
1020 raise (UnificationFailure
1023 "Can't unify %s with %s due to different inductive principles"
1024 (CicMetaSubst.ppterm ~metasenv subst t1)
1025 (CicMetaSubst.ppterm ~metasenv subst t2))))
1026 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
1027 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
1028 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
1029 fo_unif_subst_exp_named_subst
1031 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
1033 raise (UnificationFailure
1036 "Can't unify %s with %s due to different inductive constructors"
1037 (CicMetaSubst.ppterm ~metasenv subst t1)
1038 (CicMetaSubst.ppterm ~metasenv subst t2))))
1039 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
1040 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
1041 subst context metasenv te t2 ugraph
1042 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
1043 subst context metasenv t1 te ugraph
1044 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
1045 let subst',metasenv',ugraph1 =
1046 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
1048 fo_unif_subst test_equality_only
1049 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1050 | (C.LetIn (_,s1,ty1,t1), t2)
1051 | (t2, C.LetIn (_,s1,ty1,t1)) ->
1053 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
1054 | (C.Appl l1, C.Appl l2) ->
1055 (* andrea: this case should be probably rewritten in the
1058 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
1061 (fun (subst,metasenv,ugraph) t1 t2 ->
1063 test_equality_only subst context metasenv t1 t2 ugraph)
1064 (subst,metasenv,ugraph) l1 l2
1065 with (Invalid_argument msg) ->
1066 raise (UnificationFailure (lazy msg)))
1067 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
1068 (* we verify that none of the args is a Meta,
1069 since beta expanding with respoect to a metavariable
1073 let (_,t,_) = CicUtil.lookup_subst i subst in
1074 let lifted = S.subst_meta l t in
1075 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
1078 subst context metasenv reduced t2 ugraph
1079 with CicUtil.Subst_not_found _ -> *)
1080 let subst,metasenv,beta_expanded,ugraph1 =
1082 test_equality_only metasenv subst context t2 args ugraph
1084 fo_unif_subst test_equality_only subst context metasenv
1085 (C.Meta (i,l)) beta_expanded ugraph1
1086 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
1088 let (_,t,_) = CicUtil.lookup_subst i subst in
1089 let lifted = S.subst_meta l t in
1090 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
1093 subst context metasenv t1 reduced ugraph
1094 with CicUtil.Subst_not_found _ -> *)
1095 let subst,metasenv,beta_expanded,ugraph1 =
1098 metasenv subst context t1 args ugraph
1100 fo_unif_subst test_equality_only subst context metasenv
1101 (C.Meta (i,l)) beta_expanded ugraph1
1103 let lr1 = List.rev l1 in
1104 let lr2 = List.rev l2 in
1106 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
1109 | _,[] -> assert false
1112 test_equality_only subst context metasenv h1 h2 ugraph
1115 fo_unif_subst test_equality_only subst context metasenv
1116 h (C.Appl (List.rev l)) ugraph
1117 | ((h1::l1),(h2::l2)) ->
1118 let subst', metasenv',ugraph1 =
1121 subst context metasenv h1 h2 ugraph
1124 test_equality_only subst' metasenv' (l1,l2) ugraph1
1128 test_equality_only subst metasenv (lr1, lr2) ugraph
1130 | UnificationFailure s
1131 | Uncertain s as exn ->
1134 | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
1135 (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
1136 CoercDb.is_a_coercion cc1 <> None &&
1137 CoercDb.is_a_coercion cc2 <> None &&
1138 not (UriManager.eq uri1 uri2) ->
1140 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1142 let inner_coerced t =
1143 let t = CicMetaSubst.apply_subst subst t in
1147 (match CoercGraph.coerced_arg l with
1149 | Some (t,_) -> aux (List.hd l) t t)
1152 aux (Cic.Implicit None) (Cic.Implicit None) t
1154 let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
1155 let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
1158 CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
1160 | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
1163 let head1_c, head2_c =
1165 CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
1167 | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
1170 let unfold uri ens args =
1172 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
1176 | Cic.Constant (_,Some bo,_,_,_) ->
1177 CicReduction.head_beta_reduce ~delta:false
1178 (Cic.Appl (bo::args))
1181 let conclude subst metasenv ugraph last_tl1' last_tl2' =
1182 let subst',metasenv,ugraph =
1185 ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
1186 " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
1188 fo_unif_subst test_equality_only subst context
1189 metasenv last_tl1' last_tl2' ugraph
1191 if subst = subst' then raise exn
1194 let subst,metasenv,ugrph as res =
1196 fo_unif_subst test_equality_only subst' context
1197 metasenv (C.Appl l1) (C.Appl l2) ugraph
1201 (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
1202 " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1206 if CoercDb.eq_carr car1 car2 then
1207 match last_tl1,last_tl2 with
1208 | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
1211 let subst,metasenv,ugraph =
1212 fo_unif_subst test_equality_only subst context
1213 metasenv last_tl1 last_tl2 ugraph
1215 fo_unif_subst test_equality_only subst context
1216 metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
1217 | _ when CoercDb.eq_carr head1_c head2_c ->
1218 (* composite VS composition + metas avoiding
1219 * coercions not only in coerced position *)
1220 if c1 <> cc1 && c2 <> cc2 then
1221 conclude subst metasenv ugraph
1226 unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
1228 Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
1230 fo_unif_subst test_equality_only subst context
1231 metasenv l1 l2 ugraph
1235 match last_tl1 with Cic.Meta _ -> true | _ -> false in
1237 match last_tl2 with Cic.Meta _ -> true | _ -> false in
1238 if not (grow1 || grow2) then
1239 (* no flexible terminals -> no pullback, but
1240 * we still unify them, in some cases it helps *)
1241 conclude subst metasenv ugraph last_tl1 last_tl2
1245 metasenv subst context (grow1,car1) (grow2,car2)
1249 | (carr,metasenv,to1,to2)::xxx ->
1250 warn_if_not_unique xxx to1 to2 carr car1 car2;
1251 let last_tl1',(subst,metasenv,ugraph) =
1252 match grow1,to1 with
1253 | true,Some (last,coerced) ->
1255 fo_unif_subst test_equality_only subst context
1256 metasenv coerced last_tl1 ugraph
1257 | _ -> last_tl1,(subst,metasenv,ugraph)
1259 let last_tl2',(subst,metasenv,ugraph) =
1260 match grow2,to2 with
1261 | true,Some (last,coerced) ->
1263 fo_unif_subst test_equality_only subst context
1264 metasenv coerced last_tl2 ugraph
1265 | _ -> last_tl2,(subst,metasenv,ugraph)
1267 conclude subst metasenv ugraph last_tl1' last_tl2')
1269 (* {{{ CSC: This is necessary because of the "elim H" tactic
1270 where the type of H is only reducible to an
1271 inductive type. This could be extended from inductive
1272 types to any rigid term. However, the code is
1273 duplicated in two places: inside applications and
1274 outside them. Probably it would be better to
1275 work with lambda-bar terms instead. *)
1276 | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
1277 | (_, Cic.MutInd _::_) ->
1278 let t1' = R.whd ~subst context t1 in
1280 C.Appl (C.MutInd _::_) ->
1281 fo_unif_subst test_equality_only
1282 subst context metasenv t1' t2 ugraph
1283 | _ -> raise (UnificationFailure (lazy "88")))
1284 | (Cic.MutInd _::_,_) ->
1285 let t2' = R.whd ~subst context t2 in
1287 C.Appl (C.MutInd _::_) ->
1288 fo_unif_subst test_equality_only
1289 subst context metasenv t1 t2' ugraph
1292 (lazy ("not a mutind :"^
1293 CicMetaSubst.ppterm ~metasenv subst t2 ))))
1296 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
1297 let subst', metasenv',ugraph1 =
1298 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
1300 let subst'',metasenv'',ugraph2 =
1301 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
1305 (fun (subst,metasenv,ugraph) t1 t2 ->
1307 test_equality_only subst context metasenv t1 t2 ugraph
1308 ) (subst'',metasenv'',ugraph2) pl1 pl2
1310 Invalid_argument _ ->
1311 raise (UnificationFailure (lazy "6.1")))
1313 "Error trying to unify %s with %s: the number of branches is not the same."
1314 (CicMetaSubst.ppterm ~metasenv subst t1)
1315 (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
1316 | (C.Rel _, _) | (_, C.Rel _) ->
1318 subst, metasenv,ugraph
1320 raise (UnificationFailure (lazy
1322 "Can't unify %s with %s because they are not convertible"
1323 (CicMetaSubst.ppterm ~metasenv subst t1)
1324 (CicMetaSubst.ppterm ~metasenv subst t2))))
1325 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
1326 let subst,metasenv,beta_expanded,ugraph1 =
1328 test_equality_only metasenv subst context t2 args ugraph
1330 fo_unif_subst test_equality_only subst context metasenv
1331 (C.Meta (i,l)) beta_expanded ugraph1
1332 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
1333 let subst,metasenv,beta_expanded,ugraph1 =
1335 test_equality_only metasenv subst context t1 args ugraph
1337 fo_unif_subst test_equality_only subst context metasenv
1338 beta_expanded (C.Meta (i,l)) ugraph1
1339 (* Works iff there are no arguments applied to it; similar to the
1341 | (_, C.MutInd _) ->
1342 let t1' = R.whd ~subst context t1 in
1345 fo_unif_subst test_equality_only
1346 subst context metasenv t1' t2 ugraph
1347 | _ -> raise (UnificationFailure (lazy "8")))
1349 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
1350 let subst',metasenv',ugraph1 =
1351 fo_unif_subst true subst context metasenv s1 s2 ugraph
1353 fo_unif_subst test_equality_only
1354 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1356 (match CicReduction.whd ~subst context t2 with
1358 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1359 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
1361 (match CicReduction.whd ~subst context t1 with
1363 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1364 | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
1366 (* delta-beta reduction should almost never be a problem for
1368 1. long computations require iota reduction
1369 2. it is extremely rare that a close term t1 (that could be unified
1370 to t2) beta-delta reduces to t1' while t2 does not beta-delta
1371 reduces in the same way. This happens only if one meta of t2
1372 occurs in head position during beta reduction. In this unluky
1373 case too much reduction will be performed on t1 and unification
1374 will surely fail. *)
1375 let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
1376 let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
1377 if t1 = t1' && t2 = t2' then
1378 raise (UnificationFailure
1381 "Can't unify %s with %s because they are not convertible"
1382 (CicMetaSubst.ppterm ~metasenv subst t1)
1383 (CicMetaSubst.ppterm ~metasenv subst t2))))
1386 fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
1388 UnificationFailure _
1390 raise (UnificationFailure
1393 "Can't unify %s with %s because they are not convertible"
1394 (CicMetaSubst.ppterm ~metasenv subst t1)
1395 (CicMetaSubst.ppterm ~metasenv subst t2))))
1397 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
1398 exp_named_subst1 exp_named_subst2 ugraph
1402 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
1403 assert (uri1=uri2) ;
1404 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1405 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
1407 Invalid_argument _ ->
1412 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
1415 raise (UnificationFailure (lazy (sprintf
1416 "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))))
1418 (* A substitution is a (int * Cic.term) list that associates a *)
1419 (* metavariable i with its body. *)
1420 (* metasenv is of type Cic.metasenv *)
1421 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
1422 (* a new substitution which is already unwinded and ready to be applied and *)
1423 (* a new metasenv in which some hypothesis in the contexts of the *)
1424 (* metavariables may have been restricted. *)
1425 let fo_unif metasenv context t1 t2 ugraph =
1426 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
1428 let enrich_msg msg subst context metasenv t1 t2 ugraph =
1431 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"
1432 (CicMetaSubst.ppterm ~metasenv subst t1)
1434 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1437 | UnificationFailure s
1439 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1440 (CicMetaSubst.ppterm ~metasenv subst t2)
1442 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1445 | UnificationFailure s
1447 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1448 (CicMetaSubst.ppcontext ~metasenv subst context)
1449 (CicMetaSubst.ppmetasenv subst metasenv)
1450 (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
1452 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
1453 (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
1455 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1456 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
1458 | UnificationFailure s
1460 | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1461 (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
1463 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1464 CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
1466 | UnificationFailure s
1468 | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1469 (CicMetaSubst.ppcontext ~metasenv subst context)
1470 (CicMetaSubst.ppmetasenv subst metasenv)
1474 let fo_unif_subst subst context metasenv t1 t2 ugraph =
1476 fo_unif_subst false subst context metasenv t1 t2 ugraph
1478 | AssertFailure msg ->
1479 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1480 | UnificationFailure msg ->
1481 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))