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);;
52 CicMetaSubst.type_of_aux' metasenv subst context term ugraph
54 | CicMetaSubst.MetaSubstFailure msg ->
57 "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"
58 (CicMetaSubst.ppterm subst term)
59 (CicMetaSubst.ppcontext subst context)
60 (CicMetaSubst.ppmetasenv metasenv subst) msg))) *)
63 let snd (_,a,_) = a in
68 (CicSubstitution.lift_meta
69 l (snd (CicUtil.lookup_subst n subst)))
71 CicUtil.Subst_not_found _ -> t)
75 let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
76 let module S = CicSubstitution in
78 let rec aux metasenv subst n context t' ugraph =
81 let subst,metasenv,ugraph1 =
82 fo_unif_subst test_equality_only subst context metasenv
83 (CicSubstitution.lift n arg) t' ugraph
86 subst,metasenv,C.Rel (1 + n),ugraph1
89 | UnificationFailure _ ->
91 | C.Rel m -> subst,metasenv,
92 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
93 | C.Var (uri,exp_named_subst) ->
94 let subst,metasenv,exp_named_subst',ugraph1 =
95 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
97 (* THIS WAS BEFORE ----
98 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
101 let (_, t') = CicMetaSubst.lookup_subst i subst in
102 aux metasenv subst n context (CicSubstitution.lift_meta l t')
104 with CicMetaSubst.SubstNotFound _ ->
105 let (subst, metasenv, context, local_context,ugraph1) =
107 (fun (subst, metasenv, context, local_context,ugraph) t ->
110 (subst, metasenv, context, None::local_context, ugraph)
112 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
114 (* andrea: in general, beta_expand can create badly typed
115 terms. This happens quite seldom in practice, UNLESS we
116 iterate on the local context. For this reason, we renounce
117 to iterate and just lift *)
121 Some t -> Some (CicSubstitution.lift 1 t)
123 subst, metasenv, C.Meta (i,l), ugraph
125 let (subst, metasenv, context, local_context) =
127 (fun t (subst, metasenv, context, local_context) ->
129 | None -> (subst, metasenv, context, None :: local_context)
132 let (subst, metasenv, t, ugraph1) =
133 aux metasenv subst n context t ugraph
135 (* THIS WAS BEFORE ----
136 (subst, metasenv, context,
137 (Some t)::local_context,ugraph1))
138 (subst, metasenv, context, [],ugraph) l
140 (subst, metasenv,(C.Meta (i, local_context)),ugraph1))
142 (subst, metasenv, context, Some t :: local_context))
143 l (subst, metasenv, context, [])
145 prerr_endline ("nuova meta :" ^ (CicPp.ppterm (C.Meta (i, local_context))));
146 (subst, metasenv, C.Meta (i, local_context)) *)
148 | C.Implicit _ as t -> subst,metasenv,t,ugraph
150 let subst,metasenv,te',ugraph1 =
151 aux metasenv subst n context te ugraph in
152 let subst,metasenv,ty',ugraph2 =
153 aux metasenv subst n context ty ugraph1 in
154 (* TASSI: sure this is in serial? *)
155 subst,metasenv,(C.Cast (te', ty')),ugraph2
157 let subst,metasenv,s',ugraph1 =
158 aux metasenv subst n context s ugraph in
159 let subst,metasenv,t',ugraph2 =
160 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
163 (* TASSI: sure this is in serial? *)
164 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
165 | C.Lambda (nn,s,t) ->
166 let subst,metasenv,s',ugraph1 =
167 aux metasenv subst n context s ugraph in
168 let subst,metasenv,t',ugraph2 =
169 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
171 (* TASSI: sure this is in serial? *)
172 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
173 | C.LetIn (nn,s,t) ->
174 let subst,metasenv,s',ugraph1 =
175 aux metasenv subst n context s ugraph in
176 let subst,metasenv,t',ugraph2 =
177 aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
180 (* TASSI: sure this is in serial? *)
181 subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
183 let subst,metasenv,revl',ugraph1 =
185 (fun (subst,metasenv,appl,ugraph) t ->
186 let subst,metasenv,t',ugraph1 =
187 aux metasenv subst n context t ugraph in
188 subst,metasenv,(t'::appl),ugraph1
189 ) (subst,metasenv,[],ugraph) l
191 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
192 | C.Const (uri,exp_named_subst) ->
193 let subst,metasenv,exp_named_subst',ugraph1 =
194 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
196 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
197 | C.MutInd (uri,i,exp_named_subst) ->
198 let subst,metasenv,exp_named_subst',ugraph1 =
199 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
201 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
202 | C.MutConstruct (uri,i,j,exp_named_subst) ->
203 let subst,metasenv,exp_named_subst',ugraph1 =
204 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
206 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
207 | C.MutCase (sp,i,outt,t,pl) ->
208 let subst,metasenv,outt',ugraph1 =
209 aux metasenv subst n context outt ugraph in
210 let subst,metasenv,t',ugraph2 =
211 aux metasenv subst n context t ugraph1 in
212 let subst,metasenv,revpl',ugraph3 =
214 (fun (subst,metasenv,pl,ugraph) t ->
215 let subst,metasenv,t',ugraph1 =
216 aux metasenv subst n context t ugraph in
217 subst,metasenv,(t'::pl),ugraph1
218 ) (subst,metasenv,[],ugraph2) pl
220 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
221 (* TASSI: not sure this is serial *)
223 (*CSC: not implemented
224 let tylen = List.length fl in
227 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
230 C.Fix (i, substitutedfl)
232 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
234 (*CSC: not implemented
235 let tylen = List.length fl in
238 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
241 C.CoFix (i, substitutedfl)
244 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
246 and aux_exp_named_subst metasenv subst n context ens ugraph =
248 (fun (uri,t) (subst,metasenv,l,ugraph) ->
249 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
250 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
252 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
254 FreshNamesGenerator.mk_fresh_name ~subst
255 metasenv context (Cic.Name "Heta") ~typ:argty
257 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
260 subst, metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
262 subst, metasenv, C.Lambda (fresh_name,argty,t'), ugraph2
266 and beta_expand_many test_equality_only metasenv subst context t l ugraph =
268 (fun (subst,metasenv,t,ugraph) arg ->
269 beta_expand test_equality_only metasenv subst context t arg ugraph
270 ) (subst,metasenv,t,ugraph) l
272 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
273 let subst,metasenv,hd,ugraph =
275 (fun arg (subst,metasenv,t,ugraph) ->
276 let subst,metasenv,t,ugraph1 =
277 beta_expand test_equality_only
278 metasenv subst context t arg ugraph
280 subst,metasenv,t,ugraph1
281 ) args (subst,metasenv,t,ugraph)
283 subst,metasenv,hd,ugraph
286 (* NUOVA UNIFICAZIONE *)
287 (* A substitution is a (int * Cic.term) list that associates a
288 metavariable i with its body.
289 A metaenv is a (int * Cic.term) list that associate a metavariable
291 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
292 a new substitution which is _NOT_ unwinded. It must be unwinded before
295 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
296 let module C = Cic in
297 let module R = CicReduction in
298 let module S = CicSubstitution in
299 let t1 = deref subst t1 in
300 let t2 = deref subst t2 in
302 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
305 subst, metasenv, ugraph
308 (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
310 let ok,subst,metasenv,ugraph1 =
313 (fun (b,subst,metasenv,ugraph) t1 t2 ->
314 if b then true,subst,metasenv,ugraph else
317 | _,None -> true,subst,metasenv,ugraph
318 | Some t1', Some t2' ->
319 (* First possibility: restriction *)
320 (* Second possibility: unification *)
321 (* Third possibility: convertibility *)
323 R.are_convertible subst context t1' t2' ugraph in
325 true,subst,metasenv,ugraph1
328 let subst,metasenv,ugraph2 =
330 (* TASSI: is this another try that should use ugraph? *)
331 test_equality_only subst context metasenv t1' t2' ugraph
333 true,subst,metasenv,ugraph2
335 Not_found -> false,subst,metasenv,ugraph1)
336 ) (true,subst,metasenv,ugraph) ln lm
338 Invalid_argument _ ->
339 raise (UnificationFailure (sprintf
340 "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)))
343 subst,metasenv,ugraph1
345 raise (UnificationFailure (sprintf
346 "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."
347 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
349 let _,subst,metasenv,ugraph1 =
352 (fun (j,subst,metasenv,ugraph) t1 t2 ->
355 | _,None -> j+1,subst,metasenv,ugraph
356 | Some t1', Some t2' ->
357 (* First possibility: restriction *)
358 (* Second possibility: unification *)
359 (* Third possibility: convertibility *)
362 ~subst ~metasenv context t1' t2' ugraph
365 j+1,subst,metasenv, ugraph1
368 let subst,metasenv,ugraph2 =
371 subst context metasenv t1' t2' ugraph
373 j+1,subst,metasenv,ugraph2
376 | UnificationFailure _ ->
377 prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j));
378 let metasenv, subst =
379 CicMetaSubst.restrict
380 subst [(n,j)] metasenv in
381 j+1,subst,metasenv,ugraph1)
382 ) (1,subst,metasenv,ugraph) ln lm
386 (UnificationFailure "1")
389 "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."
390 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
391 | Invalid_argument _ ->
393 (UnificationFailure "2"))
396 "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))))*)
397 in subst,metasenv,ugraph1
399 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
400 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
402 | (t, C.Meta (n,l)) ->
405 C.Meta (n,_), C.Meta (m,_) when n < m -> false
406 | _, C.Meta _ -> false
409 let lower = fun x y -> if swap then y else x in
410 let upper = fun x y -> if swap then x else y in
411 let fo_unif_subst_ordered
412 test_equality_only subst context metasenv m1 m2 ugraph =
413 fo_unif_subst test_equality_only subst context metasenv
414 (lower m1 m2) (upper m1 m2) ugraph
419 let (_, oldt) = CicMetaSubst.lookup_subst n subst in
420 let lifted_oldt = S.lift_meta l oldt in
421 let ty_lifted_oldt,ugraph1 =
422 type_of_aux' metasenv subst context lifted_oldt ugraph
424 let tyt,ugraph2 = type_of_aux' metasenv subst context t ugraph1 in
425 let (subst, metasenv, ugraph3) =
426 fo_unif_subst_ordered test_equality_only subst context metasenv
427 tyt ty_lifted_oldt ugraph2
429 fo_unif_subst_ordered
430 test_equality_only subst context metasenv t lifted_oldt ugraph3
431 with CicMetaSubst.SubstNotFound _ ->
432 (* First of all we unify the type of the meta with the type of the term *)
433 let subst,metasenv,ugraph1 =
434 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
436 let tyt,ugraph1 = type_of_aux' metasenv subst context t ugraph in
439 subst context metasenv tyt (S.lift_meta l meta_type) ugraph1
440 with AssertFailure _ ->
441 (* TODO huge hack!!!!
442 * we keep on unifying/refining in the hope that the problem will be
443 * eventually solved. In the meantime we're breaking a big invariant:
444 * the terms that we are unifying are no longer well typed in the
445 * current context (in the worst case we could even diverge)
448 prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
449 prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
451 (subst, metasenv,ugraph))
453 let t',metasenv,subst =
455 (* TASSI: I hope delift does nothing with universes *)
456 CicMetaSubst.delift n subst context metasenv l t
458 (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
459 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
463 C.Sort (C.Type u) when not test_equality_only ->
464 let u' = CicUniv.fresh () in
465 let s = C.Sort (C.Type u') in
467 CicUniv.add_ge (upper u u') (lower u u') ugraph1 in
471 (* Unifying the types may have already instantiated n. Let's check *)
473 let (_, oldt) = CicMetaSubst.lookup_subst n subst in
474 let lifted_oldt = S.lift_meta l oldt in
475 fo_unif_subst_ordered
476 test_equality_only subst context metasenv t lifted_oldt ugraph2
478 CicMetaSubst.SubstNotFound _ ->
479 let (_, context, _) = CicUtil.lookup_meta n metasenv in
480 let subst = (n, (context, t'')) :: subst in
482 (* CicMetaSubst.apply_subst_metasenv [n,(context, t'')] metasenv *)
483 CicMetaSubst.apply_subst_metasenv subst metasenv
485 subst, metasenv,ugraph2
486 (* (n,t'')::subst, metasenv *)
490 let subst,metasenv,ugraph1 =
491 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
494 type_of_aux' metasenv subst context t ugraph
498 subst context metasenv tyt (S.lift_meta l meta_type) ugraph1
500 UnificationFailure msg
502 prerr_endline msg;raise (UnificationFailure msg)
504 prerr_endline "siamo allo huge hack";
505 (* TODO huge hack!!!!
506 * we keep on unifying/refining in the hope that
507 * the problem will be eventually solved.
508 * In the meantime we're breaking a big invariant:
509 * the terms that we are unifying are no longer well
510 * typed in the current context (in the worst case
511 * we could even diverge) *)
512 (subst, metasenv,ugraph)) in
513 let t',metasenv,subst =
515 CicMetaSubst.delift n subst context metasenv l t
517 (CicMetaSubst.MetaSubstFailure msg)->
518 raise (UnificationFailure msg)
519 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
523 C.Sort (C.Type u) when not test_equality_only ->
524 let u' = CicUniv.fresh () in
525 let s = C.Sort (C.Type u') in
527 CicUniv.add_ge (upper u u') (lower u u') ugraph1
532 (* Unifying the types may have already instantiated n. Let's check *)
534 let (_, oldt,_) = CicUtil.lookup_subst n subst in
535 let lifted_oldt = S.lift_meta l oldt in
536 fo_unif_subst_ordered
537 test_equality_only subst context metasenv t lifted_oldt ugraph2
539 CicUtil.Subst_not_found _ ->
540 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
541 let subst = (n, (context, t'',ty)) :: subst in
543 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
544 subst, metasenv, ugraph2
547 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
548 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
549 if UriManager.eq uri1 uri2 then
550 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
551 exp_named_subst1 exp_named_subst2 ugraph
553 raise (UnificationFailure "3")
555 "Can't unify %s with %s due to different constants"
556 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
557 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
558 if UriManager.eq uri1 uri2 && i1 = i2 then
559 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
560 exp_named_subst1 exp_named_subst2 ugraph
562 raise (UnificationFailure "4")
564 "Can't unify %s with %s due to different inductive principles"
565 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
566 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
567 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
568 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
569 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
570 exp_named_subst1 exp_named_subst2 ugraph
572 raise (UnificationFailure "5")
574 "Can't unify %s with %s due to different inductive constructors"
575 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
576 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
577 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
578 subst context metasenv te t2 ugraph
579 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
580 subst context metasenv t1 te ugraph
581 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
582 let subst',metasenv',ugraph1 =
583 fo_unif_subst true subst context metasenv s1 s2 ugraph
585 fo_unif_subst test_equality_only
586 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
587 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
588 let subst',metasenv',ugraph1 =
589 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
591 fo_unif_subst test_equality_only
592 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
593 | (C.LetIn (_,s1,t1), t2)
594 | (t2, C.LetIn (_,s1,t1)) ->
596 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
597 | (C.Appl l1, C.Appl l2) ->
598 (* WAS BEFORE ----------
599 let subst,metasenv,t1',t2',ugraph1 =
601 C.Meta (i,_)::_, C.Meta (j,_)::_ when i = j ->
602 subst,metasenv,t1,t2,ugraph
603 (* In the first two cases when we reach the next begin ... end
604 section useless work is done since, by construction, the list
605 of arguments will be equal.
608 (* andrea: this case should be probably rewritten in the
610 let rec beta_reduce =
612 (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
613 let he'' = CicSubstitution.subst he' t in
617 beta_reduce (Cic.Appl(he''::tl'))
620 (* andrea : this was too powerful. It works very bad with f_equal and
621 similar terms, try and see
622 C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
625 (fun (subst,metasenv) ->
626 fo_unif_subst test_equality_only subst context metasenv)
627 (subst,metasenv) l1 l2
628 with (Invalid_argument msg) -> raise (UnificationFailure msg))
629 | C.Meta (i,l)::args, _ ->
630 <<<<<<< cicUnification.ml
631 let subst,metasenv,t2',ugraph1 =
632 beta_expand_many test_equality_only metasenv subst context t2 args
635 subst,metasenv,t1,t2',ugraph1
638 let (_,t,_) = CicUtil.lookup_subst i subst in
639 let lifted = S.lift_meta l t in
640 let reduced = beta_reduce (Cic.Appl (lifted::args)) in
643 subst context metasenv reduced t2
644 with CicUtil.Subst_not_found _ ->
645 let subst,metasenv,beta_expanded =
647 test_equality_only metasenv subst context t2 args in
648 fo_unif_subst test_equality_only subst context metasenv
649 (C.Meta (i,l)) beta_expanded)
651 | _, C.Meta (i,l)::args ->
652 <<<<<<< cicUnification.ml
653 let subst,metasenv,t1',ugraph1 =
654 beta_expand_many test_equality_only metasenv subst context t1 args
657 subst,metasenv,t1',t2,ugraph1
660 let (_,t,_) = CicUtil.lookup_subst i subst in
661 let lifted = S.lift_meta l t in
662 let reduced = beta_reduce (Cic.Appl (lifted::args)) in
665 subst context metasenv t1 reduced
666 with CicUtil.Subst_not_found _ ->
667 let subst,metasenv,beta_expanded =
669 test_equality_only metasenv subst context t1 args in
670 fo_unif_subst test_equality_only subst context metasenv
671 (C.Meta (i,l)) beta_expanded)
676 <<<<<<< cicUnification.ml
677 subst,metasenv,t1,t2,ugraph
681 C.Appl l1, C.Appl l2 ->
682 let lr1 = List.rev l1 in
685 let lr1 = List.rev l1 in
686 let lr2 = List.rev l2 in
688 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
691 | _,[] -> assert false
694 test_equality_only subst context metasenv h1 h2 ugraph
697 fo_unif_subst test_equality_only subst context metasenv
698 h (C.Appl (List.rev l)) ugraph
699 | ((h1::l1),(h2::l2)) ->
700 let subst', metasenv',ugraph1 =
702 test_equality_only subst context metasenv h1 h2 ugraph
705 test_equality_only subst' metasenv' (l1,l2) ugraph1
708 test_equality_only subst metasenv (lr1, lr2) ) ugraph(*1*)
709 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
710 let subst', metasenv',ugraph1 =
711 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
713 let subst'',metasenv'',ugraph2 =
714 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
718 (fun (subst,metasenv,ugraph) t1 t2 ->
720 test_equality_only subst context metasenv t1 t2 ugraph
721 ) (subst'',metasenv'',ugraph2) pl1 pl2
723 Invalid_argument _ ->
724 raise (UnificationFailure "6"))
726 "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))) *)
727 | (C.Rel _, _) | (_, C.Rel _) ->
729 subst, metasenv,ugraph
731 raise (UnificationFailure "6")
733 "Can't unify %s with %s because they are not convertible"
734 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
735 | (C.Sort _ ,_) | (_, C.Sort _)
736 | (C.Const _, _) | (_, C.Const _)
737 | (C.MutInd _, _) | (_, C.MutInd _)
738 | (C.MutConstruct _, _) | (_, C.MutConstruct _)
739 | (C.Fix _, _) | (_, C.Fix _)
740 | (C.CoFix _, _) | (_, C.CoFix _) ->
742 subst, metasenv, ugraph
745 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
748 subst, metasenv, ugraph1
750 raise (UnificationFailure "7")
752 "Can't unify %s with %s because they are not convertible"
753 (CicMetaSubst.ppterm subst t1)
754 (CicMetaSubst.ppterm subst t2))) *)
757 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
760 subst, metasenv, ugraph1
762 raise (UnificationFailure "8")
764 "Can't unify %s with %s because they are not convertible"
765 (CicMetaSubst.ppterm subst t1)
766 (CicMetaSubst.ppterm subst t2))) *)
768 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
769 exp_named_subst1 exp_named_subst2 ugraph
773 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
775 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
776 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
778 Invalid_argument _ ->
783 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
786 raise (UnificationFailure (sprintf
787 "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)))
789 (* A substitution is a (int * Cic.term) list that associates a *)
790 (* metavariable i with its body. *)
791 (* metasenv is of type Cic.metasenv *)
792 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
793 (* a new substitution which is already unwinded and ready to be applied and *)
794 (* a new metasenv in which some hypothesis in the contexts of the *)
795 (* metavariables may have been restricted. *)
796 let fo_unif metasenv context t1 t2 ugraph =
797 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
799 let fo_unif_subst subst context metasenv t1 t2 ugraph =
800 let enrich_msg msg = (* "bella roba" *)
801 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"
802 (CicMetaSubst.ppterm subst t1)
804 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
806 with _ -> "MALFORMED")
807 (CicMetaSubst.ppterm subst t2)
809 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
811 with _ -> "MALFORMED")
812 (CicMetaSubst.ppcontext subst context)
813 (CicMetaSubst.ppmetasenv metasenv subst)
814 (CicMetaSubst.ppsubst subst) msg
817 fo_unif_subst false subst context metasenv t1 t2 ugraph
819 | AssertFailure msg -> raise (AssertFailure (enrich_msg msg))
820 | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))