From 1144e631fb9e26cddfeeb70c1f368a1f262fedac Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Fri, 4 Oct 2024 16:53:22 -0400 Subject: [PATCH] Switch to req_value --- src/haz3lcore/dynamics/Transition.re | 2 +- test/Test_Evaluator.re | 64 ++++++++++++++++------------ 2 files changed, 37 insertions(+), 29 deletions(-) diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index 7a9e8f16bf..5c936426b9 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -336,7 +336,7 @@ module Transition = (EV: EV_MODE) => { | Ap(dir, d1, d2) => let. _ = otherwise(env, (d1, (d2, _)) => Ap(dir, d1, d2) |> rewrap) and. d1' = - req_final(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1) + req_value(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1) and. (d2', d2_is_value) = req_final_or_value( req(state, env), diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re index ca85062226..37fcaba764 100644 --- a/test/Test_Evaluator.re +++ b/test/Test_Evaluator.re @@ -56,46 +56,54 @@ let tet_ap_of_hole_deferral = () => Ap( Forward, Cast( - EmptyHole |> Exp.fresh, - Unknown(Internal) |> Typ.fresh, + Cast( + EmptyHole |> Exp.fresh, + Unknown(Internal) |> Typ.fresh, + Arrow( + Unknown(Internal) |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Typ.fresh, + ) + |> Exp.fresh, Arrow( Unknown(Internal) |> Typ.fresh, Unknown(Internal) |> Typ.fresh, ) |> Typ.fresh, - ) - |> Exp.fresh, - Cast( - Tuple([ - Cast( - Float(1.) |> Exp.fresh, - Float |> Typ.fresh, + Arrow( + Prod([ Unknown(Internal) |> Typ.fresh, - ) - |> Exp.fresh, - Cast( - Bool(true) |> Exp.fresh, - Bool |> Typ.fresh, Unknown(Internal) |> Typ.fresh, - ) - |> Exp.fresh, - Cast( - Int(3) |> Exp.fresh, - Int |> Typ.fresh, Unknown(Internal) |> Typ.fresh, - ) - |> Exp.fresh, - ]) - |> Exp.fresh, - Prod([ - Unknown(Internal) |> Typ.fresh, - Unknown(Internal) |> Typ.fresh, + ]) + |> Typ.fresh, Unknown(Internal) |> Typ.fresh, - ]) + ) |> Typ.fresh, - Unknown(Internal) |> Typ.fresh, ) |> Exp.fresh, + Tuple([ + Cast( + Float(1.) |> Exp.fresh, + Float |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + Cast( + Bool(true) |> Exp.fresh, + Bool |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + Cast( + Int(3) |> Exp.fresh, + Int |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Exp.fresh, + ]) + |> Exp.fresh, ) |> Exp.fresh, Ap(