From 65d95fbc5209299eca9577528b5af050f7fe4911 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 fc4027f4d6..e1303896c2 100644 --- a/src/haz3lcore/dynamics/Evaluator.re +++ b/src/haz3lcore/dynamics/Evaluator.re @@ -4,8 +4,7 @@ open ProgramResult.Result; module EvaluatorEVMode: { type status = - | BoxedValue - | Indet + | Final | Uneval; include @@ -13,94 +12,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; + type requirement('a) = 'a; - let (&&) = (x, y) => - switch (x, y) { - | (IndetBlocked, _) => IndetBlocked - | (_, IndetBlocked) => IndetBlocked - | (IndetReady, _) => IndetReady - | (_, IndetReady) => IndetReady - | (BoxedReady, BoxedReady) => BoxedReady - }; - - type requirement('a) = (reqstate, '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); @@ -108,8 +58,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) }; }; @@ -120,8 +69,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 3416a46742..bbbe5c1374 100644 --- a/src/haz3lcore/dynamics/EvaluatorStep.re +++ b/src/haz3lcore/dynamics/EvaluatorStep.re @@ -237,17 +237,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) { @@ -260,18 +249,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)) { @@ -284,17 +261,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, []) @@ -354,13 +320,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 c178a49dfa..4dca668399 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 3d0bed42d4140500572790eecbcc100cf7341b60 Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Wed, 4 Dec 2024 13:15:56 -0500 Subject: [PATCH 2/2] Trampoline Evaluator --- src/haz3lcore/dynamics/Evaluator.re | 111 +++++++++++++++++++++++++++- src/haz3lweb/util/WorkerClient.re | 2 +- 2 files changed, 109 insertions(+), 4 deletions(-) diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re index e1303896c2..003732b049 100644 --- a/src/haz3lcore/dynamics/Evaluator.re +++ b/src/haz3lcore/dynamics/Evaluator.re @@ -2,6 +2,8 @@ open Transition; open ProgramResult.Result; +// ======== Non-tail recursive evaluator (Obselete) =========== + module EvaluatorEVMode: { type status = | Final @@ -55,14 +57,117 @@ module EvaluatorEVMode: { }; module Eval = Transition(EvaluatorEVMode); +// let rec evaluate = (state, env, d) => { +// let u = Eval.transition(evaluate, state, env, d); +// switch (u) { +// | (Final, x) => (Final, x) +// | (Uneval, x) => evaluate(state, env, x) +// }; +// }; + +// ======== Evaluator with internal stack (Current) =========== + +// This module defines the stack machine for the evaluator. +module Trampoline = { + type t('a) = + | Bind(t('b), 'b => t('a)): t('a) + | Next(unit => t('a)): t('a) + | Done('a): t('a); + + type callstack('a, 'b) = + | Finished: callstack('a, 'a) + | Continue('a => t('b), callstack('b, 'c)): callstack('a, 'c); + + let rec run: type a b. (t(b), callstack(b, a)) => a = + (t: t(b), callstack: callstack(b, a)) => ( + switch (t) { + | Bind(t, f) => (run(t, Continue(f, callstack)): a) + | Next(f) => run(f(), callstack) + | Done(x) => + switch (callstack) { + | Finished => x + | Continue(f, callstack) => run(f(x), callstack) + } + }: a + ); + + let run = run(_, Finished); + + let return = x => Done(x); + + let bind = (t, f) => Bind(t, f); + + module Syntax = { + let (let.trampoline) = (x, f) => bind(x, f); + }; +}; + +module TrampolineEVMode: { + include + EV_MODE with + type state = ref(EvaluatorState.t) and + type result = Trampoline.t((EvaluatorEVMode.status, DHExp.t)); +} = { + open Trampoline.Syntax; + + type result = Trampoline.t((EvaluatorEVMode.status, DHExp.t)); + type requirement('a) = Trampoline.t('a); + type requirements('a, 'b) = Trampoline.t(('a, 'b)); + + type state = ref(EvaluatorState.t); + let update_test = (state, id, v) => + state := EvaluatorState.add_test(state^, id, v); + + let req_final = (f, _, x) => { + let.trampoline x' = Next(() => f(x)); + Trampoline.return(x' |> snd); + }; + let rec req_all_final = (f, i, xs) => + switch (xs) { + | [] => Trampoline.return([]) + | [x, ...xs] => + let.trampoline x' = req_final(f, x => x, x); + let.trampoline xs' = req_all_final(f, i, xs); + Trampoline.return([x', ...xs']); + }; + + let otherwise = (_, c) => Trampoline.return(((), c)); + let (and.) = (t1, t2) => { + let.trampoline (x1, c1) = t1; + let.trampoline x2 = t2; + Trampoline.return(((x1, x2), c1(x2))); + }; + let (let.) = (t1, s) => { + let.trampoline (x, c) = t1; + switch (s(x)) { + | Step({expr, state_update, is_value: true, _}) => + state_update(); + Trampoline.return((EvaluatorEVMode.Final, expr)); + | Step({expr, state_update, is_value: false, _}) => + state_update(); + Trampoline.return((EvaluatorEVMode.Uneval, expr)); + | Constructor + | Value + | Indet => Trampoline.return((EvaluatorEVMode.Final, c)) + }; + }; +}; + +module TrampolineEval = Transition(TrampolineEVMode); + let rec evaluate = (state, env, d) => { - let u = Eval.transition(evaluate, state, env, d); + open Trampoline.Syntax; + let.trampoline u = TrampolineEval.transition(evaluate, state, env, d); switch (u) { - | (Final, x) => (Final, x) - | (Uneval, x) => evaluate(state, env, x) + | (Final, x) => (EvaluatorEVMode.Final, x) |> Trampoline.return + | (Uneval, x) => Trampoline.Next(() => evaluate(state, env, x)) }; }; +let evaluate = (state, env, d) => { + evaluate(state, env, d) |> Trampoline.run; +}; + let evaluate' = (env, {d, _}: Elaborator.Elaboration.t) => { let state = ref(EvaluatorState.init); let env = ClosureEnvironment.of_environment(env); diff --git a/src/haz3lweb/util/WorkerClient.re b/src/haz3lweb/util/WorkerClient.re index 92faffe6a9..276eedff01 100644 --- a/src/haz3lweb/util/WorkerClient.re +++ b/src/haz3lweb/util/WorkerClient.re @@ -2,7 +2,7 @@ open Js_of_ocaml; open WorkerServer; let name = "worker.js"; // Worker file name -let timeoutDuration = 20000; // Worker timeout in ms +let timeoutDuration = 200000000; // Worker timeout in ms let initWorker = () => Worker.create(name);