+(* delifts a term t of n levels strating from k, that is changes (Rel m)
+ * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails
+ *)
+let delift_rels_from subst metasenv k n =
+ let rec liftaux subst metasenv k =
+ let module C = Cic in
+ function
+ C.Rel m ->
+ if m < k then
+ C.Rel m, subst, metasenv
+ else if m < k + n then
+ raise DeliftingARelWouldCaptureAFreeVariable
+ else
+ C.Rel (m - n), subst, metasenv
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst',subst,metasenv =
+ List.fold_right
+ (fun (uri,t) (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
+ in
+ C.Var (uri,exp_named_subst'),subst,metasenv
+ | C.Meta (i,l) ->
+ (try
+ let (_, t,_) = lookup_subst i subst in
+ liftaux subst metasenv k (CicSubstitution.subst_meta l t)
+ with CicUtil.Subst_not_found _ ->
+ let l',to_be_restricted,subst,metasenv =
+ let rec aux con l subst metasenv =
+ match l with
+ [] -> [],[],subst,metasenv
+ | he::tl ->
+ let tl',to_be_restricted,subst,metasenv =
+ aux (con + 1) tl subst metasenv in
+ let he',more_to_be_restricted,subst,metasenv =
+ match he with
+ None -> None,[],subst,metasenv
+ | Some t ->
+ try
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ Some t',[],subst,metasenv
+ with
+ DeliftingARelWouldCaptureAFreeVariable ->
+ None,[i,con],subst,metasenv
+ in
+ he'::tl',more_to_be_restricted@to_be_restricted,subst,metasenv
+ in
+ aux 1 l subst metasenv in
+ let metasenv,subst = restrict subst to_be_restricted metasenv in
+ C.Meta(i,l'),subst,metasenv)
+ | C.Sort _ as t -> t,subst,metasenv
+ | C.Implicit _ as t -> t,subst,metasenv
+ | C.Cast (te,ty) ->
+ let te',subst,metasenv = liftaux subst metasenv k te in
+ let ty',subst,metasenv = liftaux subst metasenv k ty in
+ C.Cast (te',ty'),subst,metasenv
+ | C.Prod (n,s,t) ->
+ let s',subst,metasenv = liftaux subst metasenv k s in
+ let t',subst,metasenv = liftaux subst metasenv (k+1) t in
+ C.Prod (n,s',t'),subst,metasenv
+ | C.Lambda (n,s,t) ->
+ let s',subst,metasenv = liftaux subst metasenv k s in
+ let t',subst,metasenv = liftaux subst metasenv (k+1) t in
+ C.Lambda (n,s',t'),subst,metasenv
+ | C.LetIn (n,s,t) ->
+ let s',subst,metasenv = liftaux subst metasenv k s in
+ let t',subst,metasenv = liftaux subst metasenv (k+1) t in
+ C.LetIn (n,s',t'),subst,metasenv
+ | C.Appl l ->
+ let l',subst,metasenv =
+ List.fold_right
+ (fun t (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ t'::l,subst,metasenv) l ([],subst,metasenv) in
+ C.Appl l',subst,metasenv
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst',subst,metasenv =
+ List.fold_right
+ (fun (uri,t) (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
+ in
+ C.Const (uri,exp_named_subst'),subst,metasenv
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let exp_named_subst',subst,metasenv =
+ List.fold_right
+ (fun (uri,t) (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
+ in
+ C.MutInd (uri,tyno,exp_named_subst'),subst,metasenv
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let exp_named_subst',subst,metasenv =
+ List.fold_right
+ (fun (uri,t) (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
+ in
+ C.MutConstruct (uri,tyno,consno,exp_named_subst'),subst,metasenv
+ | C.MutCase (sp,i,outty,t,pl) ->
+ let outty',subst,metasenv = liftaux subst metasenv k outty in
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ let pl',subst,metasenv =
+ List.fold_right
+ (fun t (l,subst,metasenv) ->
+ let t',subst,metasenv = liftaux subst metasenv k t in
+ t'::l,subst,metasenv) pl ([],subst,metasenv)
+ in
+ C.MutCase (sp,i,outty',t',pl'),subst,metasenv
+ | C.Fix (i, fl) ->
+ let len = List.length fl in
+ let liftedfl,subst,metasenv =
+ List.fold_right
+ (fun (name, i, ty, bo) (l,subst,metasenv) ->
+ let ty',subst,metasenv = liftaux subst metasenv k ty in
+ let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
+ (name,i,ty',bo')::l,subst,metasenv
+ ) fl ([],subst,metasenv)
+ in
+ C.Fix (i, liftedfl),subst,metasenv
+ | C.CoFix (i, fl) ->
+ let len = List.length fl in
+ let liftedfl,subst,metasenv =
+ List.fold_right
+ (fun (name, ty, bo) (l,subst,metasenv) ->
+ let ty',subst,metasenv = liftaux subst metasenv k ty in
+ let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
+ (name,ty',bo')::l,subst,metasenv
+ ) fl ([],subst,metasenv)
+ in
+ C.CoFix (i, liftedfl),subst,metasenv
+ in
+ liftaux subst metasenv k
+
+let delift_rels subst metasenv n t =
+ delift_rels_from subst metasenv 1 n t
+
+