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 put_in_whd status subst context m1 m2 =
279 NCicReduction.reduce_machine status ~delta:max_int ~subst context m1,
280 NCicReduction.reduce_machine status ~delta:max_int ~subst context m2
283 let rec instantiate status test_eq_only metasenv subst context n lc t swap =
284 (*D*) inside 'I'; try let rc =
285 pp (lazy(string_of_int n^" :=?= "^ppterm status ~metasenv ~subst ~context t));
287 UnificationFailure (mk_msg status metasenv subst context (NCic.Meta (n,lc)) t) in
288 let move_to_subst i ((_,cc,t,_) as infos) metasenv subst =
289 let metasenv = List.remove_assoc i metasenv in
290 pp(lazy(string_of_int n ^ " :==> "^ ppterm status ~metasenv ~subst ~context:cc t));
291 metasenv, (i,infos) :: subst
293 let delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv subst =
294 pp (lazy(string_of_int n ^ " := 111 = "^
295 ppterm status ~metasenv ~subst ~context t));
296 let (metasenv, subst), t =
298 NCicMetaSubst.delift status ~unify:(unify_for_delift status)
299 metasenv subst context n lc t
300 with NCicMetaSubst.Uncertain msg ->
301 pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
302 raise (Uncertain msg)
303 | NCicMetaSubst.MetaSubstFailure msg ->
304 pp (lazy ("delift fails: " ^ Lazy.force msg));
305 raise (UnificationFailure msg)
307 pp (lazy(string_of_int n ^ " := 222 = "^
308 ppterm status ~metasenv ~subst ~context:cc t^ppmetasenv status ~subst metasenv));
309 (* Unifying the types may have already instantiated n. *)
311 let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
312 let oldt = NCicSubstitution.subst_meta status lc oldt in
313 let t = NCicSubstitution.subst_meta status lc t in
314 (* conjecture: always fail --> occur check *)
315 unify status test_eq_only metasenv subst context t oldt false
316 with NCicUtils.Subst_not_found _ ->
317 move_to_subst n (attrs,cc,t,ty) metasenv subst
319 let attrs,cc,ty = NCicUtils.lookup_meta n metasenv in
320 let kind = NCicUntrusted.kind_of_meta attrs in
321 let metasenv,t = fix status metasenv subst swap test_eq_only exc t in
322 let ty_t = NCicTypeChecker.typeof status ~metasenv ~subst context t in
323 let metasenv,subst,t =
325 `IsSort -> sortfy status exc metasenv subst context t
326 | `IsType -> tipify status exc metasenv subst context t ty_t
327 | `IsTerm -> metasenv,subst,t in
331 NCic.Implicit (`Typeof _), NCic.Sort _ ->
332 move_to_subst n (attrs,cc,t,ty_t) metasenv subst
333 | NCic.Sort (NCic.Type u1), NCic.Sort s ->
336 NCic.Type u2, false ->
338 (unopt exc (NCicEnvironment.inf ~strict:false
339 (unopt exc (NCicEnvironment.inf ~strict:true u1) @ u2))))
340 | NCic.Type u2, true ->
341 if NCicEnvironment.universe_lt u2 u1 then
342 NCic.Sort (NCic.Type u2)
344 | NCic.Prop,_ -> NCic.Sort NCic.Prop
346 move_to_subst n (attrs,cc,s,ty) metasenv subst
347 | NCic.Implicit (`Typeof _), NCic.Meta _ ->
348 move_to_subst n (attrs,cc,t,ty_t) metasenv subst
350 | NCic.Meta _, NCic.Sort _ ->
351 pp (lazy ("On the types: " ^
352 ppterm status ~metasenv ~subst ~context ty ^ "=<=" ^
353 ppterm status ~metasenv ~subst ~context ty_t));
354 let metasenv, subst =
355 unify status false metasenv subst context ty_t ty false in
356 delift_to_subst test_eq_only n lc (attrs,cc,ty) t
357 context metasenv subst
362 NCic.Implicit (`Typeof _) ->
363 let (metasenv, subst), ty_t =
365 NCicMetaSubst.delift status ~unify:(unify_for_delift status)
366 metasenv subst context n lc ty_t
367 with NCicMetaSubst.Uncertain msg ->
368 pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
369 raise (Uncertain msg)
370 | NCicMetaSubst.MetaSubstFailure msg ->
371 pp (lazy ("delift fails: " ^ Lazy.force msg));
372 raise (UnificationFailure msg)
374 delift_to_subst test_eq_only n lc (attrs,cc,ty_t) t context metasenv
377 let lty = NCicSubstitution.subst_meta status lc ty in
378 pp (lazy ("On the types: " ^
379 ppterm status ~metasenv ~subst ~context ty_t ^ "=<=" ^
380 ppterm status ~metasenv ~subst ~context lty));
381 let metasenv, subst =
382 unify status false metasenv subst context ty_t lty false
384 delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv
386 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
388 and fo_unif_w_hints during_delift status swap test_eq_only metasenv subst context (_,t1 as m1) (_,t2 as m2) =
389 try fo_unif during_delift status swap test_eq_only metasenv subst context m1 m2
391 | UnificationFailure _ as exn -> raise exn
392 | KeepReducing _ | Uncertain _ as exn ->
393 let (t1,norm1 as tm1),(t2,norm2 as tm2) =
394 put_in_whd status subst context (0,[],t1,[]) (0,[],t2,[])
397 try_hints status swap test_eq_only metasenv subst context
398 (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
403 | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2))
404 | Uncertain _ as exn -> raise exn
407 and unify_for_delift status metasenv subst context t1 t2 =
411 (fo_unif_w_hints true status false true(*test_eq_only*) metasenv subst
412 context (false,t1) (false,t2))
413 with UnificationFailure _ | Uncertain _ | KeepReducingThis _ -> None
417 and fo_unif0 during_delift status swap test_eq_only metasenv subst context (norm1,t1 as m1) (norm2,t2 as m2) =
418 (*D*) inside 'F'; try let rc =
419 pp (lazy(" " ^ ppterm status ~metasenv ~subst ~context t1 ^
420 (if swap then " ==>?== "
422 ppterm status ~metasenv ~subst ~context t2 ^ ppmetasenv status
424 pp (lazy(" " ^ ppterm status ~metasenv ~subst:[] ~context t1 ^
425 (if swap then " ==>??== "
427 ppterm status ~metasenv ~subst:[] ~context t2 ^ ppmetasenv status
431 (* CSC: To speed up Oliboni's stuff. Why is it necessary, anyway?
433 NCicUntrusted.metas_of_term subst context t1 = [] &&
434 NCicUntrusted.metas_of_term subst context t2 = []
436 if NCicReduction.are_convertible ~metasenv ~subst context t1 t2 then
439 raise (UnificationFailure (lazy "Closed terms not convertible"))
443 | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl []
444 | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) ->
445 prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
447 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
448 let a, b = if swap then b,a else a,b in
449 if NCicEnvironment.universe_leq a b then metasenv, subst
450 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
451 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
452 if NCicEnvironment.universe_eq a b then metasenv, subst
453 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
454 | (C.Sort C.Prop,C.Sort (C.Type _)) when not swap ->
455 if (not test_eq_only) then metasenv, subst
456 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
457 | (C.Sort (C.Type _), C.Sort C.Prop) when swap ->
458 if (not test_eq_only) then metasenv, subst
459 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
461 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
462 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
463 let metasenv, subst = unify status true metasenv subst context s1 s2 swap in
464 unify status test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 swap
465 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
466 let metasenv,subst=unify status test_eq_only metasenv subst context ty1 ty2 swap in
467 let metasenv,subst=unify status test_eq_only metasenv subst context s1 s2 swap in
468 let context = (name1, C.Def (s1,ty1))::context in
469 unify status test_eq_only metasenv subst context t1 t2 swap
471 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
473 let l1 = NCicUtils.expand_local_context l1 in
474 let l2 = NCicUtils.expand_local_context l2 in
475 let metasenv, subst, to_restrict, _ =
477 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
479 let metasenv, subst =
480 unify status (*test_eq_only*) true metasenv subst context
481 (NCicSubstitution.lift status s1 t1) (NCicSubstitution.lift status s2 t2)
484 metasenv, subst, to_restrict, i-1
485 with UnificationFailure _ | Uncertain _ ->
486 metasenv, subst, i::to_restrict, i-1)
487 l1 l2 (metasenv, subst, [], List.length l1)
489 if to_restrict <> [] then
490 let metasenv, subst, _, _ =
491 NCicMetaSubst.restrict status metasenv subst n1 to_restrict
496 | Invalid_argument _ -> assert false
497 | NCicMetaSubst.MetaSubstFailure msg ->
499 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
500 let term1 = NCicSubstitution.subst_meta status lc1 term in
501 let term2 = NCicSubstitution.subst_meta status lc2 term in
502 unify status test_eq_only metasenv subst context term1 term2 swap
503 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
505 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
506 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
509 (fun (metasenv, subst) t1 t2 ->
510 unify status (*test_eq_only*) true metasenv subst context t1
512 (metasenv,subst) l1 l2
513 with Invalid_argument _ ->
514 raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)))
516 | _, NCic.Meta (n, _) when is_locked n subst && not swap && not during_delift ->
517 (let (metasenv, subst), i =
518 match NCicReduction.whd status ~subst context t1 with
519 | NCic.Appl (NCic.Meta (i,l) as meta :: args) ->
520 let metasenv, lambda_Mj =
521 lambda_intros status metasenv subst context (List.length args)
522 (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
524 unify status test_eq_only metasenv subst context
525 (C.Meta (i,l)) lambda_Mj false,
527 | NCic.Meta (i,_) -> (metasenv, subst), i
529 raise (UnificationFailure (lazy "Locked term vs non
530 flexible term; probably not saturated enough yet!"))
532 let t1 = NCicReduction.whd status ~subst context t1 in
534 match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
536 let metasenv, subst =
537 instantiate status test_eq_only metasenv subst context j lj t2 true
539 (* We need to remove the out_scope_tags to avoid propagation of
540 them that triggers again the ad-hoc case *)
542 List.map (fun (i,(tag,ctx,bo,ty)) ->
545 (function `InScope | `OutScope _ -> false | _ -> true) tag
551 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
552 let term = eta_reduce status subst term in
553 let subst = List.filter (fun (j,_) -> j <> i) subst in
554 metasenv, ((i, (name, ctx, term, ty)) :: subst)
555 with Not_found -> assert false))
556 | NCic.Meta (n, _), _ when is_locked n subst && swap ->
557 fo_unif0 during_delift status false test_eq_only metasenv subst context m2 m1
559 | _, C.Meta (n,lc) when List.mem_assoc n subst ->
560 let _,_,term,_ = NCicUtils.lookup_subst n subst in
561 let term = NCicSubstitution.subst_meta status lc term in
562 fo_unif0 during_delift status swap test_eq_only metasenv subst context
564 | C.Meta (n,_), _ when List.mem_assoc n subst ->
565 fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
567 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
568 let _,_,term,_ = NCicUtils.lookup_subst i subst in
569 let term = NCicSubstitution.subst_meta status l term in
570 fo_unif0 during_delift status swap test_eq_only metasenv subst context
571 m1 (false,mk_appl status ~upto:(List.length args) term args)
572 | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
573 fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
575 | C.Meta (n,_), C.Meta (m,lc') when
576 let _,cc1,_ = NCicUtils.lookup_meta n metasenv in
577 let _,cc2,_ = NCicUtils.lookup_meta m metasenv in
578 (n < m && cc1 = cc2) ||
579 let len1 = List.length cc1 in
580 let len2 = List.length cc2 in
581 len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
582 instantiate status test_eq_only metasenv subst context m lc'
583 (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
584 | C.Meta (n,lc), C.Meta (m,lc') when
585 let _,_,tyn = NCicUtils.lookup_meta n metasenv in
586 let _,_,tym = NCicUtils.lookup_meta m metasenv in
587 let tyn = NCicSubstitution.subst_meta status lc tyn in
588 let tym = NCicSubstitution.subst_meta status lc tym in
590 NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
591 NCicEnvironment.universe_lt u1 u2
593 instantiate status test_eq_only metasenv subst context m lc'
594 (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
595 | C.Meta (n,lc), t ->
596 instantiate status test_eq_only metasenv subst context n lc
597 (NCicReduction.head_beta_reduce status ~subst t) swap
598 | t, C.Meta (n,lc) ->
599 instantiate status test_eq_only metasenv subst context n lc
600 (NCicReduction.head_beta_reduce status ~subst t) (not swap)
602 (* higher order unification case *)
603 | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
604 (* this easy_case handles "(? ?) =?= (f a)", same number of
605 * args, preferring the instantiation "f" over "\_.f a" for the
606 * metavariable in head position. Since the arguments of the meta
607 * are flexible, delift would ignore them generating a constant
608 * function even in the easy case above *)
611 | NCic.Appl (f :: f_args)
613 List.exists (NCicMetaSubst.is_flexible status context ~subst) args ->
614 let mlen = List.length args in
615 let flen = List.length f_args in
616 let min_len = min mlen flen in
617 let mhe,margs = HExtlib.split_nth (mlen - min_len) args in
618 let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in
620 Some (List.fold_left2
622 unify status test_eq_only m s context t1 t2 swap
624 ((NCicUntrusted.mk_appl meta mhe)::margs)
625 ((NCicUntrusted.mk_appl f fhe)::fargs))
626 with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
630 (match easy_case with
633 (* This case handles "(?_f ..ti..) =?= t2", abstracting every
634 * non flexible ti (delift skips local context items that are
635 * flexible) from t2 in two steps:
636 * 1) ?_f := \..xi.. .?
637 * 2) ?_f ..ti.. =?= t2 --unif_machines-->
638 ?_f[..ti..] =?= t2 --instantiate-->
639 delift [..ti..] t2 *)
640 let metasenv, lambda_Mj =
641 lambda_intros status metasenv subst context (List.length args)
642 (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
644 let metasenv, subst =
645 unify status test_eq_only metasenv subst context
646 (C.Meta (i,l)) lambda_Mj swap
648 let metasenv, subst =
649 unify status test_eq_only metasenv subst context t1 t2 swap
652 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
653 let term = eta_reduce status subst term in
654 let subst = List.filter (fun (j,_) -> j <> i) subst in
655 metasenv, ((i, (name, ctx, term, ty)) :: subst)
656 with Not_found -> assert false))
658 | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
659 fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
661 | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
663 fo_unif0 during_delift status swap test_eq_only metasenv subst context
664 (false,hd1) (false,hd2) in
667 | C.Const r -> NCicEnvironment.get_relevance status r
669 let metasenv, subst, _ =
672 (fun (metasenv, subst, relevance) t1 t2 ->
674 match relevance with b::tl -> b,tl | _ -> true, [] in
675 let metasenv, subst =
676 try unify status test_eq_only metasenv subst context t1 t2
678 with UnificationFailure _ | Uncertain _ when not b ->
681 metasenv, subst, relevance)
682 (metasenv, subst, relevance) tl1 tl2
684 Invalid_argument _ ->
685 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
686 | KeepReducing _ | KeepReducingThis _ -> assert false
690 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
691 C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
692 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys status ref1 in
693 let _,_,ty,_ = List.nth itl tyno in
694 let rec remove_prods ~subst context ty =
695 let ty = NCicReduction.whd status ~subst context ty in
698 | C.Prod (name,so,ta) ->
699 remove_prods ~subst ((name,(C.Decl so))::context) ta
703 match remove_prods ~subst [] ty with
704 | C.Sort C.Prop -> true
707 (* if not (Ref.eq ref1 ref2) then
708 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
710 let metasenv, subst =
711 unify status test_eq_only metasenv subst context outtype1 outtype2 swap in
712 let metasenv, subst =
713 try unify status test_eq_only metasenv subst context term1 term2 swap
714 with UnificationFailure _ | Uncertain _ when is_prop ->
719 (fun (metasenv,subst) t1 t2 ->
720 unify status test_eq_only metasenv subst context t1 t2 swap)
721 (metasenv, subst) pl1 pl2
722 with Invalid_argument _ -> assert false)
723 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
724 | _ when norm1 && norm2 ->
725 if (could_reduce t1 || could_reduce t2) then
726 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
728 raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
729 | _ -> raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
730 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
732 and try_hints status swap test_eq_only metasenv subst context (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
733 if NCicUntrusted.metas_of_term status subst context t1 = [] &&
734 NCicUntrusted.metas_of_term status subst context t2 = []
737 (*D*) inside 'H'; try let rc =
738 pp(lazy ("\nProblema:\n" ^
739 ppterm status ~metasenv ~subst ~context t1 ^ " =?= " ^
740 ppterm status ~metasenv ~subst ~context t2));
742 NCicUnifHint.look_for_hint status metasenv subst context t1 t2
744 let rec cand_iter = function
745 | [] -> None (* raise exc *)
746 | (metasenv,(c1,c2),premises)::tl ->
747 pp (lazy ("\nProvo il candidato:\n" ^
751 ppterm status ~metasenv ~subst ~context a ^ " =?= " ^
752 ppterm status ~metasenv ~subst ~context b) premises) ^
753 "\n-------------------------------------------\n"^
754 ppterm status ~metasenv ~subst ~context c1 ^ " = " ^
755 ppterm status ~metasenv ~subst ~context c2));
757 (*D*) inside 'K'; try let rc =
759 fo_unif false status swap test_eq_only metasenv subst context mt1 (false,c1) in
761 fo_unif false status swap test_eq_only metasenv subst context (false,c2) mt2 in
764 (fun (metasenv, subst) (x,y) ->
765 unify status test_eq_only metasenv subst context x y false)
766 (metasenv, subst) (List.rev premises)
768 pp(lazy("FUNZIONA!"));
769 Some (metasenv, subst)
770 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
772 KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
773 | KeepReducingThis _ -> assert false
776 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
779 and fo_unif during_delift status swap test_eq_only metasenv subst context (norm1,t1 as nt1) (norm2,t2 as nt2)=
780 try fo_unif0 during_delift status swap test_eq_only metasenv subst context nt1 nt2
782 UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
783 raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
785 and unify status test_eq_only metasenv subst context t1 t2 swap =
786 (*D*) inside 'U'; try let rc =
787 let fo_unif_heads_and_cont_or_unwind_and_hints
788 test_eq_only metasenv subst m1 m2 cont hm1 hm2
790 let ms, continuation =
791 (* calling the continuation inside the outermost try is an option
792 and makes unification stronger, but looks not frequent to me
793 that heads unify but not the arguments and that an hints can fix
795 try fo_unif false status swap test_eq_only metasenv subst context m1 m2, cont
797 | UnificationFailure _
798 | KeepReducing _ | Uncertain _ as exn ->
799 let (t1,norm1),(t2,norm2) = hm1, hm2 in
801 try_hints status swap test_eq_only metasenv subst context
802 (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
804 | Some x -> x, fun x -> x
807 | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
808 | UnificationFailure _ | Uncertain _ as exn -> raise exn
813 let height_of = function
814 | NCic.Const (Ref.Ref (_,Ref.Def h))
815 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
816 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
817 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
820 let small_delta_step ~subst
821 ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
823 assert (not (norm1 && norm2));
825 x1,NCicReduction.reduce_machine status ~delta:0 ~subst context m2
827 NCicReduction.reduce_machine status ~delta:0 ~subst context m1,x2
829 let h1 = height_of t1 in
830 let h2 = height_of t2 in
831 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
832 NCicReduction.reduce_machine status ~delta ~subst context m1,
833 NCicReduction.reduce_machine status ~delta ~subst context m2
835 let rec unif_machines metasenv subst =
837 | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
838 (*D*) inside 'M'; try let rc =
840 ppterm status ~metasenv ~subst ~context
841 (NCicReduction.unwind status (k1,e1,t1,s1)) ^
843 ppterm status ~metasenv ~subst ~context
844 (NCicReduction.unwind status (k2,e2,t2,s2))));
845 pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
848 | C.Const r -> NCicEnvironment.get_relevance status r
850 let unif_from_stack (metasenv, subst) (t1, t2, b) =
852 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
853 let t2 = NCicReduction.from_stack ~delta:max_int t2 in
854 unif_machines metasenv subst (put_in_whd status subst context t1 t2)
855 with UnificationFailure _ | Uncertain _ when not b ->
858 let rec check_stack l1 l2 r todo =
860 | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
861 | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
863 NCicReduction.unwind status (k1,e1,t1,List.rev l1),
864 NCicReduction.unwind status (k2,e2,t2,List.rev l2),
867 let check_stack l1 l2 r =
869 | NCic.Meta _, _ | _, NCic.Meta _ ->
870 (NCicReduction.unwind status (k1,e1,t1,s1)),
871 (NCicReduction.unwind status (k2,e2,t2,s2)),[]
872 | _ -> check_stack l1 l2 r []
875 check_stack (List.rev s1) (List.rev s2) (List.rev relevance) in
877 fo_unif_heads_and_cont_or_unwind_and_hints
878 test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
879 (fun ms -> List.fold_left unif_from_stack ms todo)
882 | KeepReducing _ -> assert false
883 | KeepReducingThis _ ->
884 assert (not (norm1 && norm2));
885 unif_machines metasenv subst (small_delta_step ~subst m1 m2)
886 | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
887 -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
888 | UnificationFailure msg
889 when could_reduce (NCicReduction.unwind status (fst m1))
890 || could_reduce (NCicReduction.unwind status (fst m2))
891 -> raise (Uncertain msg)
892 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
894 try fo_unif_w_hints false status swap test_eq_only metasenv subst context (false,t1) (false,t2)
896 | KeepReducingThis (msg,tm1,tm2) ->
898 unif_machines metasenv subst (tm1,tm2)
900 | UnificationFailure _ -> raise (UnificationFailure msg)
901 | Uncertain _ -> raise (Uncertain msg)
902 | KeepReducing _ -> assert false)
903 | KeepReducing _ -> assert false
905 (*D*) in outside None; rc with KeepReducing _ -> assert false | exn -> outside (Some exn); raise exn
907 and delift_type_wrt_terms status metasenv subst context t args =
908 let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
909 let (metasenv, subst), t =
911 NCicMetaSubst.delift status ~unify:(unify_for_delift status)
912 metasenv subst context (-1) (0,NCic.Ctx lc) t
914 NCicMetaSubst.MetaSubstFailure _
915 | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t
921 let unify status ?(test_eq_only=false) ?(swap=false) metasenv subst context t1 t2=
923 unify status test_eq_only metasenv subst context t1 t2 swap;;
925 let fix_sorts status m s =
926 fix status m s true false (UnificationFailure (lazy "no sup"))