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 status ~subst context =
140 | C.Appl (C.Const (Ref.Ref (_,Ref.Fix (_,recno,_)))::args)
141 when List.length args > recno ->
142 let t = NCicReduction.whd status ~subst context (List.nth args recno) in
143 could_reduce status ~subst context t
144 | C.Match (_,_,he,_) ->
145 let he = NCicReduction.whd status ~subst context he in
146 could_reduce status ~subst context he
147 | C.Appl (he::_) -> could_reduce status ~subst context he
148 | C.Sort _ | C.Rel _ | C.Prod _ | C.Lambda _ | C.Const _ -> false
149 | C.Appl [] | C.LetIn _ | C.Implicit _ -> assert false
152 let rec lambda_intros status metasenv subst context argsno ty =
153 pp (lazy ("LAMBDA INTROS: " ^ ppterm status ~metasenv ~subst ~context ty));
156 let metasenv, _, bo, _ =
157 NCicMetaSubst.mk_meta metasenv context ~with_type:ty `IsTerm
161 (match NCicReduction.whd status ~subst context ty with
164 lambda_intros status metasenv subst
165 ((n,C.Decl so)::context) (argsno - 1) ta
167 metasenv,C.Lambda (n,so,bo)
171 let unopt exc = function None -> raise exc | Some x -> x ;;
173 let fix (status:#NCic.status) metasenv subst is_sup test_eq_only exc t =
174 (*D*) inside 'f'; try let rc =
175 pp (lazy (status#ppterm ~metasenv ~subst ~context:[] t));
176 let rec aux test_eq_only metasenv = function
177 | NCic.Prod (n,so,ta) ->
178 let metasenv,so = aux true metasenv so in
179 let metasenv,ta = aux test_eq_only metasenv ta in
180 metasenv,NCic.Prod (n,so,ta)
181 | NCic.Sort (NCic.Type [(`CProp|`Type),_]) as orig when test_eq_only ->
183 | NCic.Sort (NCic.Type _) when test_eq_only -> raise exc
184 | NCic.Sort (NCic.Type u) when is_sup ->
185 metasenv, NCic.Sort (NCic.Type (unopt exc (NCicEnvironment.sup u)))
186 | NCic.Sort (NCic.Type u) ->
187 metasenv, NCic.Sort (NCic.Type
188 (unopt exc (NCicEnvironment.inf ~strict:false u)))
189 | NCic.Meta (n,_) as orig ->
191 let _,_,_,_ = NCicUtils.lookup_subst n subst in metasenv,orig
192 with NCicUtils.Subst_not_found _ ->
193 let metasenv, _ = NCicMetaSubst.extend_meta metasenv n in
196 NCicUntrusted.map_term_fold_a status (fun _ x -> x) test_eq_only aux metasenv t
198 aux test_eq_only metasenv t
199 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
202 let metasenv_to_subst n (kind,context,ty) metasenv subst =
203 let infos,metasenv = List.partition (fun (n',_) -> n = n') metasenv in
204 let attrs,octx,oty = match infos with [_,infos] -> infos | _ -> assert false in
205 if octx=context && oty=ty then
206 (n,(NCicUntrusted.set_kind kind attrs, octx, oty))::metasenv,subst
208 let metasenv, _, bo, _ =
209 NCicMetaSubst.mk_meta metasenv context ~attrs ~with_type:ty kind in
210 let subst = (n,(NCicUntrusted.set_kind kind attrs,octx,bo,oty))::subst in
214 let rec sortfy status exc metasenv subst context t =
215 let t = NCicReduction.whd status ~subst context t in
218 | NCic.Sort _ -> metasenv, subst
220 let attrs, context, ty = NCicUtils.lookup_meta n metasenv in
221 let kind = NCicUntrusted.kind_of_meta attrs in
222 if kind = `IsSort then
226 | NCic.Implicit (`Typeof _) ->
227 metasenv_to_subst n (`IsSort,[],ty) metasenv subst
229 let metasenv,subst,ty = sortfy status exc metasenv subst context ty in
230 metasenv_to_subst n (`IsSort,[],ty) metasenv subst)
231 | NCic.Implicit _ -> assert false
236 let indfy status exc metasenv subst context t =
237 let t = NCicReduction.whd status ~subst context t in
240 | NCic.Const (Ref.Ref (_, Ref.Ind _))
241 | NCic.Appl (NCic.Const (Ref.Ref (_, Ref.Ind _))::_) -> metasenv, subst
244 let attrs, context, ty = NCicUtils.lookup_meta n metasenv in
245 let kind = NCicUntrusted.kind_of_meta attrs in
246 if kind = `IsSort then
250 | NCic.Implicit (`Typeof _) ->
251 metasenv_to_subst n (`IsSort,[],ty) metasenv subst
253 let metasenv,subst,ty = sortfy status exc metasenv subst context ty in
254 metasenv_to_subst n (`IsSort,[],ty) metasenv subst)
256 | NCic.Implicit _ -> assert false
261 let tipify status exc metasenv subst context t ty =
263 match NCicUntrusted.kind_of_meta attrs with
264 `IsType | `IsSort -> true
267 let rec optimize_meta metasenv subst =
271 let attrs,_,_ = NCicUtils.lookup_meta n metasenv in
272 if is_type attrs then
275 let _,cc,ty = NCicUtils.lookup_meta n metasenv in
276 let metasenv,subst,ty = sortfy status exc metasenv subst cc ty in
278 NCicUntrusted.replace_in_metasenv n
279 (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
284 NCicUtils.Meta_not_found _ ->
285 let attrs, _,bo,_ = NCicUtils.lookup_subst n subst in
286 if is_type attrs then
289 let _,cc,_,ty = NCicUtils.lookup_subst n subst in
290 let metasenv,subst,ty = sortfy status exc metasenv subst cc ty in
292 NCicUntrusted.replace_in_subst n
293 (fun attrs,cc,bo,_->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
296 optimize_meta metasenv subst (NCicSubstitution.subst_meta status lc bo))
297 | _ -> metasenv,subst,false
299 let metasenv,subst,b = optimize_meta metasenv subst t in
303 let metasenv,subst,_ = sortfy status exc metasenv subst context ty in
307 let put_in_whd status subst context m1 m2 =
308 NCicReduction.reduce_machine status ~delta:max_int ~subst context m1,
309 NCicReduction.reduce_machine status ~delta:max_int ~subst context m2
312 let rec instantiate status test_eq_only metasenv subst context n lc t swap =
313 (*D*) inside 'I'; try let rc =
314 pp (lazy(string_of_int n^" :=?= "^ppterm status ~metasenv ~subst ~context t));
316 UnificationFailure (mk_msg status metasenv subst context (NCic.Meta (n,lc)) t) in
317 let move_to_subst i ((_,cc,t,_) as infos) metasenv subst =
318 let metasenv = List.remove_assoc i metasenv in
319 pp(lazy(string_of_int n ^ " :==> "^ ppterm status ~metasenv ~subst ~context:cc t));
320 metasenv, (i,infos) :: subst
322 let delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv subst =
323 pp (lazy(string_of_int n ^ " := 111 = "^
324 ppterm status ~metasenv ~subst ~context t));
325 let (metasenv, subst), t =
327 NCicMetaSubst.delift status ~unify:(unify_for_delift status)
328 metasenv subst context n lc t
329 with NCicMetaSubst.Uncertain msg ->
330 pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
331 raise (Uncertain msg)
332 | NCicMetaSubst.MetaSubstFailure msg ->
333 pp (lazy ("delift fails: " ^ Lazy.force msg));
334 raise (UnificationFailure msg)
336 pp (lazy(string_of_int n ^ " := 222 = "^
337 ppterm status ~metasenv ~subst ~context:cc t^ppmetasenv status ~subst metasenv));
338 (* Unifying the types may have already instantiated n. *)
340 let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
341 let oldt = NCicSubstitution.subst_meta status lc oldt in
342 let t = NCicSubstitution.subst_meta status lc t in
343 (* conjecture: always fail --> occur check *)
344 unify status test_eq_only metasenv subst context t oldt false
345 with NCicUtils.Subst_not_found _ ->
346 move_to_subst n (attrs,cc,t,ty) metasenv subst
348 let attrs,cc,ty = NCicUtils.lookup_meta n metasenv in
349 let kind = NCicUntrusted.kind_of_meta attrs in
350 let metasenv,t = fix status metasenv subst swap test_eq_only exc t in
351 let ty_t = NCicTypeChecker.typeof status ~metasenv ~subst context t in
352 let metasenv,subst,t =
354 `IsSort -> sortfy status exc metasenv subst context t
355 | `IsType -> tipify status exc metasenv subst context t ty_t
356 | `IsTerm -> metasenv,subst,t in
360 NCic.Implicit (`Typeof _), NCic.Sort _ ->
361 move_to_subst n (attrs,cc,t,ty_t) metasenv subst
362 | NCic.Sort (NCic.Type u1), NCic.Sort s ->
365 NCic.Type u2, false ->
367 (unopt exc (NCicEnvironment.inf ~strict:false
368 (unopt exc (NCicEnvironment.inf ~strict:true u1) @ u2))))
369 | NCic.Type u2, true ->
370 if NCicEnvironment.universe_lt u2 u1 then
371 NCic.Sort (NCic.Type u2)
373 | NCic.Prop,_ -> NCic.Sort NCic.Prop
375 move_to_subst n (attrs,cc,s,ty) metasenv subst
376 | NCic.Implicit (`Typeof _), NCic.Meta _ ->
377 move_to_subst n (attrs,cc,t,ty_t) metasenv subst
379 | NCic.Meta _, NCic.Sort _ ->
380 pp (lazy ("On the types: " ^
381 ppterm status ~metasenv ~subst ~context ty ^ "=<=" ^
382 ppterm status ~metasenv ~subst ~context ty_t));
383 let metasenv, subst =
384 unify status false metasenv subst context ty_t ty false in
385 delift_to_subst test_eq_only n lc (attrs,cc,ty) t
386 context metasenv subst
391 NCic.Implicit (`Typeof _) ->
392 let (metasenv, subst), ty_t =
394 NCicMetaSubst.delift status ~unify:(unify_for_delift status)
395 metasenv subst context n lc ty_t
396 with NCicMetaSubst.Uncertain msg ->
397 pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
398 raise (Uncertain msg)
399 | NCicMetaSubst.MetaSubstFailure msg ->
400 pp (lazy ("delift fails: " ^ Lazy.force msg));
401 raise (UnificationFailure msg)
403 delift_to_subst test_eq_only n lc (attrs,cc,ty_t) t context metasenv
406 let lty = NCicSubstitution.subst_meta status lc ty in
407 pp (lazy ("On the types: " ^
408 ppterm status ~metasenv ~subst ~context ty_t ^ "=<=" ^
409 ppterm status ~metasenv ~subst ~context lty));
410 let metasenv, subst =
411 unify status false metasenv subst context ty_t lty false
413 delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv
415 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
417 and fo_unif_w_hints during_delift status swap test_eq_only metasenv subst context (_,t1 as m1) (_,t2 as m2) =
418 try fo_unif during_delift status swap test_eq_only metasenv subst context m1 m2
420 | UnificationFailure _ as exn -> raise exn
421 | KeepReducing _ | Uncertain _ as exn ->
422 let (t1,norm1 as tm1),(t2,norm2 as tm2) =
423 put_in_whd status subst context (0,[],t1,[]) (0,[],t2,[])
426 try_hints status swap test_eq_only metasenv subst context
427 (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
432 | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2))
433 | Uncertain _ as exn -> raise exn
436 and unify_for_delift status metasenv subst context t1 t2 =
440 (fo_unif_w_hints true status false true(*test_eq_only*) metasenv subst
441 context (false,t1) (false,t2))
442 (*(unify status true(*test_eq_only*) metasenv subst
443 context t1 t2 false)*)
444 with UnificationFailure _ | Uncertain _ | KeepReducingThis _ -> None
448 and fo_unif0 during_delift status swap test_eq_only metasenv subst context (norm1,t1 as m1) (norm2,t2 as m2) =
449 (*D*) inside 'F'; try let rc =
450 pp (lazy(" " ^ ppterm status ~metasenv ~subst ~context t1 ^
451 (if swap then " ==>?== "
453 ppterm status ~metasenv ~subst ~context t2 ^ ppmetasenv status
455 pp (lazy(" " ^ ppterm status ~metasenv ~subst:[] ~context t1 ^
456 (if swap then " ==>??== "
458 ppterm status ~metasenv ~subst:[] ~context t2 ^ ppmetasenv status
462 (* CSC: To speed up Oliboni's stuff. Why is it necessary, anyway?
464 NCicUntrusted.metas_of_term subst context t1 = [] &&
465 NCicUntrusted.metas_of_term subst context t2 = []
467 if NCicReduction.are_convertible ~metasenv ~subst context t1 t2 then
470 raise (UnificationFailure (lazy "Closed terms not convertible"))
474 | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl []
475 | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) ->
476 prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
478 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
479 let a, b = if swap then b,a else a,b in
480 if NCicEnvironment.universe_leq a b then metasenv, subst
481 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
482 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
483 if NCicEnvironment.universe_eq a b then metasenv, subst
484 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
485 | (C.Sort C.Prop,C.Sort (C.Type _)) when not swap ->
486 if (not test_eq_only) then metasenv, subst
487 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
488 | (C.Sort (C.Type _), C.Sort C.Prop) when swap ->
489 if (not test_eq_only) then metasenv, subst
490 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
492 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
493 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
494 let metasenv, subst = unify status true metasenv subst context s1 s2 swap in
495 unify status test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 swap
496 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
497 let metasenv,subst=unify status test_eq_only metasenv subst context ty1 ty2 swap in
498 let metasenv,subst=unify status test_eq_only metasenv subst context s1 s2 swap in
499 let context = (name1, C.Def (s1,ty1))::context in
500 unify status test_eq_only metasenv subst context t1 t2 swap
502 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
504 let l1 = NCicUtils.expand_local_context l1 in
505 let l2 = NCicUtils.expand_local_context l2 in
506 let metasenv, subst, to_restrict, _ =
508 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
510 let metasenv, subst =
511 unify status (*test_eq_only*) true metasenv subst context
512 (NCicSubstitution.lift status s1 t1) (NCicSubstitution.lift status s2 t2)
515 metasenv, subst, to_restrict, i-1
516 with UnificationFailure _ | Uncertain _ ->
517 metasenv, subst, i::to_restrict, i-1)
518 l1 l2 (metasenv, subst, [], List.length l1)
520 if to_restrict <> [] then
521 let metasenv, subst, _, _ =
522 NCicMetaSubst.restrict status metasenv subst n1 to_restrict
527 | Invalid_argument _ -> assert false
528 | NCicMetaSubst.MetaSubstFailure msg ->
530 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
531 let term1 = NCicSubstitution.subst_meta status lc1 term in
532 let term2 = NCicSubstitution.subst_meta status lc2 term in
533 unify status test_eq_only metasenv subst context term1 term2 swap
534 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
536 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
537 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
540 (fun (metasenv, subst) t1 t2 ->
541 unify status (*test_eq_only*) true metasenv subst context t1
543 (metasenv,subst) l1 l2
544 with Invalid_argument _ ->
545 raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)))
547 | _, NCic.Meta (n, _) when is_locked n subst && not swap && not during_delift ->
548 (let (metasenv, subst), i =
549 match NCicReduction.whd status ~subst context t1 with
550 | NCic.Appl (NCic.Meta (i,l) as meta :: args) ->
551 let metasenv, lambda_Mj =
552 lambda_intros status metasenv subst context (List.length args)
553 (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
555 unify status test_eq_only metasenv subst context
556 (C.Meta (i,l)) lambda_Mj false,
558 | NCic.Meta (i,_) -> (metasenv, subst), i
560 raise (UnificationFailure (lazy "Locked term vs non
561 flexible term; probably not saturated enough yet!"))
563 let t1 = NCicReduction.whd status ~subst context t1 in
565 match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
567 let metasenv, subst =
568 instantiate status test_eq_only metasenv subst context j lj t2 true
570 (* We need to remove the out_scope_tags to avoid propagation of
571 them that triggers again the ad-hoc case *)
573 List.map (fun (i,(tag,ctx,bo,ty)) ->
576 (function `InScope | `OutScope _ -> false | _ -> true) tag
582 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
583 let term = eta_reduce status 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.Meta (n, _), _ when is_locked n subst && swap ->
588 fo_unif0 during_delift status false test_eq_only metasenv subst context m2 m1
590 | _, C.Meta (n,lc) when List.mem_assoc n subst ->
591 let _,_,term,_ = NCicUtils.lookup_subst n subst in
592 let term = NCicSubstitution.subst_meta status lc term in
593 fo_unif0 during_delift status swap test_eq_only metasenv subst context
595 | C.Meta (n,_), _ when List.mem_assoc n subst ->
596 fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
598 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
599 let _,_,term,_ = NCicUtils.lookup_subst i subst in
600 let term = NCicSubstitution.subst_meta status l term in
601 fo_unif0 during_delift status swap test_eq_only metasenv subst context
602 m1 (false,mk_appl status ~upto:(List.length args) term args)
603 | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
604 fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
606 | C.Meta (n,_), C.Meta (m,lc') when
607 let _,cc1,_ = NCicUtils.lookup_meta n metasenv in
608 let _,cc2,_ = NCicUtils.lookup_meta m metasenv in
609 (n < m && cc1 = cc2) ||
610 let len1 = List.length cc1 in
611 let len2 = List.length cc2 in
612 len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
613 instantiate status test_eq_only metasenv subst context m lc'
614 (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
615 | C.Meta (n,lc), C.Meta (m,lc') when
616 let _,_,tyn = NCicUtils.lookup_meta n metasenv in
617 let _,_,tym = NCicUtils.lookup_meta m metasenv in
618 let tyn = NCicSubstitution.subst_meta status lc tyn in
619 let tym = NCicSubstitution.subst_meta status lc tym in
621 NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
622 NCicEnvironment.universe_lt u1 u2
624 instantiate status test_eq_only metasenv subst context m lc'
625 (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
626 | C.Meta (n,lc), t ->
627 instantiate status test_eq_only metasenv subst context n lc
628 (NCicReduction.head_beta_reduce status ~subst t) swap
629 | t, C.Meta (n,lc) ->
630 instantiate status test_eq_only metasenv subst context n lc
631 (NCicReduction.head_beta_reduce status ~subst t) (not swap)
633 (* higher order unification case *)
634 | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
635 (* this easy_case handles "(? ?) =?= (f a)", same number of
636 * args, preferring the instantiation "f" over "\_.f a" for the
637 * metavariable in head position. Since the arguments of the meta
638 * are flexible, delift would ignore them generating a constant
639 * function even in the easy case above *)
642 | NCic.Appl (f :: f_args)
644 List.exists (NCicMetaSubst.is_flexible status context ~subst) args ->
645 let mlen = List.length args in
646 let flen = List.length f_args in
647 let min_len = min mlen flen in
648 let mhe,margs = HExtlib.split_nth (mlen - min_len) args in
649 let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in
651 Some (List.fold_left2
653 unify status test_eq_only m s context t1 t2 swap
655 ((NCicUntrusted.mk_appl meta mhe)::margs)
656 ((NCicUntrusted.mk_appl f fhe)::fargs))
657 with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
661 (match easy_case with
664 (* This case handles "(?_f ..ti..) =?= t2", abstracting every
665 * non flexible ti (delift skips local context items that are
666 * flexible) from t2 in two steps:
667 * 1) ?_f := \..xi.. .?
668 * 2) ?_f ..ti.. =?= t2 --unif_machines-->
669 ?_f[..ti..] =?= t2 --instantiate-->
670 delift [..ti..] t2 *)
671 let metasenv, lambda_Mj =
672 lambda_intros status metasenv subst context (List.length args)
673 (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
675 let metasenv, subst =
676 unify status test_eq_only metasenv subst context
677 (C.Meta (i,l)) lambda_Mj swap
679 let metasenv, subst =
680 unify status test_eq_only metasenv subst context t1 t2 swap
683 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
684 let term = eta_reduce status subst term in
685 let subst = List.filter (fun (j,_) -> j <> i) subst in
686 metasenv, ((i, (name, ctx, term, ty)) :: subst)
687 with Not_found -> assert false))
689 | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
690 fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
692 | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
694 fo_unif0 during_delift status swap test_eq_only metasenv subst context
695 (false,hd1) (false,hd2) in
698 | C.Const r -> NCicEnvironment.get_relevance status r
700 let metasenv, subst, _ =
703 (fun (metasenv, subst, relevance) t1 t2 ->
705 match relevance with b::tl -> b,tl | _ -> true, [] in
706 let metasenv, subst =
707 try unify status test_eq_only metasenv subst context t1 t2
709 with UnificationFailure _ | Uncertain _ when not b ->
712 metasenv, subst, relevance)
713 (metasenv, subst, relevance) tl1 tl2
715 Invalid_argument _ ->
716 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
717 | KeepReducing _ | KeepReducingThis _ -> assert false
721 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
722 C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
723 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys status ref1 in
724 let _,_,ty,_ = List.nth itl tyno in
725 let rec remove_prods ~subst context ty =
726 let ty = NCicReduction.whd status ~subst context ty in
729 | C.Prod (name,so,ta) ->
730 remove_prods ~subst ((name,(C.Decl so))::context) ta
734 match remove_prods ~subst [] ty with
735 | C.Sort C.Prop -> true
738 (* if not (Ref.eq ref1 ref2) then
739 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
741 let metasenv, subst =
742 unify status test_eq_only metasenv subst context outtype1 outtype2 swap in
743 let metasenv, subst =
744 try unify status test_eq_only metasenv subst context term1 term2 swap
745 with UnificationFailure _ | Uncertain _ when is_prop ->
750 (fun (metasenv,subst) t1 t2 ->
751 unify status test_eq_only metasenv subst context t1 t2 swap)
752 (metasenv, subst) pl1 pl2
753 with Invalid_argument _ -> assert false)
754 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
755 | _ when norm1 && norm2 ->
756 if (could_reduce status ~subst context t1 || could_reduce status ~subst context t2) then
757 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
759 raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
760 | _ -> raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
761 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
763 and try_hints status swap test_eq_only metasenv subst context (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
764 if NCicUntrusted.metas_of_term status subst context t1 = [] &&
765 NCicUntrusted.metas_of_term status subst context t2 = []
768 (*D*) inside 'H'; try let rc =
769 pp(lazy ("\nProblema:\n" ^
770 ppterm status ~metasenv ~subst ~context t1 ^ " =?= " ^
771 ppterm status ~metasenv ~subst ~context t2));
773 NCicUnifHint.look_for_hint status metasenv subst context t1 t2
775 let rec cand_iter = function
776 | [] -> None (* raise exc *)
777 | (metasenv,(c1,c2),premises)::tl ->
778 pp (lazy ("\nProvo il candidato:\n" ^
782 ppterm status ~metasenv ~subst ~context a ^ " =?= " ^
783 ppterm status ~metasenv ~subst ~context b) premises) ^
784 "\n-------------------------------------------\n"^
785 ppterm status ~metasenv ~subst ~context c1 ^ " = " ^
786 ppterm status ~metasenv ~subst ~context c2));
788 (*D*) inside 'K'; try let rc =
790 fo_unif false status swap test_eq_only metasenv subst context mt1 (false,c1) in
792 fo_unif false status swap test_eq_only metasenv subst context (false,c2) mt2 in
795 (fun (metasenv, subst) (x,y) ->
796 unify status test_eq_only metasenv subst context x y false)
797 (metasenv, subst) (List.rev premises)
799 pp(lazy("FUNZIONA!"));
800 Some (metasenv, subst)
801 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
803 KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
804 | KeepReducingThis _ -> assert false
807 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
810 and fo_unif during_delift status swap test_eq_only metasenv subst context (norm1,t1 as nt1) (norm2,t2 as nt2)=
811 try fo_unif0 during_delift status swap test_eq_only metasenv subst context nt1 nt2
813 UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
814 raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
816 and unify status test_eq_only metasenv subst context t1 t2 swap =
817 (*D*) inside 'U'; try let rc =
818 let fo_unif_heads_and_cont_or_unwind_and_hints
819 test_eq_only metasenv subst m1 m2 cont hm1 hm2
821 let ms, continuation =
822 (* calling the continuation inside the outermost try is an option
823 and makes unification stronger, but looks not frequent to me
824 that heads unify but not the arguments and that an hints can fix
826 try fo_unif false status swap test_eq_only metasenv subst context m1 m2, cont
828 | UnificationFailure _
829 | KeepReducing _ | Uncertain _ as exn ->
830 let (t1,norm1),(t2,norm2) = hm1, hm2 in
832 try_hints status swap test_eq_only metasenv subst context
833 (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
835 | Some x -> x, fun x -> x
838 | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
839 | UnificationFailure _ | Uncertain _ as exn -> raise exn
844 let height_of = function
845 | NCic.Const (Ref.Ref (_,Ref.Def h))
846 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
847 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
848 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
851 let small_delta_step ~subst
852 ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
854 assert (not (norm1 && norm2));
856 x1,NCicReduction.reduce_machine status ~delta:0 ~subst context m2
858 NCicReduction.reduce_machine status ~delta:0 ~subst context m1,x2
860 let h1 = height_of t1 in
861 let h2 = height_of t2 in
862 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
863 NCicReduction.reduce_machine status ~delta ~subst context m1,
864 NCicReduction.reduce_machine status ~delta ~subst context m2
866 let rec unif_machines metasenv subst =
868 | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
869 (*D*) inside 'M'; try let rc =
871 ppterm status ~metasenv ~subst ~context
872 (NCicReduction.unwind status (k1,e1,t1,s1)) ^
874 ppterm status ~metasenv ~subst ~context
875 (NCicReduction.unwind status (k2,e2,t2,s2))));
876 pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
879 | C.Const r -> NCicEnvironment.get_relevance status r
881 let unif_from_stack (metasenv, subst) (t1, t2, b) =
883 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
884 let t2 = NCicReduction.from_stack ~delta:max_int t2 in
885 unif_machines metasenv subst (put_in_whd status subst context t1 t2)
886 with UnificationFailure _ | Uncertain _ when not b ->
889 let rec check_stack l1 l2 r todo =
891 | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
892 | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
894 NCicReduction.unwind status (k1,e1,t1,List.rev l1),
895 NCicReduction.unwind status (k2,e2,t2,List.rev l2),
898 let check_stack l1 l2 r =
900 | NCic.Meta _, _ | _, NCic.Meta _ ->
901 (NCicReduction.unwind status (k1,e1,t1,s1)),
902 (NCicReduction.unwind status (k2,e2,t2,s2)),[]
903 | _ -> check_stack l1 l2 r []
906 check_stack (List.rev s1) (List.rev s2) (List.rev relevance) in
908 fo_unif_heads_and_cont_or_unwind_and_hints
909 test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
910 (fun ms -> List.fold_left unif_from_stack ms todo)
913 | KeepReducing _ -> assert false
914 | KeepReducingThis _ ->
915 assert (not (norm1 && norm2));
916 unif_machines metasenv subst (small_delta_step ~subst m1 m2)
917 | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
918 -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
919 | UnificationFailure msg
920 when could_reduce status ~subst context (NCicReduction.unwind status (fst m1))
921 || could_reduce status ~subst context (NCicReduction.unwind status (fst m2))
922 -> raise (Uncertain msg)
923 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
925 try fo_unif_w_hints false status swap test_eq_only metasenv subst context (false,t1) (false,t2)
927 | KeepReducingThis (msg,tm1,tm2) ->
929 unif_machines metasenv subst (tm1,tm2)
931 | UnificationFailure _ -> raise (UnificationFailure msg)
932 | Uncertain _ -> raise (Uncertain msg)
933 | KeepReducing _ -> assert false)
934 | KeepReducing _ -> assert false
936 (*D*) in outside None; rc with KeepReducing _ -> assert false | exn -> outside (Some exn); raise exn
938 and delift_type_wrt_terms status metasenv subst context t args =
939 let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
940 let (metasenv, subst), t =
942 NCicMetaSubst.delift status ~unify:(unify_for_delift status)
943 metasenv subst context (-1) (0,NCic.Ctx lc) t
945 NCicMetaSubst.MetaSubstFailure _
946 | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t
952 let unify status ?(test_eq_only=false) ?(swap=false) metasenv subst context t1 t2=
954 unify status test_eq_only metasenv subst context t1 t2 swap;;
956 let fix_sorts status m s =
957 fix status m s true false (UnificationFailure (lazy "no sup"))