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

Closure dynamics #1435

Draft
wants to merge 2 commits into
base: dev
Choose a base branch
from
+200 −284
Draft

Closure dynamics #1435

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
4bf139a
remove req-value
Negabinary Dec 2, 2024
e08b269
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
167 changes: 80 additions & 87 deletions src/haz3lcore/dynamics/Evaluator.re
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,126 +21,119 @@ module Result = {

open Result;

// 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 EvaluatorEVMode: {
type status =
| BoxedValue
| Indet
| Final
| Uneval;

include
EV_MODE with
type state = ref(EvaluatorState.t) and type result = (status, DHExp.t);
type state = ref(EvaluatorState.t) and
type result = Trampoline.t((status, DHExp.t));
} = {
open Trampoline.Syntax;

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 requirements('a, 'b) = (reqstate, 'a, 'b); // cumulative state, cumulative arguments, cumulative 'undo'
type result = Trampoline.t((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_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 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 req_final_or_value = (f, _, x) =>
switch (f(x)) {
| (BoxedValue, x) => (BoxedReady, (x, true))
| (Indet, x) => (IndetReady, (x, false))
| (Uneval, _) => failwith("Unexpected Uneval")
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) => (BoxedReady, (), c);

let (and.) = ((r1, x1, c1), (r2, x2)) => (r1 && r2, (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 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((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((Uneval, expr));
| Constructor
| Value
| Indet => Trampoline.return((Final, c))
};
};
};

module Eval = Transition(EvaluatorEVMode);

let rec evaluate = (state, env, d) => {
let u = Eval.transition(evaluate, state, env, d);
open Trampoline.Syntax;
let.trampoline u = Eval.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 = (env, {d}: Elaborator.Elaboration.t) => {
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 = Trampoline.run(result);
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 @@ -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) {
Expand All @@ -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)) {
Expand All @@ -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, [])
Expand Down Expand Up @@ -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, _}) =>
Expand Down
Loading
Loading