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 Lazy.t;;
29 exception Uncertain of string Lazy.t;;
30 exception AssertFailure of string Lazy.t;;
32 let debug_print = fun _ -> ()
34 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
35 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
36 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
37 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
39 let type_of_aux' metasenv subst context term ugraph =
42 CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph
44 CicTypeChecker.TypeCheckerFailure msg ->
48 "Kernel Type checking error:
49 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
50 (CicMetaSubst.ppterm subst term)
51 (CicMetaSubst.ppterm [] term)
52 (CicMetaSubst.ppcontext subst context)
53 (CicMetaSubst.ppmetasenv subst metasenv)
54 (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
55 raise (AssertFailure msg)
56 in profiler_toa.HExtlib.profile foo ()
60 List.exists (function Cic.Meta _ -> true | _ -> false) l
62 let rec deref subst t =
63 let snd (_,a,_) = a in
68 (CicSubstitution.subst_meta
69 l (snd (CicUtil.lookup_subst n subst)))
71 CicUtil.Subst_not_found _ -> t)
72 | Cic.Appl(Cic.Meta(n,l)::args) ->
73 (match deref subst (Cic.Meta(n,l)) with
74 | Cic.Lambda _ as t ->
75 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
76 | r -> Cic.Appl(r::args))
77 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
78 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
83 let foo () = deref subst t
84 in profiler_deref.HExtlib.profile foo ()
86 exception WrongShape;;
87 let eta_reduce after_beta_expansion after_beta_expansion_body
91 match before_beta_expansion,after_beta_expansion_body with
92 Cic.Appl l, Cic.Appl l' ->
93 let rec all_but_last check_last =
97 | [_] -> if check_last then raise WrongShape else []
98 | he::tl -> he::(all_but_last check_last tl)
100 let all_but_last check_last l =
101 match all_but_last check_last l with
106 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
107 let all_but_last = all_but_last false l in
108 (* here we should test alpha-equivalence; however we know by
109 construction that here alpha_equivalence is equivalent to = *)
110 if t = all_but_last then
114 | _,_ -> after_beta_expansion
116 WrongShape -> after_beta_expansion
118 let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
119 let module S = CicSubstitution in
120 let module C = Cic in
122 let rec aux metasenv subst n context t' ugraph =
125 let subst,metasenv,ugraph1 =
126 fo_unif_subst test_equality_only subst context metasenv
127 (CicSubstitution.lift n arg) t' ugraph
130 subst,metasenv,C.Rel (1 + n),ugraph1
133 | UnificationFailure _ ->
135 | C.Rel m -> subst,metasenv,
136 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
137 | C.Var (uri,exp_named_subst) ->
138 let subst,metasenv,exp_named_subst',ugraph1 =
139 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
141 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
143 (* andrea: in general, beta_expand can create badly typed
144 terms. This happens quite seldom in practice, UNLESS we
145 iterate on the local context. For this reason, we renounce
146 to iterate and just lift *)
150 Some t -> Some (CicSubstitution.lift 1 t)
152 subst, metasenv, C.Meta (i,l), ugraph
154 | C.Implicit _ as t -> subst,metasenv,t,ugraph
156 let subst,metasenv,te',ugraph1 =
157 aux metasenv subst n context te ugraph in
158 let subst,metasenv,ty',ugraph2 =
159 aux metasenv subst n context ty ugraph1 in
160 (* TASSI: sure this is in serial? *)
161 subst,metasenv,(C.Cast (te', ty')),ugraph2
163 let subst,metasenv,s',ugraph1 =
164 aux metasenv subst n context s ugraph in
165 let subst,metasenv,t',ugraph2 =
166 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
169 (* TASSI: sure this is in serial? *)
170 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
171 | C.Lambda (nn,s,t) ->
172 let subst,metasenv,s',ugraph1 =
173 aux metasenv subst n context s ugraph in
174 let subst,metasenv,t',ugraph2 =
175 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
177 (* TASSI: sure this is in serial? *)
178 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
179 | C.LetIn (nn,s,t) ->
180 let subst,metasenv,s',ugraph1 =
181 aux metasenv subst n context s ugraph in
182 let subst,metasenv,t',ugraph2 =
183 aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
186 (* TASSI: sure this is in serial? *)
187 subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
189 let subst,metasenv,revl',ugraph1 =
191 (fun (subst,metasenv,appl,ugraph) t ->
192 let subst,metasenv,t',ugraph1 =
193 aux metasenv subst n context t ugraph in
194 subst,metasenv,(t'::appl),ugraph1
195 ) (subst,metasenv,[],ugraph) l
197 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
198 | C.Const (uri,exp_named_subst) ->
199 let subst,metasenv,exp_named_subst',ugraph1 =
200 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
202 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
203 | C.MutInd (uri,i,exp_named_subst) ->
204 let subst,metasenv,exp_named_subst',ugraph1 =
205 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
207 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
208 | C.MutConstruct (uri,i,j,exp_named_subst) ->
209 let subst,metasenv,exp_named_subst',ugraph1 =
210 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
212 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
213 | C.MutCase (sp,i,outt,t,pl) ->
214 let subst,metasenv,outt',ugraph1 =
215 aux metasenv subst n context outt ugraph in
216 let subst,metasenv,t',ugraph2 =
217 aux metasenv subst n context t ugraph1 in
218 let subst,metasenv,revpl',ugraph3 =
220 (fun (subst,metasenv,pl,ugraph) t ->
221 let subst,metasenv,t',ugraph1 =
222 aux metasenv subst n context t ugraph in
223 subst,metasenv,(t'::pl),ugraph1
224 ) (subst,metasenv,[],ugraph2) pl
226 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
227 (* TASSI: not sure this is serial *)
229 (*CSC: not implemented
230 let tylen = List.length fl in
233 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
236 C.Fix (i, substitutedfl)
238 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
240 (*CSC: not implemented
241 let tylen = List.length fl in
244 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
247 C.CoFix (i, substitutedfl)
250 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
252 and aux_exp_named_subst metasenv subst n context ens ugraph =
254 (fun (uri,t) (subst,metasenv,l,ugraph) ->
255 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
256 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
258 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
260 FreshNamesGenerator.mk_fresh_name ~subst
261 metasenv context (Cic.Name "Hbeta") ~typ:argty
263 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
264 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
265 subst, metasenv, t'', ugraph2
266 in profiler_beta_expand.HExtlib.profile foo ()
269 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
270 let subst,metasenv,hd,ugraph =
272 (fun arg (subst,metasenv,t,ugraph) ->
273 let subst,metasenv,t,ugraph1 =
274 beta_expand test_equality_only
275 metasenv subst context t arg ugraph
277 subst,metasenv,t,ugraph1
278 ) args (subst,metasenv,t,ugraph)
280 subst,metasenv,hd,ugraph
283 (* NUOVA UNIFICAZIONE *)
284 (* A substitution is a (int * Cic.term) list that associates a
285 metavariable i with its body.
286 A metaenv is a (int * Cic.term) list that associate a metavariable
288 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
289 a new substitution which is _NOT_ unwinded. It must be unwinded before
292 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
293 let module C = Cic in
294 let module R = CicReduction in
295 let module S = CicSubstitution in
296 let t1 = deref subst t1 in
297 let t2 = deref subst t2 in
300 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
301 in profiler_are_convertible.HExtlib.profile foo ()
304 subst, metasenv, ugraph
307 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
308 let _,subst,metasenv,ugraph1 =
311 (fun (j,subst,metasenv,ugraph) t1 t2 ->
314 | _,None -> j+1,subst,metasenv,ugraph
315 | Some t1', Some t2' ->
316 (* First possibility: restriction *)
317 (* Second possibility: unification *)
318 (* Third possibility: convertibility *)
321 ~subst ~metasenv context t1' t2' ugraph
324 j+1,subst,metasenv, ugraph1
327 let subst,metasenv,ugraph2 =
330 subst context metasenv t1' t2' ugraph
332 j+1,subst,metasenv,ugraph2
335 | UnificationFailure _ ->
336 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
337 let metasenv, subst =
338 CicMetaSubst.restrict
339 subst [(n,j)] metasenv in
340 j+1,subst,metasenv,ugraph1)
341 ) (1,subst,metasenv,ugraph) ln lm
345 (UnificationFailure (lazy "1"))
348 "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."
349 (CicMetaSubst.ppterm subst t1)
350 (CicMetaSubst.ppterm subst t2))) *)
351 | Invalid_argument _ ->
353 (UnificationFailure (lazy "2")))
356 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
357 (CicMetaSubst.ppterm subst t1)
358 (CicMetaSubst.ppterm subst t2)))) *)
359 in subst,metasenv,ugraph1
360 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
361 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
363 | (t, C.Meta (n,l)) ->
366 C.Meta (n,_), C.Meta (m,_) when n < m -> false
367 | _, C.Meta _ -> false
370 let lower = fun x y -> if swap then y else x in
371 let upper = fun x y -> if swap then x else y in
372 let fo_unif_subst_ordered
373 test_equality_only subst context metasenv m1 m2 ugraph =
374 fo_unif_subst test_equality_only subst context metasenv
375 (lower m1 m2) (upper m1 m2) ugraph
378 let subst,metasenv,ugraph1 =
379 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
382 type_of_aux' metasenv subst context t ugraph
386 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
388 UnificationFailure _ as e -> raise e
389 | Uncertain msg -> raise (UnificationFailure msg)
391 debug_print (lazy "siamo allo huge hack");
392 (* TODO huge hack!!!!
393 * we keep on unifying/refining in the hope that
394 * the problem will be eventually solved.
395 * In the meantime we're breaking a big invariant:
396 * the terms that we are unifying are no longer well
397 * typed in the current context (in the worst case
398 * we could even diverge) *)
399 (subst, metasenv,ugraph)) in
400 let t',metasenv,subst =
402 CicMetaSubst.delift n subst context metasenv l t
404 (CicMetaSubst.MetaSubstFailure msg)->
405 raise (UnificationFailure msg)
406 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
410 C.Sort (C.Type u) when not test_equality_only ->
411 let u' = CicUniv.fresh () in
412 let s = C.Sort (C.Type u') in
414 CicUniv.add_ge (upper u u') (lower u u') ugraph1
419 (* Unifying the types may have already instantiated n. Let's check *)
421 let (_, oldt,_) = CicUtil.lookup_subst n subst in
422 let lifted_oldt = S.subst_meta l oldt in
423 fo_unif_subst_ordered
424 test_equality_only subst context metasenv t lifted_oldt ugraph2
426 CicUtil.Subst_not_found _ ->
427 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
428 let subst = (n, (context, t'',ty)) :: subst in
430 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
431 subst, metasenv, ugraph2
433 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
434 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
435 if UriManager.eq uri1 uri2 then
436 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
437 exp_named_subst1 exp_named_subst2 ugraph
439 raise (UnificationFailure (lazy "3"))
441 "Can't unify %s with %s due to different constants"
442 (CicMetaSubst.ppterm subst t1)
443 (CicMetaSubst.ppterm subst t2))) *)
444 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
445 if UriManager.eq uri1 uri2 && i1 = i2 then
446 fo_unif_subst_exp_named_subst
448 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
450 raise (UnificationFailure (lazy "4"))
452 "Can't unify %s with %s due to different inductive principles"
453 (CicMetaSubst.ppterm subst t1)
454 (CicMetaSubst.ppterm subst t2))) *)
455 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
456 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
457 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
458 fo_unif_subst_exp_named_subst
460 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
462 raise (UnificationFailure (lazy "5"))
464 "Can't unify %s with %s due to different inductive constructors"
465 (CicMetaSubst.ppterm subst t1)
466 (CicMetaSubst.ppterm subst t2))) *)
467 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
468 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
469 subst context metasenv te t2 ugraph
470 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
471 subst context metasenv t1 te ugraph
472 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
473 let subst',metasenv',ugraph1 =
474 fo_unif_subst true subst context metasenv s1 s2 ugraph
476 fo_unif_subst test_equality_only
477 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
478 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
479 let subst',metasenv',ugraph1 =
480 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
482 fo_unif_subst test_equality_only
483 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
484 | (C.LetIn (_,s1,t1), t2)
485 | (t2, C.LetIn (_,s1,t1)) ->
487 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
488 | (C.Appl l1, C.Appl l2) ->
489 (* andrea: this case should be probably rewritten in the
492 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
495 (fun (subst,metasenv,ugraph) t1 t2 ->
497 test_equality_only subst context metasenv t1 t2 ugraph)
498 (subst,metasenv,ugraph) l1 l2
499 with (Invalid_argument msg) ->
500 raise (UnificationFailure (lazy msg)))
501 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
502 (* we verify that none of the args is a Meta,
503 since beta expanding with respoect to a metavariable
507 let (_,t,_) = CicUtil.lookup_subst i subst in
508 let lifted = S.subst_meta l t in
509 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
512 subst context metasenv reduced t2 ugraph
513 with CicUtil.Subst_not_found _ -> *)
514 let subst,metasenv,beta_expanded,ugraph1 =
516 test_equality_only metasenv subst context t2 args ugraph
518 fo_unif_subst test_equality_only subst context metasenv
519 (C.Meta (i,l)) beta_expanded ugraph1
520 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
522 let (_,t,_) = CicUtil.lookup_subst i subst in
523 let lifted = S.subst_meta l t in
524 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
527 subst context metasenv t1 reduced ugraph
528 with CicUtil.Subst_not_found _ -> *)
529 let subst,metasenv,beta_expanded,ugraph1 =
532 metasenv subst context t1 args ugraph
534 fo_unif_subst test_equality_only subst context metasenv
535 (C.Meta (i,l)) beta_expanded ugraph1
537 let lr1 = List.rev l1 in
538 let lr2 = List.rev l2 in
540 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
543 | _,[] -> assert false
546 test_equality_only subst context metasenv h1 h2 ugraph
549 fo_unif_subst test_equality_only subst context metasenv
550 h (C.Appl (List.rev l)) ugraph
551 | ((h1::l1),(h2::l2)) ->
552 let subst', metasenv',ugraph1 =
555 subst context metasenv h1 h2 ugraph
558 test_equality_only subst' metasenv' (l1,l2) ugraph1
561 test_equality_only subst metasenv (lr1, lr2) ugraph)
562 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
563 let subst', metasenv',ugraph1 =
564 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
566 let subst'',metasenv'',ugraph2 =
567 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
571 (fun (subst,metasenv,ugraph) t1 t2 ->
573 test_equality_only subst context metasenv t1 t2 ugraph
574 ) (subst'',metasenv'',ugraph2) pl1 pl2
576 Invalid_argument _ ->
577 raise (UnificationFailure (lazy "6.1")))
579 "Error trying to unify %s with %s: the number of branches is not the same."
580 (CicMetaSubst.ppterm subst t1)
581 (CicMetaSubst.ppterm subst t2)))) *)
582 | (C.Rel _, _) | (_, C.Rel _) ->
584 subst, metasenv,ugraph
586 raise (UnificationFailure (lazy "6.2"))
588 "Can't unify %s with %s because they are not convertible"
589 (CicMetaSubst.ppterm subst t1)
590 (CicMetaSubst.ppterm subst t2))) *)
591 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
592 let subst,metasenv,beta_expanded,ugraph1 =
594 test_equality_only metasenv subst context t2 args ugraph
596 fo_unif_subst test_equality_only subst context metasenv
597 (C.Meta (i,l)) beta_expanded ugraph1
598 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
599 let subst,metasenv,beta_expanded,ugraph1 =
601 test_equality_only metasenv subst context t1 args ugraph
603 fo_unif_subst test_equality_only subst context metasenv
604 beta_expanded (C.Meta (i,l)) ugraph1
605 | (C.Sort _ ,_) | (_, C.Sort _)
606 | (C.Const _, _) | (_, C.Const _)
607 | (C.MutInd _, _) | (_, C.MutInd _)
608 | (C.MutConstruct _, _) | (_, C.MutConstruct _)
609 | (C.Fix _, _) | (_, C.Fix _)
610 | (C.CoFix _, _) | (_, C.CoFix _) ->
612 subst, metasenv, ugraph
615 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
618 subst, metasenv, ugraph1
621 (UnificationFailure (lazy (sprintf
622 "Can't unify %s with %s because they are not convertible"
623 (CicMetaSubst.ppterm subst t1)
624 (CicMetaSubst.ppterm subst t2))))
626 let t2' = R.whd ~subst context t2 in
629 fo_unif_subst test_equality_only
630 subst context metasenv t1 t2' ugraph
631 | _ -> raise (UnificationFailure (lazy "8")))
633 let t1' = R.whd ~subst context t1 in
636 fo_unif_subst test_equality_only
637 subst context metasenv t1' t2 ugraph
638 | _ -> (* raise (UnificationFailure "9")) *)
640 (UnificationFailure (lazy (sprintf
641 "Can't unify %s with %s because they are not convertible"
642 (CicMetaSubst.ppterm subst t1)
643 (CicMetaSubst.ppterm subst t2)))))
645 raise (UnificationFailure (lazy "10"))
647 "Can't unify %s with %s because they are not convertible"
648 (CicMetaSubst.ppterm subst t1)
649 (CicMetaSubst.ppterm subst t2))) *)
651 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
652 exp_named_subst1 exp_named_subst2 ugraph
656 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
658 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
659 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
661 Invalid_argument _ ->
666 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
669 raise (UnificationFailure (lazy (sprintf
670 "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))))
672 (* A substitution is a (int * Cic.term) list that associates a *)
673 (* metavariable i with its body. *)
674 (* metasenv is of type Cic.metasenv *)
675 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
676 (* a new substitution which is already unwinded and ready to be applied and *)
677 (* a new metasenv in which some hypothesis in the contexts of the *)
678 (* metavariables may have been restricted. *)
679 let fo_unif metasenv context t1 t2 ugraph =
680 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
682 let enrich_msg msg subst context metasenv t1 t2 ugraph =
684 (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"
685 (CicMetaSubst.ppterm subst t1)
687 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
689 with _ -> "MALFORMED")
690 (CicMetaSubst.ppterm subst t2)
692 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
694 with _ -> "MALFORMED")
695 (CicMetaSubst.ppcontext subst context)
696 (CicMetaSubst.ppmetasenv subst metasenv)
697 (CicMetaSubst.ppsubst subst) (Lazy.force msg))
699 let fo_unif_subst subst context metasenv t1 t2 ugraph =
701 fo_unif_subst false subst context metasenv t1 t2 ugraph
703 | AssertFailure msg ->
704 raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
705 | UnificationFailure msg ->
706 raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))