From 4bf139a6447165e50281ffb7c0619969f25dc0ec Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Mon, 2 Dec 2024 15:17:33 -0500 Subject: [PATCH 1/2] remove req-value --- src/haz3lcore/dynamics/Builtins.re | 19 +-- src/haz3lcore/dynamics/Evaluator.re | 94 ++++---------- src/haz3lcore/dynamics/EvaluatorStep.re | 38 ------ src/haz3lcore/dynamics/Transition.re | 155 ++++++++---------------- src/haz3lcore/dynamics/Unboxing.re | 46 ++++++- src/haz3lcore/dynamics/ValueChecker.re | 59 +++------ 6 files changed, 141 insertions(+), 270 deletions(-) diff --git a/src/haz3lcore/dynamics/Builtins.re b/src/haz3lcore/dynamics/Builtins.re index c47617edc6..21edcfe19e 100644 --- a/src/haz3lcore/dynamics/Builtins.re +++ b/src/haz3lcore/dynamics/Builtins.re @@ -1,3 +1,4 @@ +open Util; open DHExp; /* @@ -12,13 +13,13 @@ open DHExp; [@deriving (show({with_path: false}), sexp)] type builtin = | Const(Typ.t, DHExp.t) - | Fn(Typ.t, Typ.t, DHExp.t => DHExp.t); + | Fn(Typ.t, Typ.t, DHExp.t => option(DHExp.t)); [@deriving (show({with_path: false}), sexp)] type t = VarMap.t_(builtin); [@deriving (show({with_path: false}), sexp)] -type forms = VarMap.t_(DHExp.t => DHExp.t); +type forms = VarMap.t_(DHExp.t => option(DHExp.t)); type result = Result.t(DHExp.t, EvaluatorError.t); @@ -29,7 +30,7 @@ let fn = name: Var.t, t1: Typ.term, t2: Typ.term, - impl: DHExp.t => DHExp.t, + impl: DHExp.t => option(DHExp.t), // None if indet builtins: t, ) : t => @@ -51,8 +52,8 @@ module Pervasives = { let unary = (f: DHExp.t => result, d: DHExp.t) => { switch (f(d)) { - | Ok(r') => r' - | Error(e) => EvaluatorError.Exception(e) |> raise + | Ok(r') => Some(r') + | Error(_) => None }; }; @@ -60,8 +61,8 @@ module Pervasives = { switch (term_of(d)) { | Tuple([d1, d2]) => switch (f(d1, d2)) { - | Ok(r) => r - | Error(e) => EvaluatorError.Exception(e) |> raise + | Ok(r) => Some(r) + | Error(_) => None } | _ => raise(EvaluatorError.Exception(InvalidBoxedTuple(d))) }; @@ -71,8 +72,8 @@ module Pervasives = { switch (term_of(d)) { | Tuple([d1, d2, d3]) => switch (f(d1, d2, d3)) { - | Ok(r) => r - | Error(e) => EvaluatorError.Exception(e) |> raise + | Ok(r) => Some(r) + | Error(_) => None } | _ => raise(EvaluatorError.Exception(InvalidBoxedTuple(d))) }; diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re index 628b493e1d..89633ed371 100644 --- a/src/haz3lcore/dynamics/Evaluator.re +++ b/src/haz3lcore/dynamics/Evaluator.re @@ -23,8 +23,7 @@ open Result; module EvaluatorEVMode: { type status = - | BoxedValue - | Indet + | Final | Uneval; include @@ -32,94 +31,45 @@ module EvaluatorEVMode: { type state = ref(EvaluatorState.t) and type result = (status, DHExp.t); } = { type status = - | BoxedValue - | Indet + | Final | Uneval; type result = (status, DHExp.t); - type reqstate = - | BoxedReady - | IndetReady - | IndetBlocked; - - let (&&) = (x, y) => - switch (x, y) { - | (IndetBlocked, _) => IndetBlocked - | (_, IndetBlocked) => IndetBlocked - | (IndetReady, _) => IndetReady - | (_, IndetReady) => IndetReady - | (BoxedReady, BoxedReady) => BoxedReady - }; - - type requirement('a) = (reqstate, 'a); + type requirement('a) = 'a; - type requirements('a, 'b) = (reqstate, 'a, 'b); // cumulative state, cumulative arguments, cumulative 'undo' + type requirements('a, 'b) = ('a, 'b); // cumulative arguments, cumulative 'undo' type state = ref(EvaluatorState.t); let update_test = (state, id, v) => state := EvaluatorState.add_test(state^, id, v); - let req_value = (f, _, x) => - switch (f(x)) { - | (BoxedValue, x) => (BoxedReady, x) - | (Indet, x) => (IndetBlocked, x) - | (Uneval, _) => failwith("Unexpected Uneval") - }; - - let rec req_all_value = (f, i) => - fun - | [] => (BoxedReady, []) - | [x, ...xs] => { - let (r1, x') = req_value(f, x => x, x); - let (r2, xs') = req_all_value(f, i, xs); - (r1 && r2, [x', ...xs']); - }; - - let req_final = (f, _, x) => - switch (f(x)) { - | (BoxedValue, x) => (BoxedReady, x) - | (Indet, x) => (IndetReady, x) - | (Uneval, _) => failwith("Unexpected Uneval") - }; + let req_final = (f, _, x) => f(x) |> snd; let rec req_all_final = (f, i) => fun - | [] => (BoxedReady, []) + | [] => [] | [x, ...xs] => { - let (r1, x') = req_final(f, x => x, x); - let (r2, xs') = req_all_final(f, i, xs); - (r1 && r2, [x', ...xs']); + let x' = req_final(f, x => x, x); + let xs' = req_all_final(f, i, xs); + [x', ...xs']; }; - let req_final_or_value = (f, _, x) => - switch (f(x)) { - | (BoxedValue, x) => (BoxedReady, (x, true)) - | (Indet, x) => (IndetReady, (x, false)) - | (Uneval, _) => failwith("Unexpected Uneval") - }; - - let otherwise = (_, c) => (BoxedReady, (), c); + let otherwise = (_, c) => ((), c); - let (and.) = ((r1, x1, c1), (r2, x2)) => (r1 && r2, (x1, x2), c1(x2)); + let (and.) = ((x1, c1), x2) => ((x1, x2), c1(x2)); - let (let.) = ((r, x, c), s) => - switch (r, s(x)) { - | (BoxedReady, Step({expr, state_update, is_value: true, _})) => - state_update(); - (BoxedValue, expr); - | (IndetReady, Step({expr, state_update, is_value: true, _})) => + let (let.) = ((x, c), s) => + switch (s(x)) { + | Step({expr, state_update, is_value: true, _}) => state_update(); - (Indet, expr); - | (BoxedReady, Step({expr, state_update, is_value: false, _})) - | (IndetReady, Step({expr, state_update, is_value: false, _})) => + (Final, expr); + | Step({expr, state_update, is_value: false, _}) => state_update(); (Uneval, expr); - | (BoxedReady, Constructor) => (BoxedValue, c) - | (IndetReady, Constructor) => (Indet, c) - | (IndetBlocked, _) => (Indet, c) - | (_, Value) => (BoxedValue, c) - | (_, Indet) => (Indet, c) + | Constructor + | Value + | Indet => (Final, c) }; }; module Eval = Transition(EvaluatorEVMode); @@ -127,8 +77,7 @@ module Eval = Transition(EvaluatorEVMode); let rec evaluate = (state, env, d) => { let u = Eval.transition(evaluate, state, env, d); switch (u) { - | (BoxedValue, x) => (BoxedValue, x) - | (Indet, x) => (Indet, x) + | (Final, x) => (Final, x) | (Uneval, x) => evaluate(state, env, x) }; }; @@ -139,8 +88,7 @@ let evaluate = (env, {d}: Elaborator.Elaboration.t) => { let result = evaluate(state, env, d); let result = switch (result) { - | (BoxedValue, x) => BoxedValue(x |> DHExp.repair_ids) - | (Indet, x) => Indet(x |> DHExp.repair_ids) + | (Final, x) => BoxedValue(x |> DHExp.repair_ids) | (Uneval, x) => Indet(x |> DHExp.repair_ids) }; (state^, result); diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re index 0882fa223f..7418591e8d 100644 --- a/src/haz3lcore/dynamics/EvaluatorStep.re +++ b/src/haz3lcore/dynamics/EvaluatorStep.re @@ -58,17 +58,6 @@ module Decompose = { type requirements('a, 'b) = ('b, Result.t, ClosureEnvironment.t, 'a); type result = Result.t; - let req_value = (cont, wr, d) => { - switch (cont(d)) { - | Result.Indet => (Result.Indet, d) - | Result.BoxedValue => (Result.BoxedValue, d) - | Result.Step(objs) => ( - Result.Step(List.map(EvalObj.wrap(wr), objs)), - d, - ) - }; - }; - let (&&): (Result.t, Result.t) => Result.t = (u, v) => switch (u, v) { @@ -81,18 +70,6 @@ module Decompose = { | (BoxedValue, BoxedValue) => BoxedValue }; - let rec req_all_value' = (cont, wr, ds') => - fun - | [] => (Result.BoxedValue, []) - | [d, ...ds] => { - let (r1, v) = req_value(cont, wr(_, (ds', ds)), d); - let (r2, vs) = req_all_value'(cont, wr, [d, ...ds'], ds); - (r1 && r2, [v, ...vs]); - }; - let req_all_value = (cont, wr, ds) => { - req_all_value'(cont, wr, [], ds); - }; - let req_final = (cont, wr, d) => { ( switch (cont(d)) { @@ -105,17 +82,6 @@ module Decompose = { ); }; - let req_final_or_value = (cont, wr, d) => { - switch (cont(d)) { - | Result.Indet => (Result.BoxedValue, (d, false)) - | Result.BoxedValue => (Result.BoxedValue, (d, true)) - | Result.Step(objs) => ( - Result.Step(List.map(EvalObj.wrap(wr), objs)), - (d, false), - ) - }; - }; - let rec req_all_final' = (cont, wr, ds') => fun | [] => (Result.BoxedValue, []) @@ -175,13 +141,9 @@ module TakeStep = { type result = option(DHExp.t); // Assume that everything is either value or final as required. - let req_value = (_, _, d) => d; - let req_all_value = (_, _, ds) => ds; let req_final = (_, _, d) => d; let req_all_final = (_, _, ds) => ds; - let req_final_or_value = (_, _, d) => (d, true); - let (let.) = (rq: requirements('a, DHExp.t), rl: 'a => rule) => switch (rl(rq)) { | Step({expr, state_update, _}) => diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index 5c936426b9..de904c4532 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -18,11 +18,10 @@ open PatternMatch; to wrap the expression back up if the step couldn't be evaluated. This is followed by a series of `and. d1' = req_final(req(state, env), , )` - which indicate that in order to evaluate the step, must be final. (req_value - is also available if it needs to be a value). Note that if successful, d1' will - be the fully-evaluated version of d1. The sub-expressions are all enumerated by - the field, so i=0 indicates that it is the first sub-expression, i=1 the - second etc. + which indicate that in order to evaluate the step, must be final. Note that + if successful, d1' will be the fully-evaluated version of d1. The sub-expressions + are all enumerated by the field, so i=0 indicates that it is the first + sub-expression, i=1 the second etc. Finally, we have the Step construct that defines the actual step. Note "Step"s should be used if and only if they change the expression. If they do not change @@ -107,16 +106,6 @@ module type EV_MODE = { type requirement('a); type requirements('a, 'b); - let req_value: - (DHExp.t => result, EvalCtx.t => EvalCtx.t, DHExp.t) => - requirement(DHExp.t); - let req_all_value: - ( - DHExp.t => result, - (EvalCtx.t, (list(DHExp.t), list(DHExp.t))) => EvalCtx.t, - list(DHExp.t) - ) => - requirement(list(DHExp.t)); let req_final: (DHExp.t => result, EvalCtx.t => EvalCtx.t, DHExp.t) => requirement(DHExp.t); @@ -127,9 +116,6 @@ module type EV_MODE = { list(DHExp.t) ) => requirement(list(DHExp.t)); - let req_final_or_value: - (DHExp.t => result, EvalCtx.t => EvalCtx.t, DHExp.t) => - requirement((DHExp.t, bool)); let (let.): (requirements('a, DHExp.t), 'a => rule) => result; let (and.): @@ -257,18 +243,13 @@ module Transition = (EV: EV_MODE) => { }); } | Test(d'') => - let. _ = otherwise(env, ((d, _)) => Test(d) |> rewrap) - and. (d', is_value) = - req_final_or_value(req(state, env), d => Test(d) |> wrap_ctx, d''); + let. _ = otherwise(env, d => Test(d) |> rewrap) + and. d' = req_final(req(state, env), d => Test(d) |> wrap_ctx, d''); let result: TestStatus.t = - if (is_value) { - switch (Unboxing.unbox(Bool, d')) { - | DoesNotMatch - | IndetMatch => Indet - | Matches(b) => b ? Pass : Fail - }; - } else { - Indet; + switch (Unboxing.unbox(Bool, d')) { + | DoesNotMatch + | IndetMatch => Indet + | Matches(b) => b ? Pass : Fail }; Step({ expr: Tuple([]) |> fresh, @@ -280,8 +261,9 @@ module Transition = (EV: EV_MODE) => { | TypAp(d, tau) => let. _ = otherwise(env, d => TypAp(d, tau) |> rewrap) and. d' = - req_value(req(state, env), d => TypAp(d, tau) |> wrap_ctx, d); - switch (DHExp.term_of(d')) { + req_final(req(state, env), d => TypAp(d, tau) |> wrap_ctx, d); + let-unbox typfun = (TypFun, d'); + switch (typfun) { | TypFun(utpat, tfbody, name) => /* Rule ITTLam */ Step({ @@ -298,11 +280,7 @@ module Transition = (EV: EV_MODE) => { kind: TypFunAp, is_value: false, }) - | Cast( - d'', - {term: Forall(tp1, _), _} as t1, - {term: Forall(tp2, _), _} as t2, - ) => + | TFunCast(d'', tp1, t1, tp2, t2) => /* Rule ITTApCast */ Step({ expr: @@ -316,7 +294,6 @@ module Transition = (EV: EV_MODE) => { kind: CastTypAp, is_value: false, }) - | _ => raise(EvaluatorError.Exception(InvalidBoxedTypFun(d'))) }; | DeferredAp(d1, ds) => let. _ = otherwise(env, (d1, ds) => DeferredAp(d1, ds) |> rewrap) @@ -334,18 +311,15 @@ module Transition = (EV: EV_MODE) => { ); Value; | Ap(dir, d1, d2) => - let. _ = otherwise(env, (d1, (d2, _)) => Ap(dir, d1, d2) |> rewrap) + let. _ = otherwise(env, (d1, d2) => Ap(dir, d1, d2) |> rewrap) and. 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), - d2 => Ap2(dir, d1, d2) |> wrap_ctx, - d2, - ); - switch (DHExp.term_of(d1')) { + req_final(req(state, env), d1 => Ap1(dir, d1, d2) |> wrap_ctx, d1) + and. d2' = + req_final(req(state, env), d2 => Ap2(dir, d1, d2) |> wrap_ctx, d2); + let-unbox unboxed_fun = (Fun, d1'); + switch (unboxed_fun) { | Constructor(_) => Constructor - | Fun(dp, d3, Some(env'), _) => + | FunEnv(dp, d3, env') => let.match env'' = (env', matches(dp, d2')); Step({ expr: Closure(env'', d3) |> fresh, @@ -353,11 +327,7 @@ module Transition = (EV: EV_MODE) => { kind: FunAp, is_value: false, }); - | Cast( - d3', - {term: Arrow(ty1, ty2), _}, - {term: Arrow(ty1', ty2'), _}, - ) => + | FunCast(d3', ty1, ty2, ty1', ty2') => Step({ expr: Cast( @@ -371,28 +341,21 @@ module Transition = (EV: EV_MODE) => { is_value: false, }) | BuiltinFun(ident) => - if (d2_is_value) { - Step({ - expr: { - let builtin = - VarMap.lookup(Builtins.forms_init, ident) - |> OptUtil.get(() => { - /* This exception should never be raised because there is - no way for the user to create a BuiltinFun. They are all - inserted into the context before evaluation. */ - raise( - EvaluatorError.Exception(InvalidBuiltin(ident)), - ) - }); - builtin(d2'); - }, - state_update, - kind: BuiltinAp(ident), - is_value: false // Not necessarily a value because of InvalidOperations - }); - } else { - Indet; - } + let builtin = + VarMap.lookup(Builtins.forms_init, ident) + |> OptUtil.get(() => { + /* This exception should never be raised because there is + no way for the user to create a BuiltinFun. They are all + inserted into the context before evaluation. */ + raise( + EvaluatorError.Exception(InvalidBuiltin(ident)), + ) + }); + switch (builtin(d2')) { + | Some(expr) => + Step({expr, state_update, kind: BuiltinAp(ident), is_value: false}) + | None => Indet + }; | DeferredAp(d3, d4s) => let n_args = List.length( @@ -430,22 +393,6 @@ module Transition = (EV: EV_MODE) => { kind: DeferredAp, is_value: false, }); - | Cast(_) - | FailedCast(_) => Indet - | FixF(_) => - print_endline(Exp.show(d1)); - print_endline(Exp.show(d1')); - print_endline("FIXF"); - failwith("FixF in Ap"); - | _ => - Step({ - expr: { - raise(EvaluatorError.Exception(InvalidBoxedFun(d1'))); - }, - state_update, - kind: InvalidStep, - is_value: true, - }) }; | Deferral(_) => let. _ = otherwise(env, d); @@ -461,7 +408,7 @@ module Transition = (EV: EV_MODE) => { | If(c, d1, d2) => let. _ = otherwise(env, c => If(c, d1, d2) |> rewrap) and. c' = - req_value(req(state, env), c => If1(c, d1, d2) |> wrap_ctx, c); + req_final(req(state, env), c => If1(c, d1, d2) |> wrap_ctx, c); let-unbox b = (Bool, c'); Step({ expr: { @@ -478,7 +425,7 @@ module Transition = (EV: EV_MODE) => { | UnOp(Int(Minus), d1) => let. _ = otherwise(env, d1 => UnOp(Int(Minus), d1) |> rewrap) and. d1' = - req_value( + req_final( req(state, env), c => UnOp(Int(Minus), c) |> wrap_ctx, d1, @@ -493,7 +440,7 @@ module Transition = (EV: EV_MODE) => { | UnOp(Bool(Not), d1) => let. _ = otherwise(env, d1 => UnOp(Bool(Not), d1) |> rewrap) and. d1' = - req_value( + req_final( req(state, env), c => UnOp(Bool(Not), c) |> wrap_ctx, d1, @@ -508,7 +455,7 @@ module Transition = (EV: EV_MODE) => { | BinOp(Bool(And), d1, d2) => let. _ = otherwise(env, d1 => BinOp(Bool(And), d1, d2) |> rewrap) and. d1' = - req_value( + req_final( req(state, env), d1 => BinOp1(Bool(And), d1, d2) |> wrap_ctx, d1, @@ -523,7 +470,7 @@ module Transition = (EV: EV_MODE) => { | BinOp(Bool(Or), d1, d2) => let. _ = otherwise(env, d1 => BinOp(Bool(Or), d1, d2) |> rewrap) and. d1' = - req_value( + req_final( req(state, env), d1 => BinOp1(Bool(Or), d1, d2) |> wrap_ctx, d1, @@ -538,13 +485,13 @@ module Transition = (EV: EV_MODE) => { | BinOp(Int(op), d1, d2) => let. _ = otherwise(env, (d1, d2) => BinOp(Int(op), d1, d2) |> rewrap) and. d1' = - req_value( + req_final( req(state, env), d1 => BinOp1(Int(op), d1, d2) |> wrap_ctx, d1, ) and. d2' = - req_value( + req_final( req(state, env), d2 => BinOp2(Int(op), d1, d2) |> wrap_ctx, d2, @@ -588,13 +535,13 @@ module Transition = (EV: EV_MODE) => { let. _ = otherwise(env, (d1, d2) => BinOp(Float(op), d1, d2) |> rewrap) and. d1' = - req_value( + req_final( req(state, env), d1 => BinOp1(Float(op), d1, d2) |> wrap_ctx, d1, ) and. d2' = - req_value( + req_final( req(state, env), d2 => BinOp2(Float(op), d1, d2) |> wrap_ctx, d2, @@ -627,13 +574,13 @@ module Transition = (EV: EV_MODE) => { let. _ = otherwise(env, (d1, d2) => BinOp(String(op), d1, d2) |> rewrap) and. d1' = - req_value( + req_final( req(state, env), d1 => BinOp1(String(op), d1, d2) |> wrap_ctx, d1, ) and. d2' = - req_value( + req_final( req(state, env), d2 => BinOp2(String(op), d1, d2) |> wrap_ctx, d2, @@ -664,7 +611,7 @@ module Transition = (EV: EV_MODE) => { and. d1' = req_final(req(state, env), d1 => Cons1(d1, d2) |> wrap_ctx, d1) and. d2' = - req_value(req(state, env), d2 => Cons2(d1, d2) |> wrap_ctx, d2); + req_final(req(state, env), d2 => Cons2(d1, d2) |> wrap_ctx, d2); let-unbox ds = (List, d2'); Step({ expr: ListLit([d1', ...ds]) |> fresh, @@ -675,13 +622,13 @@ module Transition = (EV: EV_MODE) => { | ListConcat(d1, d2) => let. _ = otherwise(env, (d1, d2) => ListConcat(d1, d2) |> rewrap) and. d1' = - req_value( + req_final( req(state, env), d1 => ListConcat1(d1, d2) |> wrap_ctx, d1, ) and. d2' = - req_value( + req_final( req(state, env), d2 => ListConcat2(d1, d2) |> wrap_ctx, d2, diff --git a/src/haz3lcore/dynamics/Unboxing.re b/src/haz3lcore/dynamics/Unboxing.re index 400620026c..07bde372b3 100644 --- a/src/haz3lcore/dynamics/Unboxing.re +++ b/src/haz3lcore/dynamics/Unboxing.re @@ -15,6 +15,17 @@ open Util; the inner lists may still have casts around them after unboxing. */ +type unboxed_tfun = + | TypFun(TPat.t, Exp.t, option(string)) + | TFunCast(DHExp.t, TPat.t, Typ.t, TPat.t, Typ.t); + +type unboxed_fun = + | Constructor(string) + | FunEnv(Pat.t, Exp.t, ClosureEnvironment.t) + | FunCast(DHExp.t, Typ.t, Typ.t, Typ.t, Typ.t) + | BuiltinFun(string) + | DeferredAp(DHExp.t, list(DHExp.t)); + type unbox_request('a) = | Int: unbox_request(int) | Float: unbox_request(float) @@ -24,7 +35,9 @@ type unbox_request('a) = | List: unbox_request(list(DHExp.t)) | Cons: unbox_request((DHExp.t, DHExp.t)) | SumNoArg(string): unbox_request(unit) - | SumWithArg(string): unbox_request(DHExp.t); + | SumWithArg(string): unbox_request(DHExp.t) + | TypFun: unbox_request(unboxed_tfun) + | Fun: unbox_request(unboxed_fun); type unboxed('a) = | DoesNotMatch @@ -135,6 +148,35 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) = }; // There should be some sort of failure here when the cast doesn't go through. + /* Function-like things can look like the following when values */ + | (Fun, Constructor(name, _)) => Matches(Constructor(name)) // Perhaps we should check if the constructor actually is a function? + | (Fun, Fun(dp, d3, Some(env'), _)) => Matches(FunEnv(dp, d3, env')) + | ( + Fun, + Cast( + d3', + {term: Arrow(ty1, ty2), _}, + {term: Arrow(ty1', ty2'), _}, + ), + ) => + Matches(FunCast(d3', ty1, ty2, ty1', ty2')) + | (Fun, BuiltinFun(name)) => Matches(BuiltinFun(name)) + | (Fun, DeferredAp(d1, ds)) => Matches(DeferredAp(d1, ds)) + + /* TypFun-like things can look like the following when values */ + | (TypFun, TypFun(utpat, tfbody, name)) => + Matches(TypFun(utpat, tfbody, name)) + // Note: We might be able to handle this cast like other casts + | ( + TypFun, + Cast( + d'', + {term: Forall(tp1, _), _} as t1, + {term: Forall(tp2, _), _} as t2, + ), + ) => + Matches(TFunCast(d'', tp1, t1, tp2, t2)) + /* Any cast from unknown is indet */ | (_, Cast(_, {term: Unknown(_), _}, _)) => IndetMatch @@ -169,6 +211,8 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) = | SumNoArg(_) | SumWithArg(_) => raise(EvaluatorError.Exception(InvalidBoxedSumConstructor(expr))) + | Fun => raise(EvaluatorError.Exception(InvalidBoxedFun(expr))) + | TypFun => raise(EvaluatorError.Exception(InvalidBoxedTypFun(expr))) } /* Forms that are not yet or will never be a value */ diff --git a/src/haz3lcore/dynamics/ValueChecker.re b/src/haz3lcore/dynamics/ValueChecker.re index a6e5ab30f0..c0eeb22d96 100644 --- a/src/haz3lcore/dynamics/ValueChecker.re +++ b/src/haz3lcore/dynamics/ValueChecker.re @@ -11,66 +11,35 @@ module ValueCheckerEVMode: { type state = unit; type result = t; - type requirement('a) = ('a, (result, bool)); - type requirements('a, 'b) = ('a, (result, bool)); + type requirement('a) = ('a, result); + type requirements('a, 'b) = ('a, result); - let combine = ((r1, b1), (r2, b2)) => ( + let combine = (r1, r2) => switch (r1, r2) { | (Expr, _) => Expr | (_, Expr) => Expr | (Indet, _) => Indet | (_, Indet) => Indet | (Value, Value) => Value - }, - b1 && b2, - ); + }; - let req_value = (vc, _, d) => ( - d, - switch (vc(d)) { - | Value => (Value, true) - | Indet => (Indet, false) - | Expr => (Expr, false) - }, - ); - let req_all_value = (vc, _, ds) => - List.fold_right( - ((v1, r1), (v2, r2)) => ([v1, ...v2], combine(r1, r2)), - List.map(req_value(vc, x => x), ds), - ([], (Value, true)), - ); - let req_final = (vc, _, d) => ( - d, - switch (vc(d)) { - | Value => (Value, true) - | Indet => (Indet, true) - | Expr => (Expr, false) - }, - ); + let req_final = (vc, _, d) => (d, vc(d)); let req_all_final = (vc, _, ds) => List.fold_right( ((v1, r1), (v2, r2)) => ([v1, ...v2], combine(r1, r2)), List.map(req_final(vc, x => x), ds), - ([], (Value, true)), + ([], Value), ); - let req_final_or_value = (vc, _, d) => - switch (vc(d)) { - | Value => ((d, true), (Value, true)) - | Indet => ((d, false), (Value, true)) - | Expr => ((d, false), (Value, false)) - }; - - let otherwise = (_, _) => ((), (Value, true)); + let otherwise = (_, _) => ((), Value); - let (let.) = ((v, (r, b)), rule) => - switch (b, r, rule(v)) { - | (_, _, Constructor) => r - | (_, Expr, Indet) => Expr - | (_, _, Indet) => Indet - | (_, _, Value) => Value - | (true, _, Step(_)) => Expr - | (false, _, Step(_)) => r + let (let.) = ((v, r), rule) => + switch (r, rule(v)) { + | (_, Constructor) => r + | (Expr, Indet) => Expr + | (_, Indet) => Indet + | (_, Value) => Value + | (_, Step(_)) => Expr }; let (and.) = ((v1, r1), (v2, r2)) => { From 01a1d54a436823225c89ae81338ab9863ad42516 Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Fri, 13 Dec 2024 09:25:00 -0500 Subject: [PATCH 2/2] Fix failing test --- test/Test_Evaluator.re | 64 ++++++++++++++++++------------------------ 1 file changed, 28 insertions(+), 36 deletions(-) diff --git a/test/Test_Evaluator.re b/test/Test_Evaluator.re index 37fcaba764..ca85062226 100644 --- a/test/Test_Evaluator.re +++ b/test/Test_Evaluator.re @@ -56,53 +56,45 @@ let tet_ap_of_hole_deferral = () => Ap( Forward, Cast( - Cast( - EmptyHole |> Exp.fresh, - Unknown(Internal) |> Typ.fresh, - Arrow( - Unknown(Internal) |> Typ.fresh, - Unknown(Internal) |> Typ.fresh, - ) - |> Typ.fresh, - ) - |> Exp.fresh, + EmptyHole |> Exp.fresh, + Unknown(Internal) |> Typ.fresh, Arrow( Unknown(Internal) |> Typ.fresh, Unknown(Internal) |> Typ.fresh, ) |> Typ.fresh, - Arrow( - Prod([ + ) + |> Exp.fresh, + Cast( + 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, - ]) - |> Typ.fresh, - Unknown(Internal) |> Typ.fresh, - ) - |> Typ.fresh, - ) - |> Exp.fresh, - Tuple([ - Cast( - Float(1.) |> Exp.fresh, - Float |> Typ.fresh, - Unknown(Internal) |> Typ.fresh, - ) + ) + |> Exp.fresh, + ]) |> Exp.fresh, - Cast( - Bool(true) |> Exp.fresh, - Bool |> Typ.fresh, + Prod([ Unknown(Internal) |> Typ.fresh, - ) - |> Exp.fresh, - Cast( - Int(3) |> Exp.fresh, - Int |> Typ.fresh, Unknown(Internal) |> Typ.fresh, - ) - |> Exp.fresh, - ]) + Unknown(Internal) |> Typ.fresh, + ]) + |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) |> Exp.fresh, ) |> Exp.fresh,