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 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 test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
109 unify 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 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 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 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 test_eq_only m s c t2 t1
169 else unify 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 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));
258 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
259 if NCicEnvironment.universe_leq a b then metasenv, subst
260 else raise (fail_exc metasenv subst context t1 t2)
261 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
262 if NCicEnvironment.universe_eq a b then metasenv, subst
263 else raise (fail_exc metasenv subst context t1 t2)
264 | (C.Sort C.Prop,C.Sort (C.Type _)) ->
265 if (not test_eq_only) then metasenv, subst
266 else raise (fail_exc metasenv subst context t1 t2)
268 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
269 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
270 let metasenv, subst = unify true metasenv subst context s1 s2 in
271 unify test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
272 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
273 let metasenv,subst=unify test_eq_only metasenv subst context ty1 ty2 in
274 let metasenv,subst=unify test_eq_only metasenv subst context s1 s2 in
275 let context = (name1, C.Def (s1,ty1))::context in
276 unify test_eq_only metasenv subst context t1 t2
278 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
280 let l1 = NCicUtils.expand_local_context l1 in
281 let l2 = NCicUtils.expand_local_context l2 in
282 let metasenv, subst, to_restrict, _ =
284 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
286 let metasenv, subst =
287 unify test_eq_only metasenv subst context
288 (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
290 metasenv, subst, to_restrict, i-1
291 with UnificationFailure _ | Uncertain _ ->
292 metasenv, subst, i::to_restrict, i-1)
293 l1 l2 (metasenv, subst, [], List.length l1)
295 if to_restrict <> [] then
296 let metasenv, subst, _ =
297 NCicMetaSubst.restrict metasenv subst n1 to_restrict
302 | Invalid_argument _ -> assert false
303 | NCicMetaSubst.MetaSubstFailure msg ->
305 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
306 let term1 = NCicSubstitution.subst_meta lc1 term in
307 let term2 = NCicSubstitution.subst_meta lc2 term in
308 unify test_eq_only metasenv subst context term1 term2
309 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
311 | C.Meta (n,lc), t ->
313 let _,_,term,_ = NCicUtils.lookup_subst n subst in
314 let term = NCicSubstitution.subst_meta lc term in
315 unify test_eq_only metasenv subst context term t
316 with NCicUtils.Subst_not_found _->
317 instantiate test_eq_only metasenv subst context n lc t false)
319 | t, C.Meta (n,lc) ->
321 let _,_,term,_ = NCicUtils.lookup_subst n subst in
322 let term = NCicSubstitution.subst_meta lc term in
323 unify test_eq_only metasenv subst context t term
324 with NCicUtils.Subst_not_found _->
325 instantiate test_eq_only metasenv subst context n lc t true)
327 | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
328 let _,_,term,_ = NCicUtils.lookup_subst i subst in
329 let term = NCicSubstitution.subst_meta l term in
330 unify test_eq_only metasenv subst context (mk_appl term args) t2
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 test_eq_only metasenv subst context t1 (mk_appl term args)
337 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
338 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
341 (fun (metasenv, subst) t1 t2 ->
342 unify test_eq_only metasenv subst context t1 t2)
343 (metasenv,subst) l1 l2
344 with Invalid_argument _ ->
345 raise (fail_exc metasenv subst context t1 t2))
347 | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
348 (* we verify that none of the args is a Meta,
349 since beta expanding w.r.t a metavariable makes no sense *)
350 let metasenv, subst, beta_expanded =
353 metasenv subst context t2 args
355 unify test_eq_only metasenv subst context
356 (C.Meta (i,l)) beta_expanded
358 | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
359 let metasenv, subst, beta_expanded =
362 metasenv subst context t1 args
364 unify test_eq_only metasenv subst context
365 beta_expanded (C.Meta (i,l))
367 (* processing this case here we avoid a useless small delta step *)
368 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
370 let relevance = NCicEnvironment.get_relevance r1 in
371 let relevance = match r1 with
372 | Ref.Ref (_,Ref.Con (_,_,lno)) ->
373 let _,relevance = HExtlib.split_nth lno relevance in
374 HExtlib.mk_list false lno @ relevance
377 let metasenv, subst, _ =
380 (fun (metasenv, subst, relevance) t1 t2 ->
382 match relevance with b::tl -> b,tl | _ -> true, [] in
383 let metasenv, subst =
384 try unify test_eq_only metasenv subst context t1 t2
385 with UnificationFailure _ | Uncertain _ when not b ->
388 metasenv, subst, relevance)
389 (metasenv, subst, relevance) tl1 tl2
390 with Invalid_argument _ ->
391 raise (uncert_exc metasenv subst context t1 t2)
395 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
396 C.Match (ref2,outtype2,term2,pl2)) ->
397 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
398 let _,_,ty,_ = List.nth itl tyno in
399 let rec remove_prods ~subst context ty =
400 let ty = NCicReduction.whd ~subst context ty in
403 | C.Prod (name,so,ta) ->
404 remove_prods ~subst ((name,(C.Decl so))::context) ta
408 match remove_prods ~subst [] ty with
409 | C.Sort C.Prop -> true
412 let rec remove_prods ~subst context ty =
413 let ty = NCicReduction.whd ~subst context ty in
416 | C.Prod (name,so,ta) ->
417 remove_prods ~subst ((name,(C.Decl so))::context) ta
420 if not (Ref.eq ref1 ref2) then
421 raise (uncert_exc metasenv subst context t1 t2)
423 let metasenv, subst =
424 unify test_eq_only metasenv subst context outtype1 outtype2 in
425 let metasenv, subst =
426 try unify test_eq_only metasenv subst context term1 term2
427 with UnificationFailure _ | Uncertain _ when is_prop ->
432 (fun (metasenv,subst) ->
433 unify 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 height_of = function
445 | NCic.Const (Ref.Ref (_,Ref.Def h))
446 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
447 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
448 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
451 let put_in_whd m1 m2 =
452 NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
453 NCicReduction.reduce_machine ~delta:max_int ~subst context m2
456 ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
458 assert (not (norm1 && norm2));
460 x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
462 NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
464 let h1 = height_of t1 in
465 let h2 = height_of t2 in
466 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
467 NCicReduction.reduce_machine ~delta ~subst context m1,
468 NCicReduction.reduce_machine ~delta ~subst context m2
470 let rec unif_machines metasenv subst =
472 | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
473 (*D*) inside 'M'; try let rc =
475 pp (lazy((if are_normal then "*" else " ") ^ " " ^
476 NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
478 NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2)));
480 let relevance = [] (* TO BE UNDERSTOOD
482 | C.Const r -> NCicEnvironment.get_relevance r
484 let unif_from_stack t1 t2 b metasenv subst =
486 let t1 = NCicReduction.from_stack t1 in
487 let t2 = NCicReduction.from_stack t2 in
488 unif_machines metasenv subst (put_in_whd t1 t2)
489 with UnificationFailure _ | Uncertain _ when not b ->
492 let rec check_stack l1 l2 r todo =
494 | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
495 | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
497 NCicReduction.unwind (k1,e1,t1,List.rev l1),
498 NCicReduction.unwind (k2,e2,t2,List.rev l2),
501 let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in
503 let metasenv,subst = fo_unif test_eq_only metasenv subst hh1 hh2 in
505 (fun (metasenv,subst) (x1,x2,r) ->
506 unif_from_stack x1 x2 r metasenv subst
507 ) (metasenv,subst) todo
508 with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
509 unif_machines metasenv subst (small_delta_step m1 m2)
510 (*D*) in outside(); rc with exn -> outside (); raise exn
512 try fo_unif test_eq_only metasenv subst t1 t2
513 with UnificationFailure msg | Uncertain msg as exn ->
515 unif_machines metasenv subst
516 (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
518 | UnificationFailure _ -> raise (UnificationFailure msg)
519 | Uncertain _ -> raise exn
520 (*D*) in outside(); rc with exn -> outside (); raise exn