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 (_,_,arg,_) -> could_reduce status ~subst context arg
145 | C.Appl (he::_) -> could_reduce status ~subst context he
146 | C.Sort _ | C.Rel _ | C.Prod _ | C.Lambda _ | C.Const _ -> false
147 | C.Appl [] | C.LetIn _ | C.Implicit _ -> assert false
150 let rec lambda_intros status metasenv subst context argsno ty =
151 pp (lazy ("LAMBDA INTROS: " ^ ppterm status ~metasenv ~subst ~context ty));
154 let metasenv, _, bo, _ =
155 NCicMetaSubst.mk_meta metasenv context ~with_type:ty `IsTerm
159 (match NCicReduction.whd status ~subst context ty with
162 lambda_intros status metasenv subst
163 ((n,C.Decl so)::context) (argsno - 1) ta
165 metasenv,C.Lambda (n,so,bo)
169 let unopt exc = function None -> raise exc | Some x -> x ;;
171 let fix (status:#NCic.status) metasenv subst is_sup test_eq_only exc t =
172 (*D*) inside 'f'; try let rc =
173 pp (lazy (status#ppterm ~metasenv ~subst ~context:[] t));
174 let rec aux test_eq_only metasenv = function
175 | NCic.Prod (n,so,ta) ->
176 let metasenv,so = aux true metasenv so in
177 let metasenv,ta = aux test_eq_only metasenv ta in
178 metasenv,NCic.Prod (n,so,ta)
179 | NCic.Sort (NCic.Type [(`CProp|`Type),_]) as orig when test_eq_only ->
181 | NCic.Sort (NCic.Type _) when test_eq_only -> raise exc
182 | NCic.Sort (NCic.Type u) when is_sup ->
183 metasenv, NCic.Sort (NCic.Type (unopt exc (NCicEnvironment.sup u)))
184 | NCic.Sort (NCic.Type u) ->
185 metasenv, NCic.Sort (NCic.Type
186 (unopt exc (NCicEnvironment.inf ~strict:false u)))
187 | NCic.Meta (n,_) as orig ->
189 let _,_,_,_ = NCicUtils.lookup_subst n subst in metasenv,orig
190 with NCicUtils.Subst_not_found _ ->
191 let metasenv, _ = NCicMetaSubst.extend_meta metasenv n in
194 NCicUntrusted.map_term_fold_a status (fun _ x -> x) test_eq_only aux metasenv t
196 aux test_eq_only metasenv t
197 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
200 let metasenv_to_subst n (kind,context,ty) metasenv subst =
201 let infos,metasenv = List.partition (fun (n',_) -> n = n') metasenv in
202 let attrs,octx,oty = match infos with [_,infos] -> infos | _ -> assert false in
203 if octx=context && oty=ty then
204 (n,(NCicUntrusted.set_kind kind attrs, octx, oty))::metasenv,subst
206 let metasenv, _, bo, _ =
207 NCicMetaSubst.mk_meta metasenv context ~attrs ~with_type:ty kind in
208 let subst = (n,(NCicUntrusted.set_kind kind attrs,octx,bo,oty))::subst in
212 let rec sortfy status exc metasenv subst context t =
213 let t = NCicReduction.whd status ~subst context t in
216 | NCic.Sort _ -> metasenv, subst
218 let attrs, context, ty = NCicUtils.lookup_meta n metasenv in
219 let kind = NCicUntrusted.kind_of_meta attrs in
220 if kind = `IsSort then
224 | NCic.Implicit (`Typeof _) ->
225 metasenv_to_subst n (`IsSort,[],ty) metasenv subst
227 let metasenv,subst,ty = sortfy status exc metasenv subst context ty in
228 metasenv_to_subst n (`IsSort,[],ty) metasenv subst)
229 | NCic.Implicit _ -> assert false
234 let tipify status exc metasenv subst context t ty =
236 match NCicUntrusted.kind_of_meta attrs with
237 `IsType | `IsSort -> true
240 let rec optimize_meta metasenv subst =
244 let attrs,_,_ = NCicUtils.lookup_meta n metasenv in
245 if is_type attrs then
248 let _,cc,ty = NCicUtils.lookup_meta n metasenv in
249 let metasenv,subst,ty = sortfy status exc metasenv subst cc ty in
251 NCicUntrusted.replace_in_metasenv n
252 (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
257 NCicUtils.Meta_not_found _ ->
258 let attrs, _,bo,_ = NCicUtils.lookup_subst n subst in
259 if is_type attrs then
262 let _,cc,_,ty = NCicUtils.lookup_subst n subst in
263 let metasenv,subst,ty = sortfy status exc metasenv subst cc ty in
265 NCicUntrusted.replace_in_subst n
266 (fun attrs,cc,bo,_->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
269 optimize_meta metasenv subst (NCicSubstitution.subst_meta status lc bo))
270 | _ -> metasenv,subst,false
272 let metasenv,subst,b = optimize_meta metasenv subst t in
276 let metasenv,subst,_ = sortfy status exc metasenv subst context ty in
280 let put_in_whd status subst context m1 m2 =
281 NCicReduction.reduce_machine status ~delta:max_int ~subst context m1,
282 NCicReduction.reduce_machine status ~delta:max_int ~subst context m2
285 let rec instantiate status test_eq_only metasenv subst context n lc t swap =
286 (*D*) inside 'I'; try let rc =
287 pp (lazy(string_of_int n^" :=?= "^ppterm status ~metasenv ~subst ~context t));
289 UnificationFailure (mk_msg status metasenv subst context (NCic.Meta (n,lc)) t) in
290 let move_to_subst i ((_,cc,t,_) as infos) metasenv subst =
291 let metasenv = List.remove_assoc i metasenv in
292 pp(lazy(string_of_int n ^ " :==> "^ ppterm status ~metasenv ~subst ~context:cc t));
293 metasenv, (i,infos) :: subst
295 let delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv subst =
296 pp (lazy(string_of_int n ^ " := 111 = "^
297 ppterm status ~metasenv ~subst ~context t));
298 let (metasenv, subst), t =
300 NCicMetaSubst.delift status ~unify:(unify_for_delift status)
301 metasenv subst context n lc t
302 with NCicMetaSubst.Uncertain msg ->
303 pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
304 raise (Uncertain msg)
305 | NCicMetaSubst.MetaSubstFailure msg ->
306 pp (lazy ("delift fails: " ^ Lazy.force msg));
307 raise (UnificationFailure msg)
309 pp (lazy(string_of_int n ^ " := 222 = "^
310 ppterm status ~metasenv ~subst ~context:cc t^ppmetasenv status ~subst metasenv));
311 (* Unifying the types may have already instantiated n. *)
313 let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
314 let oldt = NCicSubstitution.subst_meta status lc oldt in
315 let t = NCicSubstitution.subst_meta status lc t in
316 (* conjecture: always fail --> occur check *)
317 unify status test_eq_only metasenv subst context t oldt false
318 with NCicUtils.Subst_not_found _ ->
319 move_to_subst n (attrs,cc,t,ty) metasenv subst
321 let attrs,cc,ty = NCicUtils.lookup_meta n metasenv in
322 let kind = NCicUntrusted.kind_of_meta attrs in
323 let metasenv,t = fix status metasenv subst swap test_eq_only exc t in
324 let ty_t = NCicTypeChecker.typeof status ~metasenv ~subst context t in
325 let metasenv,subst,t =
327 `IsSort -> sortfy status exc metasenv subst context t
328 | `IsType -> tipify status exc metasenv subst context t ty_t
329 | `IsTerm -> metasenv,subst,t in
333 NCic.Implicit (`Typeof _), NCic.Sort _ ->
334 move_to_subst n (attrs,cc,t,ty_t) metasenv subst
335 | NCic.Sort (NCic.Type u1), NCic.Sort s ->
338 NCic.Type u2, false ->
340 (unopt exc (NCicEnvironment.inf ~strict:false
341 (unopt exc (NCicEnvironment.inf ~strict:true u1) @ u2))))
342 | NCic.Type u2, true ->
343 if NCicEnvironment.universe_lt u2 u1 then
344 NCic.Sort (NCic.Type u2)
346 | NCic.Prop,_ -> NCic.Sort NCic.Prop
348 move_to_subst n (attrs,cc,s,ty) metasenv subst
349 | NCic.Implicit (`Typeof _), NCic.Meta _ ->
350 move_to_subst n (attrs,cc,t,ty_t) metasenv subst
352 | NCic.Meta _, NCic.Sort _ ->
353 pp (lazy ("On the types: " ^
354 ppterm status ~metasenv ~subst ~context ty ^ "=<=" ^
355 ppterm status ~metasenv ~subst ~context ty_t));
356 let metasenv, subst =
357 unify status false metasenv subst context ty_t ty false in
358 delift_to_subst test_eq_only n lc (attrs,cc,ty) t
359 context metasenv subst
364 NCic.Implicit (`Typeof _) ->
365 let (metasenv, subst), ty_t =
367 NCicMetaSubst.delift status ~unify:(unify_for_delift status)
368 metasenv subst context n lc ty_t
369 with NCicMetaSubst.Uncertain msg ->
370 pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
371 raise (Uncertain msg)
372 | NCicMetaSubst.MetaSubstFailure msg ->
373 pp (lazy ("delift fails: " ^ Lazy.force msg));
374 raise (UnificationFailure msg)
376 delift_to_subst test_eq_only n lc (attrs,cc,ty_t) t context metasenv
379 let lty = NCicSubstitution.subst_meta status lc ty in
380 pp (lazy ("On the types: " ^
381 ppterm status ~metasenv ~subst ~context ty_t ^ "=<=" ^
382 ppterm status ~metasenv ~subst ~context lty));
383 let metasenv, subst =
384 unify status false metasenv subst context ty_t lty false
386 delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv
388 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
390 and fo_unif_w_hints during_delift status swap test_eq_only metasenv subst context (_,t1 as m1) (_,t2 as m2) =
391 try fo_unif during_delift status swap test_eq_only metasenv subst context m1 m2
393 | UnificationFailure _ as exn -> raise exn
394 | KeepReducing _ | Uncertain _ as exn ->
395 let (t1,norm1 as tm1),(t2,norm2 as tm2) =
396 put_in_whd status subst context (0,[],t1,[]) (0,[],t2,[])
399 try_hints status swap test_eq_only metasenv subst context
400 (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
405 | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2))
406 | Uncertain _ as exn -> raise exn
409 and unify_for_delift status metasenv subst context t1 t2 =
413 (fo_unif_w_hints true status false true(*test_eq_only*) metasenv subst
414 context (false,t1) (false,t2))
415 with UnificationFailure _ | Uncertain _ | KeepReducingThis _ -> None
419 and fo_unif0 during_delift status swap test_eq_only metasenv subst context (norm1,t1 as m1) (norm2,t2 as m2) =
420 (*D*) inside 'F'; try let rc =
421 pp (lazy(" " ^ ppterm status ~metasenv ~subst ~context t1 ^
422 (if swap then " ==>?== "
424 ppterm status ~metasenv ~subst ~context t2 ^ ppmetasenv status
426 pp (lazy(" " ^ ppterm status ~metasenv ~subst:[] ~context t1 ^
427 (if swap then " ==>??== "
429 ppterm status ~metasenv ~subst:[] ~context t2 ^ ppmetasenv status
433 (* CSC: To speed up Oliboni's stuff. Why is it necessary, anyway?
435 NCicUntrusted.metas_of_term subst context t1 = [] &&
436 NCicUntrusted.metas_of_term subst context t2 = []
438 if NCicReduction.are_convertible ~metasenv ~subst context t1 t2 then
441 raise (UnificationFailure (lazy "Closed terms not convertible"))
445 | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl []
446 | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) ->
447 prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
449 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
450 let a, b = if swap then b,a else a,b in
451 if NCicEnvironment.universe_leq a b then metasenv, subst
452 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
453 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
454 if NCicEnvironment.universe_eq a b then metasenv, subst
455 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
456 | (C.Sort C.Prop,C.Sort (C.Type _)) when not swap ->
457 if (not test_eq_only) then metasenv, subst
458 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
459 | (C.Sort (C.Type _), C.Sort C.Prop) when swap ->
460 if (not test_eq_only) then metasenv, subst
461 else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
463 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
464 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
465 let metasenv, subst = unify status true metasenv subst context s1 s2 swap in
466 unify status test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 swap
467 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
468 let metasenv,subst=unify status test_eq_only metasenv subst context ty1 ty2 swap in
469 let metasenv,subst=unify status test_eq_only metasenv subst context s1 s2 swap in
470 let context = (name1, C.Def (s1,ty1))::context in
471 unify status test_eq_only metasenv subst context t1 t2 swap
473 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
475 let l1 = NCicUtils.expand_local_context l1 in
476 let l2 = NCicUtils.expand_local_context l2 in
477 let metasenv, subst, to_restrict, _ =
479 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
481 let metasenv, subst =
482 unify status (*test_eq_only*) true metasenv subst context
483 (NCicSubstitution.lift status s1 t1) (NCicSubstitution.lift status s2 t2)
486 metasenv, subst, to_restrict, i-1
487 with UnificationFailure _ | Uncertain _ ->
488 metasenv, subst, i::to_restrict, i-1)
489 l1 l2 (metasenv, subst, [], List.length l1)
491 if to_restrict <> [] then
492 let metasenv, subst, _, _ =
493 NCicMetaSubst.restrict status metasenv subst n1 to_restrict
498 | Invalid_argument _ -> assert false
499 | NCicMetaSubst.MetaSubstFailure msg ->
501 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
502 let term1 = NCicSubstitution.subst_meta status lc1 term in
503 let term2 = NCicSubstitution.subst_meta status lc2 term in
504 unify status test_eq_only metasenv subst context term1 term2 swap
505 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
507 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
508 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
511 (fun (metasenv, subst) t1 t2 ->
512 unify status (*test_eq_only*) true metasenv subst context t1
514 (metasenv,subst) l1 l2
515 with Invalid_argument _ ->
516 raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)))
518 | _, NCic.Meta (n, _) when is_locked n subst && not swap && not during_delift ->
519 (let (metasenv, subst), i =
520 match NCicReduction.whd status ~subst context t1 with
521 | NCic.Appl (NCic.Meta (i,l) as meta :: args) ->
522 let metasenv, lambda_Mj =
523 lambda_intros status metasenv subst context (List.length args)
524 (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
526 unify status test_eq_only metasenv subst context
527 (C.Meta (i,l)) lambda_Mj false,
529 | NCic.Meta (i,_) -> (metasenv, subst), i
531 raise (UnificationFailure (lazy "Locked term vs non
532 flexible term; probably not saturated enough yet!"))
534 let t1 = NCicReduction.whd status ~subst context t1 in
536 match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
538 let metasenv, subst =
539 instantiate status test_eq_only metasenv subst context j lj t2 true
541 (* We need to remove the out_scope_tags to avoid propagation of
542 them that triggers again the ad-hoc case *)
544 List.map (fun (i,(tag,ctx,bo,ty)) ->
547 (function `InScope | `OutScope _ -> false | _ -> true) tag
553 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
554 let term = eta_reduce status subst term in
555 let subst = List.filter (fun (j,_) -> j <> i) subst in
556 metasenv, ((i, (name, ctx, term, ty)) :: subst)
557 with Not_found -> assert false))
558 | NCic.Meta (n, _), _ when is_locked n subst && swap ->
559 fo_unif0 during_delift status false test_eq_only metasenv subst context m2 m1
561 | _, C.Meta (n,lc) when List.mem_assoc n subst ->
562 let _,_,term,_ = NCicUtils.lookup_subst n subst in
563 let term = NCicSubstitution.subst_meta status lc term in
564 fo_unif0 during_delift status swap test_eq_only metasenv subst context
566 | C.Meta (n,_), _ when List.mem_assoc n subst ->
567 fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
569 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
570 let _,_,term,_ = NCicUtils.lookup_subst i subst in
571 let term = NCicSubstitution.subst_meta status l term in
572 fo_unif0 during_delift status swap test_eq_only metasenv subst context
573 m1 (false,mk_appl status ~upto:(List.length args) term args)
574 | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
575 fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
577 | C.Meta (n,_), C.Meta (m,lc') when
578 let _,cc1,_ = NCicUtils.lookup_meta n metasenv in
579 let _,cc2,_ = NCicUtils.lookup_meta m metasenv in
580 (n < m && cc1 = cc2) ||
581 let len1 = List.length cc1 in
582 let len2 = List.length cc2 in
583 len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
584 instantiate status test_eq_only metasenv subst context m lc'
585 (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
586 | C.Meta (n,lc), C.Meta (m,lc') when
587 let _,_,tyn = NCicUtils.lookup_meta n metasenv in
588 let _,_,tym = NCicUtils.lookup_meta m metasenv in
589 let tyn = NCicSubstitution.subst_meta status lc tyn in
590 let tym = NCicSubstitution.subst_meta status lc tym in
592 NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
593 NCicEnvironment.universe_lt u1 u2
595 instantiate status test_eq_only metasenv subst context m lc'
596 (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
597 | C.Meta (n,lc), t ->
598 instantiate status test_eq_only metasenv subst context n lc
599 (NCicReduction.head_beta_reduce status ~subst t) swap
600 | t, C.Meta (n,lc) ->
601 instantiate status test_eq_only metasenv subst context n lc
602 (NCicReduction.head_beta_reduce status ~subst t) (not swap)
604 (* higher order unification case *)
605 | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
606 (* this easy_case handles "(? ?) =?= (f a)", same number of
607 * args, preferring the instantiation "f" over "\_.f a" for the
608 * metavariable in head position. Since the arguments of the meta
609 * are flexible, delift would ignore them generating a constant
610 * function even in the easy case above *)
613 | NCic.Appl (f :: f_args)
615 List.exists (NCicMetaSubst.is_flexible status context ~subst) args ->
616 let mlen = List.length args in
617 let flen = List.length f_args in
618 let min_len = min mlen flen in
619 let mhe,margs = HExtlib.split_nth (mlen - min_len) args in
620 let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in
622 Some (List.fold_left2
624 unify status test_eq_only m s context t1 t2 swap
626 ((NCicUntrusted.mk_appl meta mhe)::margs)
627 ((NCicUntrusted.mk_appl f fhe)::fargs))
628 with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
632 (match easy_case with
635 (* This case handles "(?_f ..ti..) =?= t2", abstracting every
636 * non flexible ti (delift skips local context items that are
637 * flexible) from t2 in two steps:
638 * 1) ?_f := \..xi.. .?
639 * 2) ?_f ..ti.. =?= t2 --unif_machines-->
640 ?_f[..ti..] =?= t2 --instantiate-->
641 delift [..ti..] t2 *)
642 let metasenv, lambda_Mj =
643 lambda_intros status metasenv subst context (List.length args)
644 (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
646 let metasenv, subst =
647 unify status test_eq_only metasenv subst context
648 (C.Meta (i,l)) lambda_Mj swap
650 let metasenv, subst =
651 unify status test_eq_only metasenv subst context t1 t2 swap
654 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
655 let term = eta_reduce status subst term in
656 let subst = List.filter (fun (j,_) -> j <> i) subst in
657 metasenv, ((i, (name, ctx, term, ty)) :: subst)
658 with Not_found -> assert false))
660 | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
661 fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
663 | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
665 fo_unif0 during_delift status swap test_eq_only metasenv subst context
666 (false,hd1) (false,hd2) in
669 | C.Const r -> NCicEnvironment.get_relevance status r
671 let metasenv, subst, _ =
674 (fun (metasenv, subst, relevance) t1 t2 ->
676 match relevance with b::tl -> b,tl | _ -> true, [] in
677 let metasenv, subst =
678 try unify status test_eq_only metasenv subst context t1 t2
680 with UnificationFailure _ | Uncertain _ when not b ->
683 metasenv, subst, relevance)
684 (metasenv, subst, relevance) tl1 tl2
686 Invalid_argument _ ->
687 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
688 | KeepReducing _ | KeepReducingThis _ -> assert false
692 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
693 C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
694 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys status ref1 in
695 let _,_,ty,_ = List.nth itl tyno in
696 let rec remove_prods ~subst context ty =
697 let ty = NCicReduction.whd status ~subst context ty in
700 | C.Prod (name,so,ta) ->
701 remove_prods ~subst ((name,(C.Decl so))::context) ta
705 match remove_prods ~subst [] ty with
706 | C.Sort C.Prop -> true
709 (* if not (Ref.eq ref1 ref2) then
710 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
712 let metasenv, subst =
713 unify status test_eq_only metasenv subst context outtype1 outtype2 swap in
714 let metasenv, subst =
715 try unify status test_eq_only metasenv subst context term1 term2 swap
716 with UnificationFailure _ | Uncertain _ when is_prop ->
721 (fun (metasenv,subst) t1 t2 ->
722 unify status test_eq_only metasenv subst context t1 t2 swap)
723 (metasenv, subst) pl1 pl2
724 with Invalid_argument _ -> assert false)
725 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
726 | _ when norm1 && norm2 ->
727 if (could_reduce status ~subst context t1 || could_reduce status ~subst context t2) then
728 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
730 raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
731 | _ -> raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
732 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
734 and try_hints status swap test_eq_only metasenv subst context (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
735 if NCicUntrusted.metas_of_term status subst context t1 = [] &&
736 NCicUntrusted.metas_of_term status subst context t2 = []
739 (*D*) inside 'H'; try let rc =
740 pp(lazy ("\nProblema:\n" ^
741 ppterm status ~metasenv ~subst ~context t1 ^ " =?= " ^
742 ppterm status ~metasenv ~subst ~context t2));
744 NCicUnifHint.look_for_hint status metasenv subst context t1 t2
746 let rec cand_iter = function
747 | [] -> None (* raise exc *)
748 | (metasenv,(c1,c2),premises)::tl ->
749 pp (lazy ("\nProvo il candidato:\n" ^
753 ppterm status ~metasenv ~subst ~context a ^ " =?= " ^
754 ppterm status ~metasenv ~subst ~context b) premises) ^
755 "\n-------------------------------------------\n"^
756 ppterm status ~metasenv ~subst ~context c1 ^ " = " ^
757 ppterm status ~metasenv ~subst ~context c2));
759 (*D*) inside 'K'; try let rc =
761 fo_unif false status swap test_eq_only metasenv subst context mt1 (false,c1) in
763 fo_unif false status swap test_eq_only metasenv subst context (false,c2) mt2 in
766 (fun (metasenv, subst) (x,y) ->
767 unify status test_eq_only metasenv subst context x y false)
768 (metasenv, subst) (List.rev premises)
770 pp(lazy("FUNZIONA!"));
771 Some (metasenv, subst)
772 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
774 KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
775 | KeepReducingThis _ -> assert false
778 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
781 and fo_unif during_delift status swap test_eq_only metasenv subst context (norm1,t1 as nt1) (norm2,t2 as nt2)=
782 try fo_unif0 during_delift status swap test_eq_only metasenv subst context nt1 nt2
784 UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
785 raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
787 and unify status test_eq_only metasenv subst context t1 t2 swap =
788 (*D*) inside 'U'; try let rc =
789 let fo_unif_heads_and_cont_or_unwind_and_hints
790 test_eq_only metasenv subst m1 m2 cont hm1 hm2
792 let ms, continuation =
793 (* calling the continuation inside the outermost try is an option
794 and makes unification stronger, but looks not frequent to me
795 that heads unify but not the arguments and that an hints can fix
797 try fo_unif false status swap test_eq_only metasenv subst context m1 m2, cont
799 | UnificationFailure _
800 | KeepReducing _ | Uncertain _ as exn ->
801 let (t1,norm1),(t2,norm2) = hm1, hm2 in
803 try_hints status swap test_eq_only metasenv subst context
804 (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
806 | Some x -> x, fun x -> x
809 | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
810 | UnificationFailure _ | Uncertain _ as exn -> raise exn
815 let height_of = function
816 | NCic.Const (Ref.Ref (_,Ref.Def h))
817 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
818 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
819 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
822 let small_delta_step ~subst
823 ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
825 assert (not (norm1 && norm2));
827 x1,NCicReduction.reduce_machine status ~delta:0 ~subst context m2
829 NCicReduction.reduce_machine status ~delta:0 ~subst context m1,x2
831 let h1 = height_of t1 in
832 let h2 = height_of t2 in
833 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
834 NCicReduction.reduce_machine status ~delta ~subst context m1,
835 NCicReduction.reduce_machine status ~delta ~subst context m2
837 let rec unif_machines metasenv subst =
839 | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
840 (*D*) inside 'M'; try let rc =
842 ppterm status ~metasenv ~subst ~context
843 (NCicReduction.unwind status (k1,e1,t1,s1)) ^
845 ppterm status ~metasenv ~subst ~context
846 (NCicReduction.unwind status (k2,e2,t2,s2))));
847 pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
850 | C.Const r -> NCicEnvironment.get_relevance status r
852 let unif_from_stack (metasenv, subst) (t1, t2, b) =
854 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
855 let t2 = NCicReduction.from_stack ~delta:max_int t2 in
856 unif_machines metasenv subst (put_in_whd status subst context t1 t2)
857 with UnificationFailure _ | Uncertain _ when not b ->
860 let rec check_stack l1 l2 r todo =
862 | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
863 | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
865 NCicReduction.unwind status (k1,e1,t1,List.rev l1),
866 NCicReduction.unwind status (k2,e2,t2,List.rev l2),
869 let check_stack l1 l2 r =
871 | NCic.Meta _, _ | _, NCic.Meta _ ->
872 (NCicReduction.unwind status (k1,e1,t1,s1)),
873 (NCicReduction.unwind status (k2,e2,t2,s2)),[]
874 | _ -> check_stack l1 l2 r []
877 check_stack (List.rev s1) (List.rev s2) (List.rev relevance) in
879 fo_unif_heads_and_cont_or_unwind_and_hints
880 test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
881 (fun ms -> List.fold_left unif_from_stack ms todo)
884 | KeepReducing _ -> assert false
885 | KeepReducingThis _ ->
886 assert (not (norm1 && norm2));
887 unif_machines metasenv subst (small_delta_step ~subst m1 m2)
888 | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
889 -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
890 | UnificationFailure msg
891 when could_reduce status ~subst context (NCicReduction.unwind status (fst m1))
892 || could_reduce status ~subst context (NCicReduction.unwind status (fst m2))
893 -> raise (Uncertain msg)
894 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
896 try fo_unif_w_hints false status swap test_eq_only metasenv subst context (false,t1) (false,t2)
898 | KeepReducingThis (msg,tm1,tm2) ->
900 unif_machines metasenv subst (tm1,tm2)
902 | UnificationFailure _ -> raise (UnificationFailure msg)
903 | Uncertain _ -> raise (Uncertain msg)
904 | KeepReducing _ -> assert false)
905 | KeepReducing _ -> assert false
907 (*D*) in outside None; rc with KeepReducing _ -> assert false | exn -> outside (Some exn); raise exn
909 and delift_type_wrt_terms status metasenv subst context t args =
910 let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
911 let (metasenv, subst), t =
913 NCicMetaSubst.delift status ~unify:(unify_for_delift status)
914 metasenv subst context (-1) (0,NCic.Ctx lc) t
916 NCicMetaSubst.MetaSubstFailure _
917 | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t
923 let unify status ?(test_eq_only=false) ?(swap=false) metasenv subst context t1 t2=
925 unify status test_eq_only metasenv subst context t1 t2 swap;;
927 let fix_sorts status m s =
928 fix status m s true false (UnificationFailure (lazy "no sup"))