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
lazy (fst (reduce ~delta:0 c)),
(fun delta -> fst (reduce ~delta c)),
lazy (unwind c)
- let from_stack ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta
+ let from_stack ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta
let from_stack_list_for_unwind ~unwind:_ l =
List.map (fun (_,_,c) -> Lazy.force c) l
let from_env ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta
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 )
let reduce_machine = R.reduce
let from_stack = RS.from_stack
+let from_env = RS.from_env
let unwind = R.unwind
let _ =