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))) *)
66 (CicSubstitution.lift_meta
67 l (snd (CicUtil.lookup_subst n subst)))
69 CicUtil.Subst_not_found _ -> t)
73 let rec beta_expand test_equality_only metasenv subst context t arg =
74 let module S = CicSubstitution in
76 let rec aux metasenv subst n context t' =
79 fo_unif_subst test_equality_only subst context metasenv
80 (CicSubstitution.lift n arg) t'
82 subst,metasenv,C.Rel (1 + n)
85 | UnificationFailure _ ->
87 | C.Rel m -> subst,metasenv, if m <= n then C.Rel m else C.Rel (m+1)
88 | C.Var (uri,exp_named_subst) ->
89 let subst,metasenv,exp_named_subst' =
90 aux_exp_named_subst metasenv subst n context exp_named_subst
92 subst,metasenv,C.Var (uri,exp_named_subst')
94 (* andrea: in general, beta_expand can create badly typed
95 terms. This happens quite seldom in practice, UNLESS we
96 iterate on the local context. For this reason, we renounce
97 to iterate and just lift *)
101 Some t -> Some (CicSubstitution.lift 1 t)
103 subst, metasenv, C.Meta (i,l)
105 let (subst, metasenv, context, local_context) =
107 (fun t (subst, metasenv, context, local_context) ->
109 | None -> (subst, metasenv, context, None :: local_context)
111 let (subst, metasenv, t) =
112 aux metasenv subst n context t
114 (subst, metasenv, context, Some t :: local_context))
115 l (subst, metasenv, context, [])
117 prerr_endline ("nuova meta :" ^ (CicPp.ppterm (C.Meta (i, local_context))));
118 (subst, metasenv, C.Meta (i, local_context)) *)
120 | C.Implicit _ as t -> subst,metasenv,t
122 let subst,metasenv,te' = aux metasenv subst n context te in
123 let subst,metasenv,ty' = aux metasenv subst n context ty in
124 subst,metasenv,C.Cast (te', ty')
126 let subst,metasenv,s' = aux metasenv subst n context s in
127 let subst,metasenv,t' =
128 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
130 subst,metasenv,C.Prod (nn, s', t')
131 | C.Lambda (nn,s,t) ->
132 let subst,metasenv,s' = aux metasenv subst n context s in
133 let subst,metasenv,t' =
134 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
136 subst,metasenv,C.Lambda (nn, s', t')
137 | C.LetIn (nn,s,t) ->
138 let subst,metasenv,s' = aux metasenv subst n context s in
139 let subst,metasenv,t' =
140 aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
142 subst,metasenv,C.LetIn (nn, s', t')
144 let subst,metasenv,revl' =
146 (fun (subst,metasenv,appl) t ->
147 let subst,metasenv,t' = aux metasenv subst n context t in
148 subst,metasenv,t'::appl
149 ) (subst,metasenv,[]) l
151 subst,metasenv,C.Appl (List.rev revl')
152 | C.Const (uri,exp_named_subst) ->
153 let subst,metasenv,exp_named_subst' =
154 aux_exp_named_subst metasenv subst n context exp_named_subst
156 subst,metasenv,C.Const (uri,exp_named_subst')
157 | C.MutInd (uri,i,exp_named_subst) ->
158 let subst,metasenv,exp_named_subst' =
159 aux_exp_named_subst metasenv subst n context exp_named_subst
161 subst,metasenv,C.MutInd (uri,i,exp_named_subst')
162 | C.MutConstruct (uri,i,j,exp_named_subst) ->
163 let subst,metasenv,exp_named_subst' =
164 aux_exp_named_subst metasenv subst n context exp_named_subst
166 subst,metasenv,C.MutConstruct (uri,i,j,exp_named_subst')
167 | C.MutCase (sp,i,outt,t,pl) ->
168 let subst,metasenv,outt' = aux metasenv subst n context outt in
169 let subst,metasenv,t' = aux metasenv subst n context t in
170 let subst,metasenv,revpl' =
172 (fun (subst,metasenv,pl) t ->
173 let subst,metasenv,t' = aux metasenv subst n context t in
174 subst,metasenv,t'::pl
175 ) (subst,metasenv,[]) pl
177 subst,metasenv,C.MutCase (sp,i,outt', t', List.rev revpl')
179 (*CSC: not implemented
180 let tylen = List.length fl in
183 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
186 C.Fix (i, substitutedfl)
187 *) (* subst,metasenv,CicMetaSubst.lift subst 1 t' *)
188 subst,metasenv,CicSubstitution.lift 1 t'
190 (*CSC: not implemented
191 let tylen = List.length fl in
194 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
197 C.CoFix (i, substitutedfl)
198 *) (* subst,metasenv,CicMetasubst.lift subst 1 t' *)
199 subst,metasenv,CicSubstitution.lift 1 t'
201 and aux_exp_named_subst metasenv subst n context ens =
203 (fun (uri,t) (subst,metasenv,l) ->
204 let subst,metasenv,t' = aux metasenv subst n context t in
205 subst,metasenv,(uri,t')::l) ens (subst,metasenv,[])
207 let argty = type_of_aux' metasenv subst context arg in
209 FreshNamesGenerator.mk_fresh_name
210 metasenv context (Cic.Name "Heta") ~typ:argty
212 let subst,metasenv,t' = aux metasenv subst 0 context t in
215 subst, metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
217 subst, metasenv, C.Lambda (fresh_name,argty,t')
219 and beta_expand_many test_equality_only metasenv subst context t args =
220 let subst,metasenv,hd =
222 (fun arg (subst,metasenv,t) ->
223 let subst,metasenv,t =
224 beta_expand test_equality_only metasenv subst context t arg in
226 ) args (subst,metasenv,t) in
229 (* NUOVA UNIFICAZIONE *)
230 (* A substitution is a (int * Cic.term) list that associates a
231 metavariable i with its body.
232 A metaenv is a (int * Cic.term) list that associate a metavariable
234 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
235 a new substitution which is _NOT_ unwinded. It must be unwinded before
238 and fo_unif_subst test_equality_only subst context metasenv t1 t2 =
239 let module C = Cic in
240 let module R = CicReduction in
241 let module S = CicSubstitution in
242 let t1 = deref subst t1 in
243 let t2 = deref subst t2 in
245 (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
246 let _,subst,metasenv =
249 (fun (j,subst,metasenv) t1 t2 ->
252 | _,None -> j+1,subst,metasenv
253 | Some t1', Some t2' ->
254 (* First possibility: restriction *)
255 (* Second possibility: unification *)
256 (* Third possibility: convertibility *)
257 if R.are_convertible ~subst ~metasenv context t1' t2' then
264 subst context metasenv t1' t2'
269 | UnificationFailure _ ->
270 prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j));
271 let metasenv, subst =
272 CicMetaSubst.restrict
273 subst [(n,j)] metasenv in
275 ) (1,subst,metasenv) ln lm
279 (UnificationFailure "1")
282 "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."
283 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
284 | Invalid_argument _ ->
286 (UnificationFailure "2"))
289 "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))))*)
291 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
292 fo_unif_subst test_equality_only subst context metasenv t2 t1
294 | (t, C.Meta (n,l)) ->
297 C.Meta (n,_), C.Meta (m,_) when n < m -> false
298 | _, C.Meta _ -> false
301 let lower = fun x y -> if swap then y else x in
302 let upper = fun x y -> if swap then x else y in
303 let fo_unif_subst_ordered
304 test_equality_only subst context metasenv m1 m2 =
305 fo_unif_subst test_equality_only subst context metasenv
306 (lower m1 m2) (upper m1 m2)
310 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
312 let tyt = type_of_aux' metasenv subst context t in
315 subst context metasenv tyt (S.lift_meta l meta_type)
317 UnificationFailure msg
319 prerr_endline msg;raise (UnificationFailure msg)
321 prerr_endline "siamo allo huge hack";
322 (* TODO huge hack!!!!
323 * we keep on unifying/refining in the hope that
324 * the problem will be eventually solved.
325 * In the meantime we're breaking a big invariant:
326 * the terms that we are unifying are no longer well
327 * typed in the current context (in the worst case
328 * we could even diverge) *)
329 (subst, metasenv)) in
330 let t',metasenv,subst =
332 CicMetaSubst.delift n subst context metasenv l t
334 (CicMetaSubst.MetaSubstFailure msg)->
335 raise (UnificationFailure msg)
336 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
340 C.Sort (C.Type u) when not test_equality_only ->
341 let u' = CicUniv.fresh () in
342 let s = C.Sort (C.Type u') in
343 ignore (CicUniv.add_ge (upper u u') (lower u u')) ;
347 (* Unifying the types may have already instantiated n. Let's check *)
349 let (_, oldt) = CicUtil.lookup_subst n subst in
350 let lifted_oldt = S.lift_meta l oldt in
351 fo_unif_subst_ordered
352 test_equality_only subst context metasenv t lifted_oldt
354 CicUtil.Subst_not_found _ ->
355 let (_, context, _) = CicUtil.lookup_meta n metasenv in
356 let subst = (n, (context, t'')) :: subst in
358 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
361 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
362 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
363 if UriManager.eq uri1 uri2 then
364 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
365 exp_named_subst1 exp_named_subst2
367 raise (UnificationFailure "3")
369 "Can't unify %s with %s due to different constants"
370 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
371 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
372 if UriManager.eq uri1 uri2 && i1 = i2 then
373 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
374 exp_named_subst1 exp_named_subst2
376 raise (UnificationFailure "4")
378 "Can't unify %s with %s due to different inductive principles"
379 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
380 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
381 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
382 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
383 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
384 exp_named_subst1 exp_named_subst2
386 raise (UnificationFailure "5")
388 "Can't unify %s with %s due to different inductive constructors"
389 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
390 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
391 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
392 subst context metasenv te t2
393 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
394 subst context metasenv t1 te
395 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
396 (* TASSI: this is the only case in which we want == *)
397 let subst',metasenv' = fo_unif_subst true
398 subst context metasenv s1 s2 in
399 fo_unif_subst test_equality_only
400 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
401 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
402 (* TASSI: ask someone a reason for not putting true here *)
403 let subst',metasenv' = fo_unif_subst test_equality_only
404 subst context metasenv s1 s2 in
405 fo_unif_subst test_equality_only
406 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
407 | (C.LetIn (_,s1,t1), t2)
408 | (t2, C.LetIn (_,s1,t1)) ->
410 test_equality_only subst context metasenv t2 (S.subst s1 t1)
411 | (C.Appl l1, C.Appl l2) ->
412 (* andrea: this case should be probably rewritten in the
414 let rec beta_reduce =
416 (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
417 let he'' = CicSubstitution.subst he' t in
421 beta_reduce (Cic.Appl(he''::tl'))
424 C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
427 (fun (subst,metasenv) ->
428 fo_unif_subst test_equality_only subst context metasenv)
429 (subst,metasenv) l1 l2
430 with (Invalid_argument msg) -> raise (UnificationFailure msg))
431 | C.Meta (i,l)::args, _ ->
433 let (_,t) = CicUtil.lookup_subst i subst in
434 let lifted = S.lift_meta l t in
435 let reduced = beta_reduce (Cic.Appl (lifted::args)) in
438 subst context metasenv reduced t2
439 with CicUtil.Subst_not_found _ ->
440 let subst,metasenv,beta_expanded =
442 test_equality_only metasenv subst context t2 args in
443 fo_unif_subst test_equality_only subst context metasenv
444 (C.Meta (i,l)) beta_expanded)
445 | _, C.Meta (i,l)::args ->
447 let (_,t) = CicUtil.lookup_subst i subst in
448 let lifted = S.lift_meta l t in
449 let reduced = beta_reduce (Cic.Appl (lifted::args)) in
452 subst context metasenv t1 reduced
453 with CicUtil.Subst_not_found _ ->
454 let subst,metasenv,beta_expanded =
456 test_equality_only metasenv subst context t1 args in
457 fo_unif_subst test_equality_only subst context metasenv
458 (C.Meta (i,l)) beta_expanded)
460 let lr1 = List.rev l1 in
461 let lr2 = List.rev l2 in
462 let rec fo_unif_l test_equality_only subst metasenv =
465 | _,[] -> assert false
467 fo_unif_subst test_equality_only subst context metasenv h1 h2
470 fo_unif_subst test_equality_only subst context metasenv
471 h (C.Appl (List.rev l))
472 | ((h1::l1),(h2::l2)) ->
473 let subst', metasenv' =
474 fo_unif_subst test_equality_only subst context metasenv h1 h2
476 fo_unif_l test_equality_only subst' metasenv' (l1,l2)
478 fo_unif_l test_equality_only subst metasenv (lr1, lr2) )
479 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
480 let subst', metasenv' =
481 fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in
482 let subst'',metasenv'' =
483 fo_unif_subst test_equality_only subst' context metasenv' t1' t2' in
486 (function (subst,metasenv) ->
487 fo_unif_subst test_equality_only subst context metasenv
488 ) (subst'',metasenv'') pl1 pl2
490 Invalid_argument _ ->
491 raise (UnificationFailure "6"))
493 "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))) *)
494 | (C.Rel _, _) | (_, C.Rel _) ->
498 raise (UnificationFailure "6")
500 "Can't unify %s with %s because they are not convertible"
501 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
502 | (C.Sort _ ,_) | (_, C.Sort _)
503 | (C.Const _, _) | (_, C.Const _)
504 | (C.MutInd _, _) | (_, C.MutInd _)
505 | (C.MutConstruct _, _) | (_, C.MutConstruct _)
506 | (C.Fix _, _) | (_, C.Fix _)
507 | (C.CoFix _, _) | (_, C.CoFix _) ->
508 if t1 = t2 || R.are_convertible ~subst ~metasenv context t1 t2 then
511 raise (UnificationFailure "7")
513 "Can't unify %s with %s because they are not convertible"
514 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
516 if R.are_convertible ~subst ~metasenv context t1 t2 then
519 raise (UnificationFailure "8")
521 "Can't unify %s with %s because they are not convertible"
522 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
524 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
525 exp_named_subst1 exp_named_subst2
529 (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
531 fo_unif_subst test_equality_only subst context metasenv t1 t2
532 ) (subst,metasenv) exp_named_subst1 exp_named_subst2
534 Invalid_argument _ ->
539 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
542 raise (UnificationFailure (sprintf
543 "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)))
545 (* A substitution is a (int * Cic.term) list that associates a *)
546 (* metavariable i with its body. *)
547 (* metasenv is of type Cic.metasenv *)
548 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
549 (* a new substitution which is already unwinded and ready to be applied and *)
550 (* a new metasenv in which some hypothesis in the contexts of the *)
551 (* metavariables may have been restricted. *)
552 let fo_unif metasenv context t1 t2 =
553 fo_unif_subst false [] context metasenv t1 t2 ;;
555 let fo_unif_subst subst context metasenv t1 t2 =
556 let enrich_msg msg = (* "bella roba" *)
557 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"
558 (CicMetaSubst.ppterm subst t1)
560 CicPp.ppterm (type_of_aux' metasenv subst context t1)
561 with _ -> "MALFORMED")
562 (CicMetaSubst.ppterm subst t2)
564 CicPp.ppterm (type_of_aux' metasenv subst context t2)
565 with _ -> "MALFORMED")
566 (CicMetaSubst.ppcontext subst context)
567 (CicMetaSubst.ppmetasenv metasenv subst)
568 (CicMetaSubst.ppsubst subst) msg
571 fo_unif_subst false subst context metasenv t1 t2
573 | AssertFailure msg -> raise (AssertFailure (enrich_msg msg))
574 | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))