2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
14 exception MetaSubstFailure of string Lazy.t
15 exception Uncertain of string Lazy.t
18 (*** Functions to apply a substitution ***)
20 let apply_subst_gen ~appl_fun subst term =
23 let module S = CicSubstitution in
26 | C.Var (uri,exp_named_subst) ->
27 let exp_named_subst' =
28 List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
30 C.Var (uri, exp_named_subst')
33 let (_, t,_) = lookup_subst i subst in
34 um_aux (S.subst_meta l t)
35 with CicUtil.Subst_not_found _ ->
36 (* unconstrained variable, i.e. free in subst*)
38 List.map (function None -> None | Some t -> Some (um_aux t)) l
42 | C.Implicit _ as t -> t
43 | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
44 | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
45 | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
46 | C.LetIn (n,s,ty,t) -> C.LetIn (n, um_aux s, um_aux ty, um_aux t)
47 | C.Appl (hd :: tl) -> appl_fun um_aux hd tl
48 | C.Appl _ -> assert false
49 | C.Const (uri,exp_named_subst) ->
50 let exp_named_subst' =
51 List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
53 C.Const (uri, exp_named_subst')
54 | C.MutInd (uri,typeno,exp_named_subst) ->
55 let exp_named_subst' =
56 List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
58 C.MutInd (uri,typeno,exp_named_subst')
59 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
60 let exp_named_subst' =
61 List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
63 C.MutConstruct (uri,typeno,consno,exp_named_subst')
64 | C.MutCase (sp,i,outty,t,pl) ->
65 let pl' = List.map um_aux pl in
66 C.MutCase (sp, i, um_aux outty, um_aux t, pl')
69 List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl
74 List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl
82 let appl_fun um_aux he tl =
83 let tl' = List.map um_aux tl in
86 Cic.Appl l -> Cic.Appl (l@tl')
87 | he' -> Cic.Appl (he'::tl')
91 Cic.Meta (m,_) -> CicReduction.head_beta_reduce t'
96 (* incr apply_subst_counter; *)
99 | _ -> apply_subst_gen ~appl_fun subst t
102 let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst"
103 let apply_subst s t =
104 profiler.HExtlib.profile (apply_subst s) t
107 let apply_subst_context subst context =
112 incr apply_subst_context_counter;
113 context_length := !context_length + List.length context;
118 | Some (n, Cic.Decl t) ->
119 let t' = apply_subst subst t in
120 Some (n, Cic.Decl t') :: context
121 | Some (n, Cic.Def (t, ty)) ->
122 let ty' = apply_subst subst ty in
123 let t' = apply_subst subst t in
124 Some (n, Cic.Def (t', ty')) :: context
125 | None -> None :: context)
128 let apply_subst_metasenv subst metasenv =
130 incr apply_subst_metasenv_counter;
131 metasenv_length := !metasenv_length + List.length metasenv;
137 (fun (n, context, ty) ->
138 (n, apply_subst_context subst context, apply_subst subst ty))
140 (fun (i, _, _) -> not (List.mem_assoc i subst))
143 let tempi_type_of_aux_subst = ref 0.0;;
144 let tempi_subst = ref 0.0;;
145 let tempi_type_of_aux = ref 0.0;;
149 exception NotInTheList;;
151 let position n (shift, lc) =
153 | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList
154 | NCic.Itl len -> n - shift
156 let rec aux k = function
157 | [] -> raise NotInTheList
158 | (Cic.Rel m)::_ when m + shift = n -> k
159 | _::tl -> aux (k+1) tl
166 let rec force_does_not_occur subst to_be_restricted t =
167 let module C = Cic in
168 let more_to_be_restricted = ref [] in
169 let rec aux k = function
170 C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur
173 | C.Implicit _ -> assert false
175 (* we do not retrieve the term associated to ?n in subst since *)
176 (* in this way we can restrict if something goes wrong *)
188 more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
193 | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
194 | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
195 | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
196 | C.LetIn (name,so,ty,dest) ->
197 C.LetIn (name, aux k so, aux k ty, aux (k+1) dest)
198 | C.Appl l -> C.Appl (List.map (aux k) l)
199 | C.Var (uri,exp_named_subst) ->
200 let exp_named_subst' =
201 List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
203 C.Var (uri, exp_named_subst')
204 | C.Const (uri, exp_named_subst) ->
205 let exp_named_subst' =
206 List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
208 C.Const (uri, exp_named_subst')
209 | C.MutInd (uri,tyno,exp_named_subst) ->
210 let exp_named_subst' =
211 List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
213 C.MutInd (uri, tyno, exp_named_subst')
214 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
215 let exp_named_subst' =
216 List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
218 C.MutConstruct (uri, tyno, consno, exp_named_subst')
219 | C.MutCase (uri,tyno,out,te,pl) ->
220 C.MutCase (uri, tyno, aux k out, aux k te, List.map (aux k) pl)
222 let len = List.length fl in
223 let k_plus_len = k + len in
226 (fun (name,j,ty,bo) -> (name, j, aux k ty, aux k_plus_len bo)) fl
230 let len = List.length fl in
231 let k_plus_len = k + len in
234 (fun (name,ty,bo) -> (name, aux k ty, aux k_plus_len bo)) fl
239 (!more_to_be_restricted, res)
241 let rec restrict subst to_be_restricted metasenv =
242 match to_be_restricted with
243 | [] -> metasenv, subst
245 let names_of_context_indexes context indexes =
250 match List.nth context (i-1) with
251 | None -> assert false
252 | Some (n, _) -> CicPp.ppname n
254 Failure _ -> assert false
257 let force_does_not_occur_in_context to_be_restricted = function
259 | Some (name, Cic.Decl t) ->
260 let (more_to_be_restricted, t') =
261 force_does_not_occur subst to_be_restricted t
263 more_to_be_restricted, Some (name, Cic.Decl t')
264 | Some (name, Cic.Def (bo, ty)) ->
265 let (more_to_be_restricted, bo') =
266 force_does_not_occur subst to_be_restricted bo
268 let more_to_be_restricted, ty' =
269 let more_to_be_restricted', ty' =
270 force_does_not_occur subst to_be_restricted ty
272 more_to_be_restricted @ more_to_be_restricted',
275 more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
277 let rec erase i to_be_restricted n = function
278 | [] -> [], to_be_restricted, []
280 let more_to_be_restricted,restricted,tl' =
281 erase (i+1) to_be_restricted n tl
283 let restrict_me = List.mem i restricted in
285 more_to_be_restricted, restricted, None:: tl'
288 let more_to_be_restricted', hd' =
289 let delifted_restricted =
293 | j::tl when j > i -> (j - i)::aux tl
298 force_does_not_occur_in_context delifted_restricted hd
300 more_to_be_restricted @ more_to_be_restricted',
301 restricted, hd' :: tl'
303 more_to_be_restricted, (i :: restricted), None :: tl')
305 let (more_to_be_restricted, metasenv) = (* restrict metasenv *)
307 (fun (n, context, t) (more, metasenv) ->
308 let to_be_restricted =
309 List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
311 let (more_to_be_restricted, restricted, context') =
312 (* just an optimization *)
313 if to_be_restricted = [] then
316 erase 1 to_be_restricted n context
319 let more_to_be_restricted', t' =
320 force_does_not_occur subst restricted t
322 let metasenv' = (n, context', t') :: metasenv in
323 (more @ more_to_be_restricted @ more_to_be_restricted',
326 raise (MetaSubstFailure (lazy (sprintf
327 "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
328 n (names_of_context_indexes context to_be_restricted)))))
331 let (more_to_be_restricted', subst) = (* restrict subst *)
333 (* TODO: cambiare dopo l'aggiunta del ty *)
334 (fun (n, (context, term,ty)) (more, subst') ->
335 let to_be_restricted =
336 List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
339 let (more_to_be_restricted, restricted, context') =
340 (* just an optimization *)
341 if to_be_restricted = [] then
344 erase 1 to_be_restricted n context
346 let more_to_be_restricted', term' =
347 force_does_not_occur subst restricted term
349 let more_to_be_restricted'', ty' =
350 force_does_not_occur subst restricted ty in
351 let subst' = (n, (context', term',ty')) :: subst' in
353 more @ more_to_be_restricted
354 @ more_to_be_restricted'@more_to_be_restricted'' in
357 let error_msg = lazy (sprintf
358 "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
359 n (names_of_context_indexes context to_be_restricted) n
360 (ppterm ~metasenv subst term))
363 debug_print (lazy error_msg);
364 debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst)));
365 debug_print (lazy ("subst = \n" ^ (ppsubst subst)));
366 debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *)
367 raise (MetaSubstFailure error_msg)))
370 restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv
375 let maxmeta = ref 0 in
376 fun () -> incr maxmeta; !maxmeta
379 let restrict metasenv subst i to_be_restricted =
380 let force_does_not_occur_in_context to_be_restricted = function
382 | Some (name, Cic.Decl t) ->
383 let (more_to_be_restricted, t') =
384 force_does_not_occur subst to_be_restricted t
386 more_to_be_restricted, Some (name, Cic.Decl t')
387 | Some (name, Cic.Def (bo, ty)) ->
388 let (more_to_be_restricted, bo') =
389 force_does_not_occur subst to_be_restricted bo
391 let more_to_be_restricted, ty' =
392 let more_to_be_restricted', ty' =
393 force_does_not_occur subst to_be_restricted ty
395 more_to_be_restricted @ more_to_be_restricted',
398 more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
400 let rec erase i to_be_restricted n = function
401 | [] -> [], to_be_restricted, []
403 let more_to_be_restricted,restricted,tl' =
404 erase (i+1) to_be_restricted n tl
406 let restrict_me = List.mem i restricted in
408 more_to_be_restricted, restricted, None:: tl'
411 let more_to_be_restricted', hd' =
412 let delifted_restricted =
416 | j::tl when j > i -> (j - i)::aux tl
421 force_does_not_occur_in_context delifted_restricted hd
423 more_to_be_restricted @ more_to_be_restricted',
424 restricted, hd' :: tl'
426 more_to_be_restricted, (i :: restricted), None :: tl')
428 let (more_to_be_restricted, metasenv) = (* restrict metasenv *)
430 (fun (n, context, t) (more, metasenv) ->
431 let to_be_restricted =
432 List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
434 let (more_to_be_restricted, restricted, context') =
435 (* just an optimization *)
436 if to_be_restricted = [] then
439 erase 1 to_be_restricted n context
442 let more_to_be_restricted', t' =
443 force_does_not_occur subst restricted t
445 let metasenv' = (n, context', t') :: metasenv in
446 (more @ more_to_be_restricted @ more_to_be_restricted',
449 raise (MetaSubstFailure (lazy (sprintf
450 "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
451 n (names_of_context_indexes context to_be_restricted)))))
454 let (more_to_be_restricted', subst) = (* restrict subst *)
456 (* TODO: cambiare dopo l'aggiunta del ty *)
457 (fun (n, (context, term,ty)) (more, subst') ->
458 let to_be_restricted =
459 List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
462 let (more_to_be_restricted, restricted, context') =
463 (* just an optimization *)
464 if to_be_restricted = [] then
467 erase 1 to_be_restricted n context
469 let more_to_be_restricted', term' =
470 force_does_not_occur subst restricted term
472 let more_to_be_restricted'', ty' =
473 force_does_not_occur subst restricted ty in
474 let subst' = (n, (context', term',ty')) :: subst' in
476 more @ more_to_be_restricted
477 @ more_to_be_restricted'@more_to_be_restricted'' in
480 let error_msg = lazy (sprintf
481 "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
482 n (names_of_context_indexes context to_be_restricted) n
483 (ppterm ~metasenv subst term))
486 debug_print (lazy error_msg);
487 debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst)));
488 debug_print (lazy ("subst = \n" ^ (ppsubst subst)));
489 debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *)
490 raise (MetaSubstFailure error_msg)))
493 restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv
498 (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_),
499 otherwise the occur check does not make sense in case of unification
501 let delift metasenv subst context n l t =
502 let to_be_restricted = ref [] in
503 let rec aux k = function
504 | NCic.Rel n as t when n <= k -> t
507 match List.nth context (n-k-1) with
508 | _,NCic.Def (bo,_) ->
509 (try C.Rel ((position (n-k) l) + k)
511 (* CSC: This bit of reduction hurts performances since it is
512 * possible to have an exponential explosion of the size of the
513 * proof. required for nat/nth_prime.ma *)
514 aux k (NCicSubstitution.lift n bo))
515 | _,NCic.Decl _ -> NCic.Rel ((position (n-k) l) + k)
516 with Failure _ -> assert false) (*Unbound variable found in delift*)
517 | NCic.Meta (i,l1) as orig ->
519 let _,_,t,_ = NCicUtil.lookup_subst i subst in
520 aux k (NCicSubstitution.subst_meta l1 t)
521 with NCicUtil.Subst_not_found _ ->
522 (* see the top level invariant *)
524 raise (MetaSubstFailure (lazy (Printf.sprintf (
525 "Cannot unify the metavariable ?%d with a term that has "^^
526 "as subterm %s in which the same metavariable "^^
527 "occurs (occur check)") i
528 (NCicPp.ppterm ~context ~metasenv ~subst t))))
530 let shift1,lc1 = l1 in
533 | NCic.Irl len, NCic.Irl len1
534 when shift1 < shift || len1 + shift1 > len + shift ->
535 (* new meta with shortened l1
536 (1 -> shift - shift1 /\ shift + len + 1 -> shift1+len1)
537 subst += (i,new meta)
538 restrict checks (deleted entry cannot occur in the type...)
541 | NCic.Irl len, NCic.Irl len1 when shift = 0 -> orig
542 | NCic.Irl len, NCic.Irl len1 ->
543 NCic.Meta (i, (shift1 - shift, lc1))
545 let lc1 = NCicUtils.expand_local_context lc1 in
546 let rec deliftl j = function
549 let tl = deliftl (j+1) tl in
550 try (aux (k+shift1) t)::tl
552 | NotInTheList | MetaSubstFailure _ ->
553 to_be_restricted := (i,j)::!to_be_restricted;
556 let l1 = deliftl 1 l1 in
557 C.Meta(i,l1)) (* or another ?k and possibly compress l1 *)
558 | t -> NCicUtils.map (fun _ k -> k+1) k aux t
561 let metasenv, subst = restrict subst !to_be_restricted metasenv in
566 let to_be_restricted = ref [] in
567 let rec deliftaux k =
568 let module C = Cic in
575 match List.nth context (m-k-1) with
576 Some (_,C.Def (t,_)) ->
578 C.Rel ((position (m-k) l) + k)
581 (*CSC: Hmmm. This bit of reduction is not in the spirit of *)
582 (*CSC: first order unification. Does it help or does it harm? *)
583 (*CSC: ANSWER: it hurts performances since it is possible to *)
584 (*CSC: have an exponential explosion of the size of the proof.*)
585 (*CSC: However, without this bit of reduction some "apply" in *)
586 (*CSC: the library fail (e.g. nat/nth_prime.ma). *)
587 deliftaux k (S.lift m t))
588 | Some (_,C.Decl t) ->
589 C.Rel ((position (m-k) l) + k)
590 | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis"))
593 raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux"))
595 | C.Var (uri,exp_named_subst) ->
596 let exp_named_subst' =
597 List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
599 C.Var (uri,exp_named_subst')
600 | C.Meta (i, l1) as t ->
602 let (_,t,_) = CicUtil.lookup_subst i subst in
603 deliftaux k (CicSubstitution.subst_meta l1 t)
604 with CicUtil.Subst_not_found _ ->
605 (* see the top level invariant *)
607 raise (MetaSubstFailure (lazy (sprintf
608 "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
609 i (ppterm ~metasenv subst t))))
615 | None::tl -> None::(deliftl (j+1) tl)
617 let l1' = (deliftl (j+1) tl) in
619 Some (deliftaux k t)::l1'
622 | MetaSubstFailure _ ->
624 (i,j)::!to_be_restricted ; None::l1'
626 let l' = deliftl 1 l1 in
630 | C.Implicit _ as t -> t
631 | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
632 | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
633 | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
634 | C.LetIn (n,s,ty,t) ->
635 C.LetIn (n, deliftaux k s, deliftaux k ty, deliftaux (k+1) t)
636 | C.Appl l -> C.Appl (List.map (deliftaux k) l)
637 | C.Const (uri,exp_named_subst) ->
638 let exp_named_subst' =
639 List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
641 C.Const (uri,exp_named_subst')
642 | C.MutInd (uri,typeno,exp_named_subst) ->
643 let exp_named_subst' =
644 List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
646 C.MutInd (uri,typeno,exp_named_subst')
647 | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
648 let exp_named_subst' =
649 List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
651 C.MutConstruct (uri,typeno,consno,exp_named_subst')
652 | C.MutCase (sp,i,outty,t,pl) ->
653 C.MutCase (sp, i, deliftaux k outty, deliftaux k t,
654 List.map (deliftaux k) pl)
656 let len = List.length fl in
659 (fun (name, i, ty, bo) ->
660 (name, i, deliftaux k ty, deliftaux (k+len) bo))
665 let len = List.length fl in
668 (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
671 C.CoFix (i, liftedfl)
678 (* This is the case where we fail even first order unification. *)
679 (* The reason is that our delift function is weaker than first *)
680 (* order (in the sense of alpha-conversion). See comment above *)
681 (* related to the delift function. *)
682 (* debug_print (lazy "First Order UnificationFailure during delift") ;
683 debug_print(lazy (sprintf
684 "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
688 (function Some t -> ppterm subst t | None -> "_") l
690 let msg = (lazy (sprintf
691 "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
692 (ppterm ~metasenv subst t)
695 (function Some t -> ppterm ~metasenv subst t | None -> "_")
701 Some t -> CicUtil.is_meta_closed (apply_subst subst t)
704 raise (Uncertain msg)
706 raise (MetaSubstFailure msg)
708 let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
712 (* delifts a term t of n levels strating from k, that is changes (Rel m)
713 * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails
715 let delift_rels_from subst metasenv k n =
716 let rec liftaux subst metasenv k =
717 let module C = Cic in
722 else if m < k + n then
723 raise DeliftingARelWouldCaptureAFreeVariable
725 C.Rel (m - n), subst, metasenv
726 | C.Var (uri,exp_named_subst) ->
727 let exp_named_subst',subst,metasenv =
729 (fun (uri,t) (l,subst,metasenv) ->
730 let t',subst,metasenv = liftaux subst metasenv k t in
731 (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
733 C.Var (uri,exp_named_subst'),subst,metasenv
736 let (_, t,_) = lookup_subst i subst in
737 liftaux subst metasenv k (CicSubstitution.subst_meta l t)
738 with CicUtil.Subst_not_found _ ->
739 let l',to_be_restricted,subst,metasenv =
740 let rec aux con l subst metasenv =
742 [] -> [],[],subst,metasenv
744 let tl',to_be_restricted,subst,metasenv =
745 aux (con + 1) tl subst metasenv in
746 let he',more_to_be_restricted,subst,metasenv =
748 None -> None,[],subst,metasenv
751 let t',subst,metasenv = liftaux subst metasenv k t in
752 Some t',[],subst,metasenv
754 DeliftingARelWouldCaptureAFreeVariable ->
755 None,[i,con],subst,metasenv
757 he'::tl',more_to_be_restricted@to_be_restricted,subst,metasenv
759 aux 1 l subst metasenv in
760 let metasenv,subst = restrict subst to_be_restricted metasenv in
761 C.Meta(i,l'),subst,metasenv)
762 | C.Sort _ as t -> t,subst,metasenv
763 | C.Implicit _ as t -> t,subst,metasenv
765 let te',subst,metasenv = liftaux subst metasenv k te in
766 let ty',subst,metasenv = liftaux subst metasenv k ty in
767 C.Cast (te',ty'),subst,metasenv
769 let s',subst,metasenv = liftaux subst metasenv k s in
770 let t',subst,metasenv = liftaux subst metasenv (k+1) t in
771 C.Prod (n,s',t'),subst,metasenv
772 | C.Lambda (n,s,t) ->
773 let s',subst,metasenv = liftaux subst metasenv k s in
774 let t',subst,metasenv = liftaux subst metasenv (k+1) t in
775 C.Lambda (n,s',t'),subst,metasenv
776 | C.LetIn (n,s,ty,t) ->
777 let s',subst,metasenv = liftaux subst metasenv k s in
778 let ty',subst,metasenv = liftaux subst metasenv k ty in
779 let t',subst,metasenv = liftaux subst metasenv (k+1) t in
780 C.LetIn (n,s',ty',t'),subst,metasenv
782 let l',subst,metasenv =
784 (fun t (l,subst,metasenv) ->
785 let t',subst,metasenv = liftaux subst metasenv k t in
786 t'::l,subst,metasenv) l ([],subst,metasenv) in
787 C.Appl l',subst,metasenv
788 | C.Const (uri,exp_named_subst) ->
789 let exp_named_subst',subst,metasenv =
791 (fun (uri,t) (l,subst,metasenv) ->
792 let t',subst,metasenv = liftaux subst metasenv k t in
793 (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
795 C.Const (uri,exp_named_subst'),subst,metasenv
796 | C.MutInd (uri,tyno,exp_named_subst) ->
797 let exp_named_subst',subst,metasenv =
799 (fun (uri,t) (l,subst,metasenv) ->
800 let t',subst,metasenv = liftaux subst metasenv k t in
801 (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
803 C.MutInd (uri,tyno,exp_named_subst'),subst,metasenv
804 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
805 let exp_named_subst',subst,metasenv =
807 (fun (uri,t) (l,subst,metasenv) ->
808 let t',subst,metasenv = liftaux subst metasenv k t in
809 (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
811 C.MutConstruct (uri,tyno,consno,exp_named_subst'),subst,metasenv
812 | C.MutCase (sp,i,outty,t,pl) ->
813 let outty',subst,metasenv = liftaux subst metasenv k outty in
814 let t',subst,metasenv = liftaux subst metasenv k t in
815 let pl',subst,metasenv =
817 (fun t (l,subst,metasenv) ->
818 let t',subst,metasenv = liftaux subst metasenv k t in
819 t'::l,subst,metasenv) pl ([],subst,metasenv)
821 C.MutCase (sp,i,outty',t',pl'),subst,metasenv
823 let len = List.length fl in
824 let liftedfl,subst,metasenv =
826 (fun (name, i, ty, bo) (l,subst,metasenv) ->
827 let ty',subst,metasenv = liftaux subst metasenv k ty in
828 let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
829 (name,i,ty',bo')::l,subst,metasenv
830 ) fl ([],subst,metasenv)
832 C.Fix (i, liftedfl),subst,metasenv
834 let len = List.length fl in
835 let liftedfl,subst,metasenv =
837 (fun (name, ty, bo) (l,subst,metasenv) ->
838 let ty',subst,metasenv = liftaux subst metasenv k ty in
839 let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
840 (name,ty',bo')::l,subst,metasenv
841 ) fl ([],subst,metasenv)
843 C.CoFix (i, liftedfl),subst,metasenv
845 liftaux subst metasenv k
847 let delift_rels subst metasenv n t =
848 delift_rels_from subst metasenv 1 n t