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 ugraph =
36 CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph
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 let snd (_,a,_) = a in
56 (CicSubstitution.subst_meta
57 l (snd (CicUtil.lookup_subst n subst)))
59 CicUtil.Subst_not_found _ -> t)
63 let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
64 let module S = CicSubstitution in
66 let rec aux metasenv subst n context t' ugraph =
69 let subst,metasenv,ugraph1 =
70 fo_unif_subst test_equality_only subst context metasenv
71 (CicSubstitution.lift n arg) t' ugraph
74 subst,metasenv,C.Rel (1 + n),ugraph1
77 | UnificationFailure _ ->
79 | C.Rel m -> subst,metasenv,
80 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
81 | C.Var (uri,exp_named_subst) ->
82 let subst,metasenv,exp_named_subst',ugraph1 =
83 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
85 (* THIS WAS BEFORE ----
86 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
89 let (_, t') = CicMetaSubst.lookup_subst i subst in
90 aux metasenv subst n context (CicSubstitution.subst_meta l t')
92 with CicMetaSubst.SubstNotFound _ ->
93 let (subst, metasenv, context, local_context,ugraph1) =
95 (fun (subst, metasenv, context, local_context,ugraph) t ->
98 (subst, metasenv, context, None::local_context, ugraph)
100 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
102 (* andrea: in general, beta_expand can create badly typed
103 terms. This happens quite seldom in practice, UNLESS we
104 iterate on the local context. For this reason, we renounce
105 to iterate and just lift *)
109 Some t -> Some (CicSubstitution.lift 1 t)
111 subst, metasenv, C.Meta (i,l), ugraph
113 let (subst, metasenv, context, local_context) =
115 (fun t (subst, metasenv, context, local_context) ->
117 | None -> (subst, metasenv, context, None :: local_context)
120 let (subst, metasenv, t, ugraph1) =
121 aux metasenv subst n context t ugraph
123 (* THIS WAS BEFORE ----
124 (subst, metasenv, context,
125 (Some t)::local_context,ugraph1))
126 (subst, metasenv, context, [],ugraph) l
128 (subst, metasenv,(C.Meta (i, local_context)),ugraph1))
130 (subst, metasenv, context, Some t :: local_context))
131 l (subst, metasenv, context, [])
133 prerr_endline ("nuova meta :" ^ (CicPp.ppterm (C.Meta (i, local_context))));
134 (subst, metasenv, C.Meta (i, local_context)) *)
136 | C.Implicit _ as t -> subst,metasenv,t,ugraph
138 let subst,metasenv,te',ugraph1 =
139 aux metasenv subst n context te ugraph in
140 let subst,metasenv,ty',ugraph2 =
141 aux metasenv subst n context ty ugraph1 in
142 (* TASSI: sure this is in serial? *)
143 subst,metasenv,(C.Cast (te', ty')),ugraph2
145 let subst,metasenv,s',ugraph1 =
146 aux metasenv subst n context s ugraph in
147 let subst,metasenv,t',ugraph2 =
148 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
151 (* TASSI: sure this is in serial? *)
152 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
153 | C.Lambda (nn,s,t) ->
154 let subst,metasenv,s',ugraph1 =
155 aux metasenv subst n context s ugraph in
156 let subst,metasenv,t',ugraph2 =
157 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
159 (* TASSI: sure this is in serial? *)
160 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
161 | C.LetIn (nn,s,t) ->
162 let subst,metasenv,s',ugraph1 =
163 aux metasenv subst n context s ugraph in
164 let subst,metasenv,t',ugraph2 =
165 aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
168 (* TASSI: sure this is in serial? *)
169 subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
171 let subst,metasenv,revl',ugraph1 =
173 (fun (subst,metasenv,appl,ugraph) t ->
174 let subst,metasenv,t',ugraph1 =
175 aux metasenv subst n context t ugraph in
176 subst,metasenv,(t'::appl),ugraph1
177 ) (subst,metasenv,[],ugraph) l
179 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
180 | C.Const (uri,exp_named_subst) ->
181 let subst,metasenv,exp_named_subst',ugraph1 =
182 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
184 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
185 | C.MutInd (uri,i,exp_named_subst) ->
186 let subst,metasenv,exp_named_subst',ugraph1 =
187 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
189 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
190 | C.MutConstruct (uri,i,j,exp_named_subst) ->
191 let subst,metasenv,exp_named_subst',ugraph1 =
192 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
194 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
195 | C.MutCase (sp,i,outt,t,pl) ->
196 let subst,metasenv,outt',ugraph1 =
197 aux metasenv subst n context outt ugraph in
198 let subst,metasenv,t',ugraph2 =
199 aux metasenv subst n context t ugraph1 in
200 let subst,metasenv,revpl',ugraph3 =
202 (fun (subst,metasenv,pl,ugraph) t ->
203 let subst,metasenv,t',ugraph1 =
204 aux metasenv subst n context t ugraph in
205 subst,metasenv,(t'::pl),ugraph1
206 ) (subst,metasenv,[],ugraph2) pl
208 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
209 (* TASSI: not sure this is serial *)
211 (*CSC: not implemented
212 let tylen = List.length fl in
215 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
218 C.Fix (i, substitutedfl)
220 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
222 (*CSC: not implemented
223 let tylen = List.length fl in
226 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
229 C.CoFix (i, substitutedfl)
232 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
234 and aux_exp_named_subst metasenv subst n context ens ugraph =
236 (fun (uri,t) (subst,metasenv,l,ugraph) ->
237 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
238 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
240 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
242 FreshNamesGenerator.mk_fresh_name ~subst
243 metasenv context (Cic.Name "Heta") ~typ:argty
245 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
248 subst, metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
250 subst, metasenv, C.Lambda (fresh_name,argty,t'), ugraph2
254 and beta_expand_many test_equality_only metasenv subst context t l ugraph =
256 (fun (subst,metasenv,t,ugraph) arg ->
257 beta_expand test_equality_only metasenv subst context t arg ugraph
258 ) (subst,metasenv,t,ugraph) l
260 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
261 let subst,metasenv,hd,ugraph =
263 (fun arg (subst,metasenv,t,ugraph) ->
264 let subst,metasenv,t,ugraph1 =
265 beta_expand test_equality_only
266 metasenv subst context t arg ugraph
268 subst,metasenv,t,ugraph1
269 ) args (subst,metasenv,t,ugraph)
271 subst,metasenv,hd,ugraph
274 (* NUOVA UNIFICAZIONE *)
275 (* A substitution is a (int * Cic.term) list that associates a
276 metavariable i with its body.
277 A metaenv is a (int * Cic.term) list that associate a metavariable
279 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
280 a new substitution which is _NOT_ unwinded. It must be unwinded before
283 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
284 let module C = Cic in
285 let module R = CicReduction in
286 let module S = CicSubstitution in
287 let t1 = deref subst t1 in
288 let t2 = deref subst t2 in
290 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
293 subst, metasenv, ugraph
296 (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
298 let ok,subst,metasenv,ugraph1 =
301 (fun (b,subst,metasenv,ugraph) t1 t2 ->
302 if b then true,subst,metasenv,ugraph else
305 | _,None -> true,subst,metasenv,ugraph
306 | Some t1', Some t2' ->
307 (* First possibility: restriction *)
308 (* Second possibility: unification *)
309 (* Third possibility: convertibility *)
311 R.are_convertible subst context t1' t2' ugraph in
313 true,subst,metasenv,ugraph1
316 let subst,metasenv,ugraph2 =
318 (* TASSI: is this another try that should use ugraph? *)
319 test_equality_only subst context metasenv t1' t2' ugraph
321 true,subst,metasenv,ugraph2
323 Not_found -> false,subst,metasenv,ugraph1)
324 ) (true,subst,metasenv,ugraph) ln lm
326 Invalid_argument _ ->
327 raise (UnificationFailure (sprintf
328 "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)))
331 subst,metasenv,ugraph1
333 raise (UnificationFailure (sprintf
334 "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."
335 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
337 let _,subst,metasenv,ugraph1 =
340 (fun (j,subst,metasenv,ugraph) t1 t2 ->
343 | _,None -> j+1,subst,metasenv,ugraph
344 | Some t1', Some t2' ->
345 (* First possibility: restriction *)
346 (* Second possibility: unification *)
347 (* Third possibility: convertibility *)
350 ~subst ~metasenv context t1' t2' ugraph
353 j+1,subst,metasenv, ugraph1
356 let subst,metasenv,ugraph2 =
359 subst context metasenv t1' t2' ugraph
361 j+1,subst,metasenv,ugraph2
364 | UnificationFailure _ ->
365 prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j));
366 let metasenv, subst =
367 CicMetaSubst.restrict
368 subst [(n,j)] metasenv in
369 j+1,subst,metasenv,ugraph1)
370 ) (1,subst,metasenv,ugraph) ln lm
374 (UnificationFailure "1")
377 "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."
378 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
379 | Invalid_argument _ ->
381 (UnificationFailure "2"))
384 "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))))*)
385 in subst,metasenv,ugraph1
387 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
388 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
390 | (t, C.Meta (n,l)) ->
393 C.Meta (n,_), C.Meta (m,_) when n < m -> false
394 | _, C.Meta _ -> false
397 let lower = fun x y -> if swap then y else x in
398 let upper = fun x y -> if swap then x else y in
399 let fo_unif_subst_ordered
400 test_equality_only subst context metasenv m1 m2 ugraph =
401 fo_unif_subst test_equality_only subst context metasenv
402 (lower m1 m2) (upper m1 m2) ugraph
407 let (_, oldt) = CicMetaSubst.lookup_subst n subst in
408 let lifted_oldt = S.subst_meta l oldt in
409 let ty_lifted_oldt,ugraph1 =
410 type_of_aux' metasenv subst context lifted_oldt ugraph
412 let tyt,ugraph2 = type_of_aux' metasenv subst context t ugraph1 in
413 let (subst, metasenv, ugraph3) =
414 fo_unif_subst_ordered test_equality_only subst context metasenv
415 tyt ty_lifted_oldt ugraph2
417 fo_unif_subst_ordered
418 test_equality_only subst context metasenv t lifted_oldt ugraph3
419 with CicMetaSubst.SubstNotFound _ ->
420 (* First of all we unify the type of the meta with the type of the term *)
421 let subst,metasenv,ugraph1 =
422 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
424 let tyt,ugraph1 = type_of_aux' metasenv subst context t ugraph in
427 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
428 with AssertFailure _ ->
429 (* TODO huge hack!!!!
430 * we keep on unifying/refining in the hope that the problem will be
431 * eventually solved. In the meantime we're breaking a big invariant:
432 * the terms that we are unifying are no longer well typed in the
433 * current context (in the worst case we could even diverge)
436 prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
437 prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
439 (subst, metasenv,ugraph))
441 let t',metasenv,subst =
443 (* TASSI: I hope delift does nothing with universes *)
444 CicMetaSubst.delift n subst context metasenv l t
446 (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
447 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
451 C.Sort (C.Type u) when not test_equality_only ->
452 let u' = CicUniv.fresh () in
453 let s = C.Sort (C.Type u') in
455 CicUniv.add_ge (upper u u') (lower u u') ugraph1 in
459 (* Unifying the types may have already instantiated n. Let's check *)
461 let (_, oldt) = CicMetaSubst.lookup_subst n subst in
462 let lifted_oldt = S.subst_meta l oldt in
463 fo_unif_subst_ordered
464 test_equality_only subst context metasenv t lifted_oldt ugraph2
466 CicMetaSubst.SubstNotFound _ ->
467 let (_, context, _) = CicUtil.lookup_meta n metasenv in
468 let subst = (n, (context, t'')) :: subst in
470 (* CicMetaSubst.apply_subst_metasenv [n,(context, t'')] metasenv *)
471 CicMetaSubst.apply_subst_metasenv subst metasenv
473 subst, metasenv,ugraph2
474 (* (n,t'')::subst, metasenv *)
478 let subst,metasenv,ugraph1 =
479 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
482 type_of_aux' metasenv subst context t ugraph
486 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
488 UnificationFailure msg
490 prerr_endline msg;raise (UnificationFailure msg)
492 prerr_endline "siamo allo huge hack";
493 (* TODO huge hack!!!!
494 * we keep on unifying/refining in the hope that
495 * the problem will be eventually solved.
496 * In the meantime we're breaking a big invariant:
497 * the terms that we are unifying are no longer well
498 * typed in the current context (in the worst case
499 * we could even diverge) *)
500 (subst, metasenv,ugraph)) in
501 let t',metasenv,subst =
503 CicMetaSubst.delift n subst context metasenv l t
505 (CicMetaSubst.MetaSubstFailure msg)->
506 raise (UnificationFailure msg)
507 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
511 C.Sort (C.Type u) when not test_equality_only ->
512 let u' = CicUniv.fresh () in
513 let s = C.Sort (C.Type u') in
515 CicUniv.add_ge (upper u u') (lower u u') ugraph1
520 (* Unifying the types may have already instantiated n. Let's check *)
522 let (_, oldt,_) = CicUtil.lookup_subst n subst in
523 let lifted_oldt = S.subst_meta l oldt in
524 fo_unif_subst_ordered
525 test_equality_only subst context metasenv t lifted_oldt ugraph2
527 CicUtil.Subst_not_found _ ->
528 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
529 let subst = (n, (context, t'',ty)) :: subst in
531 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
532 subst, metasenv, ugraph2
535 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
536 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
537 if UriManager.eq uri1 uri2 then
538 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
539 exp_named_subst1 exp_named_subst2 ugraph
541 raise (UnificationFailure "3")
543 "Can't unify %s with %s due to different constants"
544 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
545 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
546 if UriManager.eq uri1 uri2 && i1 = i2 then
547 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
548 exp_named_subst1 exp_named_subst2 ugraph
550 raise (UnificationFailure "4")
552 "Can't unify %s with %s due to different inductive principles"
553 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
554 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
555 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
556 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
557 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
558 exp_named_subst1 exp_named_subst2 ugraph
560 raise (UnificationFailure "5")
562 "Can't unify %s with %s due to different inductive constructors"
563 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
564 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
565 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
566 subst context metasenv te t2 ugraph
567 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
568 subst context metasenv t1 te ugraph
569 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
570 let subst',metasenv',ugraph1 =
571 fo_unif_subst true subst context metasenv s1 s2 ugraph
573 fo_unif_subst test_equality_only
574 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
575 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
576 let subst',metasenv',ugraph1 =
577 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
579 fo_unif_subst test_equality_only
580 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
581 | (C.LetIn (_,s1,t1), t2)
582 | (t2, C.LetIn (_,s1,t1)) ->
584 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
585 | (C.Appl l1, C.Appl l2) ->
586 (* WAS BEFORE ----------
587 let subst,metasenv,t1',t2',ugraph1 =
589 C.Meta (i,_)::_, C.Meta (j,_)::_ when i = j ->
590 subst,metasenv,t1,t2,ugraph
591 (* In the first two cases when we reach the next begin ... end
592 section useless work is done since, by construction, the list
593 of arguments will be equal.
596 (* andrea: this case should be probably rewritten in the
598 let rec beta_reduce =
600 (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
601 let he'' = CicSubstitution.subst he' t in
605 beta_reduce (Cic.Appl(he''::tl'))
607 let exists_a_meta l =
608 List.exists (function Cic.Meta _ -> true | _ -> false) l
611 C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
614 (fun (subst,metasenv,ugraph) t1 t2 ->
616 test_equality_only subst context metasenv t1 t2 ugraph)
617 (subst,metasenv,ugraph) l1 l2
618 with (Invalid_argument msg) -> raise (UnificationFailure msg))
619 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
620 (* we verify that none of the args is a Meta, since beta expanding
621 with respoect to a metavariable makes no sense
624 let (_,t,_) = CicUtil.lookup_subst i subst in
625 let lifted = S.subst_meta l t in
626 let reduced = beta_reduce (Cic.Appl (lifted::args)) in
629 subst context metasenv reduced t2 ugraph
630 with CicUtil.Subst_not_found _ ->
631 let subst,metasenv,beta_expanded,ugraph1 =
633 test_equality_only metasenv subst context t2 args ugraph
635 fo_unif_subst test_equality_only subst context metasenv
636 (C.Meta (i,l)) beta_expanded ugraph1)
637 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
639 let (_,t,_) = CicUtil.lookup_subst i subst in
640 let lifted = S.subst_meta l t in
641 let reduced = beta_reduce (Cic.Appl (lifted::args)) in
644 subst context metasenv t1 reduced ugraph
645 with CicUtil.Subst_not_found _ ->
646 let subst,metasenv,beta_expanded,ugraph1 =
648 test_equality_only metasenv subst context t1 args ugraph in
649 fo_unif_subst test_equality_only subst context metasenv
650 (C.Meta (i,l)) beta_expanded ugraph1)
652 let lr1 = List.rev l1 in
653 let lr2 = List.rev l2 in
655 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
658 | _,[] -> assert false
661 test_equality_only subst context metasenv h1 h2 ugraph
664 fo_unif_subst test_equality_only subst context metasenv
665 h (C.Appl (List.rev l)) ugraph
666 | ((h1::l1),(h2::l2)) ->
667 let subst', metasenv',ugraph1 =
669 test_equality_only subst context metasenv h1 h2 ugraph
672 test_equality_only subst' metasenv' (l1,l2) ugraph1
675 test_equality_only subst metasenv (lr1, lr2) ugraph)(**)
676 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
677 let subst', metasenv',ugraph1 =
678 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
680 let subst'',metasenv'',ugraph2 =
681 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
685 (fun (subst,metasenv,ugraph) t1 t2 ->
687 test_equality_only subst context metasenv t1 t2 ugraph
688 ) (subst'',metasenv'',ugraph2) pl1 pl2
690 Invalid_argument _ ->
691 raise (UnificationFailure "6"))
693 "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))) *)
694 | (C.Rel _, _) | (_, C.Rel _) ->
696 subst, metasenv,ugraph
698 raise (UnificationFailure "6")
700 "Can't unify %s with %s because they are not convertible"
701 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
702 | (C.Sort _ ,_) | (_, C.Sort _)
703 | (C.Const _, _) | (_, C.Const _)
704 | (C.MutInd _, _) | (_, C.MutInd _)
705 | (C.MutConstruct _, _) | (_, C.MutConstruct _)
706 | (C.Fix _, _) | (_, C.Fix _)
707 | (C.CoFix _, _) | (_, C.CoFix _) ->
709 subst, metasenv, ugraph
712 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
715 subst, metasenv, ugraph1
717 raise (UnificationFailure "7")
719 "Can't unify %s with %s because they are not convertible"
720 (CicMetaSubst.ppterm subst t1)
721 (CicMetaSubst.ppterm subst t2))) *)
723 let t2' = R.whd ~subst context t2 in
726 fo_unif_subst test_equality_only
727 subst context metasenv t1 t2' ugraph
728 | _ -> raise (UnificationFailure "8"))
730 let t1' = R.whd ~subst context t1 in
733 fo_unif_subst test_equality_only
734 subst context metasenv t1' t2 ugraph
735 | _ -> raise (UnificationFailure "9"))
738 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
741 subst, metasenv, ugraph1
743 raise (UnificationFailure "10")
745 "Can't unify %s with %s because they are not convertible"
746 (CicMetaSubst.ppterm subst t1)
747 (CicMetaSubst.ppterm subst t2))) *)
749 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
750 exp_named_subst1 exp_named_subst2 ugraph
754 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
756 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
757 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
759 Invalid_argument _ ->
764 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
767 raise (UnificationFailure (sprintf
768 "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)))
770 (* A substitution is a (int * Cic.term) list that associates a *)
771 (* metavariable i with its body. *)
772 (* metasenv is of type Cic.metasenv *)
773 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
774 (* a new substitution which is already unwinded and ready to be applied and *)
775 (* a new metasenv in which some hypothesis in the contexts of the *)
776 (* metavariables may have been restricted. *)
777 let fo_unif metasenv context t1 t2 ugraph =
778 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
780 let fo_unif_subst subst context metasenv t1 t2 ugraph =
781 let enrich_msg msg = (* "bella roba" *)
782 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"
783 (CicMetaSubst.ppterm subst t1)
785 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
787 with _ -> "MALFORMED")
788 (CicMetaSubst.ppterm subst t2)
790 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
792 with _ -> "MALFORMED")
793 (CicMetaSubst.ppcontext subst context)
794 (CicMetaSubst.ppmetasenv metasenv subst)
795 (CicMetaSubst.ppsubst subst) msg
798 fo_unif_subst false subst context metasenv t1 t2 ugraph
800 | AssertFailure msg -> raise (AssertFailure (enrich_msg msg))
801 | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))