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/.
30 | Enriched of string * Cic.substitution * Cic.context * Cic.metasenv *
31 Cic.term * Cic.term * CicUniv.universe_graph
33 let failure_msg_of_string msg = Reason msg
35 exception UnificationFailure of failure_msg;;
36 exception Uncertain of string;;
37 exception AssertFailure of failure_msg;;
39 let debug_print = fun _ -> ()
41 let type_of_aux' metasenv subst context term ugraph =
43 CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph
45 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) msg) in
55 raise (AssertFailure (Reason msg));;
58 List.exists (function Cic.Meta _ -> true | _ -> false) l
60 let rec deref subst t =
61 let snd (_,a,_) = a in
66 (CicSubstitution.subst_meta
67 l (snd (CicUtil.lookup_subst n subst)))
69 CicUtil.Subst_not_found _ -> t)
70 | Cic.Appl(Cic.Meta(n,l)::args) ->
71 (match deref subst (Cic.Meta(n,l)) with
72 | Cic.Lambda _ as t ->
73 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
74 | r -> Cic.Appl(r::args))
75 | Cic.Appl(((Cic.Lambda _) as t)::args) ->
76 deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
80 exception WrongShape;;
81 let eta_reduce after_beta_expansion after_beta_expansion_body
85 match before_beta_expansion,after_beta_expansion_body with
86 Cic.Appl l, Cic.Appl l' ->
87 let rec all_but_last check_last =
91 | [_] -> if check_last then raise WrongShape else []
92 | he::tl -> he::(all_but_last check_last tl)
94 let all_but_last check_last l =
95 match all_but_last check_last l with
100 let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
101 let all_but_last = all_but_last false l in
102 (* here we should test alpha-equivalence; however we know by
103 construction that here alpha_equivalence is equivalent to = *)
104 if t = all_but_last then
108 | _,_ -> after_beta_expansion
110 WrongShape -> after_beta_expansion
112 let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
113 let module S = CicSubstitution in
114 let module C = Cic in
115 let rec aux metasenv subst n context t' ugraph =
118 let subst,metasenv,ugraph1 =
119 fo_unif_subst test_equality_only subst context metasenv
120 (CicSubstitution.lift n arg) t' ugraph
123 subst,metasenv,C.Rel (1 + n),ugraph1
126 | UnificationFailure _ ->
128 | C.Rel m -> subst,metasenv,
129 (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
130 | C.Var (uri,exp_named_subst) ->
131 let subst,metasenv,exp_named_subst',ugraph1 =
132 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
134 subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
136 (* andrea: in general, beta_expand can create badly typed
137 terms. This happens quite seldom in practice, UNLESS we
138 iterate on the local context. For this reason, we renounce
139 to iterate and just lift *)
143 Some t -> Some (CicSubstitution.lift 1 t)
145 subst, metasenv, C.Meta (i,l), ugraph
147 | C.Implicit _ as t -> subst,metasenv,t,ugraph
149 let subst,metasenv,te',ugraph1 =
150 aux metasenv subst n context te ugraph in
151 let subst,metasenv,ty',ugraph2 =
152 aux metasenv subst n context ty ugraph1 in
153 (* TASSI: sure this is in serial? *)
154 subst,metasenv,(C.Cast (te', ty')),ugraph2
156 let subst,metasenv,s',ugraph1 =
157 aux metasenv subst n context s ugraph in
158 let subst,metasenv,t',ugraph2 =
159 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
162 (* TASSI: sure this is in serial? *)
163 subst,metasenv,(C.Prod (nn, s', t')),ugraph2
164 | C.Lambda (nn,s,t) ->
165 let subst,metasenv,s',ugraph1 =
166 aux metasenv subst n context s ugraph in
167 let subst,metasenv,t',ugraph2 =
168 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
170 (* TASSI: sure this is in serial? *)
171 subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
172 | C.LetIn (nn,s,t) ->
173 let subst,metasenv,s',ugraph1 =
174 aux metasenv subst n context s ugraph in
175 let subst,metasenv,t',ugraph2 =
176 aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
179 (* TASSI: sure this is in serial? *)
180 subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
182 let subst,metasenv,revl',ugraph1 =
184 (fun (subst,metasenv,appl,ugraph) t ->
185 let subst,metasenv,t',ugraph1 =
186 aux metasenv subst n context t ugraph in
187 subst,metasenv,(t'::appl),ugraph1
188 ) (subst,metasenv,[],ugraph) l
190 subst,metasenv,(C.Appl (List.rev revl')),ugraph1
191 | C.Const (uri,exp_named_subst) ->
192 let subst,metasenv,exp_named_subst',ugraph1 =
193 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
195 subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
196 | C.MutInd (uri,i,exp_named_subst) ->
197 let subst,metasenv,exp_named_subst',ugraph1 =
198 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
200 subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
201 | C.MutConstruct (uri,i,j,exp_named_subst) ->
202 let subst,metasenv,exp_named_subst',ugraph1 =
203 aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
205 subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
206 | C.MutCase (sp,i,outt,t,pl) ->
207 let subst,metasenv,outt',ugraph1 =
208 aux metasenv subst n context outt ugraph in
209 let subst,metasenv,t',ugraph2 =
210 aux metasenv subst n context t ugraph1 in
211 let subst,metasenv,revpl',ugraph3 =
213 (fun (subst,metasenv,pl,ugraph) t ->
214 let subst,metasenv,t',ugraph1 =
215 aux metasenv subst n context t ugraph in
216 subst,metasenv,(t'::pl),ugraph1
217 ) (subst,metasenv,[],ugraph2) pl
219 subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
220 (* TASSI: not sure this is serial *)
222 (*CSC: not implemented
223 let tylen = List.length fl in
226 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
229 C.Fix (i, substitutedfl)
231 subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
233 (*CSC: not implemented
234 let tylen = List.length fl in
237 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
240 C.CoFix (i, substitutedfl)
243 subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
245 and aux_exp_named_subst metasenv subst n context ens ugraph =
247 (fun (uri,t) (subst,metasenv,l,ugraph) ->
248 let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
249 subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
251 let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
253 FreshNamesGenerator.mk_fresh_name ~subst
254 metasenv context (Cic.Name "Hbeta") ~typ:argty
256 let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
257 let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
258 subst, metasenv, t'', ugraph2
261 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
262 let subst,metasenv,hd,ugraph =
264 (fun arg (subst,metasenv,t,ugraph) ->
265 let subst,metasenv,t,ugraph1 =
266 beta_expand test_equality_only
267 metasenv subst context t arg ugraph
269 subst,metasenv,t,ugraph1
270 ) args (subst,metasenv,t,ugraph)
272 subst,metasenv,hd,ugraph
275 (* NUOVA UNIFICAZIONE *)
276 (* A substitution is a (int * Cic.term) list that associates a
277 metavariable i with its body.
278 A metaenv is a (int * Cic.term) list that associate a metavariable
280 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
281 a new substitution which is _NOT_ unwinded. It must be unwinded before
284 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
285 let module C = Cic in
286 let module R = CicReduction in
287 let module S = CicSubstitution in
288 let t1 = deref subst t1 in
289 let t2 = deref subst t2 in
291 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
294 subst, metasenv, ugraph
297 | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
298 let _,subst,metasenv,ugraph1 =
301 (fun (j,subst,metasenv,ugraph) t1 t2 ->
304 | _,None -> j+1,subst,metasenv,ugraph
305 | Some t1', Some t2' ->
306 (* First possibility: restriction *)
307 (* Second possibility: unification *)
308 (* Third possibility: convertibility *)
311 ~subst ~metasenv context t1' t2' ugraph
314 j+1,subst,metasenv, ugraph1
317 let subst,metasenv,ugraph2 =
320 subst context metasenv t1' t2' ugraph
322 j+1,subst,metasenv,ugraph2
325 | UnificationFailure _ ->
326 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
327 let metasenv, subst =
328 CicMetaSubst.restrict
329 subst [(n,j)] metasenv in
330 j+1,subst,metasenv,ugraph1)
331 ) (1,subst,metasenv,ugraph) ln lm
335 (UnificationFailure (Reason "1"))
338 "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."
339 (CicMetaSubst.ppterm subst t1)
340 (CicMetaSubst.ppterm subst t2))) *)
341 | Invalid_argument _ ->
343 (UnificationFailure (Reason "2")))
346 "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
347 (CicMetaSubst.ppterm subst t1)
348 (CicMetaSubst.ppterm subst t2)))) *)
349 in subst,metasenv,ugraph1
350 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
351 fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
353 | (t, C.Meta (n,l)) ->
356 C.Meta (n,_), C.Meta (m,_) when n < m -> false
357 | _, C.Meta _ -> false
360 let lower = fun x y -> if swap then y else x in
361 let upper = fun x y -> if swap then x else y in
362 let fo_unif_subst_ordered
363 test_equality_only subst context metasenv m1 m2 ugraph =
364 fo_unif_subst test_equality_only subst context metasenv
365 (lower m1 m2) (upper m1 m2) ugraph
368 let subst,metasenv,ugraph1 =
369 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
372 type_of_aux' metasenv subst context t ugraph
376 subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
378 UnificationFailure msg ->raise (UnificationFailure msg)
379 | Uncertain msg -> raise (UnificationFailure (Reason msg))
381 debug_print (lazy "siamo allo huge hack");
382 (* TODO huge hack!!!!
383 * we keep on unifying/refining in the hope that
384 * the problem will be eventually solved.
385 * In the meantime we're breaking a big invariant:
386 * the terms that we are unifying are no longer well
387 * typed in the current context (in the worst case
388 * we could even diverge) *)
389 (subst, metasenv,ugraph)) in
390 let t',metasenv,subst =
392 CicMetaSubst.delift n subst context metasenv l t
394 (CicMetaSubst.MetaSubstFailure msg)->
395 raise (UnificationFailure (Reason msg))
396 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
400 C.Sort (C.Type u) when not test_equality_only ->
401 let u' = CicUniv.fresh () in
402 let s = C.Sort (C.Type u') in
404 CicUniv.add_ge (upper u u') (lower u u') ugraph1
409 (* Unifying the types may have already instantiated n. Let's check *)
411 let (_, oldt,_) = CicUtil.lookup_subst n subst in
412 let lifted_oldt = S.subst_meta l oldt in
413 fo_unif_subst_ordered
414 test_equality_only subst context metasenv t lifted_oldt ugraph2
416 CicUtil.Subst_not_found _ ->
417 let (_, context, ty) = CicUtil.lookup_meta n metasenv in
418 let subst = (n, (context, t'',ty)) :: subst in
420 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
421 subst, metasenv, ugraph2
423 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
424 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
425 if UriManager.eq uri1 uri2 then
426 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
427 exp_named_subst1 exp_named_subst2 ugraph
429 raise (UnificationFailure (Reason "3"))
431 "Can't unify %s with %s due to different constants"
432 (CicMetaSubst.ppterm subst t1)
433 (CicMetaSubst.ppterm subst t2))) *)
434 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
435 if UriManager.eq uri1 uri2 && i1 = i2 then
436 fo_unif_subst_exp_named_subst
438 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
440 raise (UnificationFailure (Reason "4"))
442 "Can't unify %s with %s due to different inductive principles"
443 (CicMetaSubst.ppterm subst t1)
444 (CicMetaSubst.ppterm subst t2))) *)
445 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
446 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
447 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
448 fo_unif_subst_exp_named_subst
450 subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
452 raise (UnificationFailure (Reason "5"))
454 "Can't unify %s with %s due to different inductive constructors"
455 (CicMetaSubst.ppterm subst t1)
456 (CicMetaSubst.ppterm subst t2))) *)
457 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
458 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
459 subst context metasenv te t2 ugraph
460 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
461 subst context metasenv t1 te ugraph
462 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
463 let subst',metasenv',ugraph1 =
464 fo_unif_subst true subst context metasenv s1 s2 ugraph
466 fo_unif_subst test_equality_only
467 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
468 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
469 let subst',metasenv',ugraph1 =
470 fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
472 fo_unif_subst test_equality_only
473 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
474 | (C.LetIn (_,s1,t1), t2)
475 | (t2, C.LetIn (_,s1,t1)) ->
477 test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
478 | (C.Appl l1, C.Appl l2) ->
479 (* andrea: this case should be probably rewritten in the
482 | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
485 (fun (subst,metasenv,ugraph) t1 t2 ->
487 test_equality_only subst context metasenv t1 t2 ugraph)
488 (subst,metasenv,ugraph) l1 l2
489 with (Invalid_argument msg) ->
490 raise (UnificationFailure (Reason msg)))
491 | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
492 (* we verify that none of the args is a Meta,
493 since beta expanding with respoect to a metavariable
497 let (_,t,_) = CicUtil.lookup_subst i subst in
498 let lifted = S.subst_meta l t in
499 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
502 subst context metasenv reduced t2 ugraph
503 with CicUtil.Subst_not_found _ -> *)
504 let subst,metasenv,beta_expanded,ugraph1 =
506 test_equality_only metasenv subst context t2 args ugraph
508 fo_unif_subst test_equality_only subst context metasenv
509 (C.Meta (i,l)) beta_expanded ugraph1
510 | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
512 let (_,t,_) = CicUtil.lookup_subst i subst in
513 let lifted = S.subst_meta l t in
514 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
517 subst context metasenv t1 reduced ugraph
518 with CicUtil.Subst_not_found _ -> *)
519 let subst,metasenv,beta_expanded,ugraph1 =
522 metasenv subst context t1 args ugraph
524 fo_unif_subst test_equality_only subst context metasenv
525 (C.Meta (i,l)) beta_expanded ugraph1
527 let lr1 = List.rev l1 in
528 let lr2 = List.rev l2 in
530 fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
533 | _,[] -> assert false
536 test_equality_only subst context metasenv h1 h2 ugraph
539 fo_unif_subst test_equality_only subst context metasenv
540 h (C.Appl (List.rev l)) ugraph
541 | ((h1::l1),(h2::l2)) ->
542 let subst', metasenv',ugraph1 =
545 subst context metasenv h1 h2 ugraph
548 test_equality_only subst' metasenv' (l1,l2) ugraph1
551 test_equality_only subst metasenv (lr1, lr2) ugraph)
552 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
553 let subst', metasenv',ugraph1 =
554 fo_unif_subst test_equality_only subst context metasenv outt1 outt2
556 let subst'',metasenv'',ugraph2 =
557 fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
561 (fun (subst,metasenv,ugraph) t1 t2 ->
563 test_equality_only subst context metasenv t1 t2 ugraph
564 ) (subst'',metasenv'',ugraph2) pl1 pl2
566 Invalid_argument _ ->
567 raise (UnificationFailure (Reason "6")))
569 "Error trying to unify %s with %s: the number of branches is not the same."
570 (CicMetaSubst.ppterm subst t1)
571 (CicMetaSubst.ppterm subst t2)))) *)
572 | (C.Rel _, _) | (_, C.Rel _) ->
574 subst, metasenv,ugraph
576 raise (UnificationFailure (Reason "6"))
578 "Can't unify %s with %s because they are not convertible"
579 (CicMetaSubst.ppterm subst t1)
580 (CicMetaSubst.ppterm subst t2))) *)
581 | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
582 let subst,metasenv,beta_expanded,ugraph1 =
584 test_equality_only metasenv subst context t2 args ugraph
586 fo_unif_subst test_equality_only subst context metasenv
587 (C.Meta (i,l)) beta_expanded ugraph1
588 | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
589 let subst,metasenv,beta_expanded,ugraph1 =
591 test_equality_only metasenv subst context t1 args ugraph
593 fo_unif_subst test_equality_only subst context metasenv
594 beta_expanded (C.Meta (i,l)) ugraph1
595 | (C.Sort _ ,_) | (_, C.Sort _)
596 | (C.Const _, _) | (_, C.Const _)
597 | (C.MutInd _, _) | (_, C.MutInd _)
598 | (C.MutConstruct _, _) | (_, C.MutConstruct _)
599 | (C.Fix _, _) | (_, C.Fix _)
600 | (C.CoFix _, _) | (_, C.CoFix _) ->
602 subst, metasenv, ugraph
605 R.are_convertible ~subst ~metasenv context t1 t2 ugraph
608 subst, metasenv, ugraph1
610 raise (* (UnificationFailure "7") *)
611 (UnificationFailure (Reason (sprintf
612 "7: Can't unify %s with %s because they are not convertible"
613 (CicMetaSubst.ppterm subst t1)
614 (CicMetaSubst.ppterm subst t2))))
616 let t2' = R.whd ~subst context t2 in
619 fo_unif_subst test_equality_only
620 subst context metasenv t1 t2' ugraph
621 | _ -> raise (UnificationFailure (Reason "8")))
623 let t1' = R.whd ~subst context t1 in
626 fo_unif_subst test_equality_only
627 subst context metasenv t1' t2 ugraph
628 | _ -> (* raise (UnificationFailure "9")) *)
630 (UnificationFailure (Reason (sprintf
631 "9: Can't unify %s with %s because they are not convertible"
632 (CicMetaSubst.ppterm subst t1)
633 (CicMetaSubst.ppterm subst t2)))))
635 raise (UnificationFailure (Reason "10"))
637 "Can't unify %s with %s because they are not convertible"
638 (CicMetaSubst.ppterm subst t1)
639 (CicMetaSubst.ppterm subst t2))) *)
641 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
642 exp_named_subst1 exp_named_subst2 ugraph
646 (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
648 fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
649 ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
651 Invalid_argument _ ->
656 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
659 raise (UnificationFailure (Reason (sprintf
660 "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))))
662 (* A substitution is a (int * Cic.term) list that associates a *)
663 (* metavariable i with its body. *)
664 (* metasenv is of type Cic.metasenv *)
665 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
666 (* a new substitution which is already unwinded and ready to be applied and *)
667 (* a new metasenv in which some hypothesis in the contexts of the *)
668 (* metavariables may have been restricted. *)
669 let fo_unif metasenv context t1 t2 ugraph =
670 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
672 let fo_unif_subst subst context metasenv t1 t2 ugraph =
674 fo_unif_subst false subst context metasenv t1 t2 ugraph
676 | AssertFailure (Enriched _ as msg) -> assert false
677 | AssertFailure (Reason msg) ->
678 raise (AssertFailure (Enriched (msg,subst,context,metasenv,t1,t2,ugraph)))
679 | UnificationFailure (Enriched _ as msg) -> assert false
680 | UnificationFailure (Reason msg) ->
681 raise (UnificationFailure (Enriched (msg,subst,context,metasenv,t1,t2,ugraph)))
687 | Enriched (msg,subst,context,metasenv,t1,t2,ugraph) ->
688 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"
689 (CicMetaSubst.ppterm subst t1)
691 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
693 with _ -> "MALFORMED")
694 (CicMetaSubst.ppterm subst t2)
696 let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
698 with _ -> "MALFORMED")
699 (CicMetaSubst.ppcontext subst context)
700 (CicMetaSubst.ppmetasenv subst metasenv)
701 (CicMetaSubst.ppsubst subst) msg