- C.Rel _ as t -> t
- | C.Var _ as t -> t
- | C.Meta i as t ->(try S.lift k (List.assoc i !unwinded)
- with Not_found ->
- if List.mem i !frozen then
- raise OccurCheck
- else
- let saved_frozen = !frozen in
- frozen := i::!frozen ;
- let res =
- try
- let t = List.assoc i subst in
- let t' = um_aux 0 t in
- unwinded := (i,t')::!unwinded ;
- S.lift k t'
- with
- Not_found ->
- (* not constrained variable, i.e. free in subst*)
- C.Meta i
- in
- frozen := saved_frozen ;
- res
- )
- | C.Sort _ as t -> t
- | C.Implicit as t -> t
- | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
- | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
- | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
- | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
+ C.Rel _ as t -> t,metasenv
+ | C.Var _ as t -> t,metasenv
+ | C.Meta (i,l) ->
+ (try
+ S.lift_meta l (List.assoc i !unwinded), metasenv
+ with Not_found ->
+ if List.mem i !frozen then raise OccurCheck
+ else
+ let saved_frozen = !frozen in
+ frozen := i::!frozen ;
+ let res =
+ try
+ let t = List.assoc i subst in
+ let t',metasenv' = um_aux metasenv t in
+ let _,metasenv'' =
+ let (_,canonical_context,_) =
+ List.find (function (m,_,_) -> m=i) metasenv
+ in
+prerr_endline ("DELIFT(" ^ CicPp.ppterm t' ^ ")") ; flush stderr ;
+List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ;
+prerr_endline "<DELIFT" ; flush stderr ;
+ S.delift canonical_context metasenv' l t'
+ in
+ unwinded := (i,t')::!unwinded ;
+ S.lift_meta l t', metasenv'
+ with
+ Not_found ->
+ (* not constrained variable, i.e. free in subst*)
+ let l',metasenv' =
+ List.fold_right
+ (fun t (tl,metasenv) ->
+ match t with
+ None -> None::tl,metasenv
+ | Some t ->
+ let t',metasenv' = um_aux metasenv t in
+ (Some t')::tl, metasenv'
+ ) l ([],metasenv)
+ in
+ C.Meta (i,l'), metasenv'
+ in
+ frozen := saved_frozen ;
+ res
+ )
+ | C.Sort _
+ | C.Implicit as t -> t,metasenv
+ | C.Cast (te,ty) ->
+ let te',metasenv' = um_aux metasenv te in
+ let ty',metasenv'' = um_aux metasenv' ty in
+ C.Cast (te',ty'),metasenv''
+ | C.Prod (n,s,t) ->
+ let s',metasenv' = um_aux metasenv s in
+ let t',metasenv'' = um_aux metasenv' t in
+ C.Prod (n, s', t'), metasenv''
+ | C.Lambda (n,s,t) ->
+ let s',metasenv' = um_aux metasenv s in
+ let t',metasenv'' = um_aux metasenv' t in
+ C.Lambda (n, s', t'), metasenv''
+ | C.LetIn (n,s,t) ->
+ let s',metasenv' = um_aux metasenv s in
+ let t',metasenv'' = um_aux metasenv' t in
+ C.LetIn (n, s', t'), metasenv''