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 rec fo_unif test_eq_only metasenv subst t1 t2 =
251 let try_hints metasenv subst context t1 t2 (* exc*) =
252 let candidates = NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2
254 let rec cand_iter = function
255 | [] -> None (* raise exc *)
256 | (metasenv,c1,c2)::tl ->
258 prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t1);
259 prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context c1);
260 prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t2);
261 prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context c2);
262 let metasenv,subst = fo_unif test_eq_only metasenv subst t1 c1 in
263 let metasenv,subst = fo_unif test_eq_only metasenv subst c2 t2 in
264 Some (fo_unif test_eq_only metasenv subst t1 t2)
266 UnificationFailure _ | Uncertain _ -> cand_iter tl
271 (*D*) inside 'F'; try let rc =
272 pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^
273 NCicPp.ppterm ~metasenv ~subst ~context t2));
277 match (try_hints metasenv subst context t1 t2) with
281 | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
282 if NCicEnvironment.universe_leq a b then metasenv, subst
283 else raise (fail_exc metasenv subst context t1 t2)
284 | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
285 if NCicEnvironment.universe_eq a b then metasenv, subst
286 else raise (fail_exc metasenv subst context t1 t2)
287 | (C.Sort C.Prop,C.Sort (C.Type _)) ->
288 if (not test_eq_only) then metasenv, subst
289 else raise (fail_exc metasenv subst context t1 t2)
291 | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
292 | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
293 let metasenv, subst = unify hdb true metasenv subst context s1 s2 in
294 unify hdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
295 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
296 let metasenv,subst=unify hdb test_eq_only metasenv subst context ty1 ty2 in
297 let metasenv,subst=unify hdb test_eq_only metasenv subst context s1 s2 in
298 let context = (name1, C.Def (s1,ty1))::context in
299 unify hdb test_eq_only metasenv subst context t1 t2
301 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
303 let l1 = NCicUtils.expand_local_context l1 in
304 let l2 = NCicUtils.expand_local_context l2 in
305 let metasenv, subst, to_restrict, _ =
307 (fun t1 t2 (metasenv, subst, to_restrict, i) ->
309 let metasenv, subst =
310 unify hdb test_eq_only metasenv subst context
311 (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
313 metasenv, subst, to_restrict, i-1
314 with UnificationFailure _ | Uncertain _ ->
315 metasenv, subst, i::to_restrict, i-1)
316 l1 l2 (metasenv, subst, [], List.length l1)
318 if to_restrict <> [] then
319 let metasenv, subst, _ =
320 NCicMetaSubst.restrict metasenv subst n1 to_restrict
325 | Invalid_argument _ -> assert false
326 | NCicMetaSubst.MetaSubstFailure msg ->
328 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
329 let term1 = NCicSubstitution.subst_meta lc1 term in
330 let term2 = NCicSubstitution.subst_meta lc2 term in
331 unify hdb test_eq_only metasenv subst context term1 term2
332 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
334 | C.Meta (n,lc), t ->
336 let _,_,term,_ = NCicUtils.lookup_subst n subst in
337 let term = NCicSubstitution.subst_meta lc term in
338 unify hdb test_eq_only metasenv subst context term t
339 with NCicUtils.Subst_not_found _->
340 instantiate hdb test_eq_only metasenv subst context n lc t false)
342 | t, C.Meta (n,lc) ->
344 let _,_,term,_ = NCicUtils.lookup_subst n subst in
345 let term = NCicSubstitution.subst_meta lc term in
346 unify hdb test_eq_only metasenv subst context t term
347 with NCicUtils.Subst_not_found _->
348 instantiate hdb test_eq_only metasenv subst context n lc t true)
350 | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
351 let _,_,term,_ = NCicUtils.lookup_subst i subst in
352 let term = NCicSubstitution.subst_meta l term in
353 unify hdb test_eq_only metasenv subst context (mk_appl term args) t2
355 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
356 let _,_,term,_ = NCicUtils.lookup_subst i subst in
357 let term = NCicSubstitution.subst_meta l term in
358 unify hdb test_eq_only metasenv subst context t1 (mk_appl term args)
360 | NCic.Appl (NCic.Meta (i,_)::_ as l1),
361 NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
364 (fun (metasenv, subst) t1 t2 ->
365 unify hdb test_eq_only metasenv subst context t1 t2)
366 (metasenv,subst) l1 l2
367 with Invalid_argument _ ->
368 raise (fail_exc metasenv subst context t1 t2))
370 | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
371 (* we verify that none of the args is a Meta,
372 since beta expanding w.r.t a metavariable makes no sense *)
373 let metasenv, subst, beta_expanded =
376 metasenv subst context t2 args
378 unify hdb test_eq_only metasenv subst context
379 (C.Meta (i,l)) beta_expanded
381 | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
382 let metasenv, subst, beta_expanded =
385 metasenv subst context t1 args
387 unify hdb test_eq_only metasenv subst context
388 beta_expanded (C.Meta (i,l))
390 (* processing this case here we avoid a useless small delta step *)
391 | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
393 let relevance = NCicEnvironment.get_relevance r1 in
394 let relevance = match r1 with
395 | Ref.Ref (_,Ref.Con (_,_,lno)) ->
396 let _,relevance = HExtlib.split_nth lno relevance in
397 HExtlib.mk_list false lno @ relevance
400 let metasenv, subst, _ =
403 (fun (metasenv, subst, relevance) t1 t2 ->
405 match relevance with b::tl -> b,tl | _ -> true, [] in
406 let metasenv, subst =
407 try unify hdb test_eq_only metasenv subst context t1 t2
408 with UnificationFailure _ | Uncertain _ when not b ->
411 metasenv, subst, relevance)
412 (metasenv, subst, relevance) tl1 tl2
413 with Invalid_argument _ ->
414 raise (uncert_exc metasenv subst context t1 t2)
418 | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
419 C.Match (ref2,outtype2,term2,pl2)) ->
420 let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
421 let _,_,ty,_ = List.nth itl tyno in
422 let rec remove_prods ~subst context ty =
423 let ty = NCicReduction.whd ~subst context ty in
426 | C.Prod (name,so,ta) ->
427 remove_prods ~subst ((name,(C.Decl so))::context) ta
431 match remove_prods ~subst [] ty with
432 | C.Sort C.Prop -> true
435 let rec remove_prods ~subst context ty =
436 let ty = NCicReduction.whd ~subst context ty in
439 | C.Prod (name,so,ta) ->
440 remove_prods ~subst ((name,(C.Decl so))::context) ta
443 if not (Ref.eq ref1 ref2) then
444 raise (uncert_exc metasenv subst context t1 t2)
446 let metasenv, subst =
447 unify hdb test_eq_only metasenv subst context outtype1 outtype2 in
448 let metasenv, subst =
449 try unify hdb test_eq_only metasenv subst context term1 term2
450 with UnificationFailure _ | Uncertain _ when is_prop ->
455 (fun (metasenv,subst) ->
456 unify hdb test_eq_only metasenv subst context)
457 (metasenv, subst) pl1 pl2
458 with Invalid_argument _ ->
459 raise (uncert_exc metasenv subst context t1 t2))
460 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
461 | _ when NCicUntrusted.metas_of_term subst context t1 = [] &&
462 NCicUntrusted.metas_of_term subst context t2 = [] ->
463 raise (fail_exc metasenv subst context t1 t2)
464 | _ -> raise (uncert_exc metasenv subst context t1 t2)
465 (*D*) in outside(); rc with exn -> outside (); raise exn
467 let height_of = function
468 | NCic.Const (Ref.Ref (_,Ref.Def h))
469 | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
470 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
471 | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
474 let put_in_whd m1 m2 =
475 NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
476 NCicReduction.reduce_machine ~delta:max_int ~subst context m2
479 ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
481 assert (not (norm1 && norm2));
483 x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
485 NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
487 let h1 = height_of t1 in
488 let h2 = height_of t2 in
489 let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
490 NCicReduction.reduce_machine ~delta ~subst context m1,
491 NCicReduction.reduce_machine ~delta ~subst context m2
493 let rec unif_machines metasenv subst =
495 | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
496 (*D*) inside 'M'; try let rc =
498 pp (lazy((if are_normal then "*" else " ") ^ " " ^
499 NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
501 NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2)));
503 let relevance = [] (* TO BE UNDERSTOOD
505 | C.Const r -> NCicEnvironment.get_relevance r
507 let unif_from_stack t1 t2 b metasenv subst =
509 let t1 = NCicReduction.from_stack t1 in
510 let t2 = NCicReduction.from_stack t2 in
511 unif_machines metasenv subst (put_in_whd t1 t2)
512 with UnificationFailure _ | Uncertain _ when not b ->
515 let rec check_stack l1 l2 r todo =
517 | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
518 | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
520 NCicReduction.unwind (k1,e1,t1,List.rev l1),
521 NCicReduction.unwind (k2,e2,t2,List.rev l2),
524 let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in
526 let metasenv,subst = fo_unif test_eq_only metasenv subst hh1 hh2 in
528 (fun (metasenv,subst) (x1,x2,r) ->
529 unif_from_stack x1 x2 r metasenv subst
530 ) (metasenv,subst) todo
531 with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
532 unif_machines metasenv subst (small_delta_step m1 m2)
533 (*D*) in outside(); rc with exn -> outside (); raise exn
535 try fo_unif test_eq_only metasenv subst t1 t2
536 with UnificationFailure msg | Uncertain msg as exn ->
538 unif_machines metasenv subst
539 (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
541 | UnificationFailure _ -> raise (UnificationFailure msg)
542 | Uncertain _ -> raise exn
543 (*D*) in outside(); rc with exn -> outside (); raise exn