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));
34 | NCic.Appl l -> NCic.Appl (l@tl)
35 | _ -> NCic.Appl (hd :: tl)
42 | NCic.Appl (NCic.Meta _::_) -> true
46 exception WrongShape;;
49 let delift_if_not_occur body orig =
51 NCicSubstitution.psubst ~avoid_beta_redexes:true
52 (fun () -> raise WrongShape) [()] body
53 with WrongShape -> orig
56 | NCic.Lambda(_, _, NCic.Appl [hd; NCic.Rel 1]) as orig ->
57 delift_if_not_occur hd orig
58 | NCic.Lambda(_, _, NCic.Appl (hd :: l)) as orig
59 when HExtlib.list_last l = NCic.Rel 1 ->
61 let args, _ = HExtlib.split_nth (List.length l - 1) l in
64 delift_if_not_occur body orig
69 module Ref = NReference;;
72 let inside c = indent := !indent ^ String.make 1 c;;
73 let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
77 prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
83 let fix_sorts swap metasenv subst context meta t =
84 let rec aux () = function
85 | NCic.Sort (NCic.Type u) as orig ->
87 match NCicEnvironment.sup u with
88 | None -> prerr_endline "no sup for" ;
89 raise (fail_exc metasenv subst context meta t)
90 | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
92 NCic.Sort (NCic.Type (
93 match NCicEnvironment.sup NCicEnvironment.type0 with
96 | NCic.Meta _ as orig -> orig
97 | t -> NCicUtils.map (fun _ _ -> ()) () aux t
102 let rec beta_expand hdb num test_eq_only swap metasenv subst context t arg =
103 let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
105 let metasenv, subst =
107 unify hdb test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
109 unify hdb test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
111 (metasenv, subst), NCic.Rel (1 + n)
112 with Uncertain _ | UnificationFailure _ ->
114 | NCic.Rel m as orig ->
115 (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
116 (* andrea: in general, beta_expand can create badly typed
117 terms. This happens quite seldom in practice, UNLESS we
118 iterate on the local context. For this reason, we renounce
119 to iterate and just lift *)
120 | NCic.Meta (i,(shift,lc)) ->
121 (metasenv,subst), NCic.Meta (i,(shift+1,lc))
122 | NCic.Prod (name, src, tgt) as orig ->
123 let (metasenv, subst), src1 = aux (n,context,true) acc src in
124 let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
125 let ms, tgt1 = aux k (metasenv, subst) tgt in
126 if src == src1 && tgt == tgt1 then ms, orig else
127 ms, NCic.Prod (name, src1, tgt1)
129 NCicUntrusted.map_term_fold_a
130 (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t
133 let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
134 let fresh_name = "Hbeta" ^ string_of_int num in
135 let (metasenv,subst), t1 =
136 aux (0, context, test_eq_only) (metasenv, subst) t in
137 let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in
139 ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
141 with NCicTypeChecker.TypeCheckerFailure _ ->
142 metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
144 and beta_expand_many hdb test_equality_only swap metasenv subst context t args =
145 (* (*D*) inside 'B'; try let rc = *)
146 pp (lazy (String.concat ", "
147 (List.map (NCicPp.ppterm ~metasenv ~subst ~context)
148 args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
149 let _, subst, metasenv, hd =
151 (fun arg (num,subst,metasenv,t) ->
152 let metasenv, subst, t =
153 beta_expand hdb num test_equality_only swap metasenv subst context t arg
155 num+1,subst,metasenv,t)
156 args (1,subst,metasenv,t)
158 pp (lazy ("Head syntesized by b-exp: " ^
159 NCicPp.ppterm ~metasenv ~subst ~context hd));
161 (* (*D*) in outside (); rc with exn -> outside (); raise exn *)
163 and instantiate hdb test_eq_only metasenv subst context n lc t swap =
164 (*D*) inside 'I'; try let rc =
165 pp (lazy(string_of_int n ^ " :=?= "^
166 NCicPp.ppterm ~metasenv ~subst ~context t));
167 let unify test_eq_only m s c t1 t2 =
168 if swap then unify hdb test_eq_only m s c t2 t1
169 else unify hdb test_eq_only m s c t1 t2
171 let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
172 let metasenv, subst, t =
174 | NCic.Implicit (`Typeof _) ->
176 (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *)
179 "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^
180 NCicPp.ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^
181 NCicPp.ppmetasenv ~subst metasenv));
183 try t, NCicTypeChecker.typeof ~subst ~metasenv context t
185 | NCicTypeChecker.AssertFailure msg ->
186 (pp (lazy "fine typeof (fallimento)");
187 let ft=fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t in
189 (prerr_endline ( ("ILLTYPED: " ^
190 NCicPp.ppterm ~metasenv ~subst ~context t
191 ^ "\nBECAUSE:" ^ Lazy.force msg ^ "\nCONTEXT:\n" ^
192 NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^
193 NCicPp.ppmetasenv ~subst metasenv
198 pp (lazy ("typeof: " ^
199 NCicPp.ppterm ~metasenv ~subst ~context ft));
200 ft, NCicTypeChecker.typeof ~subst ~metasenv context ft
201 with NCicTypeChecker.AssertFailure _ ->
203 | NCicTypeChecker.TypeCheckerFailure msg ->
204 prerr_endline (Lazy.force msg);
207 let lty = NCicSubstitution.subst_meta lc ty in
208 pp (lazy ("On the types: " ^
209 NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
210 NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
211 ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
212 let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
215 pp (lazy(string_of_int n ^ " := 111 = "^
216 NCicPp.ppterm ~metasenv ~subst ~context t));
217 let (metasenv, subst), t =
218 try NCicMetaSubst.delift metasenv subst context n lc t
219 with NCicMetaSubst.Uncertain msg ->
220 pp (lazy ("delift fails: " ^ Lazy.force msg));
221 raise (Uncertain msg)
222 | NCicMetaSubst.MetaSubstFailure msg ->
223 pp (lazy ("delift fails: " ^ Lazy.force msg));
224 raise (UnificationFailure msg)
226 pp (lazy(string_of_int n ^ " := 222 = "^
227 NCicPp.ppterm ~metasenv ~subst ~context:ctx t
228 ^ "\n" ^ NCicPp.ppmetasenv ~subst metasenv));
229 (* Unifying the types may have already instantiated n. *)
231 let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
232 let oldt = NCicSubstitution.subst_meta lc oldt in
233 let t = NCicSubstitution.subst_meta lc t in
234 (* conjecture: always fail --> occur check *)
235 unify test_eq_only metasenv subst context oldt t
236 with NCicUtils.Subst_not_found _ ->
237 (* by cumulativity when unify(?,Type_i)
238 * we could ? := Type_j with j <= i... *)
239 let subst = (n, (name, ctx, t, ty)) :: subst in
240 pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
241 ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
243 List.filter (fun (m,_) -> not (n = m)) metasenv
246 (*D*) in outside(); rc with exn -> outside (); raise exn
248 and unify hdb test_eq_only metasenv subst context t1 t2 =
249 (*D*) inside 'U'; try let rc =
250 let fo_unif test_eq_only metasenv subst t1 t2 =
251 (*D*) inside 'F'; try let rc =
252 pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^
253 NCicPp.ppterm ~metasenv ~subst ~context t2 ^ "\n" ^ NCicPp.ppmetasenv
259 | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl []
260 | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) ->
261 prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
263 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
264 if NCicEnvironment.universe_leq a b then metasenv, subst
265 else raise (fail_exc metasenv subst context t1 t2)
266 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
267 if NCicEnvironment.universe_eq a b then metasenv, subst
268 else raise (fail_exc metasenv subst context t1 t2)
269 | (C.Sort C.Prop,C.Sort (C.Type _)) ->
270 if (not test_eq_only) then metasenv, subst
271 else raise (fail_exc metasenv subst context t1 t2)
273 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
274 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
275 let metasenv, subst = unify hdb true metasenv subst context s1 s2 in
276 unify hdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
277 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
278 let metasenv,subst=unify hdb test_eq_only metasenv subst context ty1 ty2 in
279 let metasenv,subst=unify hdb test_eq_only metasenv subst context s1 s2 in
280 let context = (name1, C.Def (s1,ty1))::context in
281 unify hdb test_eq_only metasenv subst context t1 t2
283 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
285 let l1 = NCicUtils.expand_local_context l1 in
286 let l2 = NCicUtils.expand_local_context l2 in
287 let metasenv, subst, to_restrict, _ =
289 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
291 let metasenv, subst =
292 unify hdb test_eq_only metasenv subst context
293 (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
295 metasenv, subst, to_restrict, i-1
296 with UnificationFailure _ | Uncertain _ ->
297 metasenv, subst, i::to_restrict, i-1)
298 l1 l2 (metasenv, subst, [], List.length l1)
300 if to_restrict <> [] then
301 let metasenv, subst, _ =
302 NCicMetaSubst.restrict metasenv subst n1 to_restrict
307 | Invalid_argument _ -> assert false
308 | NCicMetaSubst.MetaSubstFailure msg ->
310 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
311 let term1 = NCicSubstitution.subst_meta lc1 term in
312 let term2 = NCicSubstitution.subst_meta lc2 term in
313 unify hdb test_eq_only metasenv subst context term1 term2
314 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
316 | C.Meta (n,lc), t ->
318 let _,_,term,_ = NCicUtils.lookup_subst n subst in
319 let term = NCicSubstitution.subst_meta lc term in
320 unify hdb test_eq_only metasenv subst context term t
321 with NCicUtils.Subst_not_found _->
322 instantiate hdb test_eq_only metasenv subst context n lc 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 t true)
332 | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
333 let _,_,term,_ = NCicUtils.lookup_subst i subst in
334 let term = NCicSubstitution.subst_meta l term in
335 unify hdb test_eq_only metasenv subst context (mk_appl term args) t2
337 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
338 let _,_,term,_ = NCicUtils.lookup_subst i subst in
339 let term = NCicSubstitution.subst_meta l term in
340 unify hdb test_eq_only metasenv subst context t1 (mk_appl term args)
342 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
343 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
346 (fun (metasenv, subst) t1 t2 ->
347 unify hdb test_eq_only metasenv subst context t1 t2)
348 (metasenv,subst) l1 l2
349 with Invalid_argument _ ->
350 raise (fail_exc metasenv subst context t1 t2))
352 | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
353 (* we verify that none of the args is a Meta,
354 since beta expanding w.r.t a metavariable makes no sense *)
355 let metasenv, subst, beta_expanded =
358 metasenv subst context t2 args
360 unify hdb test_eq_only metasenv subst context
361 (C.Meta (i,l)) beta_expanded
363 | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
364 let metasenv, subst, beta_expanded =
367 metasenv subst context t1 args
369 unify hdb test_eq_only metasenv subst context
370 beta_expanded (C.Meta (i,l))
372 (* processing this case here we avoid a useless small delta step *)
373 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
375 let relevance = NCicEnvironment.get_relevance r1 in
376 let relevance = match r1 with
377 | Ref.Ref (_,Ref.Con (_,_,lno)) ->
378 let _,relevance = HExtlib.split_nth lno relevance in
379 HExtlib.mk_list false lno @ relevance
382 let metasenv, subst, _ =
385 (fun (metasenv, subst, relevance) t1 t2 ->
387 match relevance with b::tl -> b,tl | _ -> true, [] in
388 let metasenv, subst =
389 try unify hdb test_eq_only metasenv subst context t1 t2
390 with UnificationFailure _ | Uncertain _ when not b ->
393 metasenv, subst, relevance)
394 (metasenv, subst, relevance) tl1 tl2
395 with Invalid_argument _ ->
396 raise (uncert_exc metasenv subst context t1 t2)
400 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
401 C.Match (ref2,outtype2,term2,pl2)) ->
402 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
403 let _,_,ty,_ = List.nth itl tyno in
404 let rec remove_prods ~subst context ty =
405 let ty = NCicReduction.whd ~subst context ty in
408 | C.Prod (name,so,ta) ->
409 remove_prods ~subst ((name,(C.Decl so))::context) ta
413 match remove_prods ~subst [] ty with
414 | C.Sort C.Prop -> true
417 if not (Ref.eq ref1 ref2) then
418 raise (uncert_exc metasenv subst context t1 t2)
420 let metasenv, subst =
421 unify hdb test_eq_only metasenv subst context outtype1 outtype2 in
422 let metasenv, subst =
423 try unify hdb test_eq_only metasenv subst context term1 term2
424 with UnificationFailure _ | Uncertain _ when is_prop ->
429 (fun (metasenv,subst) ->
430 unify hdb test_eq_only metasenv subst context)
431 (metasenv, subst) pl1 pl2
432 with Invalid_argument _ ->
433 raise (uncert_exc metasenv subst context t1 t2))
434 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
435 | _ when NCicUntrusted.metas_of_term subst context t1 = [] &&
436 NCicUntrusted.metas_of_term subst context t2 = [] ->
437 raise (fail_exc metasenv subst context t1 t2)
438 | _ -> raise (uncert_exc metasenv subst context t1 t2)
439 (*D*) in outside(); rc with exn -> outside (); raise exn
441 let try_hints metasenv subst t1 t2 (* exc*) =
443 NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2
445 let rec cand_iter = function
446 | [] -> None (* raise exc *)
447 | (metasenv,c1,c2)::tl ->
449 let metasenv,subst = fo_unif test_eq_only metasenv subst t1 c1 in
450 let metasenv,subst = fo_unif test_eq_only metasenv subst c2 t2 in
451 Some (metasenv, subst)
453 UnificationFailure _ | Uncertain _ -> cand_iter tl
457 let height_of = function
458 | NCic.Const (Ref.Ref (_,Ref.Def h))
459 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
460 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
461 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
464 let put_in_whd m1 m2 =
465 NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
466 NCicReduction.reduce_machine ~delta:max_int ~subst context m2
468 let small_delta_step ~subst
469 ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
471 assert (not (norm1 && norm2));
473 x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
475 NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
477 let h1 = height_of t1 in
478 let h2 = height_of t2 in
479 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
480 NCicReduction.reduce_machine ~delta ~subst context m1,
481 NCicReduction.reduce_machine ~delta ~subst context m2
483 let rec unif_machines metasenv subst =
485 | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
486 (*D*) inside 'M'; try let rc =
488 NCicPp.ppterm ~metasenv ~subst ~context
489 (NCicReduction.unwind (k1,e1,t1,s1)) ^
491 NCicPp.ppterm ~metasenv ~subst ~context
492 (NCicReduction.unwind (k2,e2,t2,s2))));
493 pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
494 let relevance = [] (* TO BE UNDERSTOOD
496 | C.Const r -> NCicEnvironment.get_relevance r
498 let unif_from_stack t1 t2 b metasenv subst =
500 let t1 = NCicReduction.from_stack t1 in
501 let t2 = NCicReduction.from_stack t2 in
502 unif_machines metasenv subst (put_in_whd t1 t2)
503 with UnificationFailure _ | Uncertain _ when not b ->
506 let rec check_stack l1 l2 r todo =
508 | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
509 | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
511 NCicReduction.unwind (k1,e1,t1,List.rev l1),
512 NCicReduction.unwind (k2,e2,t2,List.rev l2),
515 let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in
517 let metasenv,subst = fo_unif test_eq_only metasenv subst hh1 hh2 in
519 (fun (metasenv,subst) (x1,x2,r) ->
520 unif_from_stack x1 x2 r metasenv subst
521 ) (metasenv,subst) todo
522 with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
523 unif_machines metasenv subst (small_delta_step ~subst m1 m2)
524 (*D*) in outside(); rc with exn -> outside (); raise exn
526 try fo_unif test_eq_only metasenv subst t1 t2
527 with UnificationFailure msg | Uncertain msg as exn ->
528 match try_hints metasenv subst t1 t2 with
532 unif_machines metasenv subst
533 (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
535 | UnificationFailure _ -> raise (UnificationFailure msg)
536 | Uncertain _ -> raise exn
537 (*D*) in outside(); rc with exn -> outside (); raise exn