From 26c94ee3766de69e15b73466e97694067aeb6848 Mon Sep 17 00:00:00 2001
From: Alexander Bandukwala <7h3kk1d@gmail.com>
Date: Sun, 3 Nov 2024 18:10:03 -0500
Subject: [PATCH] Added refine for products and arrows

---
 src/haz3lcore/zipper/action/Action.re  | 13 +++++++++----
 src/haz3lcore/zipper/action/Perform.re | 27 ++++++++++++++++++++++++++
 src/haz3lweb/Keyboard.re               |  6 ++++++
 src/haz3lweb/UpdateAction.re           |  3 ++-
 4 files changed, 44 insertions(+), 5 deletions(-)

diff --git a/src/haz3lcore/zipper/action/Action.re b/src/haz3lcore/zipper/action/Action.re
index 85b24be4f1..9a94958619 100644
--- a/src/haz3lcore/zipper/action/Action.re
+++ b/src/haz3lcore/zipper/action/Action.re
@@ -84,7 +84,8 @@ type t =
   | RotateBackpack
   | MoveToBackpackTarget(planar)
   | Pick_up
-  | Put_down;
+  | Put_down
+  | Refine;
 
 module Failure = {
   [@deriving (show({with_path: false}), sexp, yojson)]
@@ -97,7 +98,8 @@ module Failure = {
     | Cant_project
     | CantPaste
     | CantReparse
-    | CantAccept;
+    | CantAccept
+    | CantRefine;
 };
 
 module Result = {
@@ -114,6 +116,7 @@ let is_edit: t => bool =
   | Destruct(_)
   | Pick_up
   | Put_down
+  | Refine
   | Buffer(Accept | Clear | Set(_)) => true
   | Copy
   | Move(_)
@@ -151,7 +154,8 @@ let is_historic: t => bool =
   | Insert(_)
   | Destruct(_)
   | Pick_up
-  | Put_down => true
+  | Put_down
+  | Refine => true
   | Project(p) =>
     switch (p) {
     | SetSyntax(_)
@@ -179,7 +183,8 @@ let prevent_in_read_only_editor = (a: t) => {
   | Pick_up
   | Put_down
   | RotateBackpack
-  | MoveToBackpackTarget(_) => true
+  | MoveToBackpackTarget(_)
+  | Refine => true
   | Project(p) =>
     switch (p) {
     | SetSyntax(_) => true
diff --git a/src/haz3lcore/zipper/action/Perform.re b/src/haz3lcore/zipper/action/Perform.re
index 5a3b90c245..11de75ee43 100644
--- a/src/haz3lcore/zipper/action/Perform.re
+++ b/src/haz3lcore/zipper/action/Perform.re
@@ -30,6 +30,32 @@ let go_z =
   module Move = Move.Make(M);
   module Select = Select.Make(M);
 
+  let refine = (z: Zipper.t) => {
+    switch (Indicated.ci_of(z, meta.statics.info_map)) {
+    | None => None
+    | Some(
+        InfoExp({
+          cls: Exp(EmptyHole),
+          status: NotInHole(Common(Ana(Consistent({ana, _})))),
+          ctx,
+          _,
+        }),
+      ) =>
+      let z =
+        Printer.zipper_of_string(
+          ~zipper_init=z,
+          switch (Typ.term_of(Typ.weak_head_normalize(ctx, ana))) {
+          | Arrow(_, _) => "fun -> "
+          | Prod(tys) =>
+            "(" ++ StringUtil.repeat(List.length(tys) - 1, ", ") ++ ") "
+          | _ => ""
+          },
+        );
+      Option.map(remold_regrout(Left, _), z);
+    | _ => None
+    };
+  };
+
   let paste = (z: Zipper.t, str: string): option(Zipper.t) => {
     open Util.OptUtil.Syntax;
     let* z = Printer.zipper_of_string(~zipper_init=z, str);
@@ -88,6 +114,7 @@ let go_z =
     | None => Error(CantPaste)
     | Some(z) => Ok(z)
     }
+  | Refine => refine(z) |> Result.of_option(~error=Action.Failure.CantRefine)
   | Cut =>
     /* System clipboard handling is done in Page.view handlers */
     switch (Destruct.go(Left, z)) {
diff --git a/src/haz3lweb/Keyboard.re b/src/haz3lweb/Keyboard.re
index 7e4e655f26..2a4dacbe60 100644
--- a/src/haz3lweb/Keyboard.re
+++ b/src/haz3lweb/Keyboard.re
@@ -224,6 +224,12 @@ let shortcuts = (sys: Key.sys): list(shortcut) =>
       "Run Benchmark",
       Benchmark(Start),
     ),
+    mk_shortcut(
+      ~mdIcon="bolt",
+      ~section="Refactoring",
+      "Refine",
+      PerformAction(Refine),
+    ),
   ]
   @ (if (ExerciseSettings.show_instructor) {instructor_shortcuts} else {[]});
 
diff --git a/src/haz3lweb/UpdateAction.re b/src/haz3lweb/UpdateAction.re
index cd2f145f3e..71321eb354 100644
--- a/src/haz3lweb/UpdateAction.re
+++ b/src/haz3lweb/UpdateAction.re
@@ -255,7 +255,8 @@ let should_scroll_to_caret =
     | Paste(_)
     | Copy
     | Cut
-    | Reparse => true
+    | Reparse
+    | Refine => true
     | Project(_)
     | Unselect(_)
     | Select(All) => false