V_______________________________________________________________ *)
module U = NUri
+module C = Cps
module S = Share
module L = Log
module G = Options
let s1, s2, s3 = s ^ " in the environment (expected)", "the term", "and in the environment (inferred)" in
L.log st BO.specs (pred level) (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
-let rec list_and map = function
+let rec list_and f map = function
| hd1 :: tl1, hd2 :: tl2 ->
- if map hd1 hd2 then list_and map (tl1, tl2) else false
- | l1, l2 -> l1 = l2
+ let f b = f (b && map hd1 hd2) in
+ list_and f map (tl1, tl2)
+ | l1, l2 -> f (l1 = l2)
let zero = Some 0
else m, r, None
| B.GRef (_, u) ->
begin match BE.get_entity u with
- | _, a, _, E.Abbr v ->
+ | _, a, _, E.Abbr (_, v) ->
m, B.gref a u, Some v
- | _, _, _, E.Abst w ->
+ | _, _, _, E.Abst (_, w) ->
if assert_tstep m true then begin
IFDEF SUMMARY THEN
if !G.summary then O.add ~grt:1 ()
step st (tstep m) w
end else
m, r, None
- | _, _, _, E.Void ->
+ | _, _, _, E.Void ->
assert false
end
| B.LRef (_, i) ->
and ac_stacks st m1 m2 =
(* L.warn "entering R.are_convertible_stacks"; *)
- if List.length m1.s <> List.length m2.s then false else
let map (c1, v1) (c2, v2) =
let m1, m2 = reset m1 ~e:c1 zero, reset m2 ~e:c2 zero in
ac st m1 v1 m2 v2
in
- list_and map (m1.s, m2.s)
+ list_and C.start map (m1.s, m2.s)
let rec ih_nfs st (m, t, r) =
match t, r with