- Some (recarg, fixes, pragma)
- with Failure _ -> None
- with
- | None -> config, true
- | Some((_,_,C.Const(Ref.Ref(_,Ref.Con _)),_::_ as c),fs,`Projection) ->
- let new_s =
- replace recindex s (RS.compute_to_stack ~reduce:(reduce ~subst
- context) ~unwind c)
- in
- let _,_,_,_,body = List.nth fs fixno in
- aux (0, [], body, new_s)
- | Some (recparam, fixes, pragma) ->
- match reduce ~delta:0 ~subst context recparam with
- | (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c, _
- when delta >= height ->
- let new_s =
- (* FIXME, we should push on the stack
- * c for CBV and recparam for CBN *)
- if pragma = `Projection then
- replace recindex s (RS.compute_to_stack ~reduce:(reduce ~subst
- context) ~unwind recparam)
- else
- replace recindex s (RS.compute_to_stack ~reduce:(reduce ~subst
- context) ~unwind c)
- in
- (0, [], head, new_s), false
- | (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c, _ ->
- let new_s =
- replace recindex s (RS.compute_to_stack ~reduce:(reduce ~subst
- context) ~unwind c)
- in
- let _,_,_,_,body = List.nth fixes fixno in
- aux (0, [], body, new_s)
- | _ -> config, true)
+ if delta >= height then
+ match pragma with
+ | `Projection ->
+ (match RS.from_stack ~delta:max_int arg with
+ | _,_,C.Const(Ref.Ref(_,Ref.Con _)),_::_ ->
+ let _,_,_,_,body = List.nth fixes fixno in
+ aux (0, [], body, s)
+ | _ -> config,false)
+ | _ -> config,false
+ else
+ match RS.from_stack ~delta:0 arg with
+ | (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c ->
+ let new_s =
+ replace recindex s
+ (RS.compute_to_stack ~reduce:(reduce ~subst context)
+ ~unwind c) in
+ let _,_,_,_,body = List.nth fixes fixno in
+ aux (0, [], body, new_s)
+ | _ -> config, true)