Editor Componentization

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

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(DHExp.Cast(inner_cast, t2_grounded, t2) |> DHExp.fresh);
+      Some(
+        DHExp.Cast(inner_cast, t2_grounded |> DHExp.replace_all_ids_typ, t2)
+        |> DHExp.fresh,
+      );
 
     | (NotGroundOrHole(t1_grounded), Hole) =>
       /* ITGround rule */
       Some(
-        DHExp.Cast(Cast(d1, t1, t1_grounded) |> DHExp.fresh, t1_grounded, t2)
+        DHExp.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,15 +14,17 @@ 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,
+let (replace_all_ids, replace_all_ids_typ) = {
+  let f:
+    'a.
+    (IdTagged.t('a) => IdTagged.t('a), IdTagged.t('a)) => IdTagged.t('a)
+   =
+    (continue, exp) => {...exp, ids: [Id.mk()]} |> continue;
+  (
+    map_term(~f_exp=f, ~f_pat=f, ~f_typ=f, ~f_tpat=f, ~f_rul=f),
+    Typ.map_term(~f_exp=f, ~f_pat=f, ~f_typ=f, ~f_tpat=f, ~f_rul=f),
   );
+};
 
 // TODO: make this function emit a map of changes
 let repair_ids =
@@ -34,6 +36,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);
+        },
     _,
   );
 

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 =
@@ -132,7 +113,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);
@@ -144,3 +125,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})
+    }
+  };