1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 exception UnificationFailure of string;;
29 exception Uncertain of string;;
30 exception AssertFailure of string;;
32 let debug_print = prerr_endline
34 let type_of_aux' metasenv subst context term =
36 CicTypeChecker.type_of_aux' ~subst metasenv context term
38 CicTypeChecker.TypeCheckerFailure msg ->
41 "Kernel Type checking error:
42 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
43 (CicMetaSubst.ppterm subst term)
44 (CicMetaSubst.ppterm [] term)
45 (CicMetaSubst.ppcontext subst context)
46 (CicMetaSubst.ppmetasenv metasenv subst)
47 (CicMetaSubst.ppsubst subst) msg) in
48 raise (AssertFailure msg);;
51 CicMetaSubst.type_of_aux' metasenv subst context term
53 | CicMetaSubst.MetaSubstFailure msg ->
56 "Type checking error: %s in context\n%s\nand metasenv\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
57 (CicMetaSubst.ppterm subst term)
58 (CicMetaSubst.ppcontext subst context)
59 (CicMetaSubst.ppmetasenv metasenv subst) msg))) *)
62 let snd (_,a,_) = a in
67 (CicSubstitution.lift_meta
68 l (snd (CicUtil.lookup_subst n subst)))
70 CicUtil.Subst_not_found _ -> t)
74 let rec beta_expand test_equality_only metasenv subst context t arg =
75 let module S = CicSubstitution in
77 let rec aux metasenv subst n context t' =
80 fo_unif_subst test_equality_only subst context metasenv
81 (CicSubstitution.lift n arg) t'
83 subst,metasenv,C.Rel (1 + n)
86 | UnificationFailure _ ->
88 | C.Rel m -> subst,metasenv, if m <= n then C.Rel m else C.Rel (m+1)
89 | C.Var (uri,exp_named_subst) ->
90 let subst,metasenv,exp_named_subst' =
91 aux_exp_named_subst metasenv subst n context exp_named_subst
93 subst,metasenv,C.Var (uri,exp_named_subst')
95 (* andrea: in general, beta_expand can create badly typed
96 terms. This happens quite seldom in practice, UNLESS we
97 iterate on the local context. For this reason, we renounce
98 to iterate and just lift *)
102 Some t -> Some (CicSubstitution.lift 1 t)
104 subst, metasenv, C.Meta (i,l)
106 let (subst, metasenv, context, local_context) =
108 (fun t (subst, metasenv, context, local_context) ->
110 | None -> (subst, metasenv, context, None :: local_context)
112 let (subst, metasenv, t) =
113 aux metasenv subst n context t
115 (subst, metasenv, context, Some t :: local_context))
116 l (subst, metasenv, context, [])
118 prerr_endline ("nuova meta :" ^ (CicPp.ppterm (C.Meta (i, local_context))));
119 (subst, metasenv, C.Meta (i, local_context)) *)
121 | C.Implicit _ as t -> subst,metasenv,t
123 let subst,metasenv,te' = aux metasenv subst n context te in
124 let subst,metasenv,ty' = aux metasenv subst n context ty in
125 subst,metasenv,C.Cast (te', ty')
127 let subst,metasenv,s' = aux metasenv subst n context s in
128 let subst,metasenv,t' =
129 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
131 subst,metasenv,C.Prod (nn, s', t')
132 | C.Lambda (nn,s,t) ->
133 let subst,metasenv,s' = aux metasenv subst n context s in
134 let subst,metasenv,t' =
135 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
137 subst,metasenv,C.Lambda (nn, s', t')
138 | C.LetIn (nn,s,t) ->
139 let subst,metasenv,s' = aux metasenv subst n context s in
140 let subst,metasenv,t' =
141 aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
143 subst,metasenv,C.LetIn (nn, s', t')
145 let subst,metasenv,revl' =
147 (fun (subst,metasenv,appl) t ->
148 let subst,metasenv,t' = aux metasenv subst n context t in
149 subst,metasenv,t'::appl
150 ) (subst,metasenv,[]) l
152 subst,metasenv,C.Appl (List.rev revl')
153 | C.Const (uri,exp_named_subst) ->
154 let subst,metasenv,exp_named_subst' =
155 aux_exp_named_subst metasenv subst n context exp_named_subst
157 subst,metasenv,C.Const (uri,exp_named_subst')
158 | C.MutInd (uri,i,exp_named_subst) ->
159 let subst,metasenv,exp_named_subst' =
160 aux_exp_named_subst metasenv subst n context exp_named_subst
162 subst,metasenv,C.MutInd (uri,i,exp_named_subst')
163 | C.MutConstruct (uri,i,j,exp_named_subst) ->
164 let subst,metasenv,exp_named_subst' =
165 aux_exp_named_subst metasenv subst n context exp_named_subst
167 subst,metasenv,C.MutConstruct (uri,i,j,exp_named_subst')
168 | C.MutCase (sp,i,outt,t,pl) ->
169 let subst,metasenv,outt' = aux metasenv subst n context outt in
170 let subst,metasenv,t' = aux metasenv subst n context t in
171 let subst,metasenv,revpl' =
173 (fun (subst,metasenv,pl) t ->
174 let subst,metasenv,t' = aux metasenv subst n context t in
175 subst,metasenv,t'::pl
176 ) (subst,metasenv,[]) pl
178 subst,metasenv,C.MutCase (sp,i,outt', t', List.rev revpl')
180 (*CSC: not implemented
181 let tylen = List.length fl in
184 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
187 C.Fix (i, substitutedfl)
188 *) (* subst,metasenv,CicMetaSubst.lift subst 1 t' *)
189 subst,metasenv,CicSubstitution.lift 1 t'
191 (*CSC: not implemented
192 let tylen = List.length fl in
195 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
198 C.CoFix (i, substitutedfl)
199 *) (* subst,metasenv,CicMetasubst.lift subst 1 t' *)
200 subst,metasenv,CicSubstitution.lift 1 t'
202 and aux_exp_named_subst metasenv subst n context ens =
204 (fun (uri,t) (subst,metasenv,l) ->
205 let subst,metasenv,t' = aux metasenv subst n context t in
206 subst,metasenv,(uri,t')::l) ens (subst,metasenv,[])
208 let argty = type_of_aux' metasenv subst context arg in
210 FreshNamesGenerator.mk_fresh_name
211 metasenv context (Cic.Name "Heta") ~typ:argty
213 let subst,metasenv,t' = aux metasenv subst 0 context t in
216 subst, metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
218 subst, metasenv, C.Lambda (fresh_name,argty,t')
220 and beta_expand_many test_equality_only metasenv subst context t args =
221 let subst,metasenv,hd =
223 (fun arg (subst,metasenv,t) ->
224 let subst,metasenv,t =
225 beta_expand test_equality_only metasenv subst context t arg in
227 ) args (subst,metasenv,t) in
230 (* NUOVA UNIFICAZIONE *)
231 (* A substitution is a (int * Cic.term) list that associates a
232 metavariable i with its body.
233 A metaenv is a (int * Cic.term) list that associate a metavariable
235 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
236 a new substitution which is _NOT_ unwinded. It must be unwinded before
239 and fo_unif_subst test_equality_only subst context metasenv t1 t2 =
240 let module C = Cic in
241 let module R = CicReduction in
242 let module S = CicSubstitution in
243 let t1 = deref subst t1 in
244 let t2 = deref subst t2 in
245 if R.are_convertible ~subst ~metasenv context t1 t2 then
249 (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
250 let _,subst,metasenv =
253 (fun (j,subst,metasenv) t1 t2 ->
256 | _,None -> j+1,subst,metasenv
257 | Some t1', Some t2' ->
258 (* First possibility: restriction *)
259 (* Second possibility: unification *)
260 (* Third possibility: convertibility *)
261 if R.are_convertible ~subst ~metasenv context t1' t2' then
268 subst context metasenv t1' t2'
273 | UnificationFailure _ ->
274 prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j));
275 let metasenv, subst =
276 CicMetaSubst.restrict
277 subst [(n,j)] metasenv in
279 ) (1,subst,metasenv) ln lm
283 (UnificationFailure "1")
286 "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
287 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
288 | Invalid_argument _ ->
290 (UnificationFailure "2"))
293 "Error trying to unify %s with %s: the lengths of the two local contexts do not match." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))*)
295 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
296 fo_unif_subst test_equality_only subst context metasenv t2 t1
298 | (t, C.Meta (n,l)) ->
301 C.Meta (n,_), C.Meta (m,_) when n < m -> false
302 | _, C.Meta _ -> false
305 let lower = fun x y -> if swap then y else x in
306 let upper = fun x y -> if swap then x else y in
307 let fo_unif_subst_ordered
308 test_equality_only subst context metasenv m1 m2 =
309 fo_unif_subst test_equality_only subst context metasenv
310 (lower m1 m2) (upper m1 m2)
314 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
316 let tyt = type_of_aux' metasenv subst context t in
319 subst context metasenv tyt (S.lift_meta l meta_type)
321 UnificationFailure msg
323 prerr_endline msg;raise (UnificationFailure msg)
325 prerr_endline "siamo allo huge hack";
326 (* TODO huge hack!!!!
327 * we keep on unifying/refining in the hope that
328 * the problem will be eventually solved.
329 * In the meantime we're breaking a big invariant:
330 * the terms that we are unifying are no longer well
331 * typed in the current context (in the worst case
332 * we could even diverge) *)
333 (subst, metasenv)) in
334 let t',metasenv,subst =
336 CicMetaSubst.delift n subst context metasenv l t
338 (CicMetaSubst.MetaSubstFailure msg)->
339 raise (UnificationFailure msg)
340 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
344 C.Sort (C.Type u) when not test_equality_only ->
345 let u' = CicUniv.fresh () in
346 let s = C.Sort (C.Type u') in
347 ignore (CicUniv.add_ge (upper u u') (lower u u')) ;
351 (* Unifying the types may have already instantiated n. Let's check *)
353 let (_, oldt,_) = CicUtil.lookup_subst n subst in
354 let lifted_oldt = S.lift_meta l oldt in
355 fo_unif_subst_ordered
356 test_equality_only subst context metasenv t lifted_oldt
358 CicUtil.Subst_not_found _ ->
359 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
360 let subst = (n, (context, t'',ty)) :: subst in
362 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
365 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
366 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
367 if UriManager.eq uri1 uri2 then
368 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
369 exp_named_subst1 exp_named_subst2
371 raise (UnificationFailure "3")
373 "Can't unify %s with %s due to different constants"
374 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
375 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
376 if UriManager.eq uri1 uri2 && i1 = i2 then
377 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
378 exp_named_subst1 exp_named_subst2
380 raise (UnificationFailure "4")
382 "Can't unify %s with %s due to different inductive principles"
383 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
384 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
385 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
386 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
387 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
388 exp_named_subst1 exp_named_subst2
390 raise (UnificationFailure "5")
392 "Can't unify %s with %s due to different inductive constructors"
393 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
394 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
395 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
396 subst context metasenv te t2
397 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
398 subst context metasenv t1 te
399 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
400 (* TASSI: this is the only case in which we want == *)
401 let subst',metasenv' = fo_unif_subst true
402 subst context metasenv s1 s2 in
403 fo_unif_subst test_equality_only
404 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
405 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
406 (* TASSI: ask someone a reason for not putting true here *)
407 let subst',metasenv' = fo_unif_subst test_equality_only
408 subst context metasenv s1 s2 in
409 fo_unif_subst test_equality_only
410 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
411 | (C.LetIn (_,s1,t1), t2)
412 | (t2, C.LetIn (_,s1,t1)) ->
414 test_equality_only subst context metasenv t2 (S.subst s1 t1)
415 | (C.Appl l1, C.Appl l2) ->
416 (* andrea: this case should be probably rewritten in the
418 let rec beta_reduce =
420 (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
421 let he'' = CicSubstitution.subst he' t in
425 beta_reduce (Cic.Appl(he''::tl'))
428 (* andrea : this was too powerful. It works very bad with f_equal and
429 similar terms, try and see
430 C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
433 (fun (subst,metasenv) ->
434 fo_unif_subst test_equality_only subst context metasenv)
435 (subst,metasenv) l1 l2
436 with (Invalid_argument msg) -> raise (UnificationFailure msg))
437 | C.Meta (i,l)::args, _ ->
439 let (_,t,_) = CicUtil.lookup_subst i subst in
440 let lifted = S.lift_meta l t in
441 let reduced = beta_reduce (Cic.Appl (lifted::args)) in
444 subst context metasenv reduced t2
445 with CicUtil.Subst_not_found _ ->
446 let subst,metasenv,beta_expanded =
448 test_equality_only metasenv subst context t2 args in
449 fo_unif_subst test_equality_only subst context metasenv
450 (C.Meta (i,l)) beta_expanded)
451 | _, C.Meta (i,l)::args ->
453 let (_,t,_) = CicUtil.lookup_subst i subst in
454 let lifted = S.lift_meta l t in
455 let reduced = beta_reduce (Cic.Appl (lifted::args)) in
458 subst context metasenv t1 reduced
459 with CicUtil.Subst_not_found _ ->
460 let subst,metasenv,beta_expanded =
462 test_equality_only metasenv subst context t1 args in
463 fo_unif_subst test_equality_only subst context metasenv
464 (C.Meta (i,l)) beta_expanded)
467 let lr1 = List.rev l1 in
468 let lr2 = List.rev l2 in
469 let rec fo_unif_l test_equality_only subst metasenv =
472 | _,[] -> assert false
474 fo_unif_subst test_equality_only subst context metasenv h1 h2
477 fo_unif_subst test_equality_only subst context metasenv
478 h (C.Appl (List.rev l))
479 | ((h1::l1),(h2::l2)) ->
480 let subst', metasenv' =
481 fo_unif_subst test_equality_only subst context metasenv h1 h2
483 fo_unif_l test_equality_only subst' metasenv' (l1,l2)
485 fo_unif_l test_equality_only subst metasenv (lr1, lr2) )
486 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
487 let subst', metasenv' =
488 fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in
489 let subst'',metasenv'' =
490 fo_unif_subst test_equality_only subst' context metasenv' t1' t2' in
493 (function (subst,metasenv) ->
494 fo_unif_subst test_equality_only subst context metasenv
495 ) (subst'',metasenv'') pl1 pl2
497 Invalid_argument _ ->
498 raise (UnificationFailure "6"))
500 "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))) *)
501 | (C.Rel _, _) | (_, C.Rel _) ->
505 raise (UnificationFailure "6")
507 "Can't unify %s with %s because they are not convertible"
508 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
509 | (C.Sort _ ,_) | (_, C.Sort _)
510 | (C.Const _, _) | (_, C.Const _)
511 | (C.MutInd _, _) | (_, C.MutInd _)
512 | (C.MutConstruct _, _) | (_, C.MutConstruct _)
513 | (C.Fix _, _) | (_, C.Fix _)
514 | (C.CoFix _, _) | (_, C.CoFix _) ->
515 if t1 = t2 || R.are_convertible ~subst ~metasenv context t1 t2 then
518 raise (UnificationFailure "7")
520 "Can't unify %s with %s because they are not convertible"
521 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
523 if R.are_convertible ~subst ~metasenv context t1 t2 then
526 raise (UnificationFailure "8")
528 "Can't unify %s with %s because they are not convertible"
529 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
531 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
532 exp_named_subst1 exp_named_subst2
536 (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
538 fo_unif_subst test_equality_only subst context metasenv t1 t2
539 ) (subst,metasenv) exp_named_subst1 exp_named_subst2
541 Invalid_argument _ ->
546 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
549 raise (UnificationFailure (sprintf
550 "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2)))
552 (* A substitution is a (int * Cic.term) list that associates a *)
553 (* metavariable i with its body. *)
554 (* metasenv is of type Cic.metasenv *)
555 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
556 (* a new substitution which is already unwinded and ready to be applied and *)
557 (* a new metasenv in which some hypothesis in the contexts of the *)
558 (* metavariables may have been restricted. *)
559 let fo_unif metasenv context t1 t2 =
560 fo_unif_subst false [] context metasenv t1 t2 ;;
562 let fo_unif_subst subst context metasenv t1 t2 =
563 let enrich_msg msg = (* "bella roba" *)
564 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
565 (CicMetaSubst.ppterm subst t1)
567 CicPp.ppterm (type_of_aux' metasenv subst context t1)
568 with _ -> "MALFORMED")
569 (CicMetaSubst.ppterm subst t2)
571 CicPp.ppterm (type_of_aux' metasenv subst context t2)
572 with _ -> "MALFORMED")
573 (CicMetaSubst.ppcontext subst context)
574 (CicMetaSubst.ppmetasenv metasenv subst)
575 (CicMetaSubst.ppsubst subst) msg
578 fo_unif_subst false subst context metasenv t1 t2
580 | AssertFailure msg -> raise (AssertFailure (enrich_msg msg))
581 | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))