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 (* higher order unification case *)
570 | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
571 (* this easy_case handles "(? ?) =?= (f a)", same number of
572 * args, preferring the instantiation "f" over "\_.f a" for the
573 * metavariable in head position. Since the arguments of the meta
574 * are flexible, delift would ignore them generating a constant
575 * function even in the easy case above *)
578 | NCic.Appl (f :: f_args)
579 when List.length args = List.length f_args &&
580 List.exists (NCicMetaSubst.is_flexible context ~subst) args ->
582 let metasenv, subst =
583 unify rdb test_eq_only metasenv subst context meta f swap
585 Some (List.fold_left2
587 unify rdb test_eq_only m s context t1 t2 swap)
588 (metasenv, subst) args f_args)
589 with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
593 (match easy_case with
596 (* This case handles "(?_f ..ti..) =?= t2", abstracting every
597 * non flexible ti (delift skips local context items that are
598 * flexible) from t2 in two steps:
599 * 1) ?_f := \..xi.. .?
600 * 2) ?_f ..ti.. =?= t2 --unif_machines-->
601 ?_f[..ti..] =?= t2 --instantiate-->
602 delift [..ti..] t2 *)
603 let metasenv, lambda_Mj =
604 lambda_intros rdb metasenv subst context (List.length args)
605 (NCicTypeChecker.typeof ~metasenv ~subst context meta)
607 let metasenv, subst =
608 unify rdb test_eq_only metasenv subst context
609 (C.Meta (i,l)) lambda_Mj swap
611 let metasenv, subst =
612 unify rdb test_eq_only metasenv subst context t1 t2 swap
615 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
616 let term = eta_reduce subst term in
617 let subst = List.filter (fun (j,_) -> j <> i) subst in
618 metasenv, ((i, (name, ctx, term, ty)) :: subst)
619 with Not_found -> assert false))
621 | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
622 unify rdb test_eq_only metasenv subst context t2 t1 (not swap)
624 (* processing this case here we avoid a useless small delta step *)
625 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
627 let relevance = NCicEnvironment.get_relevance r1 in
628 let metasenv, subst, _ =
631 (fun (metasenv, subst, relevance) t1 t2 ->
633 match relevance with b::tl -> b,tl | _ -> true, [] in
634 let metasenv, subst =
635 try unify rdb test_eq_only metasenv subst context t1 t2
637 with UnificationFailure _ | Uncertain _ when not b ->
640 metasenv, subst, relevance)
641 (metasenv, subst, relevance) tl1 tl2
643 Invalid_argument _ ->
644 raise (Uncertain (mk_msg metasenv subst context t1 t2))
645 | KeepReducing _ | KeepReducingThis _ -> assert false
649 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
650 C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
651 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
652 let _,_,ty,_ = List.nth itl tyno in
653 let rec remove_prods ~subst context ty =
654 let ty = NCicReduction.whd ~subst context ty in
657 | C.Prod (name,so,ta) ->
658 remove_prods ~subst ((name,(C.Decl so))::context) ta
662 match remove_prods ~subst [] ty with
663 | C.Sort C.Prop -> true
666 (* if not (Ref.eq ref1 ref2) then
667 raise (Uncertain (mk_msg metasenv subst context t1 t2))
669 let metasenv, subst =
670 unify rdb test_eq_only metasenv subst context outtype1 outtype2 swap in
671 let metasenv, subst =
672 try unify rdb test_eq_only metasenv subst context term1 term2 swap
673 with UnificationFailure _ | Uncertain _ when is_prop ->
678 (fun (metasenv,subst) t1 t2 ->
679 unify rdb test_eq_only metasenv subst context t1 t2 swap)
680 (metasenv, subst) pl1 pl2
681 with Invalid_argument _ -> assert false)
682 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
683 | _ when norm1 && norm2 ->
684 if (could_reduce t1 || could_reduce t2) then
685 raise (Uncertain (mk_msg metasenv subst context t1 t2))
687 raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
688 | _ -> raise (KeepReducing (mk_msg metasenv subst context t1 t2))
689 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
691 let fo_unif test_eq_only metasenv subst (norm1,t1 as nt1) (norm2,t2 as nt2)=
692 try fo_unif test_eq_only metasenv subst nt1 nt2
694 UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
695 raise (KeepReducing (mk_msg metasenv subst context t1 t2))
697 let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
698 if NCicUntrusted.metas_of_term subst context t1 = [] &&
699 NCicUntrusted.metas_of_term subst context t2 = []
702 (*D*) inside 'H'; try let rc =
703 pp(lazy ("\nProblema:\n" ^
704 ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
705 ppterm ~metasenv ~subst ~context t2));
707 NCicUnifHint.look_for_hint rdb metasenv subst context t1 t2
709 let rec cand_iter = function
710 | [] -> None (* raise exc *)
711 | (metasenv,(c1,c2),premises)::tl ->
712 pp (lazy ("\nProvo il candidato:\n" ^
716 ppterm ~metasenv ~subst ~context a ^ " =?= " ^
717 ppterm ~metasenv ~subst ~context b) premises) ^
718 "\n-------------------------------------------\n"^
719 ppterm ~metasenv ~subst ~context c1 ^ " = " ^
720 ppterm ~metasenv ~subst ~context c2));
722 (*D*) inside 'K'; try let rc =
724 fo_unif test_eq_only metasenv subst mt1 (false,c1) in
726 fo_unif test_eq_only metasenv subst (false,c2) mt2 in
729 (fun (metasenv, subst) (x,y) ->
730 unify rdb test_eq_only metasenv subst context x y false)
731 (metasenv, subst) (List.rev premises)
733 pp(lazy("FUNZIONA!"));
734 Some (metasenv, subst)
735 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
737 KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
738 | KeepReducingThis _ -> assert false
741 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
744 let put_in_whd m1 m2 =
745 NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
746 NCicReduction.reduce_machine ~delta:max_int ~subst context m2
748 let fo_unif_w_hints test_eq_only metasenv subst (_,t1 as m1) (_,t2 as m2) =
749 try fo_unif test_eq_only metasenv subst m1 m2
751 | UnificationFailure _ as exn -> raise exn
752 | KeepReducing _ | Uncertain _ as exn ->
753 let (t1,norm1 as tm1),(t2,norm2 as tm2) =
754 put_in_whd (0,[],t1,[]) (0,[],t2,[])
757 try_hints metasenv subst
758 (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
763 | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2))
764 | Uncertain _ as exn -> raise exn
767 let fo_unif_heads_and_cont_or_unwind_and_hints
768 test_eq_only metasenv subst m1 m2 cont hm1 hm2
770 let ms, continuation =
771 (* calling the continuation inside the outermost try is an option
772 and makes unification stronger, but looks not frequent to me
773 that heads unify but not the arguments and that an hints can fix
775 try fo_unif test_eq_only metasenv subst m1 m2, cont
777 | UnificationFailure _
778 | KeepReducing _ | Uncertain _ as exn ->
779 let (t1,norm1),(t2,norm2) = hm1, hm2 in
781 try_hints metasenv subst
782 (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
784 | Some x -> x, fun x -> x
787 | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
788 | UnificationFailure _ | Uncertain _ as exn -> raise exn
793 let height_of = function
794 | NCic.Const (Ref.Ref (_,Ref.Def h))
795 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
796 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
797 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
800 let small_delta_step ~subst
801 ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
803 assert (not (norm1 && norm2));
805 x1,NCicReduction.reduce_machine ~delta:0 ~subst context m2
807 NCicReduction.reduce_machine ~delta:0 ~subst context m1,x2
809 let h1 = height_of t1 in
810 let h2 = height_of t2 in
811 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
812 NCicReduction.reduce_machine ~delta ~subst context m1,
813 NCicReduction.reduce_machine ~delta ~subst context m2
815 let rec unif_machines metasenv subst =
817 | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
818 (*D*) inside 'M'; try let rc =
820 ppterm ~metasenv ~subst ~context
821 (NCicReduction.unwind (k1,e1,t1,s1)) ^
823 ppterm ~metasenv ~subst ~context
824 (NCicReduction.unwind (k2,e2,t2,s2))));
825 pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
828 | C.Const r -> NCicEnvironment.get_relevance r
830 let unif_from_stack (metasenv, subst) (t1, t2, b) =
832 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
833 let t2 = NCicReduction.from_stack ~delta:max_int t2 in
834 unif_machines metasenv subst (put_in_whd t1 t2)
835 with UnificationFailure _ | Uncertain _ when not b ->
838 let rec check_stack l1 l2 r todo =
840 | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
841 | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
843 NCicReduction.unwind (k1,e1,t1,List.rev l1),
844 NCicReduction.unwind (k2,e2,t2,List.rev l2),
847 let check_stack l1 l2 r =
849 | NCic.Meta _, _ | _, NCic.Meta _ ->
850 (NCicReduction.unwind (k1,e1,t1,s1)),
851 (NCicReduction.unwind (k2,e2,t2,s2)),[]
852 | _ -> check_stack l1 l2 r []
855 check_stack (List.rev s1) (List.rev s2) (List.rev relevance) in
857 fo_unif_heads_and_cont_or_unwind_and_hints
858 test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
859 (fun ms -> List.fold_left unif_from_stack ms todo)
862 | KeepReducing _ -> assert false
863 | KeepReducingThis _ ->
864 assert (not (norm1 && norm2));
865 unif_machines metasenv subst (small_delta_step ~subst m1 m2)
866 | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
867 -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
868 | UnificationFailure msg
869 when could_reduce (NCicReduction.unwind (fst m1))
870 || could_reduce (NCicReduction.unwind (fst m2))
871 -> raise (Uncertain msg)
872 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
874 try fo_unif_w_hints test_eq_only metasenv subst (false,t1) (false,t2)
876 | KeepReducingThis (msg,tm1,tm2) ->
878 unif_machines metasenv subst (tm1,tm2)
880 | UnificationFailure _ -> raise (UnificationFailure msg)
881 | Uncertain _ -> raise (Uncertain msg)
882 | KeepReducing _ -> assert false)
883 | KeepReducing _ -> assert false
885 (*D*) in outside None; rc with KeepReducing _ -> assert false | exn -> outside (Some exn); raise exn
887 and delift_type_wrt_terms rdb metasenv subst context t args =
888 let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
889 let (metasenv, subst), t =
892 ~unify:(fun m s c t1 t2 ->
895 try Some (unify rdb false m s c t1 t2 false)
896 with UnificationFailure _ | Uncertain _ -> None
899 metasenv subst context 0 (0,NCic.Ctx lc) t
901 NCicMetaSubst.MetaSubstFailure _
902 | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t
908 let unify rdb ?(test_eq_only=false) ?(swap=false) metasenv subst context t1 t2=
910 unify rdb test_eq_only metasenv subst context t1 t2 swap;;
913 fix m s true false (UnificationFailure (lazy "no sup"))