Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Trampoline Evaluator #1427

Closed
wants to merge 2 commits into from
Closed

Trampoline Evaluator #1427

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
65d95fb
remove req-value
Negabinary Dec 2, 2024
3d0bed4
Trampoline Evaluator
Negabinary Dec 4, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 10 additions & 9 deletions src/haz3lcore/dynamics/Builtins.re
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
open Util;
open DHExp;

/*
Expand All @@ -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);

Expand All @@ -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 =>
Expand All @@ -51,17 +52,17 @@ 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
};
};

let binary = (f: (DHExp.t, DHExp.t) => result, d: DHExp.t) => {
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)))
};
Expand All @@ -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)))
};
Expand Down
201 changes: 127 additions & 74 deletions src/haz3lcore/dynamics/Evaluator.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,126 +2,179 @@ open Transition;

open ProgramResult.Result;

// ======== Non-tail recursive evaluator (Obselete) ===========

module EvaluatorEVMode: {
type status =
| BoxedValue
| Indet
| Final
| Uneval;

include
EV_MODE with
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 req_final = (f, _, x) => f(x) |> snd;

let rec req_all_value = (f, i) =>
let rec req_all_final = (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 x' = req_final(f, x => x, x);
let xs' = req_all_final(f, i, xs);
[x', ...xs'];
};

let req_final = (f, _, x) =>
switch (f(x)) {
| (BoxedValue, x) => (BoxedReady, x)
| (Indet, x) => (IndetReady, x)
| (Uneval, _) => failwith("Unexpected Uneval")
};
let otherwise = (_, c) => ((), c);

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 (and.) = ((x1, c1), x2) => ((x1, x2), c1(x2));

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 (let.) = ((x, c), s) =>
switch (s(x)) {
| Step({expr, state_update, is_value: true, _}) =>
state_update();
(Final, expr);
| Step({expr, state_update, is_value: false, _}) =>
state_update();
(Uneval, expr);
| Constructor
| Value
| Indet => (Final, c)
};
};
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);
};
};

let otherwise = (_, c) => (BoxedReady, (), c);
module TrampolineEVMode: {
include
EV_MODE with
type state = ref(EvaluatorState.t) and
type result = Trampoline.t((EvaluatorEVMode.status, DHExp.t));
} = {
open Trampoline.Syntax;

let (and.) = ((r1, x1, c1), (r2, x2)) => (r1 && r2, (x1, x2), c1(x2));
type result = Trampoline.t((EvaluatorEVMode.status, DHExp.t));
type requirement('a) = Trampoline.t('a);
type requirements('a, 'b) = Trampoline.t(('a, 'b));

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, _})) =>
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();
(Indet, expr);
| (BoxedReady, Step({expr, state_update, is_value: false, _}))
| (IndetReady, Step({expr, state_update, is_value: false, _})) =>
Trampoline.return((EvaluatorEVMode.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)
Trampoline.return((EvaluatorEVMode.Uneval, expr));
| Constructor
| Value
| Indet => Trampoline.return((EvaluatorEVMode.Final, c))
};
};
};
module Eval = Transition(EvaluatorEVMode);

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) {
| (BoxedValue, x) => (BoxedValue, x)
| (Indet, x) => (Indet, 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);
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);
Expand Down
38 changes: 0 additions & 38 deletions src/haz3lcore/dynamics/EvaluatorStep.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand All @@ -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)) {
Expand All @@ -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, [])
Expand Down Expand Up @@ -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, _}) =>
Expand Down
Loading
Loading