- (* 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))