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 = Stdlib.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 flexible term; probably not saturated enough yet!"))
562 let t1 = NCicReduction.whd status ~subst context t1 in
564 match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
566 let metasenv, subst =
567 instantiate status test_eq_only metasenv subst context j lj t2 true
569 (* We need to remove the out_scope_tags to avoid propagation of
570 them that triggers again the ad-hoc case *)
572 List.map (fun (i,(tag,ctx,bo,ty)) ->
575 (function `InScope | `OutScope _ -> false | _ -> true) tag
581 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
582 let term = eta_reduce status subst term in
583 let subst = List.filter (fun (j,_) -> j <> i) subst in
584 metasenv, ((i, (name, ctx, term, ty)) :: subst)
585 with Not_found -> assert false))
586 | NCic.Meta (n, _), _ when is_locked n subst && swap ->
587 fo_unif0 during_delift status false test_eq_only metasenv subst context m2 m1
589 | _, C.Meta (n,lc) when List.mem_assoc n subst ->
590 let _,_,term,_ = NCicUtils.lookup_subst n subst in
591 let term = NCicSubstitution.subst_meta status lc term in
592 fo_unif0 during_delift status swap test_eq_only metasenv subst context
594 | C.Meta (n,_), _ when List.mem_assoc n subst ->
595 fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
597 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
598 let _,_,term,_ = NCicUtils.lookup_subst i subst in
599 let term = NCicSubstitution.subst_meta status l term in
600 fo_unif0 during_delift status swap test_eq_only metasenv subst context
601 m1 (false,mk_appl status ~upto:(List.length args) term args)
602 | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
603 fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
605 | C.Meta (n,_), C.Meta (m,lc') when
606 let _,cc1,_ = NCicUtils.lookup_meta n metasenv in
607 let _,cc2,_ = NCicUtils.lookup_meta m metasenv in
608 (n < m && cc1 = cc2) ||
609 let len1 = List.length cc1 in
610 let len2 = List.length cc2 in
611 len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
612 instantiate status test_eq_only metasenv subst context m lc'
613 (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
614 | C.Meta (n,lc), C.Meta (m,lc') when
615 let _,_,tyn = NCicUtils.lookup_meta n metasenv in
616 let _,_,tym = NCicUtils.lookup_meta m metasenv in
617 let tyn = NCicSubstitution.subst_meta status lc tyn in
618 let tym = NCicSubstitution.subst_meta status lc tym in
620 NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
621 NCicEnvironment.universe_lt u1 u2
623 instantiate status test_eq_only metasenv subst context m lc'
624 (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
625 | C.Meta (n,lc), t ->
626 instantiate status test_eq_only metasenv subst context n lc
627 (NCicReduction.head_beta_reduce status ~subst t) swap
628 | t, C.Meta (n,lc) ->
629 instantiate status test_eq_only metasenv subst context n lc
630 (NCicReduction.head_beta_reduce status ~subst t) (not swap)
632 (* higher order unification case *)
633 | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
634 (* this easy_case handles "(? ?) =?= (f a)", same number of
635 * args, preferring the instantiation "f" over "\_.f a" for the
636 * metavariable in head position. Since the arguments of the meta
637 * are flexible, delift would ignore them generating a constant
638 * function even in the easy case above *)
641 | NCic.Appl (f :: f_args)
643 List.exists (NCicMetaSubst.is_flexible status context ~subst) args ->
644 let mlen = List.length args in
645 let flen = List.length f_args in
646 let min_len = min mlen flen in
647 let mhe,margs = HExtlib.split_nth (mlen - min_len) args in
648 let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in
650 Some (List.fold_left2
652 unify status test_eq_only m s context t1 t2 swap
654 ((NCicUntrusted.mk_appl meta mhe)::margs)
655 ((NCicUntrusted.mk_appl f fhe)::fargs))
656 with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
660 (match easy_case with
663 (* This case handles "(?_f ..ti..) =?= t2", abstracting every
664 * non flexible ti (delift skips local context items that are
665 * flexible) from t2 in two steps:
666 * 1) ?_f := \..xi.. .?
667 * 2) ?_f ..ti.. =?= t2 --unif_machines-->
668 ?_f[..ti..] =?= t2 --instantiate-->
669 delift [..ti..] t2 *)
670 let metasenv, lambda_Mj =
671 lambda_intros status metasenv subst context (List.length args)
672 (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
674 let metasenv, subst =
675 unify status test_eq_only metasenv subst context
676 (C.Meta (i,l)) lambda_Mj swap
678 let metasenv, subst =
679 unify status test_eq_only metasenv subst context t1 t2 swap
682 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
683 let term = eta_reduce status subst term in
684 let subst = List.filter (fun (j,_) -> j <> i) subst in
685 metasenv, ((i, (name, ctx, term, ty)) :: subst)
686 with Not_found -> assert false))
688 | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
689 fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
691 | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
693 fo_unif0 during_delift status swap test_eq_only metasenv subst context
694 (false,hd1) (false,hd2) in
697 | C.Const r -> NCicEnvironment.get_relevance status r
699 let metasenv, subst, _ =
702 (fun (metasenv, subst, relevance) t1 t2 ->
704 match relevance with b::tl -> b,tl | _ -> true, [] in
705 let metasenv, subst =
706 try unify status test_eq_only metasenv subst context t1 t2
708 with UnificationFailure _ | Uncertain _ when not b ->
711 metasenv, subst, relevance)
712 (metasenv, subst, relevance) tl1 tl2
714 Invalid_argument _ ->
715 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
716 | KeepReducing _ | KeepReducingThis _ -> assert false
720 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
721 C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
722 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys status ref1 in
723 let _,_,ty,_ = List.nth itl tyno in
724 let rec remove_prods ~subst context ty =
725 let ty = NCicReduction.whd status ~subst context ty in
728 | C.Prod (name,so,ta) ->
729 remove_prods ~subst ((name,(C.Decl so))::context) ta
733 match remove_prods ~subst [] ty with
734 | C.Sort C.Prop -> true
737 (* if not (Ref.eq ref1 ref2) then
738 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
740 let metasenv, subst =
741 unify status test_eq_only metasenv subst context outtype1 outtype2 swap in
742 let metasenv, subst =
743 try unify status test_eq_only metasenv subst context term1 term2 swap
744 with UnificationFailure _ | Uncertain _ when is_prop ->
749 (fun (metasenv,subst) t1 t2 ->
750 unify status test_eq_only metasenv subst context t1 t2 swap)
751 (metasenv, subst) pl1 pl2
752 with Invalid_argument _ -> assert false)
753 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
754 | _ when norm1 && norm2 ->
755 if (could_reduce status ~subst context t1 || could_reduce status ~subst context t2) then
756 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
758 raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
759 | _ -> raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
760 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
762 and try_hints status swap test_eq_only metasenv subst context (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
763 if NCicUntrusted.metas_of_term status subst context t1 = [] &&
764 NCicUntrusted.metas_of_term status subst context t2 = []
767 (*D*) inside 'H'; try let rc =
768 pp(lazy ("\nProblema:\n" ^
769 ppterm status ~metasenv ~subst ~context t1 ^ " =?= " ^
770 ppterm status ~metasenv ~subst ~context t2));
772 NCicUnifHint.look_for_hint status metasenv subst context t1 t2
774 let rec cand_iter = function
775 | [] -> None (* raise exc *)
776 | (metasenv,(c1,c2),premises)::tl ->
777 pp (lazy ("\nProvo il candidato:\n" ^
781 ppterm status ~metasenv ~subst ~context a ^ " =?= " ^
782 ppterm status ~metasenv ~subst ~context b) premises) ^
783 "\n-------------------------------------------\n"^
784 ppterm status ~metasenv ~subst ~context c1 ^ " = " ^
785 ppterm status ~metasenv ~subst ~context c2));
787 (*D*) inside 'K'; try let rc =
789 fo_unif false status swap test_eq_only metasenv subst context mt1 (false,c1) in
791 fo_unif false status swap test_eq_only metasenv subst context (false,c2) mt2 in
794 (fun (metasenv, subst) (x,y) ->
795 unify status test_eq_only metasenv subst context x y false)
796 (metasenv, subst) (List.rev premises)
798 pp(lazy("FUNZIONA!"));
799 Some (metasenv, subst)
800 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
802 KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
803 | KeepReducingThis _ -> assert false
806 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
809 and fo_unif during_delift status swap test_eq_only metasenv subst context (norm1,t1 as nt1) (norm2,t2 as nt2)=
810 try fo_unif0 during_delift status swap test_eq_only metasenv subst context nt1 nt2
812 UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
813 raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
815 and unify status test_eq_only metasenv subst context t1 t2 swap =
816 (*D*) inside 'U'; try let rc =
817 let fo_unif_heads_and_cont_or_unwind_and_hints
818 test_eq_only metasenv subst m1 m2 cont hm1 hm2
820 let ms, continuation =
821 (* calling the continuation inside the outermost try is an option
822 and makes unification stronger, but looks not frequent to me
823 that heads unify but not the arguments and that an hints can fix
825 try fo_unif false status swap test_eq_only metasenv subst context m1 m2, cont
827 | UnificationFailure _
828 | KeepReducing _ | Uncertain _ as exn ->
829 let (t1,norm1),(t2,norm2) = hm1, hm2 in
831 try_hints status swap test_eq_only metasenv subst context
832 (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
834 | Some x -> x, fun x -> x
837 | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
838 | UnificationFailure _ | Uncertain _ as exn -> raise exn
843 let height_of = function
844 | NCic.Const (Ref.Ref (_,Ref.Def h))
845 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
846 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
847 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
850 let small_delta_step ~subst
851 ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
853 assert (not (norm1 && norm2));
855 x1,NCicReduction.reduce_machine status ~delta:0 ~subst context m2
857 NCicReduction.reduce_machine status ~delta:0 ~subst context m1,x2
859 let h1 = height_of t1 in
860 let h2 = height_of t2 in
861 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
862 NCicReduction.reduce_machine status ~delta ~subst context m1,
863 NCicReduction.reduce_machine status ~delta ~subst context m2
865 let rec unif_machines metasenv subst =
867 | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
868 (*D*) inside 'M'; try let rc =
870 ppterm status ~metasenv ~subst ~context
871 (NCicReduction.unwind status (k1,e1,t1,s1)) ^
873 ppterm status ~metasenv ~subst ~context
874 (NCicReduction.unwind status (k2,e2,t2,s2))));
875 pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
878 | C.Const r -> NCicEnvironment.get_relevance status r
880 let unif_from_stack (metasenv, subst) (t1, t2, b) =
882 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
883 let t2 = NCicReduction.from_stack ~delta:max_int t2 in
884 unif_machines metasenv subst (put_in_whd status subst context t1 t2)
885 with UnificationFailure _ | Uncertain _ when not b ->
888 let rec check_stack l1 l2 r todo =
890 | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
891 | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
893 NCicReduction.unwind status (k1,e1,t1,List.rev l1),
894 NCicReduction.unwind status (k2,e2,t2,List.rev l2),
897 let check_stack l1 l2 r =
899 | NCic.Meta _, _ | _, NCic.Meta _ ->
900 (NCicReduction.unwind status (k1,e1,t1,s1)),
901 (NCicReduction.unwind status (k2,e2,t2,s2)),[]
902 | _ -> check_stack l1 l2 r []
905 check_stack (List.rev s1) (List.rev s2) (List.rev relevance) in
907 fo_unif_heads_and_cont_or_unwind_and_hints
908 test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
909 (fun ms -> List.fold_left unif_from_stack ms todo)
912 | KeepReducing _ -> assert false
913 | KeepReducingThis _ ->
914 assert (not (norm1 && norm2));
915 unif_machines metasenv subst (small_delta_step ~subst m1 m2)
916 | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
917 -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
918 | UnificationFailure msg
919 when could_reduce status ~subst context (NCicReduction.unwind status (fst m1))
920 || could_reduce status ~subst context (NCicReduction.unwind status (fst m2))
921 -> raise (Uncertain msg)
922 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
924 try fo_unif_w_hints false status swap test_eq_only metasenv subst context (false,t1) (false,t2)
926 | KeepReducingThis (msg,tm1,tm2) ->
928 unif_machines metasenv subst (tm1,tm2)
930 | UnificationFailure _ -> raise (UnificationFailure msg)
931 | Uncertain _ -> raise (Uncertain msg)
932 | KeepReducing _ -> assert false)
933 | KeepReducing _ -> assert false
935 (*D*) in outside None; rc with KeepReducing _ -> assert false | exn -> outside (Some exn); raise exn
937 and delift_type_wrt_terms status metasenv subst context t args =
938 let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
939 let (metasenv, subst), t =
941 NCicMetaSubst.delift status ~unify:(unify_for_delift status)
942 metasenv subst context (-1) (0,NCic.Ctx lc) t
944 NCicMetaSubst.MetaSubstFailure _
945 | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t
951 let unify status ?(test_eq_only=false) ?(swap=false) metasenv subst context t1 t2=
953 unify status test_eq_only metasenv subst context t1 t2 swap;;
955 let fix_sorts status m s =
956 fix status m s true false (UnificationFailure (lazy "no sup"))