- (_,Ref.Fix (fixno,recindex,height)) as refer) as head),s) as config ->
-(* if delta >= height then config else *)
- (match
- try Some (RS.from_stack ~delta (List.nth s recindex))
- with Failure _ -> None
- with
- | None -> config, true
- | Some recparam ->
- let fixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in
- match reduce ~delta:0 ~subst context recparam with
- | (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c, _
- when delta >= height ->
- let new_s =
- 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)
+ (_,Ref.Fix (fixno,recindex,height)) as refer)),s) as config ->
+ (let arg = try Some (List.nth s recindex) with Failure _ -> None in
+ match arg with
+ None -> config, true
+ | Some arg ->
+ let fixes,(_,_,pragma),_ =
+ NCicEnvironment.get_checked_fixes_or_cofixes refer in
+ 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)