Cleanup

hazelgrove · Oct 1, 2024 · 2d06ac3 · 2d06ac3
1 parent 6f24600
commit 2d06ac3
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 39 deletions.
diff --git 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
@@ -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
@@ -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,