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;;
18 let (===) x y = Pervasives.compare x y = 0 ;;
20 let uncert_exc metasenv subst context t1 t2 =
22 "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
23 " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
26 let fail_exc metasenv subst context t1 t2 =
27 UnificationFailure (lazy (
28 "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
29 " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2));
32 let mk_appl ~upto hd tl =
33 NCicReduction.head_beta_reduce ~upto
35 | NCic.Appl l -> NCic.Appl (l@tl)
36 | _ -> NCic.Appl (hd :: tl))
43 | NCic.Appl (NCic.Meta _::_) -> true
47 exception WrongShape;;
50 let delift_if_not_occur body orig =
52 NCicSubstitution.psubst ~avoid_beta_redexes:true
53 (fun () -> raise WrongShape) [()] body
54 with WrongShape -> orig
57 | NCic.Lambda(_, _, NCic.Appl [hd; NCic.Rel 1]) as orig ->
58 delift_if_not_occur hd orig
59 | NCic.Lambda(_, _, NCic.Appl (hd :: l)) as orig
60 when HExtlib.list_last l = NCic.Rel 1 ->
62 let args, _ = HExtlib.split_nth (List.length l - 1) l in
65 delift_if_not_occur body orig
70 module Ref = NReference;;
73 let inside c = indent := !indent ^ String.make 1 c;;
74 let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
77 prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
82 let fix_sorts swap metasenv subst context meta t =
83 let rec aux () = function
84 | NCic.Sort (NCic.Type u) as orig ->
86 match NCicEnvironment.sup u with
87 | None -> prerr_endline "no sup for" ;
88 raise (fail_exc metasenv subst context meta t)
89 | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
91 NCic.Sort (NCic.Type (
92 match NCicEnvironment.sup NCicEnvironment.type0 with
95 | NCic.Meta _ as orig -> orig
96 | t -> NCicUtils.map (fun _ _ -> ()) () aux t
101 let rec beta_expand hdb num test_eq_only swap metasenv subst context t arg =
102 let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
104 let metasenv, subst =
106 unify hdb test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
108 unify hdb test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
110 (metasenv, subst), NCic.Rel (1 + n)
111 with Uncertain _ | UnificationFailure _ ->
113 | NCic.Rel m as orig ->
114 (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
115 (* andrea: in general, beta_expand can create badly typed
116 terms. This happens quite seldom in practice, UNLESS we
117 iterate on the local context. For this reason, we renounce
118 to iterate and just lift *)
119 | NCic.Meta (i,(shift,lc)) ->
120 (metasenv,subst), NCic.Meta (i,(shift+1,lc))
121 | NCic.Prod (name, src, tgt) as orig ->
122 let (metasenv, subst), src1 = aux (n,context,true) acc src in
123 let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
124 let ms, tgt1 = aux k (metasenv, subst) tgt in
125 if src == src1 && tgt == tgt1 then ms, orig else
126 ms, NCic.Prod (name, src1, tgt1)
128 NCicUntrusted.map_term_fold_a
129 (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t
132 let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
133 let fresh_name = "Hbeta" ^ string_of_int num in
134 let (metasenv,subst), t1 =
135 aux (0, context, test_eq_only) (metasenv, subst) t in
136 let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in
138 ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
140 with NCicTypeChecker.TypeCheckerFailure _ ->
141 metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
143 and beta_expand_many hdb test_equality_only swap metasenv subst context t args =
144 (* (*D*) inside 'B'; try let rc = *)
145 pp (lazy (String.concat ", "
146 (List.map (NCicPp.ppterm ~metasenv ~subst ~context)
147 args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
148 let _, subst, metasenv, hd =
150 (fun arg (num,subst,metasenv,t) ->
151 let metasenv, subst, t =
152 beta_expand hdb num test_equality_only swap metasenv subst context t arg
154 num+1,subst,metasenv,t)
155 args (1,subst,metasenv,t)
157 pp (lazy ("Head syntesized by b-exp: " ^
158 NCicPp.ppterm ~metasenv ~subst ~context hd));
160 (* (*D*) in outside (); rc with exn -> outside (); raise exn *)
162 and instantiate hdb test_eq_only metasenv subst context n lc t swap =
163 (*D*) inside 'I'; try let rc =
164 pp (lazy(string_of_int n ^ " :=?= "^
165 NCicPp.ppterm ~metasenv ~subst ~context t));
166 let unify test_eq_only m s c t1 t2 =
167 if swap then unify hdb test_eq_only m s c t2 t1
168 else unify hdb test_eq_only m s c t1 t2
170 let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
171 let metasenv, subst, t =
173 | NCic.Implicit (`Typeof _) ->
175 (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *)
178 "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^
179 NCicPp.ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^
180 NCicPp.ppmetasenv ~subst metasenv));
182 try t, NCicTypeChecker.typeof ~subst ~metasenv context t
184 | NCicTypeChecker.AssertFailure msg ->
185 (pp (lazy "fine typeof (fallimento)");
186 let ft=fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t in
188 (prerr_endline ( ("ILLTYPED: " ^
189 NCicPp.ppterm ~metasenv ~subst ~context t
190 ^ "\nBECAUSE:" ^ Lazy.force msg ^ "\nCONTEXT:\n" ^
191 NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^
192 NCicPp.ppmetasenv ~subst metasenv
197 pp (lazy ("typeof: " ^
198 NCicPp.ppterm ~metasenv ~subst ~context ft));
199 ft, NCicTypeChecker.typeof ~subst ~metasenv context ft
200 with NCicTypeChecker.AssertFailure _ ->
202 | NCicTypeChecker.TypeCheckerFailure msg ->
203 prerr_endline (Lazy.force msg);
206 let lty = NCicSubstitution.subst_meta lc ty in
207 pp (lazy ("On the types: " ^
208 NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
209 NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
210 ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
211 let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
214 pp (lazy(string_of_int n ^ " := 111 = "^
215 NCicPp.ppterm ~metasenv ~subst ~context t));
216 let (metasenv, subst), t =
217 try NCicMetaSubst.delift metasenv subst context n lc t
218 with NCicMetaSubst.Uncertain msg ->
219 pp (lazy ("delift fails: " ^ Lazy.force msg));
220 raise (Uncertain msg)
221 | NCicMetaSubst.MetaSubstFailure msg ->
222 pp (lazy ("delift fails: " ^ Lazy.force msg));
223 raise (UnificationFailure msg)
225 pp (lazy(string_of_int n ^ " := 222 = "^
226 NCicPp.ppterm ~metasenv ~subst ~context:ctx t
227 ^ "\n" ^ NCicPp.ppmetasenv ~subst metasenv));
228 (* Unifying the types may have already instantiated n. *)
230 let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
231 let oldt = NCicSubstitution.subst_meta lc oldt in
232 let t = NCicSubstitution.subst_meta lc t in
233 (* conjecture: always fail --> occur check *)
234 unify test_eq_only metasenv subst context oldt t
235 with NCicUtils.Subst_not_found _ ->
236 (* by cumulativity when unify(?,Type_i)
237 * we could ? := Type_j with j <= i... *)
238 let subst = (n, (name, ctx, t, ty)) :: subst in
239 pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
240 ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
242 List.filter (fun (m,_) -> not (n = m)) metasenv
245 (*D*) in outside(); rc with exn -> outside (); raise exn
247 and unify hdb test_eq_only metasenv subst context t1 t2 =
248 (*D*) inside 'U'; try let rc =
249 let fo_unif test_eq_only metasenv subst t1 t2 =
250 (*D*) inside 'F'; try let rc =
251 pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
252 NCicPp.ppterm ~metasenv ~subst ~context t2 ^ "\n" ^ NCicPp.ppmetasenv
258 | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl []
259 | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) ->
260 prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
262 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
263 if NCicEnvironment.universe_leq a b then metasenv, subst
264 else raise (fail_exc metasenv subst context t1 t2)
265 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
266 if NCicEnvironment.universe_eq a b then metasenv, subst
267 else raise (fail_exc metasenv subst context t1 t2)
268 | (C.Sort C.Prop,C.Sort (C.Type _)) ->
269 if (not test_eq_only) then metasenv, subst
270 else raise (fail_exc metasenv subst context t1 t2)
272 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
273 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
274 let metasenv, subst = unify hdb true metasenv subst context s1 s2 in
275 unify hdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
276 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
277 let metasenv,subst=unify hdb test_eq_only metasenv subst context ty1 ty2 in
278 let metasenv,subst=unify hdb test_eq_only metasenv subst context s1 s2 in
279 let context = (name1, C.Def (s1,ty1))::context in
280 unify hdb test_eq_only metasenv subst context t1 t2
282 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
284 let l1 = NCicUtils.expand_local_context l1 in
285 let l2 = NCicUtils.expand_local_context l2 in
286 let metasenv, subst, to_restrict, _ =
288 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
290 let metasenv, subst =
291 unify hdb test_eq_only metasenv subst context
292 (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
294 metasenv, subst, to_restrict, i-1
295 with UnificationFailure _ | Uncertain _ ->
296 metasenv, subst, i::to_restrict, i-1)
297 l1 l2 (metasenv, subst, [], List.length l1)
299 if to_restrict <> [] then
300 let metasenv, subst, _ =
301 NCicMetaSubst.restrict metasenv subst n1 to_restrict
306 | Invalid_argument _ -> assert false
307 | NCicMetaSubst.MetaSubstFailure msg ->
309 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
310 let term1 = NCicSubstitution.subst_meta lc1 term in
311 let term2 = NCicSubstitution.subst_meta lc2 term in
312 unify hdb test_eq_only metasenv subst context term1 term2
313 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
315 | C.Meta (n,lc), t ->
317 let _,_,term,_ = NCicUtils.lookup_subst n subst in
318 let term = NCicSubstitution.subst_meta lc term in
319 unify hdb test_eq_only metasenv subst context term t
320 with NCicUtils.Subst_not_found _->
321 instantiate hdb test_eq_only metasenv subst context n lc
322 (NCicReduction.head_beta_reduce ~subst t) false)
324 | t, C.Meta (n,lc) ->
326 let _,_,term,_ = NCicUtils.lookup_subst n subst in
327 let term = NCicSubstitution.subst_meta lc term in
328 unify hdb test_eq_only metasenv subst context t term
329 with NCicUtils.Subst_not_found _->
330 instantiate hdb test_eq_only metasenv subst context n lc
331 (NCicReduction.head_beta_reduce ~subst t) true)
333 | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
334 let _,_,term,_ = NCicUtils.lookup_subst i subst in
335 let term = NCicSubstitution.subst_meta l term in
336 unify hdb test_eq_only metasenv subst context
337 (mk_appl ~upto:(List.length args) term args) t2
339 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
340 let _,_,term,_ = NCicUtils.lookup_subst i subst in
341 let term = NCicSubstitution.subst_meta l term in
342 unify hdb test_eq_only metasenv subst context t1
343 (mk_appl ~upto:(List.length args) term args)
345 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
346 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
349 (fun (metasenv, subst) t1 t2 ->
350 unify hdb test_eq_only metasenv subst context t1 t2)
351 (metasenv,subst) l1 l2
352 with Invalid_argument _ ->
353 raise (fail_exc metasenv subst context t1 t2))
355 | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
356 (* we verify that none of the args is a Meta,
357 since beta expanding w.r.t a metavariable makes no sense *)
358 let metasenv, subst, beta_expanded =
361 metasenv subst context t2 args
363 unify hdb test_eq_only metasenv subst context
364 (C.Meta (i,l)) beta_expanded
366 | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
367 let metasenv, subst, beta_expanded =
370 metasenv subst context t1 args
372 unify hdb test_eq_only metasenv subst context
373 beta_expanded (C.Meta (i,l))
375 (* processing this case here we avoid a useless small delta step *)
376 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
378 let relevance = NCicEnvironment.get_relevance r1 in
379 let relevance = match r1 with
380 | Ref.Ref (_,Ref.Con (_,_,lno)) ->
381 let _,relevance = HExtlib.split_nth lno relevance in
382 HExtlib.mk_list false lno @ relevance
385 let metasenv, subst, _ =
388 (fun (metasenv, subst, relevance) t1 t2 ->
390 match relevance with b::tl -> b,tl | _ -> true, [] in
391 let metasenv, subst =
392 try unify hdb test_eq_only metasenv subst context t1 t2
393 with UnificationFailure _ | Uncertain _ when not b ->
396 metasenv, subst, relevance)
397 (metasenv, subst, relevance) tl1 tl2
398 with Invalid_argument _ ->
399 raise (uncert_exc metasenv subst context t1 t2)
403 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
404 C.Match (ref2,outtype2,term2,pl2)) ->
405 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
406 let _,_,ty,_ = List.nth itl tyno in
407 let rec remove_prods ~subst context ty =
408 let ty = NCicReduction.whd ~subst context ty in
411 | C.Prod (name,so,ta) ->
412 remove_prods ~subst ((name,(C.Decl so))::context) ta
416 match remove_prods ~subst [] ty with
417 | C.Sort C.Prop -> true
420 if not (Ref.eq ref1 ref2) then
421 raise (uncert_exc metasenv subst context t1 t2)
423 let metasenv, subst =
424 unify hdb test_eq_only metasenv subst context outtype1 outtype2 in
425 let metasenv, subst =
426 try unify hdb test_eq_only metasenv subst context term1 term2
427 with UnificationFailure _ | Uncertain _ when is_prop ->
432 (fun (metasenv,subst) ->
433 unify hdb test_eq_only metasenv subst context)
434 (metasenv, subst) pl1 pl2
435 with Invalid_argument _ ->
436 raise (uncert_exc metasenv subst context t1 t2))
437 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
438 | _ when NCicUntrusted.metas_of_term subst context t1 = [] &&
439 NCicUntrusted.metas_of_term subst context t2 = [] ->
440 raise (fail_exc metasenv subst context t1 t2)
441 | _ -> raise (uncert_exc metasenv subst context t1 t2)
442 (*D*) in outside(); rc with exn -> outside (); raise exn
444 let try_hints metasenv subst t1 t2 (* exc*) =
446 prerr_endline ("\n\n\n looking for hints for : " ^
447 NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
448 NCicPp.ppterm ~metasenv ~subst ~context t2);
451 NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2
453 let rec cand_iter = function
454 | [] -> None (* raise exc *)
455 | (metasenv,c1,c2)::tl ->
457 prerr_endline ("\n attempt: " ^
458 NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
459 NCicPp.ppterm ~metasenv ~subst ~context c1 ^ " AND " ^
460 NCicPp.ppterm ~metasenv ~subst ~context c2 ^ " ==?== " ^
461 NCicPp.ppterm ~metasenv ~subst ~context t2);
464 let metasenv,subst = unify hdb test_eq_only metasenv subst context t1 c1 in
465 let metasenv,subst = unify hdb test_eq_only metasenv subst context c2 t2 in
466 Some (metasenv, subst)
468 UnificationFailure _ | Uncertain _ ->
469 prerr_endline (" <candidate fails");
474 let height_of = function
475 | NCic.Const (Ref.Ref (_,Ref.Def h))
476 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
477 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
478 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
481 let put_in_whd m1 m2 =
482 NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
483 NCicReduction.reduce_machine ~delta:max_int ~subst context m2
485 let small_delta_step ~subst
486 ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
488 assert (not (norm1 && norm2));
490 x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
492 NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
494 let h1 = height_of t1 in
495 let h2 = height_of t2 in
496 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
497 NCicReduction.reduce_machine ~delta ~subst context m1,
498 NCicReduction.reduce_machine ~delta ~subst context m2
500 let rec unif_machines metasenv subst =
502 | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
503 (*D*) inside 'M'; try let rc =
505 NCicPp.ppterm ~metasenv ~subst ~context
506 (NCicReduction.unwind (k1,e1,t1,s1)) ^
508 NCicPp.ppterm ~metasenv ~subst ~context
509 (NCicReduction.unwind (k2,e2,t2,s2))));
510 pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
511 let relevance = [] (* TO BE UNDERSTOOD
513 | C.Const r -> NCicEnvironment.get_relevance r
515 let unif_from_stack t1 t2 b metasenv subst =
517 let t1 = NCicReduction.from_stack t1 in
518 let t2 = NCicReduction.from_stack t2 in
519 unif_machines metasenv subst (put_in_whd t1 t2)
520 with UnificationFailure _ | Uncertain _ when not b ->
523 let rec check_stack l1 l2 r todo =
525 | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
526 | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
528 NCicReduction.unwind (k1,e1,t1,List.rev l1),
529 NCicReduction.unwind (k2,e2,t2,List.rev l2),
532 let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in
534 let metasenv,subst = fo_unif test_eq_only metasenv subst hh1 hh2 in
536 (fun (metasenv,subst) (x1,x2,r) ->
537 unif_from_stack x1 x2 r metasenv subst
538 ) (metasenv,subst) todo
539 with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
540 unif_machines metasenv subst (small_delta_step ~subst m1 m2)
541 (*D*) in outside(); rc with exn -> outside (); raise exn
543 try fo_unif test_eq_only metasenv subst t1 t2
545 | UnificationFailure msg as exn ->
547 unif_machines metasenv subst
548 (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
550 | UnificationFailure _ -> raise (UnificationFailure msg)
551 | Uncertain _ -> raise exn)
552 | Uncertain msg as exn ->
553 match try_hints metasenv subst t1 t2 with
557 unif_machines metasenv subst
558 (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
560 | UnificationFailure _ -> raise (UnificationFailure msg)
561 | Uncertain _ -> raise exn
562 (*D*) in outside(); rc with exn -> outside (); raise exn