-let rec unwind metasenv subst unwinded t =
- let unwinded = ref unwinded in
- let frozen = ref [] in
- let rec um_aux metasenv =
- let module C = Cic in
- let module S = CicSubstitution in
- function
- 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 (MetaSubstFailure
- "Failed to unify due to cyclic constraints (occur check)")
- 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,_) = CicUtil.lookup_meta i metasenv in
- delift i subst 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''
- | C.Appl (he::tl) ->
- let tl',metasenv' =
- List.fold_right
- (fun t (tl,metasenv) ->
- let t',metasenv' = um_aux metasenv t in
- t'::tl, metasenv'
- ) tl ([],metasenv)
- in
- begin
- match um_aux metasenv' he with
- (C.Appl l, metasenv'') -> C.Appl (l@tl'),metasenv''
- | (he', metasenv'') -> C.Appl (he'::tl'),metasenv''
- end
- | C.Appl _ -> assert false
- | C.Const (uri,exp_named_subst) ->
- let exp_named_subst', metasenv' =
- List.fold_right
- (fun (uri,t) (tl,metasenv) ->
- let t',metasenv' = um_aux metasenv t in
- (uri,t')::tl, metasenv'
- ) exp_named_subst ([],metasenv)
- in
- C.Const (uri,exp_named_subst'),metasenv'
- | C.MutInd (uri,typeno,exp_named_subst) ->
- let exp_named_subst', metasenv' =
- List.fold_right
- (fun (uri,t) (tl,metasenv) ->
- let t',metasenv' = um_aux metasenv t in
- (uri,t')::tl, metasenv'
- ) exp_named_subst ([],metasenv)
- in
- C.MutInd (uri,typeno,exp_named_subst'),metasenv'
- | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
- let exp_named_subst', metasenv' =
- List.fold_right
- (fun (uri,t) (tl,metasenv) ->
- let t',metasenv' = um_aux metasenv t in
- (uri,t')::tl, metasenv'
- ) exp_named_subst ([],metasenv)
- in
- C.MutConstruct (uri,typeno,consno,exp_named_subst'),metasenv'
- | C.MutCase (sp,i,outty,t,pl) ->
- let outty',metasenv' = um_aux metasenv outty in
- let t',metasenv'' = um_aux metasenv' t in
- let pl',metasenv''' =
- List.fold_right
- (fun p (pl,metasenv) ->
- let p',metasenv' = um_aux metasenv p in
- p'::pl, metasenv'
- ) pl ([],metasenv'')
- in
- C.MutCase (sp, i, outty', t', pl'),metasenv'''
- | C.Fix (i, fl) ->
- let len = List.length fl in
- let liftedfl,metasenv' =
- List.fold_right
- (fun (name, i, ty, bo) (fl,metasenv) ->
- let ty',metasenv' = um_aux metasenv ty in
- let bo',metasenv'' = um_aux metasenv' bo in
- (name, i, ty', bo')::fl,metasenv''
- ) fl ([],metasenv)
- in
- C.Fix (i, liftedfl),metasenv'
- | C.CoFix (i, fl) ->
- let len = List.length fl in
- let liftedfl,metasenv' =
- List.fold_right
- (fun (name, ty, bo) (fl,metasenv) ->
- let ty',metasenv' = um_aux metasenv ty in
- let bo',metasenv'' = um_aux metasenv' bo in
- (name, ty', bo')::fl,metasenv''
- ) fl ([],metasenv)
- in
- C.CoFix (i, liftedfl),metasenv'
- in
- let t',metasenv' = um_aux metasenv t in
- t',metasenv',!unwinded
-
-let apply_subst subst t =
- (* metasenv will not be used nor modified. So, let's use a dummy empty one *)
- let metasenv = [] in
- let (t',_,_) = unwind metasenv [] subst t in
- t'
-
-(* apply_subst_reducing subst (Some (mtr,reductions_no)) t *)
-(* performs as (apply_subst subst t) until it finds an application of *)
-(* (META [meta_to_reduce]) that, once unwinding is performed, creates *)
-(* a new beta-redex; in this case up to [reductions_no] consecutive *)
-(* beta-reductions are performed. *)
-(* Hint: this function is usually called when [reductions_no] *)
-(* eta-expansions have been performed and the head of the new *)
-(* application has been unified with (META [meta_to_reduce]): *)
-(* during the unwinding the eta-expansions are undone. *)
-
-let rec apply_subst_context subst =
- List.map (function
- | Some (n, Cic.Decl t) -> Some (n, Cic.Decl (apply_subst subst t))
- | Some (n, Cic.Def (t, ty)) ->
- let ty' =
- match ty with
- | None -> None
- | Some ty -> Some (apply_subst subst ty)
- in
- Some (n, Cic.Def (apply_subst subst t, ty'))
- | None -> None)