Skip to content

Commit

Permalink
remove req-value
Browse files Browse the repository at this point in the history
  • Loading branch information
@Negabinary
Negabinary committed Dec 5, 2024
1 parent 297b04b commit 4bf139a
Show file tree
Hide file tree
Showing 6 changed files with 141 additions and 270 deletions.
19 changes: 10 additions & 9 deletions src/haz3lcore/dynamics/Builtins.re
View file
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
94 changes: 21 additions & 73 deletions src/haz3lcore/dynamics/Evaluator.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,112 +23,61 @@ open Result;

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 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);

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)
};
};
Expand All @@ -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);
Expand Down
38 changes: 0 additions & 38 deletions src/haz3lcore/dynamics/EvaluatorStep.re
View file
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

0 comments on commit 4bf139a

Please sign in to comment.