(* Takes a well-typed term and *)
(* 1) Performs beta-iota-zeta reduction until delta reduction is needed *)
-(* Zeta-reduction is performed if and only if the simplified form of its *)
-(* definiendum (applied to the actual arguments) is different from the *)
-(* non-simplified form. *)
(* 2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted *)
(* w.r.t. zero or more variables and if the Fix can be reductaed, than it*)
(* is reduced, the delta-reduction is succesfull and the whole algorithm *)
-(* is applied again to the new redex; Step 3) is applied to the result *)
+(* is applied again to the new redex; Step 3.1) is applied to the result *)
(* of the recursive simplification. Otherwise, if the Fix can not be *)
(* reduced, than the delta-reductions fails and the delta-redex is *)
(* not reduced. Otherwise, if the delta-residual is not the *)
-(* lambda-abstraction of a Fix, then it is reduced and the result is *)
-(* directly returned, without performing step 3). *)
-(* 3) Folds the application of the constant to the arguments that did not *)
+(* lambda-abstraction of a Fix, then it performs step 3.2). *)
+(* 3.1) Folds the application of the constant to the arguments that did not *)
(* change in every iteration, i.e. to the actual arguments for the *)
(* lambda-abstractions that precede the Fix. *)
+(* 3.2) Computes the head beta-zeta normal form of the term. Then it tries *)
+(* reductions. If the reduction cannot be performed, it returns the *)
+(* original term (not the head beta-zeta normal form of the definiendum) *)
(*CSC: It does not perform simplification in a Case *)
let simpl context =
match List.nth context (n-1) with
Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
| Some (_,C.Def (bo,_)) ->
- let lifted_bo = S.lift n bo in
- let applied_lifted_bo = mk_appl lifted_bo l in
- let simplified = try_delta_expansion context l t lifted_bo in
- if simplified = applied_lifted_bo then
- if l = [] then t else C.Appl (t::l)
- else
- simplified
+ try_delta_expansion context l t (S.lift n bo)
| None -> raise RelToHiddenHypothesis
with
Failure _ -> assert false)
in
aux [] l body
in
- (**** Step 3 ****)
+ (**** Step 3.1 ****)
let term_to_fold, delta_expanded_term_to_fold =
match constant_args with
[] -> term,body
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
+ (**** Step 3.2 ****)
+ let rec aux l =
+ function
+ C.Lambda (name,s,t) ->
+ (match l with
+ [] -> raise AlreadySimplified
+ | he::tl ->
+ (* when name is Anonimous the substitution should *)
+ (* be superfluous *)
+ aux tl (S.subst he t))
+ | C.LetIn (_,s,t) -> aux l (S.subst s t)
+ | t ->
+ let simplified = reduceaux context l t in
+ if t = simplified then
+ raise AlreadySimplified
+ else
+ simplified
+ in
+ (try aux l body
+ with
+ AlreadySimplified ->
+ if l = [] then term else C.Appl (term::l))
| AlreadySimplified ->
(* If we performed delta-reduction, we would find a Fix *)
(* not applied to a constructor. So, we refuse to perform *)
| _,_ ->
raise
(ProofEngineTypes.Fail
- "The term to unfold is not a constant, a variable or a bound variable ")
+ (lazy "The term to unfold is not a constant, a variable or a bound variable "))
in
let appl he tl =
if tl = [] then he else Cic.Appl (he::tl) in
let cannot_delta_expand t =
raise
(ProofEngineTypes.Fail
- ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded")) in
+ (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in
let rec hd_delta_beta context tl =
function
Cic.Rel n as t ->
if res = [] then
raise
(ProofEngineTypes.Fail
- ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))
+ (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)))
else
res
in
projects / helm.git / blobdiff