exception WrongShape;;
exception AlreadySimplified;;
-(*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
-(*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where *)
-(*CSC: Fix foo *)
-(*CSC: {foo [n,m:nat]:nat := *)
-(*CSC: Cases m of O => n | (S p) => (foo (S O) p) end *)
-(*CSC: } *)
(* Takes a well-typed term and *)
(* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
(* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
C.Rel n as t ->
(match List.nth context (n-1) with
Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
- | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
+ | Some (_,C.Def bo) ->
+ try_delta_expansion l t (S.lift n bo)
| None -> raise RelToHiddenHypothesis
)
| C.Var (uri,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 context l body',
- List.rev rev_constant_args
- | _ -> raise AlreadySimplified
- )
- | _ -> raise WrongShape
- in
- aux [] l (CicSubstitution.subst_vars exp_named_subst' body)
- in
- (**** Step 3 ****)
- let term_to_fold, delta_expanded_term_to_fold =
- let body' = CicSubstitution.subst_vars exp_named_subst' body in
- match constant_args with
- [] -> C.Const (uri,exp_named_subst'), body'
- | _ ->
- C.Appl ((C.Const (uri,exp_named_subst'))::constant_args),
- C.Appl (body'::constant_args)
- in
- let simplified_term_to_fold =
- reduceaux context [] delta_expanded_term_to_fold
- in
- replace (=) simplified_term_to_fold term_to_fold res
- with
- WrongShape ->
- (* The constant does not unfold to a Fix lambda-abstracted *)
- (* w.r.t. zero or more variables. We just perform reduction.*)
- reduceaux context l
- (CicSubstitution.subst_vars exp_named_subst' body)
- | AlreadySimplified ->
- (* If we performed delta-reduction, we would find a Fix *)
- (* not applied to a constructor. So, we refuse to perform *)
- (* delta-reduction. *)
- let t' = C.Const (uri,exp_named_subst') in
- if l = [] then t' else C.Appl (t'::l)
- end
+ C.Constant (_,Some body,_,_) ->
+ try_delta_expansion l
+ (C.Const (uri,exp_named_subst'))
+ (CicSubstitution.subst_vars exp_named_subst' body)
| C.Constant (_,None,_,_) ->
let t' = C.Const (uri,exp_named_subst') in
if l = [] then t' else C.Appl (t'::l)
if l = [] then t' else C.Appl (t'::l)
and reduceaux_exp_named_subst context l =
List.map (function uri,t -> uri,reduceaux context [] t)
+ (**** Step 2 ****)
+ and try_delta_expansion l term body =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ try
+ 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 context l body',
+ List.rev rev_constant_args
+ | _ -> raise AlreadySimplified
+ )
+ | _ -> raise WrongShape
+ in
+ aux [] l body
+ in
+ (**** Step 3 ****)
+ let term_to_fold, delta_expanded_term_to_fold =
+ match constant_args with
+ [] -> term,body
+ | _ -> C.Appl (term::constant_args), C.Appl (body::constant_args)
+ in
+ let simplified_term_to_fold =
+ reduceaux context [] delta_expanded_term_to_fold
+ in
+ replace (=) simplified_term_to_fold term_to_fold res
+ with
+ WrongShape ->
+ (* The constant does not unfold to a Fix lambda-abstracted *)
+ (* w.r.t. zero or more variables. We just perform reduction.*)
+ reduceaux context l body
+ | AlreadySimplified ->
+ (* If we performed delta-reduction, we would find a Fix *)
+ (* not applied to a constructor. So, we refuse to perform *)
+ (* delta-reduction. *)
+ if l = [] then term else C.Appl (term::l)
in
reduceaux context []
;;
projects / helm.git / commitdiff