Editor Componentization (#1297)

Makefile

@@ -18,10 +18,10 @@ change-deps:
 	sed -i'.old' '/host-/d' hazel.opam.locked  # remove host- lines which are arch-specific. Not using -i '' because of portability issues https://stackoverflow.com/questions/4247068/sed-command-with-i-option-failing-on-mac-but-works-on-linux
 
 setup-instructor:
-	cp src/haz3lweb/ExerciseSettings_instructor.re src/haz3lweb/ExerciseSettings.re
+	cp src/haz3lweb/exercises/settings/ExerciseSettings_instructor.re src/haz3lweb/exercises/settings/ExerciseSettings.re
 
 setup-student: 
-	cp src/haz3lweb/ExerciseSettings_student.re src/haz3lweb/ExerciseSettings.re
+	cp src/haz3lweb/exercises/settings/ExerciseSettings_student.re src/haz3lweb/exercises/settings/ExerciseSettings.re
 
 dev-helper:
 	dune fmt --auto-promote || true

docs/ui-architecture.md

@@ -0,0 +1,90 @@
+# UI Architecture Guide
+
+Last updated 2024-11-22
+
+Since [#1297](https://github.com/hazelgrove/hazel/pull/1297), the UI portion of Hazel is split into components, where each component is a file that follows the following format with inner modules:
+
+```reason
+module Model { ... }
+
+module Update { ... }
+
+(optional)
+module Selection { ... }
+
+module View { ... }
+
+```
+
+This roughly follows the elm architecture for an application where 
+* an application's current state is stored using a `Model.t`, 
+* an `Update.update` function takes an action (`Update.t`) and a `Model.t` and returns the next `Model.t`
+* a `View.view` function takes the current state of the model, and returns a virtual DOM (our representation of HTML)
+
+
+
+## What goes in the `Model.t`?
+
+Anything that describes the current state of the Hazel editor goes in `Model.t`. This includes:
+
+* The `Model.t` of subcomponents
+
+* Any values that can be directly manipulated by the user (Often annotated with a `\\ UPDATED` comment)
+
+* Anything we don't want to recalculate every redraw (Often annotated with a `\\ CALCULATED` comment)
+
+If the `Model.t` includes some things that we may not want to save (e.g. the typing information of the current editor), as well as `Model.t`, we also include a similar `Model.persistent` type, along with functions `Model.persist` and `Model.unpersist` to convert.
+
+## `Update.update` and `Update.calculate`
+
+Inside the `Update` module, there are two important functions:
+
+`Update.update : (~settings: Settings.t, Update.t, Model.t) -> Updated.t(Model.t)`
+
+`Update.calculate : (~settings: Settings.t, Model.t, ...) -> Model.t`
+
+The `update` function always runs first, and makes minimal changes to record the intention of the user in the model. (e.g. if the user types some text, add the text to the segment). The `calculate` function runs next and and works out all the downstream changes. (e.g. updating the statics, and starting evaluation), 
+
+These two functions are separated for a couple reasons:
+
+* An `update` on some specific ui element in the program may want to trigger a `calculate` everywhere else in the app (e.g. to re-evaluate the user's program). 
+
+* Looking to the future, we will want to eventually use the Bonsai library to incrementalize the `calculate` step.
+
+The result of `Update.update` is wrapped in a `Updated.t(...)` which, among other things, records whether the entire app should recalculate after this change. If you return `Updated.return(model)` it will recalculate, and if you return `Updated.return_quiet(model)` it won't recalculate. If you're not sure it's generally safer to use `return`. Look at the optional arguments on `return` if you want more control over what gets recalculated.
+
+## Selection
+
+The `Selection` module is only required if it's possible for this component or a component inside this component to be active (i.e. has the cursor, takes key events).
+
+`Selection.t` is a data structure that can store where within this component the selection currently is.
+
+The other functions in `Selection` help the app make decisions based on the current selection, e.g. what to do on key presses, what type to show at the bottom of the screen.
+
+## View
+
+The view function usually has the following signature:
+
+```
+let view =
+      (
+        ~globals,
+        ~selected: option(Selection.t),
+        ~inject: Update.t => Ui_effect.t(unit),
+        ~signal: event => Ui_effect.t(unit),
+        model: Model.t,
+      ) => Node.t
+```
+
+`~globals` provides access to global values such as settings, fonts, etc. 
+
+`~selected` tells you whether the current element is selected
+
+`~inject` lets you perform an update action at this component, e.g. in response to a click or other user input
+
+`~signal` is a way to propagate events, such as clicks, upwards to this component's parent.
+
+## The Future
+
+This system could be viewed as an in-between state, between the original implementation (with one large model and update type) and a fully-incremental Bonsai implementation (where subcomponent inclusion and downstream calculation are handled fully by Bonsai).
+

src/haz3lcore/dynamics/Builtins.re

@@ -264,14 +264,25 @@ module Pervasives = {
         }
       );
 
-    let string_sub = _ =>
+    let string_sub = name =>
       ternary((d1, d2, d3) =>
         switch (term_of(d1), term_of(d2), term_of(d3)) {
         | (String(s), Int(idx), Int(len)) =>
           try(Ok(String(String.sub(s, idx, len)) |> fresh)) {
           | _ =>
             // TODO: make it clear that the problem could be with d3 too
-            Ok(DynamicErrorHole(d2, IndexOutOfBounds) |> fresh)
+            Ok(
+              DynamicErrorHole(
+                Ap(
+                  Forward,
+                  BuiltinFun(name) |> fresh,
+                  Tuple([d1, d2, d3]) |> fresh,
+                )
+                |> fresh,
+                IndexOutOfBounds,
+              )
+              |> fresh,
+            )
           }
         | (String(_), Int(_), _) => Error(InvalidBoxedIntLit(d3))
         | (String(_), _, _) => Error(InvalidBoxedIntLit(d2))

src/haz3lcore/dynamics/Casts.re

@@ -125,19 +125,28 @@ let rec transition = (~recursive=false, d: DHExp.t): option(DHExp.t) => {
 
     | (Hole, NotGroundOrHole(t2_grounded)) =>
       /* ITExpand rule */
-      let inner_cast = Cast(d1, t1, t2_grounded) |> DHExp.fresh;
+      let inner_cast =
+        Cast(d1, t1, t2_grounded |> DHExp.replace_all_ids_typ) |> DHExp.fresh;
       // HACK: we need to check the inner cast here
       let inner_cast =
         switch (transition(~recursive, inner_cast)) {
         | Some(d1) => d1
         | None => inner_cast
         };
-      Some(Cast(inner_cast, t2_grounded, t2) |> DHExp.fresh);
+      Some(
+        Cast(inner_cast, t2_grounded |> DHExp.replace_all_ids_typ, t2)
+        |> DHExp.fresh,
+      );
 
     | (NotGroundOrHole(t1_grounded), Hole) =>
       /* ITGround rule */
       Some(
-        Cast(Cast(d1, t1, t1_grounded) |> DHExp.fresh, t1_grounded, t2)
+        Cast(
+          Cast(d1, t1, t1_grounded |> DHExp.replace_all_ids_typ)
+          |> DHExp.fresh,
+          t1_grounded |> DHExp.replace_all_ids_typ,
+          t2,
+        )
         |> DHExp.fresh,
       )
 

src/haz3lcore/dynamics/DHExp.re

@@ -14,16 +14,6 @@ let mk = (ids, term): t => {
   {ids, copied: true, term};
 };
 
-// TODO: make this function emit a map of changes
-let replace_all_ids =
-  map_term(
-    ~f_exp=(continue, exp) => {...exp, ids: [Id.mk()]} |> continue,
-    ~f_pat=(continue, exp) => {...exp, ids: [Id.mk()]} |> continue,
-    ~f_typ=(continue, exp) => {...exp, ids: [Id.mk()]} |> continue,
-    ~f_tpat=(continue, exp) => {...exp, ids: [Id.mk()]} |> continue,
-    ~f_rul=(continue, exp) => {...exp, ids: [Id.mk()]} |> continue,
-  );
-
 // TODO: make this function emit a map of changes
 let repair_ids =
   map_term(
@@ -34,6 +24,32 @@ let repair_ids =
         } else {
           continue(exp);
         },
+    ~f_typ=
+      (continue, typ) =>
+        if (Typ.rep_id(typ) == Id.invalid) {
+          replace_all_ids_typ(typ);
+        } else {
+          continue(typ);
+        },
+    _,
+  );
+
+let repair_ids_typ =
+  Typ.map_term(
+    ~f_exp=
+      (continue, exp) =>
+        if (Exp.rep_id(exp) == Id.invalid) {
+          replace_all_ids(exp);
+        } else {
+          continue(exp);
+        },
+    ~f_typ=
+      (continue, typ) =>
+        if (typ.copied) {
+          replace_all_ids_typ(typ);
+        } else {
+          continue(typ);
+        },
     _,
   );
 
@@ -79,8 +95,9 @@ let rec strip_casts =
         | Undefined
         | If(_) => continue(exp)
         /* Remove casts*/
-        | FailedCast(d, _, _)
         | Cast(d, _, _) => strip_casts(d)
+        /* Keep failed casts*/
+        | FailedCast(_, _, _) => continue(exp)
         }
       },
     _,

src/haz3lcore/dynamics/DHPat.re

@@ -32,23 +32,3 @@ let rec binds_var = (m: Statics.Map.t, x: Var.t, dp: t): bool =>
     | Ap(_, _) => false
     }
   };
-
-let rec bound_vars = (dp: t): list(Var.t) =>
-  switch (dp |> term_of) {
-  | EmptyHole
-  | MultiHole(_)
-  | Wild
-  | Invalid(_)
-  | Int(_)
-  | Float(_)
-  | Bool(_)
-  | String(_)
-  | Constructor(_) => []
-  | Cast(y, _, _)
-  | Parens(y) => bound_vars(y)
-  | Var(y) => [y]
-  | Tuple(dps) => List.flatten(List.map(bound_vars, dps))
-  | Cons(dp1, dp2) => bound_vars(dp1) @ bound_vars(dp2)
-  | ListLit(dps) => List.flatten(List.map(bound_vars, dps))
-  | Ap(_, dp1) => bound_vars(dp1)
-  };

src/haz3lcore/dynamics/Evaluator.re

@@ -1,25 +1,6 @@
 open Transition;
 
-module Result = {
-  [@deriving (show({with_path: false}), sexp, yojson)]
-  type t =
-    | BoxedValue(DHExp.t)
-    | Indet(DHExp.t);
-
-  let unbox =
-    fun
-    | BoxedValue(d)
-    | Indet(d) => d;
-
-  let fast_equal = (r1, r2) =>
-    switch (r1, r2) {
-    | (BoxedValue(d1), BoxedValue(d2))
-    | (Indet(d1), Indet(d2)) => DHExp.fast_equal(d1, d2)
-    | _ => false
-    };
-};
-
-open Result;
+open ProgramResult.Result;
 
 module EvaluatorEVMode: {
   type status =
@@ -133,7 +114,7 @@ let rec evaluate = (state, env, d) => {
   };
 };
 
-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);
@@ -145,3 +126,20 @@ let evaluate = (env, {d}: Elaborator.Elaboration.t) => {
     };
   (state^, result);
 };
+
+let evaluate =
+    (~settings: CoreSettings.t, ~env=Builtins.env_init, elab: DHExp.t)
+    : ProgramResult.t(ProgramResult.inner) =>
+  switch () {
+  | _ when !settings.dynamics => Off({d: elab})
+  | _ =>
+    switch (evaluate'(env, {d: elab})) {
+    | exception (EvaluatorError.Exception(reason)) =>
+      print_endline("EvaluatorError:" ++ EvaluatorError.show(reason));
+      ResultFail(EvaulatorError(reason));
+    | exception exn =>
+      print_endline("EXN:" ++ Printexc.to_string(exn));
+      ResultFail(UnknownException(Printexc.to_string(exn)));
+    | (state, result) => ResultOk({result, state})
+    }
+  };