From 2d06ac3f84e7d299b4040b83bc3378016c02ab47 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 1 Oct 2024 15:47:57 -0400 Subject: [PATCH] Cleanup --- src/haz3lcore/dynamics/Elaborator.re | 17 +++++-------- src/haz3lcore/dynamics/Evaluator.re | 2 -- src/haz3lcore/dynamics/Transition.re | 37 +++++++++------------------- 3 files changed, 17 insertions(+), 39 deletions(-) diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index 4dd2d6465a..0f2287bef4 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -334,15 +334,9 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { let a'' = fresh_cast(a', tya, tyf1); Exp.Ap(dir, f'', a'') |> rewrap |> cast_from(tyf2); | DeferredAp(f, args) => - print_endline("DeferredAp"); - print_endline("\t f: " ++ UExp.show(f)); - print_endline("\t args: " ++ [%derive.show: list(UExp.t)](args)); let (f', tyf) = elaborate(m, f); let (args', tys) = List.map(elaborate(m), args) |> ListUtil.unzip; let (tyf1, tyf2) = Typ.matched_arrow(ctx, tyf); - print_endline("\t f': " ++ DHExp.show(f')); - print_endline("\t tyf1: " ++ Typ.show(tyf1)); - print_endline("\t tyf2: " ++ Typ.show(tyf2)); let ty_fargs = Typ.matched_prod(ctx, List.length(args), tyf1); let f'' = fresh_cast( @@ -356,11 +350,12 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { ((arg, _)) => Exp.is_deferral(arg), List.combine(args, ty_fargs), ); - - let remaining_arg_ty = - List.length(remaining_args) == 1 - ? snd(List.hd(remaining_args)) - : Prod(List.map(snd, remaining_args)) |> Typ.temp; + // TODO Should this be a product in the singleton case or not + // let remaining_arg_ty = + // List.length(remaining_args) == 1 + // ? snd(List.hd(remaining_args)) + // : Prod(List.map(snd, remaining_args)) |> Typ.temp; + let remaining_arg_ty = Prod(List.map(snd, remaining_args)) |> Typ.temp; DeferredAp(f'', args'') |> rewrap |> cast_from(Arrow(remaining_arg_ty, tyf2) |> Typ.temp); diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re index 82d1774679..fb877accd7 100644 --- a/src/haz3lcore/dynamics/Evaluator.re +++ b/src/haz3lcore/dynamics/Evaluator.re @@ -124,9 +124,7 @@ module EvaluatorEVMode: { module Eval = Transition(EvaluatorEVMode); let rec evaluate = (state, env, d) => { - print_endline("Evaluating: " ++ DHExp.show(d)); let u = Eval.transition(evaluate, state, env, d); - print_endline("Evaluated: " ++ DHExp.show(snd(u))); switch (u) { | (BoxedValue, x) => (BoxedValue, x) | (Indet, x) => (Indet, x) diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index c9f981f52c..795fce4242 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -315,12 +315,9 @@ module Transition = (EV: EV_MODE) => { kind: CastTypAp, is_value: false, }) - | _ => - print_endline("TypAp raised InvalidBoxedTypFun"); - raise(EvaluatorError.Exception(InvalidBoxedTypFun(d'))); + | _ => raise(EvaluatorError.Exception(InvalidBoxedTypFun(d'))) }; | DeferredAp(d1, ds) => - print_endline("DeferredAp"); let. _ = otherwise(env, (d1, ds) => DeferredAp(d1, ds) |> rewrap) and. _ = req_final( @@ -346,8 +343,6 @@ module Transition = (EV: EV_MODE) => { d2 => Ap2(dir, d1, d2) |> wrap_ctx, d2, ); - print_endline("AP2"); - print_endline("\t d1': " ++ DHExp.show(d1')); switch (DHExp.term_of(d1')) { | Constructor(_) => Constructor | Fun(dp, d3, Some(env'), _) => @@ -385,8 +380,9 @@ module Transition = (EV: EV_MODE) => { /* 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. */ - print_endline("BuiltinFun raised InvalidBuiltin"); - raise(EvaluatorError.Exception(InvalidBuiltin(ident))); + raise( + EvaluatorError.Exception(InvalidBuiltin(ident)), + ) }); builtin(d2'); }, @@ -399,10 +395,6 @@ module Transition = (EV: EV_MODE) => { } /* This case isn't currently used because deferrals are elaborated away */ | DeferredAp(d3, d4s) => - print_endline("DeferredAp in Ap"); - print_endline("\t d2: " ++ DHExp.show(d2)); - print_endline("\t d3: " ++ DHExp.show(d3)); - print_endline("\t d4s: " ++ [%derive.show: list(DHExp.t)](d4s)); let n_args = List.length( List.filter( @@ -412,7 +404,6 @@ module Transition = (EV: EV_MODE) => { d4s, ), ); - print_endline("\tn_args: " ++ string_of_int(n_args)); let-unbox args = if (n_args == 1) { ( @@ -422,7 +413,6 @@ module Transition = (EV: EV_MODE) => { } else { (Tuple(n_args), d2); }; - print_endline("\targs: " ++ [%derive.show: list(Exp.t)](args)); let new_args = { let rec go = (deferred, args) => switch ((deferred: list(Exp.t))) { @@ -436,23 +426,18 @@ module Transition = (EV: EV_MODE) => { go(d4s, args); }; - print_endline( - "\tnew_args: " ++ [%derive.show: list(Exp.t)](new_args), - ); - let ret = Ap(Forward, d3, Tuple(new_args) |> fresh) |> fresh; - print_endline("\tret: " ++ DHExp.show(ret)); - Step({expr: ret, state_update, kind: DeferredAp, is_value: false}); + Step({ + expr: Ap(Forward, d3, Tuple(new_args) |> fresh) |> fresh, + state_update, + 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"); + | FixF(_) => failwith("FixF in Ap") | _ => Step({ expr: { - print_endline("AP raised InvalidBoxedFun"); raise(EvaluatorError.Exception(InvalidBoxedFun(d1'))); }, state_update,