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 tipify status exc metasenv subst context t ty =
238 match NCicUntrusted.kind_of_meta attrs with
239 `IsType | `IsSort -> true
242 let rec optimize_meta metasenv subst =
246 let attrs,_,_ = NCicUtils.lookup_meta n metasenv in
247 if is_type attrs then
250 let _,cc,ty = NCicUtils.lookup_meta n metasenv in
251 let metasenv,subst,ty = sortfy status exc metasenv subst cc ty in
253 NCicUntrusted.replace_in_metasenv n
254 (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
259 NCicUtils.Meta_not_found _ ->
260 let attrs, _,bo,_ = NCicUtils.lookup_subst n subst in
261 if is_type attrs then
264 let _,cc,_,ty = NCicUtils.lookup_subst n subst in
265 let metasenv,subst,ty = sortfy status exc metasenv subst cc ty in
267 NCicUntrusted.replace_in_subst n
268 (fun attrs,cc,bo,_->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
271 optimize_meta metasenv subst (NCicSubstitution.subst_meta status lc bo))
272 | _ -> metasenv,subst,false
274 let metasenv,subst,b = optimize_meta metasenv subst t in
278 let metasenv,subst,_ = sortfy status exc metasenv subst context ty in
282 let put_in_whd status subst context m1 m2 =
283 NCicReduction.reduce_machine status ~delta:max_int ~subst context m1,
284 NCicReduction.reduce_machine status ~delta:max_int ~subst context m2
287 let rec instantiate status test_eq_only metasenv subst context n lc t swap =
288 (*D*) inside 'I'; try let rc =
289 pp (lazy(string_of_int n^" :=?= "^ppterm status ~metasenv ~subst ~context t));
291 UnificationFailure (mk_msg status metasenv subst context (NCic.Meta (n,lc)) t) in
292 let move_to_subst i ((_,cc,t,_) as infos) metasenv subst =
293 let metasenv = List.remove_assoc i metasenv in
294 pp(lazy(string_of_int n ^ " :==> "^ ppterm status ~metasenv ~subst ~context:cc t));
295 metasenv, (i,infos) :: subst
297 let delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv subst =
298 pp (lazy(string_of_int n ^ " := 111 = "^
299 ppterm status ~metasenv ~subst ~context t));
300 let (metasenv, subst), t =
302 NCicMetaSubst.delift status ~unify:(unify_for_delift status)
303 metasenv subst context n lc t
304 with NCicMetaSubst.Uncertain msg ->
305 pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
306 raise (Uncertain msg)
307 | NCicMetaSubst.MetaSubstFailure msg ->
308 pp (lazy ("delift fails: " ^ Lazy.force msg));
309 raise (UnificationFailure msg)
311 pp (lazy(string_of_int n ^ " := 222 = "^
312 ppterm status ~metasenv ~subst ~context:cc t^ppmetasenv status ~subst metasenv));
313 (* Unifying the types may have already instantiated n. *)
315 let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
316 let oldt = NCicSubstitution.subst_meta status lc oldt in
317 let t = NCicSubstitution.subst_meta status lc t in
318 (* conjecture: always fail --> occur check *)
319 unify status test_eq_only metasenv subst context t oldt false
320 with NCicUtils.Subst_not_found _ ->
321 move_to_subst n (attrs,cc,t,ty) metasenv subst
323 let attrs,cc,ty = NCicUtils.lookup_meta n metasenv in
324 let kind = NCicUntrusted.kind_of_meta attrs in
325 let metasenv,t = fix status metasenv subst swap test_eq_only exc t in
326 let ty_t = NCicTypeChecker.typeof status ~metasenv ~subst context t in
327 let metasenv,subst,t =
329 `IsSort -> sortfy status exc metasenv subst context t
330 | `IsType -> tipify status exc metasenv subst context t ty_t
331 | `IsTerm -> metasenv,subst,t in
335 NCic.Implicit (`Typeof _), NCic.Sort _ ->
336 move_to_subst n (attrs,cc,t,ty_t) metasenv subst
337 | NCic.Sort (NCic.Type u1), NCic.Sort s ->
340 NCic.Type u2, false ->
342 (unopt exc (NCicEnvironment.inf ~strict:false
343 (unopt exc (NCicEnvironment.inf ~strict:true u1) @ u2))))
344 | NCic.Type u2, true ->
345 if NCicEnvironment.universe_lt u2 u1 then
346 NCic.Sort (NCic.Type u2)
348 | NCic.Prop,_ -> NCic.Sort NCic.Prop
350 move_to_subst n (attrs,cc,s,ty) metasenv subst
351 | NCic.Implicit (`Typeof _), NCic.Meta _ ->
352 move_to_subst n (attrs,cc,t,ty_t) metasenv subst
354 | NCic.Meta _, NCic.Sort _ ->
355 pp (lazy ("On the types: " ^
356 ppterm status ~metasenv ~subst ~context ty ^ "=<=" ^
357 ppterm status ~metasenv ~subst ~context ty_t));
358 let metasenv, subst =
359 unify status false metasenv subst context ty_t ty false in
360 delift_to_subst test_eq_only n lc (attrs,cc,ty) t
361 context metasenv subst
366 NCic.Implicit (`Typeof _) ->
367 let (metasenv, subst), ty_t =
369 NCicMetaSubst.delift status ~unify:(unify_for_delift status)
370 metasenv subst context n lc ty_t
371 with NCicMetaSubst.Uncertain msg ->
372 pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
373 raise (Uncertain msg)
374 | NCicMetaSubst.MetaSubstFailure msg ->
375 pp (lazy ("delift fails: " ^ Lazy.force msg));
376 raise (UnificationFailure msg)
378 delift_to_subst test_eq_only n lc (attrs,cc,ty_t) t context metasenv
381 let lty = NCicSubstitution.subst_meta status lc ty in
382 pp (lazy ("On the types: " ^
383 ppterm status ~metasenv ~subst ~context ty_t ^ "=<=" ^
384 ppterm status ~metasenv ~subst ~context lty));
385 let metasenv, subst =
386 unify status false metasenv subst context ty_t lty false
388 delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv
390 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
392 and fo_unif_w_hints during_delift status swap test_eq_only metasenv subst context (_,t1 as m1) (_,t2 as m2) =
393 try fo_unif during_delift status swap test_eq_only metasenv subst context m1 m2
395 | UnificationFailure _ as exn -> raise exn
396 | KeepReducing _ | Uncertain _ as exn ->
397 let (t1,norm1 as tm1),(t2,norm2 as tm2) =
398 put_in_whd status subst context (0,[],t1,[]) (0,[],t2,[])
401 try_hints status swap test_eq_only metasenv subst context
402 (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
407 | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2))
408 | Uncertain _ as exn -> raise exn
411 and unify_for_delift status metasenv subst context t1 t2 =
415 (fo_unif_w_hints true status false true(*test_eq_only*) metasenv subst
416 context (false,t1) (false,t2))
417 (*(unify status true(*test_eq_only*) metasenv subst
418 context t1 t2 false)*)
419 with UnificationFailure _ | Uncertain _ | KeepReducingThis _ -> None
423 and fo_unif0 during_delift status swap test_eq_only metasenv subst context (norm1,t1 as m1) (norm2,t2 as m2) =
424 (*D*) inside 'F'; try let rc =
425 pp (lazy(" " ^ ppterm status ~metasenv ~subst ~context t1 ^
426 (if swap then " ==>?== "
428 ppterm status ~metasenv ~subst ~context t2 ^ ppmetasenv status
430 pp (lazy(" " ^ ppterm status ~metasenv ~subst:[] ~context t1 ^
431 (if swap then " ==>??== "
433 ppterm status ~metasenv ~subst:[] ~context t2 ^ ppmetasenv status
437 (* CSC: To speed up Oliboni's stuff. Why is it necessary, anyway?
439 NCicUntrusted.metas_of_term subst context t1 = [] &&
440 NCicUntrusted.metas_of_term subst context t2 = []
442 if NCicReduction.are_convertible ~metasenv ~subst context t1 t2 then
445 raise (UnificationFailure (lazy "Closed terms not convertible"))
449 | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl []
450 | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) ->
451 prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
453 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
454 let a, b = if swap then b,a else a,b in
455 if NCicEnvironment.universe_leq a b then metasenv, subst
456 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
457 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
458 if NCicEnvironment.universe_eq a b then metasenv, subst
459 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
460 | (C.Sort C.Prop,C.Sort (C.Type _)) when not swap ->
461 if (not test_eq_only) then metasenv, subst
462 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
463 | (C.Sort (C.Type _), C.Sort C.Prop) when swap ->
464 if (not test_eq_only) then metasenv, subst
465 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
467 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
468 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
469 let metasenv, subst = unify status true metasenv subst context s1 s2 swap in
470 unify status test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 swap
471 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
472 let metasenv,subst=unify status test_eq_only metasenv subst context ty1 ty2 swap in
473 let metasenv,subst=unify status test_eq_only metasenv subst context s1 s2 swap in
474 let context = (name1, C.Def (s1,ty1))::context in
475 unify status test_eq_only metasenv subst context t1 t2 swap
477 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
479 let l1 = NCicUtils.expand_local_context l1 in
480 let l2 = NCicUtils.expand_local_context l2 in
481 let metasenv, subst, to_restrict, _ =
483 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
485 let metasenv, subst =
486 unify status (*test_eq_only*) true metasenv subst context
487 (NCicSubstitution.lift status s1 t1) (NCicSubstitution.lift status s2 t2)
490 metasenv, subst, to_restrict, i-1
491 with UnificationFailure _ | Uncertain _ ->
492 metasenv, subst, i::to_restrict, i-1)
493 l1 l2 (metasenv, subst, [], List.length l1)
495 if to_restrict <> [] then
496 let metasenv, subst, _, _ =
497 NCicMetaSubst.restrict status metasenv subst n1 to_restrict
502 | Invalid_argument _ -> assert false
503 | NCicMetaSubst.MetaSubstFailure msg ->
505 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
506 let term1 = NCicSubstitution.subst_meta status lc1 term in
507 let term2 = NCicSubstitution.subst_meta status lc2 term in
508 unify status test_eq_only metasenv subst context term1 term2 swap
509 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
511 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
512 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
515 (fun (metasenv, subst) t1 t2 ->
516 unify status (*test_eq_only*) true metasenv subst context t1
518 (metasenv,subst) l1 l2
519 with Invalid_argument _ ->
520 raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)))
522 | _, NCic.Meta (n, _) when is_locked n subst && not swap && not during_delift ->
523 (let (metasenv, subst), i =
524 match NCicReduction.whd status ~subst context t1 with
525 | NCic.Appl (NCic.Meta (i,l) as meta :: args) ->
526 let metasenv, lambda_Mj =
527 lambda_intros status metasenv subst context (List.length args)
528 (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
530 unify status test_eq_only metasenv subst context
531 (C.Meta (i,l)) lambda_Mj false,
533 | NCic.Meta (i,_) -> (metasenv, subst), i
535 raise (UnificationFailure (lazy "Locked term vs non
536 flexible term; probably not saturated enough yet!"))
538 let t1 = NCicReduction.whd status ~subst context t1 in
540 match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
542 let metasenv, subst =
543 instantiate status test_eq_only metasenv subst context j lj t2 true
545 (* We need to remove the out_scope_tags to avoid propagation of
546 them that triggers again the ad-hoc case *)
548 List.map (fun (i,(tag,ctx,bo,ty)) ->
551 (function `InScope | `OutScope _ -> false | _ -> true) tag
557 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
558 let term = eta_reduce status subst term in
559 let subst = List.filter (fun (j,_) -> j <> i) subst in
560 metasenv, ((i, (name, ctx, term, ty)) :: subst)
561 with Not_found -> assert false))
562 | NCic.Meta (n, _), _ when is_locked n subst && swap ->
563 fo_unif0 during_delift status false test_eq_only metasenv subst context m2 m1
565 | _, C.Meta (n,lc) when List.mem_assoc n subst ->
566 let _,_,term,_ = NCicUtils.lookup_subst n subst in
567 let term = NCicSubstitution.subst_meta status lc term in
568 fo_unif0 during_delift status swap test_eq_only metasenv subst context
570 | C.Meta (n,_), _ when List.mem_assoc n subst ->
571 fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
573 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
574 let _,_,term,_ = NCicUtils.lookup_subst i subst in
575 let term = NCicSubstitution.subst_meta status l term in
576 fo_unif0 during_delift status swap test_eq_only metasenv subst context
577 m1 (false,mk_appl status ~upto:(List.length args) term args)
578 | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
579 fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
581 | C.Meta (n,_), C.Meta (m,lc') when
582 let _,cc1,_ = NCicUtils.lookup_meta n metasenv in
583 let _,cc2,_ = NCicUtils.lookup_meta m metasenv in
584 (n < m && cc1 = cc2) ||
585 let len1 = List.length cc1 in
586 let len2 = List.length cc2 in
587 len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
588 instantiate status test_eq_only metasenv subst context m lc'
589 (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
590 | C.Meta (n,lc), C.Meta (m,lc') when
591 let _,_,tyn = NCicUtils.lookup_meta n metasenv in
592 let _,_,tym = NCicUtils.lookup_meta m metasenv in
593 let tyn = NCicSubstitution.subst_meta status lc tyn in
594 let tym = NCicSubstitution.subst_meta status lc tym in
596 NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
597 NCicEnvironment.universe_lt u1 u2
599 instantiate status test_eq_only metasenv subst context m lc'
600 (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
601 | C.Meta (n,lc), t ->
602 instantiate status test_eq_only metasenv subst context n lc
603 (NCicReduction.head_beta_reduce status ~subst t) swap
604 | t, C.Meta (n,lc) ->
605 instantiate status test_eq_only metasenv subst context n lc
606 (NCicReduction.head_beta_reduce status ~subst t) (not swap)
608 (* higher order unification case *)
609 | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
610 (* this easy_case handles "(? ?) =?= (f a)", same number of
611 * args, preferring the instantiation "f" over "\_.f a" for the
612 * metavariable in head position. Since the arguments of the meta
613 * are flexible, delift would ignore them generating a constant
614 * function even in the easy case above *)
617 | NCic.Appl (f :: f_args)
619 List.exists (NCicMetaSubst.is_flexible status context ~subst) args ->
620 let mlen = List.length args in
621 let flen = List.length f_args in
622 let min_len = min mlen flen in
623 let mhe,margs = HExtlib.split_nth (mlen - min_len) args in
624 let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in
626 Some (List.fold_left2
628 unify status test_eq_only m s context t1 t2 swap
630 ((NCicUntrusted.mk_appl meta mhe)::margs)
631 ((NCicUntrusted.mk_appl f fhe)::fargs))
632 with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
636 (match easy_case with
639 (* This case handles "(?_f ..ti..) =?= t2", abstracting every
640 * non flexible ti (delift skips local context items that are
641 * flexible) from t2 in two steps:
642 * 1) ?_f := \..xi.. .?
643 * 2) ?_f ..ti.. =?= t2 --unif_machines-->
644 ?_f[..ti..] =?= t2 --instantiate-->
645 delift [..ti..] t2 *)
646 let metasenv, lambda_Mj =
647 lambda_intros status metasenv subst context (List.length args)
648 (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
650 let metasenv, subst =
651 unify status test_eq_only metasenv subst context
652 (C.Meta (i,l)) lambda_Mj swap
654 let metasenv, subst =
655 unify status test_eq_only metasenv subst context t1 t2 swap
658 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
659 let term = eta_reduce status subst term in
660 let subst = List.filter (fun (j,_) -> j <> i) subst in
661 metasenv, ((i, (name, ctx, term, ty)) :: subst)
662 with Not_found -> assert false))
664 | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
665 fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
667 | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
669 fo_unif0 during_delift status swap test_eq_only metasenv subst context
670 (false,hd1) (false,hd2) in
673 | C.Const r -> NCicEnvironment.get_relevance status r
675 let metasenv, subst, _ =
678 (fun (metasenv, subst, relevance) t1 t2 ->
680 match relevance with b::tl -> b,tl | _ -> true, [] in
681 let metasenv, subst =
682 try unify status test_eq_only metasenv subst context t1 t2
684 with UnificationFailure _ | Uncertain _ when not b ->
687 metasenv, subst, relevance)
688 (metasenv, subst, relevance) tl1 tl2
690 Invalid_argument _ ->
691 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
692 | KeepReducing _ | KeepReducingThis _ -> assert false
696 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
697 C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
698 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys status ref1 in
699 let _,_,ty,_ = List.nth itl tyno in
700 let rec remove_prods ~subst context ty =
701 let ty = NCicReduction.whd status ~subst context ty in
704 | C.Prod (name,so,ta) ->
705 remove_prods ~subst ((name,(C.Decl so))::context) ta
709 match remove_prods ~subst [] ty with
710 | C.Sort C.Prop -> true
713 (* if not (Ref.eq ref1 ref2) then
714 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
716 let metasenv, subst =
717 unify status test_eq_only metasenv subst context outtype1 outtype2 swap in
718 let metasenv, subst =
719 try unify status test_eq_only metasenv subst context term1 term2 swap
720 with UnificationFailure _ | Uncertain _ when is_prop ->
725 (fun (metasenv,subst) t1 t2 ->
726 unify status test_eq_only metasenv subst context t1 t2 swap)
727 (metasenv, subst) pl1 pl2
728 with Invalid_argument _ -> assert false)
729 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
730 | _ when norm1 && norm2 ->
731 if (could_reduce status ~subst context t1 || could_reduce status ~subst context t2) then
732 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
734 raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
735 | _ -> raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
736 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
738 and try_hints status swap test_eq_only metasenv subst context (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
739 if NCicUntrusted.metas_of_term status subst context t1 = [] &&
740 NCicUntrusted.metas_of_term status subst context t2 = []
743 (*D*) inside 'H'; try let rc =
744 pp(lazy ("\nProblema:\n" ^
745 ppterm status ~metasenv ~subst ~context t1 ^ " =?= " ^
746 ppterm status ~metasenv ~subst ~context t2));
748 NCicUnifHint.look_for_hint status metasenv subst context t1 t2
750 let rec cand_iter = function
751 | [] -> None (* raise exc *)
752 | (metasenv,(c1,c2),premises)::tl ->
753 pp (lazy ("\nProvo il candidato:\n" ^
757 ppterm status ~metasenv ~subst ~context a ^ " =?= " ^
758 ppterm status ~metasenv ~subst ~context b) premises) ^
759 "\n-------------------------------------------\n"^
760 ppterm status ~metasenv ~subst ~context c1 ^ " = " ^
761 ppterm status ~metasenv ~subst ~context c2));
763 (*D*) inside 'K'; try let rc =
765 fo_unif false status swap test_eq_only metasenv subst context mt1 (false,c1) in
767 fo_unif false status swap test_eq_only metasenv subst context (false,c2) mt2 in
770 (fun (metasenv, subst) (x,y) ->
771 unify status test_eq_only metasenv subst context x y false)
772 (metasenv, subst) (List.rev premises)
774 pp(lazy("FUNZIONA!"));
775 Some (metasenv, subst)
776 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
778 KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
779 | KeepReducingThis _ -> assert false
782 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
785 and fo_unif during_delift status swap test_eq_only metasenv subst context (norm1,t1 as nt1) (norm2,t2 as nt2)=
786 try fo_unif0 during_delift status swap test_eq_only metasenv subst context nt1 nt2
788 UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
789 raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
791 and unify status test_eq_only metasenv subst context t1 t2 swap =
792 (*D*) inside 'U'; try let rc =
793 let fo_unif_heads_and_cont_or_unwind_and_hints
794 test_eq_only metasenv subst m1 m2 cont hm1 hm2
796 let ms, continuation =
797 (* calling the continuation inside the outermost try is an option
798 and makes unification stronger, but looks not frequent to me
799 that heads unify but not the arguments and that an hints can fix
801 try fo_unif false status swap test_eq_only metasenv subst context m1 m2, cont
803 | UnificationFailure _
804 | KeepReducing _ | Uncertain _ as exn ->
805 let (t1,norm1),(t2,norm2) = hm1, hm2 in
807 try_hints status swap test_eq_only metasenv subst context
808 (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
810 | Some x -> x, fun x -> x
813 | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
814 | UnificationFailure _ | Uncertain _ as exn -> raise exn
819 let height_of = function
820 | NCic.Const (Ref.Ref (_,Ref.Def h))
821 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
822 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
823 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
826 let small_delta_step ~subst
827 ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
829 assert (not (norm1 && norm2));
831 x1,NCicReduction.reduce_machine status ~delta:0 ~subst context m2
833 NCicReduction.reduce_machine status ~delta:0 ~subst context m1,x2
835 let h1 = height_of t1 in
836 let h2 = height_of t2 in
837 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
838 NCicReduction.reduce_machine status ~delta ~subst context m1,
839 NCicReduction.reduce_machine status ~delta ~subst context m2
841 let rec unif_machines metasenv subst =
843 | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
844 (*D*) inside 'M'; try let rc =
846 ppterm status ~metasenv ~subst ~context
847 (NCicReduction.unwind status (k1,e1,t1,s1)) ^
849 ppterm status ~metasenv ~subst ~context
850 (NCicReduction.unwind status (k2,e2,t2,s2))));
851 pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
854 | C.Const r -> NCicEnvironment.get_relevance status r
856 let unif_from_stack (metasenv, subst) (t1, t2, b) =
858 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
859 let t2 = NCicReduction.from_stack ~delta:max_int t2 in
860 unif_machines metasenv subst (put_in_whd status subst context t1 t2)
861 with UnificationFailure _ | Uncertain _ when not b ->
864 let rec check_stack l1 l2 r todo =
866 | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
867 | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
869 NCicReduction.unwind status (k1,e1,t1,List.rev l1),
870 NCicReduction.unwind status (k2,e2,t2,List.rev l2),
873 let check_stack l1 l2 r =
875 | NCic.Meta _, _ | _, NCic.Meta _ ->
876 (NCicReduction.unwind status (k1,e1,t1,s1)),
877 (NCicReduction.unwind status (k2,e2,t2,s2)),[]
878 | _ -> check_stack l1 l2 r []
881 check_stack (List.rev s1) (List.rev s2) (List.rev relevance) in
883 fo_unif_heads_and_cont_or_unwind_and_hints
884 test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
885 (fun ms -> List.fold_left unif_from_stack ms todo)
888 | KeepReducing _ -> assert false
889 | KeepReducingThis _ ->
890 assert (not (norm1 && norm2));
891 unif_machines metasenv subst (small_delta_step ~subst m1 m2)
892 | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
893 -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
894 | UnificationFailure msg
895 when could_reduce status ~subst context (NCicReduction.unwind status (fst m1))
896 || could_reduce status ~subst context (NCicReduction.unwind status (fst m2))
897 -> raise (Uncertain msg)
898 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
900 try fo_unif_w_hints false status swap test_eq_only metasenv subst context (false,t1) (false,t2)
902 | KeepReducingThis (msg,tm1,tm2) ->
904 unif_machines metasenv subst (tm1,tm2)
906 | UnificationFailure _ -> raise (UnificationFailure msg)
907 | Uncertain _ -> raise (Uncertain msg)
908 | KeepReducing _ -> assert false)
909 | KeepReducing _ -> assert false
911 (*D*) in outside None; rc with KeepReducing _ -> assert false | exn -> outside (Some exn); raise exn
913 and delift_type_wrt_terms status metasenv subst context t args =
914 let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
915 let (metasenv, subst), t =
917 NCicMetaSubst.delift status ~unify:(unify_for_delift status)
918 metasenv subst context (-1) (0,NCic.Ctx lc) t
920 NCicMetaSubst.MetaSubstFailure _
921 | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t
927 let unify status ?(test_eq_only=false) ?(swap=false) metasenv subst context t1 t2=
929 unify status test_eq_only metasenv subst context t1 t2 swap;;
931 let fix_sorts status m s =
932 fix status m s true false (UnificationFailure (lazy "no sup"))