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;;
17 exception KeepReducing of string Lazy.t;;
18 exception KeepReducingThis of
19 string Lazy.t * (NCicReduction.machine * bool) *
20 (NCicReduction.machine * bool) ;;
22 let (===) x y = Pervasives.compare x y = 0 ;;
24 let mk_msg metasenv subst context t1 t2 =
26 "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
27 " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
29 let mk_appl ~upto hd tl =
30 NCicReduction.head_beta_reduce ~upto
32 | NCic.Appl l -> NCic.Appl (l@tl)
33 | _ -> NCic.Appl (hd :: tl))
36 exception WrongShape;;
38 let eta_reduce subst t =
39 let delift_if_not_occur body =
41 Some (NCicSubstitution.psubst ~avoid_beta_redexes:true
42 (fun () -> raise WrongShape) [()] body)
43 with WrongShape -> None
45 let rec eat_lambdas ctx = function
46 | NCic.Lambda (name, src, tgt) ->
47 eat_lambdas ((name, src) :: ctx) tgt
48 | NCic.Meta (i,lc) as t->
50 let _,_,t,_ = NCicUtils.lookup_subst i subst in
51 let t = NCicSubstitution.subst_meta lc t in
53 with NCicUtils.Subst_not_found _ -> ctx, t)
56 let context_body = eat_lambdas [] t in
57 let rec aux = function
59 | (name, src)::ctx, (NCic.Appl (hd::[NCic.Rel 1]) as bo) ->
60 (match delift_if_not_occur hd with
61 | None -> aux (ctx,NCic.Lambda(name,src, bo))
62 | Some bo -> aux (ctx,bo))
63 | (name, src)::ctx, (NCic.Appl args as bo)
64 when HExtlib.list_last args = NCic.Rel 1 ->
65 let args, _ = HExtlib.split_nth (List.length args - 1) args in
66 (match delift_if_not_occur (NCic.Appl args) with
67 | None -> aux (ctx,NCic.Lambda(name,src, bo))
68 | Some bo -> aux (ctx,bo))
69 | (name, src) :: ctx, t ->
70 aux (ctx,NCic.Lambda(name,src, t))
76 module Ref = NReference;;
78 let debug = ref false;;
83 prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
88 let time1 = Unix.gettimeofday () in
89 indent := !indent ^ String.make 1 c;
90 times := time1 :: !times;
91 prerr_endline ("{{{" ^ !indent ^ " ")
97 let time2 = Unix.gettimeofday () in
99 match !times with time1::tl -> times := tl; time1 | [] -> assert false in
100 prerr_endline ("}}} " ^ !indent ^ " " ^ string_of_float (time2 -. time1));
102 | Some e -> prerr_endline ("exception raised: " ^ Printexc.to_string e)
105 indent := String.sub !indent 0 (String.length !indent -1)
107 Invalid_argument _ -> indent := "??"; ()
111 let ppcontext ~metasenv ~subst c =
112 "\nctx:\n"^ NCicPp.ppcontext ~metasenv ~subst c
114 let ppmetasenv ~subst m = "\nmenv:\n" ^ NCicPp.ppmetasenv ~subst m;;
116 let ppcontext ~metasenv:_metasenv ~subst:_subst _context = "";;
117 let ppmetasenv ~subst:_subst _metasenv = "";;
118 let ppterm ~metasenv ~subst ~context = NCicPp.ppterm ~metasenv ~subst ~context;;
119 (* let ppterm ~metasenv:_ ~subst:_ ~context:_ _ = "";; *)
121 let is_locked n subst =
123 match NCicUtils.lookup_subst n subst with
124 | tag, _,_,_ when NCicMetaSubst.is_out_scope_tag tag -> true
126 with NCicUtils.Subst_not_found _ -> false
129 let rec mk_irl stop base =
130 if base > stop then []
131 else (NCic.Rel base) :: mk_irl stop (base+1)
134 (* the argument must be a term in whd *)
135 let rec could_reduce =
138 | C.Appl (C.Const (Ref.Ref (_,Ref.Fix (_,recno,_)))::args)
139 when List.length args > recno -> could_reduce (List.nth args recno)
140 | C.Match (_,_,arg,_) -> could_reduce arg
141 | C.Appl (he::_) -> could_reduce he
142 | C.Sort _ | C.Rel _ | C.Prod _ | C.Lambda _ | C.Const _ -> false
143 | C.Appl [] | C.LetIn _ | C.Implicit _ -> assert false
146 let rec lambda_intros rdb metasenv subst context argsno ty =
147 pp (lazy ("LAMBDA INTROS: " ^ ppterm ~metasenv ~subst ~context ty));
150 let metasenv, _, bo, _ =
151 NCicMetaSubst.mk_meta metasenv context ~with_type:ty `IsTerm
155 (match NCicReduction.whd ~subst context ty with
158 lambda_intros rdb metasenv subst
159 ((n,C.Decl so)::context) (argsno - 1) ta
161 metasenv,C.Lambda (n,so,bo)
165 let unopt exc = function None -> raise exc | Some x -> x ;;
167 let fix metasenv subst is_sup test_eq_only exc t =
168 (*D*) inside 'f'; try let rc =
169 pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context:[] t));
170 let rec aux test_eq_only metasenv = function
171 | NCic.Prod (n,so,ta) ->
172 let metasenv,so = aux true metasenv so in
173 let metasenv,ta = aux test_eq_only metasenv ta in
174 metasenv,NCic.Prod (n,so,ta)
175 | NCic.Sort (NCic.Type [(`CProp|`Type),_]) as orig when test_eq_only ->
177 | NCic.Sort (NCic.Type _) when test_eq_only -> raise exc
178 | NCic.Sort (NCic.Type u) when is_sup ->
179 metasenv, NCic.Sort (NCic.Type (unopt exc (NCicEnvironment.sup u)))
180 | NCic.Sort (NCic.Type u) ->
181 metasenv, NCic.Sort (NCic.Type
182 (unopt exc (NCicEnvironment.inf ~strict:false u)))
183 | NCic.Meta (n,_) as orig ->
185 let _,_,_,_ = NCicUtils.lookup_subst n subst in metasenv,orig
186 with NCicUtils.Subst_not_found _ ->
187 let metasenv, _ = NCicMetaSubst.extend_meta metasenv n in
190 NCicUntrusted.map_term_fold_a (fun _ x -> x) test_eq_only aux metasenv t
192 aux test_eq_only metasenv t
193 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
196 let metasenv_to_subst n (kind,context,ty) metasenv subst =
197 let infos,metasenv = List.partition (fun (n',_) -> n = n') metasenv in
198 let attrs,octx,oty = match infos with [_,infos] -> infos | _ -> assert false in
199 if octx=context && oty=ty then
200 (n,(NCicUntrusted.set_kind kind attrs, octx, oty))::metasenv,subst
202 let metasenv, _, bo, _ =
203 NCicMetaSubst.mk_meta metasenv context ~attrs ~with_type:ty kind in
204 let subst = (n,(NCicUntrusted.set_kind kind attrs,octx,bo,oty))::subst in
208 let rec sortfy exc metasenv subst context t =
209 let t = NCicReduction.whd ~subst context t in
212 | NCic.Sort _ -> metasenv, subst
214 let attrs, context, ty = NCicUtils.lookup_meta n metasenv in
215 let kind = NCicUntrusted.kind_of_meta attrs in
216 if kind = `IsSort then
220 | NCic.Implicit (`Typeof _) ->
221 metasenv_to_subst n (`IsSort,[],ty) metasenv subst
223 let metasenv,subst,ty = sortfy exc metasenv subst context ty in
224 metasenv_to_subst n (`IsSort,[],ty) metasenv subst)
225 | NCic.Implicit _ -> assert false
230 let tipify exc metasenv subst context t ty =
232 match NCicUntrusted.kind_of_meta attrs with
233 `IsType | `IsSort -> true
236 let rec optimize_meta metasenv subst =
240 let attrs,_,_ = NCicUtils.lookup_meta n metasenv in
241 if is_type attrs then
244 let _,cc,ty = NCicUtils.lookup_meta n metasenv in
245 let metasenv,subst,ty = sortfy exc metasenv subst cc ty in
247 NCicUntrusted.replace_in_metasenv n
248 (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
253 NCicUtils.Meta_not_found _ ->
254 let attrs, _,bo,_ = NCicUtils.lookup_subst n subst in
255 if is_type attrs then
258 let _,cc,_,ty = NCicUtils.lookup_subst n subst in
259 let metasenv,subst,ty = sortfy exc metasenv subst cc ty in
261 NCicUntrusted.replace_in_subst n
262 (fun attrs,cc,bo,_->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
265 optimize_meta metasenv subst (NCicSubstitution.subst_meta lc bo))
266 | _ -> metasenv,subst,false
268 let metasenv,subst,b = optimize_meta metasenv subst t in
272 let metasenv,subst,_ = sortfy exc metasenv subst context ty in
276 let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
277 (*D*) inside 'I'; try let rc =
278 pp (lazy(string_of_int n^" :=?= "^ppterm ~metasenv ~subst ~context t));
280 UnificationFailure (mk_msg metasenv subst context (NCic.Meta (n,lc)) t) in
281 let move_to_subst i ((_,cc,t,_) as infos) metasenv subst =
282 let metasenv = List.remove_assoc i metasenv in
283 pp(lazy(string_of_int n ^ " :==> "^ ppterm ~metasenv ~subst ~context:cc t));
284 metasenv, (i,infos) :: subst
286 let delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv subst =
287 pp (lazy(string_of_int n ^ " := 111 = "^
288 ppterm ~metasenv ~subst ~context t));
289 let (metasenv, subst), t =
292 ~unify:(fun m s c t1 t2 ->
295 try Some (unify rdb test_eq_only m s c t1 t2 false)
296 with UnificationFailure _ | Uncertain _ -> None
299 metasenv subst context n lc t
300 with NCicMetaSubst.Uncertain msg ->
301 pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
302 raise (Uncertain msg)
303 | NCicMetaSubst.MetaSubstFailure msg ->
304 pp (lazy ("delift fails: " ^ Lazy.force msg));
305 raise (UnificationFailure msg)
307 pp (lazy(string_of_int n ^ " := 222 = "^
308 ppterm ~metasenv ~subst ~context:cc t^ppmetasenv ~subst metasenv));
309 (* Unifying the types may have already instantiated n. *)
311 let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
312 let oldt = NCicSubstitution.subst_meta lc oldt in
313 let t = NCicSubstitution.subst_meta lc t in
314 (* conjecture: always fail --> occur check *)
315 unify rdb test_eq_only metasenv subst context t oldt false
316 with NCicUtils.Subst_not_found _ ->
317 move_to_subst n (attrs,cc,t,ty) metasenv subst
319 let attrs,cc,ty = NCicUtils.lookup_meta n metasenv in
320 let kind = NCicUntrusted.kind_of_meta attrs in
321 let metasenv,t = fix metasenv subst swap test_eq_only exc t in
322 let ty_t = NCicTypeChecker.typeof ~metasenv ~subst context t in
323 let metasenv,subst,t =
325 `IsSort -> sortfy exc metasenv subst context t
326 | `IsType -> tipify exc metasenv subst context t ty_t
327 | `IsTerm -> metasenv,subst,t in
331 NCic.Implicit (`Typeof _), NCic.Sort _ ->
332 move_to_subst n (attrs,cc,t,ty_t) metasenv subst
333 | NCic.Sort (NCic.Type u1), NCic.Sort s ->
336 NCic.Type u2, false ->
338 (unopt exc (NCicEnvironment.inf ~strict:false
339 (unopt exc (NCicEnvironment.inf ~strict:true u1) @ u2))))
340 | NCic.Type u2, true ->
341 if NCicEnvironment.universe_lt u2 u1 then
342 NCic.Sort (NCic.Type u2)
344 | NCic.Prop,_ -> NCic.Sort NCic.Prop
346 move_to_subst n (attrs,cc,s,ty) metasenv subst
347 | NCic.Implicit (`Typeof _), NCic.Meta _ ->
348 move_to_subst n (attrs,cc,t,ty_t) metasenv subst
350 | NCic.Meta _, NCic.Sort _ ->
351 pp (lazy ("On the types: " ^
352 ppterm ~metasenv ~subst ~context ty ^ "=<=" ^
353 ppterm ~metasenv ~subst ~context ty_t));
354 let metasenv, subst =
355 unify rdb false metasenv subst context ty_t ty false in
356 delift_to_subst test_eq_only n lc (attrs,cc,ty) t
357 context metasenv subst
362 NCic.Implicit (`Typeof _) ->
363 let (metasenv, subst), ty_t =
366 ~unify:(fun m s c t1 t2 ->
368 let res = try Some (unify rdb test_eq_only m s c t1 t2 false )
369 with UnificationFailure _ | Uncertain _ -> None
372 metasenv subst context n lc ty_t
373 with NCicMetaSubst.Uncertain msg ->
374 pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
375 raise (Uncertain msg)
376 | NCicMetaSubst.MetaSubstFailure msg ->
377 pp (lazy ("delift fails: " ^ Lazy.force msg));
378 raise (UnificationFailure msg)
380 delift_to_subst test_eq_only n lc (attrs,cc,ty_t) t context metasenv
383 let lty = NCicSubstitution.subst_meta lc ty in
384 pp (lazy ("On the types: " ^
385 ppterm ~metasenv ~subst ~context lty ^ "=<=" ^
386 ppterm ~metasenv ~subst ~context ty_t));
387 let metasenv, subst =
388 unify rdb false metasenv subst context ty_t lty false
390 delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv
392 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
394 and unify rdb test_eq_only metasenv subst context t1 t2 swap =
395 (*D*) inside 'U'; try let rc =
396 let fo_unif test_eq_only metasenv subst (norm1,t1) (norm2,t2) =
397 (*D*) inside 'F'; try let rc =
398 pp (lazy(" " ^ ppterm ~metasenv ~subst ~context t1 ^
399 (if swap then " ==>?== "
401 ppterm ~metasenv ~subst ~context t2 ^ ppmetasenv
403 pp (lazy(" " ^ ppterm ~metasenv ~subst:[] ~context t1 ^
404 (if swap then " ==>??== "
406 ppterm ~metasenv ~subst:[] ~context t2 ^ ppmetasenv
410 (* CSC: To speed up Oliboni's stuff. Why is it necessary, anyway?
412 NCicUntrusted.metas_of_term subst context t1 = [] &&
413 NCicUntrusted.metas_of_term subst context t2 = []
415 if NCicReduction.are_convertible ~metasenv ~subst context t1 t2 then
418 raise (UnificationFailure (lazy "Closed terms not convertible"))
422 | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl []
423 | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) ->
424 prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
426 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
427 let a, b = if swap then b,a else a,b in
428 if NCicEnvironment.universe_leq a b then metasenv, subst
429 else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
430 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
431 if NCicEnvironment.universe_eq a b then metasenv, subst
432 else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
433 | (C.Sort C.Prop,C.Sort (C.Type _)) when not swap ->
434 if (not test_eq_only) then metasenv, subst
435 else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
436 | (C.Sort (C.Type _), C.Sort C.Prop) when swap ->
437 if (not test_eq_only) then metasenv, subst
438 else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
440 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
441 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
442 let metasenv, subst = unify rdb true metasenv subst context s1 s2 swap in
443 unify rdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 swap
444 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
445 let metasenv,subst=unify rdb test_eq_only metasenv subst context ty1 ty2 swap in
446 let metasenv,subst=unify rdb test_eq_only metasenv subst context s1 s2 swap in
447 let context = (name1, C.Def (s1,ty1))::context in
448 unify rdb test_eq_only metasenv subst context t1 t2 swap
450 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
452 let l1 = NCicUtils.expand_local_context l1 in
453 let l2 = NCicUtils.expand_local_context l2 in
454 let metasenv, subst, to_restrict, _ =
456 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
458 let metasenv, subst =
459 unify rdb (*test_eq_only*) true metasenv subst context
460 (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
463 metasenv, subst, to_restrict, i-1
464 with UnificationFailure _ | Uncertain _ ->
465 metasenv, subst, i::to_restrict, i-1)
466 l1 l2 (metasenv, subst, [], List.length l1)
468 if to_restrict <> [] then
469 let metasenv, subst, _, _ =
470 NCicMetaSubst.restrict metasenv subst n1 to_restrict
475 | Invalid_argument _ -> assert false
476 | NCicMetaSubst.MetaSubstFailure msg ->
478 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
479 let term1 = NCicSubstitution.subst_meta lc1 term in
480 let term2 = NCicSubstitution.subst_meta lc2 term in
481 unify rdb test_eq_only metasenv subst context term1 term2 swap
482 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
484 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
485 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
488 (fun (metasenv, subst) t1 t2 ->
489 unify rdb (*test_eq_only*) true metasenv subst context t1
491 (metasenv,subst) l1 l2
492 with Invalid_argument _ ->
493 raise (UnificationFailure (mk_msg metasenv subst context t1 t2)))
495 | _, NCic.Meta (n, _) when is_locked n subst && not swap->
496 (let (metasenv, subst), i =
497 match NCicReduction.whd ~subst context t1 with
498 | NCic.Appl (NCic.Meta (i,l) as meta :: args) ->
499 let metasenv, lambda_Mj =
500 lambda_intros rdb metasenv subst context (List.length args)
501 (NCicTypeChecker.typeof ~metasenv ~subst context meta)
503 unify rdb test_eq_only metasenv subst context
504 (C.Meta (i,l)) lambda_Mj false,
506 | NCic.Meta (i,_) -> (metasenv, subst), i
508 raise (UnificationFailure (lazy "Locked term vs non
509 flexible term; probably not saturated enough yet!"))
511 let t1 = NCicReduction.whd ~subst context t1 in
513 match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
515 let metasenv, subst =
516 instantiate rdb test_eq_only metasenv subst context j lj t2 true
518 (* We need to remove the out_scope_tags to avoid propagation of
519 them that triggers again the ad-hoc case *)
521 List.map (fun (i,(tag,ctx,bo,ty)) ->
524 (function `InScope | `OutScope _ -> false | _ -> true) tag
530 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
531 let term = eta_reduce subst term in
532 let subst = List.filter (fun (j,_) -> j <> i) subst in
533 metasenv, ((i, (name, ctx, term, ty)) :: subst)
534 with Not_found -> assert false))
535 | NCic.Meta (n, _), _ when is_locked n subst && swap ->
536 unify rdb test_eq_only metasenv subst context t2 t1 false
538 | t, C.Meta (n,lc) when List.mem_assoc n subst ->
539 let _,_,term,_ = NCicUtils.lookup_subst n subst in
540 let term = NCicSubstitution.subst_meta lc term in
541 unify rdb test_eq_only metasenv subst context t term swap
542 | C.Meta (n,_), _ when List.mem_assoc n subst ->
543 unify rdb test_eq_only metasenv subst context t2 t1 (not swap)
545 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
546 let _,_,term,_ = NCicUtils.lookup_subst i subst in
547 let term = NCicSubstitution.subst_meta l term in
548 unify rdb test_eq_only metasenv subst context t1
549 (mk_appl ~upto:(List.length args) term args) swap
550 | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
551 unify rdb test_eq_only metasenv subst context t2 t1 (not swap)
553 | C.Meta (n,_), C.Meta (m,lc') when
554 let _,cc1,_ = NCicUtils.lookup_meta n metasenv in
555 let _,cc2,_ = NCicUtils.lookup_meta m metasenv in
556 (n < m && cc1 = cc2) ||
557 let len1 = List.length cc1 in
558 let len2 = List.length cc2 in
559 len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
560 instantiate rdb test_eq_only metasenv subst context m lc'
561 (NCicReduction.head_beta_reduce ~subst t1) (not swap)
562 | C.Meta (n,lc), t ->
563 instantiate rdb test_eq_only metasenv subst context n lc
564 (NCicReduction.head_beta_reduce ~subst t) swap
565 | t, C.Meta (n,lc) ->
566 instantiate rdb test_eq_only metasenv subst context n lc
567 (NCicReduction.head_beta_reduce ~subst t) (not swap)
569 | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
570 let metasenv, lambda_Mj =
571 lambda_intros rdb metasenv subst context (List.length args)
572 (NCicTypeChecker.typeof ~metasenv ~subst context meta)
574 let metasenv, subst =
575 unify rdb test_eq_only metasenv subst context
576 (C.Meta (i,l)) lambda_Mj swap
578 let metasenv, subst =
579 unify rdb test_eq_only metasenv subst context t1 t2 swap
582 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
583 let term = eta_reduce subst term in
584 let subst = List.filter (fun (j,_) -> j <> i) subst in
585 metasenv, ((i, (name, ctx, term, ty)) :: subst)
586 with Not_found -> assert false)
587 | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
588 unify rdb test_eq_only metasenv subst context t2 t1 (not swap)
590 (* processing this case here we avoid a useless small delta step *)
591 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
593 let relevance = NCicEnvironment.get_relevance r1 in
594 let metasenv, subst, _ =
597 (fun (metasenv, subst, relevance) t1 t2 ->
599 match relevance with b::tl -> b,tl | _ -> true, [] in
600 let metasenv, subst =
601 try unify rdb test_eq_only metasenv subst context t1 t2
603 with UnificationFailure _ | Uncertain _ when not b ->
606 metasenv, subst, relevance)
607 (metasenv, subst, relevance) tl1 tl2
609 Invalid_argument _ ->
610 raise (Uncertain (mk_msg metasenv subst context t1 t2))
611 | KeepReducing _ | KeepReducingThis _ -> assert false
615 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
616 C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
617 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
618 let _,_,ty,_ = List.nth itl tyno in
619 let rec remove_prods ~subst context ty =
620 let ty = NCicReduction.whd ~subst context ty in
623 | C.Prod (name,so,ta) ->
624 remove_prods ~subst ((name,(C.Decl so))::context) ta
628 match remove_prods ~subst [] ty with
629 | C.Sort C.Prop -> true
632 (* if not (Ref.eq ref1 ref2) then
633 raise (Uncertain (mk_msg metasenv subst context t1 t2))
635 let metasenv, subst =
636 unify rdb test_eq_only metasenv subst context outtype1 outtype2 swap in
637 let metasenv, subst =
638 try unify rdb test_eq_only metasenv subst context term1 term2 swap
639 with UnificationFailure _ | Uncertain _ when is_prop ->
644 (fun (metasenv,subst) t1 t2 ->
645 unify rdb test_eq_only metasenv subst context t1 t2 swap)
646 (metasenv, subst) pl1 pl2
647 with Invalid_argument _ -> assert false)
648 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
649 | _ when norm1 && norm2 ->
650 if (could_reduce t1 || could_reduce t2) then
651 raise (Uncertain (mk_msg metasenv subst context t1 t2))
653 raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
654 | _ -> raise (KeepReducing (mk_msg metasenv subst context t1 t2))
655 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
657 let fo_unif test_eq_only metasenv subst (norm1,t1 as nt1) (norm2,t2 as nt2)=
658 try fo_unif test_eq_only metasenv subst nt1 nt2
660 UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
661 raise (KeepReducing (mk_msg metasenv subst context t1 t2))
663 let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
664 if NCicUntrusted.metas_of_term subst context t1 = [] &&
665 NCicUntrusted.metas_of_term subst context t2 = []
668 (*D*) inside 'H'; try let rc =
669 pp(lazy ("\nProblema:\n" ^
670 ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
671 ppterm ~metasenv ~subst ~context t2));
673 NCicUnifHint.look_for_hint rdb metasenv subst context t1 t2
675 let rec cand_iter = function
676 | [] -> None (* raise exc *)
677 | (metasenv,(c1,c2),premises)::tl ->
678 pp (lazy ("\nProvo il candidato:\n" ^
682 ppterm ~metasenv ~subst ~context a ^ " =?= " ^
683 ppterm ~metasenv ~subst ~context b) premises) ^
684 "\n-------------------------------------------\n"^
685 ppterm ~metasenv ~subst ~context c1 ^ " = " ^
686 ppterm ~metasenv ~subst ~context c2));
688 (*D*) inside 'K'; try let rc =
690 fo_unif test_eq_only metasenv subst mt1 (false,c1) in
692 fo_unif test_eq_only metasenv subst (false,c2) mt2 in
695 (fun (metasenv, subst) (x,y) ->
696 unify rdb test_eq_only metasenv subst context x y false)
697 (metasenv, subst) (List.rev premises)
699 pp(lazy("FUNZIONA!"));
700 Some (metasenv, subst)
701 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
703 KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
704 | KeepReducingThis _ -> assert false
707 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
710 let put_in_whd m1 m2 =
711 NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
712 NCicReduction.reduce_machine ~delta:max_int ~subst context m2
714 let fo_unif_w_hints test_eq_only metasenv subst (_,t1 as m1) (_,t2 as m2) =
715 try fo_unif test_eq_only metasenv subst m1 m2
717 | UnificationFailure _ as exn -> raise exn
718 | KeepReducing _ | Uncertain _ as exn ->
719 let (t1,norm1 as tm1),(t2,norm2 as tm2) =
720 put_in_whd (0,[],t1,[]) (0,[],t2,[])
723 try_hints metasenv subst
724 (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
729 | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2))
730 | Uncertain _ as exn -> raise exn
733 let fo_unif_heads_and_cont_or_unwind_and_hints
734 test_eq_only metasenv subst m1 m2 cont hm1 hm2
736 let ms, continuation =
737 (* calling the continuation inside the outermost try is an option
738 and makes unification stronger, but looks not frequent to me
739 that heads unify but not the arguments and that an hints can fix
741 try fo_unif test_eq_only metasenv subst m1 m2, cont
743 | UnificationFailure _
744 | KeepReducing _ | Uncertain _ as exn ->
745 let (t1,norm1),(t2,norm2) = hm1, hm2 in
747 try_hints metasenv subst
748 (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
750 | Some x -> x, fun x -> x
753 | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
754 | UnificationFailure _ | Uncertain _ as exn -> raise exn
759 let height_of = function
760 | NCic.Const (Ref.Ref (_,Ref.Def h))
761 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
762 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
763 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
766 let small_delta_step ~subst
767 ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
769 assert (not (norm1 && norm2));
771 x1,NCicReduction.reduce_machine ~delta:0 ~subst context m2
773 NCicReduction.reduce_machine ~delta:0 ~subst context m1,x2
775 let h1 = height_of t1 in
776 let h2 = height_of t2 in
777 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
778 NCicReduction.reduce_machine ~delta ~subst context m1,
779 NCicReduction.reduce_machine ~delta ~subst context m2
781 let rec unif_machines metasenv subst =
783 | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
784 (*D*) inside 'M'; try let rc =
786 ppterm ~metasenv ~subst ~context
787 (NCicReduction.unwind (k1,e1,t1,s1)) ^
789 ppterm ~metasenv ~subst ~context
790 (NCicReduction.unwind (k2,e2,t2,s2))));
791 pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
792 let relevance = [] (* TO BE UNDERSTOOD
794 | C.Const r -> NCicEnvironment.get_relevance r
796 let unif_from_stack (metasenv, subst) (t1, t2, b) =
798 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
799 let t2 = NCicReduction.from_stack ~delta:max_int t2 in
800 unif_machines metasenv subst (put_in_whd t1 t2)
801 with UnificationFailure _ | Uncertain _ when not b ->
804 let rec check_stack l1 l2 r todo =
806 | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
807 | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
809 NCicReduction.unwind (k1,e1,t1,List.rev l1),
810 NCicReduction.unwind (k2,e2,t2,List.rev l2),
813 let check_stack l1 l2 r =
815 | NCic.Meta _, _ | _, NCic.Meta _ ->
816 (NCicReduction.unwind (k1,e1,t1,s1)),
817 (NCicReduction.unwind (k2,e2,t2,s2)),[]
818 | _ -> check_stack l1 l2 r []
820 let hh1,hh2,todo = check_stack (List.rev s1) (List.rev s2) relevance in
822 fo_unif_heads_and_cont_or_unwind_and_hints
823 test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
824 (fun ms -> List.fold_left unif_from_stack ms todo)
827 | KeepReducing _ -> assert false
828 | KeepReducingThis _ ->
829 assert (not (norm1 && norm2));
830 unif_machines metasenv subst (small_delta_step ~subst m1 m2)
831 | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
832 -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
833 | UnificationFailure msg
834 when could_reduce (NCicReduction.unwind (fst m1))
835 || could_reduce (NCicReduction.unwind (fst m2))
836 -> raise (Uncertain msg)
837 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
839 try fo_unif_w_hints test_eq_only metasenv subst (false,t1) (false,t2)
841 | KeepReducingThis (msg,tm1,tm2) ->
843 unif_machines metasenv subst (tm1,tm2)
845 | UnificationFailure _ -> raise (UnificationFailure msg)
846 | Uncertain _ -> raise (Uncertain msg)
847 | KeepReducing _ -> assert false)
848 | KeepReducing _ -> assert false
850 (*D*) in outside None; rc with KeepReducing _ -> assert false | exn -> outside (Some exn); raise exn
852 and delift_type_wrt_terms rdb metasenv subst context t args =
853 let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
854 let (metasenv, subst), t =
857 ~unify:(fun m s c t1 t2 ->
860 try Some (unify rdb false m s c t1 t2 false)
861 with UnificationFailure _ | Uncertain _ -> None
864 metasenv subst context 0 (0,NCic.Ctx lc) t
866 NCicMetaSubst.MetaSubstFailure _
867 | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t
873 let unify rdb ?(test_eq_only=false) ?(swap=false) metasenv subst context t1 t2=
875 unify rdb test_eq_only metasenv subst context t1 t2 swap;;
878 fix m s true false (UnificationFailure (lazy "no sup"))