Merge branch 'projectors-live' of github.com:hazelgrove/hazel into cards

docs/stepper-and-filter.md

@@ -109,7 +109,7 @@ program, issue command for change the evaluation mode (big-step or
 small-step, lazy or eager), and a narrower filter has a higher priority.
 
 For the matching part, I choose the Hazel language it's self as the
-pattern language. `UPat` and `DHPat` won't work since they only matches
+pattern language. `Pat` and `DHPat` won't work since they only matches
 against *values*, indicating I have to extend them somehow so that they
 can match against *expressions*. The empty hole is take as the
 match all filter, i.e. `*` in many other matching languages. It will

dune-project

@@ -1,4 +1,5 @@
 (lang dune 3.16)
+
 (using menhir 2.0)
 
 (name hazel)
@@ -9,15 +10,17 @@
  (github hazelgrove/hazel))
 
 (authors "Hazel Development Team")
+
 (maintainers "Hazel Development Team")
 
 (license MIT)
 
 (package
  (name hazel)
  (allow_empty)
- (synopsis "Hazel, a live functional programming environment with typed holes")
-;  (description "A longer description")
+ (synopsis
+  "Hazel, a live functional programming environment with typed holes")
+ ;  (description "A longer description")
  ; (tags
  ; (topics "to describe" your project))
  (depends
@@ -26,20 +29,31 @@
   (menhir
    (>= 2.0))
   yojson
-  (reason (>= 3.12.0))
+  (reason
+   (>= 3.12.0))
   ppx_yojson_conv_lib
   ppx_yojson_conv
   incr_dom
   bisect_ppx
-  (omd (>= 2.0.0~alpha4))
+  (omd
+   (>= 2.0.0~alpha4))
   ezjs_idb
   bonsai
   ppx_deriving
   ptmap
-  (uuidm (= 0.9.8)) ; 0.9.9 has breaking deprecated changes
+  (uuidm
+   (= 0.9.8)) ; 0.9.9 has breaking deprecated changes
   unionFind
   ocamlformat
-  (junit_alcotest :with-test)
-  ocaml-lsp-server)) ; After upgrading to opam 2.2 use with-dev https://opam.ocaml.org/blog/opam-2-2-0/
+  (junit_alcotest
+   (and
+    (>= 2.1.0)
+    :with-test))
+  ocaml-lsp-server
+  qcheck
+  qcheck-alcotest
+  ppx_deriving_qcheck))
+
+; After upgrading to opam 2.2 use with-dev https://opam.ocaml.org/blog/opam-2-2-0/
 
 ; See the complete stanza docs at https://dune.readthedocs.io/en/stable/reference/dune-project/index.html

licenses/Icons.md

@@ -0,0 +1 @@
+The icons used in Hazel, including the Hazel icon, are from The Noun Project (https://thenounproject.com/) under the Icon Pro license (https://thenounproject.com/legal/terms-of-use/#icon-licenses).

src/haz3lcore/dynamics/Builtins.re

@@ -1,3 +1,4 @@
+open Util;
 open DHExp;
 
 /*
@@ -12,13 +13,13 @@ open DHExp;
 [@deriving (show({with_path: false}), sexp)]
 type builtin =
   | Const(Typ.t, DHExp.t)
-  | Fn(Typ.t, Typ.t, DHExp.t => DHExp.t);
+  | Fn(Typ.t, Typ.t, DHExp.t => option(DHExp.t));
 
 [@deriving (show({with_path: false}), sexp)]
 type t = VarMap.t_(builtin);
 
 [@deriving (show({with_path: false}), sexp)]
-type forms = VarMap.t_(DHExp.t => DHExp.t);
+type forms = VarMap.t_(DHExp.t => option(DHExp.t));
 
 type result = Result.t(DHExp.t, EvaluatorError.t);
 
@@ -29,7 +30,7 @@ let fn =
       name: Var.t,
       t1: Typ.term,
       t2: Typ.term,
-      impl: DHExp.t => DHExp.t,
+      impl: DHExp.t => option(DHExp.t), // None if indet
       builtins: t,
     )
     : t =>
@@ -51,17 +52,17 @@ module Pervasives = {
 
     let unary = (f: DHExp.t => result, d: DHExp.t) => {
       switch (f(d)) {
-      | Ok(r') => r'
-      | Error(e) => EvaluatorError.Exception(e) |> raise
+      | Ok(r') => Some(r')
+      | Error(_) => None
       };
     };
 
     let binary = (f: (DHExp.t, DHExp.t) => result, d: DHExp.t) => {
       switch (term_of(d)) {
       | Tuple([d1, d2]) =>
         switch (f(d1, d2)) {
-        | Ok(r) => r
-        | Error(e) => EvaluatorError.Exception(e) |> raise
+        | Ok(r) => Some(r)
+        | Error(_) => None
         }
       | _ => raise(EvaluatorError.Exception(InvalidBoxedTuple(d)))
       };
@@ -71,8 +72,8 @@ module Pervasives = {
       switch (term_of(d)) {
       | Tuple([d1, d2, d3]) =>
         switch (f(d1, d2, d3)) {
-        | Ok(r) => r
-        | Error(e) => EvaluatorError.Exception(e) |> raise
+        | Ok(r) => Some(r)
+        | Error(_) => None
         }
       | _ => raise(EvaluatorError.Exception(InvalidBoxedTuple(d)))
       };
@@ -308,6 +309,8 @@ module Pervasives = {
   };
 
   open Impls;
+
+  // Update src/haz3lmenhir/Lexer.mll when any new builtin is added
   let builtins =
     VarMap.empty
     |> const("infinity", Float, infinity)

src/haz3lcore/dynamics/DHPat.re

@@ -3,32 +3,3 @@ include Pat;
 /* A Dynamic Pattern (DHPat) is a pattern that is part of an expression
    that has been type-checked. Hence why these functions take both a
    pattern, dp, and an info map, m, with type information. */
-
-/**
- * Whether dp contains the variable x outside of a hole.
- */
-let rec binds_var = (m: Statics.Map.t, x: Var.t, dp: t): bool =>
-  switch (Statics.get_pat_error_at(m, rep_id(dp))) {
-  | Some(_) => false
-  | None =>
-    switch (dp |> term_of) {
-    | EmptyHole
-    | MultiHole(_)
-    | Wild
-    | Invalid(_)
-    | Int(_)
-    | Float(_)
-    | Bool(_)
-    | String(_)
-    | Constructor(_) => false
-    | Cast(y, _, _)
-    | Wrap(y, _) => binds_var(m, x, y)
-    | Var(y) => Var.eq(x, y)
-    | Tuple(dps) => dps |> List.exists(binds_var(m, x))
-    | Cons(dp1, dp2) => binds_var(m, x, dp1) || binds_var(m, x, dp2)
-    | ListLit(d_list) =>
-      let new_list = List.map(binds_var(m, x), d_list);
-      List.fold_left((||), false, new_list);
-    | Ap(_, _) => false
-    }
-  };

src/haz3lcore/dynamics/EvalCtx.re

@@ -33,12 +33,12 @@ type term =
   | Cast(t, Typ.t, Typ.t)
   | FailedCast(t, Typ.t, Typ.t)
   | DynamicErrorHole(t, InvalidOperationError.t)
-  | MatchScrut(t, list((UPat.t, DHExp.t)))
+  | MatchScrut(t, list((Pat.t, DHExp.t)))
   | MatchRule(
       DHExp.t,
-      UPat.t,
+      Pat.t,
       t,
-      (list((UPat.t, DHExp.t)), list((UPat.t, DHExp.t))),
+      (list((Pat.t, DHExp.t)), list((Pat.t, DHExp.t))),
     )
 and t =
   | Mark