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 (status:#NCic.status) metasenv subst context t1 t2 =
26 "Can't unify " ^ status#ppterm ~metasenv ~subst ~context t1 ^
27 " with " ^ status#ppterm ~metasenv ~subst ~context t2))
29 let mk_appl status ~upto hd tl =
30 NCicReduction.head_beta_reduce status ~upto
32 | NCic.Appl l -> NCic.Appl (l@tl)
33 | _ -> NCic.Appl (hd :: tl))
36 exception WrongShape;;
38 let eta_reduce status subst t =
39 let delift_if_not_occur body =
41 Some (NCicSubstitution.psubst status ~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 status 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 (UnificationFailure msg) -> prerr_endline ("exception raised: NCicUnification.UnificationFailure:" ^ Lazy.force msg)
103 | Some (Uncertain msg) -> prerr_endline ("exception raised: NCicUnification.Uncertain:" ^ Lazy.force msg)
104 | Some e -> prerr_endline ("exception raised: " ^ Printexc.to_string e)
107 indent := String.sub !indent 0 (String.length !indent -1)
109 Invalid_argument _ -> indent := "??"; ()
113 let ppcontext status ~metasenv ~subst c =
114 "\nctx:\n"^ status#ppcontext ~metasenv ~subst c
116 let ppmetasenv status ~subst m = "\nmenv:\n" ^ status#ppmetasenv ~subst m;;
118 let ppcontext _status ~metasenv:_metasenv ~subst:_subst _context = "";;
119 let ppmetasenv _status ~subst:_subst _metasenv = "";;
120 let ppterm (status:#NCic.status) ~metasenv ~subst ~context = status#ppterm ~metasenv ~subst ~context;;
121 (* let ppterm status ~metasenv:_ ~subst:_ ~context:_ _ = "";; *)
123 let is_locked n subst =
125 match NCicUtils.lookup_subst n subst with
126 | tag, _,_,_ when NCicMetaSubst.is_out_scope_tag tag -> true
128 with NCicUtils.Subst_not_found _ -> false
131 let rec mk_irl stop base =
132 if base > stop then []
133 else (NCic.Rel base) :: mk_irl stop (base+1)
136 (* the argument must be a term in whd *)
137 let rec could_reduce =
140 | C.Appl (C.Const (Ref.Ref (_,Ref.Fix (_,recno,_)))::args)
141 when List.length args > recno -> could_reduce (List.nth args recno)
142 | C.Match (_,_,arg,_) -> could_reduce arg
143 | C.Appl (he::_) -> could_reduce he
144 | C.Sort _ | C.Rel _ | C.Prod _ | C.Lambda _ | C.Const _ -> false
145 | C.Appl [] | C.LetIn _ | C.Implicit _ -> assert false
148 let rec lambda_intros status metasenv subst context argsno ty =
149 pp (lazy ("LAMBDA INTROS: " ^ ppterm status ~metasenv ~subst ~context ty));
152 let metasenv, _, bo, _ =
153 NCicMetaSubst.mk_meta metasenv context ~with_type:ty `IsTerm
157 (match NCicReduction.whd status ~subst context ty with
160 lambda_intros status metasenv subst
161 ((n,C.Decl so)::context) (argsno - 1) ta
163 metasenv,C.Lambda (n,so,bo)
167 let unopt exc = function None -> raise exc | Some x -> x ;;
169 let fix (status:#NCic.status) metasenv subst is_sup test_eq_only exc t =
170 (*D*) inside 'f'; try let rc =
171 pp (lazy (status#ppterm ~metasenv ~subst ~context:[] t));
172 let rec aux test_eq_only metasenv = function
173 | NCic.Prod (n,so,ta) ->
174 let metasenv,so = aux true metasenv so in
175 let metasenv,ta = aux test_eq_only metasenv ta in
176 metasenv,NCic.Prod (n,so,ta)
177 | NCic.Sort (NCic.Type [(`CProp|`Type),_]) as orig when test_eq_only ->
179 | NCic.Sort (NCic.Type _) when test_eq_only -> raise exc
180 | NCic.Sort (NCic.Type u) when is_sup ->
181 metasenv, NCic.Sort (NCic.Type (unopt exc (NCicEnvironment.sup u)))
182 | NCic.Sort (NCic.Type u) ->
183 metasenv, NCic.Sort (NCic.Type
184 (unopt exc (NCicEnvironment.inf ~strict:false u)))
185 | NCic.Meta (n,_) as orig ->
187 let _,_,_,_ = NCicUtils.lookup_subst n subst in metasenv,orig
188 with NCicUtils.Subst_not_found _ ->
189 let metasenv, _ = NCicMetaSubst.extend_meta metasenv n in
192 NCicUntrusted.map_term_fold_a status (fun _ x -> x) test_eq_only aux metasenv t
194 aux test_eq_only metasenv t
195 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
198 let metasenv_to_subst n (kind,context,ty) metasenv subst =
199 let infos,metasenv = List.partition (fun (n',_) -> n = n') metasenv in
200 let attrs,octx,oty = match infos with [_,infos] -> infos | _ -> assert false in
201 if octx=context && oty=ty then
202 (n,(NCicUntrusted.set_kind kind attrs, octx, oty))::metasenv,subst
204 let metasenv, _, bo, _ =
205 NCicMetaSubst.mk_meta metasenv context ~attrs ~with_type:ty kind in
206 let subst = (n,(NCicUntrusted.set_kind kind attrs,octx,bo,oty))::subst in
210 let rec sortfy status exc metasenv subst context t =
211 let t = NCicReduction.whd status ~subst context t in
214 | NCic.Sort _ -> metasenv, subst
216 let attrs, context, ty = NCicUtils.lookup_meta n metasenv in
217 let kind = NCicUntrusted.kind_of_meta attrs in
218 if kind = `IsSort then
222 | NCic.Implicit (`Typeof _) ->
223 metasenv_to_subst n (`IsSort,[],ty) metasenv subst
225 let metasenv,subst,ty = sortfy status exc metasenv subst context ty in
226 metasenv_to_subst n (`IsSort,[],ty) metasenv subst)
227 | NCic.Implicit _ -> assert false
232 let tipify status exc metasenv subst context t ty =
234 match NCicUntrusted.kind_of_meta attrs with
235 `IsType | `IsSort -> true
238 let rec optimize_meta metasenv subst =
242 let attrs,_,_ = NCicUtils.lookup_meta n metasenv in
243 if is_type attrs then
246 let _,cc,ty = NCicUtils.lookup_meta n metasenv in
247 let metasenv,subst,ty = sortfy status exc metasenv subst cc ty in
249 NCicUntrusted.replace_in_metasenv n
250 (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
255 NCicUtils.Meta_not_found _ ->
256 let attrs, _,bo,_ = NCicUtils.lookup_subst n subst in
257 if is_type attrs then
260 let _,cc,_,ty = NCicUtils.lookup_subst n subst in
261 let metasenv,subst,ty = sortfy status exc metasenv subst cc ty in
263 NCicUntrusted.replace_in_subst n
264 (fun attrs,cc,bo,_->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
267 optimize_meta metasenv subst (NCicSubstitution.subst_meta status lc bo))
268 | _ -> metasenv,subst,false
270 let metasenv,subst,b = optimize_meta metasenv subst t in
274 let metasenv,subst,_ = sortfy status exc metasenv subst context ty in
278 let rec instantiate status test_eq_only metasenv subst context n lc t swap =
279 (*D*) inside 'I'; try let rc =
280 pp (lazy(string_of_int n^" :=?= "^ppterm status ~metasenv ~subst ~context t));
282 UnificationFailure (mk_msg status metasenv subst context (NCic.Meta (n,lc)) t) in
283 let move_to_subst i ((_,cc,t,_) as infos) metasenv subst =
284 let metasenv = List.remove_assoc i metasenv in
285 pp(lazy(string_of_int n ^ " :==> "^ ppterm status ~metasenv ~subst ~context:cc t));
286 metasenv, (i,infos) :: subst
288 let delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv subst =
289 pp (lazy(string_of_int n ^ " := 111 = "^
290 ppterm status ~metasenv ~subst ~context t));
291 let (metasenv, subst), t =
293 NCicMetaSubst.delift status
294 ~unify:(fun m s c t1 t2 ->
297 try Some (unify status test_eq_only m s c t1 t2 false)
298 with UnificationFailure _ | Uncertain _ -> None
301 metasenv subst context n lc t
302 with NCicMetaSubst.Uncertain msg ->
303 pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
304 raise (Uncertain msg)
305 | NCicMetaSubst.MetaSubstFailure msg ->
306 pp (lazy ("delift fails: " ^ Lazy.force msg));
307 raise (UnificationFailure msg)
309 pp (lazy(string_of_int n ^ " := 222 = "^
310 ppterm status ~metasenv ~subst ~context:cc t^ppmetasenv status ~subst metasenv));
311 (* Unifying the types may have already instantiated n. *)
313 let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
314 let oldt = NCicSubstitution.subst_meta status lc oldt in
315 let t = NCicSubstitution.subst_meta status lc t in
316 (* conjecture: always fail --> occur check *)
317 unify status test_eq_only metasenv subst context t oldt false
318 with NCicUtils.Subst_not_found _ ->
319 move_to_subst n (attrs,cc,t,ty) metasenv subst
321 let attrs,cc,ty = NCicUtils.lookup_meta n metasenv in
322 let kind = NCicUntrusted.kind_of_meta attrs in
323 let metasenv,t = fix status metasenv subst swap test_eq_only exc t in
324 let ty_t = NCicTypeChecker.typeof status ~metasenv ~subst context t in
325 let metasenv,subst,t =
327 `IsSort -> sortfy status exc metasenv subst context t
328 | `IsType -> tipify status exc metasenv subst context t ty_t
329 | `IsTerm -> metasenv,subst,t in
333 NCic.Implicit (`Typeof _), NCic.Sort _ ->
334 move_to_subst n (attrs,cc,t,ty_t) metasenv subst
335 | NCic.Sort (NCic.Type u1), NCic.Sort s ->
338 NCic.Type u2, false ->
340 (unopt exc (NCicEnvironment.inf ~strict:false
341 (unopt exc (NCicEnvironment.inf ~strict:true u1) @ u2))))
342 | NCic.Type u2, true ->
343 if NCicEnvironment.universe_lt u2 u1 then
344 NCic.Sort (NCic.Type u2)
346 | NCic.Prop,_ -> NCic.Sort NCic.Prop
348 move_to_subst n (attrs,cc,s,ty) metasenv subst
349 | NCic.Implicit (`Typeof _), NCic.Meta _ ->
350 move_to_subst n (attrs,cc,t,ty_t) metasenv subst
352 | NCic.Meta _, NCic.Sort _ ->
353 pp (lazy ("On the types: " ^
354 ppterm status ~metasenv ~subst ~context ty ^ "=<=" ^
355 ppterm status ~metasenv ~subst ~context ty_t));
356 let metasenv, subst =
357 unify status false metasenv subst context ty_t ty false in
358 delift_to_subst test_eq_only n lc (attrs,cc,ty) t
359 context metasenv subst
364 NCic.Implicit (`Typeof _) ->
365 let (metasenv, subst), ty_t =
367 NCicMetaSubst.delift status
368 ~unify:(fun m s c t1 t2 ->
370 let res = try Some (unify status test_eq_only m s c t1 t2 false )
371 with UnificationFailure _ | Uncertain _ -> None
374 metasenv subst context n lc ty_t
375 with NCicMetaSubst.Uncertain msg ->
376 pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
377 raise (Uncertain msg)
378 | NCicMetaSubst.MetaSubstFailure msg ->
379 pp (lazy ("delift fails: " ^ Lazy.force msg));
380 raise (UnificationFailure msg)
382 delift_to_subst test_eq_only n lc (attrs,cc,ty_t) t context metasenv
385 let lty = NCicSubstitution.subst_meta status lc ty in
386 pp (lazy ("On the types: " ^
387 ppterm status ~metasenv ~subst ~context ty_t ^ "=<=" ^
388 ppterm status ~metasenv ~subst ~context lty));
389 let metasenv, subst =
390 unify status false metasenv subst context ty_t lty false
392 delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv
394 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
396 and unify status test_eq_only metasenv subst context t1 t2 swap =
397 (*D*) inside 'U'; try let rc =
398 let fo_unif test_eq_only metasenv subst (norm1,t1) (norm2,t2) =
399 (*D*) inside 'F'; try let rc =
400 pp (lazy(" " ^ ppterm status ~metasenv ~subst ~context t1 ^
401 (if swap then " ==>?== "
403 ppterm status ~metasenv ~subst ~context t2 ^ ppmetasenv status
405 pp (lazy(" " ^ ppterm status ~metasenv ~subst:[] ~context t1 ^
406 (if swap then " ==>??== "
408 ppterm status ~metasenv ~subst:[] ~context t2 ^ ppmetasenv status
412 (* CSC: To speed up Oliboni's stuff. Why is it necessary, anyway?
414 NCicUntrusted.metas_of_term subst context t1 = [] &&
415 NCicUntrusted.metas_of_term subst context t2 = []
417 if NCicReduction.are_convertible ~metasenv ~subst context t1 t2 then
420 raise (UnificationFailure (lazy "Closed terms not convertible"))
424 | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl []
425 | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) ->
426 prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
428 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
429 let a, b = if swap then b,a else a,b in
430 if NCicEnvironment.universe_leq a b then metasenv, subst
431 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
432 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
433 if NCicEnvironment.universe_eq a b then metasenv, subst
434 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
435 | (C.Sort C.Prop,C.Sort (C.Type _)) when not swap ->
436 if (not test_eq_only) then metasenv, subst
437 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
438 | (C.Sort (C.Type _), C.Sort C.Prop) when swap ->
439 if (not test_eq_only) then metasenv, subst
440 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
442 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
443 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
444 let metasenv, subst = unify status true metasenv subst context s1 s2 swap in
445 unify status test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 swap
446 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
447 let metasenv,subst=unify status test_eq_only metasenv subst context ty1 ty2 swap in
448 let metasenv,subst=unify status test_eq_only metasenv subst context s1 s2 swap in
449 let context = (name1, C.Def (s1,ty1))::context in
450 unify status test_eq_only metasenv subst context t1 t2 swap
452 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
454 let l1 = NCicUtils.expand_local_context l1 in
455 let l2 = NCicUtils.expand_local_context l2 in
456 let metasenv, subst, to_restrict, _ =
458 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
460 let metasenv, subst =
461 unify status (*test_eq_only*) true metasenv subst context
462 (NCicSubstitution.lift status s1 t1) (NCicSubstitution.lift status s2 t2)
465 metasenv, subst, to_restrict, i-1
466 with UnificationFailure _ | Uncertain _ ->
467 metasenv, subst, i::to_restrict, i-1)
468 l1 l2 (metasenv, subst, [], List.length l1)
470 if to_restrict <> [] then
471 let metasenv, subst, _, _ =
472 NCicMetaSubst.restrict status metasenv subst n1 to_restrict
477 | Invalid_argument _ -> assert false
478 | NCicMetaSubst.MetaSubstFailure msg ->
480 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
481 let term1 = NCicSubstitution.subst_meta status lc1 term in
482 let term2 = NCicSubstitution.subst_meta status lc2 term in
483 unify status test_eq_only metasenv subst context term1 term2 swap
484 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
486 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
487 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
490 (fun (metasenv, subst) t1 t2 ->
491 unify status (*test_eq_only*) true metasenv subst context t1
493 (metasenv,subst) l1 l2
494 with Invalid_argument _ ->
495 raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)))
497 | _, NCic.Meta (n, _) when is_locked n subst && not swap->
498 (let (metasenv, subst), i =
499 match NCicReduction.whd status ~subst context t1 with
500 | NCic.Appl (NCic.Meta (i,l) as meta :: args) ->
501 let metasenv, lambda_Mj =
502 lambda_intros status metasenv subst context (List.length args)
503 (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
505 unify status test_eq_only metasenv subst context
506 (C.Meta (i,l)) lambda_Mj false,
508 | NCic.Meta (i,_) -> (metasenv, subst), i
510 raise (UnificationFailure (lazy "Locked term vs non
511 flexible term; probably not saturated enough yet!"))
513 let t1 = NCicReduction.whd status ~subst context t1 in
515 match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
517 let metasenv, subst =
518 instantiate status test_eq_only metasenv subst context j lj t2 true
520 (* We need to remove the out_scope_tags to avoid propagation of
521 them that triggers again the ad-hoc case *)
523 List.map (fun (i,(tag,ctx,bo,ty)) ->
526 (function `InScope | `OutScope _ -> false | _ -> true) tag
532 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
533 let term = eta_reduce status subst term in
534 let subst = List.filter (fun (j,_) -> j <> i) subst in
535 metasenv, ((i, (name, ctx, term, ty)) :: subst)
536 with Not_found -> assert false))
537 | NCic.Meta (n, _), _ when is_locked n subst && swap ->
538 unify status test_eq_only metasenv subst context t2 t1 false
540 | t, C.Meta (n,lc) when List.mem_assoc n subst ->
541 let _,_,term,_ = NCicUtils.lookup_subst n subst in
542 let term = NCicSubstitution.subst_meta status lc term in
543 unify status test_eq_only metasenv subst context t term swap
544 | C.Meta (n,_), _ when List.mem_assoc n subst ->
545 unify status test_eq_only metasenv subst context t2 t1 (not swap)
547 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
548 let _,_,term,_ = NCicUtils.lookup_subst i subst in
549 let term = NCicSubstitution.subst_meta status l term in
550 unify status test_eq_only metasenv subst context t1
551 (mk_appl status ~upto:(List.length args) term args) swap
552 | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
553 unify status test_eq_only metasenv subst context t2 t1 (not swap)
555 | C.Meta (n,_), C.Meta (m,lc') when
556 let _,cc1,_ = NCicUtils.lookup_meta n metasenv in
557 let _,cc2,_ = NCicUtils.lookup_meta m metasenv in
558 (n < m && cc1 = cc2) ||
559 let len1 = List.length cc1 in
560 let len2 = List.length cc2 in
561 len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
562 instantiate status test_eq_only metasenv subst context m lc'
563 (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
564 | C.Meta (n,lc), C.Meta (m,lc') when
565 let _,_,tyn = NCicUtils.lookup_meta n metasenv in
566 let _,_,tym = NCicUtils.lookup_meta m metasenv in
567 let tyn = NCicSubstitution.subst_meta status lc tyn in
568 let tym = NCicSubstitution.subst_meta status lc tym in
570 NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
571 NCicEnvironment.universe_lt u1 u2
573 instantiate status test_eq_only metasenv subst context m lc'
574 (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
575 | C.Meta (n,lc), t ->
576 instantiate status test_eq_only metasenv subst context n lc
577 (NCicReduction.head_beta_reduce status ~subst t) swap
578 | t, C.Meta (n,lc) ->
579 instantiate status test_eq_only metasenv subst context n lc
580 (NCicReduction.head_beta_reduce status ~subst t) (not swap)
582 (* higher order unification case *)
583 | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
584 (* this easy_case handles "(? ?) =?= (f a)", same number of
585 * args, preferring the instantiation "f" over "\_.f a" for the
586 * metavariable in head position. Since the arguments of the meta
587 * are flexible, delift would ignore them generating a constant
588 * function even in the easy case above *)
591 | NCic.Appl (f :: f_args)
593 List.exists (NCicMetaSubst.is_flexible status context ~subst) args ->
594 let mlen = List.length args in
595 let flen = List.length f_args in
596 let min_len = min mlen flen in
597 let mhe,margs = HExtlib.split_nth (mlen - min_len) args in
598 let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in
600 Some (List.fold_left2
602 unify status test_eq_only m s context t1 t2 swap
604 ((NCicUntrusted.mk_appl meta mhe)::margs)
605 ((NCicUntrusted.mk_appl f fhe)::fargs))
606 with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
610 (match easy_case with
613 (* This case handles "(?_f ..ti..) =?= t2", abstracting every
614 * non flexible ti (delift skips local context items that are
615 * flexible) from t2 in two steps:
616 * 1) ?_f := \..xi.. .?
617 * 2) ?_f ..ti.. =?= t2 --unif_machines-->
618 ?_f[..ti..] =?= t2 --instantiate-->
619 delift [..ti..] t2 *)
620 let metasenv, lambda_Mj =
621 lambda_intros status metasenv subst context (List.length args)
622 (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
624 let metasenv, subst =
625 unify status test_eq_only metasenv subst context
626 (C.Meta (i,l)) lambda_Mj swap
628 let metasenv, subst =
629 unify status test_eq_only metasenv subst context t1 t2 swap
632 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
633 let term = eta_reduce status subst term in
634 let subst = List.filter (fun (j,_) -> j <> i) subst in
635 metasenv, ((i, (name, ctx, term, ty)) :: subst)
636 with Not_found -> assert false))
638 | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
639 unify status test_eq_only metasenv subst context t2 t1 (not swap)
641 (* processing this case here we avoid a useless small delta step *)
642 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
644 let relevance = NCicEnvironment.get_relevance status r1 in
645 let metasenv, subst, _ =
648 (fun (metasenv, subst, relevance) t1 t2 ->
650 match relevance with b::tl -> b,tl | _ -> true, [] in
651 let metasenv, subst =
652 try unify status test_eq_only metasenv subst context t1 t2
654 with UnificationFailure _ | Uncertain _ when not b ->
657 metasenv, subst, relevance)
658 (metasenv, subst, relevance) tl1 tl2
660 Invalid_argument _ ->
661 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
662 | KeepReducing _ | KeepReducingThis _ -> assert false
666 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
667 C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
668 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys status ref1 in
669 let _,_,ty,_ = List.nth itl tyno in
670 let rec remove_prods ~subst context ty =
671 let ty = NCicReduction.whd status ~subst context ty in
674 | C.Prod (name,so,ta) ->
675 remove_prods ~subst ((name,(C.Decl so))::context) ta
679 match remove_prods ~subst [] ty with
680 | C.Sort C.Prop -> true
683 (* if not (Ref.eq ref1 ref2) then
684 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
686 let metasenv, subst =
687 unify status test_eq_only metasenv subst context outtype1 outtype2 swap in
688 let metasenv, subst =
689 try unify status test_eq_only metasenv subst context term1 term2 swap
690 with UnificationFailure _ | Uncertain _ when is_prop ->
695 (fun (metasenv,subst) t1 t2 ->
696 unify status test_eq_only metasenv subst context t1 t2 swap)
697 (metasenv, subst) pl1 pl2
698 with Invalid_argument _ -> assert false)
699 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
700 | _ when norm1 && norm2 ->
701 if (could_reduce t1 || could_reduce t2) then
702 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
704 raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
705 | _ -> raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
706 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
708 let fo_unif test_eq_only metasenv subst (norm1,t1 as nt1) (norm2,t2 as nt2)=
709 try fo_unif test_eq_only metasenv subst nt1 nt2
711 UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
712 raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
714 let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
715 if NCicUntrusted.metas_of_term status subst context t1 = [] &&
716 NCicUntrusted.metas_of_term status subst context t2 = []
719 (*D*) inside 'H'; try let rc =
720 pp(lazy ("\nProblema:\n" ^
721 ppterm status ~metasenv ~subst ~context t1 ^ " =?= " ^
722 ppterm status ~metasenv ~subst ~context t2));
724 NCicUnifHint.look_for_hint status metasenv subst context t1 t2
726 let rec cand_iter = function
727 | [] -> None (* raise exc *)
728 | (metasenv,(c1,c2),premises)::tl ->
729 pp (lazy ("\nProvo il candidato:\n" ^
733 ppterm status ~metasenv ~subst ~context a ^ " =?= " ^
734 ppterm status ~metasenv ~subst ~context b) premises) ^
735 "\n-------------------------------------------\n"^
736 ppterm status ~metasenv ~subst ~context c1 ^ " = " ^
737 ppterm status ~metasenv ~subst ~context c2));
739 (*D*) inside 'K'; try let rc =
741 fo_unif test_eq_only metasenv subst mt1 (false,c1) in
743 fo_unif test_eq_only metasenv subst (false,c2) mt2 in
746 (fun (metasenv, subst) (x,y) ->
747 unify status test_eq_only metasenv subst context x y false)
748 (metasenv, subst) (List.rev premises)
750 pp(lazy("FUNZIONA!"));
751 Some (metasenv, subst)
752 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
754 KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
755 | KeepReducingThis _ -> assert false
758 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
761 let put_in_whd m1 m2 =
762 NCicReduction.reduce_machine status ~delta:max_int ~subst context m1,
763 NCicReduction.reduce_machine status ~delta:max_int ~subst context m2
765 let fo_unif_w_hints test_eq_only metasenv subst (_,t1 as m1) (_,t2 as m2) =
766 try fo_unif test_eq_only metasenv subst m1 m2
768 | UnificationFailure _ as exn -> raise exn
769 | KeepReducing _ | Uncertain _ as exn ->
770 let (t1,norm1 as tm1),(t2,norm2 as tm2) =
771 put_in_whd (0,[],t1,[]) (0,[],t2,[])
774 try_hints metasenv subst
775 (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
780 | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2))
781 | Uncertain _ as exn -> raise exn
784 let fo_unif_heads_and_cont_or_unwind_and_hints
785 test_eq_only metasenv subst m1 m2 cont hm1 hm2
787 let ms, continuation =
788 (* calling the continuation inside the outermost try is an option
789 and makes unification stronger, but looks not frequent to me
790 that heads unify but not the arguments and that an hints can fix
792 try fo_unif test_eq_only metasenv subst m1 m2, cont
794 | UnificationFailure _
795 | KeepReducing _ | Uncertain _ as exn ->
796 let (t1,norm1),(t2,norm2) = hm1, hm2 in
798 try_hints metasenv subst
799 (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
801 | Some x -> x, fun x -> x
804 | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
805 | UnificationFailure _ | Uncertain _ as exn -> raise exn
810 let height_of = function
811 | NCic.Const (Ref.Ref (_,Ref.Def h))
812 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
813 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
814 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
817 let small_delta_step ~subst
818 ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
820 assert (not (norm1 && norm2));
822 x1,NCicReduction.reduce_machine status ~delta:0 ~subst context m2
824 NCicReduction.reduce_machine status ~delta:0 ~subst context m1,x2
826 let h1 = height_of t1 in
827 let h2 = height_of t2 in
828 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
829 NCicReduction.reduce_machine status ~delta ~subst context m1,
830 NCicReduction.reduce_machine status ~delta ~subst context m2
832 let rec unif_machines metasenv subst =
834 | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
835 (*D*) inside 'M'; try let rc =
837 ppterm status ~metasenv ~subst ~context
838 (NCicReduction.unwind status (k1,e1,t1,s1)) ^
840 ppterm status ~metasenv ~subst ~context
841 (NCicReduction.unwind status (k2,e2,t2,s2))));
842 pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
845 | C.Const r -> NCicEnvironment.get_relevance status r
847 let unif_from_stack (metasenv, subst) (t1, t2, b) =
849 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
850 let t2 = NCicReduction.from_stack ~delta:max_int t2 in
851 unif_machines metasenv subst (put_in_whd t1 t2)
852 with UnificationFailure _ | Uncertain _ when not b ->
855 let rec check_stack l1 l2 r todo =
857 | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
858 | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
860 NCicReduction.unwind status (k1,e1,t1,List.rev l1),
861 NCicReduction.unwind status (k2,e2,t2,List.rev l2),
864 let check_stack l1 l2 r =
866 | NCic.Meta _, _ | _, NCic.Meta _ ->
867 (NCicReduction.unwind status (k1,e1,t1,s1)),
868 (NCicReduction.unwind status (k2,e2,t2,s2)),[]
869 | _ -> check_stack l1 l2 r []
872 check_stack (List.rev s1) (List.rev s2) (List.rev relevance) in
874 fo_unif_heads_and_cont_or_unwind_and_hints
875 test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
876 (fun ms -> List.fold_left unif_from_stack ms todo)
879 | KeepReducing _ -> assert false
880 | KeepReducingThis _ ->
881 assert (not (norm1 && norm2));
882 unif_machines metasenv subst (small_delta_step ~subst m1 m2)
883 | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
884 -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
885 | UnificationFailure msg
886 when could_reduce (NCicReduction.unwind status (fst m1))
887 || could_reduce (NCicReduction.unwind status (fst m2))
888 -> raise (Uncertain msg)
889 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
891 try fo_unif_w_hints test_eq_only metasenv subst (false,t1) (false,t2)
893 | KeepReducingThis (msg,tm1,tm2) ->
895 unif_machines metasenv subst (tm1,tm2)
897 | UnificationFailure _ -> raise (UnificationFailure msg)
898 | Uncertain _ -> raise (Uncertain msg)
899 | KeepReducing _ -> assert false)
900 | KeepReducing _ -> assert false
902 (*D*) in outside None; rc with KeepReducing _ -> assert false | exn -> outside (Some exn); raise exn
904 and delift_type_wrt_terms status metasenv subst context t args =
905 let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
906 let (metasenv, subst), t =
908 NCicMetaSubst.delift status
909 ~unify:(fun m s c t1 t2 ->
912 try Some (unify status false m s c t1 t2 false)
913 with UnificationFailure _ | Uncertain _ -> None
916 metasenv subst context (-1) (0,NCic.Ctx lc) t
918 NCicMetaSubst.MetaSubstFailure _
919 | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t
925 let unify status ?(test_eq_only=false) ?(swap=false) metasenv subst context t1 t2=
927 unify status test_eq_only metasenv subst context t1 t2 swap;;
929 let fix_sorts status m s =
930 fix status m s true false (UnificationFailure (lazy "no sup"))