- | C.Const (uri,cookingsno) as t ->
- (match CicEnvironment.get_cooked_obj uri cookingsno with
- C.Definition (_,body,_,_) ->
- begin
- try
- (**** Step 2 ****)
- let res,constant_args =
- let rec aux rev_constant_args l =
- function
- C.Lambda (name,s,t) as t' ->
- begin
- match l with
- [] -> raise WrongShape
- | he::tl ->
- (* when name is Anonimous the substitution should be *)
- (* superfluous *)
- aux (he::rev_constant_args) tl (S.subst he t)
- end
- | C.LetIn (_,s,t) ->
- aux rev_constant_args l (S.subst s t)
- | C.Fix (i,fl) as t ->
- let tys =
- List.map (function (name,_,ty,_) ->
- Some (C.Name name, C.Decl ty)) fl
- in
- let (_,recindex,_,body) = List.nth fl i in
- let recparam =
- try
- List.nth l recindex
- with
- _ -> raise AlreadySimplified
- in
- (match CicReduction.whd context recparam with
- C.MutConstruct _
- | C.Appl ((C.MutConstruct _)::_) ->
- let body' =
- let counter = ref (List.length fl) in
- List.fold_right
- (function _ ->
- decr counter ; S.subst (C.Fix (!counter,fl))
- ) fl body
- in
- (* Possible optimization: substituting whd *)
- (* recparam in l *)
- reduceaux (tys@context) l body',
- List.rev rev_constant_args
- | _ -> raise AlreadySimplified
- )
- | _ -> raise WrongShape
- in
- aux [] l body
- in
- (**** Step 3 ****)
- let term_to_fold =
- match constant_args with
- [] -> C.Const (uri,cookingsno)
- | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ reduceaux_exp_named_subst context l exp_named_subst
+ in
+ (match CicEnvironment.get_obj uri with
+ C.Constant (_,Some body,_,_) ->
+ begin
+ try
+ (**** Step 2 ****)
+ let res,constant_args =
+ let rec aux rev_constant_args l =
+ function
+ C.Lambda (name,s,t) as t' ->
+ begin
+ match l with
+ [] -> raise WrongShape
+ | he::tl ->
+ (* when name is Anonimous the substitution should *)
+ (* be superfluous *)
+ aux (he::rev_constant_args) tl (S.subst he t)
+ end
+ | C.LetIn (_,s,t) ->
+ aux rev_constant_args l (S.subst s t)
+ | C.Fix (i,fl) as t ->
+ let tys =
+ List.map (function (name,_,ty,_) ->
+ Some (C.Name name, C.Decl ty)) fl
+ in
+ let (_,recindex,_,body) = List.nth fl i in
+ let recparam =
+ try
+ List.nth l recindex
+ with
+ _ -> raise AlreadySimplified
+ in
+ (match CicReduction.whd context recparam with
+ C.MutConstruct _
+ | C.Appl ((C.MutConstruct _)::_) ->
+ let body' =
+ let counter = ref (List.length fl) in
+ List.fold_right
+ (function _ ->
+ decr counter ; S.subst (C.Fix (!counter,fl))
+ ) fl body
+ in
+ (* Possible optimization: substituting whd *)
+ (* recparam in l *)
+ reduceaux (tys@context) l body',
+ List.rev rev_constant_args
+ | _ -> raise AlreadySimplified
+ )
+ | _ -> raise WrongShape
+ in
+ aux [] l (CicSubstitution.subst_vars exp_named_subst' body)