exception AssertFailure of string Lazy.t;;
+let debug = ref false;;
+let pp m = if !debug then prerr_endline (Lazy.force m) else ();;
+
module type Strategy = sig
type stack_term
type env_term
(Ref.Decl|Ref.Ind _|Ref.Con _|Ref.CoFix _))), _) as config ->
config, true
| (_, _, (C.Const (Ref.Ref
- (_,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)
| (k, e, C.Match (_,_,term,pl),s) as config ->
let decofix = function
| (_,_,C.Const(Ref.Ref(_,Ref.CoFix c)as refer),s)->
when (Ref.eq r1 r2 &&
List.length (E.get_relevance r1) >= List.length tl1) ->
let relevance = E.get_relevance r1 in
+(* if the types were convertible the following optimization is sound
let relevance = match r1 with
| Ref.Ref (_,Ref.Con (_,_,lno)) ->
let _,relevance = HExtlib.split_nth lno relevance in
HExtlib.mk_list false lno @ relevance
| _ -> relevance
in
+*)
(try
HExtlib.list_forall_default3_var
(fun t1 t2 b -> not b || aux true context t1 t2 )