Final tutorial sys

src/haz3lcore/lang/term/TermBase.re

@@ -118,7 +118,11 @@
         ~f_typ=continue,
         ~f_tpat=continue,
         ~f_rul=continue,
-        ~f_any=continue,
+        // ~f_any=continue,
+        ~f_any=(rec_call, x) => {
+                 print_endline("Breaking recursion at ~f_any");
+                 rec_call(x);
+               }, /* just return the input without recursing */
         x: any_t,
       ) => {
     let rec_call = (y: any_t): any_t =>

src/haz3lcore/statics/Elaborator.re

@@ -32,6 +32,7 @@ let fresh_cast = (d: DHExp.t, t1: Typ.t, t2: Typ.t): Exp.t => {
 };
 
 let fresh_pat_cast = (p: DHPat.t, t1: Typ.t, t2: Typ.t): DHPat.t => {
+  print_endline("fresh_pat_cast");
   switch (p.term) {
   | Label(_) => p
   | _ =>
@@ -279,6 +280,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: Exp.t): (DHExp.t, Typ.t) => {
 
   let (elaborated_type, ana, ctx, co_ctx, statics_pseudo_elaborated) =
     elaborated_type(m, uexp);
+
   let cast_from = (ty, exp) => fresh_cast(exp, ty, elaborated_type);
   let (_, rewrap) = Exp.unwrap(uexp);
   let uexp = rewrap(statics_pseudo_elaborated.term);

src/haz3lweb/Export.re

@@ -6,6 +6,7 @@ type all = {
   explainThisModel: string,
   scratch: string,
   exercise: string,
+  tutorial: string,
   documentation: string,
   log: string,
 };
@@ -16,6 +17,7 @@ type all_f22 = {
   settings: string,
   scratch: string,
   exercise: string,
+  tutorial: string,
   log: string,
 };
 
@@ -24,6 +26,8 @@ let mk_all = (~core_settings, ~instructor_mode, ~log) => {
   let explainThisModel = ExplainThisModel.Store.export();
   let scratch = ScratchMode.Store.export();
   let documentation = ScratchMode.StoreDocumentation.export();
+  let tutorial =
+    TutorialsMode.Store.export(~settings=core_settings, ~instructor_mode);
   let exercise =
     ExercisesMode.Store.export(~settings=core_settings, ~instructor_mode);
   {
@@ -32,6 +36,7 @@ let mk_all = (~core_settings, ~instructor_mode, ~log) => {
     scratch,
     documentation,
     exercise,
+    tutorial,
     log,
   };
 };
@@ -40,7 +45,7 @@ let export_all = (~settings, ~instructor_mode, ~log) => {
   mk_all(~core_settings=settings, ~instructor_mode, ~log) |> yojson_of_all;
 };
 
-let import_all = (~import_log: string => unit, data, ~specs) => {
+let import_all = (~import_log: string => unit, data, ~specs, ~tutorial_specs) => {
   let all =
     try(data |> Yojson.Safe.from_string |> all_of_yojson) {
     | _ =>
@@ -49,6 +54,7 @@ let import_all = (~import_log: string => unit, data, ~specs) => {
         settings: all_f22.settings,
         scratch: all_f22.scratch,
         documentation: "",
+        tutorial: all_f22.tutorial,
         exercise: all_f22.exercise,
         log: all_f22.log,
         explainThisModel: "",
@@ -65,6 +71,12 @@ let import_all = (~import_log: string => unit, data, ~specs) => {
     ~specs,
     ~instructor_mode,
   );
+  TutorialsMode.Store.import(
+    ~settings=settings.core,
+    all.tutorial,
+    ~tutorial_specs,
+    ~instructor_mode,
+  );
   import_log(all.log);
 };
 

src/haz3lweb/Store.re

@@ -7,6 +7,8 @@ type key =
   | Mode
   | Scratch
   | Documentation
+  | Tutorial(Haz3lcore.Id.t)
+  | CurrentTutorial
   | CurrentExercise
   | Exercise(Exercise.key);
 
@@ -17,6 +19,8 @@ let key_to_string =
   | Mode => "MODE"
   | Scratch => "SAVE_SCRATCH"
   | Documentation => "SAVE_DOCUMENTATION"
+  | Tutorial(id) => Haz3lcore.Id.to_string(id)
+  | CurrentTutorial => "CUR_TUTORIAL"
   | CurrentExercise => "CUR_EXERCISE"
   | Exercise(key) => key |> Exercise.sexp_of_key |> Sexplib.Sexp.to_string;
 

src/haz3lweb/app/common/Icons.re

@@ -231,3 +231,5 @@ let command_palette_sparkle =
       "m554.76 426.6c6.5195-23.285 24.715-41.48 48-48-23.297-6.5-41.5-24.707-48-48-6.5 23.293-24.707 41.5-48 48 23.281 6.5195 41.477 24.715 48 48z",
     ],
   );
+
+let next = Node.text("➡️");

src/haz3lweb/app/common/Widgets.re

@@ -79,3 +79,15 @@ let file_select_button_named = (~tooltip="", id, icon, on_input) =>
     ~attrs=[clss(["named-menu-item"])],
     [file_select_button(id, icon, on_input), div([text(tooltip)])],
   );
+
+let menu_item = (~label, ~on_click) =>
+  div(~attrs=[Attr.on_click(_ => on_click())], [text(label)]);
+
+let dropdown = (~label, ~items) =>
+  div(
+    ~attrs=[Attr.class_("dropdown-container")],
+    [
+      div(~attrs=[Attr.class_("dropdown-label")], [text(label)]),
+      div(~attrs=[Attr.class_("dropdown-menu")], items),
+    ],
+  );

src/haz3lweb/app/editors/Editors.re

@@ -3,18 +3,21 @@ module Model = {
   type mode =
     | Scratch
     | Documentation
+    | Tutorial
     | Exercises;
 
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t =
     | Scratch(ScratchMode.Model.t)
     | Documentation(ScratchMode.Model.t)
+    | Tutorial(TutorialsMode.Model.t)
     | Exercises(ExercisesMode.Model.t);
 
   let mode_string: t => string =
     fun
     | Scratch(_) => "Scratch"
     | Documentation(_) => "Documentation"
+    | Tutorial(_) => "Tutorial"
     | Exercises(_) => "Exercises";
 };
 
@@ -41,6 +44,11 @@ module Store = {
         ScratchMode.StoreDocumentation.load()
         |> ScratchMode.Model.unpersist_documentation(~settings),
       )
+    | Tutorial =>
+      Model.Tutorial(
+        TutorialsMode.Store.load(~settings, ~instructor_mode)
+        |> TutorialsMode.Model.unpersist(~settings, ~instructor_mode),
+      )
     | Exercises =>
       Model.Exercises(
         ExercisesMode.Store.load(~settings, ~instructor_mode)
@@ -59,6 +67,9 @@ module Store = {
       ScratchMode.StoreDocumentation.save(
         ScratchMode.Model.persist_documentation(m),
       );
+    | Model.Tutorial(m) =>
+      StoreMode.save(Tutorial);
+      TutorialsMode.Store.save(~instructor_mode, m);
     | Model.Exercises(m) =>
       StoreMode.save(Exercises);
       ExercisesMode.Store.save(~instructor_mode, m);
@@ -74,6 +85,7 @@ module Update = {
     | SwitchMode(Model.mode)
     // Scratch & Documentation
     | Scratch(ScratchMode.Update.t)
+    | Tutorial(TutorialsMode.Update.t)
     // Exercises
     | Exercises(ExercisesMode.Update.t);
 
@@ -99,6 +111,15 @@ module Update = {
           m,
         );
       Model.Documentation(scratch);
+    | (Tutorial(action), Tutorial(m)) =>
+      let* exercises =
+        TutorialsMode.Update.update(
+          ~globals,
+          ~schedule_action=a => schedule_action(Tutorial(a)),
+          action,
+          m,
+        );
+      Model.Tutorial(exercises);
     | (Exercises(action), Exercises(m)) =>
       let* exercises =
         ExercisesMode.Update.update(
@@ -108,11 +129,17 @@ module Update = {
           m,
         );
       Model.Exercises(exercises);
+    | (Tutorial(_), Exercises(_))
+    | (Tutorial(_), Scratch(_))
+    | (Tutorial(_), Documentation(_))
     | (Scratch(_), Exercises(_))
+    | (Scratch(_), Tutorial(_))
     | (Exercises(_), Scratch(_))
+    // | (Exercises(_), Exercises(_))
     | (Exercises(_), Documentation(_)) => model |> return_quiet
     | (SwitchMode(Scratch), Scratch(_))
     | (SwitchMode(Documentation), Documentation(_))
+    | (Exercises(_), Tutorial(_)) => model |> return_quiet
     | (SwitchMode(Exercises), Exercises(_)) => model |> return_quiet
     | (SwitchMode(Scratch), _) =>
       Model.Scratch(
@@ -128,6 +155,19 @@ module Update = {
            ),
       )
       |> return
+    | (SwitchMode(Tutorial), Tutorial(_)) => model |> return_quiet
+    | (SwitchMode(Tutorial), _) =>
+      Model.Tutorial(
+        TutorialsMode.Store.load(
+          ~settings=globals.settings.core,
+          ~instructor_mode=globals.settings.instructor_mode,
+        )
+        |> TutorialsMode.Model.unpersist(
+             ~settings=globals.settings.core,
+             ~instructor_mode=globals.settings.instructor_mode,
+           ),
+      )
+      |> return
     | (SwitchMode(Exercises), _) =>
       Model.Exercises(
         ExercisesMode.Store.load(
@@ -163,6 +203,15 @@ module Update = {
           m,
         ),
       )
+    | Model.Tutorial(m) =>
+      Model.Tutorial(
+        TutorialsMode.Update.calculate(
+          ~schedule_action=a => schedule_action(Tutorial(a)),
+          ~settings,
+          ~is_edited,
+          m,
+        ),
+      )
     | Model.Exercises(m) =>
       Model.Exercises(
         ExercisesMode.Update.calculate(
@@ -181,7 +230,8 @@ module Selection = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t =
     | Scratch(ScratchMode.Selection.t)
-    | Exercises(ExerciseMode.Selection.t);
+    | Exercises(ExerciseMode.Selection.t)
+    | Tutorial(TutorialMode.Selection.t);
 
   let get_cursor_info = (~selection: t, editors: Model.t): cursor(Update.t) => {
     switch (selection, editors) {
@@ -191,11 +241,19 @@ module Selection = {
     | (Scratch(selection), Documentation(m)) =>
       let+ ci = ScratchMode.Selection.get_cursor_info(~selection, m);
       Update.Scratch(ci);
+    | (Tutorial(selection), Tutorial(m)) =>
+      let+ ci = TutorialsMode.Selection.get_cursor_info(~selection, m);
+      Update.Tutorial(ci);
     | (Exercises(selection), Exercises(m)) =>
       let+ ci = ExercisesMode.Selection.get_cursor_info(~selection, m);
       Update.Exercises(ci);
+    | (Scratch(_), Tutorial(_))
+    | (Exercises(_), Tutorial(_))
     | (Scratch(_), Exercises(_))
     | (Exercises(_), Scratch(_))
+    | (Tutorial(_), Scratch(_))
+    | (Tutorial(_), Exercises(_))
+    | (Tutorial(_), Documentation(_))
     | (Exercises(_), Documentation(_)) => empty
     };
   };
@@ -209,12 +267,20 @@ module Selection = {
     | (Some(Scratch(selection)), Documentation(m)) =>
       ScratchMode.Selection.handle_key_event(~selection, ~event, m)
       |> Option.map(x => Update.Scratch(x))
+    | (Some(Tutorial(selection)), Tutorial(m)) =>
+      TutorialsMode.Selection.handle_key_event(~selection, ~event, m)
+      |> Option.map(x => Update.Tutorial(x))
     | (Some(Exercises(selection)), Exercises(m)) =>
       ExercisesMode.Selection.handle_key_event(~selection, ~event, m)
       |> Option.map(x => Update.Exercises(x))
     | (Some(Scratch(_)), Exercises(_))
+    | (Some(Scratch(_)), Tutorial(_))
+    | (Some(Exercises(_)), Tutorial(_))
     | (Some(Exercises(_)), Scratch(_))
     | (Some(Exercises(_)), Documentation(_))
+    | (Some(Tutorial(_)), Scratch(_))
+    | (Some(Tutorial(_)), Documentation(_))
+    | (Some(Tutorial(_)), Exercises(_))
     | (None, _) => None
     };
   };
@@ -228,6 +294,9 @@ module Selection = {
     | Documentation(m) =>
       ScratchMode.Selection.jump_to_tile(tile, m)
       |> Option.map(((x, y)) => (Update.Scratch(x), Scratch(y)))
+    | Tutorial(m) =>
+      TutorialsMode.Selection.jump_to_tile(~settings, tile, m)
+      |> Option.map(((x, y)) => (Update.Tutorial(x), Tutorial(y)))
     | Exercises(m) =>
       ExercisesMode.Selection.jump_to_tile(~settings, tile, m)
       |> Option.map(((x, y)) => (Update.Exercises(x), Exercises(y)))
@@ -237,6 +306,7 @@ module Selection = {
     fun
     | Model.Scratch(_) => Scratch(MainEditor)
     | Model.Documentation(_) => Scratch(MainEditor)
+    | Model.Tutorial(_) => Tutorial((Tutorial.YourImpl, MainEditor))
     | Model.Exercises(_) => Exercises((Exercise.Prelude, MainEditor));
 };
 
@@ -284,6 +354,20 @@ module View = {
         ~inject=a => Update.Scratch(a) |> inject,
         m,
       )
+    | Tutorial(m) =>
+      TutorialsMode.View.view(
+        ~signal=
+          fun
+          | MakeActive(s) => signal(MakeActive(Tutorial(s))),
+        ~globals,
+        ~selection=
+          switch (selection) {
+          | Some(Tutorial(s)) => Some(s)
+          | _ => None
+          },
+        ~inject=a => Update.Tutorial(a) |> inject,
+        m,
+      )
     | Exercises(m) =>
       ExercisesMode.View.view(
         ~signal=
@@ -309,6 +393,12 @@ module View = {
         ~inject=x => inject(Update.Scratch(x)),
         s,
       )
+    | Tutorial(e) =>
+      TutorialsMode.View.file_menu(
+        ~globals,
+        ~inject=x => inject(Update.Tutorial(x)),
+        e,
+      )
     | Exercises(e) =>
       ExercisesMode.View.file_menu(
         ~globals,
@@ -329,6 +419,7 @@ module View = {
                 fun
                 | "Scratch" => inject(Update.SwitchMode(Scratch))
                 | "Documentation" => inject(Update.SwitchMode(Documentation))
+                | "Tutorial" => inject(Update.SwitchMode(Tutorial))
                 | "Exercises" => inject(Update.SwitchMode(Exercises))
                 | _ => failwith("Invalid mode")
               ),
@@ -338,10 +429,11 @@ module View = {
                 switch (editors) {
                 | Scratch(_) => "Scratch"
                 | Documentation(_) => "Documentation"
+                | Tutorial(_) => "Tutorial"
                 | Exercises(_) => "Exercises"
                 },
               ),
-              ["Scratch", "Documentation", "Exercises"],
+              ["Scratch", "Documentation", "Tutorial", "Exercises"],
             ),
           ),
         ],
@@ -363,6 +455,12 @@ module View = {
           ~inject=a => Update.Scratch(a) |> inject,
           m,
         )
+      | Tutorial(m) =>
+        TutorialsMode.View.top_bar(
+          ~globals,
+          ~inject=a => Update.Tutorial(a) |> inject,
+          m,
+        )
       | Exercises(m) =>
         ExercisesMode.View.top_bar(
           ~globals,